Ponencia
Provably Total Primitive Recursive Functions: Theories with Induction
Autor/es | Cordón Franco, Andrés
Fernández Margarit, Alejandro Lara Martín, Francisco Félix |
Departamento | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial |
Fecha de publicación | 2004 |
Fecha de depósito | 2019-06-28 |
Publicado en |
|
ISBN/ISSN | 978-3-540-23024-3 0302-9743 |
Resumen | A natural example of a function algebra is R (T), the class of provably total computable functions (p.t.c.f.) of a theory T in the language of first order Arithmetic. In this paper a simple characterization of that kind ... A natural example of a function algebra is R (T), the class of provably total computable functions (p.t.c.f.) of a theory T in the language of first order Arithmetic. In this paper a simple characterization of that kind of function algebras is obtained. This provides a useful tool for studying the class of primitive recursive functions in R (T). We prove that this is the class of p.t.c.f. of the theory axiomatized by the induction scheme restricted to (parameter free) Δ1(T)–formulas (i.e. Σ1–formulas which are equivalent in T to Π1–formulas). Moreover, if T is a sound theory and proves that exponentiation is a total function, we characterize the class of primitive recursive functions in R (T) as a function algebra described in terms of bounded recursion (and composition). Extensions of this result are related to open problems on complexity classes. We also discuss an application to the problem on the equivalence between (parameter free) Σ1–collection and (uniform) Δ1–induction schemes in Arithmetic. The proofs lean upon axiomatization and conservativeness properties of the scheme of Δ1(T)–induction and its parameter free version. |
Cita | Cordón Franco, A., Fernández Margarit, A. y Lara Martín, F.F. (2004). Provably Total Primitive Recursive Functions: Theories with Induction. En CSL 2004: 18th International Workshop on Computer Science Logic (355-369), Karpacz, Poland: Springer. |
Ficheros | Tamaño | Formato | Ver | Descripción |
---|---|---|---|---|
Provably Total Primitive.pdf | 342.1Kb | [PDF] | Ver/ | |