On the definability of functionals in Gödel's theory T
Matthew P. Szudzik · arXiv (Cornell University) · 2010
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 S, and the operator R_tau for primitive recursion on objects of type tau. It is known that the functions from non-negative integers to non-negative integers that can be defined in this theory are exactly the