Ramified Frege arithmetic (Q766295)

This is a contribution to the so-called neologicist program according to which Frege's logicist foundation of arithmetic can be vindicated on the ground of a consistent fragment of Frege's \textit{Grundgesetze der Arithmetik}, basically including second-order logic with full impredicative comprehension and the so-called Hume's principle HP (for a systematic survey and development see, e.g., \textit{J. P. Burgess}'s monograph [Fixing Frege. Princeton, NJ: Princeton University Press (2005; Zbl 1089.03001)]. HP states that two concepts have the same number if and only if they are in a 1-1 correspondence. Frege arithmetic is the system based upon full second-order logic and HP, and Frege's theorem is the statement that Frege arithmetic extends the Dedekind-Peano full second-order impredicative arithmetic. Recent investigations have considered the following problem: What is the weakest fragment of Frege's arithmetic where the axioms on zero, successor and natural numbers can be derived? In particular, is a predicative fragment of second-order comprehension sufficient? By a theorem of \textit{Ø. Linnebo} [Bull. Symb. Log. 10, No. 2, 153--174 (2004; Zbl 1068.03051)] the existence of the successor cannot be derived by means of predicative comprehension and essentially requires \(\Pi^1_1\)-comprehension. Also \(\Pi^1_1\)-comprehension is required for verifying the defining equations of addition and multiplication and in the proof of induction. Now the main result of the paper is that the ramified predicative theory does indeed prove the existence of an appropriate successor. Indeed, it is shown (Theorem 6.1) that the theory of zero and successor based on second-order ramified arithmetic can interpret Robinson's arithmetic Q and hence a significant fragment of first-order Peano arithmetic (i.e. \(\mathrm{I}\Delta_0(\mathrm{exp})\)). To sum up, in the end ``impredicative second-order reasoning is only needed for the proof of mathematical induction''.