# Extensional realizability for intuitionistic set theory

Emanuele Frittaion  School of Mathematics, University of Leeds, UK  and
Michael Rathjen  School of Mathematics, University of Leeds, UK

###### Abstract.

In generic realizability for set theories, realizers treat unbounded
quantifiers generically. To this form of realizability, we add another layer
of extensionality by requiring that realizers ought to act extensionally on
realizers, giving rise to a realizability universe $\mathrm{V_{ex}}(A)$ in
which the axiom of choice in all finite types, ${\sf AC}_{{\sf FT}}$, is
realized, where $A$ stands for an arbitrary partial combinatory algebra. This
construction furnishes “inner models” of many set theories that additionally
validate ${\sf AC}_{{\sf FT}}$, in particular it provides a self-validating
semantics for ${\sf CZF}$ (Constructive Zermelo-Fraenkel set theory) and ${\sf
IZF}$ (Intuitionistic Zermelo-Fraenkel set theory). One can also add large set
axioms and many other principles.

###### Key words and phrases:

Intuitionistic, constructive, set theory, realizability, extensionality

###### 2010 Mathematics Subject Classification:

Primary: 03F03; Secondary: 03F25, 03F50

The authors’ research was supported by a grant from John Templeton Foundation
“A new dawn of Intuitionism: Mathematical and Philosophical advances” (grant
ID 60842).

###### Contents

  1. 1 Introduction
  2. 2 Partial combinatory algebras
  3. 3 The theory ${\sf CZF}$
  4. 4 Finite types and axiom of choice
  5. 5 Defining extensional realizability in ${\sf CZF}$
  6. 6 Soundness for intuitionistic first order logic with equality
  7. 7 Soundness for ${\sf CZF}$
  8. 8 Realizing the axiom of choice in all finite types
  9. 9 Soundness for ${\sf IZF}$
  10. 10 Conclusions

##  1\. Introduction

In this paper we define an extensional version of generic111The descriptive
attribute “generic” for this kind of realizability is due to McCarty [19, p.
31]. realizability over any given partial combinatory algebra (pca) and prove
that it provides a self-validating semantics for ${\sf CZF}$ (Constructive
Zermelo-Fraenkel set theory) as well as ${\sf IZF}$ (Intuitionistic Zermelo-
Fraenkel set theory), i.e., every theorem of ${\sf CZF}$ (${\sf IZF}$) is
realized by just assuming the axioms of ${\sf CZF}$ (${\sf IZF}$) in the
background theory. Moreover, it is shown that the axiom of choice in all
finite types, ${\sf AC}_{{\sf FT}}$, also holds under this
interpretation.222As a byproduct, we reobtain the already known result (e.g.
[24, 4.31, 4.33]) that augmenting ${\sf CZF}$ by ${\sf AC}_{{\sf FT}}$ does
not increase the stock of provably recursive functions. Likewise, we reobtain
the result (a consequence of [13]) that augmenting ${\sf IZF}$ by ${\sf
AC}_{{\sf FT}}$ does not increase the stock of provably recursive functions.
This uniform tool of realizability can be combined with forcing to show that
${\sf IZF}+{\sf AC}_{{\sf FT}}$ is conservative over ${\sf IZF}$ with respect
to arithmetic formulae (and similar results with large set axioms). For
special cases, namely, finite type dependent choice, ${\sf DC}_{{\sf FT}}$,
and finite type countable choice, ${\sf CAC}_{{\sf FT}}$,333${\sf DC}_{{\sf
FT}}$ is the scheme $\forall x^{\sigma}\,\exists
y^{\sigma}\,\varphi(x,y)\to\forall x^{\sigma}\,\exists
f^{0\sigma}\,[f(0)=x\;\wedge\;\forall n\,\varphi(f(n),f(n+1))]$, while ${\sf
CAC}_{{\sf FT}}$ stands for the scheme $\forall n\,\exists
y^{\tau}\,\varphi(n,y)\to\exists f^{0\tau}\,\forall n\,\varphi(n,f(n))$. this
has been shown in [12, Theorem 5.1] and [5, XV.2], but not for ${\sf AC}_{{\sf
FT}}$. The same technology works for ${\sf CZF}$. However, for several
subtheories of ${\sf CZF}$ (with exponentiation in lieu of subset collection)
such conservativity results have already been obtained by Gordeev [16] by very
different methods, using total combinatory algebras and an abstract form of
realizability combined with genuine proof-theoretic machinery.

Generic realizability is markedly different from Kleene’s number and function
realizability as well as modified realizability. It originates with Kreisel’s
and Troelstra’s [18] definition of realizability for second order Heyting
arithmetic and the theory of species. Here, the clauses for the realizability
relation $\Vdash$ relating to second order quantifiers are the following:
$e\Vdash\forall X\,\phi(X)\Leftrightarrow\forall X\,e\Vdash\phi(X)$,
$e\Vdash\exists X\,\phi(X)\Leftrightarrow\exists X\,e\Vdash\phi(X)$. This type
of realizability does not seem to give any constructive interpretation to set
quantifiers; realizing numbers “pass through” quantifiers. However, one could
also say that thereby the collection of sets of natural numbers is generically
conceived. Kreisel-Troelstra realizability was applied to systems of higher
order arithmetic and set theory by Friedman [14] and to further set theories
by Beeson [4]. An immediate descendant of the interpretations of Friedman and
Beeson was used by McCarty [19, 20], who, unlike the realizabilities of
Beeson, devised realizability directly for extensional ${\sf IZF}$: “we found
it a nuisance to interpret the extensional theory into the intensional before
realizing.”  ([19, p. 82]). A further generalization, inspired by a remark of
Feferman in [9], that McCarty introduced was that he used realizers from
applicative structures, i.e. arbitrary models of Feferman’s theory
$\mathrm{APP}$, rather than just natural numbers.

Generic realizability [19] is based on the construction of a realizability
universe $\mathrm{V}(A)$ on top of an applicative structure or partial
combinatory algebra $A$. Whereas in [19, 20] the approach is geared towards
${\sf IZF}$, making use of transfinite iterations of the powerset operation,
it was shown in [25] that ${\sf CZF}$ suffices for a formalization of
$\mathrm{V}(A)$ and the generic realizability based upon it. This tool has
been successfully applied to the proof-theoretic analysis of ${\sf CZF}$ ever
since [22, 23, 26, 28].

With regard to ${\sf AC}_{{\sf FT}}$, it is perhaps worth mentioning that, by
using generic realizability [19], one can show that ${\sf AC}_{0,\tau}$ for
$\tau\in\\{0,1\\}$ holds in the realizability universe $\mathrm{V}(A)$ for any
pca $A$ (cf. also [8]). For instance, one can take Kleene’s first algebra.
With some effort, one can also see that ${\sf AC}_{1,\tau}$ for
$\tau\in\\{0,1\\}$ holds in $\mathrm{V}(A)$ by taking, e.g., Kleene’s second
algebra. It is conceivable that one can construct a specific pca $A$ so as to
validate ${\sf AC}_{{\sf FT}}$ in $\mathrm{V}(A)$. In this paper we show that,
by building extensionality into the realizability universe and by adapting the
definition of realizability, it is possible to satisfy choice in all finite
types at once, regardless of the partial combinatory algebra $A$ one starts
with.

Extensional variants of realizability in the context of (finite type)
arithmetic have been investigated by Troelstra (see [32]) and van Oosten [34,
35], as well as [15, 33], and for both arithmetic and set theory by Gordeev in
[16]. For earlier references on extensional realizability, in particular [17],
where the notion for first order arithmetic first appeared, and [21], see
Troelstra [32, p. 441].

##  2\. Partial combinatory algebras

Combinatory algebras are the brainchild of Schönfinkel [27] who presented his
ideas in Göttingen in 1920. The quest for an optimization of his framework,
singling out a minimal set of axioms, engendered much work and writings from
1929 onwards, notably by Curry [6, 7], under the heading of combinatory logic.
Curiously, a very natural generalization of Schönfinkel’s structures, where
the application operation is not required to be always defined, was
axiomatically characterized only in 1975 by Feferman in the shape of the most
basic axioms of his theory $T_{0}$ of explicit mathematics [9]444In the
literature, this subtheory of $T_{0}$ has been christened $\mathrm{EON}$ (for
elementary theory of operations and numbers; see [5, p. 102]) and
$\mathrm{APP}$ (on account of comprising the applicative axioms of $T_{0}$;
see [29, Chapter 9, Section 5]). However, to be precise let us point out that
$T_{0}$ as formulated in [11] differs from the original formulation in [9]:
[11] has a primitive classification constant $\mathbb{N}$ for the natural
numbers as well as constants for successor and predecessor on $\mathbb{N}$,
and more crucially, equality is not assumed to be decidable and the
definition-by-cases operation is restricted to $\mathbb{N}$. and in [10, p.
70]. Feferman called these structures applicative structures.

######  Notation 2.1.

In order to introduce the notion of a pca, we shall start with that of a
partial operational structure $(M,\cdot)$, where $\cdot$ is just a partial
binary operation on $M$. We use $a\cdot b\simeq c$ to convey that $a\cdot b$
is defined and equal to $c$. $a\cdot b\downarrow$ stands for $\exists
c\,(a\cdot b\simeq c)$. In what follows, instead of $a\cdot b$ we will just
write $ab$. We also employ the association to the left convention, meaning
that e.g. $abc\simeq d$ stands for the following: there exists $e$ such that
$ab\simeq e$ and $ec\simeq d$.

######  Definition 2.2.

A partial combinatory algebra (pca) is a partial operational structure
$(A,\cdot)$ such that $A$ has at least two elements and there are elements
$\mathbf{k}$ and $\mathbf{s}$ in $A$ such that $\mathbf{k}a$, $\mathbf{s}a$
and $\mathbf{s}ab$ are always defined, and

  * •

$\mathbf{k}ab\simeq a$;

  * •

$\mathbf{s}abc\simeq ac(bc)$.

The combinators $k$ and $s$ are due to Schönfinkel [27] while the axiomatic
treatment, although formulated just in the total case, is due to Curry [7].
The word “combinatory” appears because of a property known as combinatory
completeness described next. For more information on pcas see [9, 11, 5, 35].

######  Definition 2.3.

Given a pca $A$, one can form application terms over $A$ by decreeing that:

  1. (i)

variables $x_{1},x_{2},\ldots$ and the constants $\mathbf{k}$ and $\mathbf{s}$
are applications terms over $A$;

  2. (ii)

elements of $A$ are application terms over $A$;

  3. (iii)

given application terms $s$ and $t$ over $A$, $(ts)$ is also an application
term over $A$.

Application terms over $A$ will also be called $A$-terms. Terms generated
solely by clauses (i)–(iii), will be called application terms.

An $A$-term $q$ without free variables has an obvious interpretation $q^{A}$
in $A$ by interpreting elements of $A$ by themselves and letting $(ts)^{A}$ be
$t^{A}\cdot s^{A}$ with $\cdot$ being the partial operation of $A$. Of course,
$q$ may fail to denote an element of $A$. We write $A\models q\downarrow$ (or
just $q\downarrow$) if it does, i.e., if $q^{A}$ yields an element of $A$.

The combinatory completeness of a pca $A$ is encapsulated in
$\lambda$-abstraction (see [9, p. 95], [11, p. 63], and [5, p. 101] for more
details).

######  Lemma 2.4 ($\lambda$-abstraction).

For every term $t$ with variables among the distinct variables
$x,x_{1},\ldots,x_{n}$, one can find in an effective way a new term $s$,
denoted $\lambda x.t$, such that

  * •

the variables of $s$ are the variables of $t$ except for $x$,

  * •

$s[a_{1}/x_{1},\ldots,a_{n}/x_{n}]\downarrow$ for all $a_{1},\ldots,a_{n}\in
A$,

  * •

$(s[a_{1}/x_{1},\ldots,a_{n}/x_{n}])a\simeq
t[a/x,a_{1}/x_{1},\ldots,a_{n}/x_{n}]$ for all $a,a_{1},\ldots,a_{n}\in A$.

The term $\lambda x.t$ is built solely with the aid of $\mathbf{k},\mathbf{s}$
and symbols occurring in $t$.

An immediate consequence of the foregoing abstraction lemma is the recursion
theorem for pca’s (see [9, p. 96], [11, p. 63], [5, p. 103]).

######  Lemma 2.5 (Recursion theorem).

There exists a closed application term $\mathbf{f}$ such that for every pca
$A$ and $a,b\in A$ we have $A\models{\mathbf{f}}\downarrow$ and

  * •

$A\models\mathbf{f}a\downarrow$;

  * •

$A\models\mathbf{f}ab\simeq a(\mathbf{f}a)b$.

###### Proof.

The heuristic approach consists in finding a fixed point of the form $cc$. Let
us search for $\mathbf{f}$ satisfying $\mathbf{f}a\simeq cc$, and hence find a
solution of the equation

$ccb\simeq a(cc)b.$

By using $\lambda$-abstraction, we can easily arrange to have, for every $d$,

$cdb\simeq a(dd)b.$

