Ordinal analysis and the set existence property for intuitionistic set theories

On account of being governed by constructive logic, intuitionistic theories [Formula: see text] often enjoy various existence properties. The most common is the numerical existence property (NEP). It entails that an existential theorem of [Formula: see text] of the form [Formula: see text] can be witnessed by a numeral [Formula: see text] such that [Formula: see text] proves [Formula: see text]. While NEP holds almost universally for natural intuitionistic set theories, the general existence property (EP), i.e. the property of a theory that for every existential theorem, a provably definable witness can be found, is known to fail for some prominent intuitionistic set theories such as Intuitionistic Zermelo–Fraenkel set theory (IZF) and constructive Zermelo–Fraenkel set theory (CZF). Both of these theories are formalized with collection rather than replacement as the latter is often difficult to apply in an intuitionistic context because of the uniqueness requirement. In light of this, one is clearly tempted to single out collection as the culprit that stymies the EP in such theories. Beeson stated the following open problem: ‘Does any reasonable set theory with collection have the existence property? and added in proof: The problem is still open for IZF with only bounded separation.’ (Beeson. 1985 Foundations of constructive mathematics, p. 203. Berlin, Germany: Springer.) In this article, it is shown that IZF with bounded separation, that is, separation for formulas in which only bounded quantifiers of the forms [Formula: see text] are allowed, indeed has the EP. Moreover, it is also shown that CZF with the exponentiation axiom in place of the subset collection axiom has the EP. Crucially, in both cases, the proof involves a detour through ordinal analyses of infinitary systems of intuitionistic set theory, i.e. advanced techniques from proof theory. This article is part of the theme issue ‘Modern perspectives in Proof Theory’.