Proof Theory and Meaning: on second order logic

“Proof Theory and Meaning: on second order logic,” pp 157–170 in Logica 2007 Yearbook, edited by Michal Pelis, Filosofia, 2008.

Second order quantification is puzzling. The second order quantifiers have natural and compelling inference rules, and they also have natural models. These do not match: the inference rules are sound for the models, but not complete, so either the proof rules are too weak or the models are too strong. Some, such as Quine, take this to be no real problem, since they take “second order logic” to be a misnomer. It is not logic but set theory in sheep’s clothing, so one would not expect to have a sound and complete axiomatisation of the theory.

I think that this judgement is incorrect, and in this paper I attempt to explain why. I show how on Nuel Belnap’s criterion for logicality, second order quantification can count as properly logic so-called, since the quantifiers are properly defined by their inference rules, and the addition of second order quantification to a basic language is conservative. With this notion of logicality in hand I then diagnose the incompleteness of the proof theory of second order logic in what seems to be a novel way.