The definability of functionals in Godel's theory T

Matthew Szudzik

Abstract:
Godel's theory T 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_sigma for primitive recursion on
objects of type sigma.  It is known that the functions from integers to
integers that can be defined in this theory are exactly the
<epsilon_0-recursive functions of integers.  But it is not well-known
which FUNCTIONALS of arbitrary type can be defined in Godel's theory T. 
We show that when the domain and codomain are restricted to pure, closed
lambda-terms, the functionals of arbitrary type that are definable in
Godel's theory T are exactly those functionals that can be encoded as
<epsilon_0-recursive functions of integers.  This result has many
interesting consequences, including a new characterization of Godel's
theory T.