Indeed, let $\mathbf{f}:=\lambda a.cc$, where $c:=\lambda db.a(dd)b$. Then $f$
is as desired. ∎

In every pca, one has pairing and unpairing555Let $\mathbf{p}=\lambda
xyz.zxy$, $\mathbf{p_{0}}:=\lambda x.x\mathbf{k}$, and
$\mathbf{p_{1}}:=\lambda x.x\bar{\mathbf{k}}$, where
$\bar{\mathbf{k}}:=\lambda xy.y$. Projections $\mathbf{p_{0}}$ and
$\mathbf{p_{1}}$ need not be total. For realizability purposes, however, it is
not necessary to have total projections. combinators $\mathbf{p}$,
$\mathbf{p_{0}}$, and $\mathbf{p_{1}}$ such that:

  * •

$\mathbf{p}ab\downarrow$;

  * •

$\mathbf{p_{i}}(\mathbf{p}a_{0}a_{1})\simeq a_{i}$.

Generic realizability is based on partial combinatory algebras with some
additional structure (see however Remark 2.7).

######  Definition 2.6.

We say that $A$ is a pca over $\omega$ if there are extra 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$

$\displaystyle\operatorname{\mathbf{succ}}\bar{n}$
$\displaystyle\simeq\overline{n+1},$
$\displaystyle\operatorname{\mathbf{pred}}\overline{n+1}$
$\displaystyle\simeq\bar{n},$
$\mathbf{d}\bar{n}\bar{m}ab\simeq\begin{cases}a&n=m;\\\ b&n\neq m.\end{cases}$

One then defines $\mathbf{0}:=\bar{0}$ and $\mathbf{1}:=\bar{1}$.

The notion of a pca over $\omega$ coincides with the notion of $\omega$-pca+
in, e.g., [22].

Note that one can do without $\mathbf{k}$ by letting
$\mathbf{k}:=\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{n}ab\simeq\mathbf{d}\bar{n}\bar{m}ab\simeq b$
for all $a,b$. On the other hand, by our definition, every pca contains at
least two elements.

######  Remark 2.7.

The notion of a pca over $\omega$ is slightly impoverished one compared to
that of a model of Beeson’s theory $\mathbf{PCA}^{+}$ [5, VI.2] or Feferman’s
applicative structures [11]. However, for our purposes all the differences
between these structures are immaterial as every pca can be expanded to a
model of $\mathbf{PCA}^{+}$, which at the same time is also an applicative
structure (see [5, VI.2.9]).

By using, say, Curry numerals, one obtains a combinator $\mathbf{d}$ for this
representation of natural numbers. So, every pca can be turned into a pca over
$\omega$ by using Curry numerals. On the other hand, the notion of pca over
$\omega$ allows for other possible representations of natural numbers. Note
that the existence of a combinator $\mathbf{d}$ for a given representation of
natural numbers (together with a predecessor combinator), entails the
existence of a primitive recursion operator $\mathbf{r}$ for such
representation, that is, an element $\mathbf{r}$ such that:

$\displaystyle\mathbf{r}ab\bar{0}$ $\displaystyle\simeq a;$
$\displaystyle\mathbf{r}ab\overline{n+1}$ $\displaystyle\simeq
b(\mathbf{r}ab\bar{n})\bar{n}.$

##  3\. The theory ${\sf CZF}$

The logic of ${\sf CZF}$ (Constructive Zermelo-Fraenkel set theory) is
intuitionistic first order logic with equality. The only nonlogical symbol is
$\in$ as in classical Zermelo-Fraenkel set theory $\sf ZF$.

Axioms

1\. Extensionality: $\forall x\,\forall y\,(\forall z\,(z\in x\leftrightarrow
z\in y)\rightarrow x=y)$,

2\. Pairing: $\forall x\,\forall y\,\exists z\,(x\in z\land y\in z)$,

3\. Union: $\forall x\,\exists y\,\forall u\,\forall z\,(u\in z\land z\in
x\rightarrow u\in y)$,

4\. Infinity: $\exists x\,\forall y\,(y\in x\leftrightarrow y=0\lor\exists
z\in x\,(y=z\cup\\{z\\}))$,

5\. Set induction: $\forall x\,(\forall y\in
x\,\varphi(y)\rightarrow\varphi(x))\rightarrow\forall x\,\varphi(x)$, for all
formulae $\varphi$,

6\. Bounded separation: $\forall x\,\exists y\,\forall z\,(z\in
y\leftrightarrow z\in x\land\varphi(z))$, for $\varphi$ bounded, where a
formula is bounded if all quantifiers appear in the form $\forall x\in y$ and
$\exists x\in y$,

7\. Strong collection: $\forall u\in x\,\exists
v\,\varphi(u,v)\rightarrow\exists y\,(\forall u\in x\,\exists v\in
y\,\varphi(u,v)\land\forall v\in y\,\exists u\in x\,\varphi(u,v))$, for all
formulae $\varphi$,

8\. Subset collection: $\forall x\,\forall y\,\exists z\,\forall p\,(\forall
u\in x\,\exists v\in y\,\varphi(u,v,p)\rightarrow\exists q\in z\,(\forall u\in
x\,\exists v\in q\,\varphi(u,v,p)\land\forall v\in q\,\exists u\in
x\,\varphi(u,v,p)))$, for all formulae $\varphi$.

######  Notation 3.1.

Let $x=0$ be $\forall y\in x\,\neg(y=y)$ and $x=y\cup\\{y\\}$ be $\forall z\in
x\,(z\in y\lor z=y)\land\forall z\in y\,(z\in x)\land y\in x$.

##  4\. Finite types and axiom of choice

Finite types $\sigma$ and their associated extensions $F_{\sigma}$ are defined
by the following clauses:

  * •

$o\in{\sf FT}$ and $F_{o}=\omega$;

  * •

if $\sigma,\tau\in{\sf FT}$, then $(\sigma)\tau\in{\sf FT}$ and

$F_{(\sigma)\tau}=F_{\sigma}\to F_{\tau}=\\{\text{total functions from
$F_{\sigma}$ to $F_{\tau}$}\\}.$

For brevity we write $\sigma\tau$ for $(\sigma)\tau$, if the type $\sigma$ is
written as a single symbol. We say that $x\in F_{\sigma}$ has type $\sigma$.

The set ${\sf FT}$ of all finite types, the set
$\\{F_{\sigma}\colon\sigma\in{\sf FT}\\}$, and the set
$\mathbb{F}=\bigcup_{\sigma\in{\sf FT}}F_{\sigma}$ all exist in ${\sf CZF}$.

######  Definition 4.1 (Axiom of choice in all finite types).

The schema ${\sf AC}_{{\sf FT}}$ consists of formulae

$\forall x^{\sigma}\,\exists y^{\tau}\,\varphi(x,y)\rightarrow\exists
f^{\sigma\tau}\,\forall x^{\sigma}\,\varphi(x,f(x)),$

where $\sigma$ and $\tau$ are (standard) finite types.

######  Notation 4.2.

We write $\forall x^{\sigma}\,\varphi(x)$ and $\exists x^{\sigma}\,\varphi(x)$
as a shorthand for $\forall x\,(x\in F_{\sigma}\rightarrow\varphi(x))$ and
$\exists x\,(x\in F_{\sigma}\land\varphi(x))$ respectively.

##  5\. Defining extensional realizability in ${\sf CZF}$

In ${\sf CZF}$, given a pca $A$ over $\omega$, we inductively define a class
$\mathrm{V_{ex}}(A)$ such that

$\forall x\,(x\in\mathrm{V_{ex}}(A)\leftrightarrow x\subseteq A\times
A\times\mathrm{V_{ex}}(A)).$

The intuition for $\langle{a,b,y}\rangle\in x$ is that $a$ and $b$ are _equal
realizers_ of the fact that $y^{A}\in x^{A}$, where
$x^{A}=\\{y^{A}\colon\langle{a,b,y}\rangle\in x\text{ for some }a,b\in A\\}$.

General information on how to handle inductive definitions in ${\sf CZF}$ can
be found in [1, 2, 3]. The inductive definition of $\mathrm{V_{ex}}(A)$ within
${\sf CZF}$ is on par with that of $\mathrm{V}(A)$, the specifics of which
appear in [25, 3.4].

######  Notation 5.1.

We use $(a)_{i}$ or simply $a_{i}$ for $\mathbf{p_{i}}a$. Whenever we write an
application term $t$, we assume that it is defined. In other words, a formula
$\varphi(t)$ stands for $\exists a\,(t\simeq a\land\varphi(a))$.

######  Definition 5.2 (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_{ex}}(A)$. The atomic
cases fall under the scope of definitions by transfinite recursion.

$\displaystyle a=b$ $\displaystyle\Vdash x\in y$
$\displaystyle\Leftrightarrow$ $\displaystyle\exists
z\,(\langle(a)_{0},(b)_{0},z\rangle\in y\land(a)_{1}=(b)_{1}\Vdash x=z)$
$\displaystyle a=b$ $\displaystyle\Vdash x=y$ $\displaystyle\Leftrightarrow$
$\displaystyle\forall\langle c,d,z\rangle\in x\,((ac)_{0}=(bd)_{0}\Vdash z\in
y)\text{ and }$ $\displaystyle\forall\langle c,d,z\rangle\in
y\,((ac)_{1}=(bd)_{1}\Vdash z\in x)$ $\displaystyle a=b$
$\displaystyle\Vdash\varphi\land\psi$ $\displaystyle\Leftrightarrow$
$\displaystyle(a)_{0}=(b)_{0}\Vdash\varphi\land(a)_{1}=(b)_{1}\Vdash\psi$
$\displaystyle a=b$ $\displaystyle\Vdash\varphi\lor\psi$
$\displaystyle\Leftrightarrow$
$\displaystyle(a)_{0}\simeq(b)_{0}\simeq\mathbf{0}\land(a)_{1}=(b)_{1}\Vdash\varphi\text{
or }$
$\displaystyle(a)_{0}\simeq(b)_{0}\simeq\mathbf{1}\land(a)_{1}=(b)_{1}\Vdash\psi$
$\displaystyle a=b$ $\displaystyle\Vdash\neg\varphi$
$\displaystyle\Leftrightarrow$ $\displaystyle\forall
c,d\,\neg(c=d\Vdash\varphi)$ $\displaystyle a=b$
$\displaystyle\Vdash\varphi\rightarrow\psi$ $\displaystyle\Leftrightarrow$
$\displaystyle\forall c,d\,(c=d\Vdash\varphi\rightarrow ac=bd\Vdash\psi)$
$\displaystyle a=b$ $\displaystyle\Vdash\forall x\in y\,\varphi$
$\displaystyle\Leftrightarrow$ $\displaystyle\forall\langle c,d,x\rangle\in
y\,(ac=bd\Vdash\varphi)$ $\displaystyle a=b$ $\displaystyle\Vdash\exists x\in
y\,\varphi$ $\displaystyle\Leftrightarrow$ $\displaystyle\exists
x\,(\langle(a)_{0},(b)_{0},x\rangle\in y\land(a)_{1}=(b)_{1}\Vdash\varphi)$
$\displaystyle a=b$ $\displaystyle\Vdash\forall x\,\varphi$
$\displaystyle\Leftrightarrow$ $\displaystyle\forall
x\in\mathrm{V_{ex}}(A)\,(a=b\Vdash\varphi)$ $\displaystyle a=b$
$\displaystyle\Vdash\exists x\,\varphi$ $\displaystyle\Leftrightarrow$
$\displaystyle\exists x\in\mathrm{V_{ex}}(A)\,(a=b\Vdash\varphi)$

######  Notation 5.3.

We write $a\Vdash\varphi$ for $a=a\Vdash\varphi$.

The above definition builds on the variant [25] of generic realizability [19],
where bounded quantifiers are treated as quantifiers in their own right. Note
that in the language of ${\sf CZF}$, bounded quantifiers can be seen as
syntactic sugar by letting $\forall x\in y\,\varphi:=\forall x\,(x\in
y\rightarrow\varphi)$ and $\exists x\in y\,\varphi:=\exists x\,(x\in
y\land\varphi)$. Nothing gets lost in translation, thanks to the following.

######  Lemma 5.4.

There are closed application terms $\mathbf{u}$ and $\mathbf{v}$ such that
${\sf CZF}$ proves

$\mathbf{u}\Vdash\forall x\in y\,\varphi\leftrightarrow\forall x\,(x\in
y\rightarrow\varphi),$ $\mathbf{v}\Vdash\exists x\in
y\,\varphi\leftrightarrow\exists x\,(x\in y\land\varphi).$

The advantage of having special clauses for bounded quantifiers is that it
simplifies a great deal the construction of realizers.

######  Remark 5.5.

