2.1 $\mathsf {CZF}$ and $\mathsf {IZF}$

In this paper, we will be concerned with (extensions of) $\mathsf {CZF}$ (constructive Zermelo–Fraenkel set theory) and $\mathsf {IZF}$ (intuitionistic Zermelo–Fraenkel set theory). The logic is intuitionistic first order logic with equality in the language of classical $\mathsf {ZF}$ . As usual, a formula is bounded, or $\Delta _0$ , if all quantifiers appear in the form $\forall x\in y$ and $\exists x\in y$ .

The theory $\mathsf {CZF}$ consists of the following axioms:

$^{\ast} $ Let $x=0$ be $\forall y\in x\, (y\notin x)$ and $x=y\cup \{y\}$ be $\forall z\kern-1pt \in\kern-1pt x\, (z\kern-1pt \in\kern-1pt y\lor z\kern-1pt =\kern-1pt y)\land \forall z\kern-1pt \in\kern-1pt y\, (z\in x)\land y\kern-1pt \in\kern-1pt x$ .

The theory $\mathsf {IZF}$ consists of extensionality, pairing, union, infinity, induction,

Thus $\mathsf {IZF}$ is $\mathsf {CZF}$ with bounded separation replaced by full separation and subset collection replaced by powerset. Note that powerset implies subset collection, and strong collection follows from separation and collection. It is well known that $\mathsf { CZF}$ with classical logic, and hence $\mathsf {IZF}$ with classical logic, is equivalent to $\mathsf {ZF}$ .

2.2 Countable and dependent choice

The full axiom of choice $\mathsf {AC}$ is known to imply forms of excluded middle [Reference Diaconescu11]. For example, $\mathsf {CZF}+\mathsf {AC}+\text { separation}=\mathsf {IZF}+\mathsf {AC}=\mathsf {ZFC}$ (cf. [Reference Aczel and Rathjen4]). Nevertheless, countable choice and several forms of dependent choice are deemed constructively acceptable. Note that $\mathsf {RDC}$ is an axiom of Myhill’s $\mathsf {CST}$ (constructive set theory) [Reference Myhill24], which provides a standard set-theoretical framework for Bishop-style constructive mathematics [Reference Bishop9]. Dependent choice also features in Brouwer’s intuitionistic analysis (cf. [Reference Troelstra and van Dalen34]).

Countable choice ( $\mathsf {AC}_{\omega }$ ): if $\forall n\in \omega \, \exists y\, \varphi (n,y)$ , then there exists a function f with $\operatorname {{\mathrm {dom}}}(f)=\omega $ such that $\forall n\in \omega \, \varphi (n,f(n))$ , for all formulae $\varphi $ .

Dependent choice ( $\mathsf {DC}$ ): if $\forall x\, \exists y\, \varphi (x,y)$ , then for every x there is a function f with $\operatorname {{\mathrm {dom}}}(f)=\omega $ such that $f(0)=x$ and $\forall n\in \omega \, \varphi (f(n),f(n+1))$ , for all formulae $\varphi $ .

Limited dependent choice ( $\mathsf {DC}^{\dagger }$ ): if X is a set and $\forall x\in X\, \exists y\in X\, \varphi (x,y)$ , then for every $x\in X$ there is a function $f\colon \omega \to X$ such that $f(0)=x$ and $\forall n\in \omega \, \varphi (f(n),f(n+1))$ , for all formulae $\varphi $ .

Relativized dependent choice ( $\mathsf {RDC}$ ): if $\forall x\, (\psi (x)\rightarrow \exists y\, (\psi (y)\land \varphi (x,y)))$ , then for every x such that $\psi (x)$ , there is a function f with $\operatorname {{\mathrm {dom}}}(f)=\omega $ such that $f(0)=x$ and $\forall n\in \omega \, \varphi (f(n),f(n+1))$ , for all formulae $\psi $ and $\varphi $ .

Limited relativized dependent choice ( $\mathsf {RDC}^{\dagger }$ ): if X is a set and $\forall x\in X\, (\psi (x)\rightarrow \exists y\in X\, (\psi (y)\land \varphi (x,y)))$ , then for every $x\in X$ such that $\psi (x)$ , there is a function $f\colon \omega \to X$ such that $f(0)=x$ and $\forall n\in \omega \, \varphi (f(n),f(n+1))$ , for all formulae $\psi $ and $\varphi $ .

Note that classically, say over $\mathsf {ZF}$ , the above forms of dependent choice are all equivalent to one another. Over $\mathsf {CZF}$ , $\mathsf {RDC}\rightarrow \mathsf {DC}$ and $\mathsf {RDC}\rightarrow \mathsf {RDC}^{\dagger }\rightarrow \mathsf {DC}^{\dagger }\rightarrow \mathsf { AC}_{\omega }$ . Over $\mathsf {IZF}$ , due to separation, $\mathsf {RDC}^{\dagger }\leftrightarrow \mathsf {DC}^{\dagger }$ .

2.3 Inductive definitions and the regular extension axiom

The theory $\mathsf {CZF}$ allows for a smooth treatment of inductively defined classes [Reference Aczel3, Reference Aczel and Rathjen4].

Definition 2.1. An inductive definition is a class $\Phi $ of ordered pairs. In other words, any formula $\Phi (X,x)$ is an inductive definition. We write

or simply $(X,x)\in \Phi $ , in place of $\Phi (X,x)$ . A class I is closed under $\Phi $ if, whenever $(X,x)\in \Phi $ and $X\subseteq I$ , we have $x\in I$ .

Proof See, e.g., [Reference Aczel and Rathjen4] for details. The class $I(\Phi )$ is defined as follows. A set of ordered pairs Z is called an iteration set for $\Phi $ if for every $\langle {u,x}\rangle \in Z$ there exists $(X,x)\in \Phi $ such that $X\subseteq \bigcup _{v\in u}\{z\mid \langle {v,z}\rangle \in Z\}$ . Let

$$\begin{align*}I(\Phi)=\bigcup_u\{ x\mid \text{there is an iteration set } Z \text{ such that }\langle{u,x}\rangle\in Z\}.\end{align*}$$

To prove that $I(\Phi )$ is closed under $\Phi $ we invoke strong collection. The fact that $I(\Phi )$ is the smallest class closed under $\Phi $ is proved by induction.

Theorem 2.3 (Induction on the inductive definition $\Phi $ ).

$\mathsf {CZF}$ proves

$$\begin{align*}\forall (X,x)\in\Phi\, (\forall y\in X\, \varphi(y)\rightarrow \varphi(x))\rightarrow \forall x\in I(\Phi)\, \varphi(x), \end{align*}$$

for every formula $\varphi $ .

In the presence of Aczel’s $\mathsf {REA}$ (regular extension axiom), one can show that many inductively defined classes exist as sets.

Definition 2.4 (Regular).

A set X is regular if it is transitive and, whenever $x\in X$ and R is a set such that $\forall u\in x\, \exists v\in X\, (\langle {u,v}\rangle \in R)$ , then there is a $y\in X$ such that

$$\begin{align*}\forall u\in x\, \exists v\in y\, (\langle{u,v}\rangle\in R)\land \forall v\in y\, \exists u\in x\, (\langle{u,v}\rangle\in R). \end{align*}$$

In particular, if $R\colon x\to X$ is a function, then $\operatorname {{\mathrm {ran}}}(R)\in X$ .

Regular extension axiom ( $\mathsf {REA}$ ): every set is a subset of a regular set.

2.4 Dependent type constructions

The usual type constructors ${\Pi }$ (dependent product), ${\Sigma }$ (dependent sum), $\mathrm {I}$ (identity), and $\mathrm {W}$ have obvious set-theoretic analogues.

Definition 2.7 ( $\mathsf {CZF}$ ).

Let F be a function with $\operatorname {{\mathrm {dom}}}(F)=X$ . Let

$$ \begin{align*} {\Pi}(X,F)&= \prod_{x\in X}F(x)=\{f\colon X\to \bigcup_{x\in X}F(x)\mid \forall x\in X\, (f(x)\in F(x))\} && ({{Cartesian\ product}}), \\ {\Sigma}(X,F)&=\sum_{x\in X}F(x)=\{ \langle{x,y}\rangle\mid x\in X\land y\in F(x)\} && ({{disjoint\ union}}). \end{align*} $$

For x, y sets, let $\mathrm {I}(x,y)=\{z\in \{0\}\mid x=y\}$ .

