Local induction and provably total computable functions: A case study

Abstract

Let I Π 2- denote the fragment of Peano Arithmetic obtained by restricting the induction scheme to parameter free Π 2 formulas. Answering a question of R. Kaye, L. Beklemishev showed that the provably total computable functions (p.t.c.f.) of I Π 2- are, precisely, the primitive recursive ones. In this work we give a new proof of this fact through an analysis of the p.t.c.f. of certain local versions of induction principles closely related to I Π 2-. This analysis is essentially based on the equivalence between local induction rules and restricted forms of iteration. In this way, we obtain a more direct answer to Kaye's question, avoiding the metamathematical machinery (reflection principles, provability logic,...) needed for Beklemishev's original proof. © 2012 Springer-Verlag.