In the context of (finite type) arithmetic, extensional notions of
realizability typically give rise to a partial equivalence relation. Namely,
for every formula $\varphi$, the relation $\\{(a,b)\in A^{2}\colon
a=b\Vdash\varphi\\}$ is symmetric and transitive. This is usually seen by
induction on $\varphi$, the atomic case being trivial. The situation, though,
is somewhat different in set theory. Say that $a=b\Vdash x\in y$ and
$b=c\Vdash x\in y$. All we know is that for some $u,v\in\mathrm{V_{ex}}(A)$ we
have that
$\langle{(a)_{0},(b)_{0},u}\rangle,\langle{(b)_{0},(c)_{0},v}\rangle\in y$,
$(a)_{1}=(b)_{1}\Vdash x=u$, and $(b)_{1}=(c)_{1}\Vdash x=v$. Since $u$ and
$v$ need not be the same set, even if elements of $\mathrm{V_{ex}}(A)$ behave
as expected, that is, $\\{(a,b)\colon\langle{a,b,y}\rangle\in x\\}$ is
symmetric and transitive for any given $x,y\in\mathrm{V_{ex}}(A)$,666One could
inductively define $\mathrm{V_{ex}}(A)$ so as to make $\\{(a,b)\in
A^{2}\colon\langle{a,b,y}\rangle\in x\\}$ symmetric and transitive. Just let
$x\in\mathrm{V_{ex}}(A)$ if and only if  • $x$ consists of triples
$\langle{a,b,y}\rangle$ with $y\in\mathrm{V_{ex}}(A)$; • whenever
$\langle{a,b,y}\rangle\in x$, $\langle{b,a,y}\rangle\in x$; • whenever
$\langle{a,b,y}\rangle\in x$ and $\langle{b,c,y}\rangle\in x$, also
$\langle{a,c,y}\rangle\in x$. we cannot conclude that $a=c\Vdash x\in y$. So,
transitivity can fail.

As it turns out, for our purposes, this is not an issue at all. Note however
that the canonical names for objects of finite type do indeed behave as
desired and so does the relation $a=b\Vdash\varphi$ for formulas of finite
type arithmetic. This is in fact key in validating the axiom of choice in all
finite types (Section 8). Except for this deviation, the clauses for
connectives and quantifiers follow the general blueprint of extensional
realizability. We just feel justified in keeping the notation
$a=b\Vdash\varphi$.

##  6\. Soundness for intuitionistic first order logic with equality

From now on, let $A$ be a pca over $\omega$ within ${\sf CZF}$. Realizability
of the equality axioms relies on the following fact about pca’s.

######  Lemma 6.1 (Double recursion theorem).

There are combinators $\mathbf{g}$ and $\mathbf{h}$ such that, for all
$a,b,c\in A$:

  * •

$\mathbf{g}ab\downarrow$ and $\mathbf{h}ab\downarrow$;

  * •

$\mathbf{g}abc\simeq a(\mathbf{h}ab)c$;

  * •

$\mathbf{h}abc\simeq b(\mathbf{g}ab)c$.

###### Proof.

Let $t(a,b):=\lambda xc.a(\lambda c.bxc)c$. Set $\mathbf{g}:=\lambda
ab.\mathbf{f}t(a,b)$, where $\mathbf{f}$ is the fixed point operator from the
recursion theorem. Set $\mathbf{h}:=\lambda abc.b(\mathbf{f}t(a,b))c$. Verify
that $\mathbf{g}$ and $\mathbf{h}$ are as desired. ∎

######  Lemma 6.2.

There are closed application terms $\mathbf{i_{r}}$, $\mathbf{i_{s}}$,
$\mathbf{i_{t}}$, $\mathbf{i_{0}}$ and $\mathbf{i_{1}}$ such that ${\sf CZF}$
proves, for all $x,y,z\in\mathrm{V_{ex}}(A)$,

  1. $(1)$

$\mathbf{i_{r}}\Vdash x=x$;

  2. $(2)$

$\mathbf{i_{s}}\Vdash x=y\rightarrow y=x$;

  3. $(3)$

$\mathbf{i_{t}}\Vdash x=y\land y=z\rightarrow x=z$;

  4. $(4)$

$\mathbf{i_{0}}\Vdash x=y\land y\in z\rightarrow x\in z$;

  5. $(5)$

$\mathbf{i_{1}}\Vdash x=y\land z\in x\rightarrow z\in y$.

######  Notation 6.3.

Write, say, $a_{ij}$ for $\mathbf{p_{j}}(\mathbf{p_{i}}a)$.

###### Proof.

(1) By the recursion theorem in $A$, we can find $\mathbf{i_{r}}$ such that

$\mathbf{i_{r}}a\simeq\mathbf{p}(\mathbf{p}a\mathbf{i_{r}})(\mathbf{p}a\mathbf{i_{r}}).$

By set induction, we show that $\mathbf{i_{r}}\Vdash x=x$ for every
$x\in\mathrm{V_{ex}}(A)$. Let $\langle{a,b,y}\rangle\in x$. We want
$(\mathbf{i_{r}}a)_{0}=(\mathbf{i_{r}}b)_{0}\Vdash y\in x$. Now
$(\mathbf{i_{r}}a)_{00}\simeq a$ and similarly for $b$. On the other hand,
$(\mathbf{i_{r}}a)_{01}\simeq(\mathbf{i_{r}}b)_{01}\simeq\mathbf{i_{r}}$. By
induction, $\mathbf{i_{r}}\Vdash y=y$, and so we are done. Similarly for
$(\mathbf{i_{r}}a)_{1}=(\mathbf{i_{r}}b)_{1}\Vdash y\in x$.

(2) We just need to interchange. Let

$\mathbf{i_{s}}:=\lambda ac.\mathbf{p}(ac)_{1}(ac)_{0}.$

Suppose $a=b\Vdash x=y$. We want $\mathbf{i_{s}}a=\mathbf{i_{s}}b\Vdash y=x$.
Let $\langle{c,d,z}\rangle\in y$. By definition, $(ac)_{1}=(bd)_{1}\Vdash z\in
x$. Now $(ac)_{1}\simeq(\mathbf{i_{s}}ac)_{0}$, and similarly
$(bd)_{1}\simeq(\mathbf{i_{s}}bd)_{0}$. Then we are done. Similarly for the
other direction.

(3,4) Combinators $\mathbf{i_{t}}$ and $\mathbf{i_{0}}$ are defined by a
double recursion in $A$. By induction on triples $\langle{x,y,z}\rangle$, one
then shows that $\mathbf{i_{t}}\Vdash x=y\land y=z\rightarrow x=z$ and
$\mathbf{i_{0}}\Vdash x=y\land y\in z\rightarrow x\in z$. Eventually,
$\mathbf{i_{t}}$ and $\mathbf{i_{r}}$ are solutions of equations of the form

$\displaystyle\mathbf{i_{t}}a$ $\displaystyle\simeq\mathbf{t}\mathbf{i_{0}}a,$
$\displaystyle\mathbf{i_{0}}a$ $\displaystyle\simeq\mathbf{r}\mathbf{i_{t}}a,$

where $\mathbf{t}$ and $\mathbf{r}$ are given closed application terms. These
are given by the fixed point operators from the double recursion theorem.

(5) Set

$\mathbf{i_{1}}:=\lambda
a.\mathbf{p}(a_{0}a_{10})_{00}(\mathbf{i_{t}}(\mathbf{p}a_{11}(a_{0}a_{10})_{01})).$

∎

######  Theorem 6.4.

For every formula $\varphi(x_{1},\ldots,x_{n})$ provable in intuitionistic
first order logic with equality, there exists a closed application term
$\mathbf{e}$ such that ${\sf CZF}$ proves $\mathbf{e}\Vdash\forall
x_{1}\cdots\forall x_{n}\,\varphi(x_{1},\ldots,x_{n})$.

###### Proof.

The proof is similar to [19, 5.3] and [25, 4.3]. ∎

##  7\. Soundness for ${\sf CZF}$

We start with a lemma concerning bounded separation.

######  Lemma 7.1 (${\sf CZF}$).

Let $\varphi(u)$ be a bounded formula with parameters from
$\mathrm{V_{ex}}(A)$ and $x\subseteq\mathrm{V_{ex}}(A)$. Then

$\\{\langle{a,b,u}\rangle\colon a,b\in A\land u\in x\land
a=b\Vdash\varphi(u)\\}$

is a set.

###### Proof.

As in [25, Lemma 4.5, Lemma 4.6, Corollary 4.7]. ∎

######  Theorem 7.2.

For every theorem $\varphi$ of ${\sf CZF}$, there is a closed application term
$\mathbf{e}$ such that ${\sf CZF}$ proves $\mathbf{e}\Vdash\varphi$.

###### Proof.

In view of Theorem 6.4, it is sufficient to show that every axiom of ${\sf
CZF}$ has a realizer. The proof is similar to that of [25, Theorem 5.1]. The
rationale is simple: use the same realizers, duplicate the names. Remember
that $\mathbf{e}\Vdash\varphi$ means $\mathbf{e}=\mathbf{e}\Vdash\varphi$.

Extensionality. Let $x,y\in\mathrm{V_{ex}}(A)$. Suppose $a=b\Vdash z\in
x\leftrightarrow z\in y$ for all $z\in\mathrm{V_{ex}}(A)$. We look for
$\mathbf{e}$ such that $\mathbf{e}a=\mathbf{e}b\Vdash x=y$. Set

$\mathbf{e}:=\lambda
ac.\mathbf{p}(a_{0}(\mathbf{p}c\mathbf{i_{r}}))(a_{1}(\mathbf{p}c\mathbf{i_{r}})).$

Suppose $\langle{c,d,z}\rangle\in x$. Then
$\mathbf{p}c\mathbf{i_{r}}=\mathbf{p}d\mathbf{i_{r}}\Vdash z\in x$, since
$\mathbf{i_{r}}\Vdash z=z$. Then
$a_{0}(\mathbf{p}c\mathbf{i_{r}})=b_{0}(\mathbf{p}d\mathbf{i_{r}})\Vdash z\in
y$. Therefore, $(\mathbf{e}ac)_{0}=(\mathbf{e}bd)_{0}\Vdash z\in y$, as
desired. The other direction is similar.

Pairing. Find $\mathbf{e}$ such that for all $x,y\in\mathrm{V_{ex}}(A)$,

$\mathbf{e}\Vdash x\in z\land y\in z,$

for some $z\in\mathrm{V_{ex}}(A)$. Let $x,y\in\mathrm{V_{ex}}(A)$ be given.
Define
$z=\\{\langle{\mathbf{0},\mathbf{0},x}\rangle,\langle{\mathbf{0},\mathbf{0},y}\rangle\\}$.
Let

$\mathbf{e}=\mathbf{p}(\mathbf{p}\mathbf{0}\mathbf{i_{r}})(\mathbf{p}\mathbf{0}\mathbf{i_{r}}).$

Union. Find $\mathbf{e}$ such that for all $x\in\mathrm{V_{ex}}(A)$,

$\mathbf{e}\Vdash\forall u\in x\,\forall v\in u\,(v\in y),$

for some $y\in\mathrm{V_{ex}}(A)$. Given $x\in\mathrm{V_{ex}}(A)$, let
$y=\\{\langle{c,d,v}\rangle\colon\exists\langle{a,b,u}\rangle\in
x\,(\langle{c,d,v}\rangle\in u)\\}$. Set $\mathbf{e}:=\lambda
ac.\mathbf{p}c\mathbf{i_{r}}$.

Infinity. Let $\dot{\omega}=\\{\langle{\bar{n},\bar{n},\dot{n}}\rangle\colon
n\in\omega\\}$, where
$\dot{n}=\\{\langle{\bar{m},\bar{m},\dot{m}}\rangle\colon m<n\\}$. Let us find
$\mathbf{e}$ such that for all $y\in\mathrm{V_{ex}}(A)$,

$\mathbf{e}\Vdash y\in\dot{\omega}\leftrightarrow y=0\lor\exists
z\in\dot{\omega}\,(y=z\cup\\{z\\}).$

Recall that $y=0$ stands for $\forall x\in y\,\neg(x=x)$ and $y=z\cup\\{z\\}$
stands for $\forall x\in y\,(x\in z\lor x=z)\land(\forall x\in z\,(x\in
y)\land z\in y)$.

Let $\vartheta(y):=y=0\lor\exists z\in\dot{\omega}\,(y=z\cup\\{z\\})$. We want
$\mathbf{e}$ such that for every $y\in\mathrm{V_{ex}}(A)$

$\mathbf{e}_{0}\Vdash y\in\dot{\omega}\rightarrow\vartheta(y),$
$\mathbf{e}_{1}\Vdash\vartheta(y)\rightarrow y\in\dot{\omega}.$

Let us first consider (1). Suppose $a=b\Vdash y\in\dot{\omega}$. We want
$\mathbf{e}_{0}a=\mathbf{e}_{0}b\Vdash\vartheta(y)$.

By definition, there is $n\in\omega$ such that $a_{0}\simeq
b_{0}\simeq\bar{n}$ and $a_{1}=b_{1}\Vdash y=\dot{n}$.

Case $n=0$. Then $\mathbf{0}\Vdash y=0$, and so
$\mathbf{p}\mathbf{0}\mathbf{0}\Vdash\vartheta(y)$.