Given a class I, we say that x is an I-set if x belongs to I.

2.5 Choice for dependent types

Presentation axiom ( $\mathsf {PAx}$ ): every set is an image of a base.

${\Pi }{\Sigma }$ axiom of choice ( ${\Pi }{\Sigma }\text {-}\mathsf {AC}$ ): every ${\Pi }{\Sigma }$ -set is a base.

${\Pi }{\Sigma }$ presentation axiom ( ${\Pi }{\Sigma }\text {-}\mathsf {PAx}$ ): every set is an image of a ${\Pi }{\Sigma }$ -set and every ${\Pi }{\Sigma }$ -set is a base.

We have analogue axioms for ${\Pi }{\Sigma }\mathrm {I}$ and relatives. A simple argument shows that $\mathsf {CZF}+\mathsf {PAx}\vdash \mathsf { DC}^{\dagger }$ (cf. [Reference Aczel1, p. 65] and [Reference Aczel2, p. 27]). Aczel’s interpretation of $\mathsf {CZF}$ in type theory [Reference Aczel1] validates $\mathsf {RDC}$ [Reference Aczel1, Theorem 7.1], [Reference Aczel2, Theorem 5.7] and ${\Pi }{\Sigma }\mathrm {I}\text {-}\mathsf {PAx}$ [Reference Aczel2, Theorem 7.4]. In [Reference Aczel3], the type-theoretic interpretation of $\mathsf {CZF}+\mathsf {REA}$ (by using $\mathrm {W}$ -types) is shown to validate $\mathsf {RDC}$ and ${\Pi }{\Sigma }\mathrm {W}\mathrm {I}\text {-}\mathsf {PAx}$ [Reference Aczel3, Theorem 5.6].Footnote ⁵ Similarly, Rathjen’s formulae-as-classes interpretation provides a model of $\mathsf {CZF}+\mathsf { RDC}+{\Pi }{\Sigma }\mathrm {I}\text {-}\mathsf {AC}$ in $\mathsf {CZF}_{\mathsf {exp}}$ [Reference Rathjen29, Theorem 4.13] and of $\mathsf {CZF}+\mathsf {REA}+\mathsf {RDC}+{\Pi }{\Sigma }\mathrm {W}\mathrm {I}\text {-}\mathsf {AC}$ in $\mathsf {CZF}_{\mathsf { exp}}+\mathsf {REA}$ [Reference Rathjen29, Theorem 4.33], where $\mathsf {CZF}_{\mathsf {exp}}$ is $\mathsf {CZF}$ with exponentiation in lieu of subset collection.

We introduce the following natural extensions of $\mathsf {AC}_{\mathsf {FT}}$ and $\mathsf {RDC}_{\mathsf {FT}}$ .

${\Pi }{\Sigma }$ limited axiom of choice ( ${\Pi }{\Sigma }\text {-}\mathsf {AC}^{\dagger }$ ): if X and Y are ${\Pi }{\Sigma }$ -sets and $\forall x\in X\, \exists y\in Y\, \varphi (x,y)$ , then there is a function $f\colon X\to Y$ such that $\forall x\in X\, \varphi (x,f(x))$ , for all formulae $\varphi $ .

${\Pi }{\Sigma }$ limited relativized dependent choice ( ${\Pi }{\Sigma }\text {-}\mathsf {RDC}^{\dagger }$ ): this is just $\mathsf { RDC}^{\dagger }$ restricted to ${\Pi }{\Sigma }$ -sets.

We have similar axioms for ${\Pi }{\Sigma }\mathrm {I}$ and relatives. Each schema can be replaced by a single axiom over say $\mathsf { IZF}+\mathsf {REA}$ . This is just an upper bound. For example, over $\mathsf {CZF}$ , ${\Pi }{\Sigma }\text {-}\mathsf {AC}^{\dagger }$ is equivalent to:

If X and Y are ${\Pi }{\Sigma }$ -sets, then for every relation R such that $\forall x\in X\, \exists y\in Y\, (\langle {x,y}\rangle \in R)$ , there is a function $f\colon X\to Y$ such that $\forall x\in X\, (\langle {x,f(x)}\rangle \in R)$ .

Clearly, ${\Pi }{\Sigma }\text {-}\mathsf {AC}^{\dagger }$ follows from ${\Pi }{\Sigma }\text {-}\mathsf {AC}$ , and similarly for ${\Pi }{\Sigma }\mathrm {I}$ and the like. Note that ${\Pi }{\Sigma }\text {-}\mathsf {AC}^{\dagger }$ already includes the axiom of choice for all finite types.

Theorem 2.15 does not translate to ${\Pi }{\Sigma }\text {-}\mathsf {AC}^{\dagger }$ and relatives. For example, the proof of [Reference Aczel3, Theorem 3.7] consists in showing, under ${\Pi }{\Sigma }\text {-}\mathsf {AC}$ , that every set in ${\Pi }{\Sigma }\mathrm {I}$ is in bijection with a set in ${\Pi }{\Sigma }$ . The use of ${\Pi }{\Sigma }\text {-}\mathsf {AC}$ is essential. The proof of the following is trivial.

3.1 Partial combinatory algebras

Generic realizability is based on the notion of partial combinatory algebra. Let us review some basic facts. For more information, we refer the reader to [Reference Beeson7, Reference Feferman12, Reference Feferman13, Reference van Oosten26].

Every partial algebra A induces a partial interpretation of closed applications terms over A by elements of A in the obvious way.

The combinators $\mathbf k$ and $\mathbf s$ are due to Schönfinkel [Reference Schönfinkel31] and the defining equations, although formulated just in the total case, are due to Curry [Reference Curry10]. The name combinatory stems from the property known as combinatory completeness. Informally, this means that we can form $\lambda $ -terms.

An immediate consequence of $\lambda $ -abstraction is the existence of pairing and unpairing combinators $\mathbf p$ , $\mathbf {p_0}$ , and $\mathbf {p_1}$ such that $\mathbf pab\downarrow $ and $\mathbf {p_i}(\mathbf pa_0a_1)\simeq a_i$ .Footnote ⁶ A more remarkable application of $\lambda $ -abstraction is the recursion theorem for pca’s.

It is worth considering some additional structure (see however Remark 3.9).

Definition 3.8. We say that A is a pca over $\omega $ if there are combinators $\mathbf {succ}, \mathbf {pred}$ (successor and predecessor combinators), $\mathbf d$ (definition by cases combinator), and a map $n\mapsto \bar n$ from $\omega $ to A such that for all $n\in \omega $

$$ \begin{align*} \operatorname{\mathrm{\mathbf{succ}}} \bar n&\simeq \overline{n+1}, & \operatorname{\mathrm{\mathbf{pred}}}\overline{n+1}&\simeq \bar n, & \mathbf d\bar n\bar mab\simeq \begin{cases} a, & n=m,\\ b, & n\neq m. \end{cases} \end{align*} $$

One then defines $\mathbf 0=_{\mathrm {def}}\bar 0$ and ${\mathbf 1}=_{\mathrm {def}}\bar 1$ .

For the rest of the paper, by a pca we really mean a pca over $\omega $ . The only closed terms we ever need are built up by using the combinators $\mathbf k$ , $\mathbf s$ , $\mathbf p$ , $\mathbf {p_0}$ , $\mathbf {p_1}$ , $\mathbf 0$ , ${\mathbf 1}$ , $\mathbf {succ}$ , $\mathbf {pred}$ , and $\mathbf d$ .

Note that one can do without $\mathbf k$ by letting $\mathbf k=_{\mathrm {def}}\mathbf d\mathbf 0\mathbf 0$ . The existence of $\mathbf d$ implies that the map $n\mapsto \bar n$ is one-to-one. In fact, suppose $\bar n=\bar m$ but $n\neq m$ . Then $\mathbf d\bar n\bar n\simeq \mathbf d\bar n\bar m$ . It then follows that $a\simeq \mathbf d\bar n\bar nab\simeq \mathbf d\bar n\bar mab\simeq b$ for all $a,b$ . On the other hand, by our definition, every pca contains at least two elements.

3.2 Defining realizability

The inductive definition of $\mathrm {V_{ext}}(A)$ within $\mathsf {CZF}$ is on par with that of $\mathrm {V}(A)$ [Reference Rathjen30,Lemma 3.4].

Definition 3.12 (Extensional realizability).

