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?
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