Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences
Open AccessResearch articles

Ordinal analysis and the set existence property for intuitionistic set theories

Michael Rathjen

Michael Rathjen

Department of Pure Mathematics, University of Leeds, Leeds LS2 9JT, UK

[email protected]

Contribution: Conceptualization, Writing – review & editing

Google Scholar

Find this author on PubMed

    Abstract

    On account of being governed by constructive logic, intuitionistic theories T often enjoy various existence properties. The most common is the numerical existence property (NEP). It entails that an existential theorem of T of the form (xN)A(x) can be witnessed by a numeral n¯ such that T proves A(n¯). 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 (xa),(xa),(xa),(xa) 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’.

    1. Introduction

    Intuitionistic theories are renowned for very desirable meta-mathematical properties, most prominently disjunction and existence properties. There are standard tools available to obtain these properties for Heyting arithmetic and theories with quantification over sets of natural numbers or the functions from Baire space (e.g. second-order arithmetic and function arithmetic), whereas set theories with their transfinite hierarchies of sets can raise formidable technical challenges.

    Definition 1.1.

    We will consider theories T the language of which, L(T) comprises the language of the set theory. Furthermore, to simplify matters, we shall assume that L(T) has a constant ω naming the set of von Neumann natural numbers, and for each n, there is a constant n¯ denoting the nth element of ω.

    (i)

    T has the disjunction property (DP), if whenever TAB holds for sentences A and B of T, then TA or TB.

    (ii)

    T has the numerical existence property (NEP), if whenever T(xω)A(x) holds for a formula A(x) with at most the free variable x, then TA(n¯) for some n.

    (iii)

    T has the existence property (EP), if whenever TxA(x) holds for a formula A(x) having at most the free variable x, then there is a formula C(x) with exactly x free, so that

    T!x[C(x)A(x)].

    While the DP and NEP hold for many intuitionistic set theories (even with choice principles) (see [1,–6]), verifying the EP poses considerably more difficult technical problems, provided the property holds at all. As Beeson wrote in his book [1, p. 202]:

    ‘It has turned out to be difficult to establish the existence property for constructive set theories, and new techniques have been developed for the purpose. From this perspective, the methods of this chapter [Chapter IX] [.] represent the frontier of knowledge in the subject of constructive set theory.’

    The history of the methods that Beeson is referring to has its roots in notions of realizability developed by Kleene. Friedman [2] developed realizability notions reminiscent of Kleene’s slash [7,8]. This tool was then extended and deployed to various intuitionistic set theories by Friedman and Myhill [3,4]. Myhill [3] showed that intuitionistic ZF, when based on replacement rather than collection (notated by IZFR from now on), has the EP. Myhill [4] did not answer the question whether the full EP still holds when one adds relativized dependent choice (RDC). Friedman & Ščedrov [9] subsequently showed this to be the case, i.e. IZFR+RDC also has the EP. Alas, none of the foregoing methods seemed to provide a tool to settle the question for set theories with collection. Then Friedman & Ščedrov [10] proved that Intuitionistic Zermelo–Fraenkel set theory (IZF) actually does not have the EP, and much later, Swan [11] showed, via a method entirely different from [10], that CZF also lacks the EP. Beeson in [1, p. 2003] 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.’ ([1, p. 203]).

    In this article, we describe a route that shows that Intuitionistic Zermelo–Fraenkel Set Theory with strong collection but bounded separation, i.e. separation for formulas in which only bounded quantifiers of the forms (xa),(xa),(xa)and(xa) are allowed, indeed has the EP. The latter theory is dubbed CZFP in this article. Moreover, it is also shown that constructive Zermelo–Fraenkel set theory with the exponentiation axiom in lieu of the subset collection axiom, CZFE, has the EP. The novel technical tool featuring in this article is the employment of ordinal analysis from the proof theory that allows one, in conjunction with the reductions established in [12], to overcome the difficulties posed by collection.

    A little signposting as to the contents of the article is in order. Section 2 features the weak existence property (wEP), which was researched in [12], and we review the main results of [12], notably that CZFP and CZFE possess the wEP. Moreover, [12] showed that these theories are partially conservative over their intuitionistic Kripke–Platek-like counterparts IKP(P) and IKP(E), respectively, and, moreover, that if they possess the EP for certain syntactically restricted classes of formulae, then the EP would hold for CZFP and CZFE tout court. This material will be reviewed in §2. Section 3 is devoted to a sketch of the ordinal analyses of IKP(P) and IKP(E). A crucial step in overcoming the problems with collection is the technique of collapsing infinite derivations whereby all instances of collection in the derivation are removed. Section 4 looks at the systems CZFP,R and CZFE,R that arise from CZFP and CZFE, respectively, by replacing the strong collection scheme by the replacement scheme. With the help of the ordinal analyses from §3, it is shown that CZFP and CZFE are conservative over their counterparts CZFP,R and CZFE,R for ΣP and ΣE formulae, respectively. Section 5 is concerned with demonstrating that CZFP,R and CZFE,R have the EP, using well-established technology. The final §6 then reaps the fruits of all the hard work, ascertaining that CZFP and CZFE have the EP, too.

    2. Preparations: from the weak to the strong existence property

    When investigating the EP problem, one is naturally drawn to investigate a related but weaker form, termed the weak existence property (wEP), defined in [12] by the relaxed requirement of finding, for every existential theorem, an inhabited and provably definable set of witnesses.

    Definition 2.1. ([12, Definition 1.2])

    Let T be a theory whose language, L(T), comprises the standard language of set theory.

    (i)

    T is said to have the wEP if whenever

    TxA(x),
    holds for a formula A(x) having at most the free variable x, then there is a formula C(x) with exactly x free, such that
    T!xC(x),Tx[C(x)uux]andTx[C(x)uxA(u)].

    (ii)

    A more general version of wEP allows for additional parameters. The uniform weak existence property (uwEP) is the following property: if

    TuxA(u,x)
    holds for a formula A(u,x) having at most the free variables u,x, then there is a formula C(u,x) with exactly u,x free, such that
    Tu!xC(u,x),Tux[C(u,x)zzx],andTux[C(u,x)zxA(u,z)].

    Clearly, uwEP subsumes wEP. As already pointed out in [12, proposition 1.3], IZF does not satisfy wEP either.

    Proposition 2.2.

    IZF does not have the weak existence property.

    Proof.

    According to ([10], theorem 1.1), IZF does not have the EP for some sentences of the form

    x[yD(y)yxD(y)].2.1
    Let E(x) be the part in square brackets of the previous formula. If wEP held for IZF, then one could find a formula C(u) such that IZF!uC(u)u[C(u)u inhabited] and IZFu[C(u)xuE(x)]. But then IZF!u[C(u)E(u)], contradicting the aforementioned theorem from [10].

    Note that formulae of the form (2.1) are readily deducible in IZF, using Collection and Separation. Thus, in light of Myhill’s result that IZFR has the EP, clearly collection is implicated in the failure of EP for IZF. It will turn out, however, that separation for formulae with unrestricted quantifiers is also responsible for this failure.

    There is another important intuitionistic set theory for which EP fails. Constructive Zermelo–Fraenkel set theory (CZF) was singled out by Aczel as a theory distinguished by the fact that it has canonical interpretation in Martin–Löf type theory (cf. [13]). While Myhill isolated the Exponentiation Axiom as the ‘correct’ constructive counterpart of the Power Set Axiom, CZF has an axiom scheme called Subset Collection (cf. [1315]), which is stronger than exponentiation.1 Subset collection implies exponentiation and is a consequence of powerset. In the presence of the other axioms of CZF, subset collection is equivalent to the fullness axiom (cf. [15, 5.1.2]). The latter stipulates that given any sets A and B, there exists a set C (called full) of multi-valued functions from A to B such that for every multi-valued function R from A to B, there exists SR with SC.2 Strength-wise, an enormous hiatus separates Exponentiation from Powerset. The fullness axiom simply decrees the existence of a full set. As there does not appear to exist a method to define a full set of multi-valued functions without invoking Powerset or choice (e.g. from NN to N), the current author conjectured that CZF is another example of a set theory lacking the wEP. This was later ascertained by Andrew Swan via an ingenious combination of three realizability models.

    Theorem 2.3. (Swan)

    CZF does not have the weak existence property.

    Proof.

    Swan, in [11], proves that CZF fails to have the EP. His counter-example is provided by the statement that there exists a full set of multi-valued functions from N to N. However, if CZF could prove that there exists a definable inhabited set D consisting entirely of full sets of multi-valued functions from N to N, then D would furnish a provably definable set of such multi-valued functions. Accordingly, CZF lacks the wEP, too.

    Clearly, wEP is an interesting property. The article [12] established that, as far as CZF is concerned, subset collection is the sole culprit for the failure of wEP. In it, several other important intuitionistic set theories with collection were shown to have the wEP, notably CZF based on exponentiation (rather than subset collection) as well as the strengthening of CZF with the powerset axiom.3 These theories will be delineated in detail in the next subsection.

    (a) The systems CZFE and CZFP

    CZF formulated with exponentiation, CZFE, has the same language as that of the classical Zermelo–Fraenkel set theory, the only non-logical symbol being . Its logic is intuitionistic first-order logic with equality. Its non-logical axioms include extensionality, pairing and union in their usual forms. The other axioms are the following.

    Infinity: xu[ux(=uvxu=v+1)] where v+1=v{v}.

    Set induction: x[yxC(y)C(x)]xC(x)

    Bounded separation: abx[xbxaC(x)]

    for all bounded formulae C. A set-theoretic formula is called bounded or restricted or Δ0 if its build-up from prime formulae uses only ¬,,,,xy and xy.

    Strong collection: for all formulae C,

    a[xayC(x,y)b[xaybC(x,y)ybxaC(x,y)]].
    Exponentiation: letting Fun(f,a,b) be short for the formula saying that f is a function from the set a to the set b, this is
    abcf(Fun(f,a,b)fc).
    For the much stronger system with the powerset axiom (Pow), added, i.e.
    xyz(zyzy),
    we use the acronym CZFP. Observe that both exponentiation and subset collection are implied by Pow (cf. [14, proposition 7.2]).

    (b) Intuitionistic Kripke–Platek-like set theories

    The proof theory of intuitionistic Kripke–Platek set theory (KP) and its beefed up versions via exponentiation and powerset, respectively, are a central tool for proving the results of this article. Recall (cf. [18]) that the axioms of the classical KP consist of extensionality, pair, union, infinity and bounded separation xu[ux(uaA(u))] for all bounded formulae A(u), bounded collection xayB(x,y)zxayzB(x,y) for all bounded formulae B(x,y) and set induction x[(yxC(y))C(x)]xC(x) for all formulae C(x).

    By IKP, we notate the intuitionistic version of KP. It will be important later to consider a version of IKP that uses Σ replacement in lieu of Δ0 collection. Σ replacement is the schema

    xa!yC(x,y)by[ybxaC(x,y)],2.2
    where C(x,y) is a Σ formula, i.e. a formula belonging to the smallest class of formulae containing the Δ0-formulae closed under , and the quantifiers uc,uc,v. By IKPR, we denote the variant of IKP based on Σ replacement instead of Δ0 collection. Since Σ replacement is provable in IKP (e.g. [14], theorem 11.7), IKPR is a subtheory of IKP.

    i Power and exponentiation Kripke–Platek set theory

    These theories come with a germane notion of bounded quantifier. Subset bounded quantifiers xy and xy are abbreviations for x(xy) and x(xy), respectively.

    A formula is said to be in Δ0P if all its quantifiers are of the form Qxy or Qxy, where Q is or and x and y are distinct variables.

    Let Fun(f,x,y) be an acronym for the bounded formula expressing that f is a function with domain x and co-domain y. Exponentiation bounded quantifiers fxy and fxy serve as abbreviations for f(Fun(f,x,y)) and x(Fun(f,x,y)), respectively.

    Definition 2.4.

    The class of Δ0P contains the atomic formulae and is closed under ,,,¬ and the quantifiers

    xa,xa,xa,xa.
    The class of Δ0E formulae contains the atomic formulae and is closed under ,,,¬ and the quantifiers
    xa,xa,fab,fab.

    Definition 2.5.

    IKP(E) has the same language and logic as IKP. Its axioms are extensionality, pairing, union, infinity, exponentiation, Δ0E-separation and Δ0E-collection.

    IKP(P) has the same language and logic as IKP. Its axioms are extensionality, pairing, union, infinity, powerset, Δ0P-separation and Δ0P-collection.

    The transitive classical models of IKP(P) are called power admissible sets in [19].

    An alternative way of axiomatizing IKP(P) proceeds by adding a function symbol P for the powerset function as a primitive symbol to the language and the axiom

    y[yP(x)yx],
    and allowing the new symbol to occur in the schemes of Δ0 separation and collection to the Δ0 formulae of this new language. Similarly, IKP(E) can be formulated by adding a primitive function symbol E for the exponentiation function.

    Lemma 2.6. ([12, lemma 2.4])

    Let CZF be CZF without subset collection. The following hold:

    (i)

    IKP is a subtheory of CZF;

    (ii)

    IKP(E) is a subtheory of CZFE;

    (iii)

    IKP(P) is a subtheory of CZFP.

    Note that the foregoing Lemma implies that, despite having just Δ0-separation at the axiomatic level, CZFE proves Δ0E-separation and CZFP proves Δ0P-separation.

    (c) Conservativity over intuitionistic Kripke–Platek set theories

    As shown in [12], CZF, CZFE and CZFP are conservative over their intuitionistic Kripke–Platek counterparts for syntactically restricted forms of formulae. These results will be of relevance later.

    The Σ formulae constitute an important syntactic class in the KP (cf. [18]). Their extensions to the contexts of IKP(E) and IKP(P) (singled out in [12], definition 2.5) are equally important.

    Definition 2.7.

    The Σ formulae are the smallest class of formulae containing the Δ0-formulae closed under , and the quantifiers xa,xa,x.

    The ΣE formulae are the smallest class of formulae containing the Δ0E-formulae closed under , and the quantifiers xa,xa,fab,fab,x.

    The ΣP formulae are the smallest class of formulae containing the Δ0P-formulae closed under , and the quantifiers xa,xa,xa,xa,x.

    Definition 2.8.

    We say that a formula D is Π2, Π2E or Π2P if it is of the form xyA(x,y) with A(x,y) being, respectively, Δ0, Δ0E and Δ0P.

    Theorem 2.9. ([12, theorem 4.8])

    (i)

    CZF is conservative over IKP for Π2 sentences.

    (ii)

    CZFE is conservative over IKP(E) for Π2E sentences.

    (iii)

    CZFP is conservative over IKP(P) for Π2P sentences.

    (d) Towards the existence property

    As it will turn out, a first crucial step towards establishing the EP was already achieved in [12]. To see this, though, it is fruitful to scour the details of the proofs leading to the following result.

    Theorem 2.10. ([12, theorem 3.10])

    IKP, IKP(E), IKP(P), CZF, CZFE and CZFP have the wEP. Indeed, they satisfy the stronger property uwEP.4

    A few comments as to the technology deployed in [12] are in order. The main tool consists of a notion of realizability where realizers are programs for various notions of set recursive functions (such functions were e.g. studied in [2023]), especially power and exponentiation recursive functions. Moreover, realizers for existential formulas consist of inhabited sets of realizers, and the notion of realizability is paired with that of truth. This notion is completely different from the generic realizability used by Beeson ([1], VIII.6) and McCarty [24] that has its roots in a notion of realizability for intuitionistic second-order arithmetic due to Kreisel & Troelstra [25]. The idea of using sets of realizers rather than single ones is akin to the Diller & Nahm [26,27] variant of Gödel’s functional interpretation.

    Let T be any of the theories CZF, CZFE or CZFP. According to [12], the goal of settling the EP for T can be achieved by tackling the perhaps more manageable question of whether the Kripke–Platek counterpart of T has the EP for Σ, ΣP and ΣE existential theorems, respectively.

    Definition 2.11.

    Let Ξ be a set of formulae. T is said to have the EP for Ξ if whenever TxA(x) for a sentence xA(x) with A(x) in Ξ, then one finds a formula C(x) (with at most x free) such that

    T!x[C(x)A(x)].
    In [12, definition 5.1], it was also required that C(x) belongs to Ξ. But this is not really necessary for the applications made in [12, theorems 5.2 and 5.3], and hence, we use the relaxed notion.

    Theorem 2.12. ([12, theorems 5.2, 5.3])

    (i)

    If IKP has the EP for Σ formulae, then IKP and CZF have the EP.

    (ii)

    If IKP(E) has the EP for ΣE formulae, then IKP(E) and CZFE have the EP.

    (iii)

    If IKP(P) has the EP for ΣP formulae, then IKP(P) and CZFP have the EP.

    In the cases of IKP and CZF, it has already been shown that the strategy suggested by theorem 2.12 can be successful. Theorem 6.1 will furnish yet another proof.

    Corollary 2.13.

    IKP and CZF have the EP.

    Proof.

    This result is stated as Corollary 6.1 in [12]. There is a sketch of a proof in [12], anticipating the ordinal analysis of IKP from [28]. More details are provided in the proofs of [28, theorem 2.35 and remark 2.36]. There it is shown that if IKPxC(x) for a Σ-sentence, then there is a cut-free proof of it in the infinitary proof system IRSΩ, which can then be milked to extract a term s¯ of IRSΩ and an ordinal representation α¯<Ω in BΩ(εΩ+1) such that IRSΩ proves C(s¯)Lα¯. The entire ordinal analysis of the infinitary proof can already be formalized in IKP. As a consequence, IKP proves that there is an ordinal α denoted by α¯ and a set s denoted by s¯ such that LαC(s). This is then also a fact provable in CZF, and thus, since CZF has the numerical EP by the proof of theorem 6.1 in [5] (just ignore the subset collection part), there are concrete such terms α¯,s¯ (note that terms of IRSΩ can be assumed to be coded as naturals), which can be described by Σ formulae, say B1(x) and B2(x). As a result, we have CZF!α!s[B1(α)B2(s)LαC(s)]. The latter being a Σ formula, it is also provable in IKP by theorem 2.9 (i). Hence, IKP has the EP for Σ formulae. In the light of theorem 2.12 (i), it follows that IKP and CZF have the EP.

    3. Ordinal analyses of Kripke–Platek-like intuitionistic set theories

    According to theorem 2.12, one could ascertain the EP for CZFE and CZFP, respectively, if one succeeded in establishing the EP for ΣE formulae for IKP(E) and the EP for ΣP formulae for IKP(P), respectively. The usual techniques for showing the EP (cf. [1], chapter IX), however, do not work for theories with collection. The ordinal-theoretic proof theory, though, has developed tools for eliminating collection axioms from proofs in infinitary proof systems, using intricate techniques for collapsing derivations. Originally, these techniques were developed for classical theories much weaker than IKP(P) [29,30]. An important step towards an ordinal analysis of the classical Power Kripke–Platek set theory was taken in [31]. A further important step was taken by Cook & Rathjen in [28], furnishing ordinal analyses of intuitionistic power and exponentiation Kripke–Platek set theory. Especially the treatment of the latter theory turned out to be wickedly complex. In the case of intuitionistic power Kripke–Platek set theory, one can base the infinitary proof system on a term structure where one can directly read off a term’s level in the power hierarchy. This is not possible in the pertinent ‘exponentiation hierarchy’. Instead, a term’s level is viewed as a changeable property within the infinitary system.

    The technical source for this chapter is the long article [28] (93 pages) by Cook & Rathjen. We will adumbrate its contents, not only for the reader's sake but also in order to extract some of its hidden implications.

    (a) Ordinal analysis of IKP(P)

    We first turn to IKP(P) because it is much simpler to deal with. In what follows, the proof system for IKP(P) will be the usual Gentzen sequent calculus for intuitionistic logic, which derives intuitionistic sequents of the form ΓΔ, where Γ and Δ are finite sets of formulae and Δ contains at most one formula.

    Definition 3.1.

    One formal point is that while previously subset bounded quantifiers

    (xa)A(x)and(xa)A(x)
    were viewed as abbreviations, here they are treated as quantifiers in their own right, not abbreviations. Accordingly, these quantifiers require their own logical rules.
    (pbL)Γ,abF(a)ΔΓ,(xb)F(x)Δ(pbR)ΓabF(a)Γ(xb)F(x)
    (pbL)Γ,abF(a)ΔΓ,(xb)F(x)Δ(pbR)ΓabF(a)Γ(xb)F(x)
    of course, where a is not to occur in the conclusion of the rules (pbL) and (pbR).

    (i) An ordinal representation system

    Following [28, definition 2.2], we provide a very brief description of a primitive recursive ordinal notation system for the Bachmann–Howard ordinal.

    Definition 3.2.

    Let Ω be a ‘big’ ordinal (in fact we could have chosen ω1CK, see [32]). We define the sets BΩ(α) and ordinals ψΩ(α) by transfinite recursion on α as follows:

    BΩ(α)={closureof{0,Ω}under:+,ξωξ(ξψΩ(ξ))ξ<α3.1
    and
    ψΩ(α)=min{ρ<Ω:ρBΩ(α)}.3.2

    As it turns out, ψΩ(α) is always defined, and therefore, ψΩ(α)<Ω. Furthermore, it is the case that letting BΩ(α)Ω:={αBΩ(α)α<Ω}, we have BΩ(α)Ω={ββ<ψΩ(α)}.

    Let εΩ+1 be the least ordinal η>Ω such that ωη=η. The set BΩ(εΩ+1) engenders a primitive recursive ordinal representation system [33,34]. The ubiquitous ordinal ψΩ(εΩ+1) is known as the Bachmann–Howard ordinal. In the literature, one finds several equivalent variants of the representation system for this ordinal.

    (ii) The infinitary system IRSΩP

    Next, we introduce the infinitary proof system IRSΩP from [28].

    Definition 3.3. ([28, Definition 2.3])

    All ordinals are assumed to be members of BΩ(εΩ+1). When defining the IRSΩP terms, we also assign an ordinal level, t.

    1.

    For each α<Ω, Vα is an IRSΩP term with Vα=α.

    2.

    For each α<Ω, we have infinitely many free variables a0α,a1α,a2α,., with aiα=α.

    3.

    If F(x,y¯) is a Δ0P-formula of IKP(P) (whose free variables are exactly those indicated) and s¯s1,,sn are IRSΩP terms, then the formal expression [xVαF(x,s¯)] is an IRSΩP term with [xVαF(x,s¯)]:=α.

    Note that IRSΩP-terms can contain subterms of a higher level, or from higher up the von Neumann hierarchy in the intended interpretation. This reflects the impredicativity of the power set operation. The IRSΩP formulae are of the form A(s1,,sn), where A(a1,,an) is a formula of IKP(P) with all free variables indicated and s1,,sn are IRSΩP terms. A formula A(s1,,sn) of IRSΩP is Δ0P if A(a1,,an) is a Δ0P formula of IKP(P).

    The Σ˙P formulae of IRSΩP are the smallest collection containing the Δ0P-formulae and containing AB, AB, (xs)A, (xs)A, (xs)A, (xs)A, xA, ¬C and CA whenever it contains A and B and C is a Π˙P-formula. The Π˙P-formulae are the smallest collection containing the Δ0P formulae and containing AB, AB, (xs)A, (xs)A, (xs)A, (xs)A, xA, ¬D and DA whenever it contains A and B and D is a Σ˙P-formula.5

    Following ([28], definition 3.2), the axioms of IRSΩP are as follows:

    (A1)

    Γ,AA for A in Δ0P.

    (A2)

    Γt=t.

    (A3)

    Γ,s1=t1,,sn=tn,A(s1,,sn)A(t1,,tn) for A(s1,,sn) in Δ0P.

    (A4)

    ΓsVα if s<α.

    (A5)

    ΓsVα if sα.

    (A6)

    Γ,t[xVαF(x,s¯)]F(t,s¯) for F(t,s¯) is Δ0P and t<α.

    (A7)

    Γ,F(t,s¯)t[xVαF(x,s¯)] for F(t,s¯) is Δ0P and t<α.

    The inference rules of IRSΩP are as follows:
    (bL)Γ,stF(s)ΔΓ,(xt)F(x)IΔ if s<t(bR)ΓstF(s) for all s<tΓ(xt)F(x)I(bL)Γ,stF(s)Δ for all s<tΓ,(xt)F(x)IΔ(bR)ΓstF(s)Γ(xt)F(x)I if s<t(pbL)Γ,stF(s)ΔΓ,(xt)F(x)IΔ if st(pbR)ΓstF(s) for all stΓ(xt)F(x)I(pbL)Γ,stF(s)Δ for all stΓ,(xt)F(x)IΔ(pbR)ΓstF(s)Γ(xt)F(x)I if st(L)Γ,F(s)ΔΓ,xF(x)IΔ
    (R)ΓF(s) for all sΓxF(x)I(L)Γ,F(s)Δ for all sΓ,xF(x)IΔ(R)ΓF(s)ΓxF(x)I(L)Γ,rtr=sΔ for all r<tΓ,stIΔ
    (R)Γrtr=sΓ,stI if r<t(L)Γ,rtr=sΔ for all rtΓ,stIΔ(R)Γrtr=sΓstI if rs
    (Cut) Γ,AΔΓAΓIΔ(Σ˙P-Ref)ΓAΓzAzII if A is a Σ˙P-formula, 
    as well as the rules (L), (R), (L), (R), (¬L), (¬R), (), (L) and (R) from IRSΩ. Here, as per usual, Az results from A by restricting all unbounded quantifiers to z.

    Definition 3.4.

    The rank of a formula is defined in ([28], definition 3.3) as follows.

    (i)

    rk(st):=max{s+1,t+1}.

    (ii)

    rk((xt)F(x)):=rk((xt)F(x)):=max{t,rk(F(V0))+2}.

    (iii)

    rk((xt)F(x)):=rk((xt)F(x)):=max{t+1,rk(F(V0))+2}.

    (iv)

    rk(xF(x)):=rk(xF(x)):=max{Ω,rk(F(V0))+2}.

    (v)

    rk(AB):=rk(AB):=rk(AB):=max{rk(A),rk(B)}+1.

    (vi)

    rk(¬A):=rk(A)+1.

    Crucially, observe that a formula with only bounded quantifiers has a rank <Ω, whereas a formula with an unbounded quantifier has a rank Ω.

    We take the notion of operator controlled derivability for IRSΩP from Definition 3.6 [28] (originally due to Buchholz [35]), where the relation H|αρΓΔ is defined for an operator H, ordinals α,ρ and ΓΔ, an intuitionistic sequent of IRSΩP formulae. We will just highlight the conditions for two crucial inferences.

    (Cut)H|α0ρΓ,BΔH|α0ρΓBH|αρΓΔα0<αrk(B)<ρ
    and
    (Σ˙P-Ref)H|α0ρΓAH|αρΓzAzα0+1,Ω<αA is a Σ˙Pformula

    (iii) Embedding IKP(P) into IRSΩP

    The first important result that links IKP(P) to IRSΩP is that every deduction in IKP(P) can be transformed into one in the infinitary system IRSΩP.

    Theorem 3.5. ([28, theorem 3.24])

    If IKP(P)Γ(a¯)Δ(a¯), where Γ(a¯)Δ(a¯) is an intuitionistic sequent containing exactly the free variables a¯=a1,,an, then there exists an m<ω (which we may calculate from the derivation) such that

    H[s¯]ΩωmΩ+mΓ(s¯)Δ(s¯),
    for any operator H and any IRSΩP terms s¯=s1,,sn.

    (iv) Cut elimination for IRSΩP

    The main advantage of IRSΩP over IKP(P) is the former’s amenability to partial cut elimination and the possibility to remove instances of (Σ˙P-Ref), which embody collection, from certain derivations via collapsing.

    Theorem 3.6. (Partial cut elimination for IRSΩP)

    [[28], theorem 3.11] If H|αΩ+n+1ΓΔ, then H|ωn(α)Ω+1ΓΔ, where ω0(β):=β and ωk+1(β):=ωωk(β).

    Lemma 3.7. (Boundedness)

    [[28], lemma 3.12] If A is a Σ˙P-formula, B is a Π˙P-formula, αβ<Ω and βH, then

    (i)

    If H|αρΓA then H|αρΓAVβ.

    (ii)

    If H|αρΓ,BΔ then H|αρΓ,BVβΔ.

    Boundedness is a crucial tool in the next result.

    Theorem 3.8. (Collapsing for IRSΩP)

    [[28], theorem 3.13] Suppose that ηHη, Δ is a set of at most one Σ˙P-formula and Γ a set of Π˙P-formulae. Then

    Hη|αΩ+1ΓΔimpliesHα^|ψΩ(α^)ψΩ(α^)ΓΔ.
    Here, β^=η+ωΩ+β and the operators Hξ are those defined in [28] definition 2.18.

    In actuality, in light of 3.7, we have

    Hη|αΩ+1ΓΔimpliesHα^|ψΩ(α^)ψΩ(α^)ΓVτΔVτ,
    with τ:=ψΩ(α^).

    Observe that the collapsing theorem eliminates all inference rules (Σ˙P-Ref) in the derivation.

    (b) Ordinal analysis of IKP(E)

    In the same vein as for IKP(P), one can furnish an ordinal analysis for the Kripke–Platek system IKP(E) based on exponentiation, though this is much more difficult than for IKP(P). It was achieved in [28] via the infinitary proof system IRSΩE. Again, we will briefly introduce the main features of IRSΩE and sketch the main results from [28] needed for this article.

    (i) A sequent calculus formulation of IKP(E)
    Definition 3.9.

    In the sequent calculus rendering of IKP(E), there are additional exponentiation bounded quantifiers of the form

    (xab)A(x)and(xab)A(x),
    treated as quantifiers in their own right, not abbreviations. Quantifiers of the form x, x will be called unbounded, whereas the quantifiers (xab),(xab),(xa),(xa) count as bounded ones. A Δ0E-formula of IKP(E) is one that contains only bounded quantifiers.

    As mentioned earlier, IKP(E) derives intuitionistic sequents, like in the following axiom for

    Exponentiation: Γz(xab)(xz).

    To express the rules for the exponentiation bounded quantifiers, one uses a formula ‘fun(x,a,b)’, whose intuitive meaning is ‘x is a function from a to b’:

    fun(x,a,b):=xa×b(ya)(zb)((y,z)x)(ya)(z1b)(z2b)[((y,z1)x(y,z2)x)z1=z2].
    The rules are as follows:
    (εbL)Γ,fun(c,a,b)F(c)ΔΓ,(xab)F(x)Δ(εbR)Γfun(c,a,b)F(c)Γ(xab)F(x)
    (εbL)Γ,fun(c,a,b)F(c)ΔΓ,(xab)F(x)Δ(εbR)Γfun(c,a,b)F(c)Γ(xab)F(x)
    with the proviso that the variable c in (EbL) and (EbR) is an eigenvariable.

    (ii) The infinitary system IRSΩE

    Next we need the infinitary system IRSΩE of [28, section 4.2], within which one can embed IKP(E) and carry out an ordinal analysis.

    Definition 3.10.

    Akin to the von Neumann hierarchy built by iterating the powerset operation, one may define an exponentiation hierarchy through the ‘ordinals’ of BΩ(εΩ+1)Ω:={αBΩ(εΩ+1)α<Ω} as follows:

    E0:=andE1:={},Eα+2:={X|X is definable over Eα+1, with parameters}{f|fun(f,a,b) for some a,bEα},Eλ:=β<λEβfor λ a limit,andEλ+1:={X|X is definable over Eα+1, with parameters}for λ a limit.
    The sets Eα are transitive; see [28, lemma 4.2].

    Note that the E-hierarchy can be defined in IKPR(E) up to any ordinal representation α<Ω for which transfinite induction is provable as the case distinctions therein are decidable for ordinal representations. The idea behind IRSΩE is to serve as a proof system for reasoning about the E-hierarchy.

    Definition 3.11.

    The terms of IRSΩE are defined as follows:

    1.

    Eα is an IRSΩE term for each α<Ω.

    2.

    aiα is an IRSΩE term for each α<Ω and each i<ω, these terms will be known as IRSΩE’s free variables.

    3.

    If F(a,b1,,bn) is a Δ0E formula of IKP(E) containing exactly the free variables indicated, and t,s1,,sn are IRSΩE terms, then

    [xt|F(x,s¯)]
    is also a term of IRSΩE.

    Note that while it was straightforward to assign the level α to a complex term [xVαF(x,s¯)] of IRSΩP by viewing it as a denizen of the von Neumann hierarchy, it is not clear how to locate an IRSΩE term within the E-hierarchy just by looking at the syntactic build-up of that term.

    The formulae of IRSΩE are of the form F(s1,,sn), where F(a1,,an) is a formula of IKP(E) with all free variables indicated and s1,,sn are IRSΩE terms. The formula A(s1,,sn) is said to be Δ0E if A(a1,,an) is a Δ0E formula of IKP(E).

    An important class of formulae was isolated in [28, definition 4.3]. The Σ˙E formulae are the smallest collection containing the Δ0E formulae such that AB, AB, (xt)A, (xt)A, (xab)A, (xab)A, xA, ¬C and CA are in Σ˙E whenever A and B are in Σ˙E and C is in Π˙E. The Π˙E formulae are the smallest collection containing the Δ0E formulae such that AB, AB, (xt)A, (xt)A, (xab)A, (xab)A, xA, ¬C and CA are in Π˙E whenever A and B are in Π˙E and C is in Σ˙E.

    For the details of the notion of operator controlled in IRSΩE, we refer the reader to [28, section 4]. IKP(E) can be embedded in IRSΩE, and the counterparts to theorems 3.5, 3.6, 3.7 and 3.8 ensue. We will just record the last one, which removes all inference rules (Σ˙E-Ref) from the derivation.

    Theorem 3.12. (Collapsing for IRSΩE)

    Suppose that ηHη, Δ is a set of at most one Σ˙E-formula and Γ a set of Π˙E-formulae. Then

    Hη|αΩ+1ΓΔimpliesHα^|ψΩ(α^)ψΩ(α^)ΓEτΔEτ,
    where τ:=ψΩ(α^), β^:=η+ωΩ+β, and the operators Hξ are those defined in [28] definition 2.18.

    Proof.

    See ([28, theorem 4.13]).

    (c) Background theory for ordinal analyses

    For the proof strategy of this article, it is important to ponder what background theory suffices for the task of carrying out the foregoing ordinal analyses. By the latter, we mean the embedding, cut elimination and collapsing theorems, but not the soundness theorems 2.35, 3.25 and 4.25 of [28]. If T is one of the theories IKP, IKP(P) or IKP(E) and TC with C being a Σ, Σ˙E or Σ˙P sentence, respectively, then one can explicitly determine a natural n such that the entire ordinal analysis for this statement requires only ordinals from BΩ(ωn(Ω+1)) (where ω0(Ω+1)=Ω+1 and ωk+1(Ω+1)=ωωk(Ω+1)). Certainly, transfinite induction over the ordinal representations of BΩ(ωn(Ω+1)) will be required, but actually very little beyond that. Recall that IKPR arises from IKP by substituting Σ replacement for strong collection. The claim is that IKPR is capacious enough.

    Theorem 3.13.

    The proof-theoretic ordinal of IKPR is the Bachmann–Howard ordinal. In particular, for every n, IKPR proves transfinite induction on the ordinal presentations of BΩ(ωn(Ω+1)) for arbitrary formulae.

    Proof.

    This was shown in [36, theorem 4.13] to hold for the theory CZFR0, i.e. CZF without subset collection and replacement in lieu of strong collection. Scouring its proof, it turns out that CZFR0 can be replaced by IKPR. Replacement is, for instance, used in the proof of [36, theorem 2.6] on which [36, theorem 4.13] builds, but fortunately it is just an instance of Σ replacement therein.

    An obstacle for formalizing ordinal analysis within IKPR, though, is posed by the need to formalize the notion of operator controlled derivability H|αρΓA. This notion is an example of a Σ-inductive definition (cf. [18, chapter V]). While it is no problem to formalize such definitions in the presence of Σ-collection, it does not seem to be possible with just Σ replacement at one’s disposal (see [36, section 2] for a discussion). To obviate this problem, the first observation is that instead of arbitrary operators one just needs recursive operators taking finite sets of ordinal representations as inputs and outputs. The main idea is then that we can do everything with recursive proof trees controlled by a recursive operator instead of arbitrary operator controlled derivations. A proof-tree controlled by a recursive operator H is a tree, with each node labelled by: a sequent, a rule of inference or the designation ‘Axiom’, two sets of formulas specifying the set of principal and minor formulas, respectively, of that inference, and two ordinals (length and cut–rank) such that the sequent is obtained from those immediately above it through the application of the specified rule of inference, additionally controlled by H. The well-foundedness of a proof-tree is then witnessed by the (first) ordinal 'tags' which are in reverse order of the tree order. Furthermore, one needs to show that all the proof-theoretic operations such as embedding, cut elimination and collapsing can be engineered via recursive functions acting on them. The upshot is that there are well-known techniques for handling infinite derivations in intuitionistic systems (even of arithmetic) via codes for recursive proof trees or even primitive recursive ones (see, for instance [3741]), and that this treatment is deployable in IKPR.

    4. Partial conservativity over systems based on replacement

    The ordinal analyses of IKP, IKP(E) and IKP(P) of [28] can be used to obtain conservativity results over the counterparts with replacement in lieu of collection. We will use the acronyms IKPR, IKPR(P) and IKPR(E) for the theories with Σ replacement, ΣE replacement and ΣP replacement instead of Σ collection, ΣE collection and ΣP collection, respectively.

    Theorem 4.1.

    (i)

    IKP+Σ˙-reflection is conservative over IKPR for Σ˙-sentences.

    (ii)

    IKP(E)+Σ˙E-reflection is conservative over IKPR(E) for Σ˙E-sentences.

    (iii)

    IKP(P)+Σ˙P-reflection is conservative over IKPR(P) for Σ˙P-sentences.

    Proof.

    Let us start with (iii). So suppose that IKP(P)+Σ˙P-reflection proves a Σ˙P-sentence A. The length of this finite deduction determines a number n such that the entire ordinal analysis for this deduction, comprising the embedding theorems 3.5, theorem 3.6 and the collapsing theorem 3.8, solely uses ordinals from the set BΩ(ωn(Ω+1)), where ω0(Ω+1)=Ω+1 and ωk+1(Ω+1)=ωωk(Ω+1). Moreover, it follows from theorem 3.13 that transfinite induction along the ordinals of BΩ(ωn(Ω+1)) is provable in IKPR for arbitrary formulae. As argued in §3c, we can determine a recursive operator H, a recursive proof-tree and ordinals α,ρ<Ω with α,ρBΩ(ωn(Ω+1)) such that H|αρΓA, and, moreover, we gain this insight in IKPR.

    Switching to IKPR(P), we aim to conclude that A is also true. Temporarily, let VARP be the set of variables with labels in BΩ(ωn(Ω+1)). Moreover, we only consider IRSΩP-terms created from ordinals in BΩ(ωn(Ω+1)). Let Vα be obtained by iterating the powerset operation α-times for αBΩ(ωn(Ω+1))Ω, i.e. for ξ,λ<α, let

    V0:=,AAAAVξ+1:={X|XVξ},AAAAVλ:=β<λVβfor λ a limit.
    This hierarchy is definable in IKPR(P) using ΣP replacement and powerset since one has transfinite induction over BΩ(ωn(Ω+1))Ω (for any formula) and the case distinctions (as to zero, successor and limit ordinal (representation)) are decidable.

    We then only consider variable assignments v:VARPVψΩ(ωn(Ω+1)), of course satisfying v(aiα)Vα+1 for each i. The assignment v canonically propagates to all terms via

    v(Vα)=Vα
    and
    v({xVα|F(x,s1,,sn)})={xVα|F(x,v(s1),,v(sn))}.
    Moreover, it can be seen that v(s)Vs+1, and thus, v(s)VψΩ((ωn(Ω+1)).

    We then obtain the following soundness result for IRSΩP as in [28, theorem 3.25]: Suppose Γ[s1,,sn] is a finite set of Π˙P formulae with max{rk(A)|AΓ}Ω and Δ[s1,,sn] a set containing at most one Σ˙P formula such that

    H|αρΓ[s¯]Δ[s¯]for some operator H and some α,ρBΩ(ωn(Ω+1))Ω.
    Then, for any assignment v going to VψΩ(ωn(Ω+1)),
    VψΩ((ωn(Ω+1))Γ[v(s1),,v(sn)]Δ[v(s1),,v(sn)].
    Here, Γ and Δ stand for the conjunction of formulae in Γ and the disjunction of formulae in Δ, respectively (by convention = and =). For a more detailed proof, see [28, 3.25].

    By soundness, we therefore have VψΩ((ωn(Ω+1))A for the assignment vs, which interprets any variable by . As a result, A is provable in IKPR(P).

    We now turn to the proof of (ii), which is to a large extent similar to that of (iii). Of course, it is based on the much more complicated ordinal analysis of IKP(E) from [28] section 4. Analogously to IRSΩP, one proves a soundness theorem for certain IRSΩE derivable sequents. Again we consider only variable assignments

    v:VAREEψΩ(ωn(Ω+1)),
    such that v(aiα)Eα+1 for all i<ω and ordinals α. Here, Eβ refers to the E-hierarchy of definition 3.10. Again, such an assignment propagates to all IRSΩE terms by letting
    v(Eα)=Eα
    and
    v([xt|F(x,s1,,sn)])={xv(t)|F(x,v(s1),,v(sn))}.
    As mentioned earlier, the crucial difference between here and the case of IRSΩP is that for a given term t, it is no longer possible to describe the location of v(t) within the E-hierarchy solely by inspecting its syntactic structure, albeit it is possible to place an upper bound on that location using the following function:
    m(Eα):=αm(aiα):=αandm([xt|F(x,s1,,sn)]):=max(m(t),m(s1),,m(sn))+1.
    We then have that v(s)Em(s)+1 for any s, though in general m(s) only determines an upper bound on a term’s position in the E-hierarchy. According to [28, theorem 4.25], one obtains the following soundness result for IRSΩE. Let Γ[s1,,sn] be a finite set of Π˙E formulae with max{rk(A)|AΓ}Ω and Δ[s1,,sn] be a set containing at most one Σ˙E formula such that
    H|αρΓ[s¯]Δ[s¯]for some operator H and some α,ρBΩ(ωn(Ω+1))Ω.
    Then, given any assignment v going into EψΩ(ωn(Ω+1)),
    EψΩ(ωn(Ω+1))Γ[v(s1),,v(sn)]Δ[v(s1),,v(sn)].
    Finally, for (i), we use the constructible hierarchy defined by transfinite recursion along the ordinals of BΩ(ωn(Ω+1))Ω.
    L0:=Lξ+1:={X|X is definable over Lξ, with parameters}andLλ:=β<λLβfor λ a limit.
    This hierarchy is definable in IKPR using just ΣP replacement rather than Σ collection (for details, see [42]).

    Noting that they do not contain free variables, terms t of IRSΩ (see [28, subsection 2.3]), are assigned to sets v(t) in the obvious way, namely,

    v(Lα)=Lα
    and
    v([xt|F(x,s1,,sn)Lα])={xv(t)|F(x,v(s1),,v(sn))Lα}.
    As a result, one gets a soundness theorem for IRSΩ in the same way as for IRSΩP, yielding (i).

    5. Existence property for theories with replacement

    Let CZFR, CZFE,R and CZFP,R be the counterparts theories obtained from of CZF, CZFE and CZFP, respectively, by having the replacement scheme instead of the strong collection scheme.

    From theorems 4.1 and 2.12, it follows that CZF, CZFP and CZFE have the EP if CZFR, CZFP,R and CZFE,R, respectively, have this property. Techniques to establish the EP for intuitionistic set theories based on replacement rather than collection are available. Friedman [2] introduced a modification of Kleene’s slashing technology and used it to prove the EP for various systems of type theory and higher-order arithmetic. These results were extended to versions of intuitionistic Zermelo–Fraenkel set theory with replacement by Friedman and Myhill in [3] and to constructive set theories by Myhill [4].

    The technology can also be deployed in cases such as the theories CZFP,R and CZFE,R. Owing to it being well-documented in the research literature (especially [3,4], and also in book form in [1], IX) and due to page restrictions, I shall just sketch the main steps.6

    Definition 5.1.

    Let L be a first-order language comprising the language of set theory, SL its set of sentences, AL its atomic sentences and TL its set of closed terms. For T a set of L-sentences, let Thm(T) be {ASLTA}. Let MAL be a non-empty set of atoms and PSL such that Thm(T)P and P is closed under modus ponens, i.e. AP and ADP yields DP.

    Friedman realizability, R(T,M,P), is the unique set FSL such that the following conditions are met.

    GFGM, for GAL,⊥∉FADFAF and DF,ADFAPF or DPF,ADFAPF implies DF,xB(x)FB(t)F for all tTL,andxB(x)FB(t)PF for some tTL.
    We say that T realizes A relative to M and P if AR(T,M,P).

    The fundamental property of R is given by the following.

    Theorem 5.2. (Friedman)

    TR(T,M,P) implies that Thm(T)R(T,M,P).

    Proof.

    [2], theorem 2.1.

    Let us give an outline as to how it can be shown that IKPR, IKPR(P), IKPR(E), CZFR, CZFP,R and CZFE,R (and similar theories) possess the EP. Let T be any of these theories. T will just serve the purpose of a generic example to which this technology applies. Suppose TuA(u), where the formula has no free variables. In a first step, one builds a conservative extension T+ of T such that we have T+A(t) for some term t of the enriched language. Translating back to the original language will give us the result. In the light of theorem 5.2, we only need to produce such a term t for each set existence axiom of T. As it suffices to show that there is a formula G(x) such that

    Tu[A(u)x(xuG(x))],
    the idea is to introduce comprehension terms.

    Definition 5.3.

    For each formula G(x) with at most x free such that Tyx(xyG(x)), we introduce a comprehension term [xG(x)]. Two comprehension terms s,t are viewed as equivalent if their defining formulae are provably equivalent in T, and we write st to convey this. We extend the language of set theory by a new constant ct for each comprehension term t[xG(x)], and then write Gt(x) for G(x). Let L be this new language and T be the theory in this new language consisting of the axioms of T along with

    x(xctGt(x)),
    for each comprehension term t.

    Proposition 5.4.

    T is a conservative extension of T.

    Proof.

    This is achieved by simply replacing every atomic tt, with t,t comprehension terms, by

    uv[x(xuGt(x))x(xvGt(x))vu].

    To arrive at the theory T+, we need an even larger class of set-indexed constants, C+.

    Definition 5.5.

    C+ is defined via the following inductive definition:7

    If c is a constant of L and X{cYC+Tcb}, then bXC+.

    For dbXC+, we write d for b, and d+ for X.

    Let L+ be the extension of L via the new set-indexed constants. Let T+ be the theory in the language L with the axioms of CZFP,R augmented by the axioms

    x[xdAt(x)],
    where dct for a comprehension term t.

    Proposition 5.6.

    T+ is a conservative extension of T.

    Proof.

    The proof idea is for a formula A of L+ to replace each occurrence of dC+ by d.

    Finally, we are in a position to make use of theorem 5.2. In the latter let T be T and P be Thm(T+) and M be the set of atomic sentences ed, where e belongs to d+. The pivotal move is to show that for each set existence axiom

    yx[xyA(x)],
    of T+, there is a set X so that
    eXA(e)PF,
    where F=R(T,M,P). As a result, for b[xA(x)], we will have yx[xyA(x)]PF, and hence, by theorem 5.2, Thm(T)F.

    Accordingly, if TuH(u), then uH(u)F, so that there is a sC+ with T+H(d). Consequently, TH(d). As d is of the form ct for a comprehension term t, we arrive at

    Tu[H(u)x(xuAt(x))].

    Theorem 5.7.

    IKPR, IKPR(E), IKPR(P), CZFR, CZFE,R and CZFP,R have the EP.

    The aforementioned proof works for a wide variety of theories whose set-existence axioms are explicit, i.e. if they define the denizens of the set being asserted to exist in the form

    u[D(u)yx(xyG(x,u))].
    In [3, section 6], it is shown in detail that axioms of the aforementioned form are always realizable.

    6. Conclusion

    Preparations are finished now, and we can show that various theories with collection axioms have the EP.

    Theorem 6.1.

    IKP, IKP(E), IKP(P), CZF, CZFE and CZFP have the EP.

    Proof.

    As an example we show this for CZFE. By theorem 2.12 (ii), it suffices to show that IKP(E) has the EP for ΣE formulae. So assume IKP(E)xB(x) for a closed ΣE formula. Theorem 4.1(ii) yields that IKPR(E)xB(x), and hence, invoking theorem 5.7, there is a formula C(x) (with at most x free) such that IKPR(E)!x[C(x)B(x)]. In consequence, IKP(E)!x[C(x)B(x)].

    The proofs for the other theories follow the same pattern.

    Data accessibility

    This article has no additional data.

    Authors' contributions

    M.R: conceptualization, writing—review and editing.

    Conflict of interest declaration

    I declare I have no competing interests.

    Funding

    Research funded by EPSRC (grant no. EP/K023128/1).

    Acknowledgements

    The author acknowledges support by the John Templeton Foundation for the project A new dawn of Intuitionism: Mathematical and Philosophical advances (grant no. ID 60842).

    Footnotes

    1 If one assumes a choice principle, called the presentation axiom, exponentiation yields subset collection (cf. [15], 10.3.3).

    2 The statement that for any two sets the class of multi-valued functions between them is a set is too strong as it is equivalent to powerset (cf. [15], 5.1.6).

    3 Burr ([16], corollary 5.12) and Diller ([17], proposition 4.4) showed that higher type versions of constructive set theory, but without subset collection and exponentiation, enjoy weak forms of the term existence property.

    4 ([12], theorem 3.10) does not state this for IKP, IKP(E) and IKP(P), but it is easily checked that theorems 3.7–3.9 of [12] also work for IKP, IKP(E) and IKP(P), respectively, from which this follows.

    5 Note that the Σ˙P-formulae comprise the ΣP-formulae of definition 2.7. In the terminology of [28], however, the ΣP-formulae are identical to the Σ˙P-formulae, but this clashes with the terminology of [12], hence the dot.

    6 In 2012, I attended a talk by Ali Lloyd who was a PhD student of Peter Aczel back then. It was about ascertaining the EP for CZFE,R, with a discussion of the metatheory required for such a proof. The approach was also based on Friedman realizability as in this section. Moreover, he mentioned in the talk that Peter Aczel had shown the EP for CZFE,R with a proof being formalizable in IZFR. Alas, I was unsuccessful finding any traces of this on the worldwide net.

    7 Notably, this kind of definition can be formalized in CZF as a class inductive definition.

    One contribution of 11 to a theme issue ‘Modern perspectives in Proof Theory’.

    Published by the Royal Society under the terms of the Creative Commons Attribution License http://creativecommons.org/licenses/by/4.0/, which permits unrestricted use, provided the original author and source are credited.

    References