Repositorio de producción científica de la Universidad de Sevilla

Local induction and provably total computable functions

 

Advanced Search
 
Opened Access Local induction and provably total computable functions
Cites

Show item statistics
Icon
Export to
Author: 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
Date: 2014
Published in: Annals of Pure and Applied Logic, 165 (9), 1429-1444.
Document type: Article
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.
Cite: 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.
Size: 223.3Kb
Format: PDF

URI: https://hdl.handle.net/11441/87547

DOI: 10.1016/j.apal.2014.04.012

See editor´s version

This work is under a Creative Commons License: 
Attribution-NonCommercial-NoDerivatives 4.0 Internacional

This item appears in the following Collection(s)