set which is extensionally equal to $\\{a\\}$ by Section 14.1 Finally, let

$b\coloneqq\\{(a^{n},\pi)\operatorname{\hskip 1.42271pt\mid\hskip
1.42271pt}n\in\omega,\pi\in\Pi\\}.$

Since $\\{a\\}\times\Pi\subseteq b$, $\lVert
a\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}b\rVert=\Pi$
and therefore $\textnormal{{I}}\Vdash a\mathop{\varepsilon}b$. Therefore, it
will suffice to prove that

$\lambda u\boldsymbol{.}u\textnormal{{I}}\Vdash\forall x(\forall
y(x\mathop{\varepsilon}y\rightarrow
y\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}b)\rightarrow
x\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}b).$

So, fix $c$ and suppose that we can find some $t$ and $\pi$ such that
$t\Vdash\forall y(c\mathop{\varepsilon}y\rightarrow
y\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}b)$ and
$\pi\in\lVert
c\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}b\rVert$. Note
that, by definition, $(c,\pi)\in b$. For our witness $y$ we shall take
$d=\\{c\\}\times\Pi$, noting that for any $\pi^{\prime}\in\Pi$, we shall have
that $(d,\pi^{\prime})\in b$.

We shall first prove that $\textnormal{{I}}\Vdash
c\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}d\rightarrow\perp$.
To do this suppose $s\Vdash
c\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}d$ and
$\sigma\in\Pi$. By definition, $\forall\tau\in\lVert
c\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}d\rVert=\\{\pi^{\prime}\operatorname{\hskip
1.42271pt\mid\hskip 1.42271pt}(c,\pi^{\prime})\in d\\}=\Pi$,
$s\star\tau\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$. Therefore,
$\textnormal{{I}}\star s\boldsymbol{.}\sigma\succ
s\star\sigma\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$, which completes this
observation. Then, since $\textnormal{{I}}\Vdash c\mathop{\varepsilon}d$,
$t\textnormal{{I}}\Vdash
d\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}b$ and thus,
$\lambda u\boldsymbol{.}u\textnormal{{I}}\star t\boldsymbol{.}\pi\succ
t\textnormal{{I}}\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$,
which completes the proof.

We can now conclude that our realizability model satisfies
$\operatorname{\textnormal{{ZF}}_{\varepsilon}}$.

Suppose that $\textnormal{{V}}\models\textnormal{{ZF}}$ and
$\mathcal{A}=(\Lambda,\Pi,\prec,\mathbin{\text{$\bot\mkern-11.0mu\bot$}})$ is
a realizability algebra. Then for every axiom $\varphi$ of
$\operatorname{\textnormal{{ZF}}_{\varepsilon}}$,
$\mathcal{N}^{\mathcal{A},\textnormal{{V}}}\Vdash\varphi$.

##  13 Names and Ordinals

###  13.1 Reish Names

In this short subsection we introduce a way to interpret every ground model
set in the realizability model, by defining the $\emph{reish of }a$, where
reish stands for _recursive_. In the traditional presentation where the sets
of the realizability model are all sets in the ground model, one considers the
gimel of $a$, $\text{\Large\cjRL{g}}(a)$, defined by
$\text{\Large\cjRL{g}}(a)\coloneqq a\times\Pi$. The issue with this operation
is that if $a$ is not a name in N, then in the extensional model
$\text{\Large\cjRL{g}}(a)$ may be very impoverished. Notably, if $a$ does not
contain any pair of the form $(b,\pi)$ where $\pi\in\Pi$ then one can easily
see that $\lVert\forall
x(x\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}a)\rVert=\emptyset$
from which it follows that in the extensional model $\Vdash a\simeq\emptyset$.
In particular, from this we can conclude that for any ordinal $\alpha$,
$\Vdash\forall x^{\text{\Large\cjRL{g}}(\alpha)}(x\simeq 0)$.

Instead, we shall consider $\text{\Large\cjRL{r}}({a})$ which is constructed
by applying the gimel process recursively to all elements of $a$. This is a
very blunt tool which in general will be difficult to work with because for
any $b\in a$,
$\lVert\text{\Large\cjRL{r}}({b})\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\text{\Large\cjRL{r}}({a})\rVert=\Pi$.
This will cause problems in practice because if $\pi\in\lVert\forall
x^{\text{\Large\cjRL{r}}({a})}\varphi(x)\rVert$ then we cannot specify the
$b\in a$ for which $\pi\in\lVert\varphi(\text{\Large\cjRL{r}}({b}))\rVert$.
Therefore, in order to have $t\Vdash\forall
x^{\text{\Large\cjRL{r}}({a})}\varphi(x)$ one needs $t$ to uniformly realize
$t\Vdash\varphi(\text{\Large\cjRL{r}}({b}))$ for all $b\in a$ without
reference to which witness we are working with. For example, it is not known
if it is possible to prove

$\forall n\mathop{\varepsilon}\text{\Large\cjRL{r}}({\omega})\,\forall
x((\forall
y(y+1\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}x\rightarrow
y\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}x)\rightarrow
n\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}x)\rightarrow\text{\Large\cjRL{r}}({0})\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}x),$

which would imply that every element of $\text{\Large\cjRL{r}}({\omega})$ was
an integer and therefore that $\text{\Large\cjRL{r}}({\omega})$ was
extensionaly equal to the first limit ordinal. However, it is a good starting
point to work from and we will consider an alternative approach in 13.3.

We define an interpretation $\text{\Large\cjRL{r}}({x})$ recursively for
$x\in\textnormal{{V}}$ as

$\text{\Large\cjRL{r}}({x})\coloneqq\\{(\text{\Large\cjRL{r}}({y}),\pi)\operatorname{\hskip
1.42271pt\mid\hskip 1.42271pt}y\in x,\,\pi\in\Pi\\}.$

If $a\subseteq b$ then
$\mathcal{N}\Vdash\text{\Large\cjRL{r}}({a})\subseteq\text{\Large\cjRL{r}}({b})$.

###### Proof.

Fix $t$ to be a realizer such that $t\Vdash\forall x(x\subseteq x)$ (for
example, see Section 11.1) and fix
$s\boldsymbol{.}\pi\in\lVert\text{\Large\cjRL{r}}({a})\subseteq\text{\Large\cjRL{r}}({b})\rVert=\bigcup_{c}\\{s\boldsymbol{.}\pi\operatorname{\hskip
1.42271pt\mid\hskip
1.42271pt}(\text{\Large\cjRL{r}}({c}),\pi)\in\text{\Large\cjRL{r}}({a}),s\Vdash\text{\Large\cjRL{r}}({c})\not\in\text{\Large\cjRL{r}}({b})\\}$.
Now, if $(\text{\Large\cjRL{r}}({c}),\pi)\in\text{\Large\cjRL{r}}({a})$, then
we must have that $c\in a$ and therefore $c\in b$. Thus,
$t\boldsymbol{.}t\boldsymbol{.}\pi\in\lVert\text{\Large\cjRL{r}}({c})\not\in\text{\Large\cjRL{r}}({b})\rVert$
which means that $s\star
t\boldsymbol{.}t\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$.
Thus, $\lambda
u\boldsymbol{.}(ut)t\Vdash\text{\Large\cjRL{r}}({a})\subseteq\text{\Large\cjRL{r}}({b})$.
∎

If $a\in b$ then
$\textnormal{{I}}\Vdash\text{\Large\cjRL{r}}({a})\mathop{\varepsilon}\text{\Large\cjRL{r}}({b})$.
Thus, if $a\in b$ then
$\mathcal{N}\Vdash\text{\Large\cjRL{r}}({a})\not\simeq\text{\Large\cjRL{r}}({b})$.

###  13.2 Ordinals

We now wish to discuss ordinals in
$\operatorname{\textnormal{{ZF}}_{\varepsilon}}$. In order to do this, we will
first specify precisely what we mean by this concept. For the purpose of this
section, we will be very careful to differentiate between the
$\mathop{\varepsilon}$ version and the $\in$ version of each definition.

($\operatorname{\textnormal{{ZF}}_{\varepsilon}}$) We say that a set $a$ is a
$\mathop{\varepsilon}$_-ordinal_ if it is a $\mathop{\varepsilon}$-transitive
set of $\mathop{\varepsilon}$-transitive sets. That is,

$\forall x\mathop{\varepsilon}a\,\forall
y\mathop{\varepsilon}x\,(y\mathop{\varepsilon}a)\quad\land\quad\forall
z\mathop{\varepsilon}a\,\forall x\mathop{\varepsilon}z\,\forall
y\mathop{\varepsilon}x\,(y\mathop{\varepsilon}z).$

Note that over $\operatorname{\textnormal{{ZF}}_{\varepsilon}}$,
$\mathop{\varepsilon}$-ordinals are not always the same as the standard
definition of ordinals as transitive sets well-ordered by the
$\mathop{\varepsilon}$-relation. For example, if $\text{\Large\cjRL{r}}({2})$
has size greater than 2 then there are two ordinals, $a$ and $b$, such that
$a\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}b$,
$b\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}a$ but
$(a\cup\\{a\\})\cup(b\cup\\{b\\})$ is an $\mathop{\varepsilon}$-ordinal on
which the $\mathop{\varepsilon}$-relation does not linearly order the set. On
the other hand, it is easy to see in ZF that $\alpha$ is an ordinal if and
only if it is a transitive set of transitive sets.

$(\operatorname{\textnormal{{ZF}}_{\varepsilon}})$

  1. i.

If $a$ is a $\mathop{\varepsilon}$-transitive set, then it is a
$\in$-transitive set.

  2. ii.

If $a$ is a $\mathop{\varepsilon}$-ordinal, then it is a $\in$-ordinal.

###### Proof.

Suppose that $a$ is a $\mathop{\varepsilon}$-transitive set and take $c\in
b\in a$. Then there exists some $x\mathop{\varepsilon}a$ such that $x\simeq b$
and there exists some $y\mathop{\varepsilon}x$ such that $y\simeq c$. Since
$a$ is assumed to be $\mathop{\varepsilon}$-transitive,
$y\mathop{\varepsilon}a$. Therefore $x\in a$ by definition of $\in$.

Next, suppose that $a$ is a $\mathop{\varepsilon}$-ordinal. We have already
shown that $a$ is $\in$-transitive, so it suffices to prove that every $b\in
a$ is $\in$-transitive. So let $d\in c\in b\in a$. Then we can find
$z\mathop{\varepsilon}y\mathop{\varepsilon}x\mathop{\varepsilon}a$ such that
$x\simeq b$, $y\simeq c$ and $z\simeq d$. Since $a$ is a
$\mathop{\varepsilon}$-ordinal, $z\mathop{\varepsilon}x$ and therefore $d\in
x$. Finally, $d\in x$ and $x\simeq b$ gives us $d\in b$, as required. ∎

There exists a realizer $\theta\in\mathcal{R}$ such that whenever $\delta$ is
an ordinal in V then $\theta\Vdash``\text{\Large\cjRL{r}}({\delta})\text{ is a
}\mathop{\varepsilon}\text{-ordinal''}$.

###### Proof.

Let $\delta$ be an ordinal in V. We shall show that
$\text{\Large\cjRL{r}}({\delta})$ is a $\mathop{\varepsilon}$-transitive set.
The fact that it consists of $\mathop{\varepsilon}$-transitive sets will
follow by a similar argument. To do this, we shall show that

$\textnormal{{I}}\Vdash\forall x^{\text{\Large\cjRL{r}}({\delta})}\forall
y(y\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\text{\Large\cjRL{r}}({\delta})\rightarrow
y\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}x).$

To do this, fix $\beta\in\delta$, $c\in\textnormal{{N}}$, $t\Vdash
c\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\text{\Large\cjRL{r}}({\delta})$
and $\pi\in\lVert
c\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\text{\Large\cjRL{r}}({\beta})\rVert$.
Now $\lVert
c\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\text{\Large\cjRL{r}}({\beta})\rVert=\\{\sigma\operatorname{\hskip
1.42271pt\mid\hskip 1.42271pt}(c,\sigma)\in\text{\Large\cjRL{r}}({\beta})\\}$.
So, since this set is non-empty, it must be the case that $\lVert
c\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\text{\Large\cjRL{r}}({\beta})\rVert=\Pi$
and $c=\text{\Large\cjRL{r}}({\gamma})$ for some $\gamma\in\beta$. Therefore,
$\lVert
c\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\text{\Large\cjRL{r}}({\delta})\rVert=\lVert\text{\Large\cjRL{r}}({\gamma})\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\text{\Large\cjRL{r}}({\delta})\rVert=\Pi$
and therefore $t\star\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$, from
which the result follows. ∎

###  13.3 Ordinal Representations

We now present an alternative method to represent certain ordinals in the
realizability model which will give a much more usable interpretation. This
interpretation will give a representation for every ordinal less than the size
of the realizability model. This method is explored in much more detail in
[FG20] where it was shown that the objects in the realizability model named by
these ordinals behave like their ground model counterparts.

Let
$\mathcal{A}=(\Lambda_{(A,B)},\Pi_{(A,B)},\prec,\mathbin{\text{$\bot\mkern-11.0mu\bot$}})$
be a realizability algebra where $|A|=\kappa$ is infinite and $|B|\leq\kappa$
and let $(\nu_{\alpha}\operatorname{\hskip 1.42271pt\mid\hskip
1.42271pt}\alpha\in\kappa)$ be an enumeration of $\Lambda$. Without loss of
generality, we can assume that for every $n\in\omega$, $\nu_{n}=\underline{n}$
with just the small caveat that if $\kappa=\omega$ then this will in fact be
an enumeration of order type $\omega+\omega$ rather than $|\Lambda|$.

For $\alpha\in\kappa$, let
$\hat{\alpha}\coloneqq\\{(\hat{\beta},\nu_{\beta}\boldsymbol{.}\pi)\operatorname{\hskip
1.42271pt\mid\hskip 1.42271pt}\pi\in\Pi,\beta\in\alpha\\}$.

The precise ordering for the term structure does not matter, what is important
is that we have a way to “decode” which element of $\hat{\alpha}$ we have
picked. Namely, if $\lVert
x\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\hat{\alpha}\rVert\neq\emptyset$
then it must be of the form
$\\{\nu_{\beta}\boldsymbol{.}\pi\operatorname{\hskip 1.42271pt\mid\hskip
1.42271pt}\pi\in\Pi\\}$ for some $\beta\in\alpha$ and therefore our falsity
value tells us which element of $\hat{\alpha}$ our $x$ is meant to correspond
to.

If $\beta<\alpha\leq\kappa$ then $\lambda
u\boldsymbol{.}u\nu_{\beta}\Vdash\hat{\beta}\mathop{\varepsilon}\hat{\alpha}$.

###### Proof.

Suppose that
$t\Vdash\hat{\beta}\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\hat{\alpha}$
and $\pi\in\Pi$. Then, by definition, we have that
$\nu_{\beta}\boldsymbol{.}\pi\in\lVert\hat{\beta}\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\hat{\alpha}\rVert$
from which it follows that $\lambda u\boldsymbol{.}u\nu_{\beta}\star
t\boldsymbol{.}\pi\succ t\nu_{\beta}\star\pi\succ
t\star\nu_{\beta}\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$.
∎

Recall Section 10.1 where we defined the restricted quantifier $\forall x^{a}$
to have the falsity value

$\lVert\forall x^{a}\varphi(x)\rVert=\\{\pi\operatorname{\hskip
1.42271pt\mid\hskip 1.42271pt}\exists
b\in\textnormal{{dom}}(a)\,\pi\in\lVert\varphi(b)\rVert\\}$

and then proved that this behaves as a restricted quantifier in certain cases.
Here we want to modify the definition of the restricted quantifier to take
into account the $\nu_{\alpha}$. In order to ease notation we shall use the
same notation for both these notions and note that it will always be clear
from the context which of these interpretations we are using.

For $\alpha\leq\kappa$, we define the restricted quantifier $\forall
x^{\hat{\alpha}}$ to have the following meaning:

$\lVert\forall
x^{\hat{\alpha}}\varphi(x)\rVert=\bigcup_{\beta\in\alpha}\\{\nu_{\beta}\boldsymbol{.}\pi\operatorname{\hskip
1.42271pt\mid\hskip 1.42271pt}\pi\in\lVert\varphi(\hat{\beta})\rVert\\}.$

As before, we can see that this behaves as the bounded quantifier.

For every $\alpha\leq\kappa$,

  1. i.

$\lambda u\boldsymbol{.}\lambda v\boldsymbol{.}\lambda
w\boldsymbol{.}v(uw)\Vdash\forall
x^{\hat{\alpha}}\,\varphi(x)\rightarrow\forall x(\neg\varphi(x)\rightarrow
x\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\hat{\alpha})$;

  2. ii.

$\lambda u\boldsymbol{.}\textnormal{{{cc}}}\,u\Vdash\forall
x(\neg\varphi(x)\rightarrow
x\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\hat{\alpha})\rightarrow\forall
x^{\hat{\alpha}}\,\varphi(x)$.

###### Proof.

$(i)$. Suppose that $t\Vdash\forall x^{\hat{\alpha}}\,\varphi(x)$,
$s\Vdash\neg\varphi(b)$ for some $b\in\textnormal{{N}}$ and $\pi\in\lVert
b\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\hat{\alpha}\rVert$.
Since $\lVert
b\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\hat{\alpha}\rVert=\\{\sigma\operatorname{\hskip
1.42271pt\mid\hskip 1.42271pt}(b,\sigma)\in\hat{\alpha}\\}$ and this is non-
empty by assumption, we must have that $b=\hat{\beta}$ for some
$\beta\in\alpha$ and $\pi=\nu_{\beta}\boldsymbol{.}\pi^{\prime}$ for some
$\pi^{\prime}\in\Pi$. We need to prove that $\lambda u\boldsymbol{.}\lambda
v\boldsymbol{.}\lambda w\boldsymbol{.}v(uw)\star
t\boldsymbol{.}s\boldsymbol{.}\nu_{\beta}\boldsymbol{.}\pi^{\prime}\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$
or, in other words, that
$s\star(t\nu_{\beta})\boldsymbol{.}\pi^{\prime}\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$.
By the hypothesis on $t$, since $\beta\in\alpha$,
$t\star\nu_{\beta}\boldsymbol{.}\sigma\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$
for any $\sigma\in\lVert\varphi(\hat{\beta})\rVert$. Therefore, this gives us
that $t\nu_{\beta}\Vdash\varphi(\hat{\beta})$. Finally, since
$s\Vdash\varphi(\hat{\beta})\rightarrow\perp$, $s\star
t\nu_{\beta}\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$ as
desired.

$(ii)$. Suppose that $t\Vdash\forall x(\neg\varphi(x)\rightarrow
x\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\hat{\alpha})$
and $\sigma\in\lVert\forall x^{\hat{\alpha}}\,\varphi(x)\rVert$. First, fix
$\beta\in\alpha$ and $\pi\in\Pi$ such that
$\sigma=\nu_{\beta}\boldsymbol{.}\pi\in\lVert\varphi(\hat{\beta})\rVert$. Now

$\lVert\forall x(\neg\varphi(x)\rightarrow
x\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\hat{\alpha})\rVert=\bigcup_{c\in\textnormal{{N}}}\lVert\neg\varphi(c)\rightarrow
c\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\hat{\alpha}\rVert=\bigcup_{\gamma\in\alpha}\\{s\boldsymbol{.}\nu_{\gamma}\boldsymbol{.}\sigma\operatorname{\hskip
1.42271pt\mid\hskip
1.42271pt}s\Vdash\neg\varphi(\hat{\gamma}),\nu_{\gamma}\boldsymbol{.}\sigma\in\lVert\hat{\gamma}\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\hat{\alpha}\rVert\\}.$

Therefore, for any $s\boldsymbol{.}\nu_{\gamma}\boldsymbol{.}\sigma$ in the
above set, $t\star
s\boldsymbol{.}\nu_{\gamma}\boldsymbol{.}\sigma\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$.
Next, since $\nu_{\beta}\boldsymbol{.}\pi\in\lVert\varphi(\hat{\beta})\rVert$,
$\textnormal{{k}}_{\nu_{\beta}\boldsymbol{.}\pi}\Vdash\neg\varphi(\hat{\beta})$
by Section 9. Thus,
$\textnormal{{k}}_{\nu_{\beta}\boldsymbol{.}\pi}\boldsymbol{.}\nu_{\beta}\boldsymbol{.}\pi\in\lVert\forall
x(\neg\varphi(x)\rightarrow
x\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\hat{\alpha})\rVert$
and
$t\star\textnormal{{k}}_{\nu_{\beta}\boldsymbol{.}\pi}\boldsymbol{.}\nu_{\beta}\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$.
Finally, the result follows by evaluating the realizer in the proposition:

