A Simple Proof of Parsons' Theorem
Fernando A.F. Ferreira · Notre Dame Journal of Formal Logic · 2005
Let $\mathsf{I\Sigma_1}$ be the fragment of elementary Peano arithmetic in which induction is restricted to $\Sigma_1$-formulas. More than three decades ago, Parsons showed that the provably total functions of $\mathsf{I\Sigma_1}$ are exactly the primitive recursive functions. In this paper, we observe that Parsons' result is a consequence of Herbrand's theorem concerning the $\exists \forall \exists$-consequences of universal theories. We give a self-contained proof requiring only basic knowledge of mathematical logic.