Frege: Frege's Theorem

It has long been known that in the context of axiomatic second-order logic (SOL), Hume's Principle (HP) is mutually interpretable with "the universe is Dedekind infinite" (DI). I offer a more fine-grained analysis of the logical strength of HP, measured by deductive implications rather than interpretability. The main result is that HP is not deductively conservative over SOL + DI. That is, SOL + HP proves additional theorems in the language of pure second-order logic that are not provable from SOL (...) + DI alone. Arguably, then, HP is not just a pure axiom of infinity, but rather it carries additional logical content. On the other hand, I show that HP is $\Pi^1_1$ conservative over SOL + DI, and that HP is conservative over SOL + DI + "the universe is well ordered" (WO). Next, I show that SOL + HP does not prove any of the simplest and most natural versions of the axiom of choice, including WO and weaker principles. Lastly, I discuss other axioms of infinity. I show that HP does not prove the Splitting or Pairing principles (axioms of infinity stronger than DI). (shrink)

It has been known for a few years that no more than Pi-1-1 comprehension is needed for the proof of "Frege's Theorem". One can at least imagine a view that would regard Pi-1-1 comprehension axioms as logical truths but deny that status to any that are more complex—a view that would, in particular, deny that full second-order logic deserves the name. Such a view would serve the purposes of neo-logicists. It is, in fact, no part of my view that, say, (...) Delta-3-1 comprehension axioms are not logical truths. What I am going to suggest, however, is that there is a special case to be made on behalf of Pi-1-1 comprehension. Making the case involves investigating extensions of first-order logic that do not rely upon the presence of second-order quantifiers. A formal system for so-called "ancestral logic" is developed, and it is then extended to yield what I call "Arché logic". (shrink)