Erik Palmgren: Intuitionistic Ramified Type Theory
Time: Wed 2017-03-01 10.00 - 11.45
Location: Room 22, building 5, Kräftriket, Department of Mathematics, Stockholm University
Participating: Erik Palmgren
Abstract: In this talk we examine the natural interpretation of a ramified type hierarchy into Martin-Löf type theory with an infinite sequence of universes. It is shown that under this interpretation some useful special cases of Russell's reducibility axiom are valid. This is enough to make the type hierarchy usable for development of constructive mathematics. We present a ramified type theory IRTT suitable for this purpose. IRTT allows for all the basic set-theoretic constructions.