New paper: A constructive examination of a Russell-style ramified type theory

[Erik Palmgren]

This paper may perhaps be of interest to some
readers of this list. In a nutshell: What if Russell had
gone intuitionistic instead of impredicative?


A constructive examination of a Russell-style ramified type theory

Erik Palmgren

Abstract. In this paper 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 predicative
interpretation some useful special cases of Russell’s reducibility axiom
are valid, namely functional reducibility. This is sufficient to make
the type hierarchy usable for development of constructive mathematics.
We present a ramified type theory suitable for this purpose. One may
regard the results of this paper as an alternative solution to the
problems of Russell’s theory, which avoids impredicativity, but instead
imposes constructive logic.

Full paper:

http://staff.math.su.se/palmgren/CERRTT.pdf