Department of Mathematical Sciences
Carnegie Mellon University
|Title:||The Definability of functionals in Gödel's theory Τ||
Gödel's theory Τ can be understood as a theory of the simply-typed lambda calculus that is extended to include the constant 0, the successor function, and operators Rσ for primitive recursion on objects of type σ. It is known that the functions from integers to integers that can be defined in this theory are exactly the <ε0-recursive functions of integers. But it is not well-known which functionals of arbitrary type can be defined in Gödel's theory Τ. We show that when the domain and codomain are restricted to pure, closed lambda-terms, the functionals of arbitrary type that are definable in Gödel's theory Τ are exactly those functionals that can be encoded as <ε0-recursive functions of integers. This result has many interesting consequences, including a new characterization of Gödel's theory Τ.