Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
4661749 | Annals of Pure and Applied Logic | 2014 | 16 Pages |
Let IΠ2− denote the fragment of Peano Arithmetic obtained by restricting the induction scheme to parameter free Π2Π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≥0n≥0. In particular, we derive a new conservation result for these theories, namely that IΠn+1− is Πn+2Πn+2-conservative over IΣnIΣn for each n≥1n≥1.