Injecting uniformities into Peano arithmetic

DOI10.1016/J.APAL.2008.09.004MaRDI QIDQ1006608zbMATH OpenOpenAlexFDO

Publication date 25 March 2009

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.apal.2008.09.004

arithmetic conservation functional interpretations uniformities

Functionals in proof theory (03F10) Relative consistency and interpretations (03F25) First-order arithmetic and fragments (03F30) Second- and higher-order arithmetic and fragments (03F35)

Review text

The theory \(\mathsf{PA}^{\omega}_{\leq}\) extends Gödel's \(\mathsf{T}\) by a rule-governed (intensional) majorizability relation \(\leq\). This article provides a bounded functional interpretation of \(\mathsf{PA}^{\omega}_{\leq}\) into itself which only cares for bounds for witnesses of existential statements. Due to its simplicity, it is evident that principles such as Monotone Bounded Choice, Bounded Collection and Majorizability Axioms can be added to \(\mathsf{PA}^{\omega}_{\leq}\) without increasing the provable \(\forall\exists\)-sentences of the language of \(\mathsf{PA}^{\omega}_{\leq}\). As an illustrative application, it is shown that the extension of \(\mathsf{PRA}^{\omega}_{\leq}\) by the three aforementioned principles contains the subsystem \(\mathsf{WKL}_0\) of second-order arithmetic, which thus is conservative over \(\mathsf{RCA}_0\) for \(\Pi^0_2\)-sentences.

Recommendations

Cites work

Cited in

(16)

This page was built for publication: Injecting uniformities into Peano arithmetic

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