Consistency statements and iterations of computable functions in \(\mathrm{I}\Sigma_1\) and PRA (Q711565)

The paper is devoted to the interrelations between two weak systems of arithmetic: PRA (= primitive recursive arithmetic) and I\(\Sigma_{1}\) (= Robinson's arithmetic Q plus the \(\Sigma_{1}\)-induction rule). A characterization of I\(\Sigma_{1}\) in terms of PRA and iterations of a class of functions is given. In particular, it is shown that PRA is closed under iterations of these functions whereas I\(\Sigma_{1}\) is provably closed under iteration. A sufficient condition for a model of PRA to be a model of I\(\Sigma_{1}\) is given. This enables the author to give a model-theoretic proof of Parson's theorem stating that I\(\Sigma_{1}\) is \(\Pi_{2}\) conservative over PRA. A purely syntactical proof of Parson's theorem is also given. It is also shown that I\(\Sigma_{1}\) proves the consistency of PRA on a definable I\(\Sigma_{1}\)-cut. A consequence of this is the fact that proofs in I\(\Sigma_{1}\) can have non-elementary speed up over proofs in PRA.