We define the relation $a=b\Vdash \varphi $ , where $a,b\in A$ and $\varphi $ is a realizability formula with parameters in $\mathrm {V_{ext}}(A)$ . The atomic cases fall under the scope of definitions by transfinite recursion.

$$ \begin{align*} a=b&\Vdash x\in y && \Leftrightarrow && \exists z\, (\langle (a)_0,(b)_0,z\rangle \in y\land (a)_1=(b)_1\Vdash x=z),\\ a=b& \Vdash x=y && \Leftrightarrow &&\forall \langle c,d,z\rangle \in x\, ((ac)_0=(bd)_0\Vdash z\in y) \text{ and } \\ &&&&& \forall \langle c,d,z\rangle \in y\, ((ac)_1=(bd)_1\Vdash z\in x),\\ a=b& \Vdash \varphi\land \psi && \Leftrightarrow && (a)_0=(b)_0\Vdash \varphi \land (a)_1=(b)_1\Vdash \psi, \\ a=b& \Vdash \varphi\lor\psi && \Leftrightarrow && (a)_0=(b)_0=\mathbf 0\land (a)_1=(b)_1\Vdash \varphi \text{ or } \\ &&&&& (a)_0=(b)_0={\mathbf 1}\land (a)_1=(b)_1\Vdash \psi, \\ a=b&\Vdash \neg\varphi && \Leftrightarrow && \forall c, d\, \neg (c=d\Vdash \varphi), \\ a=b&\Vdash \varphi\rightarrow\psi && \Leftrightarrow && \forall c,d\, (c=d\Vdash \varphi\rightarrow ac=bd\Vdash \psi), \\ a=b& \Vdash \forall x\in y\, \varphi && \Leftrightarrow && \forall \langle c,d,x\rangle\in y\, (ac=bd\Vdash \varphi), \\ a=b&\Vdash \exists x\in y\, \varphi && \Leftrightarrow && \exists x\, (\langle (a)_0,(b)_0,x\rangle \in y\land (a)_1=(b)_1\Vdash \varphi),\\ a=b& \Vdash \forall x\, \varphi && \Leftrightarrow && \forall x\in \mathrm{V_{ext}}(A)\, (a=b\Vdash \varphi), \\ a=b& \Vdash \exists x\, \varphi && \Leftrightarrow && \exists x\in \mathrm{V_{ext}}(A)\, (a=b\Vdash \varphi). \end{align*} $$

We will repeatedly use the following internal pairing function $\langle {x,y}\rangle _{\!A}$ in $\mathrm {V_{ext}}(A)$ .

Definition 3.14 (Pairing).

For $x,y\in \mathrm {V_{ext}}(A)$ , let

$$ \begin{align*} \{{x}\}_{A}&=\{\langle{\mathbf 0,\mathbf 0,x}\rangle\}, \\ \{{x,y}\}_{A}&=\{\langle{\mathbf 0,\mathbf 0,x}\rangle,\langle{{\mathbf 1},{\mathbf 1},y}\rangle\}, \\ \langle{x,y}\rangle_{\!A}&=\{\langle{\mathbf 0,\mathbf 0,\{{x}\}_{A}}\rangle, \langle{{\mathbf 1},{\mathbf 1},\{{x,y}\}_{A}}\rangle\}. \end{align*} $$

Note that all these sets are in $\mathrm {V_{ext}}(A)$ .

We use $\operatorname {{\mathrm {OP}}}(z,x,y)$ as abbreviation for the set-theoretic formula expressing that z is the ordered pair of x and y. In standard notation, $z=\langle {x,y}\rangle $ . Ordered pairs can be defined as usual as $\langle {x,y}\rangle =_{\mathrm {def}}\{\{x\},\{x,y\}\}$ .

Lemma 3.15. There are closed terms ${\mathbf u}_i$ such that $\mathsf {CZF}$ proves

$$ \begin{align*} {\mathbf u}_0 & \Vdash \operatorname{{\mathrm{OP}}}(\langle{x,y}\rangle_{\!A},x,y),\\ {\mathbf u}_1 & \Vdash \langle{x,y}\rangle_{\!A}=\langle{u,v}\rangle_{\!A}\rightarrow x=u\land y=v, \\ {\mathbf u}_2 &\Vdash \operatorname{{\mathrm{OP}}}(z,x,y) \rightarrow z=\langle{x,y}\rangle_{\!A}. \end{align*} $$

Proof This holds in the case of generic realizability. See [Reference Rathjen30, Theorem 6.2] for $\mathsf {REA}$ and [Reference Rathjen30, Theorem 10.1] for $\mathsf {DC}^{\dagger }$ (there called $\mathsf {DC}$ ), $\mathsf {RDC}$ , and $\mathsf { PAx}$ . The other axioms are treated in a similar way. In the case of extensional generic realizability, the proof is a nearly verbatim copy of that for generic realizability.

Let us sketch a proof for $\mathsf {PAx}$ . We wish to find a closed term ${\mathbf e}$ such that, over $\mathsf {CZF}+\mathsf {PAx}$ ,

$$\begin{align*}{\mathbf e}\Vdash \forall y\, \exists x\, \exists f\, (x \text{ is a base and } f\colon x\twoheadrightarrow y). \end{align*}$$

By definition, this means that for every $y\in \mathrm {V_{ext}}(A)$ there are $x,f\in \mathrm {V_{ext}}(A)$ such that

$$\begin{align*}{\mathbf e}\Vdash x \text{ is a base and } f\colon x\twoheadrightarrow y. \end{align*}$$

Let $y\in \mathrm {V_{ext}}(A)$ . By $\mathsf {PAx}$ in the background universe, there exists a base B and a function F from B onto y. Say $F(u)=\langle {a_u,b_u,z_u}\rangle \in y$ for $u\in B$ . By transfinite recursion, define

$$\begin{align*}\check u=\{\langle{\mathbf 0,\mathbf 0, \check{v}}\rangle\mid v\in u\}. \end{align*}$$

Then for every set u, $\check u\in \mathrm {V_{ext}}(A)$ . Moreover, by induction, one can show that these names are absolute, namely,

$$\begin{align*}u=v \leftrightarrow (\Vdash \check{u}=\check{v}). \end{align*}$$

Let

$$ \begin{align*} x&=\{\langle{a_u,b_u,\check u}\rangle\mid u\in B\},\\[5pt] f&=\{\langle{a_u,b_u,\langle{\check u,z_u}\rangle_{\!A}}\rangle\mid u\in B\}, \end{align*} $$

where $\langle {u,v}\rangle _{\!A}$ is the internal pair in $\mathrm {V_{ext}}(A)$ from Definition 3.14. One can find a closed term $\mathbf f$ such that $\mathbf f \Vdash \operatorname {{\mathrm {Fun}}}(f)$ thanks to the absoluteness of $\check {}$ names. It is not difficult to build a closed term ${\mathbf t}$ such that ${\mathbf t} \Vdash f\colon x\twoheadrightarrow y$ . Finally, it is straightforward to cook up a closed term $\mathbf b$ and show that $\mathbf b\Vdash x \text { is a base}$ , by using the fact that B is a base.

In view of Definition 3.18, our goal is to show that:

• • $T\models T+{\Pi }{\Sigma }\mathrm {I}\text {-}\mathsf {AC}^{\dagger }+{\Pi }{\Sigma }\mathrm {I}\text {-}\mathsf {RDC}^{\dagger }$ ,

• • $T+\mathsf {REA}\models T+\mathsf {REA}+{\Pi }{\Sigma }\mathrm {W}\mathrm {I}\text {-}\mathsf { AC}^{\dagger }+{\Pi }{\Sigma }\mathrm {W}\mathrm {I}\text {-}\mathsf {RDC}^{\dagger }$ ,

where T is as in Theorem 3.19.

4.1 Dependent types over partial combinatory algebras

Given a pca A, we wish to define extensional type structures on A, that is, structures of the form

$$\begin{align*}(\mathbb{T},\sim,(A_{\sigma},\sim_{\sigma})_{\sigma\in\mathbb{T}}), \end{align*}$$

where $\sim $ is a partial equivalence relation on A and $\sim _{\sigma }$ is a partial equivalence relation on A for every $\sigma $ such that $\sigma \sim \sigma $ . Then $\mathbb {T}=\{\sigma \in A\mid \sigma \sim \sigma \}$ and $A_{\sigma }=\{a\in A\mid a\sim _{\sigma } a\}$ for every $\sigma \in \mathbb {T}$ . Clearly, we want equivalent types to have the same elements. We must then ensure that if $\sigma \sim \tau $ , then $a\sim _{\sigma } b$ iff $a\sim _{\tau } b$ .