Case $n>0$. We have
$\operatorname{\mathbf{pred}}a_{0}\simeq\operatorname{\mathbf{pred}}b_{0}\simeq\bar{m}$
with $n=m+1$. We aim for a term $t(x)$ such that $t(a)=t(b)\Vdash\exists
z\in\dot{\omega}\,(y=z\cup\\{z\\})$ by requiring

$t(a)_{0}\simeq t(b)_{0}\simeq\bar{m},$ $t(a)_{1}=t(b)_{1}\Vdash
y=\dot{m}\cup\\{\dot{m}\\}.$

If we succeed, then

$\mathbf{p}\mathbf{1}t(a)=\mathbf{p}\mathbf{1}t(b)\Vdash\vartheta(y).$

Now, (3) amounts to

$\displaystyle t(a)_{10}=t(b)_{10}$ $\displaystyle\Vdash\forall x\in
y\,(x\in\dot{m}\lor x=\dot{m})$ (4) $\displaystyle t(a)_{110}=t(b)_{110}$
$\displaystyle\Vdash\forall x\in\dot{m}\,(x\in y)$ (5) $\displaystyle
t(a)_{111}=t(b)_{111}$ $\displaystyle\Vdash\dot{m}\in y$ (6)

Part (4). Let $\langle{c,d,x}\rangle\in y$. Then
$(a_{1}c)_{0}=(b_{1}d)_{0}\Vdash x\in\dot{n}$, that is,

$\langle{(a_{1}c)_{00},(b_{1}d)_{00},\dot{k}}\rangle\in\dot{n},$
$(a_{1}c)_{01}=(b_{1}d)_{01}\Vdash x=\dot{k},$

where $(a_{1}c)_{00}\simeq(b_{1}d)_{00}\simeq\bar{k}$. Here we have two more
cases. If $k=m$, then

$\mathbf{p}\mathbf{1}(a_{1}c)_{01}=\mathbf{p}\mathbf{1}(b_{1}d)_{01}\Vdash
x\in\dot{m}\lor x=\dot{m}.$

If $k<m$, then $\langle{\bar{k},\bar{k},\dot{k}}\rangle\in\dot{m}$ and
$\mathbf{p}\bar{k}(a_{1}c)_{01}=\mathbf{p}\bar{k}(b_{1}d)_{01}\Vdash
x\in\dot{m}$, so that

$\mathbf{p}\mathbf{0}(\mathbf{p}\bar{k}(a_{1}c)_{01})=\mathbf{p}\mathbf{0}(\mathbf{p}\bar{k}(b_{1}d)_{01})\Vdash
x\in\dot{m}\lor x=\dot{m}.$

Then $t(a)$ such that

$t(a)_{10}\simeq\lambda
c.\mathbf{d}(a_{1}c)_{00}(\operatorname{\mathbf{pred}}a_{0})(\mathbf{p}\mathbf{1}(a_{1}c)_{01})(\mathbf{p}\mathbf{0}(a_{1}c)_{0})$

is as desired.

Parts (5) and (6). Let $t(a)$ satisfy

$t(a)_{110}\simeq\lambda x.(a_{1}x)_{1},$
$t(a)_{111}\simeq(a_{1}(\operatorname{\mathbf{pred}}a_{0}))_{1}.$

We want $\mathbf{e}$ such that

$\mathbf{e}_{0}\simeq\lambda
a.\mathbf{d}\mathbf{0}a_{0}(\mathbf{p}\mathbf{0}\mathbf{0})(\mathbf{p}\mathbf{1}t(a)).$

Then $\mathbf{e}_{0}$ does the job.

As for (2), suppose $a=b\Vdash\vartheta(y)$. We want
$\mathbf{e}_{1}a=\mathbf{e}_{1}b\Vdash y\in\dot{\omega}$. By unravelling the
definitions, we obtain two cases.

(i) $a_{0}\simeq b_{0}\simeq\mathbf{0}$ and $a_{1}=b_{1}\Vdash y=0$. It
follows that $y=\dot{0}$ and so $\mathbf{i_{r}}\Vdash y=\dot{0}$. Therefore
$\mathbf{p}a_{0}\mathbf{i_{r}}=\mathbf{p}b_{0}\mathbf{i_{r}}\Vdash
y\in\dot{\omega}$, as
$\langle{\mathbf{0},\mathbf{0},\dot{0}}\rangle\in\dot{\omega}$.

(ii) $a_{0}\simeq b_{0}\simeq\mathbf{1}$ and $a_{1}=b_{1}\Vdash\exists
z\in\dot{\omega}\,(y=z\cup\\{z\\})$ Then there exists $m\in\omega$ such that
$a_{10}\simeq b_{10}\simeq\bar{m}$ and

$a_{11}=b_{11}\Vdash y=\dot{m}\cup\\{\dot{m}\\}.$

We aim for a term $s(x)$ such that $s(a)=s(b)\Vdash y=\dot{n}$, where $n=m+1$.
If we succeed, then

$\mathbf{p}(\operatorname{\mathbf{succ}}a_{10})s(a)=\mathbf{p}(\operatorname{\mathbf{succ}}b_{10})s(b)\Vdash
y\in\dot{\omega}.$

Note in fact that
$\operatorname{\mathbf{succ}}a_{10}\simeq\operatorname{\mathbf{succ}}b_{10}\simeq\bar{n}$.

For the left to right inclusion, suppose $\langle{c,d,x}\rangle\in y$. Our
goal is $(s(a)c)_{0}=(s(b)d)_{0}\Vdash x\in\dot{n}$. It follows from (7) that

$a_{110}=b_{110}\Vdash\forall x\in y\,(x\in\dot{m}\lor x=\dot{m}),$

and therefore

$a_{110}c=b_{110}d\Vdash x\in\dot{m}\lor x=\dot{m}.$

¿From (8) we get two more cases. First case:
$(a_{110}c)_{0}\simeq(b_{110}d)_{0}\simeq\mathbf{0}$ and
$(a_{110}c)_{1}=(b_{110}d)_{1}\Vdash x\in\dot{m}$. Then one can verify that

$(a_{110}c)_{1}=(b_{110}d)_{1}\Vdash x\in\dot{n}.$

Second case: $(a_{110}c)_{0}\simeq(b_{110}d)_{0}\simeq\mathbf{1}$ and
$(a_{110}c)_{1}=(b_{110}d)_{1}\Vdash x=\dot{m}$. Then

$\mathbf{p}\bar{m}(a_{110}c)_{1}=\mathbf{p}\bar{m}(b_{110}d)_{1}\Vdash
x\in\dot{n}.$

Let $s(x)$ be such that

$(s(a)c)_{0}\simeq\mathbf{d}\mathbf{0}(a_{110}c)_{0}(a_{110}c)_{1}(\mathbf{p}a_{10}(a_{110}c)_{1}).$

For the right to left inclusion, suppose $k<n$. Our goal is
$(s(a)\bar{k})_{1}=(s(b)\bar{k})_{1}\Vdash\dot{k}\in y$. It follows from (7)
that

$\displaystyle a_{1110}=b_{1110}$ $\displaystyle\Vdash\forall
x\in\dot{m}\,(x\in y),$ (9) $\displaystyle a_{1111}=b_{1111}$
$\displaystyle\Vdash\dot{m}\in y.$ (10)

If $k<m$, then $\langle{\bar{k},\bar{k},\dot{k}}\rangle\in\dot{m}$, and hence
$a_{1110}\bar{k}=b_{1110}\bar{k}\Vdash\dot{k}\in y$ by (9). On the other hand,
if $k=m$ then (10) gives us the realizers. Therefore let $s(x)$ be such that

$(s(a)\bar{k})_{1}\simeq\mathbf{d}\bar{k}a_{10}a_{1111}(a_{1110}\bar{k}).$

We thus want $\mathbf{e}$ such that

$\mathbf{e}_{1}\simeq\lambda
a.\mathbf{d}\mathbf{0}a_{0}(\mathbf{p}a_{0}\mathbf{i_{r}})(\mathbf{p}(\operatorname{\mathbf{succ}}a_{10})s(a)).$

Then $\mathbf{e}_{1}$ does the job.

Set induction. By the recursion theorem, let $\mathbf{e}$ be such that
$\mathbf{e}a\simeq a(\lambda c.\mathbf{e}a)$. Prove that

$\mathbf{e}\Vdash\forall x\,(\forall y\in
x\,\varphi(y)\rightarrow\varphi(x))\rightarrow\forall x\,\varphi(x).$

Let $a=b\Vdash\forall x\,(\forall y\in x\,\varphi(y)\rightarrow\varphi(x))$.
By definition, $a=b\Vdash\forall y\in x\,\varphi(y)\rightarrow\varphi(x)$ for
every $x\in\mathrm{V_{ex}}(A)$. By set induction, we show that
$\mathbf{e}a=\mathbf{e}b\Vdash\varphi(x)$ for every $x\in\mathrm{V_{ex}}(A)$.
Assume by induction that $\mathbf{e}a=\mathbf{e}b\Vdash\varphi(y)$ for every
$\langle{c,d,y}\rangle\in x$. This means that $\lambda c.\mathbf{e}a=\lambda
d.\mathbf{e}b\Vdash\forall y\in x\,\varphi(y)$. Then $a(\lambda
c.\mathbf{e}a)=b(\lambda d.\mathbf{e}b)\Vdash\varphi(x)$. The conclusion
$\mathbf{e}a=\mathbf{e}b\Vdash\varphi(x)$ follows.

Bounded separation. Find $\mathbf{e}$ such that for all
$x\in\mathrm{V_{ex}}(A)$,

$\mathbf{e}\Vdash\forall u\in y\,(u\in x\land\varphi(u))\land\forall u\in
x\,(\varphi(u)\rightarrow u\in y),$

for some $y\in\mathrm{V_{ex}}(A)$. Given $x\in\mathrm{V_{ex}}(A)$, let

$y=\\{\langle{\mathbf{p}ac,\mathbf{p}bd,u}\rangle\colon\langle{a,b,u}\rangle\in
x\land c=d\Vdash\varphi(u)\\}.$

It follows from Lemma 7.1 that $y$ is a set. Moreover, $y$ belongs to
$\mathrm{V_{ex}}(A)$. We want $\mathbf{e}$ such that

$\displaystyle\mathbf{e}_{0}$ $\displaystyle\Vdash\forall u\in y\,(u\in
x\land\varphi(u)),$ $\displaystyle\mathbf{e}_{1}$ $\displaystyle\Vdash\forall
u\in x\,(\varphi(u)\rightarrow u\in y).$

By letting $\mathbf{e}=\mathbf{p}e_{0}e_{1}$, where

$\displaystyle e_{0}$ $\displaystyle:=\lambda
f.\mathbf{p}(\mathbf{p}f_{0}\mathbf{i_{r}})f_{1},$ $\displaystyle e_{1}$
$\displaystyle:=\lambda ac.\mathbf{p}(\mathbf{p}ac)\mathbf{i_{r}},$

one verifies that $\mathbf{e}$ is as desired.

Strong Collection. Set $\mathbf{e}:=\lambda a.\mathbf{p}(\lambda
c.\mathbf{p}c(ac))(\lambda c.\mathbf{p}c(ac))$. Let $a=b\Vdash\forall u\in
x\,\exists v\,\varphi(u,v)$. By strong collection, we can find a set $y$ such
that

  * •

$\forall\langle{c,d,u}\rangle\in x\,\exists
v\in\mathrm{V_{ex}}(A)\,(\langle{c,d,v}\rangle\in y\land
ac=bd\Vdash\varphi(u,v))$, and

  * •

$\forall z\in y\,\exists\langle{c,d,u}\rangle\in x\,\exists
v\in\mathrm{V_{ex}}(A)\,(z=\langle{c,d,v}\rangle\land
ac=bd\Vdash\varphi(u,v))$.

In particular, $y\in\mathrm{V_{ex}}(A)$. Show that

$\mathbf{e}a=\mathbf{e}b\Vdash\forall u\in x\,\exists v\in
y\,\varphi(u,v)\land\forall v\in y\exists u\in x\,\varphi(u,v).$

Subset collection. We look for $\mathbf{e}$ such that for all
$x,y\in\mathrm{V_{ex}}(A)$ there is a $z\in\mathrm{V_{ex}}(A)$ such that for
all $p\in\mathrm{V_{ex}}(A)$

$\mathbf{e}\Vdash\forall u\in x\,\exists v\in
y\,\varphi(u,v,p)\rightarrow\exists q\in z\,\psi(x,q,p),$

where

$\psi(x,q,p):=\forall u\in x\,\exists v\in q\,\varphi(u,v,p)\land\forall v\in
q\,\exists u\in x\,\varphi(u,v,p).$

Form the set $y^{\prime}=\\{\langle{f,g,v}\rangle\colon f,g\in A\land\exists
i,j\in A\,\langle{i,j,v}\rangle\in y\\}$. By subset collection, we can find a
set $z^{\prime}$ such that for all $a,b,p$, if

$\forall\langle{c,d,u}\rangle\in
x\,\exists\langle{\mathbf{p}ac,\mathbf{p}bd,v}\rangle\in
y^{\prime}\,(ac)_{1}=(bd)_{1}\Vdash\varphi(u,v,p),$

