Speaker:  Matthew Szudzik Department of Mathematical Sciences Carnegie Mellon University 

Title:  The Definability of functionals in Gödel's theory Τ 

Abstract: 
Gödel's theory Τ can be understood as a theory of the simplytyped 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 wellknown 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 lambdaterms, 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 Τ.