Two proofs of Parsons' Theorem

Abstract

It is well-known that IΣ1 is ΙΙ2-conservative over PRA. This fact is often referred to as Parsons’ theorem. In this paper we provide two proofs of the theorem. One is proof-theoretic and easily formalizable. The other proof is model-theoretic. The main ingredient of the second proof is a characterization of IΣ1 in terms of provable closure under the iteration operation on functions.