Ramified Frege arithmetic

DOI10.1007/S10992-010-9158-YMaRDI QIDQ766295zbMATH OpenOpenAlexFDO

Publication date 23 March 2012

Published in Journal of Philosophical Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10992-010-9158-y

Frege arithmetic ramified second-order logic second-order arithmetic

Philosophical and critical aspects of logic and foundations (03A05) Second- and higher-order arithmetic and fragments (03F35)

Review text

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.

Recommendations

Cites work

Cited in

(8)

This page was built for publication: Ramified Frege arithmetic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q766295)