Ordinals in Type Theory

If a type system for functional programming ensures that evaluation of properly typed expressions terminates, and the type system is decidable, then the type system is necessarily incomplete. This is an expression of the unsolvability of the halting problem. Very roughly, one can measure the incompleteness of such a type system with a countable ordinal -- the supremum of those that can be expressed with properly typed expressions. This has been extensively studied for almost 70 years, since Gentzen. Together with P. Hancock and A. Setzer we have been analysing the ordinals of systems such as Martin-Lof Type Theory with one universe. While the ordinal of this system is known (P. Aczel), the proofs that it is the correct ordinal are very indirect. We have been working on a direct construction of this ordinal, and introduces the notion of lenses for this purpose. This has been presented as an invited lecture at the CSL meeting, August 1997.

We also intend to develop a natural representation of ordinals as iterative sets (which model Aczel's constructive version of Zermelo-Fraenkel Set Theory following an idea of Herman Jervell.

Last modified: Thu May 28 13:01:00 MET DST 1998