Injecting uniformities into Peano arithmetic (Q1006608)

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.