$\lambda u\boldsymbol{.}\textnormal{{{cc}}}\,u\star
t\boldsymbol{.}\nu_{\beta}\boldsymbol{.}\pi\succ\textnormal{{{cc}}}\,t\star\nu_{\beta}\boldsymbol{.}\pi\succ\textnormal{{{cc}}}\star
t\boldsymbol{.}\nu_{\beta}\boldsymbol{.}\pi\succ
t\star\textnormal{{k}}_{\nu_{\beta}\boldsymbol{.}\pi}\boldsymbol{.}\nu_{\beta}\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}.$

∎

There exists a realizer $\theta\in\mathcal{R}$ such that for every
$\alpha\leq\kappa$,

$\theta\Vdash``\hat{\alpha}\text{ is a
}\mathop{\varepsilon}\text{-ordinal''}.$

###### Proof.

As in the case for $\text{\Large\cjRL{r}}({\alpha})$ we shall show that
$\hat{\alpha}$ is a $\mathop{\varepsilon}$-transitive set. The fact that it
consists of $\mathop{\varepsilon}$-transitive sets will follow by a similar
argument. To do this, we shall show that

$\lambda v\boldsymbol{.}\lambda w\boldsymbol{.}\lambda
k\boldsymbol{.}w(\lambda u\boldsymbol{.}uk)\Vdash\forall
x^{\hat{\alpha}}\forall
y(y\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\hat{\alpha}\rightarrow
y\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}x).$

First, observe that $\lVert\forall x^{\hat{\alpha}}\forall
y(y\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\hat{\alpha}\rightarrow
y\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}x)\rVert=\bigcup_{\beta\in\alpha}\bigcup_{\gamma\in\beta}\\{\nu_{\beta}\boldsymbol{.}t\boldsymbol{.}\nu_{\gamma}\boldsymbol{.}\pi\operatorname{\hskip
1.42271pt\mid\hskip
1.42271pt}t\Vdash\hat{\gamma}\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\hat{\alpha},\,\pi\in\Pi\\}$.
So, fix $\gamma<\beta<\alpha$, $\pi\in\Pi$ and
$t\Vdash\hat{\gamma}\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\hat{\alpha}$.
Since $\gamma\in\alpha$, by Section 13.3, $\lambda
u\boldsymbol{.}u\nu_{\gamma}\Vdash\hat{\gamma}\mathop{\varepsilon}\hat{\alpha}$
and therefore

$\lambda v\boldsymbol{.}\lambda w\boldsymbol{.}\lambda
k\boldsymbol{.}w(\lambda
u\boldsymbol{.}uk)\star\nu_{\beta}\boldsymbol{.}t\boldsymbol{.}\nu_{\gamma}\boldsymbol{.}\pi\succ
t(\lambda u\boldsymbol{.}u\nu_{\gamma})\star\pi\succ t\star(\lambda
u\boldsymbol{.}u\nu_{\gamma})\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}.$

∎

A key difference between $\mathop{\varepsilon}$-ordinals and $\in$-ordinals is
the principle of _trichotomy_ ; for any $\in$-ordinal $\alpha$, if
$\beta,\gamma\in\alpha$ then either $\beta\in\gamma$, $\gamma\in\beta$ or
$\beta\simeq\gamma$. We end this section with a discussion of
$\mathop{\varepsilon}$-ordinals which satisfy
$\mathop{\varepsilon}$_-trichotomy_. Such ordinals are particularly useful
because they have a much richer structure within the non-extensional language.
For example, we shall see that such ordinals contain unique representatives of
their $\in$-elements and satisfy the _Least Ordinal Principle_ ; if $X$ is a
non-empty subset of $\hat{\alpha}$ then $X$ has a $\mathop{\varepsilon}$-least
element. To ease notation it is useful to add in the symbol
$\subseteq_{\mathop{\varepsilon}}$ for non-extensional subsets.

$(\operatorname{\textnormal{{ZF}}_{\varepsilon}})$
$a\subseteq_{\mathop{\varepsilon}}b$ is an abbreviation for the formula
$\forall x(x\mathop{\varepsilon}a\rightarrow x\mathop{\varepsilon}b)$.

$(\operatorname{\textnormal{{ZF}}_{\varepsilon}})$ We say that a
$\mathop{\varepsilon}$-ordinal $a$ is $\mathop{\varepsilon}$_-Trichotomous_ if

$\forall x\mathop{\varepsilon}a\forall
y\mathop{\varepsilon}a(x\mathop{\varepsilon}y\lor x=y\lor
y\mathop{\varepsilon}x).$

$\operatorname{\textnormal{{ZF}}_{\varepsilon}}\vdash\forall a(a\text{ is a
}\mathop{\varepsilon}\text{-Trichotomous ordinal }\rightarrow\forall
x\mathop{\varepsilon}a\forall y\mathop{\varepsilon}a(x\simeq y\rightarrow
x=y)).$

###### Proof.

Suppose that $a$ is a $\mathop{\varepsilon}$-Trichotomous ordinal and fix
$x,y\mathop{\varepsilon}a$ such that $x\neq y$. Then, by trichotomy, we must
have that either $x\mathop{\varepsilon}y$ or $y\mathop{\varepsilon}x$ from
which it follows that either $x\in y$ or $y\in x$. But, from either of these
cases it follows that $x\not\simeq y$, otherwise we would obtain the
contradictory statement $x\in x$. ∎

[Least Ordinal Principle]

$\operatorname{\textnormal{{ZF}}_{\varepsilon}}\vdash\forall a\forall
X(a\text{ is a }\mathop{\varepsilon}\text{-Trichotomous ordinal }\land
X\subseteq_{\mathop{\varepsilon}}a\land\exists z(z\mathop{\varepsilon}X)\\\
\longrightarrow\quad\exists z\mathop{\varepsilon}X\forall
y\mathop{\varepsilon}X(z\mathop{\varepsilon}y\lor z=y)).$

###### Proof.

Suppose that $a$ is a $\mathop{\varepsilon}$-Trichotomous ordinal and fix
$X\subseteq_{\mathop{\varepsilon}}a$ such that $\exists
z(z\mathop{\varepsilon}X)$. Using $\in$-Foundation (which follows classically
from $\in$-Induction) we can fix $z\mathop{\varepsilon}X$ such that $z\cap
X\simeq\emptyset$, that is $\forall y\neg(y\in z\land y\in X)$. To see that
this $z$ witnesses the claim, by trichotomy it suffices to show that $\forall
y\mathop{\varepsilon}X(y\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}z)$.
But, if $y\mathop{\varepsilon}X$ then $y\in X$ and therefore $y\not\in z$ by
$\in$-minimality of $z$. Thus,
$y\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}z$. ∎

One would like to show that for any $\alpha\in\kappa$, $\hat{\alpha}$ is a
trichotomous $\mathop{\varepsilon}$-ordinal. However, in order to do that we
need to add a special instruction, $\chi$, which allows one to compare the
indices of ordinals. This is done in section 3 of [FG20].

Let $\chi\in\Lambda$ be a special instruction. We extend the order $\prec$ to
be the smallest pre-order on $\Lambda\star\Pi$ such that for any
$\alpha,\beta\in\kappa$, $t,s,r\in\Lambda$ and $\pi\in\Pi$,

$\chi\star\nu_{\alpha}\boldsymbol{.}\nu_{\beta}\boldsymbol{.}t\boldsymbol{.}s\boldsymbol{.}r\boldsymbol{.}\pi\succ\begin{cases}t\star\pi&\text{if
}\ \alpha<\beta,\\\ s\star\pi&\text{if }\ \alpha=\beta,\\\ r\star\pi&\text{if
}\ \beta<\alpha.\end{cases}$

Suppose that $\chi\in\Lambda$ and $\prec$ has been expanded to satisfy Section
13.3. Then there exists a realizer $\theta\in\mathcal{R}$ such that for every
$\alpha\leq\kappa$,

$\theta\Vdash``\hat{\alpha}\text{ is a
}\mathop{\varepsilon}\text{-Trichotomous ordinal''}.$

###### Proof.

It will suffice to show that

$\lambda b\boldsymbol{.}\lambda c\boldsymbol{.}\lambda u\boldsymbol{.}\lambda
v\boldsymbol{.}\lambda w\boldsymbol{.}((((\chi b)c)(ub))(v))(wc)\Vdash\forall
x^{\hat{\alpha}}\,\forall
y^{\hat{\alpha}}(x\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}y\rightarrow(x\neq
y\rightarrow(y\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}x\rightarrow\perp))).$

Fix $\beta,\gamma\in\kappa$ and set $\eta=\lambda u\boldsymbol{.}\lambda
v\boldsymbol{.}\lambda
w\boldsymbol{.}((((\chi\nu_{\beta})\nu_{\gamma})(u\nu_{\beta}))(v))(w\nu_{\gamma})$.
Fix $\beta,\gamma\in\kappa$,
$t\Vdash\hat{\beta}\mathop{\varepsilon}\hat{\gamma}$,
$s\Vdash\hat{\beta}\neq\hat{\gamma}$,
$r\Vdash\hat{\gamma}\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\hat{\beta}$
and $\pi\in\Pi$. If $\beta<\gamma$ then $\eta\star
t\boldsymbol{.}s\boldsymbol{.}r\boldsymbol{.}\pi\succ
t\nu_{\beta}\star\pi\succ
t\star\nu_{\beta}\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$
since $(\hat{\beta},\nu_{\beta}\boldsymbol{.}\pi)\in\hat{\gamma}$. Similarly,
if $\gamma<\beta$ then $\eta\star
t\boldsymbol{.}s\boldsymbol{.}r\boldsymbol{.}\pi\succ
r\star\nu_{\gamma}\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$.
Finally, if $\beta=\gamma$ then $\lVert\hat{\beta}\neq\hat{\gamma}\rVert=\Pi$
and therefore, $\eta\star
t\boldsymbol{.}s\boldsymbol{.}r\boldsymbol{.}\pi\succ
s\star\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$. ∎

If one restricts $\chi$ to only comparing indices of Church numbers then
$\chi$ can in fact be constructed as a $\lambda$-term without the need for
special instructions (see Section 21 for the details). From this it follows
that $\hat{\omega}$ is always a $\mathop{\varepsilon}$-Trichotomous ordinal.

It is further shown in [FG20] that any realizability model $\mathcal{N}$
satisfies “$\hat{n}$ is the $n$th ordinal” and “$\hat{\omega}$ is the first
limit ordinal”.

##  14 Implementing Pairing

The next problem we want to address is how to discuss functions in the
realizability model. There are two main issues associated with this problem;
what do we mean by a function, and given a function in the ground model is it
possible to “lift” it to a function in the realizability model. A very typical
example of the question of lifting is when given a function $1_{E}\colon
a\rightarrow 2$ defined by $1_{E}(x)=1$ if $x\in E$ and $1_{E}(x)=0$
otherwise. The lifting of such functions to $\mathcal{N}$, in particular the
trivial Boolean algebra operations on $\\{0,1\\}$, are used to prove
statements about the Boolean algebra $\text{\Large\cjRL{r}}({2})$. In order to
address these problems, we first need a method to implement unordered and
ordered pairs.

Traditionally, the ordered pair of two sets $a$ and $b$, $(a,b)$, is defined
to be $\\{\\{a,b\\},\\{a\\}\\}$. However, this turns out to be a difficult
definition to encode because of the difficulty in using disjunctions in the
realizability model. Instead we shall first give an encoding for unordered
pairs which uses the two distinct $\lambda_{c}$-terms $\underline{0}$ and
$\underline{1}$ to distinguish the elements of the pairs. Then we shall
implement Wiener’s definition of ordered pairs, which is
$\\{\\{\\{a\\},\emptyset\\},\\{\\{b\\}\\}\\}$. This will turn out to work
because it will assign different structures to $a$ from $b$, allowing us to
identify which one is which. Note that the specific coding mechanism used is
not important because internally within our realizability models we could
easily move between different implementations of ordered pairs.

###  14.1 Unordered Pairs

We begin with Krivine’s implementation of singletons in the realizability
model from [Kri12]. After this we will give an implementation of unordered
pairs. Recall that in the proof of Pairing in $\mathcal{N}$ the name for the
pair of the sets $a$ and $b$ was $\\{a,b\\}\times\Pi$, however it will turn
out to be beneficial to take a different implementation in order to be able to
distinguish
$a\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\\{a,b\\}$
from
$b\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\\{a,b\\}$.

For $a\in\textnormal{{N}}$, $\textnormal{{sng}}(a)\coloneqq\\{a\\}\times\Pi$.

The following are realizable in $\mathcal{N}$:

  1. i.

$\forall x\forall
y(\textnormal{{sng}}(x)=\textnormal{{sng}}(y)\xhookrightarrow{}x=y)$;

  2. ii.

$\forall x(\textnormal{{sng}}(x)\not\simeq\text{\Large\cjRL{r}}({0}))$;

  3. iii.

$\forall x\forall y(x\in\textnormal{{sng}}(y)\rightarrow x\simeq y)$;

  4. iv.

$\forall x\forall y(x\simeq
y\rightarrow\textnormal{{sng}}(x)\simeq\textnormal{{sng}}(y))$;

  5. v.

$\forall x\forall
y(\textnormal{{sng}}(x)\simeq\textnormal{{sng}}(y)\rightarrow x\simeq y)$.

###### Proof.

  1. i.

Fix $a,b\in\textnormal{{N}}$, we shall prove that
$\textnormal{{I}}\Vdash\textnormal{{sng}}(a)=\textnormal{{sng}}(b)\xhookrightarrow{}a=b$.
If $\textnormal{{sng}}(a)\neq\textnormal{{sng}}(b)$ then
$\lVert\textnormal{{sng}}(a)=\textnormal{{sng}}(b)\xhookrightarrow{}a=b\rVert=\emptyset$
and the result trivially follows. So suppose that
$\textnormal{{sng}}(a)=\textnormal{{sng}}(b)$. Then we obviously have that
$a=b$ and thus
$\lVert\textnormal{{sng}}(a)=\textnormal{{sng}}(b)\xhookrightarrow{}a=b\rVert=\lVert
a=b\rVert=\\{t\boldsymbol{.}\pi\operatorname{\hskip 1.42271pt\mid\hskip
1.42271pt}\pi\in\Pi,\,\forall\sigma\in\Pi(t\star\sigma\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}})\\}$.
Therefore, I realizes the desired statement.

  2. ii.

Fix $a\in\textnormal{{N}}$, it will suffice to prove that $\lambda
u\boldsymbol{.}u\textnormal{{I}}\Vdash\textnormal{{sng}}(a)\subseteq\text{\Large\cjRL{r}}({0})\rightarrow\perp$.
So suppose that
$t\Vdash\textnormal{{sng}}(a)\subseteq\text{\Large\cjRL{r}}({0})$ and
$\pi\in\Pi$. Then, by the proof of Extensionality from Section 12, we have
that $t\Vdash\forall z(z\not\in\text{\Large\cjRL{r}}({0})\rightarrow
z\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\textnormal{{sng}}(a))$.
By Section 10.1, this in particular gives $t\Vdash
a\not\in\text{\Large\cjRL{r}}({0})\rightarrow
a\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\textnormal{{sng}}(a)$.
Now $\lVert
a\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\textnormal{{sng}}(a)\rVert=\Pi$
while $\lVert a\not\in\text{\Large\cjRL{r}}({0})\rVert=\emptyset$, because
$\text{\Large\cjRL{r}}({0})=\emptyset$. Thus
$t\star\textnormal{{I}}\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$,
and the result follows.

  3. iii.

Fix $a,b\in\textnormal{{N}}$. It will suffice to prove that

$\textnormal{{I}}\Vdash a\not\simeq b\rightarrow
a\not\in\textnormal{{sng}}(b).$

So suppose that $t\Vdash a\not\simeq b$ and $\pi\in\lVert
a\not\in\textnormal{{sng}}(b)\rVert$. Then
$\pi=s\boldsymbol{.}s^{\prime}\boldsymbol{.}\sigma$ where
$(b,\sigma)\in\textnormal{{sng}}(b)$, $s\Vdash a\subseteq b$ and
$s^{\prime}\Vdash b\subseteq a$. But this gives us that $t\star
s\boldsymbol{.}s^{\prime}\boldsymbol{.}\sigma\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$
and thus $\textnormal{{I}}\star t\boldsymbol{.}\pi$ is also in
$\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$.

  4. iv.

Fix $a,b\in\textnormal{{N}}$, it will suffice to prove that

$\lambda u\boldsymbol{.}\lambda v\boldsymbol{.}\lambda
w\boldsymbol{.}(wu)v\Vdash a\subseteq b\rightarrow(b\subseteq
a\rightarrow(\textnormal{{sng}}(a)\subseteq\textnormal{{sng}}(b))).$

To do this, suppose that $t\Vdash a\subseteq b$, $s\Vdash b\subseteq a$,
$(c,\pi)\in\textnormal{{sng}}(a)$ and $r\Vdash c\not\in\textnormal{{sng}}(b)$.
Since $\textnormal{{sng}}(a)=\\{a\\}\times\Pi$, we must have that $c=a$ and
therefore $r\Vdash a\not\in\textnormal{{sng}}(b)$. However, since
$(b,\pi)\in\textnormal{{sng}}(b)$, $t\boldsymbol{.}s\boldsymbol{.}\pi\in\lVert
a\not\in\textnormal{{sng}}(b)\rVert$. Thus, $r\star
t\boldsymbol{.}s\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$,
completing the proof.

  5. v.

Fix $a,b\in\textnormal{{N}}$, it will suffice to show that

$\lambda
u\boldsymbol{.}\textnormal{{{cc}}}\,u\Vdash\textnormal{{sng}}(a)\subseteq\textnormal{{sng}}(b)\rightarrow
a\subseteq b.$

We also note that a very similar argument could be used to show that
$\textnormal{{sng}}(a)\subseteq\textnormal{{sng}}(b)\rightarrow b\subseteq a$
is also realizable.

So, fix $t\Vdash\textnormal{{sng}}(a)\subseteq\textnormal{{sng}}(b)$ and
$\pi\in\lVert a\subseteq b\rVert$. Then $t\Vdash\forall
z(z\not\in\textnormal{{sng}}(b)\rightarrow
z\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\textnormal{{sng}}(a))$
so, in particular, $t\Vdash a\not\in\textnormal{{sng}}(b)\rightarrow
a\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\textnormal{{sng}}(a)$.
Now, by definition, $\lVert a\not\in\textnormal{{sng}}(b)\rVert=$ $\lVert
a\subseteq b\rightarrow(b\subseteq a\rightarrow
b\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\textnormal{{sng}}(b))\rVert$.
But, by Section 9, $\textnormal{{k}}_{\pi}\Vdash a\subseteq
b\rightarrow(b\subseteq a\rightarrow
b\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\textnormal{{sng}}(b))$
and therefore $\textnormal{{{cc}}}\,t\star\pi\succ\textnormal{{{cc}}}\star
t\boldsymbol{.}\pi\succ
t\star\textnormal{{k}}_{\pi}\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$.

∎

Let $a,b\in\textnormal{{N}}$. The _unordered pair_ of $a$ and $b$,
$\textnormal{{up}}(a,b)$, is

$\textnormal{{up}}(a,b)\coloneqq\\{(a,\underline{0}\boldsymbol{.}\pi)\operatorname{\hskip
1.42271pt\mid\hskip
1.42271pt}\pi\in\Pi\\}\cup\\{(b,\underline{1}\boldsymbol{.}\pi)\operatorname{\hskip
1.42271pt\mid\hskip 1.42271pt}\pi\in\Pi\\}.$

We next show that up satisfies many of the basic properties one would expect
an unordered pair to have in the realizability model. Namely; it is well-
defined with respect to non-extensional equality, extensionally the ordered
pair of $a$ and $b$ is the same as that of $b$ and $a$, and if $z$ is in the
unordered pair of $a$ and $b$ then $z$ is either extensionally equal to $a$ or
to $b$.