From now on, definitions and theorems take place in $\mathsf {CZF}$ , unless we are dealing with $\mathrm {W}$ -types, in which case we work in $\mathsf {CZF}+\mathsf {REA}$ .

Notation 4.2. Given a pca A, $a,b,c\in A$ , and $n\in \omega $ , we write:

$$ \begin{align*} \mathsf{N}_n&=_{\mathrm{def}} \mathbf p \bar 0\bar n, & \mathsf{N}&=_{\mathrm{def}}\mathbf p\bar 1\mathbf 0, \\ {\Pi}_ab&=_{\mathrm{def}} \mathbf p \bar 2(\mathbf pab), & {\Sigma}_ab&=_{\mathrm{def}}\mathbf p \bar 3(\mathbf pab), \\ \mathrm{I}_c(a,b)&=_{\mathrm{def}} \mathbf p \bar 4(\mathbf p c(\mathbf pab)), & \mathrm{W}_ab &=_{\mathrm{def}}\mathbf p \bar 5(\mathbf p ab). \end{align*} $$

This ensures unique readability. For example, $\mathsf {N}\neq {\Pi }_a b$ , and ${\Pi }_ab={\Pi }_cd$ implies $a=b$ and $c=d$ .

Remark 4.4. To be precise, each type structure from Definition 4.3 is an inductively defined class I of triples $\langle {\sigma ,\tau ,B}\rangle $ . The intended meaning is $\sigma \sim \tau $ and $a\sim _{\sigma } b$ iff $\langle {a,b}\rangle \in B$ . For instance, the rules for the introduction of ${\Pi }$ -types and $\mathrm {W}$ -types are

where $\sigma ,\tau ,i,j\in A$ , and for some set $B\subseteq A\times A$ and some function F with $\operatorname {{\mathrm {dom}}}(F)=B$ , we have:

• • $\{\langle {\sigma ,\tau ,B}\rangle \}\cup \{\langle {ia,jb,F(a,b)}\rangle \mid \langle {a,b}\rangle \in B\}\subseteq X$ ,

• • $C=\{\langle {f,g}\rangle \in A\times A\mid \forall \langle {a,b}\rangle \in B\, (\langle {fa,gb}\rangle \in F(a,b))\}$ ,

• • $D=\{\langle {c,d}\rangle \in A\times A\mid \langle {c_0,d_0}\rangle \in B\land \forall \langle {p,q}\rangle \in F(c_0,d_0)\, \langle {c_1p,d_1p}\rangle \in D\}$ .

It is not difficult to see that D has a bounded inductive definition, and therefore by Theorem 2.6 is a set in $\mathsf { CZF}+\mathsf {REA}$ .

By induction on the inductive definition of I, one may show that if $\langle {\sigma ,\tau _0,B_0}\rangle \in I$ and $\langle {\sigma ,\tau _1,B_1}\rangle \in I$ , then $B_0=B_1$ . Hence, by letting

$$ \begin{align*} \sim &=_{\mathrm{def}} \{\langle{\sigma,\tau}\rangle\mid \exists B\, \langle{\sigma,\tau,B}\rangle\in I\}, \\ \sim_{\sigma} &=_{\mathrm{def}} \bigcup\{ B\mid \exists \tau\, \langle{\sigma,\tau,B}\rangle\in I\}, \end{align*} $$

we obtain in particular that if $\langle {\sigma ,\tau ,B}\rangle \in I$ , then $B=\bigcup \{B\mid \exists \tau \, \langle {\sigma ,\tau ,B}\rangle \in I\}$ is a set, and so $\sim _{\sigma }$ is a set as well.

4.2 Representing ${\Pi }{\Sigma }\mathrm {W}\mathrm {I}$

Note that in any of the type structures here considered, if i is a family of types over $\sigma $ , then ${\Pi }_{\sigma } i$ and ${\Sigma }_{\sigma } i$ are types. Moreover, if $\sigma \sim \tau $ and $i\approx _{\sigma } j$ , then $i\approx _{\tau } j$ .

Definition 4.7 (Mapping typed elements of A in $\mathrm {V_{ext}}(A)$ ).

For $n\in \omega $ , let

$$\begin{align*}\dot n=\{\langle{\bar m,\bar m,\dot m}\rangle\mid m<n\}. \end{align*}$$

For every ${\Pi }{\Sigma }\mathrm {I}$ -type $\sigma $ , we inductively define $a^{\sigma }\in \mathrm {V_{ext}}(A)$ for every a of type $\sigma $ by:

• • if $\sigma =\mathsf {N}_n$ or $\sigma =\mathsf {N}$ , let $a^{\sigma }=\dot m$ , where $a=\bar m$ ;

• • if $\alpha ={\Pi }_{\sigma } i$ , let $ f^{\alpha }=\{\langle {a,b,\langle {a^{\sigma },(fa)^{\tau }}\rangle _{\!A}}\rangle \mid a\sim _{\sigma } b\land ia=\tau \}$ ;

• • if $\beta ={\Sigma }_{\sigma } i$ , let $ a^{\beta }=\langle {(a_0)^{\sigma },(a_1)^{\tau }}\rangle _{\!A}$ , where $ia_0= \tau $ ;

• • if $\gamma =\mathrm {I}_{\sigma }(a,b)$ , let $ c^{\gamma }=0 $ .

For ${\Pi }{\Sigma }\mathrm {W}\mathrm {I}$ -types, we add the clause:

• • if $\delta =\mathrm {W}_{\sigma } i$ , let $c^{\delta }=\langle {a^{\sigma },\{\langle {p,q,\langle {p^{ia},(c_1p)^{\delta }}\rangle _{\!A}}\rangle \mid p\sim _{ia} q\}}\rangle _{\!A}$ , where $a=c_0$ .

Remark 4.8. A comment on the above definition may be in order. The class function $(\sigma ,a)\mapsto a^{\sigma }$ is obtained by defining a class E of pairs $\langle {\sigma ,e_{\sigma }}\rangle $ , the intended meaning of which is $e_{\sigma }=\{\langle {a,a^{\sigma }}\rangle \mid a\in A_{\sigma }\}$ , where $A_{\sigma }=\{a\in A\mid a\text { has type } \sigma \}$ . Note that $A_{\sigma }$ is a set. Hence, $a^{\sigma }$ is really $e_{\sigma }(a)$ . For example, the rules for ${\Sigma }$ -types and $\mathrm {W}$ -types are

where $\sigma $ is type, i is a family of types over $\sigma $ , and there exist functions $e_{\sigma }$ and f on $A_{\sigma }$ such that:

• • $\operatorname {{\mathrm {Fun}}}(f(a))\land \operatorname {{\mathrm {dom}}}(f(a))=A_{ia}$ , for every $a\in A_{\sigma }$ ,

• • $X=\{\langle {\sigma ,e_{\sigma }}\rangle \}\cup \{\langle {ia,f(a)}\rangle \mid a\in A_{\sigma }\}$ ,

• • $e_{\beta }=\{\langle {a,\langle {e_{\sigma }(a_0),f(a_0,a_1)}\rangle _{\!A}}\rangle \mid a\text { has type } {\Sigma }_{\sigma } i\}$ ,

and $e_{\delta }$ is inductively defined by the clause:

• • if c has type $\mathrm {W}_{\sigma } i$ and there exists a function k with $\operatorname {{\mathrm {dom}}}(k)=A_{ic_0}$ such that $\langle {c_1p,k(p)}\rangle \in e_{\delta }$ for every $p\in \operatorname {{\mathrm {dom}}}(k)$ , then

  $$\begin{align*}\langle{c,\langle{e_{\sigma}(c_0),\{\langle{p,q,\langle{f(c_0,p), k(p)}\rangle_{\!A}}\rangle\mid p\sim_{ic_0} q\}}\rangle_{\!A}}\rangle \in e_{\delta}. \end{align*}$$

By induction on the inductive definition of E, one shows that E is a class function on $\mathbb {T}$ , and $E(\sigma )=e_{\sigma }\colon A_{\sigma }\to \mathrm {V_{ext}}(A)$ , for every type $\sigma $ . Note that $e_{\delta }$ has a bounded inductive definition and so is a set in $\mathsf {CZF}+\mathsf {REA}$ .

Proof By induction on the (inductive definition of the) type structure. The cases $\sigma =\tau =\mathsf {N}_n$ and $\sigma =\tau =\mathsf {N}$ are straightforward.

