10
$\begingroup$

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 Answers 1

5

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].

1: http://www.jstor.org/stable/2266967

  • 0
    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).2012-11-22
  • 1
    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).2012-11-22
  • 0
    @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.2012-11-22
  • 0
    Thanks for this. It would be striking indeed if this is the first explicit statement (some 20 years later than you might have expected??).2012-11-22