The Pi_3-Reflecting Universe

Anton Setzer

(Swansea)

The research is part of a programme with the goal of extending Martin-Loef Type Theory (MLTT) in order to reach as much proof theoretic strength as possible. From a computer science point of view the hope is to find new data structures which can be used in general programming. Some of the ideas developed as part of this project (the Mahlo universe, see below) have already been used in order to develop a closed formalisation of inductive-recursive definitions. The use of this in generic programming is currently been explored by P. Dybjers, Marcin Benke and Patrik Jansson. In this talk we will first review the main principles of MLTT (universes and the W-type) which already allow us to reach considerable strength (Kripke-Platek set theory extended by one recursively inaccessible -- the notion of a recursively inaccessible will be explained in this talk). We then give some idea why we reach this strength. Then we will look at the Mahlo universe as developed by the author, which reaches the strength of one recursively Mahlo ordinal (a notion which will again be explained in the talk). Finally we look at how to design a theory the author conjectures to reach the strength of on Pi_3-reflecting-ordinal.
Tuesday 24th February 2004, 14:00
Robert Recorde Room
Department of Computer Science