Abstract

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