# An example of a totally computable function that is not definable in system T?

Could you give me an example of a totally computable function of type N × N → N that is not definable in System T? Thanks.

• I think this needs to be edited. "nat ⨯ nat → nat" does not make sense. Did you mean $\mathbb{N} \times \mathbb{N} \to \mathbb{N}$? – M.S. Dousti Nov 30 '10 at 21:25

Concretely, fix a Godel encoding, and then let $f$ be the function which takes a pair consisting of a Godel-encoding of a closed term of type $\mathbb{N} \to \mathbb{N}$, and a natural number in $\mathbb{N}$, and returns the value of the application. This function is not definable in T. It's a worthwhile exercise to work out how you can use a self-interpreter to define an infinitely looping program.
Gödel'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 $\epsilon$-recursive functions of non-negative integers. But it is not well-known which functionals of arbitrary type can be defined in T. We show that when the domain and codomain are restricted to pure closed normal forms, the functionals of arbitrary type that are definable in T are exactly those functionals that can be encoded as $\epsilon$-recursive functions of non-negative integers. This result has many interesting consequences, including a new characterization of T.