A theory of rules for enumerated classes of functions

Archive for Mathematical Logic 34 (1):47-63 (1995)
  Copy   BIBTEX


We define an applicative theoryCL 2 similar to combinatory logic which can be interpreted in classes of functions possessing an enumerating function. In contrast to the models of classical combinatory logic, it is not necessarily assumed that the enumerating function itself belongs to that function class. Thereby we get a variety of possible models including e. g. the classes of primitive recursive, recursive, elementary, polynomial-time comptable ofɛ 0-recursive functions.We show that inCL 2 a major part of the metatheory of enumerated classes of functions can be developed. Namely, a kind of λ-abstraction can be defined and abstract versions of theS n m - and (Primitive) Recursion Theorems are proved. Thereby, a closer analysis of the phenomenon of the different recursion theorems is achieved.A theory closely related toCL 2 can be used to replace the applicative part of Feferman's theories for explicit mathematics. So this work can be seen as an answer to Feferman's question to formulate a theory for explicit mathematics in which operations can be interpreted as primitive recursive or even more feasible ones.Finally it is shown that the proof-theoretical strength of various theoreies for explicit mathematics is preserved when replacing the applicative part of the theories by our theory together with an operation for primitive recursion



    Upload a copy of this work     Papers currently archived: 92,150

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

Unary primitive recursive functions.Daniel E. Severin - 2008 - Journal of Symbolic Logic 73 (4):1122-1138.
Accessible recursive functions.Stanley S. Wainer - 1999 - Bulletin of Symbolic Logic 5 (3):367-388.
On nested simple recursion.Ján Komara - 2011 - Archive for Mathematical Logic 50 (5-6):617-624.
Ramsey's Theorem for Pairs and Provably Recursive Functions.Alexander Kreuzer & Ulrich Kohlenbach - 2009 - Notre Dame Journal of Formal Logic 50 (4):427-444.
Classical recursion theory: the theory of functions and sets of natural numbers.Piergiorgio Odifreddi - 1989 - New York, N.Y., USA: Sole distributors for the USA and Canada, Elsevier Science Pub. Co..
Polynomial time operations in explicit mathematics.Thomas Strahm - 1997 - Journal of Symbolic Logic 62 (2):575-594.
Subrecursive functions on partial sequences.Karl-Heinz Niggl - 1999 - Archive for Mathematical Logic 38 (3):163-193.


Added to PP

13 (#1,039,612)

6 months
2 (#1,203,746)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

Truth, Pretense and the Liar Paradox.Bradley Armour-Garb & James A. Woodbridge - 2015 - In T. Achourioti, H. Galinon, J. Martínez Fernández & K. Fujimoto (eds.), Unifying the Philosophy of Truth. Dordrecht: Imprint: Springer. pp. 339-354.

Add more citations

References found in this work

The lambda calculus: its syntax and semantics.Hendrik Pieter Barendregt - 1981 - New York, N.Y.: Sole distributors for the U.S.A. and Canada, Elsevier Science Pub. Co..
A well-ordering proof for Feferman's theoryT 0.Gerhard Jäger - 1983 - Archive for Mathematical Logic 23 (1):65-77.
Foundations of Constructive Mathematics.Michael J. Beeson - 1987 - Studia Logica 46 (4):398-399.
Understanding uniformity in Feferman's explicit mathematics.Thomas Glaß - 1995 - Annals of Pure and Applied Logic 75 (1-2):89-106.

Add more references