The following are realizable in $\mathcal{N}$:

  1. i.

$\forall x_{1}\forall x_{2}\forall y_{1}\forall
y_{2}(\textnormal{{up}}(x_{1},y_{1})=\textnormal{{up}}(x_{2},y_{2})\xhookrightarrow{}(x_{1}=x_{2}\land
y_{1}=y_{2}))$;

  2. ii.

$\forall x\forall y\forall
z(z\mathop{\varepsilon}\textnormal{{up}}(x,y)\rightarrow
z\mathop{\varepsilon}\textnormal{{up}}(y,x))$;

  3. iii.

$\forall x\forall y(\textnormal{{up}}(x,y)\simeq\textnormal{{up}}(y,x))$;

  4. iv.

$\forall x\forall y\forall z(z\in\textnormal{{up}}(x,y)\rightarrow(z\not\simeq
y\rightarrow z\simeq x))$.

###### Proof.

  1. i.

For the first claim, fix $a_{1},a_{2},b_{1}$ and $b_{2}$ in N. If
$\textnormal{{up}}(a_{1},b_{1})\neq\textnormal{{up}}(a_{2},b_{2})$ then

$\lVert\textnormal{{up}}(a_{1},b_{1})=\textnormal{{up}}(a_{2},b_{2})\xhookrightarrow{}(a_{1}=a_{2}\land
b_{1}=b_{2})\rVert=\emptyset$

and the result trivially follows. So suppose that
$\textnormal{{up}}(a_{1},b_{1})=\textnormal{{up}}(a_{2},b_{2})$. Then it is
obviously the case that $a_{1}=a_{2}$ and $b_{1}=b_{2}$ and thus
$\textnormal{{I}}\Vdash a_{1}=b_{1}$ and $\textnormal{{I}}\Vdash a_{2}=b_{2}$,
from which the result follows.

  2. ii.

Fix $a,b$ and $c$ in N. We shall show that a realizer for the second statement
is $\lambda u\boldsymbol{.}\lambda i\boldsymbol{.}\big{(}i(\lambda
v\boldsymbol{.}u\underline{0})\big{)}\big{(}u\underline{1}\big{)}$. So,
suppose that $t\Vdash c\mathop{\varepsilon}\textnormal{{up}}(a,b)$ and
$(c,\underline{i}\boldsymbol{.}\pi)\in\textnormal{{up}}(b,a)$. Then either
$i=0$ and $c=b$ or $i=1$ and $c=a$. In the first case we have
$t\star\underline{1}\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$
while in the second case
$t\star\underline{0}\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$.
The conclusion then follows from the verification that

$\big{(}\underline{0}(\lambda
v\boldsymbol{.}t\underline{0})\big{)}\big{(}t\underline{1}\big{)}\star\pi\succ
t\star\underline{1}\boldsymbol{.}\pi$ and $\big{(}\underline{1}(\lambda
v\boldsymbol{.}t\underline{0})\big{)}\big{(}t\underline{1}\big{)}\star\pi\succ
t\star\underline{0}\boldsymbol{.}\pi$.

  3. iii.

The third claim follows from the second claim alongside the observation that,
in $\operatorname{\textnormal{{ZF}}_{\varepsilon}}$, $\forall a\forall
x(x\mathop{\varepsilon}a\rightarrow x\in a)$.

  4. iv.

For the final claim, fix $a,b$ and $c$ in N, $t\Vdash
c\not\in\textnormal{{up}}(a,b)\rightarrow\perp$, $s\Vdash c\simeq
b\rightarrow\perp$ and $\pi\in\lVert c\simeq a\rVert$. We shall show that

$\theta_{1}\coloneqq\lambda e_{t}\boldsymbol{.}\lambda
e_{s}\boldsymbol{.}cc\,(\lambda e_{k}\boldsymbol{.}e_{t}\theta_{0})$

is a realizer for the desired statement, where

$\theta_{0}\coloneqq\lambda e_{q}\boldsymbol{.}\lambda
e_{r}\boldsymbol{.}\lambda i\boldsymbol{.}(((i\lambda
w\boldsymbol{.}e_{s})e_{k})e_{q})e_{r}$

will give a realizer for $c\not\in\textnormal{{up}}(a,b)$. To do this, first
observe that $\textnormal{{k}}_{\pi}\Vdash c\simeq a\rightarrow\perp$. Now,
any element of $\lVert c\not\in\textnormal{{up}}(a,b)\rVert$ is either of the
form $q\boldsymbol{.}r\boldsymbol{.}\underline{0}\boldsymbol{.}\sigma$, where
$q\Vdash c\subseteq a$ and $r\Vdash a\subseteq c$ or of the form
$q\boldsymbol{.}r\boldsymbol{.}\underline{1}\boldsymbol{.}\sigma$, where
$q\Vdash c\subseteq b$ and $r\Vdash b\subseteq c$. In the first case, we have
that $\textnormal{{k}}_{\pi}\star
q\boldsymbol{.}r\boldsymbol{.}\sigma\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$
while in the second $s\star
q\boldsymbol{.}r\boldsymbol{.}\sigma\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$.
Next,

$\displaystyle\theta_{0}[e_{s}\coloneqq
s,e_{k}\coloneqq\textnormal{{k}}_{\pi}]\star
q\boldsymbol{.}r\boldsymbol{.}\underline{0}\boldsymbol{.}\sigma$
$\displaystyle\succ(((\underline{0}\lambda
w\boldsymbol{.}s)\textnormal{{k}}_{\pi})q)r\star\sigma$
$\displaystyle\succ\lambda u\boldsymbol{.}\lambda
v\boldsymbol{.}v\star(\lambda
w\boldsymbol{.}s)\boldsymbol{.}\textnormal{{k}}_{\pi}\boldsymbol{.}q\boldsymbol{.}r\boldsymbol{.}\sigma\succ\textnormal{{k}}_{\pi}\star
q\boldsymbol{.}r\boldsymbol{.}\sigma.$

Similarly, since $\underline{1}=\lambda u\boldsymbol{.}\lambda
v\boldsymbol{.}u(v)$, $\theta_{0}[e_{s}\coloneqq
s,e_{k}\coloneqq\textnormal{{k}}_{\pi}]\star
q\boldsymbol{.}r\boldsymbol{.}\underline{1}\boldsymbol{.}\sigma\succ s\star
q\boldsymbol{.}r\boldsymbol{.}\sigma$. Thus, we have that
$\theta_{0}[e_{s}\coloneqq s,e_{k}\coloneqq\textnormal{{k}}_{\pi}]\Vdash
c\not\in\textnormal{{up}}(a,b)$ which means that
$t\star\theta_{0}[e_{s}\coloneqq
s,e_{k}\coloneqq\textnormal{{k}}_{\pi}]\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$.
Finally,

$\theta_{1}\star
t\boldsymbol{.}s\boldsymbol{.}\pi\succ\textnormal{{{cc}}}\star(\lambda
e_{k}\boldsymbol{.}t\theta_{0}[e_{s}\coloneqq s])\boldsymbol{.}\pi\succ\lambda
e_{k}\boldsymbol{.}t\theta_{0}[e_{s}\coloneqq
s]\star\textnormal{{k}}_{\pi}\boldsymbol{.}\pi\succ
t\star\theta_{0}[e_{s}\coloneqq s,e_{k}\coloneqq
k]\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}.$

∎

Finally, with a more involved proof, we can show that up is compatible with
extensional equivalence.

It is realizable in $\mathcal{N}$ that

$\forall x_{1}\forall x_{2}\forall y_{1}\forall y_{2}\,(x_{1}\simeq
x_{2}\rightarrow(y_{1}\simeq
y_{2}\rightarrow\textnormal{{up}}(x_{1},y_{1})\simeq\textnormal{{up}}(x_{2},y_{2}))).$

###### Proof.

Fix $a_{1},a_{2},b_{1}$ and $b_{2}$ in N and let

$\theta_{2}\coloneqq\lambda e_{t}\boldsymbol{.}\lambda
e_{s}\boldsymbol{.}\lambda e_{r}\boldsymbol{.}\lambda
i\boldsymbol{.}\bigg{(}\Big{(}\underline{i}\Big{(}\lambda
w\boldsymbol{.}(\textnormal{{I}}e_{s})(\lambda
u\boldsymbol{.}u\underline{1})\Big{)}\Big{)}\Big{(}(\textnormal{{I}}e_{t})(\lambda
u\boldsymbol{.}u\underline{0})\Big{)}\bigg{)}\Big{(}e_{r}\Big{)}.$

It will suffice to prove that

$\theta_{2}\Vdash a_{1}\simeq a_{2}\rightarrow(b_{1}\simeq
b_{2}\rightarrow\textnormal{{up}}(a_{1},b_{1})\subseteq\textnormal{{up}}(a_{2},b_{2})).$

First note that, by using the proof that Extensionality is realizable in
$\mathcal{N}$ from Section 12, we have that

$\textnormal{{I}}\Vdash\forall x\forall y\forall z\,(x\simeq
y\rightarrow(y\mathop{\varepsilon}z\rightarrow x\in z)).$

Also,
$\lVert\textnormal{{up}}(a_{1},b_{1})\subseteq\textnormal{{up}}(a_{2},b_{2})\rVert=\bigcup_{c}\\{r\boldsymbol{.}\underline{i}\boldsymbol{.}\pi\operatorname{\hskip
1.42271pt\mid\hskip
1.42271pt}(c,\underline{i}\boldsymbol{.}\pi)\in\textnormal{{up}}(a_{1},b_{1}),\,r\Vdash
c\not\in\textnormal{{up}}(a_{2},b_{2})\\}.$

Now, fix $t\Vdash a_{1}\simeq a_{2}$, $s\Vdash b_{1}\simeq b_{2}$,
$(c,\underline{i}\boldsymbol{.}\pi)\in\textnormal{{up}}(a_{1},b_{1})$ and
$r\Vdash c\not\in\textnormal{{up}}(a_{2},b_{2})$. If $i=0$ then we must have
that $c=a_{1}$ and thus $r\Vdash a_{1}\not\in\textnormal{{up}}(a_{2},b_{2})$.
Now, $\lVert
a_{2}\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\textnormal{{up}}(a_{2},b_{2})\rVert=\\{\sigma\operatorname{\hskip
1.42271pt\mid\hskip
1.42271pt}(a_{2},\sigma)\in\textnormal{{up}}(a_{2},b_{2})\\}=\\{\underline{0}\boldsymbol{.}\sigma\operatorname{\hskip
1.42271pt\mid\hskip 1.42271pt}\sigma\in\Pi\\}$ so $\lambda
u\boldsymbol{.}u\underline{0}\Vdash
a_{2}\mathop{\varepsilon}\textnormal{{up}}(a_{2},b_{2})$. Therefore,
$(\textnormal{{I}}t)(\lambda u\boldsymbol{.}u\underline{0})\Vdash
a_{1}\in\textnormal{{up}}(a_{2},b_{2})$ and thus

$(\textnormal{{I}}t)(\lambda u\boldsymbol{.}u\underline{0})\star
r\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}.$

In the same way, if $i=1$ then $r\Vdash
b_{1}\not\in\textnormal{{up}}(a_{2},b_{2})$ and $(\textnormal{{I}}s)(\lambda
u\boldsymbol{.}u\underline{1})\star
r\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}.$ Finally, the
result follows from the computations

$\bigg{(}\Big{(}\underline{0}\Big{(}\lambda
w\boldsymbol{.}(\textnormal{{I}}s)(\lambda
u\boldsymbol{.}u\underline{1})\Big{)}\Big{)}\Big{(}(\textnormal{{I}}t)(\lambda
u\boldsymbol{.}u\underline{0})\Big{)}\bigg{)}\Big{(}r\Big{)}\star\pi\succ(\textnormal{{I}}t)(\lambda
u\boldsymbol{.}u\underline{0})\star
r\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$

and

$\bigg{(}\Big{(}\underline{1}\Big{(}\lambda
w\boldsymbol{.}(\textnormal{{I}}s)(\lambda
u\boldsymbol{.}u\underline{1})\Big{)}\Big{)}\Big{(}(\textnormal{{I}}t)(\lambda
u\boldsymbol{.}u\underline{0})\Big{)}\bigg{)}\Big{(}r\Big{)}\star\pi\succ(\textnormal{{I}}s)(\lambda
u\boldsymbol{.}u\underline{1})\star
r\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$

∎

###  14.2 Ordered Pairs

The previous analysis shows that up gives a reasonable interpretation of the
unordered pair. The next objective is to define an ordered pair and repeat the
analysis to show that it behaves as expected.

Let $a,b\in\textnormal{{N}}$. The _ordered pair_ of $a$ and $b$,
$\textnormal{{op}}(a,b)$, is

$\textnormal{{op}}(a,b)\coloneqq\textnormal{{up}}(\textnormal{{up}}(\textnormal{{sng}}(a),\text{\Large\cjRL{r}}({0})),\textnormal{{sng}}(\textnormal{{sng}}(b))).$

The first thing we wish to deduce is that the ordered pair can distinguish
between the first and the second element. Namely, if
$\textnormal{{op}}(x_{1},y_{1})\simeq\textnormal{{op}}(x_{2},y_{2})$ then we
should be able to realize that $x_{1}\simeq x_{2}$ and $y_{1}\simeq y_{2}$. In
order to do this, we first need to prove a technical lemma. This lemma is the
reason why we have chosen to using Wiener’s definition of ordered pairs.

For any $a,b,x\in\textnormal{{N}}$, the following are realizable in
$\mathcal{N}$:

  1. i.

$\textnormal{{up}}(\textnormal{{sng}}(x),\text{\Large\cjRL{r}}({0}))\not\simeq\textnormal{{up}}(\textnormal{{sng}}(a),\text{\Large\cjRL{r}}({0}))\rightarrow\textnormal{{up}}(\textnormal{{sng}}(x),\text{\Large\cjRL{r}}({0}))\not\in\textnormal{{op}}(a,b)$;

  2. ii.

$\textnormal{{sng}}(\textnormal{{sng}}(x))\not\simeq\textnormal{{sng}}(\textnormal{{sng}}(b))\rightarrow\textnormal{{sng}}(\textnormal{{sng}}(x))\not\in\textnormal{{op}}(a,b)$;

###### Proof.

First, note that

$\lVert\textnormal{{up}}(\textnormal{{sng}}(x),\text{\Large\cjRL{r}}({0}))\not\in\textnormal{{op}}(a,b)\rVert=\bigcup_{c}\\{s\boldsymbol{.}s^{\prime}\boldsymbol{.}\underline{i}\boldsymbol{.}\pi\operatorname{\hskip
1.42271pt\mid\hskip
1.42271pt}(c,\underline{i}\boldsymbol{.}\pi)\in\textnormal{{op}}(a,b),\\\
s\Vdash\textnormal{{up}}(\textnormal{{sng}}(x),\text{\Large\cjRL{r}}({0}))\subseteq
c,\,s^{\prime}\Vdash
c\subseteq\textnormal{{up}}(\textnormal{{sng}}(x),\text{\Large\cjRL{r}}({0}))\\}.$

Suppose that
$t\Vdash\textnormal{{up}}(\textnormal{{sng}}(x),\text{\Large\cjRL{r}}({0}))\not\simeq\textnormal{{up}}(\textnormal{{sng}}(a),\text{\Large\cjRL{r}}({0}))$,
$(c,\underline{i}\boldsymbol{.}\pi)\in\textnormal{{op}}(a,b)$ and
$s,s^{\prime}$ realize the relevant statements. Then $c$ is either
$\textnormal{{up}}(\textnormal{{sng}}(a),\text{\Large\cjRL{r}}({0}))$ or
$\textnormal{{sng}}(\textnormal{{sng}}(b))$. If
$c=\textnormal{{up}}(\textnormal{{sng}}(a),\text{\Large\cjRL{r}}({0}))$ then
$i=0$ and $t\star
s\boldsymbol{.}s^{\prime}\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$.

So, suppose that $c=\textnormal{{sng}}(\textnormal{{sng}}(b))$ and thus $i=1$.
Then

$s\Vdash\forall z(z\not\in\textnormal{{sng}}(\textnormal{{sng}}(b))\rightarrow
z\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\textnormal{{up}}(\textnormal{{sng}}(x),\text{\Large\cjRL{r}}({0}))).$

In particular,
$s\Vdash\text{\Large\cjRL{r}}({0})\not\in\textnormal{{sng}}(\textnormal{{sng}}(b))\rightarrow\text{\Large\cjRL{r}}({0})\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\textnormal{{up}}(\textnormal{{sng}}(x),\text{\Large\cjRL{r}}({0}))$.
Then, since $\\{\underline{1}\boldsymbol{.}\sigma\operatorname{\hskip
1.42271pt\mid\hskip
1.42271pt}\sigma\in\Pi\\}=\lVert\text{\Large\cjRL{r}}({0})\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\textnormal{{up}}(\textnormal{{sng}}(x),\text{\Large\cjRL{r}}({0}))\rVert$,
$s\underline{1}\Vdash\text{\Large\cjRL{r}}({0})\not\in\textnormal{{sng}}(\textnormal{{sng}}(b))\rightarrow\perp$.
Next, by .(iii), we have that there exists some term $r_{s}$ (dependent only
on $s$) such that
$r_{s}\Vdash\textnormal{{sng}}(b)\simeq\text{\Large\cjRL{r}}({0})$. However,
by .(ii) there is a realizer $r_{0}$ such that
$r_{0}\Vdash\textnormal{{sng}}(b)\not\simeq\text{\Large\cjRL{r}}({0})$ because
$\text{\Large\cjRL{r}}({0})=\emptyset$. Thus, $r_{s}\star
r_{0}\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$.

The conclusion for the first claim follows from creating a realizer $r_{1}$
such that $r_{1}\star
t\boldsymbol{.}s\boldsymbol{.}s^{\prime}\boldsymbol{.}\underline{0}\boldsymbol{.}\pi\succ
t\star s\boldsymbol{.}s^{\prime}\boldsymbol{.}\pi$ while $r_{1}\star
t\boldsymbol{.}s\boldsymbol{.}s^{\prime}\boldsymbol{.}\underline{1}\boldsymbol{.}\pi\succ
r_{s}\star r_{0}\boldsymbol{.}\pi$, which is relatively straightforward to do.

The second claim follows be a very similar argument to the one above. Namely,
we take
$t\Vdash\textnormal{{sng}}(\textnormal{{sng}}(x))\not\simeq\textnormal{{sng}}(\textnormal{{sng}}(b))$,
$(c,\underline{i}\boldsymbol{.}\pi)\in\textnormal{{op}}(a,b)$,
$s\Vdash\textnormal{{sng}}(\textnormal{{sng}}(b))\subseteq c$ and
$s^{\prime}\Vdash c\subseteq\textnormal{{sng}}(\textnormal{{sng}}(b))$. If
$c=\textnormal{{sng}}(\textnormal{{sng}}(b))$, then $i=1$ and $t\star
s\boldsymbol{.}s^{\prime}\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$.

So suppose that
$c=\textnormal{{up}}(\textnormal{{sng}}(a),\text{\Large\cjRL{r}}({0}))$. Then
$s^{\prime}\Vdash\textnormal{{up}}(\textnormal{{sng}}(a),\text{\Large\cjRL{r}}({0}))\subseteq\textnormal{{sng}}(\textnormal{{sng}}(x))$
and the same argument as above gives us that there is a realizer
$r_{s^{\prime}}$ such that $r_{s^{\prime}}\star
r_{0}\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$. The
conclusion then follows from creating a realizer $r_{2}$ such that $r_{2}\star
t\boldsymbol{.}s\boldsymbol{.}s^{\prime}\boldsymbol{.}\underline{1}\boldsymbol{.}\pi\succ
t\star s\boldsymbol{.}s^{\prime}\boldsymbol{.}\pi$ while $r_{2}\star
t\boldsymbol{.}s\boldsymbol{.}s^{\prime}\boldsymbol{.}\underline{0}\boldsymbol{.}\pi\succ
r_{s^{\prime}}\star r_{0}\boldsymbol{.}\pi$. ∎

The following two propositions show that the function op is also compatible
with extensional equality and thus gives a reasonable interpretation of
ordered pairs.

