A Constructive Examination of a Russell-style Ramified Type Theory
From MaRDI portal
Publication:6285822
DOI10.1017/BSL.2018.4arXiv1704.06812MaRDI QIDQ6285822FDOQ6285822
Authors: Erik Palmgren 
Publication date: 22 April 2017
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.
Metamathematics of constructive systems (03F50) Second- and higher-order arithmetic and fragments (03F35) Type theory (03B38)
This page was built for publication: A Constructive Examination of a Russell-style Ramified Type Theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6285822)
