Article
Local induction and provably total computable functions
Author/s | Cordón Franco, Andrés
Lara Martín, Francisco Félix |
Department | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial |
Publication Date | 2014 |
Deposit Date | 2019-06-24 |
Published in |
|
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 ... 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. |
Project ID. | MTM2008–06435
MTM2011–26840 |
Citation | Cordón Franco, A. y Lara Martín, F.F. (2014). Local induction and provably total computable functions. Annals of Pure and Applied Logic, 165 (9), 1429-1444. |
Files | Size | Format | View | Description |
---|---|---|---|---|
cie-2014.pdf | 223.3Kb | [PDF] | View/ | |