then there is a $q\in z^{\prime}$ such that

$\forall\langle{c,d,u}\rangle\in x\,\exists w\in q\,\vartheta\land\forall w\in
q\,\exists\langle{c,d,u}\rangle\in x\,\vartheta,$

where $\vartheta=\vartheta(c,d,u,w;a,b,p)$ is

$\exists
v\,(w=\langle{\mathbf{p}ac,\mathbf{p}bd,v}\rangle\land(ac)_{1}=(bd)_{1}\Vdash\varphi(u,v,p)).$

Note that the $q\in z^{\prime}$ asserted to exist is a subset of $y^{\prime}$
and so $q\in\mathrm{V_{ex}}(A)$. On the other hand, there might be $q\in
z^{\prime}$ that are not in $\mathrm{V_{ex}}(A)$, and hence $z^{\prime}$ need
not be a subset of $\mathrm{V_{ex}}(A)$. Let $z^{\prime\prime}=\\{q\cap
y^{\prime}\colon q\in z^{\prime}\\}$. Now,
$z^{\prime\prime}\subseteq\mathrm{V_{ex}}(A)$. Finally, set

$z=\\{\langle{\mathbf{0},\mathbf{0},q}\rangle\colon q\in z^{\prime\prime}\\}.$

Then $z\in\mathrm{V_{ex}}(A)$. It remains to find $\mathbf{e}$. Let
$p\in\mathrm{V_{ex}}(A)$ and suppose

$a=b\Vdash\forall u\in x\,\exists v\in y\,\varphi(u,v,p).$

We would like to have

$\mathbf{e}a=\mathbf{e}b\Vdash\exists q\in z\,\psi(x,q,p).$

By definition of $z$, we let $(\mathbf{e}a)_{0}\simeq\mathbf{0}$ and we look
for a $q\in z^{\prime\prime}$ such that
$(\mathbf{e}a)_{1}=(\mathbf{e}b)_{1}\Vdash\psi(x,q,p)$, that is,

$\displaystyle(\mathbf{e}a)_{10}=(\mathbf{e}b)_{10}$
$\displaystyle\Vdash\forall u\in x\,\exists v\in q\,\varphi(u,v,p),$
$\displaystyle(\mathbf{e}a)_{11}=(\mathbf{e}b)_{11}$
$\displaystyle\Vdash\forall v\in q\,\exists u\in x\,\varphi(u,v,p).$

By (13) one can see that the parameters $a,b,p$ satisfy (11). Let $q\in
z^{\prime}$ be as in (12). We have already noticed that $q\in
z^{\prime\prime}$. Let $\mathbf{e}$ be such that

$\displaystyle(\mathbf{e}a)_{10}$ $\displaystyle\simeq\lambda
c.\mathbf{p}(\mathbf{p}ac)(ac)_{1},$ $\displaystyle(\mathbf{e}a)_{11}$
$\displaystyle\simeq\lambda f.\mathbf{p}f_{1}(f_{0}f_{1})_{1}.$

One can verify that $\mathbf{e}$ is as desired. ∎

##  8\. Realizing the axiom of choice in all finite types

We will make use of certain canonical names for pairs in $\mathrm{V_{ex}}(A)$.

######  Definition 8.1 (Internal pairing).

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