It is realizable in $\mathcal{N}$ that

$\forall x_{1}\forall x_{2}\forall y_{1}\forall
y_{2}\,(\textnormal{{op}}(x_{1},y_{1})\simeq\textnormal{{op}}(x_{2},y_{2})\rightarrow(x_{1}\simeq
x_{2}\land y_{1}\simeq y_{2})).$

###### Proof.

Fix $a_{1},b_{1},a_{2}$ and $b_{2}$ in N. It will suffice to show that if
$\mathcal{N}\Vdash\textnormal{{op}}(a_{1},b_{1})\subseteq\textnormal{{op}}(a_{2},b_{2})$
(that it to say, some $t$ realizes this statement) then

$\mathcal{N}\Vdash a_{1}\simeq a_{2}\qquad\text{and}\qquad\mathcal{N}\Vdash
b_{1}\simeq b_{2}.$

For the first of these statements, suppose that $t\Vdash\forall
z(z\not\in\textnormal{{op}}(a_{2},b_{2})\rightarrow
z\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\textnormal{{op}}(a_{1},b_{1}))$.
In particular, this means that

$t\Vdash\textnormal{{up}}(\textnormal{{sng}}(a_{1}),\text{\Large\cjRL{r}}({0}))\not\in\textnormal{{op}}(a_{2},b_{2})\rightarrow\textnormal{{up}}(\textnormal{{sng}}(a_{1}),\text{\Large\cjRL{r}}({0}))\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\textnormal{{op}}(a_{1},b_{1}).$

Now,
$\lVert\textnormal{{up}}(\textnormal{{sng}}(a_{1}),\text{\Large\cjRL{r}}({0}))\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\textnormal{{op}}(a_{1},b_{1})\rVert=\\{\underline{0}\boldsymbol{.}\pi\operatorname{\hskip
1.42271pt\mid\hskip 1.42271pt}\pi\in\Pi\\}$ which means that $t\star
s\boldsymbol{.}\underline{0}\boldsymbol{.}\sigma\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$
whenever $\sigma\in\Pi$ and
$s\Vdash\textnormal{{up}}(\textnormal{{sng}}(a_{1}),\text{\Large\cjRL{r}}({0}))\not\in\textnormal{{op}}(a_{2},b_{2})$.
From this, we can conclude that

$\lambda
u\boldsymbol{.}(tu)\underline{0}\Vdash\textnormal{{up}}(\textnormal{{sng}}(a_{1}),\text{\Large\cjRL{r}}({0}))\in\textnormal{{op}}(a_{2},b_{2}).$

We now work internally in any model, $\mathcal{N}$, of the realizable theory
T. By the contrapositive of .(i),

$\mathcal{N}\Vdash\textnormal{{up}}(\textnormal{{sng}}(a_{1}),\text{\Large\cjRL{r}}({0}))\simeq\textnormal{{up}}(\textnormal{{sng}}(a_{2}),\text{\Large\cjRL{r}}({0}))$

Next, we obviously have that
$\mathcal{N}\Vdash\textnormal{{sng}}(a_{1})\mathop{\varepsilon}\textnormal{{up}}(\textnormal{{sng}}(a_{1}),\text{\Large\cjRL{r}}({0}))$
so, by Section 8,
$\mathcal{N}\Vdash\textnormal{{sng}}(a_{1})\in\textnormal{{up}}(\textnormal{{sng}}(a_{2}),\text{\Large\cjRL{r}}({0}))$.
However, by .(ii),
$\mathcal{N}\Vdash\textnormal{{sng}}(a_{1})\not\simeq\text{\Large\cjRL{r}}({0})$
so, by .(iv),
$\mathcal{N}\Vdash\textnormal{{sng}}(a_{1})\simeq\textnormal{{sng}}(a_{2})$.
Finally, by .(v), $\mathcal{N}\Vdash a_{1}\simeq a_{2}$.

The second of these statements follows from a very similar argument: With the
same assumption on $t$ we have that $t\star
s\boldsymbol{.}\underline{1}\boldsymbol{.}\sigma\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$
whenever $\sigma\in\Pi$ and
$s\Vdash\textnormal{{sng}}(\textnormal{{sng}}(b_{1}))\not\in\textnormal{{op}}(a_{2},b_{2})$
and therefore

$\lambda
u\boldsymbol{.}(tu)\underline{1}\Vdash\textnormal{{sng}}(\textnormal{{sng}}(b_{1}))\in\textnormal{{op}}(a_{2},b_{2}).$

Therefore, by the contrapositive of .(ii),
$\mathcal{N}\Vdash\textnormal{{sng}}(\textnormal{{sng}}(b_{1}))\simeq\textnormal{{sng}}(\textnormal{{sng}}(b_{2}))$.
Finally, two applications of .(v) gives us that $\mathcal{N}\Vdash b_{1}\simeq
b_{2}$. ∎

It is realizable in $\mathcal{N}$ that

$\forall x_{1}\forall x_{2}\forall y_{1}\forall y_{2}\,(x_{1}\simeq
x_{2}\rightarrow(y_{1}\simeq
y_{2}\rightarrow\textnormal{{op}}(x_{1},y_{1})\simeq\textnormal{{op}}(x_{2},y_{2}))).$

###### Proof.

The proof of this proposition will be very similar to proof of Section 14.1.
Fix $a_{1},a_{2},b_{1}$ and $b_{2}$ in N. If will suffice to find a realizer
$\theta$ such that

$\theta\Vdash a_{1}\simeq a_{2}\rightarrow(b_{1}\simeq
b_{2}\rightarrow\textnormal{{op}}(a_{1},b_{1})\subseteq\textnormal{{op}}(a_{2},b_{2})).$

To do this, let $t\Vdash a_{1}\simeq a_{2}$, $s\Vdash b_{1}\simeq b_{2}$,
$(c,\underline{i}\boldsymbol{.}\pi)\in\textnormal{{op}}(a_{1},b_{1})$ and
$r\Vdash c\not\in\textnormal{{op}}(a_{2},b_{2})$. If $i=0$ then we must have
that
$c=\textnormal{{up}}(\textnormal{{sng}}(a_{1}),\text{\Large\cjRL{r}}({0}))$
and thus
$r\Vdash\textnormal{{up}}(\textnormal{{sng}}(a_{1}),\text{\Large\cjRL{r}}({0}))\not\in\textnormal{{op}}(a_{2},b_{2})$.
Now, since
$\lVert\textnormal{{up}}(\textnormal{{sng}}(a_{2}),\text{\Large\cjRL{r}}({0}))\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\textnormal{{op}}(a_{2},b_{2})\rVert=\\{\underline{0}\boldsymbol{.}\sigma\operatorname{\hskip
1.42271pt\mid\hskip 1.42271pt}\sigma\in\Pi\\}$, $\lambda
u\boldsymbol{.}u\underline{0}\Vdash\textnormal{{up}}(\textnormal{{sng}}(a_{2}),\text{\Large\cjRL{r}}({0}))\mathop{\varepsilon}\textnormal{{op}}(a_{2},b_{2})$.
Next, using .(iv) and Section 14.1 we have that

$\mathcal{N}\Vdash(a_{1}\simeq
a_{2})\rightarrow(\textnormal{{sng}}(a_{1})\simeq\textnormal{{sng}}(a_{2}))\rightarrow(\textnormal{{up}}(\textnormal{{sng}}(a_{1}),\text{\Large\cjRL{r}}({0}))\simeq\textnormal{{up}}(\textnormal{{sng}}(a_{2}),\text{\Large\cjRL{r}}({0}))),$

so we can find a realizer $v_{t}$ (dependent on $t$) such that
$v_{t}\Vdash\textnormal{{up}}(\textnormal{{sng}}(a_{1}),\text{\Large\cjRL{r}}({0})))\simeq\textnormal{{up}}(\textnormal{{sng}}(a_{2},\text{\Large\cjRL{r}}({0})))$.
Hence, using the proof that Extensionality is realizable in $\mathcal{N}$ from
Section 12, we have that $(\textnormal{{I}}v_{t})(\lambda
u\boldsymbol{.}u\underline{0})\Vdash\textnormal{{up}}(\textnormal{{sng}}(a_{1}),\text{\Large\cjRL{r}}({0}))\in\textnormal{{op}}(a_{2},b_{2})$
and thus

$(\textnormal{{I}}v_{t})(\lambda u\boldsymbol{.}u\underline{0})\star
r\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}.$

In a similar way, if $i=1$ then
$r\Vdash\textnormal{{sng}}(\textnormal{{sng}}(b_{1}))\not\in\textnormal{{op}}(a_{2},b_{2})$
and we can find a realizer $v_{s}$ (dependent on $s$) such that
$(\textnormal{{I}}v_{s})(\lambda
u\boldsymbol{.}u\underline{1})\Vdash\textnormal{{sng}}(\textnormal{{sng}}(b_{1}))\in\textnormal{{op}}(a_{2},b_{2})$,
giving $(\textnormal{{I}}v_{s})(\lambda u\boldsymbol{.}u\underline{1})\star
r\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$.

One can see that the desired realizer is then

$\lambda t\boldsymbol{.}\lambda s\boldsymbol{.}\lambda r\boldsymbol{.}\lambda
i\bigg{(}\Big{(}i\Big{(}\lambda w\boldsymbol{.}(\textnormal{{I}}v_{s})(\lambda
u\boldsymbol{.}u\underline{1})\Big{)}\Big{)}\Big{(}(\textnormal{{I}}v_{t})(\lambda
u\boldsymbol{.}u\underline{0})\Big{)}\bigg{)}\Big{(}r\Big{)}$, which concludes
the proof. ∎

###  14.3 Cartesian Products

To conclude this section, we see that this definition of ordered pairs allows
us to define Cartesian products of recursive names.

$c$ is said to be a _Cartesian product_ of $a$ and $b$ if:

  * •

$\forall x\mathop{\varepsilon}a\,\forall
y\mathop{\varepsilon}b\,(\textnormal{{op}}(x,y)\mathop{\varepsilon}c)$;

  * •

$\forall z((\forall x\mathop{\varepsilon}a\,\forall
y\mathop{\varepsilon}b\,\textnormal{{op}}(x,y)\not\simeq z)\rightarrow
z\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}c)$.

Observe that the second condition is equivalent to the claim that every
element of $c$ is an ordered pair consisting of an element of $a$ and an
element of $b$, that is $\forall z\mathop{\varepsilon}c\,\exists
x\mathop{\varepsilon}a\,\exists
y\mathop{\varepsilon}b(z\simeq\textnormal{{op}}(x,y))$.

Given sets $a$ and $b$ in the ground model define

$\textnormal{{Cart}}(a,b)\coloneqq\\{(\textnormal{{op}}(\text{\Large\cjRL{r}}({x}),\text{\Large\cjRL{r}}({y})),\pi)\operatorname{\hskip
1.42271pt\mid\hskip 1.42271pt}x\in a,\,y\in b,\,\pi\in\Pi\\}$.

$\mathcal{N}\Vdash\textnormal{{Cart}}(a,b)\text{ is the Cartesian product of
}\text{\Large\cjRL{r}}({a})\text{ and }\text{\Large\cjRL{r}}({b})$.

###### Proof.

We shall first prove that

$\textnormal{{I}}\Vdash\forall w_{0}^{\text{\Large\cjRL{r}}({a})}\,\forall
w_{1}^{\text{\Large\cjRL{r}}({b})}\,(\textnormal{{op}}(w_{0},w_{1})\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\textnormal{{Cart}}(a,b)\rightarrow\perp).$

To this end, fix $x\in a$, $y\in b$,
$t\Vdash\textnormal{{op}}(\text{\Large\cjRL{r}}({x}),\text{\Large\cjRL{r}}({y}))\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\textnormal{{Cart}}(a,b)$
and $\pi\in\Pi$. Then, by definition of Cart,
$\lVert\textnormal{{op}}(\text{\Large\cjRL{r}}({x}),\text{\Large\cjRL{r}}({y}))\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\textnormal{{Cart}}(a,b)\rVert=\Pi$
and thus $\textnormal{{I}}\star t\boldsymbol{.}\pi\succ
t\star\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$.

For the second claim, we shall prove that

$\lambda u\boldsymbol{.}u\theta\Vdash\forall z((\forall
w_{0}^{\text{\Large\cjRL{r}}({a})}\,\forall
w_{1}^{\text{\Large\cjRL{r}}({b})}\,\textnormal{{op}}(w_{0},w_{1})\not\simeq
z)\rightarrow
z\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\textnormal{{Cart}}(a,b)),$

where $\theta$ is a fixed realizer such that $\theta\Vdash\forall x(x\simeq
x)$ (for an example of such a realizer see Section 11.1).

For this, fix
$(\textnormal{{op}}(\text{\Large\cjRL{r}}({x}),\text{\Large\cjRL{r}}({y})),\pi)\in\textnormal{{Cart}}(a,b)$
and $t\Vdash\forall w_{0}^{\text{\Large\cjRL{r}}({a})}\,\forall
w_{1}^{\text{\Large\cjRL{r}}({b})}\,\textnormal{{op}}(w_{0},w_{1})\not\simeq\textnormal{{op}}(\text{\Large\cjRL{r}}({x}),\text{\Large\cjRL{r}}({y}))$.
Then, in particular, we have that
$t\Vdash\textnormal{{op}}(\text{\Large\cjRL{r}}({x}),\text{\Large\cjRL{r}}({y}))\not\simeq\textnormal{{op}}(\text{\Large\cjRL{r}}({x}),\text{\Large\cjRL{r}}({y}))$
and thus
$t\star\theta\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$. ∎

##  15 Functions

In its most naive form, a function is a collection of ordered pairs such that
whenever the first co-ordinates are equal then so are the second co-ordinates.
Due to there being two versions of “equality” in
$\operatorname{\textnormal{{ZF}}_{\varepsilon}}$ this gives rise to multiple
different interpretations of what a function should be.

[$\operatorname{\textnormal{{ZF}}_{\varepsilon}}$] A
$\mathop{\varepsilon}$-function with domain $a$ is a set $f$ satisfying:

  * •

($\mathop{\varepsilon}$-totality) $\forall x\mathop{\varepsilon}a\,\exists
y\,\textnormal{{op}}(x,y)\mathop{\varepsilon}f$;

  * •

$\forall x\mathop{\varepsilon}a\,\forall
y,y^{\prime}(\textnormal{{op}}(x,y)\mathop{\varepsilon}f\land\textnormal{{op}}(x,y^{\prime})\mathop{\varepsilon}f\rightarrow
y=y^{\prime})$.

We will write $\mathop{\varepsilon}\textnormal{{-Func}}(f)$ to indicate that
$f$ is a $\mathop{\varepsilon}$-function.

[$\operatorname{\textnormal{{ZF}}_{\varepsilon}}$] A $\in$-function with
domain $a$ is a set $f$ satisfying:

  * •

($\in$-totality) $\forall x\in a\,\exists y\,\textnormal{{op}}(x,y)\in f$;

  * •

$\forall x\in a\,\forall y,y^{\prime}(\textnormal{{op}}(x,y)\in
f\land\textnormal{{op}}(x,y^{\prime})\in f\rightarrow y\simeq y^{\prime})$.

We will write $\in\textnormal{{-Func}}(f)$ to indicate that $f$ is a
$\in$-function.

$b$ is said to be a co-domain of a $\mathop{\varepsilon}$-function $f$ if
whenever $\textnormal{{op}}(x,y)\mathop{\varepsilon}f$ then
$y\mathop{\varepsilon}b$ (and similarly for $\in$-functions). When we wish to
identify such a $b$ we will alternatively write $f$ as $f\colon a\rightarrow
b$, and it will be clear from the context what type of function $f$ is.

The definition of functions given here is perhaps not the most accurate
definition because we have not required that every element of $f$ is an
ordered pair and the first component of such an ordered pair is an element of
$a$. This could easily be added to the definition, however it would make
proving that a given set in N is a function more tedious without adding any
useful information. Instead we note that for any reasonable definition of
function we can restrict the set using $\mathop{\varepsilon}$-Separation to
only look at relevant ordered pairs.

Also, on occasion it will be simpler to phrase a function as a binary relation
satisfying the relevant translations of the conditions, for example $\forall
x\mathop{\varepsilon}a\,\forall y,y^{\prime}(f(x,y)\land
f(x,y^{\prime})\rightarrow y=y^{\prime})$. Clearly, given a function defined
in this way we can find a set representing this function in the obvious way.

In most of the conservativity results between ZF and
$\operatorname{\textnormal{{ZF}}_{\varepsilon}}$ one shows that the $\epsilon$
definition of a concept directly relates to the $\in$ definition. However,
this is not the case here. For example, take two distinct sets $x$ and $y$
which are extensionally equal (such as $\\{(a,\pi)\operatorname{\hskip
1.42271pt\mid\hskip 1.42271pt}\pi\in\Pi\\}$ and
$\\{(a,\underline{0}\boldsymbol{.}\pi)\operatorname{\hskip 1.42271pt\mid\hskip
1.42271pt}\pi\in\Pi\\}$). Then there is a $\mathop{\varepsilon}$-function
$f\colon\\{x,y\\}\times\Pi\rightarrow\text{\Large\cjRL{r}}({2})$ given by
sending $x$ to $\text{\Large\cjRL{r}}({0})$ and $y$ to
$\text{\Large\cjRL{r}}({1})$. However, this does not translate to a
$\in$-function because such a function would need to send $x$ to both
$\text{\Large\cjRL{r}}({0})$ and $\text{\Large\cjRL{r}}({1})$ which are not
extensionally equal sets. Instead, for conservativity results, we need an
intermediate notion of function.

[$\operatorname{\textnormal{{ZF}}_{\varepsilon}}$] An _extensional_ function
with domain $a$ is a set $f$ satisfying:

  * •

($\mathop{\varepsilon}$-totality) $\forall x\mathop{\varepsilon}a\,\exists
y\,\textnormal{{op}}(x,y)\mathop{\varepsilon}f$;

  * •

$\forall x,x^{\prime}\mathop{\varepsilon}a\,\forall y,y^{\prime}(x\simeq
x^{\prime}\land\textnormal{{op}}(x,y)\mathop{\varepsilon}f\land\textnormal{{op}}(x^{\prime},y^{\prime})\mathop{\varepsilon}f\rightarrow
y\simeq y^{\prime})$.

We will write $\textnormal{{Ext-Func}}(f)$ to indicate that $f$ is an
extensional function.

In the definitions of $\mathop{\varepsilon}$-functions and $\in$-functions we
only needed to assume that for every $x$ in $a$ and $y,y^{\prime}$ if $f(x,y)$
and $f(x,y^{\prime})$ both hold then $y$ and $y^{\prime}$ are equal. On the
other hand, in the definition of an extensional function we have needed to
strengthen this condition to the claim that if $x\simeq x^{\prime}$ and both
$f(x,y)$ and $f(x^{\prime},y^{\prime})$ hold then $y\simeq y^{\prime}$. It is
relatively straight forward to see that the additional $x^{\prime}$ is not
needed in either of the first two definitions, however its inclusion for
extensional functions is needed to ensure that they translate cleanly to
$\in$-functions.

Suppose that $f$ is a $\in$-function with domain $a$. Let $g$ be the binary
relation defined by

$\textnormal{{op}}(x,y)\mathop{\varepsilon}g\Longleftrightarrow
x\mathop{\varepsilon}a\land\textnormal{{op}}(x,y)\in f.$

Then $g$ is an extensional function with domain $a$. Similarly, if $g$ is an
extensional function with domain $a$ and $f$ is the binary relation defined by

