Correspondence between Nuprl and the Ramified Theory of Types

摘要

In Russell's Ramified Theory of Types (RTT), two hierarchical concepts dominate:orders and types. Despite the disappearance of orders which have a strong correlation with predicativity, predicative logic still plays an influential role in Computer Science. An important example is the proof checker Nuprl, which is based on Martin Loe's Type Theory which uses type universes. Those type universes, and also degrees of expressions in AUTHOMATH, are closely related to orders. In this paper, we concentrate on Nuprl. We describe Nuprl as a Pure Type System and relate it to Russell's RTT. To be successful at so doing, we are forced to explicitly typing Nuprl (but this is not restrictive). We show also that Russell's orders play a crucial role in understanding the hierarchy of Nuprl.