From the weak to the strong existence property (Q448335)

A theory \(T\) has the weak existence property (\textbf{wEP}) if, for any closed formula of the form \(\exists x\,A(x)\) deducible in \(T\), there exists a formula \(C(x)\) with \(x\) the only free variable such that the following formulae are deducible in \(T\): \(\exists! x\,C(x)\), \(\forall x\,(C(x)\to\exists u\,u\in x)\), \(\forall x\,(C(x)\to(\forall u\in x)\,A(u))\). It is proved that the following intuitionistic set theories have \textbf{wEP}: \(\mathbf C\mathbf Z\mathbf F^-\), \(\mathbf C\mathbf Z\mathbf F_{\mathcal E}\), and \(\mathbf C\mathbf Z\mathbf F_{\mathcal P}\), i.e., constructive Zermelo-Fraenkel set theory (\(\mathbf C\mathbf Z\mathbf F\)), respectively, without the scheme of set collection, with exponentiation, and with the power set axiom. For proving this result the author defines a realizability based on indices of general set recursive (or \(E\)-recursive) functions introduced earlier [the author, NATO Sci. Ser. III, Comput. Syst. Sci. 200, 279--322 (2006; Zbl 1128.03047)]. Namely, for any set-theoretical formula \(B\) a formula \(a\Vdash_{\mathfrak{rv}\text{t}}B\) is defined inductively. For atomic \(A\), \(a\Vdash_{\mathfrak{rv}\text{t}}A\) is \(A\); \(a\Vdash_{\mathfrak{rv}\text{t}}(A\lor B)\) is \(\exists x\,x\in a\land(\forall d\in a)\,(j_0d=0\land j_1d\Vdash_{\mathfrak{rv}\text{t}}A\lor j_0d=1\land j_1d\Vdash_{\mathfrak{rv}\text{t}}B)\); \(a\Vdash_{\mathfrak{rv}\text{t}}\neg A\) is \(\neg A\land\forall c\,\neg c\Vdash_{\mathfrak{rv}\text{t}}A\); \(a\Vdash_{\mathfrak{rv}\text{t}}(A\to B)\) is \((A\to B)\land\forall c\,(c\Vdash_{\mathfrak{rv}\text{t}}A\to[a](c)\Vdash_{\mathfrak{rv}\text{t}}B)\); \(a\Vdash_{\mathfrak{rv}\text{t}}\exists x\,A(x)\) is \(\exists x\,x\in a\land(\forall d\in a)\,j_1d\Vdash_{\mathfrak{rv}\text{t}}A(j_0d)\). Thus a realizer for an existential statement provides a set of witnesses. Variants of the realizability \(\Vdash_{\mathfrak{rv}\text{t}}^{\mathcal E}\) and \(\Vdash_{\mathfrak{rv}\text{t}}^{\mathcal P}\) are based on the class of \(E\)-recursive functions extended, respectively, by the functions \(\text{exp}(a,b)\) (the set of all functions from \(a\) to \(b\)) and \({\mathcal P}(x)\). The theories \(\mathbf C\mathbf Z\mathbf F^-\), \(\mathbf C\mathbf Z\mathbf F_{\mathcal E}\), and \(\mathbf C\mathbf Z\mathbf F_{\mathcal P}\) are provably correct relative to the realizabilities \(\Vdash_{\mathfrak{rv}\text{t}}\), \(\Vdash_{\mathfrak{rv}\text{t}}^{\mathcal E}\), and \(\Vdash_{\mathfrak{rv}\text{t}}^{\mathcal P}\), respectively. Namely, if a formula \(D(u_1,\ldots,u_r)\) is deducible in the theory \(\mathbf C\mathbf Z\mathbf F^-\), then one can effectively construct an index of an \(E\)-recursive function \(g\) such that \(\mathbf C\mathbf Z\mathbf F^-\vdash\forall a_1,\ldots,a_r\,g(a_1,\ldots,a_r)\Vdash_{\mathfrak{rv}\text{t}} D(a_1,\ldots,a_r)\) and the same holds for other theories and corresponding classes of functions and realizabilities. These forms of realizability are also used for proving that the theories under consideration are conservative for restricted classes of formulae over their intuitionistic Kripke-Platek counterparts. A proof sketch that intuitionistic Kripke-Platek set theory has the existence property for \(\Sigma\) formulae is given. This implies that \(\mathbf C\mathbf Z\mathbf F^-\) has the existence property.