$\textnormal{{op}}(x,y)\in f\Longleftrightarrow\exists
c\mathop{\varepsilon}a(x\simeq
c\land\textnormal{{op}}(c,y)\mathop{\varepsilon}g,$

then $f$ is a $\in$-function with domain $a$.

As an example of conservativity, we briefly discuss a definition of
_cardinals_ in $\operatorname{\textnormal{{ZF}}_{\varepsilon}}$.

A relation $f$ with domain $a$ is said to be a
$\mathop{\varepsilon}$-injection if

$\forall x,x^{\prime}\mathop{\varepsilon}a\,\forall
y\,\big{(}\textnormal{{op}}(x,y)\mathop{\varepsilon}f\land\textnormal{{op}}(x^{\prime},y)\mathop{\varepsilon}f\rightarrow
x\simeq x^{\prime}\big{)}.$

A relation $f$ with domain $a$ is said to be a
$\mathop{\varepsilon}$-surjection on $b$ if

$\forall y\mathop{\varepsilon}b\,\exists
x\mathop{\varepsilon}a\,\textnormal{{op}}(x,y)\mathop{\varepsilon}f.$

An ordinal $a$ is said to be a $\mathop{\varepsilon}$_-cardinal_ if for every
$b\mathop{\varepsilon}a$ there is no extensional function which is a
$\mathop{\varepsilon}$-surjection of $b$ onto $a$.

If $a$ is a $\mathop{\varepsilon}$-cardinal, then it is a $\in$-cardinal.

###### Proof.

Let $a$ be an $\mathop{\varepsilon}$-ordinal. We shall show that if $a$ is not
a $\in$-cardinal then $a$ is not a $\mathop{\varepsilon}$-cardinal. To this
end, suppose that $b\in a$ and $f\colon b\rightarrow a$ was a
$\in$-surjection. Fix $z\mathop{\varepsilon}a$ such that $b\simeq z$ and
define a binary relation $g$ by

$\textnormal{{op}}(x,y)\mathop{\varepsilon}g\Longleftrightarrow\exists c\in
a\,\big{(}\textnormal{{op}}(x,c)\in f\land c\simeq y\big{)}.$

We shall show that $g$ defines a $\mathop{\varepsilon}$-surjection from $z$
onto $a$. There are three things to prove: that $g$ is
$\mathop{\varepsilon}$-total on $a$; $g$ is an extensional function; and $g$
is a $\mathop{\varepsilon}$-surjection.

For the first claim, take $x\mathop{\varepsilon}z$. Then $x\in z$ and
therefore $x\in b$, by .(vii). Since $f$ is $\in$-total, we can fix $c\in a$
such that $\textnormal{{op}}(x,c)\in f$ and then fix $y\mathop{\varepsilon}a$
such that $y\simeq c$. Hence, we have
$\textnormal{{op}}(x,y)\mathop{\varepsilon}g$.

For the second claim, fix $x,x^{\prime}\mathop{\varepsilon}b$,
$y,y^{\prime}\mathop{\varepsilon}a$ and suppose that
$\textnormal{{op}}(x,y)\mathop{\varepsilon}g$,
$\textnormal{{op}}(x^{\prime},y^{\prime})\mathop{\varepsilon}g$ and $x\simeq
x^{\prime}$. Fix $c,c^{\prime}\in a$ such that $\textnormal{{op}}(x,c)\in f$,
$\textnormal{{op}}(x^{\prime},c^{\prime})\in f$, $c\simeq y$ and
$c^{\prime}\simeq y^{\prime}$. Since $f$ is a $\in$-function, $x,x^{\prime}\in
b$ and $x\simeq x^{\prime}$, we must have that $c\simeq c^{\prime}$. Therefore
$y\simeq c\simeq c^{\prime}\simeq y^{\prime}$.

For the final claim, fix $y\mathop{\varepsilon}a$. Then $y\in a$ so, since $f$
is a $\in$-surjection, we can fix $t\in b$ such that
$\textnormal{{op}}(t,y)\in f$ holds. Since $t\in b$ and $b\simeq z$, $t\in z$.
Therefore, there exists some $d\mathop{\varepsilon}z$ such that $t\simeq d$.
Since $g$ is $\mathop{\varepsilon}$-total, we can fix
$y^{\prime}\mathop{\varepsilon}a$ such that
$\textnormal{{op}}(d,y^{\prime})\mathop{\varepsilon}g$ and then, by
definition, $c\in a$ such that $\textnormal{{op}}(d,c)\in f$ and $c\simeq
y^{\prime}$. Finally, since $f$ is a function and $t\simeq d$, $y\simeq
c\simeq y^{\prime}$, from which we can conclude that
$\textnormal{{op}}(d,y)\mathop{\varepsilon}g$ as required. ∎

##  16 Lifting Functions

Here we give a general framework to lift functions from the ground model to
the realizability model, the idea being that they should extend the (natural
interpretations of the) function from the ground model. For example, if
$f\colon 2\rightarrow 2$ is a ground model function then there should be some
$\mathop{\varepsilon}$-function
$\tilde{f}\colon\text{\Large\cjRL{r}}({2})\rightarrow\text{\Large\cjRL{r}}({2})$
such that
$\mathcal{N}\Vdash\tilde{f}(\text{\Large\cjRL{r}}({i}))=\text{\Large\cjRL{r}}({f(i)})$
for $i\in\\{0,1\\}$.

Suppose that $a,b\in\textnormal{{V}}$ and $f\colon a\rightarrow b$ is a
function. We define the _lift_ of $f$, $\tilde{f}$ as

$\tilde{f}\coloneqq\\{(\textnormal{{op}}(\text{\Large\cjRL{r}}({c}),\text{\Large\cjRL{r}}({f(c)})),\pi)\operatorname{\hskip
1.42271pt\mid\hskip 1.42271pt}c\in a,\pi\in\Pi\\}.$

We begin by showing that $\tilde{f}$ is a lift of the function $f$ in some
precise sense:

For any $c$ in $a$,

$\textnormal{{I}}\Vdash\forall
z\big{(}\textnormal{{op}}(\text{\Large\cjRL{r}}({c}),z)\mathop{\varepsilon}\tilde{f}\rightarrow\text{\Large\cjRL{r}}({f(c)})=z\big{)}\text{
and }\textnormal{{I}}\Vdash\forall
z\big{(}\text{\Large\cjRL{r}}({f(c)})=z\xhookrightarrow{}\textnormal{{op}}(\text{\Large\cjRL{r}}({c}),z)\mathop{\varepsilon}\tilde{f}\big{)}.$

###### Proof.

For the first claim, suppose that
$t\Vdash\textnormal{{op}}(\text{\Large\cjRL{r}}({c}),z)\mathop{\varepsilon}\tilde{f}$,
$s\Vdash\text{\Large\cjRL{r}}({f(c)})\neq z$ and $\pi\in\Pi$. We shall show
that
$s\Vdash\textnormal{{op}}(\text{\Large\cjRL{r}}({c}),z)\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\tilde{f}$
from which it shall follow that $\textnormal{{I}}\star
t\boldsymbol{.}s\boldsymbol{.}\pi\succ t\star
s\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$. But this
follows from the observation that
$\lVert\textnormal{{op}}(\text{\Large\cjRL{r}}({c}),z)\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\tilde{f}\rVert=\Pi$
if $z=\text{\Large\cjRL{r}}({f(c)})$ and equals $\emptyset$ otherwise, which
means that
$\lVert\textnormal{{op}}(\text{\Large\cjRL{r}}({c}),z)\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\tilde{f}\rVert=\lVert\text{\Large\cjRL{r}}({f(c)})\neq
z\rVert$.

For the second claim, if $\text{\Large\cjRL{r}}({f(c)})\neq z$ then
$\lVert\text{\Large\cjRL{r}}({f(c)})=z\xhookrightarrow{}\textnormal{{op}}(\text{\Large\cjRL{r}}({c}),z)\mathop{\varepsilon}\tilde{f}\rVert=\emptyset$
and thus I trivially realizes this. Otherwise,
$\text{\Large\cjRL{r}}({f(c)})=z$ and
$\lVert\text{\Large\cjRL{r}}({f(c)})=\text{\Large\cjRL{r}}({f(c)})\xhookrightarrow{}\textnormal{{op}}(\text{\Large\cjRL{r}}({c}),\text{\Large\cjRL{r}}({f(c)}))\mathop{\varepsilon}\tilde{f}\rVert=\lVert\textnormal{{op}}(\text{\Large\cjRL{r}}({c}),\text{\Large\cjRL{r}}({f(c)}))\mathop{\varepsilon}\tilde{f}\rVert=\\{t\boldsymbol{.}\pi\operatorname{\hskip
1.42271pt\mid\hskip
1.42271pt}\pi\in\Pi,\forall\sigma\in\Pi(t\star\sigma\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}})\\}$.
Therefore, for any such $t$ and $\pi$, $\textnormal{{I}}\star
t\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$. ∎

$\lambda u\boldsymbol{.}\lambda v\boldsymbol{.}vu\Vdash\forall
x^{\text{\Large\cjRL{r}}({a})}\forall y\forall y^{\prime}(y\neq
y^{\prime}\rightarrow\textnormal{{op}}(x,y)\mathop{\varepsilon}\tilde{f}\rightarrow\textnormal{{op}}(x,y^{\prime})\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\tilde{f}).$
Therefore, $\tilde{f}$ is realized to be a $\mathop{\varepsilon}$-function
with domain $\text{\Large\cjRL{r}}({a})$.

###### Proof.

Fix $c\in a$, $d,d^{\prime}\in\textnormal{{N}}$ and suppose that $t\Vdash
d\neq d^{\prime}$,
$s\Vdash\textnormal{{op}}(\text{\Large\cjRL{r}}({c}),d)\mathop{\varepsilon}\tilde{f}$
while
$(\textnormal{{op}}(\text{\Large\cjRL{r}}({c}),d^{\prime}),\pi)\in\tilde{f}$.
By definition of $\tilde{f}$, we must have that
$d^{\prime}=\text{\Large\cjRL{r}}({f(c)})$. There are now two cases;
$d\neq\text{\Large\cjRL{r}}({f(c)})$ and $d=\text{\Large\cjRL{r}}({f(c)})$.

If $d\neq\text{\Large\cjRL{r}}({f(c)})$ then
$\lVert\textnormal{{op}}(\text{\Large\cjRL{r}}({c}),d)\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\tilde{f}\rVert=\emptyset$
and therefore
$\lVert\textnormal{{op}}(\text{\Large\cjRL{r}}({c}),d)\mathop{\varepsilon}\tilde{f}\rVert=\Lambda\star\Pi$.
From this it follows that $\lambda u\boldsymbol{.}\lambda
v\boldsymbol{.}vu\star t\boldsymbol{.}s\boldsymbol{.}\pi\succ s\star
t\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$.

On the other hand, if $d=\text{\Large\cjRL{r}}({f(c)})$ then
$\lVert\textnormal{{op}}(\text{\Large\cjRL{r}}({c}),d)\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\tilde{f}\rVert=\Pi=\lVert
d\neq d^{\prime}\rVert$. From this it follows that
$t\boldsymbol{.}\pi\in\lVert\textnormal{{op}}(\text{\Large\cjRL{r}}({c}),d)\mathop{\varepsilon}\tilde{f}\rVert$
and therefore $\lambda u\boldsymbol{.}\lambda v\boldsymbol{.}vu\star
t\boldsymbol{.}s\boldsymbol{.}\pi\succ s\star
t\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$. ∎

Finally, we can see that $\text{\Large\cjRL{r}}({b})$ is a co-domain of
$\tilde{f}$:

$\textnormal{{I}}\Vdash\forall x^{\text{\Large\cjRL{r}}({a})}\forall
y(y\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\text{\Large\cjRL{r}}({b})\rightarrow\textnormal{{op}}(x,y)\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\tilde{f})$.

###### Proof.

Fix $c\in a$, $d\in\textnormal{{N}}$ and suppose that $t\Vdash
d\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\text{\Large\cjRL{r}}({b})$
while $(\textnormal{{op}}(\text{\Large\cjRL{r}}({c}),d),\pi)\in\tilde{f}$.
Then, by definition, we must have that $d=f(\text{\Large\cjRL{r}}({c}))$ which
means that $\textnormal{{I}}\Vdash
d\mathop{\varepsilon}\text{\Large\cjRL{r}}({b})$. Therefore, we have
$\textnormal{{I}}\star
t\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$. ∎

###  16.1 Lifting Functions with Multiple Arguments

If one were to try and lift a function $f\colon a_{0}\times a_{1}\rightarrow
b$ using the previous methodology this would give us a function
$\tilde{f}\colon\text{\Large\cjRL{r}}({a_{0}\times a_{1}})\rightarrow b$ in
$\mathcal{N}$ rather than a more useful function with domain
$\text{\Large\cjRL{r}}({a_{0}})\times\text{\Large\cjRL{r}}({a_{1}})$. However,
this can be achieved by a slight alteration to the definition of the lift.
Since the proof follows by the same argument as in the earlier propositions,
we will omit it.

Suppose that $f\colon a_{0}\times a_{1}\rightarrow b$ is a function. Let

$\tilde{f}\colon\\{(\textnormal{{op}}(\textnormal{{op}}(\text{\Large\cjRL{r}}({x_{0}}),\text{\Large\cjRL{r}}({x_{1}})),\text{\Large\cjRL{r}}({f(x_{0},x_{1})})),\pi)\operatorname{\hskip
1.42271pt\mid\hskip 1.42271pt}x_{0}\in a_{0},x_{1}\in a_{1},\pi\in\Pi\\}.$

Then
$\mathcal{N}\Vdash\tilde{f}\colon\textnormal{{Cart}}(a_{0},a_{1})\rightarrow\text{\Large\cjRL{r}}({b})\text{
is a }\mathop{\varepsilon}\text{-function}$. Moreover, for any $x_{0}\in
a_{0}$ and $x_{1}\in a_{1}$,

I $\displaystyle\Vdash\forall
z\big{(}\textnormal{{op}}(\textnormal{{op}}(\text{\Large\cjRL{r}}({x_{0}}),\text{\Large\cjRL{r}}({x_{1}})),z)\mathop{\varepsilon}\tilde{f}\rightarrow\text{\Large\cjRL{r}}({f(x_{0},x_{1})})=z\big{)}\text{
and }$ I $\displaystyle\Vdash\forall
z\big{(}\text{\Large\cjRL{r}}({f(x_{0},x_{1})})=z\xhookrightarrow{}\textnormal{{op}}(\textnormal{{op}}(\text{\Large\cjRL{r}}({x_{0}}),\text{\Large\cjRL{r}}({x_{1}})),z)\mathop{\varepsilon}\tilde{f}\big{)}.$

We recall here that, in $\mathcal{N}$, $\textnormal{{Cart}}(a_{0},a_{1})$ is a
name for the Cartesian product of $\text{\Large\cjRL{r}}({a_{0}})$ and
$\text{\Large\cjRL{r}}({a_{1}})$. Therefore, unless there is room for
confusion, we shall also refer to this set as the lift of the function $f$ and
use the same notation because this is what we want to mean by lifting a
function with domain $a_{0}\times a_{1}$.

The above result could be easily further generalised to allow for the lift of
a function $f\colon a_{0}\times\dots a_{n}\rightarrow b$ for any finite $n$ in
the obvious way.

$\text{\Large\cjRL{r}}({2})$ is a Boolean algebra with binary operations
$\lor$ and $\land$ and unary operation $-$ given by the lift of the
corresponding (trivial) operations on $\\{0,1\\}$.

###### Proof.

Formally, this is proven by showing that the above operations satisfy
commutativity, associativity, distributivity, absorption and complementations.
All of these are straightforward, and we briefly discuss one of the absorption
cases as an example.

$\textnormal{{I}}\Vdash\forall x^{\text{\Large\cjRL{r}}({2})}\forall
y^{\text{\Large\cjRL{r}}({2})}\;(x\land(x\lor y)=x).$

It suffices to prove that if $i,j\in\\{0,1\\}$ then
$\textnormal{{I}}\Vdash\text{\Large\cjRL{r}}({i})\land(\text{\Large\cjRL{r}}({i})\lor\text{\Large\cjRL{r}}({j}))=\text{\Large\cjRL{r}}({i})$.
But, this is immediate from the fact that $\\{0,1\\}$ is a Boolean algebra and
the operations lift the operations on $\\{0,1\\}$. ∎

We would have liked to lift the function to an extensional function in the
realizability model, however in general this does not seem possible to do. The
issue is that there may not be a realizer $t$ such that, for any $a\neq b$,
$t\Vdash\text{\Large\cjRL{r}}({a})\not\simeq\text{\Large\cjRL{r}}({b})$.

This becomes a problem when one wants to prove $\mathcal{N}\Vdash\forall
z(\textnormal{{op}}(\text{\Large\cjRL{r}}({c}),z)\in\tilde{f}\rightarrow\text{\Large\cjRL{r}}({f(c)})\simeq
z)$. If $\textnormal{{op}}(\text{\Large\cjRL{r}}({c}),z)\in\tilde{f}$ then we
can find some $d\mathop{\varepsilon}a$ for which
$\textnormal{{op}}(\text{\Large\cjRL{r}}({c}),z)\simeq\textnormal{{op}}(\text{\Large\cjRL{r}}({d}),\text{\Large\cjRL{r}}({f(d)}))$.
It will then be the case that, in $\mathcal{N}$,
$z\simeq\text{\Large\cjRL{r}}({f(d)})$. The issue is that we cannot prove
$\mathcal{N}\Vdash\text{\Large\cjRL{r}}({c})\simeq\text{\Large\cjRL{r}}({d})\rightarrow\text{\Large\cjRL{r}}({f(c)})\simeq\text{\Large\cjRL{r}}({f(d)})$
and therefore it is unclear how one could conclude that
$\mathcal{N}\Vdash\text{\Large\cjRL{r}}({f(c)})\simeq z$.

###  16.2 Lifting Class Functions

Formally, the implementations for singletons, unordered pairs and ordered
pairs have only been defined externally for elements of N. In this short
section we outline how to internalise these functions so as to naturally view
them as class functions over the structure. As mentioned in Section 9.1 this
will then allow us to enrich the theory
$\operatorname{\textnormal{{ZF}}_{\varepsilon}}$ by any
$\mathcal{A}$-definable function in a way that allows us to internalise such
functions with the theory. In order to do this, we need a general method to
universally lift a function
$f\colon\textnormal{{N}}\rightarrow\textnormal{{N}}$.

Suppose that $f\colon\textnormal{{N}}\rightarrow\textnormal{{N}}$ is a
function (as defined in the ground model). We define the _universal lift_ of
$f$, $\tilde{f}$, as

$\tilde{f}\coloneqq\\{(\textnormal{{op}}(a,f(a)),\pi)\operatorname{\hskip
1.42271pt\mid\hskip 1.42271pt}a\in\textnormal{{N}},\pi\in\Pi\\}.$

Suppose that $f\colon\textnormal{{N}}\rightarrow\textnormal{{N}}$. Then, in
$\mathcal{N}$,

  1. i.

For every $a\in\textnormal{{N}}$, $\forall
z\,(\textnormal{{op}}(a,z)\mathop{\varepsilon}\tilde{f}\rightarrow z=f(a))$
and $\forall
z\,(f(a)=z\rightarrow\textnormal{{op}}(a,z)\mathop{\varepsilon}\tilde{f})$.
That is, $\tilde{f}$ agrees with $f$ on N.

  2. ii.

$\forall x\,\exists y\,\textnormal{{op}}(x,y)\mathop{\varepsilon}\tilde{f}$
and $\forall x\,\forall y\,\forall
y^{\prime}\,(\textnormal{{op}}(x,y)\mathop{\varepsilon}\tilde{f}\land\textnormal{{op}}(x,y^{\prime})\mathop{\varepsilon}\tilde{f}\rightarrow
y=y^{\prime})$. That is, $\tilde{f}$ is a class
$\mathop{\varepsilon}$-function.

Since the proof to this theorem is the same as for the lift of the set
function $f\colon a\rightarrow b$, we will omit it.

Using the analogous construction to Section 16.1, it is also possible to lift
any function $f\colon\textnormal{{N}}^{n}\rightarrow\textnormal{{N}}$ for any
$n\in\omega$.

The following functions universally lift to the realizability model and
therefore can be viewed as internal functions in $\mathcal{N}$.

  * •

$\textnormal{{sng}}\colon\textnormal{{N}}\rightarrow\textnormal{{N}}$,
$a\mapsto\\{a\\}\times\Pi$;

  * •

$\textnormal{{up}}\colon\textnormal{{N}}\times\textnormal{{N}}\rightarrow\textnormal{{N}}$,
$(a,b)\mapsto\\{(a,\underline{0}\boldsymbol{.}\pi)\operatorname{\hskip
1.42271pt\mid\hskip
1.42271pt}\pi\in\Pi\\}\cup\\{(b,\underline{1}\boldsymbol{.}\pi)\operatorname{\hskip
1.42271pt\mid\hskip 1.42271pt}\pi\in\Pi\\}$;

  * •

