Mathematical logic seminar - October 20, 2005

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 <ε₀-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 <ε₀-recursive functions of integers. This result has many interesting consequences, including a new characterization of Gödel's theory Τ.