# A Constructive Examination of a Russell-style Ramified Type Theory

## TL;DR

This paper explores a predicative, constructive interpretation of Russell's ramified type theory within Martin-Löf type theory, showing its usefulness for constructive mathematics and suggesting a related notion of predicative elementary topos.

## Contribution

It provides a constructive, predicative version of Russell's ramified type theory compatible with Martin-Löf type theory, avoiding impredicativity.

## Key findings

- Functional reducibility holds in the interpretation.
- The type hierarchy supports constructive mathematics.
- Suggests a natural notion of predicative elementary topos.

## Abstract

In this paper we examine the natural interpretation of a ramified type hierarchy into Martin-L\"of 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. The intuitionistic ramified type theory introduced here, also suggests that there is a natural associated notion of predicative elementary topos.