Sigh. Glancing through Chapter 22 of my Gödel book late last night, my eye was caught by a sentence on p. 197. I stared in disbelief. It says that ACA0 is the second-order theory you get when you restrict the φ(x) we can substitute into the Comprehension Scheme to those which lack second-order quantifiers. That’s fine. But there in four black and white words it also says — as if it is the same thing — that the φ(x) must belong to LA (the language of first-order arithmetic). Which is of course plain wrong. The φ(x) might contain second-order free variables/parameters.
Aaargghh! How on earth did that stray false clause get in? Checking an earlier version of the book, it wasn’t there: so it must have been a later ‘helpful’ addition!
The psychology of this kind of “thinko” (I can hardly plead that it is a typo!) is intriguing. How is it possible to write, and then no doubt let pass on another reading or two, something you know perfectly well to be false? Sigh.