Marcus Rossberg – Non-Conservativeness in Higher-Order Logic
The Montreal Inter-University Workshop on the History and Philosophy of Mathematics presents:
Marcus Rossberg (Connecticut):
Non-Conservativeness in Higher-Order Logic
Friday, March 12, 2010
McGill University, Leacock Building, Room 927. 3:30-5:00pm
Abstract: I present a new difficulty that proof-theoretic approaches to a theory of meaning face. I show that third-order logic is not conservative over second-order logic: there are sentences formulated in pure second-order logic that are theorems of third-order logic, but cannot be proven in second-order logic. The proof is a corollary of the definability of a truth predicate for second-order arithmetic in third- order logic, that has until now escape attention. The challenge is that this inability to demonstrate the truth of such second-order sentences using the operational rules of second-order logic alone seems to refute the claim of proof-theoretic semantics that the meaning of the quantifiers is determined by their introduction and elimination rules: such sentences — being truths of third-order logic — should be true in virtue of the meaning of the logical vocabulary. An investigation of the Henkin models for higher-order logic suggests, perhaps surprisingly, that the meaning of the second- and higher-order quantifier is determined by their introduction and elimination rules after all.