Erik Palmgren: A Constructive Examination of a Russell Style Ramified Type Theory

Explore a constructive examination of Russell-style ramified type theory in this 32-minute lecture from the Hausdorff Trimester Program: Types, Sets and Constructions. Delve into the natural interpretation of a ramified type hierarchy within Martin-Löf type theory, featuring an infinite sequence of universes. Discover how the predicative interpretation validates useful special cases of Russell's reducibility axiom, particularly functional reducibility, enabling the development of constructive mathematical analysis in Bishop's style. Examine a proposed ramified type theory designed for this purpose, offering an alternative solution to the proliferation of real number levels in Russell's theory while avoiding impredicativity and embracing constructive logic. Consider the implications of this intuitionistic ramified type theory, including its potential connection to a natural notion of predicative elementary topos.