$\textnormal{{op}}\colon\textnormal{{N}}\times\textnormal{{N}}\rightarrow\textnormal{{N}}$,
$(a,b)\mapsto\textnormal{{up}}(\textnormal{{up}}(\textnormal{{sng}}(a),\text{\Large\cjRL{r}}({0})),\textnormal{{sng}}(\textnormal{{sng}}(b)))$;

  * •

$a\mathbin{\mathchoice{\ooalign{$\displaystyle\cup$\cr$\displaystyle{\raisebox{0.5pt}{\scalebox{0.4}{$\mathcal{N}$}}}$}}{\ooalign{$\textstyle\cup$\cr$\textstyle{\raisebox{0.5pt}{\scalebox{0.4}{$\mathcal{N}$}}}$}}{\ooalign{$\scriptstyle\cup$\cr$\scriptstyle{\raisebox{0.5pt}{\scalebox{0.4}{$\mathcal{N}$}}}$}}{\ooalign{$\scriptscriptstyle\cup$\cr$\scriptscriptstyle{\raisebox{0.5pt}{\scalebox{0.4}{$\mathcal{N}$}}}$}}}b\colon\textnormal{{N}}\times\textnormal{{N}}\rightarrow$,
$(a,b)\mapsto\\{(x,\underline{0}\boldsymbol{.}\pi)\operatorname{\hskip
1.42271pt\mid\hskip 1.42271pt}(x,\pi)\in
a\\}\cup\\{(x,\underline{1}\boldsymbol{.}\pi)\operatorname{\hskip
1.42271pt\mid\hskip 1.42271pt}(x,\pi)\in b\\}$. This function gives a
canonical way to define the non-extensional union of two sets;

  * •

$w\mathcal{P}\colon\textnormal{{N}}\rightarrow\textnormal{{N}}$,
$a\mapsto\mathcal{P}(\textnormal{{dom}}(a)\times\Pi)\times\Pi$. This function
gives a canonical weak power set for every set $a$.

[A note on unions] a

It is easy to see that, for any $a,b\in\textnormal{{N}}$, $\lambda
u\boldsymbol{.}u\underline{0}\Vdash
x\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}a\mathbin{\mathchoice{\ooalign{$\displaystyle\cup$\cr$\displaystyle{\raisebox{0.5pt}{\scalebox{0.4}{$\mathcal{N}$}}}$}}{\ooalign{$\textstyle\cup$\cr$\textstyle{\raisebox{0.5pt}{\scalebox{0.4}{$\mathcal{N}$}}}$}}{\ooalign{$\scriptstyle\cup$\cr$\scriptstyle{\raisebox{0.5pt}{\scalebox{0.4}{$\mathcal{N}$}}}$}}{\ooalign{$\scriptscriptstyle\cup$\cr$\scriptscriptstyle{\raisebox{0.5pt}{\scalebox{0.4}{$\mathcal{N}$}}}$}}}b\rightarrow
x\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}a$, $\lambda
u\boldsymbol{.}u\underline{1}\Vdash
x\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}a\mathbin{\mathchoice{\ooalign{$\displaystyle\cup$\cr$\displaystyle{\raisebox{0.5pt}{\scalebox{0.4}{$\mathcal{N}$}}}$}}{\ooalign{$\textstyle\cup$\cr$\textstyle{\raisebox{0.5pt}{\scalebox{0.4}{$\mathcal{N}$}}}$}}{\ooalign{$\scriptstyle\cup$\cr$\scriptstyle{\raisebox{0.5pt}{\scalebox{0.4}{$\mathcal{N}$}}}$}}{\ooalign{$\scriptscriptstyle\cup$\cr$\scriptscriptstyle{\raisebox{0.5pt}{\scalebox{0.4}{$\mathcal{N}$}}}$}}}b\rightarrow
x\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}b$ and $\lambda
u\boldsymbol{.}\lambda v\boldsymbol{.}\lambda i\boldsymbol{.}(i\lambda
w\boldsymbol{.}v)u\Vdash
x\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}a\rightarrow(x\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}b\rightarrow
x\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}a\mathbin{\mathchoice{\ooalign{$\displaystyle\cup$\cr$\displaystyle{\raisebox{0.5pt}{\scalebox{0.4}{$\mathcal{N}$}}}$}}{\ooalign{$\textstyle\cup$\cr$\textstyle{\raisebox{0.5pt}{\scalebox{0.4}{$\mathcal{N}$}}}$}}{\ooalign{$\scriptstyle\cup$\cr$\scriptstyle{\raisebox{0.5pt}{\scalebox{0.4}{$\mathcal{N}$}}}$}}{\ooalign{$\scriptscriptstyle\cup$\cr$\scriptscriptstyle{\raisebox{0.5pt}{\scalebox{0.4}{$\mathcal{N}$}}}$}}}b)$.
Thus $\mathcal{N}\Vdash\forall
x(x\mathop{\varepsilon}a\mathbin{\mathchoice{\ooalign{$\displaystyle\cup$\cr$\displaystyle{\raisebox{0.5pt}{\scalebox{0.4}{$\mathcal{N}$}}}$}}{\ooalign{$\textstyle\cup$\cr$\textstyle{\raisebox{0.5pt}{\scalebox{0.4}{$\mathcal{N}$}}}$}}{\ooalign{$\scriptstyle\cup$\cr$\scriptstyle{\raisebox{0.5pt}{\scalebox{0.4}{$\mathcal{N}$}}}$}}{\ooalign{$\scriptscriptstyle\cup$\cr$\scriptscriptstyle{\raisebox{0.5pt}{\scalebox{0.4}{$\mathcal{N}$}}}$}}}b\leftrightarrow(x\mathop{\varepsilon}a\lor
x\mathop{\varepsilon}b))$ so
$\mathbin{\mathchoice{\ooalign{$\displaystyle\cup$\cr$\displaystyle{\raisebox{0.5pt}{\scalebox{0.4}{$\mathcal{N}$}}}$}}{\ooalign{$\textstyle\cup$\cr$\textstyle{\raisebox{0.5pt}{\scalebox{0.4}{$\mathcal{N}$}}}$}}{\ooalign{$\scriptstyle\cup$\cr$\scriptstyle{\raisebox{0.5pt}{\scalebox{0.4}{$\mathcal{N}$}}}$}}{\ooalign{$\scriptscriptstyle\cup$\cr$\scriptscriptstyle{\raisebox{0.5pt}{\scalebox{0.4}{$\mathcal{N}$}}}$}}}$
does give a name for the non-extensional union of two sets.

It would have been preferable to define the name for the union as simply
$a\cup b$, using the true union in the ground model. One can see that
$\mathcal{N}\Vdash
x\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}a\cup
b\rightarrow(x\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}a\lor
x\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}b)$ and
therefore $a\cup b$ contains the union of the two sets, the difficulty is in
the reverse direction. This is because we run into the standard issue that
from $(x,\pi)\in a\cup b$ we cannot decide from $\pi$ whether $(x,\pi)\in a$
or $(x,\pi)\in b$.

###  16.3 Images of Functions

Due to our coding of ordered pairs, it is cumbersome to deal with the image of
a lifted function. To see the issue consider trying to solve

$\forall x\tilde{f}(x)\mathop{\varepsilon}a.$

Formally, to realize this we would need to realize something of the form

$\forall x(\forall
y(\textnormal{{op}}(x,y)\mathop{\varepsilon}\tilde{f}\rightarrow
y\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}a)\rightarrow\perp).$

Therefore, we introduce an easier way to phrase such statements through a new
falsity value.

Suppose that $f\colon a\rightarrow b$ is a function in the ground model and
let $\tilde{f}$ be the standard name for the lift of $f$. Then, for any
formula $\varphi(u,v,\overrightarrow{w})$ and
$\overrightarrow{w}\in\textnormal{{N}}$,

$\lVert\varphi(x,\tilde{f}(x),\overrightarrow{w})\rVert=\begin{cases}\lVert\varphi(x,\text{\Large\cjRL{r}}({d}),\overrightarrow{w})\rVert&\text{
if }x=\text{\Large\cjRL{r}}({c})\text{ and }f(c)=d\text{ for some }d\in b,\\\
\emptyset&\text{ otherwise.}\end{cases}$

We note that, since $f$ is a function, the above $d\in b$ is uniquely defined.
We now prove that this set provides a way to interpret the image of
$\tilde{f}$. For simplicity, we will suppress the parameter
$\overrightarrow{w}$.

For every formula $\varphi$,

$\mathcal{N}\Vdash\forall x^{\text{\Large\cjRL{r}}({a})}\forall
y\big{(}\textnormal{{op}}(x,y)\mathop{\varepsilon}\tilde{f}\rightarrow(\varphi(x,y)\rightarrow\varphi(x,\tilde{f}(x)))\big{)}.$

###### Proof.

It will suffice to prove that

$\textnormal{{I}}\Vdash\forall x^{\text{\Large\cjRL{r}}({a})}\forall
y(\neg\varphi(x,\tilde{f}(x))\rightarrow(\varphi(x,y)\rightarrow\textnormal{{op}}(x,y)\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\tilde{f})).$

To do this, fix $c\in a$, $z\in\textnormal{{N}}$, and $d\in B$ such that
$f(c)=d$. Then,
$\lVert\neg\varphi(\text{\Large\cjRL{r}}({c}),\tilde{f}(\text{\Large\cjRL{r}}({c}))\rVert=\lVert\neg\varphi(\text{\Large\cjRL{r}}({c}),\text{\Large\cjRL{r}}({d}))\rVert$.
So, if
$t\Vdash\neg\varphi(\text{\Large\cjRL{r}}({c}),\text{\Large\cjRL{r}}({d}))$,
$s\Vdash\varphi(\text{\Large\cjRL{r}}({c}),z)$ and
$(\textnormal{{op}}(\text{\Large\cjRL{r}}({c}),z),\pi)\in\tilde{f}$ then we
must have that $z=\text{\Large\cjRL{r}}({d})$. Hence, $\textnormal{{I}}\star
t\boldsymbol{.}s\boldsymbol{.}\pi\succ t\star
s\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$. ∎

For every formula $\varphi$,

$\mathcal{N}\Vdash\forall
x^{\text{\Large\cjRL{r}}({a})}\big{(}\varphi(x,\tilde{f}(x))\rightarrow\forall
y(\textnormal{{op}}(x,y)\mathop{\varepsilon}\tilde{f}\rightarrow\varphi(x,y))\big{)}.$

###### Proof.

It will suffice to prove that

$\lambda g\boldsymbol{.}\lambda h\boldsymbol{.}hg\Vdash\forall
x^{\text{\Large\cjRL{r}}({a})}(\varphi(x,\tilde{f}(x))\rightarrow\forall
y(\neg\varphi(x,y)\rightarrow\textnormal{{op}}(x,y)\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\tilde{f})).$

Again, fix $c\in a$ and $d\in b$ such that $f(c)=d$. Next, suppose that
$t\Vdash\varphi(\text{\Large\cjRL{r}}({c}),\text{\Large\cjRL{r}}({d}))$ and
$s\boldsymbol{.}\pi\in\lVert\forall
y(\neg\varphi(\text{\Large\cjRL{r}}({c}),y)\rightarrow\textnormal{{op}}(\text{\Large\cjRL{r}}({c}),y)\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\tilde{f})\rVert$.
Then, for some $z\in\textnormal{{N}}$,
$s\Vdash\neg\varphi(\text{\Large\cjRL{r}}({c}),z)$ and
$(\textnormal{{op}}(\text{\Large\cjRL{r}}({c}),z),\pi)\in\tilde{f}$, from
which it follows that $z=\text{\Large\cjRL{r}}({d})$. Thus $\lambda
g\boldsymbol{.}\lambda h\boldsymbol{.}hg\star
t\boldsymbol{.}s\boldsymbol{.}\pi\succ s\star
t\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$. ∎

As an example of this alternative interpretation we reprove Section 16 to show
that $\text{\Large\cjRL{r}}({b})$ is a codomain of $\tilde{f}$.

$\textnormal{{I}}\Vdash\forall
x^{\text{\Large\cjRL{r}}({a})}(\tilde{f}(x)\mathop{\varepsilon}\text{\Large\cjRL{r}}({b}))$.

###### Proof.

Fix $c\in a$,
$t\Vdash\tilde{f}(c)\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\text{\Large\cjRL{r}}({b})$
and $\pi\in\Pi$. Then
$\lVert\tilde{f}(c)\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\text{\Large\cjRL{r}}({b})\rVert=\lVert\text{\Large\cjRL{r}}({d})\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\text{\Large\cjRL{r}}({b})\rVert$
where $d=f(c)$. But, since $d\in b$, this set is equal to $\Pi$, from which it
follows that $\textnormal{{I}}\star t\boldsymbol{.}\pi\succ
t\star\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$. ∎

##  17 Non-extensional Axiom of Choice and Dependant Choice

In this section we discuss the non-extensional Axiom of Choice, denoted NEAC,
which is a version of the Axiom of Choice that holds in many realizability
models. Assuming full AC in V, Theorem 4.18 of [Kri12] shows that NEAC holds
in any realizability model produced from a countable realizability algebra
which contains the additional instruction “ _quote_ ”. A more generalised
argument is also given in Section 4.2 of [FG20], which adds a generalisation
to quote as well as an additional instruction777which essentially allows one
to realize that $\widehat{\alpha+1}$ is the successor of $\hat{\alpha}$ to
obtain NEAC in realizability models of uncountable size.

Suppose that
$\mathcal{A}=(\Lambda,\Pi,\prec,\mathbin{\text{$\bot\mkern-11.0mu\bot$}})$ is
a countable realizability algebra and let $t\mapsto\eta_{t}$ be an enumeration
of $\Lambda$ in order type $\omega$. Then $\mathcal{A}$ contains the
instruction _quote_ if there exists a special instruction
$\textnormal{{q}}\in\Lambda$ such that for any $t,s\in\Lambda$ and
$\pi\in\Pi$,

$\textnormal{{q}}\star t\boldsymbol{.}s\boldsymbol{.}\pi\succ
t\star\underline{\eta_{s}}\boldsymbol{.}\pi,$

where $\underline{\eta_{s}}$ is Church numeral associated to
$\eta_{s}\in\omega$.

So let us fix a countable realizability algebra $\mathcal{A}$ and suppose that
$\Lambda$ contains the instruction _quote_. NEAC is the statement that every
binary relation can be refined into a (non-extensional)
$\mathop{\varepsilon}$-function. More formally,

NEAC is the statement:

$\forall z\,\exists
f\,(f\subseteq_{\mathop{\varepsilon}}z\land\mathop{\varepsilon}\textnormal{{-Func}}(f)\land\forall
x\forall y\exists
y^{\prime}(\textnormal{{op}}(x,y)\mathop{\varepsilon}z\rightarrow\textnormal{{op}}(x,y^{\prime})\mathop{\varepsilon}f)).$

The extensional version of NEAC (where $f$ is an extensional function) implies
the Axiom of Choice. To see this, suppose $A$ were a family of non-empty sets
and let $z$ be the binary relation defined by $(i,x)\in z$ if and only if
$i\in A\land x\in i$. Now, if we can refine $z$ to an extensional function,
$f$, this will be a choice function for $A$. This is because if $i,j\in A$ and
$i\simeq j$ then $f(i)\simeq f(j)$.

On the other hand, if we can only refine $z$ to a non-extensional
$\mathop{\varepsilon}$-function this will not suffice because we may have
$i\simeq j$ but $f(i)\not\simeq f(j)$. Therefore, we have not chosen a unique
extensional element of each set in $A$.

Suppose that $\mathcal{A}$ is a countable realizability algebra and $\Lambda$
contains a special instruction q satisfying the instruction quote. Then for
any formula $\varphi(u,x_{1},\dots,x_{n})$ in $Fml_{\mathop{\varepsilon}}$
there exists a class function
$g_{\varphi}\colon\omega\times\textnormal{{N}}^{n}\rightarrow\textnormal{{N}}$
such that

$\mathcal{N}\Vdash\forall x_{1},\dots,x_{n}(\exists
u\,\varphi(u,x_{1},\dots,x_{n})\rightarrow\exists
n^{\hat{\omega}}\varphi(\tilde{g}_{\varphi}(n,x_{1},\dots,x_{n}),x_{1},\dots,x_{n})),$

where $\tilde{g}_{\varphi}$ is the lift of $g_{\varphi}$ to a
$\mathop{\varepsilon}$-class function as defined in Section 16.2.

###### Proof.

For simplicity, we will assume that $\varphi(u,x)$ has precisely two free
variables. Fix an enumeration $(\nu_{n}\operatorname{\hskip
1.42271pt\mid\hskip 1.42271pt}n\in\omega)$ of $\Lambda$ and let
$t\mapsto\eta_{t}$ be the inverse of the enumeration (so $\nu_{\eta_{t}}=t$).

Given $n\in\omega$, set $P_{n}\coloneqq\\{\pi\in\Pi\operatorname{\hskip
1.42271pt\mid\hskip
1.42271pt}\nu_{n}\star\underline{n}\boldsymbol{.}\pi\not\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}\\}$.
Now, using the Axiom of Choice, we can define a function
$g_{\varphi}\colon\omega\times\textnormal{{N}}\rightarrow\textnormal{{N}}$
such that for any $a\in\textnormal{{N}}$ and $n\in\omega$, if
$P_{n}\cap\lVert\forall u\neg\varphi(u,a)\rVert\neq\emptyset$ then
$P_{n}\cap\lVert\neg\varphi(g_{\varphi}(n,a),a)\rVert\neq\emptyset$. Finally,
let
$\tilde{g}_{\varphi}\coloneqq\\{(\textnormal{{op}}(\textnormal{{op}}(u,a),g_{\varphi}(u,a)),\pi)\operatorname{\hskip
1.42271pt\mid\hskip 1.42271pt}u,a\in\textnormal{{N}},\pi\in\Pi\\}$ be the lift
of $g_{\varphi}$ to a class $\mathop{\varepsilon}$-function.

It will suffice to show that

$\lambda u\boldsymbol{.}(\textnormal{{q}}u)u\Vdash\forall x\,(\forall
n^{\hat{\omega}}\neg\varphi(\tilde{g}_{\varphi}(n,x),x)\rightarrow\forall
u\neg\varphi(u,x)).$

Suppose, for sake of a contradiction, that this was not the case. Then we can
fix $a\in\textnormal{{N}}$, $t\Vdash\forall
n^{\hat{\omega}}\neg\varphi(\tilde{g}_{\varphi}(n,a),a)$ and
$\pi\in\lVert\forall u\neg\varphi(u,a)\rVert$ such that $\lambda
u\boldsymbol{.}(\textnormal{{q}}u)u\star
t\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$. Next, observe
that from this we obtain

$(\textnormal{{q}}u)u\star t\boldsymbol{.}\pi\succ\textnormal{{q}}\star
t\boldsymbol{.}t\boldsymbol{.}\pi\succ
t\star\underline{\eta_{t}}\boldsymbol{.}\pi\not\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}.$

Therefore $\pi\in P_{\eta_{t}}\cap\lVert\forall u\neg\varphi(u,a)\rVert$. So,
by the construction of $g_{\varphi}$, we can fix some $\sigma\in
P_{\eta_{t}}\cap\lVert\neg\varphi(g_{\varphi}(\eta_{t},a),a)\rVert$. But then
we have the desired contradiction because $\sigma\in P_{\eta_{t}}$ implies
that
$t\star\underline{\eta_{t}}\boldsymbol{.}\sigma\not\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$
while $\underline{\eta_{t}}\boldsymbol{.}\sigma\in\lVert\forall
n^{\hat{\omega}}\neg\varphi(\tilde{g}_{\varphi}(n,a),a)\rVert$ gives us
$t\star\underline{\eta_{t}}\boldsymbol{.}\sigma\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$.
∎

Suppose that $\mathcal{A}$ is a countable realizability algebra and $\Lambda$
contains a special instruction q satisfying the instruction quote. Then
$\mathcal{N}\Vdash\textnormal{{NEAC}}$.

###### Proof.

First, by Section 17, let
$g\colon\omega\times\textnormal{{N}}^{3}\rightarrow\textnormal{{N}}$ be a
$\mathop{\varepsilon}$-function such that

