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