Inaccessibility in constructive set theory and type theory Original Research Article

This paper is the first in a series whose objective is to study notions of large sets in the context of formal theories of constructivity. The two theories considered are Aczelʹs constructive set theory (CZF) and Martin-Löfʹs intuitionistic theory of types. This paper treats Mahloʹs π-numbers which give rise classically to the enumerations of inaccessibles of all transfinite orders. We extend the axioms of CZF and show that the resulting theory, when augmented by the tertium non-datur, is equivalent to ZF plus the assertion that there are inaccessibles of all transfinite orders. Finally, the theorems of that extension of CZF are interpreted in an extension of Martin-Löfʹs intuitionistic theory of types by a universe.