Inaccessible set axioms may have little consistency strength Original Research Article

The paper investigates inaccessible set axioms and their consistency strength in constructive set theory. In View the MathML source inaccessible sets are of the form View the MathML source where κ is a strongly inaccessible cardinal and View the MathML source denotes the κth level of the von Neumann hierarchy. Inaccessible sets figure prominently in category theory as Grothendieck universes and are related to universes in type theory. The objective of this paper is to show that the consistency strength of inaccessible set axioms heavily depend on the context in which they are embedded. The context here will be the theory View the MathML source of constructive Zermelo–Fraenkel set theory but without ∈-Induction (foundation). Let View the MathML source be the statement that for every set there is an inaccessible set containing it. View the MathML source is a mathematically rich theory in which one can easily formalize Bishop style constructive mathematics and a great deal of category theory. View the MathML source also has a realizability interpretation in type theory which gives its theorems a direct computational meaning. The main result presented here is that the proof theoretic ordinal of View the MathML source is a small ordinal known as the Feferman–Schütte ordinal View the MathML source.