# Who first explicitly noted that second-order logic is unaxiomatizable?

As every student now knows, second-order logical consequence is unaxiomatizable. (At least when we read the second-order quantifiers in the natural way, as running over all possible properties on the first-order domain).

Does anyone happen to know who, back in the glory days, was first really clear and explicit about this?

-

## 1 Answer

Leon Henkin stated this fact without reference in his 1950 paper in the JSL where he proved the completeness theorem for second-order logic in Henkin semantics [1].

-
I had a hunch the answer lies within this paper, but I couldn't find it in a quick review (and I would have never guessed that Henkin just stated this without proof, rather than the fact being known before that). – Asaf Karagila Nov 22 '12 at 16:32
Indeed, Henkin says "This follows from results of Godel concerning systems containing a theory of natural numbers, because a finite categorical set of axioms for the positive integers can be formulated within a second order calculus to which a functional constant has been added." So Henkin does does not give a reference, but he provides a proof (without the details, but it is quite clear this is a proof). – boumol Nov 22 '12 at 16:41
@Asaf: it is the second paragraph. Boumol has transcribed the argument Henkin gives, but the part I find more relevant to the question is the phrase "For the functional calculus of second order, ..., a very different kind of result is known". Textual analysis of mathematics is risky, but I think that the phrasing "is known" instead of "can be shown" indicates Henkin thought others were already familiar with the result. I think it is likely to have originated as a folk theorem. – Carl Mummert Nov 22 '12 at 17:12
Thanks for this. It would be striking indeed if this is the first explicit statement (some 20 years later than you might have expected??). – Peter Smith Nov 22 '12 at 20:04