$\mathcal{N}\Vdash\forall z\forall x(\exists
u(\textnormal{{op}}(x,u)\mathop{\varepsilon}z)\rightarrow\exists
n^{\hat{\omega}}(\textnormal{{op}}(x,\tilde{g}(n,z,x))\mathop{\varepsilon}z)).$

Now, working within any model of the realized theory, since $\hat{\omega}$ is
a Trichotomous $\mathop{\varepsilon}$-ordinal (Section 13.3) it satisfies the
Least Ordinal Principle (Section 13.3); if $\exists
u(\textnormal{{op}}(x,u)\mathop{\varepsilon}z)$ then $\exists
n\in\hat{\omega}$ such that
$\textnormal{{op}}(x,\tilde{g}(n,z,x))\mathop{\varepsilon}z$ and for all
$m<n$, $\textnormal{{op}}(x,\tilde{g}(m,z,x))\mathop{\varepsilon}z$.

Therefore, we can define a function $f$ in $\mathcal{N}$ such that
$\textnormal{{op}}(x,y)\mathop{\varepsilon}f$ if and only if
$\textnormal{{op}}(x,y)\mathop{\varepsilon}z$ and $y=\tilde{g}(n,z,x)$ where
$n$ is the minimal such element of $\hat{\omega}$ (whenever it exists).
Clearly, we have $f\subseteq_{\mathop{\varepsilon}}z$ and for any $x,y$ there
exists some $y^{\prime}$ such that if
$\textnormal{{op}}(x,y)\mathop{\varepsilon}z$ then
$\textnormal{{op}}(x,y^{\prime})\mathop{\varepsilon}z$.

To show that $f$ is a $\mathop{\varepsilon}$-function, suppose that
$\textnormal{{op}}(x,y)\mathop{\varepsilon}f$ and
$\textnormal{{op}}(x,y^{\prime})\mathop{\varepsilon}f$. Then
$y=\tilde{g}(n,z,x)$ and $y^{\prime}=\tilde{g}(n^{\prime},z,x)$ for some
$n,n^{\prime}\mathop{\varepsilon}\hat{\omega}$ both of which are minimal.
Since they are both minimal and $\hat{\omega}$ is extensionally an ordinal, in
the extensional structure it must be the case that $n\simeq n^{\prime}$ and
therefore $n=n^{\prime}$ by Section 13.3. ∎

$\operatorname{\textnormal{{ZF}}_{\varepsilon}}\vdash\textnormal{{NEAC}}\rightarrow\textnormal{{DC}}_{\in}$.
Hence, if $\mathcal{A}$ is a countable realizability algebra and $\Lambda$
contains a special instruction q satisfying the instruction quote, then the
extensional version of DC is realized in $\mathcal{N}$.

###### Proof.

We take $\textnormal{{DC}}_{\in}$ in the following form:

$\forall a\forall R(\forall x\in a\exists y\in a\,\textnormal{{op}}(x,y)\in
R\\\ \rightarrow\exists g(\textnormal{{Ext-Func}}(g)\land
g\colon\hat{\omega}\rightarrow a\land\forall
n\in\hat{\omega}\,\textnormal{{op}}(g(n),g(n+1))\in R)).$

Fixing $a$ and $R$, suppose that $\forall x\in a\exists y\in
a\,\textnormal{{op}}(x,y)\in R$ and set

$z\coloneqq\bigcup_{x\in a}\\{\textnormal{{op}}(x,y)\operatorname{\hskip
1.42271pt\mid\hskip 1.42271pt}y\in a\land\textnormal{{op}}(x,y)\in R\\}.$

By NEAC we can fix a non-extensional function
$f\subseteq_{\mathop{\varepsilon}}z$ which refines the relation $z$. Now, fix
$x\mathop{\varepsilon}a$. Then we can define a function
$g\colon\hat{\omega}\rightarrow a$ recursively by setting $g(0)=x$ and
$g(n+1)$ to be the unique $y$ such that
$\textnormal{{op}}(g(n),y)\mathop{\varepsilon}f$, where we observe that
uniqueness follows from $f$ being a non-extensional function. To see that $g$
is the required extensional function, we first have that $g$ is clearly a
total function on $\hat{\omega}$ since $f\subseteq_{\mathop{\varepsilon}}z$.
Now, fix $n,n^{\prime}\mathop{\varepsilon}\hat{\omega}$ and
$y,y^{\prime}\mathop{\varepsilon}a$ and suppose that $n\simeq n^{\prime}$,
$\textnormal{{op}}(n,y)\mathop{\varepsilon}g$ and
$\textnormal{{op}}(n^{\prime},y^{\prime})\mathop{\varepsilon}g$. Then, by
Section 13.3, we must have that $n=n^{\prime}$ and therefore $y=y^{\prime}$.
In particular, this means that $y\simeq y^{\prime}$, so $g$ is indeed
extensional. ∎

##  18 Non-trivial Realizability Models

Here we repeat the analysis from Section 4 of [Kri18] to show that it is
possible to produce a non-trivial realizability model such that the Boolean
algebra $\text{\Large\cjRL{r}}({2})$ has exactly $4$ elements. To produce this
model we will use the first three Church numerals; $\underline{0}=\lambda
u\boldsymbol{.}\lambda v\boldsymbol{.}v$, $\underline{1}=\lambda
u\boldsymbol{.}\lambda v\boldsymbol{.}uv$ and $\underline{2}=\lambda
u\boldsymbol{.}\lambda v\boldsymbol{.}(\underline{1}u)(uv)=\lambda
u\boldsymbol{.}\lambda v\boldsymbol{.}u(uv)$. We begin with the observation by
Krivine that while $\text{\Large\cjRL{r}}({2})$ may contain
$\mathop{\varepsilon}$-elements which are neither $\text{\Large\cjRL{r}}({0})$
or $\text{\Large\cjRL{r}}({1})$, all such sets are empty.

$\textnormal{{I}}\Vdash\forall x^{\text{\Large\cjRL{r}}({2})}\forall
y(x\neq\text{\Large\cjRL{r}}({1})\rightarrow
y\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}x)$.

###### Proof.

By Section 10.1 it suffices to prove the claim for
$x=\text{\Large\cjRL{r}}({0})$ and $x=\text{\Large\cjRL{r}}({1})$. Firstly, if
$x=\text{\Large\cjRL{r}}({0})$ then $\lVert
a\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\text{\Large\cjRL{r}}({0})\rVert=\emptyset$
for any $a\in\textnormal{{N}}$ and thus $\lVert\forall
y(\text{\Large\cjRL{r}}({0})\neq\text{\Large\cjRL{r}}({1})\rightarrow
y\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\text{\Large\cjRL{r}}({0}))\rVert=\emptyset$.
Therefore, in this case any term realizes the statement. On the other hand, if
$x=\text{\Large\cjRL{r}}({1})$ then
$\lVert\text{\Large\cjRL{r}}({1})\neq\text{\Large\cjRL{r}}({1})\rVert=\Pi$.
Therefore, for any $a\in\textnormal{{N}}$, if
$t\Vdash\text{\Large\cjRL{r}}({1})\neq\text{\Large\cjRL{r}}({1})$ and
$(a,\pi)\in\text{\Large\cjRL{r}}({1})$, $\textnormal{{I}}\star
t\boldsymbol{.}\pi\in\Pi$. Thus I realizes the statement. ∎

Say that $(\bar{\Lambda},\bar{\Pi})$ is _generated_ by $(T,X)$ if
$\bar{\Lambda}$ and $\bar{\Pi}$ are the smallest classes satisfying:

  * •

$\forall t\in T\;t\in\bar{\Lambda}$,

  * •

$\forall\omega\in X\;\omega\in\bar{\Pi}$,

  * •

Every variable is in $\bar{\Lambda}$,

  * •

If $t,s\in\bar{\Lambda}$ then $ts\in\bar{\Lambda}$,

  * •

If $u$ is a variable and $t\in\bar{\Lambda}$ then $\lambda
u\boldsymbol{.}t\in\bar{\Lambda}$,

  * •

$\textnormal{{{cc}}}\in\bar{\Lambda}$,

  * •

$\forall\pi\in\bar{\Pi}\;\textnormal{{k}}_{\pi}\in\bar{\Lambda}$,

  * •

If $t\in\bar{\Lambda}$ and $\pi\in\bar{\Pi}$ then
$t\boldsymbol{.}\pi\in\bar{\Pi}$.

Namely, $(\bar{\Lambda},\bar{\Pi})$ is generated by $(T,X)$ if the collection
of special instructions is contained in $T$ and the collection of stack
constants is contained in $X$.

We consider the realizability algebra
$\mathcal{A}=(\Lambda,\Pi,\prec,\mathbin{\text{$\bot\mkern-11.0mu\bot$}})$
given as follows:

  * •

$(\Lambda,\Pi)$ is generated by
$(\\{\textnormal{{d}}\\},\\{\pi^{0},\pi^{1}\\})$. That is, there is exactly
one special instruction, d and exactly two stack constants, $\pi^{0}$ and
$\pi^{1}$.

  * •

For $i\in\\{0,1\\}$ we let $(\Lambda^{i},\Pi^{i})$ be the sets generated by
$(\\{\textnormal{{d}}\\},\\{\pi^{i}\\})$.

  * •

For $i,j\in\\{0,1\\}$ we define
$\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{j}$ to be the least set
$P\subseteq\Lambda^{i}\star\Pi^{i}$ such that:

    1. 1.

$\textnormal{{d}}\star\underline{j}\boldsymbol{.}\pi\in P$ for every
$\pi\in\Pi^{i}$,

    2. 2.

If $t\star\pi\in\Lambda^{i}\star\Pi^{i}$ and $s\star\sigma\in P$ then
$t\star\pi\succ s\star\sigma\Rightarrow t\star\pi\in P$,

    3. 3.

If at least two out of the three processes $t\star\pi$, $s\star\pi$,
$r\star\pi$ are in $P$ then
$\textnormal{{d}}\star\underline{2}\boldsymbol{.}t\boldsymbol{.}s\boldsymbol{.}r\boldsymbol{.}\pi\in
P$.

  * •

$\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$ is defined by
$(\Lambda\star\Pi)\setminus\mathbin{\text{$\bot\mkern-11.0mu\bot$}}=(\Lambda^{0}\star\Pi^{0})\setminus\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{0}_{0}\,\cup\,(\Lambda^{1}\star\Pi^{1})\setminus\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{1}_{1}$.
That is, a process $t\star\pi$ is in
$\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$ if and only if either:

    1. 1.

$t\star\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{0}_{0}\cup\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{1}_{1}$,

    2. 2.

$t\star\pi\in(\Lambda\star\Pi)\setminus(\Lambda^{0}\star\Pi^{0}\cup\Lambda^{1}\star\Pi^{1})$,
i.e. both stack constants $\pi^{0}$ and $\pi^{1}$ appear in $t\star\pi$.

Since there is no additional requirement on d in terms of how it interacts
with the pre-order,

$\textnormal{{d}}\star\pi\succ
s\star\sigma\quad\Longleftrightarrow\quad\textnormal{{d}}\star\pi=s\star\sigma.$

Also, by the minimality requirement on the ordering, for any processes
$t\star\pi$ and $s\star\sigma$, if $t\star\pi\succ s\star\sigma$ then there
must exist a finite sequence

$t\star\pi=t_{0}\star\pi_{0}\succ_{1}\dots\succ_{1}t_{k}\star\pi_{k}=s\star\sigma$

of distinct processes such that each reduction
$t_{n}\star\pi_{n}\succ_{1}t_{n+1}\star\pi_{n+1}$ is a one-step evaluation
given by one of the defining constraints on $\succ_{1}$. In this case the only
restrains on $\succ_{1}$ are the four basic requirements of push, grab, save,
and restore. Moreover, by inspection, it is clear that only one of these can
give a possible reduction of a given term and thus this finite sequence is
uniquely determined. From this we can conclude that (again, for this
realizability algebra):

  * •

If $t\star\pi\succ s\star\sigma$ then there is no infinite sequence of
distinct processes $(t_{n}\star\pi_{n}\operatorname{\hskip 1.42271pt\mid\hskip
1.42271pt}n\in\omega)$ such that $t\star\pi=t_{0}\star\pi_{0}\succ
t_{1}\star\pi_{1}\succ\dots\succ t_{n}\star\pi_{n}\succ\dots\succ
s\star\sigma$.

  * •

If $t\star\pi\succ s\star\sigma$ and $t\star\pi\succ r\star\tau$ then either
$s\star\sigma\succ r\star\tau$ or $r\star\tau\succ s\star\sigma$.

Due to the nature of the structure, there is an obvious isomorphism between
$\Lambda^{0}\star\Pi^{0}$ and $\Lambda^{1}\star\Pi^{1}$, which is the one
generated by sending $\pi^{0}$ to $\pi^{1}$. Namely, define
$\Xi\coloneqq\Lambda^{0}\cup\Pi^{0}\rightarrow\Lambda^{1}\cup\Pi^{1}$
recursively by the following rules:

  * •

$\Xi(\pi^{0})=\pi^{1}$;

  * •

If $u$ is a variable, then $\Xi(u)=u$;

  * •

If $u$ is a variable and $t\in\Lambda^{0}$, then $\Xi(\lambda
u\boldsymbol{.}t)=\lambda u\boldsymbol{.}\Xi(t)$;

  * •

If $u$ is a variable and $t,s\in\Lambda^{0}$, then $\Xi(t[u\coloneqq
s])=\Xi(t)[u\coloneqq\Xi(s)]$;

  * •

If $s,t\in\Lambda^{0}$, then $\Xi(ts)=\Xi(t)(\Xi(s))$;

  * •

$\Xi(\textnormal{{{cc}}})=\textnormal{{{cc}}}$ and
$\Xi(\textnormal{{d}})=\textnormal{{d}}$;

  * •

If $\pi\in\Pi^{0}$, then
$\Xi(\textnormal{{k}}_{\pi})=\textnormal{{k}}_{\Xi(\pi)}$;

  * •

If $t\in\Lambda^{0}$, and $\pi\in\Pi^{0}$ then
$\Xi(t\boldsymbol{.}\pi)=\Xi(t)\boldsymbol{.}\Xi(\pi)$.

This then extends to
$\Xi\colon\Lambda^{0}\star\Pi^{0}\rightarrow\Lambda^{1}\star\Pi^{1}$ by
$\Xi(t\star\pi)=\Xi(t)\star\Xi(\pi)$. We now see that this map provides an
isomorphism between the structures.

For all $t\star\pi,s\star\sigma\in\Lambda^{0}\star\Pi^{0}$, $s\star\sigma\succ
t\star\pi$ if and only if $\Xi(s\star\sigma)\succ\Xi(t\star\pi)$.

###### Proof.

It suffices to prove the equivalence for the four basic constraints, which
follow from the following observations:

$\Xi\big{(}ts\star\pi\big{)}=\Xi(ts)\star\Xi(\pi)=\Xi(t)(\Xi(s))\star\Xi(\pi)\succ\Xi(t)\star\Xi(s)\boldsymbol{.}\Xi(\pi)=\Xi(t\star
s\boldsymbol{.}\pi)$.

$\Xi(\lambda u\boldsymbol{.}t\star s\boldsymbol{.}\pi)=\lambda
u\boldsymbol{.}\Xi(t)\star\Xi(s)\boldsymbol{.}\Xi(\pi)\succ\Xi(t)[u\coloneqq\Xi(s)]\star\Xi(\pi)=\Xi(t[u\coloneqq
s]\star\pi)$.

$\Xi(\textnormal{{{cc}}}\star
t\boldsymbol{.}\pi)=\textnormal{{{cc}}}\star\Xi(t)\boldsymbol{.}\Xi(\pi)\succ\Xi(t)\star\textnormal{{k}}_{\Xi(\pi)}\boldsymbol{.}\Xi(\pi)=\Xi(t\star\textnormal{{k}}_{\pi}\boldsymbol{.}\pi)$.

$\Xi(\textnormal{{k}}_{\sigma}\star
t\boldsymbol{.}\pi)=\textnormal{{k}}_{\Xi(\sigma)}\star\Xi(t)\boldsymbol{.}\Xi(\pi)\succ\Xi(t)\star\Xi(\sigma)=\Xi(t\star\sigma)$.
∎

For $j\in\\{0,1\\}$,
$\Xi\textnormal{``}\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{0}_{j}=\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{1}_{j}$.

###### Proof.

Fix $j\in\\{0,1\\}$. Let
$B^{i}\coloneqq\\{\textnormal{{d}}\star\underline{j}\boldsymbol{.}\pi\operatorname{\hskip
1.42271pt\mid\hskip 1.42271pt}\pi\in\Pi^{i}\\}$, and for any collection of
processes $X$ let

$G_{0}(X)\coloneqq\\{t\star\pi\operatorname{\hskip 1.42271pt\mid\hskip
1.42271pt}\exists s\star\sigma\in X\;(t\star\pi\succ s\star\sigma)\\}$

and

$G_{1}(X)\coloneqq\\{\textnormal{{d}}\star\underline{2}\boldsymbol{.}t\boldsymbol{.}s\boldsymbol{.}r\boldsymbol{.}\pi\operatorname{\hskip
1.42271pt\mid\hskip 1.42271pt}\text{at least two of
}t\star\pi,s\star\sigma\text{ and }r\star\pi\text{ are in }X\\}.$

It is then clear by the construction of
$\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{j}$ that if we set
$T^{i}_{0}=B^{i}$ and $T^{i}_{n+1}=G_{0}(T^{i}_{n})\cup G_{1}(T^{i}_{n})$ then
$\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{j}=\bigcup_{n\in\omega}T^{i}_{n}$.
We shall inductively show that $\Xi\textnormal{``}T^{0}_{n}=T^{1}_{n}$ and
thus
$\Xi\textnormal{``}\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{0}_{j}=\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{1}_{j}$.
For this it suffices to only prove that $\Xi\textnormal{``}T^{0}_{n}\subseteq
T^{1}_{n}$, with the reverse inclusion following by considering the inverse of
$\Xi$.

Take $\textnormal{{d}}\star\underline{j}\boldsymbol{.}\pi\in T^{0}_{0}$. Then,
since $\underline{j}$ is a $\lambda_{c}$-term which contains no appearance of
$\pi^{0}$ or $\pi^{1}$,
$\Xi(\textnormal{{d}}\star\underline{j}\boldsymbol{.}\pi)=\textnormal{{d}}\star\underline{j}\boldsymbol{.}\Xi(\pi)\in
T^{1}_{0}$.

Next, suppose that $t\star\pi\in G_{0}(T^{0}_{n})$ and fix $s\star\sigma\in
T^{0}_{n}$ such that $t\star\pi\succ s\star\sigma$. Then, by the inductive
hypothesis, $\Xi(s\star\sigma)\in T^{1}_{n}$ and, by Section 18,
$\Xi(t\star\pi)\succ\Xi(s\star\sigma)$. Thus, $\Xi(t\star\pi)\in
G_{0}(T^{1}_{n}).$

Finally, suppose that
$\textnormal{{d}}\star\underline{2}\boldsymbol{.}t\boldsymbol{.}s\boldsymbol{.}r\boldsymbol{.}\pi\in
G_{1}(T^{0}_{n})$. Without loss of generality, we shall assume that
$t\star\pi$ and $s\star\pi$ are in $T^{0}_{n}$. Then, by the inductive
hypothesis, $\Xi(t\star\pi)=\Xi(t)\star\Xi(\pi)$ and
$\Xi(s\star\sigma)=\Xi(s)\star\Xi(\sigma)$ are in $T^{1}_{n}$. Thus,
$\Xi(\textnormal{{d}}\star\underline{2}\boldsymbol{.}t\boldsymbol{.}s\boldsymbol{.}r\boldsymbol{.}\pi)=\textnormal{{d}}\star\underline{2}\boldsymbol{.}\Xi(t)\boldsymbol{.}\Xi(s)\boldsymbol{.}\Xi(r)\boldsymbol{.}\Xi(\pi)\in
G_{1}(T^{1}_{n})$. ∎

If $t\star\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{j}$ and
$t\star\pi\succ s\star\sigma$, then
$s\star\sigma\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{j}$.

###### Proof.

