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

  • $\begingroup$ 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}$? $\endgroup$ – M.S. Dousti Nov 30 '10 at 21:25

Interpreters for T are not definable in T, thanks to the incompleteness theorem.

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.


This just appeared on arxive.org and may be of some help.

The definability of functionals in Gödel's theory T

Matthew P. Szudzik (Carnegie Mellon)

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.