Let $\alpha ={\Pi }_{\sigma } i\sim {\Pi }_{\tau } j=\gamma $ and $f,g\in A_{\alpha }$ . Recall that:

$$ \begin{align*} f^{\alpha}&=\{\langle{a,b,\langle{a^{\sigma},(fa)^{ia}}\rangle_{\!A}}\rangle\mid a\sim_{\sigma} b\};\\ g^{\gamma}&=\{\langle{a,b,\langle{a^{\tau},(ga)^{ja}}\rangle_{\!A}}\rangle\mid a\sim_{\tau} b\}. \end{align*} $$

Suppose $\Vdash f^{\alpha }=g^{\gamma }$ . Let us show that $f\sim _{\alpha } g$ . Let $a\sim _{\sigma } b$ . We want to prove $fa\sim _{\rho } gb$ , where $\rho =ia$ . By definition of realizability, we have that

$$\begin{align*}\Vdash \langle{a^{\sigma},(fa)^{\rho}}\rangle_{\!A}=\langle{\breve{a}^{\tau},(g\breve{a})^{\eta}}\rangle_{\!A}, \end{align*}$$

for some $\breve {a}\in A_{\tau }$ , where $\eta =j\breve {a}$ . Then $\Vdash a^{\sigma }=\breve a^{\tau }$ and $\Vdash (fa)^{\rho }=(g\breve a)^{\eta }$ . By induction, $a\sim _{\sigma } \breve a$ and $fa\sim _{\rho } g\breve a$ . By Lemma 4.5, $\breve a\sim _{\sigma } b$ . Hence, $\breve a\sim _{\tau } b$ , and therefore $g\breve a\sim _{\eta } gb$ . Since $i\approx _{\sigma } j$ , it also follows from $a\sim _{\sigma } \breve a$ that $\rho \sim \eta $ . Thus $g\breve a\sim _{\rho } gb$ . By transitivity, $fa\sim _{\rho } gb$ .

Now suppose $f\sim _{\alpha } g$ . We wish to show that $f^{\alpha }=g^{\gamma }$ . Since $\sigma \sim \tau $ , it suffices to show that if $a\in A_{\sigma }$ , then $a^{\sigma }=a^{\tau }$ and $(fa)^{ia}=(ga)^{ja}$ . This follows by induction since $\sigma \sim \tau $ , $a\sim _{\sigma } a$ , $ia\sim ja$ , and $fa\sim _{ia} ga$ .

The cases ${\Sigma }_{\sigma } i$ , $\mathrm {I}_{\sigma }(a,b)$ and $\mathrm {W}_{\sigma } i$ are left as an exercise.

By virtue of Lemmas 4.5 and 4.11, every $X_{\sigma }$ is injectively presented in the following sense.

Definition 4.12. A set $x\in \mathrm {V_{ext}}(A)$ is injectively presented if

$$\begin{align*}x=\{\langle{a,b,f(a)}\rangle\mid a\sim b\}, \end{align*}$$

where $\sim $ is a partial equivalence relation on A and f is a (definable) function from the domain of $\sim $ to $\mathrm {V_{ext}}(A)$ such that:

• • $\Vdash f(a)=f(b)$ implies $a\sim b$ ;

• • $a\sim b$ implies $f(a)=f(b)$ .

This property will ensure the validity of choice for names of the form $X_{\sigma }$ (see Theorem 4.17).

Theorem 4.14. There are closed terms such that:

(i) $$ \begin{align} \mathbf o&\Vdash X_{\mathsf{N}}=\omega; \end{align} $$

(ii) $$ \begin{align} \mathbf{fun}&\Vdash \operatorname{{\mathrm{Fun}}}(F_{\sigma,i})\land \operatorname{{\mathrm{dom}}}(F_{\sigma,i}) = X_{\sigma}; \end{align} $$

(iii) $$ \begin{align} \mathbf{prod}&\Vdash X_{{\Pi}_{\sigma} i}={\Pi}(X_{\sigma}, F_{\sigma,i}); \end{align} $$

(iv) $$ \begin{align} \mathbf{sum}&\Vdash X_{{\Sigma}_{\sigma} i}={\Sigma}(X_{\sigma}, F_{\sigma,i}); \end{align} $$

(v) $$ \begin{align} \mathbf{id}&\Vdash X_{\mathrm{I}_{\sigma}(a,b)}=\mathrm{I}(a^{\sigma},b^{\sigma}); \end{align} $$

(vi) $$ \begin{align} \mathbf w&\Vdash X_{\mathrm{W}_{\sigma} i}=\mathrm{W}(X_{\sigma},F_{\sigma,i}), \end{align} $$

where $\sigma $ is a type, i is a family of types over $\sigma $ , and $a,b$ have type $\sigma $ .

Theorem 4.16. There are closed terms $\mathbf i$ and ${\mathbf e}$ such that:

$$\begin{align*}c=d\Vdash X\in {\Pi}{\Sigma}\mathrm{I} \ \ \text{implies} \ \ \sigma=\mathbf ic\sim\mathbf id\ \ \text{and}\ \ \mathbf ec={\mathbf e} d\Vdash X=X_{\sigma}, \end{align*}$$

for every $X\in \mathrm {V_{ext}}(A)$ . The same for ${\Pi }{\Sigma }\mathrm {W}\mathrm {I}$ .

We prove Theorems 4.14 and 4.16 in Section 6.

4.3 Realizing choice

Theorem 4.17 ( $\mathsf {AC}_{\sigma ,\tau }$ ).

There is a closed term ${\mathbf e}$ such that $\mathsf {CZF}$ proves

$$\begin{align*}{\mathbf e} \Vdash \forall x\in X_{\sigma}\, \exists y\in X_{\tau}\, \varphi(x,y)\rightarrow \exists f\colon X_{\sigma}\to X_{\tau}\, \forall x\in X_{\sigma}\, \varphi(x,f(x)), \end{align*}$$

for all ${\Pi }{\Sigma }\mathrm {I}$ -types $\sigma ,\tau $ and for every formula $\varphi $ . The same for $\mathsf {CZF}+\mathsf {REA}$ and ${\Pi }{\Sigma }\mathrm {W}\mathrm {I}$ -types.

Proof Suppose $c=d\Vdash \forall x\in X_{\sigma }\, \exists y\in X_{\tau }\, \varphi (x,y)$ . Then, whenever $a\sim _{\sigma } b$ , we have $(ca)_0\sim _{\tau } (db)_0$ and $(ca)_1=(db)_1\Vdash \varphi (a^{\sigma },e^{\tau })$ , where $e=(ca)_0$ . Let

$$\begin{align*}f=\{\langle{a,b,\langle{a^{\sigma},e^{\tau}}\rangle_{\!A}}\rangle\mid a\sim_{\sigma} b\land e=(ca)_0\}. \end{align*}$$

Then $f\in \mathrm {V_{ext}}(A)$ . We wish to find ${\mathbf e}$ such that

$$\begin{align*}{\mathbf e} c=\mathbf ed\Vdash f\colon X_{\sigma}\to X_{\tau}\land \forall x\in X_{\sigma}\, \varphi(x,f(x)). \end{align*}$$

It suffices to look for closed terms $\mathbf {r},\mathbf {c},\mathbf {f}$ such that:

(1) $$ \begin{align} \mathbf{r}c = \mathbf{r}d \Vdash f\subseteq X_{\sigma}\times X_{\tau}, \qquad\qquad\qquad\qquad\qquad\qquad \end{align} $$

(2) $$ \begin{align} \mathbf cc = \mathbf cd \Vdash \forall x\in X_{\sigma}\, \exists y\, \exists z\in f\, (\operatorname{{\mathrm{OP}}}(z,x,y)\land \varphi(x,y)), \end{align} $$

(3) $$ \begin{align} \mathbf fc = \mathbf fd \Vdash f \text{ is functional}, \qquad\qquad\qquad\qquad\qquad\quad \ \ \end{align} $$

where $f\subseteq X_{\sigma }\times X_{\tau }$ stands for $\forall z\in f\, \exists x\in X_{\sigma }\, \exists y\in X_{\tau }\, \operatorname {{\mathrm {OP}}}(z,x,y)$ , and f is functional stands for