$\\{{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\\}.$

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

Below we shall use $\mathrm{UP}(x,y,z)$ and $\mathrm{OP}(x,y,z)$ as
abbreviations for the set-theoretic formulae expressing, respectively, that
$z$ is the unordered pair of $x$ and $y$ (in standard notation, $z=\\{x,y\\}$)
and $z$ is the ordered pair of $x$ and $y$ (in standard notation,
$z=\langle{x,y}\rangle$). E.g., $\mathrm{UP}(x,y,z)$ stands for $x\in z\land
y\in z\land\forall u\in z\,(u=x\lor u=y)$. Similarly, one can pick a suitable
rendering of $\mathrm{OP}(x,y,z)$ according to the definition of ordered pair
$\langle{x,y}\rangle:=\\{\\{x\\},\\{x,y\\}\\}$.

######  Lemma 8.2.

There are closed application terms $\mathbf{u_{0}}$, $\mathbf{u_{1}}$,
$\mathbf{v}$, $\mathbf{w}$, $\mathbf{z}$ such that for all
$x,y\in\mathrm{V_{ex}}(A)$

$\displaystyle\mathbf{u_{0}}$
$\displaystyle\Vdash\mathrm{UP}(x,x,\\{{x}\\}_{A}),$
$\displaystyle\mathbf{u_{1}}$
$\displaystyle\Vdash\mathrm{UP}(x,y,\\{{x,y}\\}_{A}),$
$\displaystyle\mathbf{v}$
$\displaystyle\Vdash\mathrm{OP}(x,y,\langle{x,y}\rangle_{\\!A}),$
$\displaystyle\mathbf{w}$
$\displaystyle\Vdash\langle{x,y}\rangle_{\\!A}=\langle{u,v}\rangle_{\\!A}\rightarrow
x=u\land y=v,$ $\displaystyle\mathbf{z}$
$\displaystyle\Vdash\mathrm{OP}(x,y,z)\rightarrow
z=\langle{x,y}\rangle_{\\!A}.$

###### Proof.

This is similar to [19, 3.2, 3.4]. ∎

We now build a copy of the hereditarily effective operations relative to a pca
$A$.

######  Definition 8.3 ($\mathsf{HEO}_{A}$).

Let $A$ be a pca over $\omega$ with map $n\mapsto\bar{n}$ from $\omega$ to
$A$. For any finite type $\sigma$, we define $a=_{\sigma}b$ with $a,b\in A$ by
letting:

  * •

$a=_{0}b$ iff there is $n\in\omega$ such that $a=b=\bar{n}$;

  * •

$a=_{\sigma\tau}b$ iff for every $c=_{\sigma}d$ we have $ac=_{\tau}bd$.

Let $A_{\sigma}=\\{a\in A\colon a=_{\sigma}a\\}$.

######  Lemma 8.4.

For any type $\sigma$, and for all $a,b,c\in A$:

  * •

if $a=_{\sigma}b$ and $b=_{\sigma}c$, then $a=_{\sigma}a$, $b=_{\sigma}a$, and
$a=_{\sigma}c$.

It thus follows that $A_{\sigma}=\bigcup_{b\in A}\\{a\in A\colon
a=_{\sigma}b\\}=\bigcup_{a\in A}\\{b\in A\colon a=_{\sigma}b\\}$ and
$=_{\sigma}$ is an equivalence relation on $A_{\sigma}$.

###### Proof.

By induction on the type. ∎

######  Definition 8.5 (Internalization of objects of finite type).

For $a\in A_{\sigma}$, we define ${a}^{\sigma}\in\mathrm{V_{ex}}(A)$ as
follows:

  * •

if $a=\bar{n}$, let
${a}^{o}=\\{\langle{\bar{m},\bar{m},{\bar{m}}^{o}}\rangle\colon m<n\\}$;

  * •

if $a\in A_{\sigma\tau}$, let
${a}^{\sigma\tau}=\\{\langle{c,d,\langle{c^{\sigma},{e}^{\tau}}\rangle_{\\!A}}\rangle\colon
c=_{\sigma}d\text{ and }ac\simeq e\\}$.

Finally, for any finite type $\sigma$, let

$\dot{F}_{\sigma}=\\{\langle{a,b,{a}^{\sigma}}\rangle\colon a=_{\sigma}b\\}$

be our name for $F_{\sigma}$.

Note that $\dot{F}_{o}=\dot{\omega}$, where $\dot{\omega}$ is the name for
$\omega$ used to realize the infinity axiom in the proof of Theorem 7.2.

######  Notation 8.6.

Write $\Vdash\varphi$ for $\exists a,b\in A\,(a=b\Vdash\varphi)$.

######  Lemma 8.7 (Absoluteness and uniqueness up to extensional equality).

For all $a,b\in A_{\sigma}$,

  * •

$\Vdash{a}^{\sigma}={b}^{\sigma}$ implies $a=_{\sigma}b$,

  * •

$a=_{\sigma}b$ implies ${a}^{\sigma}={b}^{\sigma}$.

###### Proof.

By induction on the type.

Type $o$. Let $a=\bar{n}$ and $b=\bar{m}$ with $n,m\in\omega$. Suppose
$\Vdash{a}^{o}={b}^{o}$. By a double arithmetical induction one shows $n=m$.
The second part is obvious as $a=_{o}b$ implies $a=b$.

Type $\sigma\tau$. Let $a,b\in A_{\sigma\tau}$. Suppose
$\Vdash{a}^{\sigma\tau}={b}^{\sigma\tau}$. The aim is to show that
$a=_{\sigma\tau}b$. Let $c\in A_{\sigma}$ and $ac\simeq e$. Then
$\Vdash\langle{{c}^{\sigma},{e}^{\tau}}\rangle_{\\!A}\in{a}^{\sigma\tau}$ and
hence
$\Vdash\langle{{c}^{\sigma},{e}^{\tau}}\rangle_{\\!A}\in{b}^{\sigma\tau}$.
¿From the latter we infer that there exist $c_{0}\in A_{\sigma}$ and $e_{0}\in
A_{\tau}$ such that $bc_{0}\simeq e_{0}$ and
$\Vdash\langle{{c}^{\sigma},{e}^{\tau}}\rangle_{\\!A}=\langle{{c_{0}}^{\sigma},{e_{0}}^{\tau}}\rangle_{\\!A}$.
By the properties of internal pairing, we obtain
$\Vdash{c}^{\sigma}={c_{0}}^{\sigma}\;\wedge\;{e}^{\tau}={e_{0}}^{\tau}$
giving $c=_{\sigma}c_{0}$ and $e=_{\tau}e_{0}$ by the induction hypothesis.
Whence $ac=_{\tau}bc_{0}=_{\tau}bc$ as $b\in A_{\sigma\tau}$. As a result one
has $ac=_{\tau}bd$ whenever $c=_{\sigma}d$, yielding $a=_{\sigma\tau}b$.

For the second part, suppose $a=_{\sigma\tau}b$. An element of
${a}^{\sigma\tau}$ is of the form
$\langle{c,d,\langle{{c}^{\sigma},{e}^{\tau}}\rangle_{\\!A}}\rangle$ where
$c=_{\sigma}d$ and $ac\simeq e$. Let $e_{0}\simeq bc$. As $ac=_{\tau}bc$ the
induction hypothesis yields ${e}^{\tau}={e_{0}}^{\tau}$, and hence
$\langle{c,d,\langle{{c}^{\sigma},{e}^{\tau}}\rangle_{\\!A}}\rangle=\langle{c,d,\langle{{c}^{\sigma},{e_{0}}^{\tau}}\rangle_{\\!A}}\rangle\in{b}^{\sigma\tau}$,
showing ${a}^{\sigma\tau}\subseteq{b}^{\sigma\tau}$. Owing to the symmetry of
the argument, we can conclude that ${a}^{\sigma\tau}={b}^{\sigma\tau}$. ∎

######  Theorem 8.8 (Choice).

There exists a closed application term $\mathbf{e}$ such that ${\sf CZF}$
proves

$\mathbf{e}\Vdash\forall x\in\dot{F}_{\sigma}\,\exists
y\in\dot{F}_{\tau}\,\varphi(x,y)\rightarrow\exists
f\colon\dot{F}_{\sigma}\to\dot{F}_{\tau}\,\forall
x\in\dot{F}_{\sigma}\,\varphi(x,f(x)),$

for all finite types $\sigma$ and $\tau$ and for every formula $\varphi$.

###### Proof.

Suppose $a=b\Vdash\forall x\in\dot{F}_{\sigma}\,\exists
y\in\dot{F}_{\tau}\,\varphi(x,y)$. By definition, this means that for every
$\langle{c,d,{c}^{\sigma}}\rangle\in\dot{F}_{\sigma}$ we have

$\langle{(ac)_{0},(bd)_{0},{e}^{\tau}}\rangle\in\dot{F}_{\tau},$
$(ac)_{1}=(bd)_{1}\Vdash\varphi({c}^{\sigma},{e}^{\tau}),$

where $e\simeq(ac)_{0}$. Let

$f=\\{\langle{c,d,\langle{{c}^{\sigma},{e}^{\tau}}\rangle_{\\!A}}\rangle\colon
c=_{\sigma}d\land e\simeq(ac)_{0}\\}.$

Note that $c=_{\sigma}d$ implies $(ac)_{0}\downarrow$ by (1).

Below we shall use $z=\langle x,y\rangle$ as a somewhat sloppy abbreviation
for $\mathrm{OP}(x,y,z)$. We look for an $\mathbf{e}$ such that

$(\mathbf{e}a)_{0}=(\mathbf{e}b)_{0}\Vdash\forall z\in f\,\exists
x\in\dot{F}_{\sigma}\,\exists y\in\dot{F}_{\tau}\,(z=\langle{x,y}\rangle),$
$(\mathbf{e}a)_{10}=(\mathbf{e}b)_{10}\Vdash\forall
x\in\dot{F}_{\sigma}\,\exists y\in\dot{F}_{\tau}\,\exists z\in
f\,(z=\langle{x,y}\rangle\land\varphi(x,y)),$
$(\mathbf{e}a)_{11}=(\mathbf{e}b)_{11}\Vdash\forall z_{0}\in f\,\forall
z_{1}\in f\,\forall x,y_{0},y_{1}\,(z_{0}=\langle{x,y_{0}}\rangle\land
z_{1}=\langle{x,y_{1}}\rangle\rightarrow y_{0}=y_{1}).$

First, note that $\lambda c.(ac)_{0}=_{\sigma\tau}\lambda d.(bd)_{0}$. This
follows from (1). In fact, $c=_{\sigma}d$ implies $(ac)_{0}=_{\tau}(bd)_{0}$,
for all $c,d\in A$. Moreover, since this is an equivalence relation, we have
$\lambda c.(ac)_{0}\in A_{\sigma\tau}$.

For (3), let $\mathbf{e}$ be such that

$\displaystyle((\mathbf{e}a)_{0}c)_{0}$ $\displaystyle\simeq c,$
$\displaystyle((\mathbf{e}a)_{0}c)_{10}$ $\displaystyle\simeq(ac)_{0},$
$\displaystyle((\mathbf{e}a)_{0}c)_{11}$ $\displaystyle\simeq\mathbf{v},$

where $\mathbf{v}\Vdash\langle{x,y}\rangle_{\\!A}=\langle{x,y}\rangle$ for all
$x,y\in\mathrm{V_{ex}}(A)$ as in Lemma 8.2. Let us show that any such
$\mathbf{e}$ satisfies (3). Let
$\langle{c,d,\langle{{c}^{\sigma},{e}^{\tau}}\rangle_{\\!A}}\rangle\in f$,
where $e\simeq(ac)_{0}$. We would like

$(\mathbf{e}a)_{0}c=(\mathbf{e}b)_{0}d\Vdash\exists
x\in\dot{F}_{\sigma}\,\exists
y\in\dot{F}_{\tau}\,(\langle{{c}^{\sigma},{e}^{\tau}}\rangle_{\\!A}=\langle{x,y}\rangle).$

Now, $\langle{c,d,{c}^{\sigma}}\rangle\in\dot{F}_{\sigma}$,
$c\simeq((\mathbf{e}a)_{0}c)_{0}$, and $d\simeq((\mathbf{e}b)_{0}d)_{0}$.
Therefore, we just need to verify

$((\mathbf{e}a)_{0}c)_{1}=((\mathbf{e}b)_{0}d)_{1}\Vdash\exists
y\in\dot{F}_{\tau}\,\langle{{c}^{\sigma},{e}^{\tau}}\rangle_{\\!A}=\langle{{c}^{\sigma},y}\rangle.$

Similarly, $\langle{(ac)_{0},(bd)_{0},{e}^{\sigma}}\rangle\in\dot{F}_{\tau}$
since, as noted before, $(ac)_{0}=_{\tau}(bd)_{0}$. On the other hand,
$(ac)_{0}\simeq((\mathbf{e}a)_{0}c)_{10}$ and
$(bd)_{0}\simeq((\mathbf{e}b)_{0}d)_{10}$. So we just need to show that

$((\mathbf{e}a)_{0}c)_{11}=((\mathbf{e}b)_{0}d)_{11}\Vdash\langle{{c}^{\sigma},{e}^{\tau}}\rangle_{\\!A}=\langle{{c}^{\sigma},{e}^{\tau}}\rangle.$

Now,
$((\mathbf{e}a)_{0}c)_{11}\simeq((\mathbf{e}b)_{0}d)_{11}\simeq\mathbf{v}$,
and
$\mathbf{v}\Vdash\langle{{c}^{\sigma},{e}^{\tau}}\rangle_{\\!A}=\langle{{c}^{\sigma},{e}^{\tau}}\rangle$.
So we are done.

As for (4), Let $\mathbf{e}$ be such that

$\displaystyle((\mathbf{e}a)_{10}c)_{0}$ $\displaystyle\simeq(ac)_{0},$
$\displaystyle((\mathbf{e}a)_{10}c)_{10}$ $\displaystyle\simeq(ac)_{0},$
$\displaystyle((\mathbf{e}a)_{10}c)_{110}$ $\displaystyle\simeq\mathbf{v},$
$\displaystyle((\mathbf{e}a)_{10}c)_{111}$ $\displaystyle\simeq(ac)_{1},$

where $\mathbf{v}$ is as in part (3). That $\mathbf{e}$ satisfies (4) is
proved in similar fashion by using (1) and (2).

For (5), suppose $\langle{c_{i},d_{i},z_{i}}\rangle\in f$ with
$z_{i}=\langle{{c_{i}}^{\sigma},{e_{i}}^{\tau}}\rangle_{\\!A}$ and
$e_{i}\simeq(ac_{i})_{0}$, where $i=0,1$. We are looking for an $\mathbf{e}$
such that

$(\mathbf{e}a)_{11}c_{0}c_{1}=(\mathbf{e}b)_{11}d_{0}d_{1}\Vdash
z_{0}=\langle{x,y_{0}}\rangle\land z_{1}=\langle{x,y_{1}}\rangle\rightarrow
y_{0}=y_{1},$

for all $x,y_{0},y_{1}\in\mathrm{V_{ex}}(A)$. Suppose

$g=h\Vdash z_{0}=\langle{x,y_{0}}\rangle\land z_{1}=\langle{x,y_{1}}\rangle.$

We want $(\mathbf{e}a)_{11}c_{0}c_{1}g=(\mathbf{e}b)_{11}d_{0}d_{1}h\Vdash
y_{0}=y_{1}$. Unravelling (6), we get

$g_{i}=h_{i}\Vdash\langle{{c_{i}}^{\sigma},{e_{i}}^{\tau}}\rangle_{\\!A}=\langle{x,y_{i}}\rangle.$

By Lemma 8.2,

$\mathbf{w}g_{i}=\mathbf{w}h_{i}\Vdash{c_{i}}^{\sigma}=x\land{e_{i}}^{\tau}=y_{i},$

for some closed application term $\mathbf{w}$. By the realizabilty of
equality, it follows that

$\Vdash{c_{0}}^{\sigma}={c_{1}}^{\sigma}.$

Also,

$\mathbf{p}(\mathbf{w}g_{0})_{1}(\mathbf{w}g_{1})_{1}=\mathbf{p}(\mathbf{w}h_{0})_{1}(\mathbf{w}h_{1})_{1}\Vdash{e_{0}}^{\tau}=y_{0}\land{e_{1}}^{\tau}=y_{1}.$

By absoluteness, (7) implies $c_{0}=_{\sigma}c_{1}$. As $\lambda c.(ac)_{0}\in
A_{\sigma\tau}$, we have $(ac_{0})_{0}=_{\tau}(ac_{1})_{0}$, that is,
$e_{0}=_{\tau}e_{1}$. By uniqueness, ${e_{0}}^{\tau}={e_{1}}^{\tau}$. By
realizability of equality, there is a closed application term $\mathbf{i}$
such that

$\mathbf{i}\Vdash z=y_{0}\land z=y_{1}\rightarrow y_{0}=y_{1}.$

Therefore $\mathbf{e}$ can be chosen such that

$(\mathbf{e}a)_{11}c_{0}c_{1}g\simeq\mathbf{i}(\mathbf{p}(\mathbf{w}g_{0})_{1}(\mathbf{w}g_{1})_{1})$

is as required.

By $\lambda$-abstraction, one can find $\mathbf{e}$ satisfying (3), (4), and
(5). ∎

######  Theorem 8.9 (Arrow types).

There exists a closed application term $\mathbf{e}$ such that ${\sf CZF}$
proves

$\mathbf{e}\Vdash\dot{F}_{\sigma\tau}=\dot{F}_{\sigma}\to\dot{F}_{\tau},$

for all finite types $\sigma$ and $\tau$.

###### Proof.

We look for $\mathbf{e}$ such that

$\mathbf{e}_{0}\Vdash\forall
f\in\dot{F}_{\sigma\tau}\,(f\colon\dot{F}_{\sigma}\to\dot{F}_{\tau}),$

and for every $f\in\mathrm{V_{ex}}(A)$,

$\mathbf{e}_{1}\Vdash(f\colon\dot{F}_{\sigma}\to\dot{F}_{\tau})\rightarrow
f\in\dot{F}_{\sigma\tau}.$

For $\mathbf{e}_{0}$, we need that for all $a=_{\sigma\tau}b$,

$(\mathbf{e}_{0}a)_{0}=(\mathbf{e}_{0}b)_{0}\Vdash\forall
z\in{a}^{\sigma\tau}\,\exists x\in\dot{F}_{\sigma}\,\exists
y\in\dot{F}_{\tau}\,(z=\langle{x,y}\rangle),$
$(\mathbf{e}_{0}a)_{10}=(\mathbf{e}_{0}b)_{10}\Vdash\forall
x\in\dot{F}_{\sigma}\,\exists y\in\dot{F}_{\tau}\,\exists
z\in{a}^{\sigma\tau}\,(z=\langle{x,y}\rangle),$
$(\mathbf{e}_{0}a)_{11}=(\mathbf{e}_{0}b)_{11}\Vdash\forall
z_{0}\in{a}^{\sigma\tau}\,\forall z_{1}\in{a}^{\sigma\tau}\,\forall
x,y_{0},y_{1}\,(z_{0}=\langle{x,y_{0}}\rangle\land
z_{1}=\langle{x,y_{1}}\rangle\rightarrow y_{0}=y_{1}).$

For (1), let $\mathbf{e}_{0}$ be such that

$(\mathbf{e}_{0}a)_{0}\simeq\lambda c.\mathbf{p}c(\mathbf{p}(ac)\mathbf{v}),$

where $\mathbf{v}\Vdash\langle{x,y}\rangle_{\\!A}=\langle{x,y}\rangle$ for all
$x,y\in\mathrm{V_{ex}}(A)$ as in Lemma 8.2.

Let us verify that $\mathbf{e}_{0}$ does the job. Let $a=_{\sigma\tau}b$. We
want to show

$\lambda c.\mathbf{p}c(\mathbf{p}(ac)\mathbf{v})=\lambda
d.\mathbf{p}d(\mathbf{p}(bd)\mathbf{v})\Vdash\forall
z\in{a}^{\sigma\tau}\,\exists x\in\dot{F}_{\sigma}\,\exists
y\in\dot{F}_{\tau}\,(z=\langle{x,y}\rangle).$

Let
$\langle{c,d,\langle{{c}^{\sigma},{c}^{\tau}}\rangle_{\\!A}}\rangle\in{a}^{\sigma\tau}$,
where $c=_{\sigma}d$ and $ac\simeq e$. We want

$\mathbf{p}c(\mathbf{p}(ac)\mathbf{v})=\mathbf{p}d(\mathbf{p}(bd)\mathbf{v})\Vdash\exists
x\in\dot{F}_{\sigma}\,\exists
y\in\dot{F}_{\tau}\,(\langle{{c}^{\sigma},{c}^{\tau}}\rangle_{\\!A}=\langle{x,y}\rangle).$

By definition, $\langle{c,d,{c}^{\sigma}}\rangle\in\dot{F}_{\sigma}$. Let us
check that

$\mathbf{p}(ac)\mathbf{v}=\mathbf{p}(bd)\mathbf{v}\Vdash\exists
y\in\dot{F}_{\tau}\,(\langle{{c}^{\sigma},{c}^{\tau}}\rangle_{\\!A}=\langle{{c}^{\sigma},y}\rangle).$

We have $ac=_{\tau}bd$ and hence
$\langle{ac,bd,{c}^{\tau}}\rangle\in\dot{F}_{\tau}$. Finally,

$\mathbf{v}\Vdash\langle{{c}^{\sigma},{c}^{\tau}}\rangle_{\\!A}=\langle{{c}^{\sigma},{c}^{\tau}}\rangle.$

For (2), let $\mathbf{e}_{0}$ be such that

$(\mathbf{e}_{0}a)_{10}\simeq\lambda x.\mathbf{p}(ax)(\mathbf{p}x\mathbf{v}),$

where $\mathbf{v}$ is as above.

For (3), let $\mathbf{e}_{0}$ be such that

$(\mathbf{e}_{0}a)_{11}c_{0}c_{1}g\simeq\mathbf{i}(\mathbf{p}(\mathbf{w}g_{0})_{1}(\mathbf{w}g_{1})_{1}),$

where $\mathbf{w}$ and $\mathbf{i}$ are as in the proof of Theorem 8.8.

As for $\mathbf{e}_{1}$, suppose that $f\in\mathrm{V_{ex}}(A)$ and

$a=b\Vdash f\colon\dot{F}_{\sigma}\to\dot{F}_{\tau}.$

Then

$a_{0}=b_{0}\Vdash\forall z\in f\,\exists x\in\dot{F}_{\sigma}\,\exists
y\in\dot{F}_{\tau}\,(z=\langle{x,y}\rangle),$ $a_{10}=b_{10}\Vdash\forall
x\in\dot{F}_{\sigma}\,\exists y\in\dot{F}_{\tau}\,\exists z\in
f\,(z=\langle{x,y}\rangle),$ $a_{11}=b_{11}\Vdash\forall z_{0}\in f\,\forall
z_{1}\in f\,\forall x,y_{0},y_{1}\,(z_{0}=\langle{x,y_{0}}\rangle\land
z_{1}=\langle{x,y_{1}}\rangle\rightarrow y_{0}=y_{1}).$

We aim for

$\mathbf{e}_{1}a=\mathbf{e}_{1}b\Vdash f\in\dot{F}_{\sigma\tau}.$

As in the proof of Theorem 8.8, it follows from (5) that $\lambda
c.(a_{10}c)_{0}=_{\sigma\tau}\lambda d.(b_{10}d)_{0}$. Therefore

$\langle{\lambda c.(a_{10}c)_{0},\lambda
d.(b_{10}d)_{0},{g}^{\sigma\tau}}\rangle\in\dot{F}_{\sigma\tau},$

where $g:=\lambda c.(a_{10}c)_{0}$. We thus want $\mathbf{e}_{1}$ such that

$(\mathbf{e}_{1}a)_{0}\simeq\lambda c.(a_{10}c)_{0},$
$(\mathbf{e}_{1}a)_{1}=(\mathbf{e}_{1}b)_{1}\Vdash f={g}^{\sigma\tau}.$

By definition and Lemma 8.7,

${g}^{\sigma\tau}=\\{\langle{c,d,\langle{{c}^{\sigma},{c}^{\tau}}\rangle_{\\!A}}\rangle\colon
c=_{\sigma}d\land(a_{10}c)_{0}=_{\tau}e\\}.$

($\subseteq$) Let $\langle{\tilde{c},\tilde{d},z}\rangle\in f$. We aim for
$((\mathbf{e}_{1}a)_{1}\tilde{c})_{0}=((\mathbf{e}_{1}b)_{1}\tilde{d})_{0}\Vdash
z\in{g}^{\sigma\tau}$. By (4),
$(a_{0}\tilde{c})_{0}=_{\sigma}(b_{0}\tilde{d})_{0}$ and

$(a_{0}\tilde{c})_{11}=(b_{0}\tilde{d})_{11}\Vdash
z=\langle{{c}^{\sigma},{c}^{\tau}}\rangle,$

where $c\simeq(a_{0}\tilde{c})_{0}$ and $e\simeq(a_{0}\tilde{c})_{10}$. By
Lemma 8.2, let $\mathbf{z}$ be a closed application term such that for all
$x,y,z\in\mathrm{V_{ex}}(A)$,

$\mathbf{z}\Vdash z=\langle{x,y}\rangle\rightarrow
z=\langle{x,y}\rangle_{\\!A}.$

Then

$\mathbf{z}(a_{0}\tilde{c})_{11}=\mathbf{z}(b_{0}\tilde{d})_{11}\Vdash
z=\langle{{c}^{\sigma},{c}^{\tau}}\rangle_{\\!A}.$

By using (5), (6) and absoluteness, one obtains $(a_{10}c)_{0}=_{\tau}e$. Let
$\mathbf{e}_{1}$ satisfy

$\displaystyle((\mathbf{e}_{1}a)_{1}\tilde{c})_{00}$
$\displaystyle\simeq(a_{0}\tilde{c})_{0},$
$\displaystyle((\mathbf{e}_{1}a)_{1}\tilde{c})_{01}$
$\displaystyle\simeq\mathbf{z}(a_{0}\tilde{c})_{11}.$

Then $\mathbf{e}_{1}$ is as desired.

($\supseteq$) Let
$\langle{c,d,\langle{{c}^{\sigma},{c}^{\tau}}\rangle_{\\!A}}\rangle\in{g}^{\sigma\tau}$,
with $e\simeq(a_{10}c)_{0}$. We aim for
$((\mathbf{e}_{1}a)_{1}c)_{1}=((\mathbf{e}_{1}b)_{1}d)_{1}\Vdash\langle{{c}^{\sigma},{c}^{\tau}}\rangle_{\\!A}\in
f$.

By unravelling (5), we obtain that for some $z\in\mathrm{V_{ex}}(A)$,

$\langle{(a_{10}c)_{10},(b_{10}d)_{10},z}\rangle\in f,$
$(a_{10}c)_{11}=(b_{10}d)_{11}\Vdash
z=\langle{{c}^{\sigma},{c}^{\tau}}\rangle.$

Let $\mathbf{e}_{1}$ be such that

$((\mathbf{e}_{1}a)_{1}c)_{1}\simeq\mathbf{p}(a_{10}c)_{10}(\mathbf{i_{s}}(\mathbf{z}(a_{10}c)_{11})),$

where $\mathbf{z}$ is as above.

By $\lambda$-abstraction, one can find $\mathbf{e}$ satisfying the above
equations. ∎

######  Theorem 8.10.

For all finite types $\sigma$ and $\tau$ there exists a closed application
term $\mathbf{c}$ such that ${\sf CZF}$ proves

$\mathbf{c}\Vdash\forall x^{\sigma}\,\exists
y^{\tau}\,\varphi(x,y)\rightarrow\exists f^{\sigma\tau}\,\forall
x^{\sigma}\,\varphi(x,f(x)).$

###### Proof.

A proof is obtained by combining Theorem 8.8 and Theorem 8.9. Let

$\vartheta_{0}(z):=\text{`$z$ is the set of natural numbers'},$
$\vartheta_{\sigma\tau}(z):=\exists x\,\exists
y\,(\vartheta_{\sigma}(x)\land\vartheta_{\tau}(y)\land z=x\to y).$

We are claiming that for all finite types $\sigma$ and $\tau$ there exists a
closed application term $\mathbf{c}_{\sigma\tau}$ such that ${\sf CZF}$ proves

$\mathbf{c}_{\sigma\tau}\Vdash\forall z_{\sigma}\,\forall
z_{\tau}\,(\vartheta_{\sigma}(z_{\sigma})\land\vartheta_{\tau}(z_{\tau})\rightarrow\psi(z_{\sigma},z_{\tau})),$

where $\psi(z_{\sigma},z_{\tau})$ is

$\forall x\in z_{\sigma}\,\exists y\in
z_{\tau}\,\varphi(x,y)\rightarrow\exists f\colon z_{\sigma}\to
z_{\tau}\,\forall x\in z_{\sigma}\,\varphi(x,f(x)).$

Let $\mathbf{e}_{0}$ be such that
$\mathbf{e}_{0}\Vdash\vartheta_{0}(\dot{\omega})$. By using $\mathbf{e}_{0}$
and Theorem 8.9, for every finite type $\sigma$, we can find
$\mathbf{e}_{\sigma}$ such that
$\mathbf{e}_{\sigma}\Vdash\vartheta_{\sigma}(\dot{F}_{\sigma})$. As ${\sf
CZF}\vdash\vartheta_{\sigma}(z_{0})\land\vartheta_{\sigma}(z_{1})\rightarrow
z_{0}=z_{1}$, by soundness (Theorem 7.2) there is a $\mathbf{u}_{\sigma}$ such
that

$\mathbf{u}_{\sigma}\Vdash\vartheta_{\sigma}(z_{0})\land\vartheta_{\sigma}(z_{1})\rightarrow
z_{0}=z_{1}$

for all $z_{0},z_{1}\in\mathrm{V_{ex}}(A)$. By soundness as well, there are
$\mathbf{i}_{\sigma\tau}$ and $\mathbf{j}_{\sigma\tau}$ such that

$\displaystyle\mathbf{i}_{\sigma\tau}$
$\displaystyle\Vdash\psi(\dot{F}_{\sigma},\dot{F}_{\tau})\land
z_{\sigma}=\dot{F}_{\sigma}\rightarrow\psi(z_{\sigma},\dot{F}_{\tau}),$
$\displaystyle\mathbf{j}_{\sigma\tau}$
$\displaystyle\Vdash\psi(z_{\sigma},\dot{F}_{\tau})\land
z_{\tau}=\dot{F}_{\tau}\rightarrow\psi(z_{\sigma},z_{\tau}),$

for all $z_{\sigma},z_{\tau}\in\mathrm{V_{ex}}(A)$. Finally, with the aid of
$\mathbf{e}_{\sigma}$, $\mathbf{e}_{\tau}$, $\mathbf{u}_{\sigma}$,
$\mathbf{u}_{\tau}$, $\mathbf{i}_{\sigma\tau}$, $\mathbf{j}_{\sigma\tau}$, and
of the closed application term $\mathbf{e}$ from Theorem 8.8, one can
construct $\mathbf{c}_{\sigma\tau}$ as desired. ∎

######  Corollary 8.11.

For every theorem $\varphi$ of ${\sf CZF}+{\sf AC}_{{\sf FT}}$, there is a
closed application term $\mathbf{e}$ such that ${\sf CZF}$ proves
$\mathbf{e}\Vdash\varphi$. In particular, ${\sf CZF}+{\sf AC}_{{\sf FT}}$ is
consistent relative to ${\sf CZF}$.

###### Proof.

By Theorem 7.2 and Theorem 8.10. ∎

######  Corollary 8.12.

${\sf CZF}+{\sf AC}_{{\sf FT}}$ is conservative over ${\sf CZF}$ with respect
to $\Pi^{0}_{2}$ sentences.

###### Proof.

Let $\varphi(x,y)$ be a bounded formula with displayed free variables and
suppose that

$\forall x\in\omega\,\exists y\in\omega\,\varphi(x,y)$

is provable in ${\sf CZF}$ plus ${\sf AC}_{{\sf FT}}$. By the corollary above,
we can find a closed application term $\mathbf{e}$ such that

${\sf CZF}\vdash\mathbf{e}\Vdash\forall x\in\dot{\omega}\,\exists
y\in\dot{\omega}\,\varphi(x,y).$

In particular,

${\sf CZF}\vdash\forall n\in\omega\,\exists
m\in\omega\,(e\bar{n})_{1}\Vdash\varphi(\dot{n},\dot{m}).$

It is a routine matter (cf. also [19, Chapter 4, Theorem 2.6]) to show that
realizability equals truth for bounded arithmetic formulas, namely,

${\sf CZF}\vdash\forall
n_{1},\ldots,n_{k}\in\omega\,(\psi(n_{1},\ldots,n_{k})\leftrightarrow\exists
a,b\in A\,(a=b\Vdash\psi(\dot{n}_{1},\ldots,\dot{n}_{k})),$

for $\psi(x_{1},\ldots,x_{k})$ bounded with all the free variables shown. We
can then conclude

${\sf CZF}\vdash\forall x\in\omega\,\exists y\in\omega\,\varphi(x,y).$

∎

##  9\. Soundness for ${\sf IZF}$

The theory ${\sf IZF}$ (Intuitionistic Zermelo-Fraenkel set theory) shares the
logic and language of ${\sf CZF}$. Its axioms are

1\. Extensionality,

2\. Pairing,

3\. Union,

4\. Infinity,

5\. Set induction,

6\. Separation: $\forall x\,\exists y\,\forall z\,(z\in y\leftrightarrow z\in
x\land\varphi(z))$, for all formulae $\varphi$,

7\. Collection: $\forall u\in x\,\exists v\,\varphi(u,v)\rightarrow\exists
y\,\forall u\in x\,\exists v\in y\,\varphi(u,v)$, for all formulae $\varphi$,

8\. Powerset: $\forall x\,\exists y\,\forall z\,(\forall u\in z\,(u\in
x)\rightarrow z\in y)$.

Thus ${\sf IZF}$ is a strengthening of ${\sf 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.

Note that in ${\sf IZF}$, due to the presence of powerset, the construction of
$\mathrm{V_{ex}}(A)$ can proceed by transfinite recursion along the ordinals
(cf. [19]).

######  Theorem 9.1.

For every theorem $\varphi$ of ${\sf IZF}+{\sf AC}_{{\sf FT}}$, there is a
closed application term $\mathbf{e}$ such that ${\sf IZF}$ proves
$\mathbf{e}\Vdash\varphi$. In particular, ${\sf IZF}+{\sf AC}_{{\sf FT}}$ is
consistent relative to ${\sf IZF}$.

###### Proof.

The soundness for theorems of intuitionistic first order logic with equality
follows immediately from Theorem 6.4. As for nonlogical axioms, in view of
Corollary 8.11, it is sufficient to deal with separation and powerset.

The argument for separation is similar to the corresponding argument for
bounded separation in the proof of Theorem 7.2, employing full separation in
the background theory.

It thus remains to address powerset. Write $z\subseteq x$ for $\forall u\in
z\,(u\in x)$. We look for $\mathbf{e}$ such that for all
$x\in\mathrm{V_{ex}}(A)$ there is a $y\in\mathrm{V_{ex}}(A)$ such that

$\mathbf{e}\Vdash z\subseteq x\rightarrow z\in y,$

for all $z\in\mathrm{V_{ex}}(A)$.

On account of powerset, in ${\sf IZF}$, we can define sets
$\mathrm{V_{ex}}(A)_{\alpha}$, with $\alpha$ ordinal (i.e., a transitive set
of transitive sets), such that
$\mathrm{V_{ex}}(A)=\bigcup_{\alpha}\mathrm{V_{ex}}(A)_{\alpha}$ and
$\mathrm{V_{ex}}(A)_{\alpha}=\bigcup_{\beta\in\alpha}\operatorname{\mathcal{P}}(A\times
A\times\mathrm{V_{ex}}(A)_{\beta})$. Note that in ${\sf CZF}$ the
$\mathrm{V_{ex}}(A)_{\alpha}$’s are just classes.

Given $x\in\mathrm{V_{ex}}(A)_{\alpha}$, let

$y=\\{\langle{a,b,z}\rangle\in A\times A\times\mathrm{V_{ex}}(A)_{\alpha}\mid
a=b\Vdash z\subseteq x\\}.$

The set $y$ exists by separation. Set

$\mathbf{e}:=\lambda a.\mathbf{p}a\mathbf{i_{r}}.$

It is easy to check that $y$ and $\mathbf{e}$ are as desired, once established
that if $z\in\mathrm{V_{ex}}(A)$ and $a=b\Vdash z\subseteq x$ then
$z\in\mathrm{V_{ex}}(A)_{\alpha}$. This is proved by set induction by showing
that for all $u,v\in\mathrm{V_{ex}}(A)$:

  * •

if $a=b\Vdash u\in v$ and $v\in\mathrm{V_{ex}}(A)_{\alpha}$, then
$u\in\mathrm{V_{ex}}(A)_{\beta}$ for some $\beta\in\alpha$;

  * •

if $a=b\Vdash u=v$ and $v\in\mathrm{V_{ex}}(A)_{\alpha}$, then
$u\in\mathrm{V_{ex}}(A)_{\alpha}$.

∎

As before, we obtain the following.

######  Corollary 9.2.

${\sf IZF}+{\sf AC}_{{\sf FT}}$ is conservative over ${\sf IZF}$ with respect
to $\Pi^{0}_{2}$ sentences.

##  10\. Conclusions

We defined an extensional notion of realizability that validates ${\sf CZF}$
along with all finite type axiom of choice ${\sf AC}_{{\sf FT}}$ provably in
${\sf CZF}$. We have shown that one can replace ${\sf CZF}$ with ${\sf IZF}$.
Presumably, this holds true for many other intuitionistic set theories as
well.

There is a sizable number of well-known _extra principles_ $P$ that can be
added to the mix, in the sense that $T+P$ proves $\mathbf{e}\Vdash P$, for
some closed application term $\mathbf{e}$, where $T$ is either ${\sf CZF}$ or
${\sf IZF}$. This applies to arbitrary pca’s in the case of large set axioms
such as $\sf REA$ (Regular Extension axiom) by adapting [25, Theorem 6.2]. In
the case of choice principles, this also applies to arbitrary pca’s for
Countable Choice, ${\sf DC}$ (Dependent Choice), ${\sf RDC}$ (Relativized
Dependent Choice), and ${\sf PAx}$ (Presentation Axiom) by adapting the
techniques of [8]. Specializing to the case of the first Kleene algebra, one
obtains extensional realizability of ${\sf MP}$ (Markov Principle) and forms
of ${\sf IP}$ (Independence of Premise) adapting results from [19, Section
11], [20] , [25, Section 7].

We claim that realizability combined with truth and the appropriate pca
modeled on [23, 26] yields the closure under the choice rule for finite types,
i.e.,

$\text{If }T\vdash\forall x^{\sigma}\,\exists y^{\tau}\,\varphi(x,y),\text{
then }T\vdash\exists f^{\sigma\tau}\,\forall x^{\sigma}\,\varphi(x,f(x))$

for large swathes of intuitionistic set theories.

Church’s thesis,

$\forall f\colon\omega\to\omega\,\exists e\in\omega\,\forall
x\in\omega\,(f(x)\simeq\\{e\\}(x)),$

where $\\{e\\}(x)$ is Turing machine application, and the finite type axiom of
choice are incompatible in extensional finite type arithmetic [31] (cf. [5,
Chapter 5, Theorem 6.1]).888The elementary recursion-theoretic reason that
prevents Church’s thesis from being extensionally realizable is the usual one:
there is no type $2$ extensional index in Kleene’s first algebra, that is,
there is no $e\in\omega$ such that, for all $a,b\in\omega$, if
$\\{a\\}(n)=\\{b\\}(n)$ for every $n\in\omega$, i.e., $a=_{1}b$, then
$\\{e\\}(a)=\\{e\\}(b)$. A fortiori, they are incompatible on the basis of
${\sf CZF}$, and thus of ${\sf IZF}$. However, negative versions of Church’s
thesis can still obtain in a universe in which ${\sf AC}_{{\sf FT}}$ holds.
The assertion that no function from $\omega$ to $\omega$ is incomputable is
known as weak Church’s thesis [30]:

$\forall f\colon\omega\to\omega\,\neg\neg\exists e\in\omega\,\forall
x\in\omega\,(f(x)\simeq\\{e\\}(x)).$

Using Kleene’s first algebra, one can easily verify that WCT is extensionally
realizable in ${\sf CZF}$. Therefore, ${\sf CZF}$ augmented with both ${\sf
AC}_{{\sf FT}}$ and ${\sf WCT}$ is consistent relative to ${\sf CZF}$, and
similarly for ${\sf IZF}$.

Continuity principles are a hallmark of Brouwer’s intuitionism. They are
compatible with finite type arithmetic (see [5, 30, 31, 34]) and also with set
theory (see [5, 19, 23, 22]). They are known, though, to invite conflict with
${\sf AC}_{{\sf FT}}$ (see [29, Theorem 9.6.11]). However, as in the case of
CT, negative versions of them are likely to be compatible with ${\sf AC}_{{\sf
FT}}$ on the basis of ${\sf CZF}$ and ${\sf IZF}$. Similar to the case of
${\sf CT}$, one would expect that the assertion that no function from
$\mathbb{R}$ to $\mathbb{R}$ is discontinuous can go together with ${\sf
AC}_{{\sf FT}}$. One obvious tool that suggests itself here is extensional
generic realizability based on Kleene’s second algebra. We shall not venture
into this here and add the verification of this claim to the task list.

We conclude with the following remark. It is currently unknown whether one can
provide a realizability model for choice principles based on larger type
structures. Say that $I$ is a base if for every $I$-indexed family
$(X_{i})_{i\in I}$ of inhabited sets $X_{i}$ there exists a function $f\colon
I\to\bigcup_{i\in I}X_{i}$ such that $f(i)\in X_{i}$ for every $i\in I$. Let
$\mathcal{C}$-${\sf AC}$ say that every set $I$ in the class $\mathcal{C}$ is
a base. The question is whether one can realize $\mathcal{C}$-${\sf AC}$,
where $\mathcal{C}$ is the smallest $\Pi\Sigma$-closed class, or even the
smallest $\Pi\Sigma W$-closed class, without assuming choice in the background
theory.

## References

  * [1] Peter Aczel.  The type theoretic interpretation of constructive set theory: inductive definitions.  In Logic, methodology and philosophy of science, VII (Salzburg, 1983), volume 114 of Stud. Logic Found. Math., pages 17–49. North-Holland, Amsterdam, 1986.
  * [2] Peter Aczel and Michael Rathjen.  Notes on constructive set theory.  Technical Report 40, Institut Mittag-Leffler, 2001.
  * [3] Peter Aczel and Michael Rathjen.  Notes on constructive set theory.  Available at http://www1.maths.leeds.ac.uk/~rathjen/book.pdf, 2010\.
  * [4] Michael J. Beeson.  Continuity in intuitionistic set theories.  In Studies in Logic and the Foundations of Mathematics, volume 97, pages 1–52. Elsevier, 1979.
  * [5] Michael J. Beeson.  Foundations of constructive mathematics, volume 6 of Ergebnisse der Mathematik und ihrer Grenzgebiete (3) [Results in Mathematics and Related Areas (3)].  Springer-Verlag, Berlin, 1985.
  * [6] Haskell Brooks Curry.  An analysis of logical substitution.  American Journal of Mathematics, 51:509–536, 789–834, 1929.
  * [7] Haskell Brooks Curry.  Grundlagen der kombinatorischen Logik.  American Journal of Mathematics, 51:363–384, 1930.
  * [8] Eman Dihoum and Michael Rathjen.  Preservation of choice principles under realizability.  Logic Journal of the IGPL, 27(5):746–765, 02 2019.
  * [9] Solomon Feferman.  A language and axioms for explicit mathematics.  In Algebra and logic, pages 87–139. Springer, 1975.
  * [10] Solomon Feferman.  Recursion theory and set theory: a marriage of convenience.  In Generalized Recursion Theory II, Stud. Logic Found. Math., pages 55–98. North-Holland, Amsterdam, 1978.
  * [11] Solomon Feferman.  Constructive theories of functions and classes.  In Logic Colloquium ’78, Stud. Logic Found. Math., pages 159–224. North-Holland, Amsterdam, 1979.
  * [12] H. Friedman and A. Ščedrov.  Large sets in intuitionistic set theory.  Annals of Pure and Applied Logic, 27:1–24, 1984.
  * [13] Harvey Friedman.  The consistency of classical set theory relative to a set theory with intuitionistic logic.  Journal of Symbolic Logic, 38:315–319, 1973.
  * [14] Harvey Friedman.  Some applications of Kleene’s methods for intuitionistic systems.  In Cambridge summer school in mathematical logic, pages 113–170. Springer, 1973.
  * [15] Emanuele Frittaion.  On Goodman realizability.  Notre Dame J. Formal Logic, 60(3):523–550, 08 2019.
  * [16] Lew Gordeev.  Proof-theoretical analysis of weak systems of functions and classes.  Annals of Pure and Applied Logic, 38:1–121, 1988.
  * [17] R.J. Grayson.  Note on extensional realizability, 1981.  Handwritten notes from Münster University.
  * [18] G. Kreisel and A.S. Troelstra.  Formal systems for some branches of intuitionistic analysis.  Annals of Mathematical Logic, 1:229–387, 1970.
  * [19] David Charles McCarty.  Realizability and recursive mathematics.  Thesis (Ph.D.)–The University of Edinburgh, 1985.
  * [20] David Charles McCarty.  Realizability and recursive set theory.  Ann. Pure Appl. Logic, 32(2):153–183, 1986.
  * [21] Andrew M. Pitts.  The theory of triposes.  Thesis (Ph.D.)–University of Cambridge, 1981.
  * [22] Michael Rathjen.  Constructive set theory and Brouwerian principles.  J.UCS, 11(12):2008–2033, 2005.
  * [23] Michael Rathjen.  The disjunction and related properties for constructive Zermelo-Fraenkel set theory.  J. Symbolic Logic, 70(4):1232–1254, 2005.
  * [24] Michael Rathjen.  The formulae-as-classes interpretation of constructive set theory.  In Proof Technology and Computation, pages 279–322. IOS Press, Amsterdam, 2006.
  * [25] Michael Rathjen.  Realizability for constructive Zermelo-Fraenkel set theory.  In Logic Colloquium ’03, volume 24 of Lect. Notes Log., pages 282–314. Assoc. Symbol. Logic, La Jolla, CA, 2006.
  * [26] Michael Rathjen.  Metamathematical properties of intuitionistic set theories with choice principles.  In New computational paradigms, pages 287–312. Springer, New York, 2008.
  * [27] Moses Schönfinkel.  Über die Bausteine der mathematischen Logik.  Mathematische Annalen, 92:305–316, 1924.
  * [28] Andrew W. Swan.  CZF does not have the existence property.  Ann. Pure Appl. Logic, 165(5):1115–1147, 2014.
  * [29] Anne Troelstra and Dirk van Dalen.  Constructivism in Mathematics, volume II, volume 123 of Studies in Logic and the Foundations of Mathematics.  Elsevier B. V., Amsterdam, 1988.
  * [30] A.S. Troelstra.  Metamathematical investigation of intuitionistic arithmetic and analysis.  Lecture Notes in Mathematics, Vol. 344. Springer-Verlag, Berlin, 1973\.
  * [31] A.S. Troelstra.  A note on non-extensional operations in connection with continuity and recursiveness.  Indagationes Mathematicae (Proceedings), 80(5):455 – 462, 1977\.
  * [32] A.S. Troelstra.  Realizability.  In Handbook of proof theory, volume 137 of Stud. Logic Found. Math., pages 407–473. North-Holland, Amsterdam, 1998.
  * [33] Benno van den Berg and Lotte van Slooten.  Arithmetical conservation results.  Indag. Math. (N.S.), 29(1):260–275, 2018.
  * [34] Jaap van Oosten.  Extensional realizability.  Annals of Pure and Applied Logic, 84(3):317 – 349, 1997.
  * [35] Jaap van Oosten.  Realizability: an introduction to its categorical side, volume 152 of Studies in Logic and the Foundations of Mathematics.  Elsevier B. V., Amsterdam, 2008.