Characterizing the elementary recursive functions by a fragment of Gödel's T

Archive for Mathematical Logic 39 (7):475-491 (2000)
  Copy   BIBTEX

Abstract

Let T be Gödel's system of primitive recursive functionals of finite type in a combinatory logic formulation. Let $T^{\star}$ be the subsystem of T in which the iterator and recursor constants are permitted only when immediately applied to type 0 arguments. By a Howard-Schütte-style argument the $T^{\star}$ -derivation lengths are classified in terms of an iterated exponential function. As a consequence a constructive strong normalization proof for $T^{\star}$ is obtained. Another consequence is that every $T^{\star}$ -representable number-theoretic function is elementary recursive. Furthermore, it is shown that, conversely, every elementary recursive function is representable in $T^{\star}$ .The expressive weakness of $T^{\star}$ compared to the full system T can be explained as follows: In contrast to $T$ , computation steps in $T^{\star}$ never increase the nesting-depth of ${\mathcal I}_\rho$ and ${\mathcal R}_\rho$ at recursion positions

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 76,442

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Elementary realizability.Zlatan Damnjanovic - 1997 - Journal of Philosophical Logic 26 (3):311-339.
A theory of rules for enumerated classes of functions.Andreas Schlüter - 1995 - Archive for Mathematical Logic 34 (1):47-63.
Recursive Analysis.R. L. Goodstein - 1961 - Dover Publications.
A note on da Costa-Doria “exotic formalizations”.L. Gordeev - 2010 - Archive for Mathematical Logic 49 (7-8):813-821.
Accessible recursive functions.Stanley S. Wainer - 1999 - Bulletin of Symbolic Logic 5 (3):367-388.
Unary primitive recursive functions.Daniel E. Severin - 2008 - Journal of Symbolic Logic 73 (4):1122-1138.

Analytics

Added to PP
2013-11-23

Downloads
61 (#197,152)

6 months
1 (#454,876)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Tiering as a recursion technique.Harold Simmons - 2005 - Bulletin of Symbolic Logic 11 (3):321-350.
Inductive definitions over a predicative arithmetic.Stanley S. Wainer & Richard S. Williams - 2005 - Annals of Pure and Applied Logic 136 (1-2):175-188.

Add more citations

References found in this work

Subrecursion: Functions and Hierarchies.H. E. Rose - 1984 - Oxford University Press.
The realm of primitive recursion.Harold Simmons - 1988 - Archive for Mathematical Logic 27 (2):177-188.
Subrecursion. Functions and Hierarchies.H. Schwichtenberg - 1987 - Journal of Symbolic Logic 52 (2):563-565.

Add more references