$$\begin{align*}\forall z_0\in f\, \forall z_1\in f\, \forall x\, \forall y_0\, \forall y_1\, (\operatorname{{\mathrm{OP}}}(z_0,x,y_0)\land \operatorname{{\mathrm{OP}}}(z_1,x,y_1)\rightarrow y_0=y_1). \end{align*}$$

(1) and (2) are straightforward. (3) Let $a\sim _{\sigma } b$ and $\breve a\sim _{\sigma } \breve b$ . We want

$$\begin{align*}\mathbf fca\breve a=\mathbf fd b\breve b\Vdash \operatorname{{\mathrm{OP}}}(\langle{a^{\sigma},e^{\tau}}\rangle_{\!A},x,y_0)\land \operatorname{{\mathrm{OP}}}(\langle{\breve a^{\sigma},\breve e^{\tau}}\rangle_{\!A},x,y_1)\rightarrow y_0=y_1, \end{align*}$$

for all $x,y_0,y_1\in \mathrm {V_{ext}}(A)$ , where $e=(ca)_0$ and $\breve e=(c\breve a)_0$ . Suppose

$$\begin{align*}\breve c=\breve d\Vdash \operatorname{{\mathrm{OP}}}(\langle{a^{\sigma},e^{\tau}}\rangle_{\!A},x,y_0)\land \operatorname{{\mathrm{OP}}}(\langle{\breve a^{\sigma},\breve e^{\tau}}\rangle_{\!A},x,y_1). \end{align*}$$

In particular, $\Vdash a^{\sigma }=\breve a^{\sigma }$ . By Lemma 4.11, $a\sim _{\sigma } \breve a$ . By Lemma 4.5, since $(ca)_0\sim _{\tau } (da)_0$ and $(c\breve a)_0\sim _{\tau } (da)_0$ , it follows that $(ca)_0\sim _{\tau } (c\breve a)_0$ . That is, $e\sim _{\tau } \breve e$ . By Lemma 4.11 again, we get $e^{\tau }=\breve e^{\tau }$ . By the properties of equality, there is a closed term $\mathbf q$ such that $\mathbf q\breve c=\mathbf q\breve d\Vdash y_0=y_1$ . We may let $\mathbf f=_{\mathrm {def}}\lambda ca\breve a\breve c. \mathbf q\breve c$ .

Theorem 4.18 ( $\mathsf {RDC}_{\sigma }$ ).

There is a closed term ${\mathbf e}$ such that $\mathsf {CZF}$ proves

$$ \begin{align*} {\mathbf e} \Vdash \forall x\in X_{\sigma}\, &(\psi(x)\rightarrow \exists y\in X_{\sigma}\, (\psi(x)\land \varphi(x,y))) \rightarrow \forall x\in X_{\sigma}\, (\psi(x)\rightarrow \\ &\qquad\qquad\qquad\exists f\colon \omega\to X_{\sigma}\, (f(0)=x\land \forall n\in\omega\, \varphi(f(n),f(n+1)))), \end{align*} $$

for every ${\Pi }{\Sigma }\mathrm {I}$ -type $\sigma $ and for every formula $\varphi $ . The same for $\mathsf {CZF}+\mathsf {REA}$ and ${\Pi }{\Sigma }\mathrm {W}\mathrm {I}$ -types.

Proof Suppose

(1) $$ \begin{align} c=d\Vdash \forall x\in X_{\sigma}\, (\psi(x)\rightarrow \exists y\in X_{\sigma}\, (\psi(y)\land \varphi(x,y))), \end{align} $$

$\mathring a\sim _{\sigma } \mathring b$ and $\mathring c=\mathring d\Vdash \psi (a^{\sigma })$ . We search for ${\mathbf e}$ such that

$$\begin{align*}{\mathbf e} c\mathring a\mathring c=\mathbf ed\mathring b\mathring d\Vdash \exists f \colon \omega\to X_{\sigma}\, (f(0)=\mathring a^{\sigma}\land \forall n\in\omega\, \varphi(f(n),f(n+1))). \end{align*}$$

By (1), whenever $a\sim _{\sigma } b$ and $\breve c=\breve d\Vdash \psi (a^{\sigma })$ , we have

(2) $$ \begin{align} e=(ca\breve c)_0\sim_{\sigma} (d b\breve d)_0, \end{align} $$

(3) $$ \begin{align} (ca\breve c)_1= (db\breve d)_1\Vdash \psi(e^{\sigma})\land \varphi(a^{\sigma}, e^{\sigma}). \end{align} $$

In every pca one can simulate primitive recursion. We thus have a closed term $\mathbf r$ satisfying the following equations, where r is an abbreviation for $\mathbf rc\mathring a\mathring c$ :

$$ \begin{align*} r\mathbf 0&\simeq \mathbf p \mathring a(\mathbf p\mathring c\mathbf 0);\\ r\overline{n+1}&\simeq \mathbf p (c(r\bar n)_0(r\bar n)_{10} )_0 (c(r\bar n)_0(r\bar n)_{10})_1. \end{align*} $$

By induction, owing to (2) and (3), one can verify that for every $n\in \omega $ ,

$$\begin{align*}a_n=(\mathbf rc\mathring a\mathring c \bar n)_0\sim_{\sigma} (\mathbf rd\mathring b\mathring d \bar n)_0=b_n, \end{align*}$$

$$\begin{align*}(\mathbf rc\mathring{a}\mathring{c}\: \overline{n+1})_1= (\mathbf rd\mathring b\mathring{d}\: \overline{n+1})_1\Vdash \psi(a_n^{\sigma})\land \varphi(a_n^{\sigma},a_{n+1}^{\sigma}). \end{align*}$$

Note that $\mathring a=(\mathbf rc\mathring a\mathring c \mathbf 0)_0\sim _{\sigma } (\mathbf rd\mathring b\mathring d \mathbf 0)_0=\mathring b$ , and $\mathring c=(\mathbf rc\mathring a\mathring c \mathbf 0)_{10}= (\mathbf rd\mathring b\mathring d \bar 0)_{10}=\mathring d \Vdash \psi (\mathring a^{\sigma })$ . Let

$$\begin{align*}f=\{\langle{\bar n,\bar n,\langle{\dot n,a_n^{\sigma}}\rangle_{\!A}}\rangle\mid n\in\omega\land a_n=(\mathbf rc\mathring a\mathring c \bar n)_0\}. \end{align*}$$

Then $f\in \mathrm {V_{ext}}(A)$ . By using $\mathbf r$ , it is not difficult to build ${\mathbf e}$ such that

$$\begin{align*}{\mathbf e} c\mathring a\mathring c=\mathbf ed\mathring b\mathring d\Vdash f \colon \omega\to X_{\sigma}\land f(0)=\mathring a^{\sigma}\land \forall n\in\omega\, \varphi(f(n),f(n+1)).\\[-2.8pc] \end{align*}$$

4.4 Failure of presentation

The interpretations of $\mathsf {CZF}$ and $\mathsf {CZF}+\mathsf {REA}$ in type theory validate strong presentation axioms (see Section 2.5). It is natural to ask whether extensional generic realizability validates the statement that every set is an image of a ${\Pi }{\Sigma }\mathrm {I}$ -set, even under the assumption that this holds in the background universe. If it did, in view of Theorems 2.16 and 4.19, we would obtain that $T+\text {every set is an image of a } {\Pi }{\Sigma }\mathrm {I}\text {-set} \models {\Pi }{\Sigma }\mathrm {I}\text {-}\mathsf {PAx}$ , and similarly for $T+\mathsf {REA}$ and ${\Pi }{\Sigma }\mathrm {W}\mathrm {I}$ -sets. However, the answer is negative.

Theorem 4.21. The following holds.

$$\begin{align*}\mathsf{CZF}\models\text{there is a set that is not an image of a } {\Pi}{\Sigma}\mathrm{I}\text{-set}. \end{align*}$$

Similarly for $\mathsf {CZF}+\mathsf {REA}$ and ${\Pi }{\Sigma }\mathrm {W}\mathrm {I}$ -sets.

Proof Let $y=\{\langle {\mathbf 0,\mathbf 0,\dot 0}\rangle ,\langle {\mathbf 0,\mathbf 0,\dot 1}\rangle \}\in \mathrm {V_{ext}}(A)$ . Although y is in bijection with $2=\{0,1\}$ , this fact is not realizable. The proof is the same in both cases. Let us consider the ${\Pi }{\Sigma }\mathrm {I}$ case and show that

$$\begin{align*}\mathbf 0\Vdash \neg \exists X\, \exists f\, (X\in{\Pi}{\Sigma}\mathrm{I}\land f\colon X \twoheadrightarrow y). \end{align*}$$