Suppose for a contradiction that $t\star\pi\succ s\star\sigma$ and
$t\star\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{j}$ but
$s\star\sigma\not\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{j}$. Using
Section 18, without loss of generality we can suppose that $t\star\pi\succ
s\star\sigma$ by exactly one of the basic reduction steps. We shall show that
$Q=\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{j}\setminus\\{t\star\pi\\}$
satisfies the three conditions in the definition of
$\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{j}$, contradicting the
minimality requirement.

  1. 1.

Take $\tau\in\Pi^{i}$. If
$t\star\pi=\textnormal{{d}}\star\underline{j}\boldsymbol{.}\tau$ then
$\textnormal{{d}}\star\underline{j}\boldsymbol{.}\tau\succ s\star\sigma$.
Therefore, again by the remark,
$s\star\sigma=\textnormal{{d}}\star\underline{j}\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{j}$,
contradicting the assumption on $s\star\sigma$. Thus,
$\textnormal{{d}}\star\underline{j}\boldsymbol{.}\tau\in Q$.

  2. 2.

Assume that $r\star\tau\in\Lambda^{i}\star\Pi^{i}$,
$r^{\prime}\star\tau^{\prime}\in Q$ and $r\star\tau\succ
r^{\prime}\star\tau^{\prime}$. Then
$r\star\tau\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{j}$. Now, if
$r\star\tau=t\star\pi$ then $t\star\pi\succ r^{\prime}\star\tau^{\prime}$ and
$t\star\pi\succ s\star\sigma$. Therefore, since the second one of these was
assumed to be a one step reduction, we must have that $s\star\sigma\succ
r^{\prime}\star\tau^{\prime}$. Therefore, by the second condition in the
definition of $\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{j}$,
$s\star\sigma\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{j}$, which is
again a contradiction. Thus, $r\star\tau\in Q$.

  3. 3.

Suppose at least two of $r\star\tau$, $u\star\tau$ and $v\star\tau$ were in
$Q$. Then
$\textnormal{{d}}\star\underline{2}\boldsymbol{.}r\boldsymbol{.}u\boldsymbol{.}v\boldsymbol{.}\tau\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{j}$.
Now, suppose that
$\textnormal{{d}}\star\underline{2}\boldsymbol{.}r\boldsymbol{.}u\boldsymbol{.}v\boldsymbol{.}\tau=t\boldsymbol{.}\pi$.
Then
$\textnormal{{d}}\star\underline{2}\boldsymbol{.}r\boldsymbol{.}u\boldsymbol{.}v\boldsymbol{.}\tau\succ
s\star\sigma$ and thus
$s\star\sigma=\textnormal{{d}}\star\underline{2}\boldsymbol{.}r\boldsymbol{.}u\boldsymbol{.}v\boldsymbol{.}\tau\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{j}$,
which is a contradiction. Thus,
$\textnormal{{d}}\star\underline{2}\boldsymbol{.}r\boldsymbol{.}u\boldsymbol{.}v\boldsymbol{.}\tau\in
Q$.

∎

For $i\in\\{0,1\\}$,
$\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{0}\cap\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{1}=\emptyset$.

###### Proof.

We first show that for any $\pi\in\Pi^{i}$,
$\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{1}\setminus\\{\textnormal{{d}}\star\underline{0}\boldsymbol{.}\pi\\}$
satisfies the three conditions for the definition of
$\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{1}$ and therefore, by the
minimality requirement,
$\textnormal{{d}}\star\underline{0}\boldsymbol{.}\pi\not\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{1}$.

  * •

For any $\sigma\in\Pi^{i}$,
$\textnormal{{d}}\star\underline{1}\boldsymbol{.}\sigma\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{1}$
and
$\textnormal{{d}}\star\underline{1}\boldsymbol{.}\sigma\neq\textnormal{{d}}\star\underline{0}\boldsymbol{.}\pi$,
so $\textnormal{{d}}\star\underline{1}\boldsymbol{.}\sigma$ is in the set.

  * •

Suppose $s\star\sigma\in\Lambda^{i}\star\Pi^{i}$,
$r\star\tau\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{1}\setminus\\{\textnormal{{d}}\star\underline{0}\boldsymbol{.}\pi\\}$
and $s\star\sigma\succ r\star\tau$. Then
$s\star\sigma\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{1}$ so, if
$s\star\sigma=\textnormal{{d}}\star\underline{0}\boldsymbol{.}\pi$, then
$\textnormal{{d}}\star\underline{0}\boldsymbol{.}\pi\succ r\star\tau$ and
therefore
$d\star\underline{0}\boldsymbol{.}\pi=r\star\tau\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{1}\setminus\\{d\star\underline{0}\boldsymbol{.}\pi\\}$,
which is a contradiction. Thus
$s\star\sigma\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{1}\setminus\\{\textnormal{{d}}\star\underline{0}\boldsymbol{.}\pi\\}$.

  * •

Suppose at least two of $t\star\sigma$, $s\star\sigma$ and $r\star\sigma$ were
in
$\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{1}\setminus\\{\textnormal{{d}}\star\underline{0}\boldsymbol{.}\pi\\}$.
Then
$\textnormal{{d}}\star\underline{2}\boldsymbol{.}t\boldsymbol{.}s\boldsymbol{.}r\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{1}$
and
$\textnormal{{d}}\star\underline{2}\boldsymbol{.}t\boldsymbol{.}r\boldsymbol{.}s\boldsymbol{.}\pi\neq\textnormal{{d}}\star\underline{0}\boldsymbol{.}\pi$.

We shall now prove that
$\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{0}\subseteq(\Lambda^{i}\star\Pi^{i})\setminus\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{1}$.
To do this, it suffices to prove that
$\Lambda^{i}\star\Pi^{i}\setminus\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{1}$
satisfies the three defining properties for
$\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{0}$.

  * •

By the first claim, we have that for any $\pi\in\Pi$,
$\textnormal{{d}}\star\underline{0}\boldsymbol{.}\pi\in(\Lambda^{i}\star\Pi^{i})\setminus\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{1}$.

  * •

Suppose that $t\star\pi\in\Lambda^{i}\star\Pi^{i}$,
$s\star\sigma\in(\Lambda^{i}\star\Pi^{i})\setminus\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{1}$
and $t\star\pi\succ s\star\sigma$. If $t\star\pi$ were in
$\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{1}$ then, by Section 18,
$s\star\sigma$ would also be in
$\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{1}$, which is a contradiction.

  * •

Suppose that $t\star\pi$, $s\star\pi$, $r\star\pi$ were all in
$\Lambda^{i}\star\Pi^{i}$ but
$t\star\pi,s\star\pi\not\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{1}$.
We shall show that
$\textnormal{{d}}\star\underline{2}\boldsymbol{.}t\boldsymbol{.}s\boldsymbol{.}r\boldsymbol{.}\pi\not\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{1}$.
As per usual, this will be done by showing that
$\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{1}\setminus\\{\textnormal{{d}}\star\underline{2}\boldsymbol{.}t\boldsymbol{.}s\boldsymbol{.}r\boldsymbol{.}\pi\\}$
satisfies the three defining properties for
$\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{1}$:

    * –

For any $\sigma\in\Pi^{i}$,
$\textnormal{{d}}\star\underline{1}\boldsymbol{.}\sigma\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{1}\setminus\\{\textnormal{{d}}\star\underline{2}\boldsymbol{.}t\boldsymbol{.}s\boldsymbol{.}r\boldsymbol{.}\pi\\}$.

    * –

Suppose $u\star\sigma\in\Lambda^{i}\star\Pi^{i}$, $u\star\sigma\succ
v\star\tau$ and
$v\star\tau\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{1}\setminus\\{\textnormal{{d}}\star\underline{2}\boldsymbol{.}t\boldsymbol{.}s\boldsymbol{.}r\boldsymbol{.}\pi\\}$.
Then $u\star\sigma\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{1}$. Now,
if
$u\star\sigma=\textnormal{{d}}\star\underline{2}\boldsymbol{.}t\boldsymbol{.}s\boldsymbol{.}r\boldsymbol{.}\pi$
then
$v\star\tau=\textnormal{{d}}\star\underline{2}\boldsymbol{.}t\boldsymbol{.}s\boldsymbol{.}r\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{1}\setminus\\{\textnormal{{d}}\star\underline{2}\boldsymbol{.}t\boldsymbol{.}s\boldsymbol{.}r\boldsymbol{.}\pi\\}$,
which is a contradiction.

    * –

Suppose at least two of $u_{1}\star\sigma$, $u_{2}\star\sigma$ and
$u_{3}\star\sigma$ were in
$\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{1}\setminus\\{\textnormal{{d}}\star\underline{2}\boldsymbol{.}t\boldsymbol{.}s\boldsymbol{.}r\boldsymbol{.}\pi\\}$.
Then
$\textnormal{{d}}\star\underline{2}\boldsymbol{.}u_{1}\boldsymbol{.}u_{2}\boldsymbol{.}u_{3}\boldsymbol{.}\sigma\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{1}$.
Now, if
$\textnormal{{d}}\star\underline{2}\boldsymbol{.}u_{1}\boldsymbol{.}u_{2}\boldsymbol{.}u_{3}\boldsymbol{.}\sigma=\textnormal{{d}}\star\underline{2}\boldsymbol{.}t\boldsymbol{.}s\boldsymbol{.}r\boldsymbol{.}\pi$
then we must have that $u_{1}=t$, $u_{2}=s$, $u_{3}=r$, and $\sigma=\pi$.
Therefore, at least one of $t\star\pi$ and $s\star\pi$ is in
$\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{1}$, which contradicts our
initial assumption.

∎

$\mathcal{A}$ is a coherent realizability algebra.

###### Proof.

Let $t\in\mathcal{R}$ be a realizer and suppose that
$t\star\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$ for every $\pi\in\Pi$.
As $t$ is a realizer, note that $t$ cannot contain any instance of
$\textnormal{{k}}_{\pi^{0}}$ or $\textnormal{{k}}_{\pi^{1}}$ and therefore
$t\star\pi^{i}\in\Lambda^{i}\star\Pi^{i}$ for $i\in\\{0,1\\}$. In particular,
$t\in\Lambda^{0}\cap\Lambda^{1}$ and therefore
$t\star\pi^{0}\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{0}_{0}$ and
$t\star\pi^{1}\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{1}_{1}$. Moreover,
the isomorphism $\Xi$ must fix $t$ and therefore
$\Xi(t\star\pi^{0})=t\star\pi^{1}$. Thus, by Section 18,
$t\star\pi^{1}\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{1}_{0}$ which means
that
$t\star\pi^{1}\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{1}_{0}\cap\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{1}_{1}$,
contradicting Section 18. ∎

$\textnormal{{d}}(\underline{2})\Vdash\text{``the Boolean algebra
}\text{\Large\cjRL{r}}({2})\text{ has at most four
}\mathop{\varepsilon}\text{{-}elements''}$.

###### Proof.

We shall show that

$\textnormal{{d}}(\underline{2})\Vdash\forall
x^{\text{\Large\cjRL{r}}({2})}\,\forall
y^{\text{\Large\cjRL{r}}({2})}\,(x\neq\text{\Large\cjRL{r}}({0})\land
y\neq\text{\Large\cjRL{r}}({1})\land x\neq y\rightarrow x\land y\neq x).$

To see why this suffices, first observe that if $\mathbb{B}$ is a Boolean
algebra and there exists an $a$ such that $\mathbb{0}<a<\mathbb{1}$ and both
$a$ and $-a$ are atoms888$a$ is said to be an atom is whenever $b<a$ then
$b=\mathbb{0}$, then $|\mathbb{B}|=4$. So suppose that $|\mathbb{B}|>4$ and
fix $x$ such that $\mathbb{0}<x<\mathbb{1}$ and $x$ is not an atom. This means
that we can fix $y\in\mathbb{B}$ such that $\mathbb{0}<y<x$. Then $x,y$
witness the failure of the above statement.

To prove the claim, let $m,n\in\\{0,1\\}$,
$t\Vdash\text{\Large\cjRL{r}}({m})\neq\text{\Large\cjRL{r}}({0})$,
$s\Vdash\text{\Large\cjRL{r}}({n})\neq\text{\Large\cjRL{r}}({1})$,
$r\Vdash\text{\Large\cjRL{r}}({m})\neq\text{\Large\cjRL{r}}({n})$ and
$\pi\in\lVert\text{\Large\cjRL{r}}({m})\land\text{\Large\cjRL{r}}({n})\neq\text{\Large\cjRL{r}}({m})\rVert$.
Since
$\lVert\text{\Large\cjRL{r}}({m})\land\text{\Large\cjRL{r}}({n})\neq\text{\Large\cjRL{r}}({m})\rVert\neq\emptyset$,
by definition
$\text{\Large\cjRL{r}}({m})\land\text{\Large\cjRL{r}}({n})=\text{\Large\cjRL{r}}({m})$,
from which it follows that $m\leq n$. There are then three possible cases for
$(m,n)$, $(0,0)$, $(0,1)$ and $(1,1)$, and in all of these cases at least two
of the terms $t,s,r$ realize $\perp$ and thus the resulting term is in
$\mathbin{\text{$\bot\mkern-11.0mu\bot$}}^{i}_{j}$ for any $i,j\in\\{0,1\\}$.
Hence, by the construction of the realizability model,
$\textnormal{{d}}\star\underline{2}\boldsymbol{.}t\boldsymbol{.}s\boldsymbol{.}r\boldsymbol{.}\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$.
∎

The Boolean algebra $\text{\Large\cjRL{r}}({2})$ has exactly four
$\mathop{\varepsilon}$-elements.

###### Proof.

We begin by defining two elements of N:

$\gamma_{0}=(\\{\text{\Large\cjRL{r}}({0})\\}\times\Pi^{0})\cup(\\{\text{\Large\cjRL{r}}({1})\\}\times\Pi^{1})\qquad\gamma_{1}=(\\{\text{\Large\cjRL{r}}({1})\\}\times\Pi^{0})\cup(\\{\text{\Large\cjRL{r}}({0})\\}\times\Pi^{1}).$

By construction, we have that
$\gamma_{0},\gamma_{1}\subseteq\text{\Large\cjRL{r}}({2})$. Now:

  * •

$\textnormal{{I}}\Vdash\neg\forall
x^{\text{\Large\cjRL{r}}({2})}(x\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\gamma_{0})$.
To see this, let $t\Vdash\forall
x^{\text{\Large\cjRL{r}}({2})}(x\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\gamma_{0})$
and $\pi\in\Pi$. If $\pi\in\Pi\setminus(\Pi^{0}\cup\Pi^{1})$ then
$t\star\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$ by definition. So
suppose that $\pi\in\Pi^{0}\cup\Pi^{1}$. Then, since $\lVert\forall
x^{\text{\Large\cjRL{r}}({2})}(x\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\gamma_{0})\rVert=\bigcup_{i\in
2}\lVert\text{\Large\cjRL{r}}({i})\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\gamma_{0}\rVert=\Pi^{0}\cup\Pi^{1}$,
we must also have that $t\star\pi\in\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$
as required.

  * •

$\textnormal{{d}}(\underline{0})\Vdash\text{\Large\cjRL{r}}({0})\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\gamma_{0}$
and
$\textnormal{{d}}(\underline{1})\Vdash\text{\Large\cjRL{r}}({1})\mathrel{\ooalign{\hfil$\varepsilon$\hfil\cr\hfil$/$\hfil\cr}}\gamma_{0}$,

Therefore $\gamma_{0}$ is not $\mathop{\varepsilon}$-empty and every
$\mathop{\varepsilon}$-element of $\gamma_{0}$ is not equal to
$\text{\Large\cjRL{r}}({0})$ or $\text{\Large\cjRL{r}}({1})$. Hence, we must
have that $\mathcal{N}\Vdash\exists
x(x\mathop{\varepsilon}\text{\Large\cjRL{r}}({2})\land
x\neq\text{\Large\cjRL{r}}({0})\land x\neq\text{\Large\cjRL{r}}({1}))$ from
which we can conclude that $\text{\Large\cjRL{r}}({2})$ has size precisely $4$
in $\mathcal{N}$. ∎

In fact, as proven in [Kri18], one can realize that $\gamma_{0}$ and
$\gamma_{1}$ are singletons and therefore their
$\mathop{\varepsilon}$-elements are precisely the two atoms of
$\text{\Large\cjRL{r}}({2})$.

##  19 Forcing as a Realizability Algebra

It is claimed that realizability is a generalisation of the method of forcing
because any forcing Boolean algebra can be naturally seen as a realizability
algebra. In this section we explicitly describe this translation, the
presentation of which comes from [FG20], and expand on the previous work in
order to formally state the relationship between forcing and realizability
models. We will also assume a lot of background material about Boolean
algebras and Boolean valued models, and we refer the reader to Chapters 7 and
14 of [Jec03] for the necessary background. It is worthwhile to clearly state
here that while such a translation exists, the resulting realizability model “
_loses its computation content_ ”. By this we mean there is essentially a
unique realizer for all realized statements in the model so from a realizer
for a proof we can not extract any computational data.

Let $\mathbb{B}=(\mathbb{B},\mathbb{1},\mathbb{0},\land,\lor,\neg)$ be a
complete Boolean algebra. We define a realizability algebra
$\mathcal{A}_{\mathbb{B}}=(\Lambda_{(A,B)},\Pi_{(A,B)},\prec,\mathbin{\text{$\bot\mkern-11.0mu\bot$}})$
as follows: Firstly, set $A=\emptyset$, that it to say there are no special
instructions. Next, let $(\omega_{p}\operatorname{\hskip 1.42271pt\mid\hskip
1.42271pt}p\in\mathbb{B})$ be the set of stack bottoms under some fixed
enumeration. To define the pre-order and the pole, we begin by inductively
defining a function
$\tau\colon\Lambda^{\textnormal{{open}}}\cup\Pi\rightarrow\mathbb{B}$;

  * •

for every stack bottom $\omega_{p}$, we let $\tau(\omega_{p})\coloneqq p$;

  * •

for every variable $x$,
$\tau(x)\coloneqq\tau(\textnormal{{{cc}}})\coloneqq\mathbb{1}$;

  * •

for every term $t$ and stack $\pi$, we let
$\tau(t\boldsymbol{.}\pi)=\tau(t)\land\tau(\pi)$;

  * •

for all $\lambda_{c}$-terms $t,s$, we let
$\tau(ts)\coloneqq\tau(t)\land\tau(s)$;

  * •

for every variable $u$ and every term $t$, we let $\tau(\lambda
u\boldsymbol{.}t)\coloneqq\tau(t)$;

  * •

for every stack $\pi$, we let
$\tau(\textnormal{{k}}_{\pi})\coloneqq\tau(\pi)$.

This is then naturally extended to the set of all processes by the assignment

$\tau(t\star\pi)\coloneqq\tau(t)\land\tau(\pi).$

Then, we define the pre-order by $t\star\pi\succ s\star\sigma$ if and only if
$\tau(t\star\pi)\leq\tau(s\star\sigma)$ and we let
$\mathbin{\text{$\bot\mkern-11.0mu\bot$}}$ be the set of all processes
$t\star\pi$ such that $\tau(t\star\pi)=\mathbb{0}$.

There is obviously a large amount of overlapping notation between Boolean-
valued models and realizability models. In order to hopefully make the
notation clearer for this section, while keeping the notation for
realizability harmonious with this rest of this work, we will do the
following:

  * •

$\lVert\varphi\rVert$ and $\lvert\varphi\rvert$ will refer to their usual
meanings in the realizability model.

  * •

The Boolean value of a formula $\varphi$ will be denoted by
$\llbracket\varphi\rrbracket$.

  * •

$\Vdash_{\mathcal{A}}$ refers to the realizability relation over the structure
$\mathcal{A}_{\mathbb{B}}$.

  * •

$\Vdash_{\mathbb{B}}$ refers to forcing with the Boolean algebra. Namely,
$p\Vdash_{\mathbb{B}}\varphi$ if and only if
$p\leq\llbracket\varphi\rrbracket$.

  * •

$\textnormal{{N}}^{\mathcal{A}}$ will refer to the domain of the realizability
model while $\textnormal{{V}}^{\mathbb{B}}$ will refer to the domain of the
Boolean-valued model.

We continue by observing that if two terms are mapped to the same element of
the Boolean algebra then they realize the same formulas. From this it follows
that the realizability model “ _loses its computational content_ ”. This is