Local induction and provably total computable functions

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 of I¦− 2 are, precisely, the primitive recursive ones. In this work we give a new proof of this fact through an analysis of certain local variants of induction principles closely related to I¦− 2 . 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. Our methods are model–theoretic and allow for a general study of I¦− n+1 for all n ¸ 0. In particular, we derive a new conservation result for these theories, namely that I¦− n+1 is ¦n+2–conservative over I§n for each n ¸ 1.