Towards a contradiction, suppose $\Vdash X\in {\Pi }{\Sigma }\mathrm {I}\land f\colon X \twoheadrightarrow y$ , for some $X,f\in \mathrm {V_{ext}}(A)$ . By soundness and Theorem 4.16, there is a ${\Pi }{\Sigma }\mathrm {I}$ -type $\sigma $ such that $\Vdash f\colon X_{\sigma } \twoheadrightarrow y$ . In particular, there are $a,b$ such that

$$\begin{align*}a=b\Vdash \forall v\in y\, \exists x\in X_{\sigma}\, \exists z\in f\, \operatorname{{\mathrm{OP}}}(z,x,v). \end{align*}$$

By unpacking the definition, we must have $\breve a= (a\mathbf 0)_0\sim _{\sigma }(b\mathbf 0)_0=\breve b$ and

$$\begin{align*}\Vdash \exists z\in f\, \operatorname{{\mathrm{OP}}}(z,x,\dot 0)\land \exists z\in f\, \operatorname{{\mathrm{OP}}}(z,x,\dot 1), \end{align*}$$

where $x=\breve a^{\sigma }$ . From $\Vdash \operatorname {{\mathrm {Fun}}}(f)$ , we then obtain $\Vdash \dot 0=\dot 1$ , which implies $0=1$ , for the desired contradiction.

On absoluteness

For every set x, define by transfinite recursion the name $\check x\in \mathrm {V}(\mathbb {P})$ by $\check x=\{\langle {p,\check y}\rangle \mid p\in \mathbb {P} \land y\in x\}$ . We set out to prove that for every arithmetic formula $\varphi (x_1,\ldots ,x_n)$ ,

(5) $$ \begin{align} S\vdash \forall x_1\in\omega \cdots \forall x_n\in\omega \, \forall p\, (\varphi(x_1,\ldots,x_n)\leftrightarrow p\Vdash_{\mathbb{P}} \varphi(\check x_1,\ldots,\check x_n)). \end{align} $$

The absoluteness of arithmetic sentences in the sense of (3) then follows.

It is an easy exercise to show that (5) is preserved under logical connectives and number quantifiers. It is thus sufficient to show that for every primitive recursive function $f(x_1,\ldots ,x_n)$ , the primitive recursive formula $\varphi _f(x_1,\ldots ,x_n,y)$ defining f satisfies (5). This is proved by (an external) induction on the generation of f.

For example, suppose $f(x_1,\ldots ,x_n,x)$ is defined by primitive recursion from $g(x_1,\ldots ,x_n)$ and $h(x_1,\ldots ,x_n,x,y)$ , namely,

$$ \begin{align*} f(x_1,\ldots,x_n,0)&=g(x_1,\ldots,x_n);\\ f(x_1,\ldots,x_n,x+1)&=h(x_1,\ldots,x_n,x,f(x_1,\ldots,x_n,x)). \end{align*} $$

Define $\varphi _f(x_1,\ldots ,x_n,x,y)$ as $\exists z\, (\psi (z) \land z(x)=y)$ , where $\psi (z)$ is

$$ \begin{align*} \operatorname{{\mathrm{Fun}}}(z)&\land \operatorname{{\mathrm{dom}}}(z) \in\omega \land (0\in\operatorname{{\mathrm{dom}}}(z)\rightarrow \varphi_g(x_1,\ldots,x_n,z(0))) \\ &\land \forall n\in\operatorname{{\mathrm{dom}}}(z)\, \forall m\in n\, (n=m+1\rightarrow \varphi_h(x_1,\ldots,x_n,n,z(m),z(n))). \end{align*} $$

(Note that $\varphi _f$ is equivalent to a $\Sigma $ formula if $\varphi _g$ and $\varphi _h$ are also $\Sigma $ definable.) One shows that (5) holds for $\varphi _f(x_1,\ldots ,x_n,x,y)$ , by assuming that it holds for $\varphi _g$ and $\varphi _h$ . The left-to-right direction of (5) requires some standard absoluteness arguments. For the right-to-left direction, one also uses the fact that, for every primitive recursive function $f(x_1,\ldots ,x_n)$ ,

$$ \begin{align*} S&\vdash \forall x_1\in\omega\cdots \forall x_n\in\omega\, (\exists y\in\omega \, \varphi_f(x_1,\ldots,x_n,y) \\ & \qquad \land \forall y_0\, \forall y_1\, (\varphi_f(x_1,\ldots,x_n,y_0)\land \varphi_f(x_1,\ldots,x_n,y_1)\rightarrow y_0=y_1)), \end{align*} $$

and thereby this is forced in S.

On forcing self-realizability

To obtain (4), one shows that for every arithmetic formula $\varphi (x_1,\ldots ,x_n)$ there is a $\mathbb {P}$ such that S proves:

1. (i) there is $e\in \omega $ such that for every p there is a $q\supseteq p$ forcing

   $$ \begin{align*} & \forall a_1\in\omega\cdots\forall a_n\in\omega\, (\varphi(a_1,\ldots,a_n)\rightarrow \\ & \qquad\qquad\qquad \exists b\in\omega\, (\{\check e\}^g(a_1,\ldots,a_n,0)=b\land b\Vdash_{\omega} \varphi(\dot a_1,\ldots,\dot a_n))); \end{align*} $$

2. (ii) for every p there is a $q\supseteq p$ forcing

   $$\begin{align*}\forall a_1\in\omega\cdots\forall a_n\in\omega\, \forall a,b\in\omega\, ((a=b\Vdash_{\omega} \varphi(\dot a_1,\ldots,\dot a_n))\rightarrow \varphi(a_1,\ldots,a_n)). \end{align*}$$

Here, $\{e\}^f(a,b)$ stands for $\{\{e\}^f(a)\}^f(b)$ , and so on and so forth. On a technical note, the dummy argument for $0$ is used to handle the case where $\varphi $ is closed.

Now, let $\varphi (x_1,\ldots ,x_n)$ be arithmetic. We define $\mathbb {P}$ as follows. First, let $\mathbb {Q}$ be the set of partial functions p from $\omega $ to $\omega $ such that $\operatorname {{\mathrm {dom}}}(p)$ is an image of a natural number. The point of this definition is just to make sure that, within $\mathsf {CZF}$ , the class $\mathbb {Q}$ exists as a set and the domain of every $p\in \mathbb {Q}$ is decidable, in the sense that

$$\begin{align*}\forall p\in\mathbb{Q}\, \forall x\in\omega\, (x\in\operatorname{{\mathrm{dom}}}(p)\lor x\notin\operatorname{{\mathrm{dom}}}(p)). \end{align*}$$

Note that if we are working in $\mathsf {IZF}$ , we can directly define the set $\mathbb {Q}$ of all partial functions from $\omega $ to $\omega $ with decidable domain. Enumerate all subformulas $\varphi _1,\ldots ,\varphi _k$ of $\varphi $ starting from the primitive recursive ones. Let $\mathbb {P}$ be the set of $p\in \mathbb {Q}$ such that for every subformula $\varphi _i(y_1,\ldots , y_{j}) $ of the form $\psi _0\lor \psi _1$ , for every $a_1,\ldots ,a_j\in \omega $ , if $a=(i,a_1,\ldots ,a_j)\in \operatorname {{\mathrm {dom}}}(p)$ , then $p(a)=0\land \psi _0(a_1,\ldots ,a_j)$ or $p(a)=1\land \psi _0(a_1,\ldots ,a_j)$ , and for every subformula $\varphi _i(y_1,\ldots ,y_j)$ of the form $\exists x\, \psi (x,y_1,\ldots ,y_j)$ , for every $a_1,\ldots ,a_j\in \omega $ , if $a=(i,a_1,\ldots ,a_j)\in \operatorname {{\mathrm {dom}}}(p)$ , then $\psi (p(a),a_1,\ldots ,a_j)$ .

One can write down a formula defining $\mathbb {P}$ as there are standard finitely many subformulas of $\varphi $ . Here, $(a_1,\ldots ,a_j)$ is a primitive recursive coding of sequences of natural numbers. One then shows (i) and (ii) for every subformula of $\varphi $ .

If $\varphi $ is primitive recursive, then one can find a number e such that

$$ \begin{align*} S^g\vdash \forall a_1,\ldots,a_n\in\omega (\varphi(a_1,\ldots,a_n) \leftrightarrow \{e\}^g(a_1,\ldots,a_n)\Vdash_{\omega} \varphi(\dot a_1,\ldots,\dot a_n)), \end{align*} $$

where we identify e with the corresponding numeral. This fact can be gleaned from [Reference McCarty22, Chapter 4, Theorem 2.6] in the case of $\mathsf {IZF}$ . The same holds for $\mathsf {CZF}$ [Reference Rathjen30, Proposition 8.5]. We can then use the soundness of forcing to get (i) and (ii).

The index of complex subformulas is computed according to the following table. Let i be the number of the given subformula according to our enumeration. Write $\vec {a}$ for the tuple $a_1,\ldots ,a_j$ .

$$ \begin{align*} \{e_{\varphi\land\psi}\}^f(\vec a,0)&\simeq (\{e_{\varphi}\}^f(\vec a,0),\{e_{\psi}\}^f(\vec a,0)), \\ \{e_{\varphi\lor\psi}\}^f(\vec a,0)&\simeq \begin{cases} \{e_{\varphi}\}^f(\vec a,0), & \text{if } f(i,\vec a)=0, \\ \{e_{\psi}\}^f(\vec a,0),& \text{if } f(i,\vec a)=1, \end{cases} \\ \{e_{\forall x\in\omega\, \varphi(x)}\}^f(\vec a,0,b)&\simeq \{e_{\varphi}\}^f(\vec a,b,0),\\ \{e_{\exists x\in\omega\, \varphi(x)}\}^f(\vec a,0)&\simeq (f(i,\vec a),\{e_{\varphi}\}^f(\vec a,f(i,\vec a),0)). \end{align*} $$

By way of example, let us illustrate how to obtain (i) in the existential case. For simplicity, suppose we have a subformula of the form $\exists y\in \omega \, \varphi (x,y)$ . We work in S. We have already found an index $e_{\varphi }$ for $\varphi $ . So, let e be such that

$$\begin{align*}\{e\}^f(a,0)\simeq (f(i,a),\{e_{\varphi}\}^f(a,f(i,a),0)). \end{align*}$$

Let $p\in \mathbb {P}$ . We search for a $q\supseteq p$ such that

$$\begin{align*}q\Vdash_{\mathbb{P}} \forall a\in\omega\, (\exists y\in\omega\, \varphi(a,y)\rightarrow \{\check e\}^g(a,0)\Vdash_{\omega} \exists y\in\omega\, \varphi(\dot a,y)). \end{align*}$$

Notice that, within $S^g$ ,

$$\begin{align*}(a=b\Vdash_{\omega} \exists x\in\omega\, \varphi(x)) \leftrightarrow \exists n\in\omega\, ((a)_0=(b)_0=n\land (a)_1=(b)_1\Vdash_{\omega} \varphi(\dot n)), \end{align*}$$

and thereby this is forced in S. It is then enough to find an extension $q\supseteq p$ such that

(1) $$ \begin{align} q&\Vdash_{\mathbb{P}} \forall a\in\omega\, (\exists y\in\omega\, \varphi(a,y)\rightarrow \exists c\in\omega\, \exists b\in\omega\, (\{\check e\}^g(a,0)\simeq c \notag \\ &\qquad\qquad\qquad\qquad\qquad\qquad\qquad \land (c)_0=b \land (c)_1\Vdash_{\omega} \varphi(\dot a,\dot b))). \end{align} $$

We claim that p already satisfies (1). Let $a\in \omega $ , $q\supseteq p$ , and suppose $q\Vdash _{\mathbb {P}} \exists y\in \omega \, \varphi (\check a,y)$ . We are clear if we find $r\supseteq q$ such that

(2) $$ \begin{align} r&\Vdash_{\mathbb{P}} \exists c\in\omega\, \exists b\in\omega\, (\{\check e\}^g(\check a,0)\simeq c\land (c)_0=b \notag \\ & \qquad\qquad \land \forall x\, (i(\check a,x)\rightarrow (c)_1\Vdash_{\omega} \varphi(x,\dot b))), \end{align} $$

where the formula $i(x,y)$ expresses that $y=\dot x$ for $x\in \omega $ . By definition, there is a $b\in \omega $ such that $q\Vdash _{\mathbb {P}} \varphi (\check a,\check b)$ . By absoluteness, $\varphi (a,b)$ holds. Now, we can decide whether $(i,a)\in \operatorname {{\mathrm {dom}}}(q)$ . If not, we can take $q'=q\cup \{\langle {(i,a),b}\rangle \}$ . By the assumption on $e_{\varphi }$ , there is an $s\supseteq q'$ such that

(3) $$ \begin{align} & s\Vdash_{\mathbb{P}} \exists c_1\in\omega\, (\{\check e_{\varphi}\}^g(\check a,\check b,0)\simeq c_1 \notag \\ & \qquad\qquad\qquad \land \forall x\, \forall y\, (i(\check a,x)\land i(\check b,y) \rightarrow c_1\Vdash_{\omega} \varphi(x,y))). \end{align} $$

One can see that $s\Vdash _{\mathbb {P}} \{\check e\}^g(\check a,0)\simeq (\check b,\{\check e_{\varphi }\}^g(\check a,\check b,0))$ . By (3) and soundness, one can finally find an $r\supseteq s$ satisfying (2), as desired.

Adding parameters

We briefly discuss how to generalize such conservation result to arithmetic formulas with type $1$ parameters. For example, suppose $S+\Phi \vdash \forall f\in \omega ^{\omega }\, \varphi (f)$ . Then $(S+\Phi )_f\vdash \varphi (f)$ , where, in general, $T_f$ is obtained from T by adjoining a constant symbol f and an axiom saying that f is a function from $\omega $ to $\omega $ . It clearly suffices to show that $S_f\vdash \varphi (f)$ . If we do so, then $S\vdash \forall f\in \omega ^{\omega }\, \varphi (f)$

Now consider the theory $(S_f)^g$ obtained from $S_f$ by further extending the language with a constant symbol g and an axiom saying that g is a partial function from $\omega $ to $\omega $ . Within $(S_f)^g$ , consider extensional generic realizability $a=b\Vdash _{\omega } \varphi $ , where $a,b\in \omega $ and $\varphi $ is a formula of $S_f$ , by using partial recursive application relative to the oracle $f\oplus g=\{\langle {2n,f(n)}\rangle \mid n\in \omega \}\cup \{\langle {2n+1,g(n)}\rangle \mid n\in \operatorname {{\mathrm {dom}}}(g)\}$ . Use the name $\dot f=\{\langle {n,n,\langle {\dot n,\dot m}\rangle _{\omega }}\rangle \mid f(n)=m\}\in \mathrm {V_{ext}}(\omega )$ to define realizability on formulas containing f. Note that we could extend the interpretation to every formula of $(S_f)^g$ by interpreting g with $\dot g$ , which is defined in a similar way as $\dot f$ . Show that

$$\begin{align*}\text{if } (S+\Phi)_f\vdash \psi, \text{ then } (S_f)^g\vdash \exists e\in\omega\, (e\Vdash_{\omega} \psi). \end{align*}$$

Similarly for $(S+\mathsf {REA}+\Psi )_f$ and $(S_f+\mathsf {REA})^g$ . In particular, we must have

$$\begin{align*}(S_f)^g\vdash \exists e\in\omega\, (e\Vdash_{\omega} f\colon\omega\to\omega). \end{align*}$$

This is the realizability part.

In $S_f$ , given any definable set $\mathbb {P}$ of partial functions from $\omega $ to $\omega $ , where now we can use the parameter f in defining $\mathbb {P}$ , we extend the forcing interpretation $p\Vdash _{\mathbb {P}} \varphi $ of Definition 5.4 to formulas of $(S_f)^g$ by interpreting g with $\mathring g$ , like before, and f with $\check f$ . Note that $\check f=\{\langle {p,\check z}\rangle \mid p\in \mathbb {P}\land z\in f\}=\{\langle {p,\langle {\check n,\check m}\rangle _{\mathbb {P}}}\rangle \mid p\in \mathbb {P}\land f(n)=m\}$ . The rest of the argument is roughly as before, but with everything relativized to the parameter f. In particular, one must show that arithmetic (in f) formulas are absolute for forcing. Finally, given $\varphi (f)$ , one defines $\mathbb {P}$ as before, but relative to f, and show that in $\mathrm {V}(\mathbb {P})$ , $\varphi (f)$ is self-realizing.⊣