17321 LABEL:LastPageJun. 11, 2020Sep. 01, 2021

# A program for the full axiom of choice

Jean-Louis Krivine  Université de Paris - C.N.R.S<EMAIL_ADDRESS>
###### Abstract.

The theory of classical realizability is a framework for the Curry-Howard
correspondence which enables to associate a program with each proof in
Zermelo-Fraenkel set theory. But, almost all the applications of mathematics
in physics, probability, statistics, etc. use Analysis i.e. the axiom of
dependent choice (DC) or even the (full) axiom of choice (AC). It is therefore
important to find explicit programs for these axioms. Various solutions have
been found for DC, for instance the lambda-term called ”bar recursion” or the
instruction ”quote” of LISP. We present here the first program for AC.

###### Key words and phrases:

Curry-Howard correspondence, set theory, combinatory logic, lambda-calculus,
axiom of choice

## Introduction

The Curry-Howard correspondence enables to associate a program with each proof
in classical natural deduction. But mathematical proofs not only use the rules
of natural deduction, but also _axioms_ , essentially those of Zermelo-Frænkel
set theory with axiom of choice. In order to transform these proofs into
programs, we must therefore associate with each of these axioms suitable
instructions, which is far from obvious.

The theory of _classical realizability (c.r.)_ solves this problem for all
axioms of ZF, by means of a very rudimentary programming language: the
$\lambda_{c}$-calculus, that is to say the $\lambda$-calculus with a control
instruction [Gri90].

The programs obtained in this way can therefore be written in practically any
programming language. They are said to _realize_ the axioms of ZF.

But, almost all the applications of mathematics in physics, probability,
statistics, etc. use _Analysis_ , that is to say _the axiom of dependent
choice_. The first program for this axiom, known since 1998 [BBC98], is a pure
$\lambda$-term called _bar recursion_ [Spe62, BO05, Str17]. In fact, c.r.
shows that it provides also a program for the _continuum hypothesis_ [Kri16].

Nevertheless, this solution requires the programming language to be limited to
$\lambda_{c}$-calculus, prohibiting any other instruction, which is a severe
restriction.

Classical realizability provides other programs for this axiom [Kri12, Kri18,
Kri09], which require an additional instruction (clock, signature, … , or as
in this paper, introduction of _fresh variables_). On the other hand, this
kind of solution is very flexible regarding the programming language.

There remained, however, the problem of the _full_ axiom of choice. It is
solved here, by means of new instructions which allow _branching_ or
_parallelism_ 111A detailed study of the effect of such instructions on the
characteristic Boolean algebra $\gimel 2$ is made in [Geo18].. Admittedly, the
program obtained in this way is rather complicated and we may hope for new
solutions as simple as bar recursion or clock. However, it already shows how
we can turn all proofs of ZFC into programs (more precisions about this in
Remark 45 at the end of the paper). Note that _the proof is constructive_ i.e.
it gives explicitly a program for AC: you ”merely” need to formalize this
proof itself in natural deduction and apply the proof-program correspondence
to the result.

### Outline of the paper

The framework of this article is the _theory of classical realizability_ ,
which is explained in detail in [Kri12, Kri18, Kri09]. For the sake of
simplicity, we will often refer to these papers for definitions and standard
notations.

Section 1:

Axioms and properties of _realizability algebras (r.a.)_ which are first order
structures, a generalization of both combinatory algebras and ordered sets of
forcing conditions. Intuitively, their elements are programs.

Section 2:

Each r.a. is associated with a _realizability model (r.m.)_ , a generalization
of the generic model in the theory of forcing. This model satisfies a set
theory ZFε which is a conservative extension of ZF, with a strong non
extensional membership relation $\varepsilon$.

Section 3:

Generic extensions of realizability algebras and models. We explain how a
generic extension of a given r.m. can be handled by means of a suitable
extension of the corresponding r.a. A little technical because it mixes
forcing and realizability.

Section 4:

Definition and properties of a particular realizability algebra
$\mathfrak{A}_{0}$. It contains an _instruction of parallelism_ and the
programming language allows the introduction of many other instructions. This
is therefore, in fact, a class of algebras.

At this stage, we obtain a program for the _axiom of well ordered choice
(WOC): the product of a family of non-empty sets whose index set is well
ordered is non-empty._

We get, at the same time, a new proof that WOC is weaker than AC (joint work
with Laura Fontanella; cf. [Jec73] for the usual proof).

Section 5:

Construction of a generic extension $\mathfrak{A}_{1}$ of the algebra
$\mathfrak{A}_{0}$ which allows to _realize the axiom of choice: every set can
be well ordered._

Sections 3 and 4 are independent.

Thanks to Asaf Karagila for several fruitful discussions [Kar19]. He observed
that, by exactly the same method, we obtain a program, not only for AC, but
for every axiom which can be shown compatible with ZFC _by forcing_ (Theorem
44); for instance CH, $2^{\aleph_{0}}=\aleph_{2}$ \+ Martin’s axiom, etc. (but
this does not apply to V = L).

##  1\. Realizability algebras (r.a.)

It is a first order structure, which is defined in [Kri18]. We recall here
briefly this definition and some essential properties.

A _realizability algebra_ ${\mathcal{A}}$ is made up of three sets: $\Lambda$
(the set of _terms_), $\Pi$ (the set of _stacks_), $\Lambda\star\Pi$ (the set
of _processes_) with the following operations:

  * $(\xi,\eta)\mapsto(\xi)\eta$ from $\Lambda^{2}$ into $\Lambda$ (_application_);

  * $(\xi,\pi)\mapsto\xi\,\mbox{\Large.}\,\pi$ from $\Lambda\\!\times\\!\Pi$ into $\Pi$ (_push_);

  * $(\xi,\pi)\mapsto\xi\star\pi$ from $\Lambda\\!\times\\!\Pi$ into $\Lambda\star\Pi$ (_process_);

  * $\pi\mapsto\mbox{k}_{\pi}$ from $\Pi$ into $\Lambda$ (_continuation_).

There are, in $\Lambda$, distinguished elements
$\mbox{B},\mbox{C},\mbox{I},\mbox{K},\mbox{W},\mbox{\sf cc}$, called
_elementary combinators_ or _instructions_.

Notation. The term $(\ldots(((\xi)\eta_{1})\eta_{2})\ldots)\eta_{n}$ will be
also written $(\xi)\eta_{1}\eta_{2}\ldots\eta_{n}$ or even
$\xi\eta_{1}\eta_{2}\ldots\eta_{n}$. For instance:
$\xi\eta\zeta=(\xi)\eta\zeta=(\xi\eta)\zeta=((\xi)\eta)\zeta$.

We define a preorder on $\Lambda\star\Pi$, denoted by $\succ$, which is called
_execution_ ;

$\xi\star\pi\succ\xi^{\prime}\star\pi^{\prime}$ is read as: _the process
$\xi\star\pi$ reduces to $\xi^{\prime}\star\pi^{\prime}$._

It is the smallest reflexive and transitive binary relation, such that, for
any $\xi,\eta,\zeta\in\Lambda$ and $\pi,\varpi\in\Pi$, we have:

  * $(\xi)\eta\star\pi\succ\xi\star\eta\,\mbox{\Large.}\,\pi$ (_push_).

  * $\mbox{I}\star\xi\,\mbox{\Large.}\,\pi\succ\xi\star\pi$ (_no operation_).

  * $\mbox{K}\star\xi\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\pi\succ\xi\star\pi$ (_delete_).

  * $\mbox{W}\star\xi\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\pi\succ\xi\star\eta\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\pi$ (_copy_).

  * $\mbox{C}\star\xi\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\zeta\,\mbox{\Large.}\,\pi\succ\xi\star\zeta\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\pi$ (_switch_).

  * $\mbox{B}\star\xi\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\zeta\,\mbox{\Large.}\,\pi\succ\xi\star(\eta)\zeta\,\mbox{\Large.}\,\pi$ (_apply_).

  * $\mbox{\sf cc}\star\xi\,\mbox{\Large.}\,\pi\succ\xi\star\mbox{k}_{\pi}\,\mbox{\Large.}\,\pi$ (_save the stack_).

  * $\mbox{k}_{\pi}\star\xi\,\mbox{\Large.}\,\varpi\succ\xi\star\pi$ (_restore the stack_).

We are also given a subset $\bot\bot$ of $\Lambda\star\Pi$, called ”the pole”,
such that:

$\xi\star\pi\succ\xi^{\prime}\star\pi^{\prime}$,
$\xi^{\prime}\star\pi^{\prime}\in\bot\bot$ $\Rightarrow$
$\xi\star\pi\in\bot\bot$.

Given two processes $\xi\star\pi,\xi^{\prime}\star\pi^{\prime}$, the notation
$\xi\star\pi\succ\succ\xi^{\prime}\star\pi^{\prime}$ means:

$\xi\star\pi\notin\bot\bot\Rightarrow\xi^{\prime}\star\pi^{\prime}\notin\bot\bot$.

Therefore, obviously,
$\xi\star\pi\succ\xi^{\prime}\star\pi^{\prime}\;\Rightarrow\;\xi\star\pi\succ\succ\xi^{\prime}\star\pi^{\prime}$.

Finally, we choose a set of terms PL${}_{\mathcal{A}}\subset\Lambda$,
containing the elementary combinators:
$\mbox{B},\mbox{C},\mbox{I},\mbox{K},\mbox{W},\mbox{\sf cc}$ and closed by
application. They are called the _proof-like terms of the algebra
${\mathcal{A}}$_. We write also PL instead of PLA if there is no ambiguity
about ${\mathcal{A}}$.

The algebra ${\mathcal{A}}$ is called _coherent_ if, for every proof-like term
$\theta\in\mbox{\mbox{PL}}_{\mathcal{A}}$, there exists a stack $\pi$ such
that $\theta\star\pi\notin\bot\bot$.

######  Remark 1.

A _set of forcing conditions_ can be considered as a degenerate case of
realizability algebra, if we present it in the following way:

An inf-semi-lattice $P$, with a greatest element $\mathbf{1}$ and an initial
segment $\bot\bot$ of $P$ (the set of _false_ conditions). Two conditions
$p,q\in P$ are called _compatible_ if their g.l.b. $p{\scriptstyle\land}q$ is
not in $\bot\bot$.

We get a realizability algebra if we set $\Lambda=\Pi=\Lambda\star\Pi=P$;
$\mbox{B}=\mbox{C}=\mbox{I}=\mbox{K}=\mbox{W}=\mbox{\sf cc}=\mathbf{1}$ and
PL$=\\{\mathbf{1}\\}$; $(p)q=p\,\mbox{\Large.}\,q=p\star
q=p{\scriptstyle\land}q$ and $\mbox{k}_{p}=p$. The preorder $p\succ q$ is
defined as $p\leq q$, i.e. $p{\scriptstyle\land}q=p$. The condition of
coherence is $\mathbf{1}\notin\bot\bot$.

We can translate $\lambda$-terms into terms of $\Lambda$ built with the
combinators $\mbox{B},\mbox{C},\mbox{I},\mbox{K},\mbox{W}$ in such a way that
weak head reduction is valid:

$\lambda x\,t[x]\star u\,\mbox{\Large.}\,\pi\succ t[u/x]\star\pi$

where $\lambda x\,t[x],u$ are terms and $\pi$ is a stack.

This is done in [Kri18]. Note that the usual $(\mbox{K}$,S)-translation does
not work.

In order to write programs, $\lambda$-calculus is much more intuitive than
combinatory algebra, so that we use it extensively in the following. But
combinatory algebra [CF58] is better for theory, in particular because it is a
first order structure.

##  2\. Realizability models (r.m.)

The framework is very similar to that of forcing, which is anyway a particular
case.

We use a first order language with three binary symbols
$\,\varepsilon\\!\\!\\!/\,,\notin,\subset$ ($\,\varepsilon\,$ is intended to
be a strong, non extensional membership relation; $\in$ and $\subset$ have
their usual meaning in ZF).

First order formulas are written with the only logical symbols
$\to,\forall,\bot,\top$.

The symbols $\neg,\land,\lor,\leftrightarrow,\exists$ are defined with them in
the usual way.

Given a realizability algebra, we get a _realizability model (r.m.)_ as
follows:

We start with a model ${\mathcal{M}}$ of ZFC (or even ZFL) called the _ground
model_. The axioms of ZFL are written with the sublanguage
$\\{\notin,\subset\\}$.

We build a model ${\mathcal{N}}$ of a new set theory ZFε, in the language
$\\{\,\varepsilon\\!\\!\\!/\,,\notin,\subset\\}$, the axioms of which are
given in [Kri12]. We recall them below, using the following rather standard
abbreviations:

$F_{1}\to(F_{2}\to\ldots(F_{n}\to G)\ldots)$ is written
$F_{1},F_{2},\ldots,F_{n}\to G$ or even $\vec{F}\to G$.

We use the notation $\exists x\\{F_{1},F_{2},\ldots,F_{n}\\}$ for $\forall
x(F_{1}\to(F_{2}\to\cdots\to(F_{n}\to\bot)\cdots))\to\bot$.

Of course, $x\,\varepsilon\,y$ and $x\in y$ are the formulas
$x\,\varepsilon\\!\\!\\!/\,y\to\bot$ and $x\notin y\to\bot$.

The notation $x=_{\in}\\!y\to F$ means $x\subset y,y\subset x\to F$. Thus
$x=_{\in}\\!y$, which represents the usual (extensional) equality of sets, is
the pair of formulas $\\{x\subset y,y\subset x\\}$.

We use the notations:

$(\forall x\,\varepsilon\,a)F(x)$ for $\forall x(\neg F(x)\to
x\,\varepsilon\\!\\!\\!/\,a)$ and $(\exists x\,\varepsilon\,a)\vec{F}(x)$ for
$\neg\forall x(\vec{F}(x)\to x\,\varepsilon\\!\\!\\!/\,a)$.

For instance, $(\exists x\,\varepsilon\,y)(t=_{\in}\\!u)$ is the formula
$\neg\forall x(t\subset u,u\subset t\to x\,\varepsilon\\!\\!\\!/\,y)$.

The axioms of ZFε are the following:

  1. (0)

Extensionality axioms.

$\forall x\forall y(x\in y\leftrightarrow(\exists
z\,\varepsilon\,y)x=_{\in}\\!z)$; $\forall x\forall y(x\subset
y\leftrightarrow(\forall z\,\varepsilon\,x)z\in y)$.

  2. (1)

Foundation scheme.

$\forall\vec{a}(\forall x((\forall y\,\varepsilon\,x)F(y,\vec{a})\to
F(x,\vec{a}))\to\forall x\,F(x,\vec{a}))$ for every formula
$F(x,a_{1},\ldots,a_{n})$.

The intuitive meaning of these axioms is that $\varepsilon$ is a well founded
relation and the relation $\in$ is obtained by “ collapsing ” $\varepsilon$
into an extensional relation.

The following axioms essentially express that the relation $\,\varepsilon\,$
satisfies the Zermelo-Fraenkel axioms except extensionality.

  1. (2)

Comprehension scheme.

$\forall\vec{a}\forall x\exists y\forall
z(z\,\varepsilon\,y\leftrightarrow(z\,\varepsilon\,x\land F(z,\vec{a}))$ for
every formula $F(z,\vec{a})$.

  2. (3)

Pairing axiom.

$\forall a\forall b\exists x\\{a\,\varepsilon\,x,b\,\varepsilon\,x\\}$.

  3. (4)

Union axiom.

$\forall a\exists b(\forall x\,\varepsilon\,a)(\forall
y\,\varepsilon\,x)\,y\,\varepsilon\,b$.

  4. (5)

Power set axiom.

$\forall a\exists b\forall x(\exists y\,\varepsilon\,b)\forall
z(z\,\varepsilon\,y\leftrightarrow(z\,\varepsilon\,a\land
z\,\varepsilon\,x))$.

  5. (6)

Collection scheme.

$\forall\vec{a}\forall x\exists y(\forall u\,\varepsilon\,x)(\exists
v\,F(u,v,\vec{a})\to(\exists v\,\varepsilon\,y)F(u,v,\vec{a}))$ for every
formula $F(u,v,\vec{a})$.

  6. (7)

Infinity scheme.

$\forall\vec{a}\forall x\exists y\\{x\,\varepsilon\,y,(\forall
u\,\varepsilon\,y)(\exists v\,F(u,v,\vec{a})\to(\exists
v\,\varepsilon\,y)F(u,v,\vec{a}))\\}$ for every formula $F(u,v,\vec{a})$.

It is shown in [Kri12] that ZFε is a _conservative extension of ZF._

For each formula $F(\vec{a})$ of ZFε (i.e. written with
$\,\varepsilon\\!\\!\\!/\,,\notin,\subset$) with parameters $\vec{a}$ in the
ground model ${\mathcal{M}}$ we define, in ${\mathcal{M}}$, a _falsity value_
$\|F(\vec{a})\|$ which is a subset of $\Pi$ and a _truth value_ $|F(\vec{a})|$
which is a subset of $\Lambda$.

The notation $t\mbox{ $||-\,$}F(\vec{a})$ (read “$t$ realizes $F(\vec{a})$” or
“$t$ forces $F(\vec{a})$” in the particular case of forcing) means
$t\in|F(\vec{a})|$.

We set first
$|F(\vec{a})|=\\{t\in\Lambda\;;\;(\forall\pi\in\|F(\vec{a})\|)(t\star\pi\in\bot\bot)\\}$
so that we only need to define $\|F(\vec{a})\|$, which we do by induction on
$F$:

  1. (1)

Definition of $\|a\,\varepsilon\\!\\!\\!/\,b\|$:

$\|a\,\varepsilon\\!\\!\\!/\,b\|=\\{\pi\in\Pi\;;\;(a,\pi)\in b\\}$;
$\|\bot\|=\Pi$; $\|\top\|=\emptyset$;

  2. (2)

Definition of $\|a\subset b\|$ and $\|a\notin b\|$ by induction on
$(\mbox{rk}(a)\cup\mbox{rk}(b),\mbox{rk}(a)\cap\mbox{rk}(b))$:

$\|a\subset b\|=\bigcup_{c}\\{t\,\mbox{\Large.}\,\pi\in\Pi\;;\;t\mbox{
$||-\,$}c\notin b,(c,\pi)\in a\\}$;

$\|a\notin
b\|=\bigcup_{c}\\{t\,\mbox{\Large.}\,u\,\mbox{\Large.}\,\pi\in\Pi\;;\;t\mbox{
$||-\,$}c\subset a,u\mbox{ $||-\,$}a\subset c,(c,\pi)\in b\\}$.

  3. (3)

Definition of $\|F\|$ for a non atomic formula $F$, by induction on the
length:

$\|F\to F^{\prime}\|=\\{t\,\mbox{\Large.}\,\pi\in\Pi\;;\;t\mbox{
$||-\,$}F,\pi\in\|F^{\prime}\|\\}$; $\|\forall x\,F(x)\|=\bigcup_{a}\|F(a)\|$.

This notion of realizability has two essential properties given by theorems 2
and 4 below. They are proved in [Kri12].

######  Theorem 2 (Adequacy lemma).

$||-\,$ is compatible with classical natural deduction, i.e.:

If $t_{1},\ldots,t_{n},t$ are $\lambda_{c}$-terms such that
$t_{1}:F_{1},\ldots,t_{n}:F_{n}\vdash t:F$ in classical natural deduction,
then $t_{1}\mbox{ $||-\,$}F_{1},\ldots,t_{n}\mbox{ $||-\,$}F_{n}\Rightarrow
t\mbox{ $||-\,$}F$.

In particular, any valid formula is realized by a proof-like term.

######  Remark 3.

The proof of Theorem 2 uses only item 3 in the above definition of $\|F\|$. In
other words, the values of $\|F\|$ for atomic formulas $F$ are arbitrary. This
will be used in Sections 3 and 5.

######  Theorem 4.

The axioms of ZFε are realized by proof-like terms.

It follows that _every closed formula which is consequence of ZF ε and, in
particular, every consequence of ZF, is realized by a proof-like term_.

In the following, we shall simply say “the formula $F$ is realized” instead of
“realized by a proof-like term” and use the notation $\mbox{ $||-\,$}F$.

Theorem 4 is valid _for every r.a._ The aim of this paper is to realize the
full axiom of choice AC in some particular r.a.  _suitable for programming_.

######  Remark 5.

Note that AC is realized for any r.a. associated with a set of forcing
conditions (generic extension of ${\mathcal{M}}$). But in this case, there is
only one proof-like term which is the greatest element $\mathbf{1}$.

We define the strong (Leibnitz) equality $a=b$ by $\forall
z(a\,\varepsilon\\!\\!\\!/\,z\to b\,\varepsilon\\!\\!\\!/\,z)$. It is
trivially transitive and it is symmetric by comprehension. This equality
satisfy the first order axioms of equality $\forall x\forall y(x=y\to(F(x)\to
F(y)))$ (by comprehension scheme of ZFε) and is therefore the equality in the
r.m. ${\mathcal{N}}$.

######  Lemma 6.

$\|a=b\|=\|\top\to\bot\|=\\{\xi\,\mbox{\Large.}\,\pi\;;\;\xi\in\Lambda,\pi\in\Pi\\}$
if $a\neq b$;

$\|a=a\|=\|\bot\to\bot\|=\\{\xi\,\mbox{\Large.}\,\pi\;;\;\xi\in\Lambda,\pi\in\Pi,\xi\star\pi\in\bot\bot\\}$.

######  Proof 2.1.

Let $z=\\{b\\}\\!\times\\!\Pi$ so that $\|b\,\varepsilon\\!\\!\\!/\,z\|=\Pi$.
If $a\neq b$ then $\|a\,\varepsilon\\!\\!\\!/\,z\|=\emptyset$ and therefore:

$\|a\,\varepsilon\\!\\!\\!/\,z\to
b\,\varepsilon\\!\\!\\!/\,z\|=\|\top\to\bot\|$.

If $a=b$, then $\|a\,\varepsilon\\!\\!\\!/\,z\|=\Pi$ and therefore
$\|a=b\|=\|\bot\to\bot\|$.

Finally, it is convenient to define first $\neq$ by $\|a\neq
a\|=\|\bot\|=\Pi$; $\|a\neq b\|=\|\top\|=\emptyset$ if $a\neq b$; and to
define $a=b$ as $a\neq b\to\bot$.

We define a preorder $\leq$ on the set ${\mathcal{P}}(\Pi)$ of “falsity
values” by setting:

$X\leq Y\Leftrightarrow$ there exists a proof-like term $\theta\mbox{
$||-\,$}X\to Y$. By Theorem 2, we easily see [Kri12] that
$({\mathcal{P}}(\Pi),\leq)$ is a Boolean algebra $\mathfrak{B}_{\mathcal{A}}$
_if the r.a. ${\mathcal{A}}$ is coherent_. Every formula $F(\vec{a})$ of ZFε
with parameters in the ground model ${\mathcal{M}}$ has a value
$\|F(\vec{a})\|$ in this Boolean algebra.

By means of any ultrafilter on $\mathfrak{B}_{\mathcal{A}}$, we thus obtain a
complete consistent theory in the language
$\\{\,\varepsilon\\!\\!\\!/\,,\notin,\subset\\}$ with parameters in
${\mathcal{M}}$. We take any model ${\mathcal{N}}$ of this theory and call it
_the realizability model (r.m.)_ of the realizability algebra ${\mathcal{A}}$.

Therefore, ${\mathcal{N}}$ is a model of ZFε, and in particular, a model of
ZF, that we will call ${\mathcal{N}}_{\in}$.

Thus ${\mathcal{N}}_{\in}$ is simply the model ${\mathcal{N}}$ restricted to
the language $\\{\notin,\subset\\}$.

######  Remark 7.

The ground model ${\mathcal{M}}$ is contained in ${\mathcal{N}}$ since every
element of it is a symbol of constant. But ${\mathcal{M}}$ is not a submodel
of ${\mathcal{N}}$ for the common language $\\{\notin,\subset\\}$; and, except
in the case of forcing, not every element of ${\mathcal{N}}$ “has a name” in
${\mathcal{M}}$.

When $F$ is a closed formula of ZFε, the two assertions ${\mathcal{N}}\models
F$ and $\mbox{ $||-\,$}F$ have essentially the same meaning, since
${\mathcal{N}}$ represents _any r.m._ for the given r.a. But the second
formulation requires a formal proof.

### Functionals

_A functional relation defined in ${\mathcal{N}}$_ is given by a formula
$F(x,y)$ of ZFε such that ${\mathcal{N}}\models\forall x\forall y\forall
y^{\prime}(F(x,y),F(x,y^{\prime})\to y=y^{\prime})$.

A _function_ is a functional relation which is a set.

We define now some special functional relations on ${\mathcal{N}}$ which we
call _functionals defined in ${\mathcal{M}}$_ or _functional symbols_ :

For each functional relation $f:{\mathcal{M}}^{k}\to{\mathcal{M}}$ defined in
the ground model ${\mathcal{M}}$, we add the functional symbol $f$ to the
language of ZFε. The application of $f$ to an argument $a$ will be denoted
$f[a]$. Therefore $f$ is also defined in ${\mathcal{N}}$.

We call this (trivial) operation _the extension to ${\mathcal{N}}$ of the
functional $f$_ defined in the ground model. It is a fundamental tool in all
that follows.

Note the use of brackets for $f[a]$ in this case.

######  Theorem 8.

Let $t_{1},u_{1}\ldots,t_{n},u_{n},t,u$ be $k$-ary terms built with functional
symbols, such that
${\mathcal{M}}\models\forall\vec{x}(t_{1}[\vec{x}]=u_{1}[\vec{x}],\ldots,t_{n}[\vec{x}]=u_{n}[\vec{x}]\to
t[\vec{x}]=u[\vec{x}])$.

Then $\lambda x_{1}\ldots\lambda x_{n}\lambda x(x_{1})\ldots(x_{n})x\mbox{
$||-\,$}\forall\vec{x}(t_{1}[\vec{x}]=u_{1}[\vec{x}],\ldots,t_{n}[\vec{x}]=u_{n}[\vec{x}]\to
t[\vec{x}]=u[\vec{x}])$.

######  Proof 2.2.

This easily follows from the definition above of $\|a=b\|$.

As a first example let the unary functional $\Phi_{F}[X]$ be defined in
${\mathcal{M}}$ by:

$\Phi_{F}[X]=\\{(x,\xi\,\mbox{\Large.}\,\pi)\;;\;\xi\mbox{
$||-\,$}F(x),(x,\pi)\in X\\}$.

We shall denote it by $\\{x\,\varepsilon\,X\;;\;F(x)\\}$ (in this notation,
$x$ is a bound variable) because it corresponds to the comprehension scheme in
the model ${\mathcal{N}}$. Note that the use of $\varepsilon$ reminds that
this expression must be interpreted in ${\mathcal{N}}$.

We define now in ${\mathcal{M}}$ the unary functional $\gimel
X=X\\!\times\\!\Pi$, so that we have:

$\|x\,\varepsilon\\!\\!\\!/\,\gimel X\|=\Pi$ if $x\in X$ and
$\|x\,\varepsilon\\!\\!\\!/\,\gimel X\|=\emptyset$ if $x\notin X$.

For any $X$ in ${\mathcal{M}}$, we define the quantifier $\forall x^{\gimel
X}$ by setting $\|\forall x^{\gimel X}F(x)\|=\bigcup_{x\in X}\|F(x)\|$.

######  Lemma 9.

$\mbox{ $||-\,$}\forall x^{\gimel X}F(x)\leftrightarrow\forall
x(x\,\varepsilon\,\gimel X\to F(x))$.

######  Proof 2.3.

In fact, we have $\|\forall x(\neg F(x)\to x\,\varepsilon\\!\\!\\!/\,\gimel
X)\|=\|\forall x^{\gimel X}\neg\neg F(x)\|$.

Now we have trivially:

$\lambda x(x)\mbox{I}\,\mbox{ $||-\,$}\forall x^{\gimel X}F(x)\to\forall
x^{\gimel X}\neg\neg F(x)$ and $\mbox{\sf cc}\mbox{ $||-\,$}\forall x^{\gimel
X}\neg\neg F(x)\to\forall x^{\gimel X}F(x)$.

######  Lemma 10.

Let $f$ be a functional $k$-ary symbol defined in ${\mathcal{M}}$ such that
$f:X_{1}\\!\times\\!\cdots\\!\times\\!X_{k}\to X$. Then its extension to
${\mathcal{N}}$ is such that $f:\gimel
X_{1}\\!\times\\!\cdots\\!\times\\!\gimel X_{k}\to\gimel X$.

######  Proof 2.4.

Trivial.

By Theorem 8 and Lemma 10, the algebra operations on the Boolean algebra
$2=\\{0,1\\}$ extended to $\gimel 2$, turn it into a Boolean algebra which we
call _the characteristic Boolean algebra_ of the r.m. ${\mathcal{N}}$. In the
ground model ${\mathcal{M}}$, we define the functional $(a,x)\mapsto ax$ from
$2\\!\times\\!{\mathcal{M}}$ into ${\mathcal{M}}$ by $0x=\emptyset$ and
$1x=x$. It extends to ${\mathcal{N}}$ into a functional $\gimel
2\\!\times\\!{\mathcal{N}}\to{\mathcal{N}}$ such that $(ab)x=a(bx)$ for
$a,b\,\varepsilon\,\gimel 2$ and every $x$ in ${\mathcal{N}}$.

######  Lemma 11.

$\mbox{I}\,\mbox{ $||-\,$}\forall\vec{x}\forall\vec{y}\forall a^{\gimel
2}(af[\vec{x},\vec{y}]=af[a\vec{x},\vec{y}])$ for every functional symbol $f$
defined in ${\mathcal{M}}$.

######  Proof 2.5.

Immediate since $\xi\mbox{ $||-\,$}\forall a^{\gimel 2}F(a)$ means $(\xi\mbox{
$||-\,$}F(0))\land(\xi\mbox{ $||-\,$}F(1))$.

For any formula $F(\vec{x})$ of ZF we define, in ${\mathcal{M}}$, a functional
$\langle F(\vec{x})\rangle$ with value in $\\{0,1\\}$ which is the truth value
of this formula in ${\mathcal{M}}$.222The formal definition in ZF is:
$\forall\vec{x}((F(\vec{x})\to\langle F(\vec{x})\rangle=1)\land(\neg
F(\vec{x})\to\langle F(\vec{x})\rangle=0))$. The extension of this functional
to the model ${\mathcal{N}}$ takes its values in the Boolean algebra $\gimel
2$ (cf. [Kri15]).

The binary functionals $\langle x\notin y\rangle$ and $\langle x\subset
y\rangle$ define on the r.m. ${\mathcal{N}}$ a structure of _Boolean model_ on
the Boolean algebra $\gimel 2$, that we denote by ${\mathcal{M}}_{\gimel 2}$.
It is an elementary extension of ${\mathcal{M}}$ since the truth value of
every closed formula of ZF with parameters in ${\mathcal{M}}$ is the same in
${\mathcal{M}}$ and ${\mathcal{M}}_{\gimel 2}$.

Any ultrafilter ${\mathcal{U}}$ on $\gimel 2$ would therefore give a (two-
valued) model ${\mathcal{M}}_{\gimel 2}/{\mathcal{U}}$ which is an elementary
extension of ${\mathcal{M}}$. In [Kri15], it is shown that there exists one
and only one ultrafilter ${\mathcal{D}}$ on $\gimel 2$ such that the model
${\mathcal{M}}_{\gimel 2}/{\mathcal{D}}$, which we shall denote as
${\mathcal{M}}_{\mathcal{D}}$, is well founded (in ${\mathcal{N}}$). The
binary relations $\notin,\subset$ of ${\mathcal{M}}_{\mathcal{D}}$ are thus
defined by $\langle x\notin y\rangle\,\varepsilon\,{\mathcal{D}}$ and $\langle
x\subset y\rangle\,\varepsilon\,{\mathcal{D}}$.

Moreover, ${\mathcal{M}}_{\mathcal{D}}$ is isomorphic with a transitive
submodel of ${\mathcal{N}}_{\in}$ with the same ordinals. In fact, if we start
with a ground model ${\mathcal{M}}$ which satisfies V = L, then
${\mathcal{M}}_{\mathcal{D}}$ is isomorphic with the constructible class of
${\mathcal{N}}_{\in}$.

######  Remark 12.

We have defined _four first order structures_ on the model ${\mathcal{N}}$:

  * •

The realizability model ${\mathcal{N}}$ itself uses the language
$\\{\,\varepsilon\\!\\!\\!/\,,\notin,\subset\\}$ of ZFε.

The equality on ${\mathcal{N}}$ is the Leibnitz equality =, which is the
strongest possible.

  * •

The model ${\mathcal{N}}_{\in}$ of ZF is restricted to the language
$\\{\notin,\subset\\}$.

The equality on ${\mathcal{N}}_{\in}$ is the extensional equality $=_{\in}$.

  * •

The Boolean model ${\mathcal{M}}_{\gimel 2}$ with the language
$\\{\notin,\subset\\}$ of ZF and with truth values in $\gimel 2$; it is an
elementary extension of the ground model ${\mathcal{M}}$.

The equality on ${\mathcal{M}}_{\gimel 2}$ is $\langle x=y\rangle=1$ which is
the same as Leibnitz equality.

  * •

The model ${\mathcal{M}}_{\mathcal{D}}$ with the same language, also an
elementary extension of ${\mathcal{M}}$; if $F(\vec{a})$ is a closed formula
of ZF with parameters (in ${\mathcal{N}}$), then
${\mathcal{M}}_{\mathcal{D}}\models F(\vec{a})$ iff
${\mathcal{N}}\models\langle F(\vec{a})\rangle\,\varepsilon\,{\mathcal{D}}$.

The equality on ${\mathcal{M}}_{\mathcal{D}}$ is given by $\langle
x=y\rangle\,\varepsilon\,{\mathcal{D}}$.

The proof of existence of the ultrafilter ${\mathcal{D}}$ in [Kri15] is not so
simple. But it is useless in the present paper, because $\gimel 2$ will be the
four elements algebra, with two atoms $a_{0},a_{1}$ which give the two trivial
ultrafilters on $\gimel 2$. It is easily seen (Lemma 29) that one of them, say
$a_{0}$ gives a well founded model denoted by ${\mathcal{M}}_{a_{0}}$ which is
the class $a_{0}{\mathcal{N}}={\mathcal{M}}_{\mathcal{D}}$. The class
${\mathcal{M}}_{a_{1}}=a_{1}{\mathcal{N}}$ is also an elementary extension of
${\mathcal{M}}$ (but not well founded, cf. Remark 39). Finally we have
${\mathcal{M}}_{\gimel
2}={\mathcal{N}}=a_{0}{\mathcal{N}}\\!\times\\!a_{1}{\mathcal{N}}$ since the
Boolean model ${\mathcal{M}}_{\gimel 2}$ is simply a product in this case, and
equality is the same on ${\mathcal{M}}_{\gimel 2}$ and ${\mathcal{N}}$ (Remark
12).

### Integers

We define, in the ground model ${\mathcal{M}}$, the functional $x\mapsto
x^{+}=x\cup\\{x\\}$ and extend it to the r.m. ${\mathcal{N}}$. It is injective
in ${\mathcal{M}}$ and therefore also in ${\mathcal{N}}$.

For each $n\in\mathbb{N}$, we define $\underline{n}\in$ PL by induction:
$\underline{0}=\lambda x\lambda y\,y=\mbox{K}\mbox{I}$;
$\underline{n}^{+}=s\underline{n}$ where $s=\lambda n\lambda f\lambda
x(nf)(f)x=(\mbox{B}\mbox{W})(\mbox{B})\mbox{B}$ (and $n^{+}$ is $n+1$).

We define
$\widetilde{\mathbb{N}}=\\{(n,\underline{n}\,\mbox{\Large.}\,\pi)\;;\;n\in\mathbb{N},\pi\in\Pi\\}$.
We can use it as the set of integers of the model ${\mathcal{N}}$ as shown by
the following Theorem 13.

We define the quantifier $\forall n^{\mbox{\footnotesize int}}$ by setting
$\|\forall n^{\mbox{\footnotesize
int}}F(n)\|=\\{\underline{n}\,\mbox{\Large.}\,\pi\;;\;n\in\mathbb{N},\pi\in\|F(n)\|\\}$.

######  Theorem 13.

For every formula $F(x)$ of ZFε, the following formulas are realized:

i) $0\,\varepsilon\,\widetilde{\mathbb{N}}$; $\forall
n(n\,\varepsilon\,\widetilde{\mathbb{N}}\to
n^{+}\,\varepsilon\,\widetilde{\mathbb{N}})$;

ii) $F(0),\forall n(F(n)\to F(n^{+}))\to(\forall
n\,\varepsilon\,\widetilde{\mathbb{N}})F(n)$;

iii) $\forall n^{\mbox{\footnotesize int}}F(n)\leftrightarrow(\forall
n\,\varepsilon\,\widetilde{\mathbb{N}})F(n)$.

######  Proof 2.6.

i) Let $\xi\mbox{ $||-\,$}0\,\varepsilon\\!\\!\\!/\,\widetilde{\mathbb{N}}$;
then $\xi\star\underline{0}\,\mbox{\Large.}\,\pi\in\bot\bot$ for all
$\pi\in\Pi$. Therefore $\lambda x(x)\underline{0}\mbox{
$||-\,$}0\,\varepsilon\\!\\!\\!/\,\widetilde{\mathbb{N}}\to\bot$.

Let $\xi\mbox{ $||-\,$}n^{+}\,\varepsilon\\!\\!\\!/\,\widetilde{\mathbb{N}}$
and
$\underline{n}\,\mbox{\Large.}\,\pi\in\|n\,\varepsilon\\!\\!\\!/\,\widetilde{\mathbb{N}}\|$.
We have $\xi\star s\underline{n}\,\mbox{\Large.}\,\pi\in\bot\bot$ and
therefore
$\theta\star\xi\,\mbox{\Large.}\,\underline{n}\,\mbox{\Large.}\,\pi\in\bot\bot$
with $\theta=\lambda x\lambda n(x)(s)n$. Thus $\theta\mbox{ $||-\,$}\forall
n(n^{+}\,\varepsilon\\!\\!\\!/\,\widetilde{\mathbb{N}}\to
n\,\varepsilon\\!\\!\\!/\,\widetilde{\mathbb{N}})$.

ii) We show $\lambda x\lambda y\lambda z\lambda n(x)(n)yz\mbox{ $||-\,$}\neg
F(0),\forall n(F(n^{+})\to F(n))\to\forall m(F(m)\to
m\,\varepsilon\\!\\!\\!/\,\widetilde{\mathbb{N}})$.

Let $\xi\mbox{ $||-\,$}\neg F(0),\eta\mbox{ $||-\,$}\forall n(F(n^{+})\to
F(n)),\zeta\mbox{ $||-\,$}F(m)$ and
$\underline{m}\,\mbox{\Large.}\,\pi\in\|m\,\varepsilon\\!\\!\\!/\,\widetilde{\mathbb{N}}\|$.

Let us show that $\underline{m}\eta\zeta\mbox{ $||-\,$}F(0)$ by induction on
$m$:

This is clear if $m=0$. Now,
$\underline{m}^{+}\eta\zeta=s\underline{m}\eta\zeta\succ(m\eta)(\eta)\zeta$
and $\eta\zeta\mbox{ $||-\,$}F(m)$ since $\zeta\mbox{ $||-\,$}F(m^{+})$.
Therefore $(m\eta)(\eta)\zeta\mbox{ $||-\,$}F(0)$ by the induction hypothesis.

It follows that $(\xi)(\underline{m})\eta\zeta\mbox{ $||-\,$}\bot$, hence the
result.

iii) Let us use Lemma 14. We have:

$\|\forall n(^{\neg}F(n)\to
n\,\varepsilon\\!\\!\\!/\,\widetilde{\mathbb{N}})\|=\\{\mbox{k}_{\pi}\,\mbox{\Large.}\,\underline{n}\,\mbox{\Large.}\,\varpi\;;\;n\in\mathbb{N},\pi\in\|F(n)\|,\varpi\in\Pi\\}$
and by definition:

$\|\forall n^{\mbox{\footnotesize
int}}F(n)\|=\\{\underline{n}\,\mbox{\Large.}\,\pi\;;\;n\in\mathbb{N},\pi\in\|F(n)\|\\}$.
It follows easily that:

$\lambda x\lambda n(\mbox{\sf cc})\lambda k(x)kn\mbox{ $||-\,$}\forall
n(^{\neg}F(n)\to n\,\varepsilon\\!\\!\\!/\,\widetilde{\mathbb{N}})\to\forall
n^{\mbox{\footnotesize int}}F(n)$

$\lambda x\lambda k\lambda n(k)(x)n\mbox{ $||-\,$}\forall
n^{\mbox{\footnotesize int}}F(n)\to\forall n(^{\neg}F(n)\to
n\,\varepsilon\\!\\!\\!/\,\widetilde{\mathbb{N}})$.

### Some useful notations

For every set of terms $X\subset\Lambda$ and every closed formula $F$ we can
define an “extended formula” $X\to F$ by setting $\|X\to
F\|=\\{\xi\,\mbox{\Large.}\,\pi\;;\;\xi\in X,\pi\in\|F\|\\}$.

For instance, for every formula $F$, we define
${}^{\neg}F=\\{\mbox{k}_{\pi}\;;\;\pi\in\|F\|\\}$. It is a useful equivalent
of $\neg F$ by the following:

######  Lemma 14.

$\mbox{ $||-\,$}{}^{\neg}F\leftrightarrow\neg F$.

######  Proof 2.7.

If $\pi\in\|F\|$, then $\mbox{k}_{\pi}\mbox{ $||-\,$}\neg F$ and therefore
$\mbox{I}\,\mbox{ $||-\,$}^{\neg}F\to\neg F$.

Conversely, if $\xi\mbox{ $||-\,$}^{\neg}F\to\bot$, then
$\xi\star\mbox{k}_{\pi}\,\mbox{\Large.}\,\pi\in\bot\bot$ for every
$\pi\in\|F\|$;

thus $\mbox{\sf cc}\mbox{ $||-\,$}\neg^{\neg}F\to F$.

If $t,u$ are terms of the language of ZF, built with functionals in
${\mathcal{M}}$, we define another “extended formula” $t=u\hookrightarrow F$
by setting:

$\|t=u\hookrightarrow F\|=\emptyset$ if $t\neq u$; $\|t=u\hookrightarrow
F\|=\|F\|$ if $t=u$.

We write $(t_{1}=u_{1}),\ldots,(t_{n}=u_{n})\hookrightarrow F$ for
$(t_{1}=u_{1})\hookrightarrow(\cdots\hookrightarrow((t_{n}=u_{n})\hookrightarrow
F)\cdots)$.

######  Lemma 15.

$\mbox{ $||-\,$}((t=u\hookrightarrow F)\leftrightarrow(t=u\to F))$.

######  Proof 2.8.

We have immediately $\mbox{I}\,\mbox{ $||-\,$}\neg F,(t=u\hookrightarrow F)\to
t\neq u$.

Conversely $\lambda x(x)\,\mbox{I}\mbox{ $||-\,$}(t=u\to
F)\to(t=u\hookrightarrow F)$.

For instance, the conclusion of Theorem 8 may be rewritten as:

$\mbox{I}\,\mbox{
$||-\,$}\forall\vec{x}(t_{1}[\vec{x}]=u_{1}[\vec{x}],\ldots,t_{n}[\vec{x}]=u_{n}[\vec{x}]\hookrightarrow
t[\vec{x}]=u[\vec{x}])$.

Lemmas 16, 17, 18 and Theorem 20 below will be used in the following sections.

######  Lemma 16.

$\mbox{ $||-\,$}\forall x\forall y(x\,\varepsilon\,y\to\langle x\in\mbox{\rm
Cl}[y]\rangle=1)$.

######  Proof 2.9.

In the model ${\mathcal{M}}$, the unary functional symbol Cl denotes the
_transitive closure_.

We show $\mbox{I}\,\mbox{ $||-\,$}\forall x\forall y(\langle
x\in\mbox{Cl}[y]\rangle\neq 1\to x\,\varepsilon\\!\\!\\!/\,y)$: let $\xi\mbox{
$||-\,$}\langle x\in\mbox{Cl}[y]\rangle\neq 1$ and
$\pi\in\|x\,\varepsilon\\!\\!\\!/\,y\|$.

Then $(x,\pi)\in y$, therefore $x\in\mbox{Cl}(y)$. It follows that $\xi\mbox{
$||-\,$}\bot$.

######  Lemma 17.

$\mbox{I}\,\mbox{ $||-\,$}\forall X\forall a^{\gimel 2}\forall x(\langle ax\in
aX\rangle\geq a\hookrightarrow ax\,\varepsilon\,\Phi[X])$ where $\Phi$ is the
functional symbol defined in ${\mathcal{M}}$ by
$\,\Phi[X]=(X\cup\\{0\\})\\!\times\\!\Pi$ i.e. $\gimel(X\cup\\{0\\})$.

The notation $b\geq a$ for $a,b\,\varepsilon\,\gimel 2$ means, of course,
$ab=a$.

######  Proof 2.10.

This amounts to show:

  1. (1)

$x\in X\Rightarrow\,\mbox{I}\mbox{
$||-\,$}x\,\varepsilon\\!\\!\\!/\,\Phi[X]\to\bot$;

  2. (2)

$\mbox{I}\mbox{ $||-\,$}0\,\varepsilon\\!\\!\\!/\,\Phi[X]\to\bot$.

Both are trivial.

######  Lemma 18.

Let $F(x,\vec{y})$ be a formula in ZFε. Then:

$\mbox{I}\,\mbox{
$||-\,$}\forall\vec{y}(\forall\varpi^{\gimel\Pi}F(f[\varpi,\vec{y}],\vec{y})\to\forall
x\,F(x,\vec{y}))$

for some functional symbol $f$ defined in ${\mathcal{M}}$.

######  Proof 2.11.

Let $\vec{a}=(a_{1},\ldots,a_{k})$ in ${\mathcal{M}}$. Then, we have:

$\pi\in\|\forall x\,F(x,\vec{a})\|\Leftrightarrow{\mathcal{M}}\models\exists
x(\pi\in\|F(x,\vec{a})\|)\Leftrightarrow{\mathcal{M}}\models\pi\in\|F(f[\pi,\vec{a}],\vec{a})\|$

where $f$ is a functional defined in ${\mathcal{M}}$, (choice principle in
${\mathcal{M}}$).

Thus we have $\|\forall
x\,F(x,\vec{a})\|\subset\bigcup_{\varpi\in\Pi}\|F(f[\varpi,\vec{a}],\vec{a})\|$
hence the result.

######  Lemma 19.

If $X\in{\mathcal{M}}$ is transitive, then $\gimel X$ is
$\,\varepsilon\,$-transitive, i.e.:

$\,\mbox{I}\,\mbox{ $||-\,$}\forall x^{\gimel X}\forall
y(y\,\varepsilon\\!\\!\\!/\,\gimel X\to y\,\varepsilon\\!\\!\\!/\,x)$.

######  Proof 2.12.

Let $x\in X$, $\varpi\in\|y\,\varepsilon\\!\\!\\!/\,x\|$, i.e. $(y,\varpi)\in
x$ and $\xi\in\mbox{\boldmath$\Lambda$}$ such that $\xi\mbox{
$||-\,$}y\,\varepsilon\\!\\!\\!/\,\gimel X$. Since $X$ is transitive, we have
$y\in X$ and therefore $\xi\mbox{ $||-\,$}\bot$.

######  Theorem 20.

Let $\mathfrak{L}$ be the language $\\{\varepsilon,\in,\subset\\}$ of ZFε,
with a symbol for each functional definable in ${\mathcal{M}}$. Then, there
exists an $\varepsilon$-transitive $\mathfrak{L}$-elementary substructure
$\widetilde{\mathcal{N}}$ of ${\mathcal{N}}$ such that, for all $a$ in
$\widetilde{\mathcal{N}}$, there is an ordinal $\alpha$ of ${\mathcal{M}}$
such that $\widetilde{\mathcal{N}}\models a\,\varepsilon\,\gimel V_{\alpha}$.

######  Proof 2.13.

$\widetilde{\mathcal{N}}$ is made up of the elements $a$ of ${\mathcal{N}}$
such that $a\,\varepsilon\,\gimel V_{\alpha}$ for some ordinal $\alpha$ of
${\mathcal{M}}$ (note that it is not a class defined in ${\mathcal{N}}$). By
Lemma 19, each $\gimel V_{\alpha}$ is $\varepsilon$-transitive and therefore
$\widetilde{\mathcal{N}}$ is also.

Let $F(x,\vec{y})$ be a formula of $\mathfrak{L}$ and
$\vec{b}=(b_{1},\ldots,b_{k}$) be in $\widetilde{\mathcal{N}}$. We assume
$\widetilde{\mathcal{N}}\models\forall x\,F(x,\vec{b})$ and we have to show
that ${\mathcal{N}}\models\forall x\,F(x,\vec{b})$ which we do by induction on
$F$. By Lemma 18, it suffices to show that
${\mathcal{N}}\models\forall\varpi^{\gimel\Pi}F(f[\varpi,\vec{b}],\vec{b})$.
Thus let $\pi\,\varepsilon\,\gimel\Pi$; by definition of
$\widetilde{\mathcal{N}}$, there exists $X$ in ${\mathcal{M}}$ such that
$\vec{b}\,\varepsilon\,\gimel X$. Now, there exists $V_{\alpha}$ in
${\mathcal{M}}$ such that $f:\Pi\\!\times\\!X\to V_{\alpha}$ and therefore, in
${\mathcal{N}}$, we have $f:\gimel\Pi\\!\times\\!\gimel X\to\gimel
V_{\alpha}$. It follows that $f[\pi,\vec{b}]\,\varepsilon\,\gimel V_{\alpha}$
and therefore $f[\pi,\vec{b}]$ is in $\widetilde{\mathcal{N}}$.

Thus $\widetilde{\mathcal{N}}\models F(f[\pi,\vec{b}],\vec{b})$, hence
${\mathcal{N}}\models F(f[\pi,\vec{b}],\vec{b})$ by the induction hypothesis.

Replacing ${\mathcal{N}}$ by this elementary substructure, we shall suppose
from now on:

\raisebox{-0.6pt}{\footnotesize1}⃝\raisebox{-0.6pt}{\footnotesize1}⃝  _For all
$a$ in ${\mathcal{N}}$, there is an ordinal $\alpha$ of ${\mathcal{M}}$ such
that ${\mathcal{N}}\models a\,\varepsilon\,\gimel V_{\alpha}$._

Theorem 21 below is not really useful in the following, but it gives a welcome
information on the (very complex) structure of the r.m. ${\mathcal{N}}\\!.$

######  Theorem 21.

$a{\mathcal{N}}$ is a proper class for all $a\,\varepsilon\,\gimel 2,a\neq 0$;
i.e.:

$\mbox{I}\,\mbox{ $||-\,$}\forall x(\forall a^{\gimel 2}(\forall
y(ay\,\varepsilon\,x)\to a=0))$.

######  Proof 2.14.

Let us show, in fact, that $\,\mbox{I}\mbox{ $||-\,$}\forall x(\forall
a^{\gimel 2}(ax\,\varepsilon\,x\to a=0))$; in other words:

$\mbox{I}\mbox{ $||-\,$}0\,\varepsilon\,x\to 0=0$ and $\mbox{I}\mbox{
$||-\,$}x\,\varepsilon\,x\to 1=0$.

We have $(0\,\varepsilon\,x)\equiv(0\,\varepsilon\\!\\!\\!/\,x\to\bot)$ and
$(0=0)\equiv(\bot\to\bot)$ hence the first result.

Furthermore, we have
$\|x\,\varepsilon\\!\\!\\!/\,x\|=\\{\pi\in\Pi\;;\;(x,\pi)\in x\\}=\emptyset$;
thus:

$\|x\,\varepsilon\,x\|=\|x\,\varepsilon\\!\\!\\!/\,x\to\bot\|=\|\top\to\bot\|$
and $\|1=0\|=\|\top\to\bot\|$.

Hence the second result.

##  3\. Extensional generic extensions

In this section we build some tools in order to manage generic extensions
${\mathcal{N}}_{\in}[G]$ of the _extensional_ model ${\mathcal{N}}_{\in}$. We
define a new r.a. and give, in this r.a., a new way to compute the truth value
of ZF-formulas in ${\mathcal{N}}_{\in}[G]$.

Let V be fixed in ${\mathcal{M}}$. We have
$\|x\,\varepsilon\\!\\!\\!/\,\gimel\mbox{\bf V}\|=\|\langle x\in\mbox{\bf
V}\rangle\neq 1\|$ and therefore:

$\mbox{I}\,\mbox{ $||-\,$}\forall x(x\,\varepsilon\,\gimel\mbox{\bf
V}\leftrightarrow\langle x\in\mbox{\bf V}\rangle=1)$.

In other words, the $\varepsilon$-elements of $\gimel\mbox{\bf V}$ are exactly
the elements of V in the Boolean model ${\mathcal{M}}_{\gimel 2}$. In fact,
the formula $\forall x^{\gimel\mbox{\scriptsize\bf V}}F(x)$ is the same as
$\forall x(\langle x\in\mbox{\bf V}\rangle=1\hookrightarrow F(x))$.

Remember also the important (and obvious) equivalence:

$\mbox{I}\mbox{ $||-\,$}\forall x\forall y(x=y\leftrightarrow\langle
x=y\rangle=1)$

which follows from $\|x\neq y\|=\|\langle x=y\rangle\neq 1\|$ and which
identifies the r.m. ${\mathcal{N}}$ with the Boolean model
${\mathcal{M}}_{\gimel 2}$ (Remark 12).

######  Theorem 22.

${\mathcal{N}}\models\forall a\forall n^{\mbox{\footnotesize
int}}\left(a\,\varepsilon\,(\gimel\mbox{\bf
V})^{n}\to\exists!b^{\gimel(\mbox{{\scriptsize\bf V}}^{n})}\forall
i^{\mbox{\footnotesize int}}(i<n\to a(i)=b[i])\right)$.

In other words, each finite sequence of $\;\gimel\mbox{\bf V}$ in
${\mathcal{N}}$ is represented by a unique finite sequence of V in the boolean
model ${\mathcal{M}}_{\gimel 2}$.

######  Proof 3.1.

Unicity. Note first that, since there is no extensionality in ${\mathcal{N}}$,
you may have two sequences $a\neq a^{\prime}\,\varepsilon\,(\gimel\mbox{\bf
V})^{n}$ such that $a(i)=a^{\prime}(i)$ for $i<n$. Now suppose
$b,b^{\prime}\,\varepsilon\,\gimel(\mbox{\bf V}^{n})$ be such that
$b[i]=b^{\prime}[i]$ for $i<n$. Then, we have $\langle
b,b^{\prime}\in\mbox{\bf V}^{n}\rangle=1$ and $\langle(\forall
i<n)(b[i]=b^{\prime}[i])\rangle=1$. Since the boolean model
${\mathcal{M}}_{\gimel 2}$ satisfies extensionality, we get $\langle
b=b^{\prime}\rangle=1$ that is $b=b^{\prime}$.

Existence. Proof by induction on $n$. This is trivial if $n=0$: take
$b=\emptyset$.

Now, let $a\,\varepsilon\,(\gimel\mbox{\bf V})^{n+1}$ and $a^{\prime}$ be a
restriction of $a$ to $n$. Let $b^{\prime}\,\varepsilon\,\gimel(\mbox{\bf
V}^{n})$ such that $a^{\prime}(i)=b^{\prime}[i]$ for $i<n$ (induction
hypothesis).

In the ground model ${\mathcal{M}}$, we define the binary functional $+$ as
follows:

if $u$ is a finite sequence $(u_{0},\ldots,u_{n-1})$, then $u+v$ is the
sequence $(u_{0},\ldots,u_{n-1},v)$.

We extend it to ${\mathcal{N}}$ and we set $b=b^{\prime}+a(n)$ i.e. $\langle
b=b^{\prime}+a(n)\rangle=1$. Therefore $\langle b[i]=b^{\prime}[i]\rangle=1$
for $i<n$ and $\langle b[n]=a(n)\rangle=1$, i.e. $a(i)=b[i]$ for $i<n$ and
$a(n)=b[n]$.

Consider an arbitrary ordered set $(C,\leq)$ in the model ${\mathcal{N}}$. By
Theorem 20 and property
\raisebox{-0.6pt}{\footnotesize1}⃝\raisebox{-0.6pt}{\footnotesize1}⃝ (Section
2), we may suppose that $(C,\leq)\,\varepsilon\,\gimel\mbox{\bf V}$ with
$\mbox{\bf V}=V_{\alpha}$ in ${\mathcal{M}}$.

$\gimel\mbox{\bf V}$ is $\varepsilon$-transitive, by Lemma 19.

As a set of forcing conditions, $C$ is equivalent to the set $\mathfrak{C}$ of
finite subsets $X$ of $\gimel\mbox{\bf V}$ such that $X\cap C$ has a lower
bound in $C$, $\mathfrak{C}$ being ordered by inclusion.

Thus, we can define $\mathfrak{C}$ by the following formula of ZFε:

_$\mathfrak{C}(u)\equiv u\,\varepsilon\,(\gimel\mbox{\bf V})^{
<\omega}\land(\mbox{Im}(u)\cap C)$ has a lower bound in $C$_

where Im$(u)\subseteq\gimel\mbox{\bf V}$ is the (finite) image of the finite
sequence $u$.

We have ${\mathcal{N}}\models\mathfrak{C}(u)\to
u\,\varepsilon\,(\gimel\mbox{\bf V})^{<\omega}$ and therefore
${\mathcal{N}}\models\mathfrak{C}(u)\to u\,\varepsilon\,(\gimel\mbox{\bf
V}^{<\omega})$ by Theorem 22. Moreover, we have
${\mathcal{N}}\models\mathfrak{C}(\emptyset)$.

In ${\mathcal{M}}$, the function $(u,v)\mapsto uv$, from $(\mbox{\bf
V}^{<\omega})^{2}$ into $\mbox{\bf V}^{<\omega}$, which is the concatenation
of sequences, is associative with $\emptyset$ as neutral element, also denoted
by $\mathbf{1}$ (monoïd).

This function extends to ${\mathcal{N}}$ into an application of
$\gimel(\mbox{\bf V}^{<\omega})^{2}$ into $\gimel(\mbox{\bf V}^{<\omega})$
with the same properties. Thus, we write $uvw$ for $u(vw),(uv)w$, etc.

The formula $\mathfrak{C}(uv)$ of ZFε means that $u,v$ are two compatible
finite sequences of elements of $C$, i.e. the union of their images has a
lower bound in $C$. Thus $\mathfrak{C}$ becomes a set of forcing conditions
equivalent to $C$ by means of this compatibility relation.

This formula has the following properties:

$\mbox{ $||-\,$}\mathfrak{C}(puvq)\to\mathfrak{C}(pvuq),\mbox{
$||-\,$}\mathfrak{C}(puvq)\to\mathfrak{C}(puq),\mbox{
$||-\,$}\mathfrak{C}(puq)\to\mathfrak{C}(puuq)$.

It will be convenient to have only one formula and to use simply the following
consequence:

\raisebox{-0.6pt}{\footnotesize2}⃝\raisebox{-0.6pt}{\footnotesize2}⃝  _There
exists a proof-like term $\mathfrak{c}$ such that_ $\mathfrak{c}\mbox{
$||-\,$}\mathfrak{C}(pqrtuvw)\to\mathfrak{C}(ptruuv)$.

Consider now, in the ground model ${\mathcal{M}}$, a r.a. ${\mathcal{A}}_{0}$
which gives the r.m. ${\mathcal{N}}$.

We suppose to have an operation $(\pi,\tau)\mapsto\pi^{\tau}$ from
$\Pi\\!\times\\!\Lambda$ into $\Pi$ such that:

$(\xi\,\mbox{\Large.}\,\pi)^{\tau}=\xi\,\mbox{\Large.}\,\pi^{\tau}$ for every
$\xi,\tau\in\Lambda$ and $\pi\in\Pi$.

and two new combinators $\chi$  _(read)_ and $\chi^{\prime}$ _(write)_ such
that:

$\chi\star\xi\,\mbox{\Large.}\,\pi^{\tau}\succ\succ\xi\star\tau\,\mbox{\Large.}\,\pi$
(i.e.
$\xi\star\tau\,\mbox{\Large.}\,\pi\in\bot\bot\Rightarrow\chi\star\xi\,\mbox{\Large.}\,\pi^{\tau}\in\bot\bot$)

$\chi^{\prime}\star\tau\,\mbox{\Large.}\,\xi\,\mbox{\Large.}\,\pi\succ\succ\xi\star\pi^{\tau}$
(i.e.
$\xi\star\pi^{\tau}\in\bot\bot\Rightarrow\chi^{\prime}\star\tau\,\mbox{\Large.}\,\xi\,\mbox{\Large.}\,\pi\in\bot\bot$).

Moreover, we suppose that $\chi,\chi^{\prime}$ may be used to form proof-like
terms.

Intuitively, $\pi^{\tau}$ is obtained by putting the term $\tau$ _at the end_
of the stack $\pi$, in the same way that $\tau\,\mbox{\Large.}\,\pi$ is
obtained by putting $\tau$ _at the top_ of $\pi$.

We define now, in the ground model ${\mathcal{M}}$, a new r.a.
${\mathcal{A}}_{1}$; its r.m. will be called _the extension of ${\mathcal{N}}$
by a $\mathfrak{C}$-generic (or a $C$-generic)_.

We define the terms
$\mbox{B}^{*},\mbox{C}^{*},\mbox{I}^{*},\mbox{K}^{*},\mbox{W}^{*},\mbox{\sf
cc}^{*}$ and $\mbox{k}^{*}_{\pi}$ by the conditions:

\raisebox{-0.6pt}{\footnotesize3}⃝\raisebox{-0.6pt}{\footnotesize3}⃝
$\mbox{B}^{*}=\mbox{B}$; $\mbox{I}^{*}=\mbox{I}$;
$\mbox{C}^{*}\star\xi\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\zeta\,\mbox{\Large.}\,\pi^{\tau}\succ\xi\star\zeta\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\pi^{\mathfrak{c}\tau}$;
i.e. $\mbox{C}^{*}=\lambda x\lambda y\lambda z(\chi)\lambda
t((\chi^{\prime})(\mathfrak{c})t)xzy$;
$\mbox{K}^{*}\star\xi\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\pi^{\tau}\succ\xi\star\pi^{\mathfrak{c}\tau}$;
i.e. $\mbox{K}^{*}=\lambda x\lambda y(\chi)\lambda
t((\chi^{\prime})(\mathfrak{c})t)x$;
$\mbox{W}^{*}\star\xi\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\pi^{\tau}\succ\xi\star\eta\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\pi^{\mathfrak{c}\tau}$;
i.e. $\mbox{W}^{*}=\lambda x\lambda y(\chi)\lambda
t((\chi^{\prime})(\mathfrak{c})t)xyy$;
$\mbox{k}^{*}_{\pi}\star\xi\,\mbox{\Large.}\,\varpi^{\tau}\succ\xi\star\pi^{\mathfrak{c}\tau}$;
i.e. $\mbox{k}^{*}_{\pi}=\lambda x(\chi)\lambda
t(\mbox{k}_{\pi})((\chi^{\prime})(\mathfrak{c})t)x$; $\mbox{\sf
cc}^{*}\star\xi\,\mbox{\Large.}\,\pi^{\tau}\succ\xi\star\mbox{k}^{*}_{\pi}\,\mbox{\Large.}\,\pi^{\mathfrak{c}\tau}$;
i.e. $\mbox{\sf cc}^{*}=\lambda x(\chi)\lambda t(\mbox{\sf cc})\lambda
k(((\chi^{\prime})(\mathfrak{c})t)x)\lambda x^{\prime}(\chi)\lambda
t^{\prime}(k)((\chi^{\prime})(\mathfrak{c})t^{\prime})x^{\prime}$.

When checking below the axioms of r.a., the property needed for each
combinator is:

\raisebox{-0.6pt}{\footnotesize4}⃝\raisebox{-0.6pt}{\footnotesize4}⃝ for
$\mbox{C}^{*}$: $\mathfrak{c}\mbox{
$||-\,$}\mathfrak{C}(prtv)\to\mathfrak{C}(ptrv)$; for $\mbox{K}^{*}$:
$\mathfrak{c}\mbox{ $||-\,$}\mathfrak{C}(pqr)\to\mathfrak{C}(pr)$; for
$\mbox{W}^{*}$: $\mathfrak{c}\mbox{
$||-\,$}\mathfrak{C}(puv)\to\mathfrak{C}(puuv)$; for $\mbox{\sf cc}^{*}$:
$\mathfrak{c}\mbox{ $||-\,$}\mathfrak{C}(pu)\to\mathfrak{C}(puu)$; for
$\mbox{k}^{*}_{\pi}$: $\mathfrak{c}\mbox{
$||-\,$}\mathfrak{C}(rtw)\to\mathfrak{C}(tr)$.

We get them replacing by $\mathbf{1}$ some of the variables $p,q,r,t,u,v,w$ in
the definition
\raisebox{-0.6pt}{\footnotesize2}⃝\raisebox{-0.6pt}{\footnotesize2}⃝ of
$\mathfrak{c}$.

We define the r.a. ${\mathcal{A}}_{1}$ by setting
$\mbox{\boldmath$\Lambda$}=\Lambda\\!\times\\!\mbox{\bf V}^{<\omega}$;
$\mbox{\boldmath$\Pi$}=\Pi\\!\times\\!\mbox{\bf V}^{<\omega}$;
$\mbox{\boldmath$\Lambda$}\star\mbox{\boldmath$\Pi$}=(\Lambda\star\Pi)\\!\times\\!\mbox{\bf
V}^{<\omega}$.

$(\xi,u)\,\mbox{\Large.}\,(\pi,v)=(\xi\,\mbox{\Large.}\,\pi,uv)$;

$(\xi,u)\star(\pi,v)=(\xi\star\pi,uv)$;

$(\xi,u)(\eta,v)=(\xi\eta,uv)$.

The pole $\bot\bot\bot$ of ${\mathcal{A}}_{1}$ is defined by:

$(\xi\star\pi,u)\in\bot\bot\bot\Leftrightarrow(\forall\tau\in\Lambda)(\tau\mbox{
$||-\,$}\mathfrak{C}(u)\Rightarrow\xi\star\pi^{\tau}\in\bot\bot)$.

The combinators are:

$\mbox{B}=(\mbox{B},\mathbf{1}),\mbox{C}=(\mbox{C}^{*},\mathbf{1}),\mbox{I}=(\mbox{I},\mathbf{1}),\mbox{K}=(\mbox{K}^{*},\mathbf{1}),\mbox{W}=(\mbox{W}^{*},\mathbf{1}),\mbox{cc}=(\mbox{\sf
cc}^{*},\mathbf{1})$;

$\mbox{\bf k}_{(\pi,u)}=(\mbox{k}^{*}_{\pi},u)$;
$\mbox{\mbox{PL}}_{{\mathcal{A}}_{1}}$ is
$\\{(\theta,\mathbf{1})\;;\;\theta\in\mbox{\mbox{PL}}_{{\mathcal{A}}_{0}}\\}$.

######  Theorem 23.

${\mathcal{A}}_{1}$ is a coherent r.a.

######  Proof 3.2.

Let us prove first that ${\mathcal{A}}_{1}$ is coherent: let
$\theta\in\mbox{\mbox{PL}}_{{\mathcal{A}}_{0}}$; by definition of the formula
$\mathfrak{C}$, there exists $\tau_{0}\in\mbox{\mbox{PL}}_{{\mathcal{A}}_{0}}$
such that $\tau_{0}\mbox{ $||-\,$}\mathfrak{C}(\mathbf{1})$.

Since $\chi^{\prime}\theta\tau_{0}\in\mbox{\mbox{PL}}_{{\mathcal{A}}_{0}}$,
there exists $\pi\in\Pi$ such that
$\chi^{\prime}\theta\tau_{0}\star\pi\notin\bot\bot$, thus
$\theta\star\pi^{\tau_{0}}\notin\bot\bot$, therefore
$(\theta,\mathbf{1})\star(\pi,\mathbf{1})\notin\bot\bot\bot$.

We check now that ${\mathcal{A}}_{1}$ is a r.a.:

  * •

$(\xi,u)\star(\eta,v)\,\mbox{\Large.}\,(\pi,w)\in\bot\bot\bot\Rightarrow(\xi,u)(\eta,v)\star(\pi,w)\in\bot\bot\bot$.

By hypothesis, we have
$(\xi\star\eta\,\mbox{\Large.}\,\pi,uvw)\in\bot\bot\bot$, therefore:

$(\forall\tau\in\Lambda)(\tau\mbox{
$||-\,$}\mathfrak{C}(uvw)\to\xi\star\eta\,\mbox{\Large.}\,\pi^{\tau}\in\bot\bot)$
and therefore:

$(\forall\tau\in\Lambda)(\tau\mbox{
$||-\,$}\mathfrak{C}(uvw)\to\xi\eta\star\pi^{\tau}\in\bot\bot)$ hence the
result.

  * •

$(\xi,u)\star(\eta,v)(\zeta,w)\,\mbox{\Large.}\,(\pi,z)\in\bot\bot\bot\Rightarrow(\mbox{B},\mathbf{1})\star(\xi,u)\,\mbox{\Large.}\,(\eta,v)\,\mbox{\Large.}\,(\zeta,w)\,\mbox{\Large.}\,(\pi,z)\in\bot\bot\bot$.

By hypothesis, we have
$(\xi\star\eta\zeta\,\mbox{\Large.}\,\pi,uvwz)\in\bot\bot\bot$ therefore:

$(\forall\tau\in\Lambda)(\tau\mbox{
$||-\,$}\mathfrak{C}(uvwz)\to\xi\star\eta\zeta\,\mbox{\Large.}\,\pi^{\tau}\in\bot\bot)$
thus:

$(\forall\tau\in\Lambda)(\tau\mbox{
$||-\,$}\mathfrak{C}(uvwz)\to\mbox{B}\star\xi\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\zeta\,\mbox{\Large.}\,\pi^{\tau}\in\bot\bot)$.

  * •

$(\xi,u)\star(\zeta,w)\,\mbox{\Large.}\,(\eta,v)\,\mbox{\Large.}\,(\pi,z)\in\bot\bot\bot\Rightarrow(\mbox{C}^{*},\mathbf{1})\star(\xi,u)\,\mbox{\Large.}\,(\eta,v)\,\mbox{\Large.}\,(\zeta,w)\,\mbox{\Large.}\,(\pi,z)\in\bot\bot\bot$.

By hypothesis, we have
$(\xi\star\zeta\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\pi,uwvz)\in\bot\bot\bot$,
therefore:

$(\forall\tau\in\Lambda)(\mathfrak{c}\tau\mbox{
$||-\,$}\mathfrak{C}(uwvz)\to\xi\star\zeta\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\pi^{\mathfrak{c}\tau}\in\bot\bot)$
therefore, by definition
\raisebox{-0.6pt}{\footnotesize3}⃝\raisebox{-0.6pt}{\footnotesize3}⃝ of
$\mbox{C}^{*}$:

$(\forall\tau\in\Lambda)(\mathfrak{c}\tau\mbox{
$||-\,$}\mathfrak{C}(uwvz)\to\mbox{C}^{*}\star\xi\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\zeta\,\mbox{\Large.}\,\pi^{\tau}\in\bot\bot)$.

But, by the property
\raisebox{-0.6pt}{\footnotesize4}⃝\raisebox{-0.6pt}{\footnotesize4}⃝ of
$\mathfrak{c}$, we have:

$\tau\mbox{ $||-\,$}\mathfrak{C}(uvwz)\to\mathfrak{c}\tau\mbox{
$||-\,$}\mathfrak{C}(uwvz)$, hence the result.

  * •

$(\xi,u)\star(\pi,v)\in\bot\bot\bot\Rightarrow(\mbox{I},\mathbf{1})\star(\xi,u)\,\mbox{\Large.}\,(\pi,v)\in\bot\bot\bot$.

Immediate.

  * •

$(\xi,u)\star(\pi,w)\in\bot\bot\bot\Rightarrow(\mbox{K}^{*},\mathbf{1})\star(\xi,u)\,\mbox{\Large.}\,(\eta,v)\,\mbox{\Large.}\,(\pi,w)\in\bot\bot\bot$.

By hypothesis, we have $(\xi\star\pi,uw)\in\bot\bot\bot$, therefore:

$(\forall\tau\in\Lambda)(\mathfrak{c}\tau\mbox{
$||-\,$}\mathfrak{C}(uw)\to\xi\star\pi^{\mathfrak{c}\tau}\in\bot\bot)$,
therefore by the definition
\raisebox{-0.6pt}{\footnotesize3}⃝\raisebox{-0.6pt}{\footnotesize3}⃝ of
$\mbox{K}^{*}$:

$(\forall\tau\in\Lambda)(\mathfrak{c}\tau\mbox{
$||-\,$}\mathfrak{C}(uw)\to\mbox{K}^{*}\star\xi\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\pi^{\tau}\in\bot\bot)$.
But, by \raisebox{-0.6pt}{\footnotesize4}⃝\raisebox{-0.6pt}{\footnotesize4}⃝,
we have:

$\tau\mbox{ $||-\,$}\mathfrak{C}(uvw)\to\mathfrak{c}\tau\mbox{
$||-\,$}\mathfrak{C}(uw)$, hence the result.

  * •

$(\xi,u)\star(\eta,v)\,\mbox{\Large.}\,(\eta,v)\,\mbox{\Large.}\,(\pi,w)\in\bot\bot\bot\Rightarrow(\mbox{W}^{*},\mathbf{1})\star(\xi,u)\,\mbox{\Large.}\,(\eta,v)\,\mbox{\Large.}\,(\pi,w)\in\bot\bot\bot$.

By hypothesis, we have
$(\xi\star\eta\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\pi,uvvw)\in\bot\bot\bot$,
therefore:

$(\forall\tau\in\Lambda)(\mathfrak{c}\tau\mbox{
$||-\,$}\mathfrak{C}(uvvw)\to\xi\star\eta\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\pi^{\mathfrak{c}\tau}\in\bot\bot)$,
thus, by the definition
\raisebox{-0.6pt}{\footnotesize3}⃝\raisebox{-0.6pt}{\footnotesize3}⃝ of
$\mbox{W}^{*}$:

$(\forall\tau\in\Lambda)(\mathfrak{c}\tau\mbox{
$||-\,$}\mathfrak{C}(uvvw)\to\mbox{W}^{*}\star\xi\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\pi^{\tau}\in\bot\bot)$.
Now, by \raisebox{-0.6pt}{\footnotesize4}⃝\raisebox{-0.6pt}{\footnotesize4}⃝,
we have:

$\tau\mbox{ $||-\,$}\mathfrak{C}(uvw)\to\mathfrak{c}\tau\mbox{
$||-\,$}\mathfrak{C}(uvvw)$, hence the result: $\tau\mbox{
$||-\,$}\mathfrak{C}(uvw)\to\mbox{W}^{*}\star\xi\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\pi^{\tau}\in\bot\bot$.

  * •

$(\xi,v)\star(\pi,u)\in\bot\bot\bot\Rightarrow(\mbox{k}^{*}_{\pi},u)\star(\xi,v)\,\mbox{\Large.}\,(\varpi,w)\in\bot\bot\bot$.

By hypothesis, we have $(\xi\star\pi,vu)\in\bot\bot\bot$, therefore:
$(\forall\tau\in\Lambda)(\mathfrak{c}\tau\mbox{
$||-\,$}\mathfrak{C}(vu)\to\xi\star\pi^{\mathfrak{c}\tau}\in\bot\bot)$, thus,
by the definition
\raisebox{-0.6pt}{\footnotesize3}⃝\raisebox{-0.6pt}{\footnotesize3}⃝ of
$\mbox{k}^{*}_{\pi}$:

$(\forall\tau\in\Lambda)(\mathfrak{c}\tau\mbox{
$||-\,$}\mathfrak{C}(vu)\to\mbox{k}^{*}_{\pi}\star\xi\,\mbox{\Large.}\,\varpi^{\tau}\in\bot\bot)$.
Now, by \raisebox{-0.6pt}{\footnotesize4}⃝\raisebox{-0.6pt}{\footnotesize4}⃝,
we have:

$\tau\mbox{ $||-\,$}\mathfrak{C}(uvw)\to\mathfrak{c}\tau\mbox{
$||-\,$}\mathfrak{C}(vu)$, hence the result: $\tau\mbox{
$||-\,$}\mathfrak{C}(uvw)\to\mbox{k}^{*}_{\pi}\star\xi\,\mbox{\Large.}\,\varpi^{\tau}\in\bot\bot$.

  * •

$(\xi,u)\star(\mbox{k}^{*}_{\pi},v)\,\mbox{\Large.}\,(\pi,v)\in\bot\bot\bot\Rightarrow(\mbox{\sf
cc}^{*},\mathbf{1})\star(\xi,u)\,\mbox{\Large.}\,(\pi,v)\in\bot\bot\bot$.

By hypothesis, we have
$(\xi\star\mbox{k}^{*}_{\pi}\,\mbox{\Large.}\,\pi,uvv)\in\bot\bot\bot$,
therefore:

$(\forall\tau\in\Lambda)(\mathfrak{c}\tau\mbox{
$||-\,$}\mathfrak{C}(uvv)\to\xi\star\mbox{k}^{*}_{\pi}\,\mbox{\Large.}\,\pi^{\mathfrak{c}\tau}\in\bot\bot)$,
thus, by the definition
\raisebox{-0.6pt}{\footnotesize3}⃝\raisebox{-0.6pt}{\footnotesize3}⃝ of
$\mbox{\sf cc}^{*}$:

$(\forall\tau\in\Lambda)(\mathfrak{c}\tau\mbox{
$||-\,$}\mathfrak{C}(uvv)\to\mbox{\sf
cc}^{*}\star\xi\,\mbox{\Large.}\,\pi^{\tau}\in\bot\bot)$. But, by
\raisebox{-0.6pt}{\footnotesize4}⃝\raisebox{-0.6pt}{\footnotesize4}⃝, we have:

$\tau\mbox{ $||-\,$}\mathfrak{C}(uv)\to\mathfrak{c}\tau\mbox{
$||-\,$}\mathfrak{C}(uvv)$, hence the result: $\tau\mbox{
$||-\,$}\mathfrak{C}(uv)\to\mbox{\sf
cc}^{*}\star\xi\,\mbox{\Large.}\,\pi^{\tau}\in\bot\bot$.

### The $\mathbf{C}$-forcing defined in ${\mathcal{N}}{\mathcal{N}}$

Let $F(\vec{a})$ be a closed formula of the language of ZF with parameters in
${\mathcal{M}}$.

We define the formula $p\raisebox{-0.86108pt}{\small$\;\Vdash\,$}F(\vec{a})$
(read “$p$ forces $F(\vec{a})$”) _as the formula of ZF ε which expresses the
$C$-forcing on ${\mathcal{N}}_{\in}$_. In this formula, the variable $p$ is
restricted to $\mbox{\bf V}^{<\omega}$.

We define a subset $(((F(\vec{a}))))$ of $\Pi$ by
$(((F(\vec{a}))))=\\{(\pi,p)\;;\;\pi\in\|p\raisebox{-0.86108pt}{\small$\;\nVdash\,$}\neg
F(\vec{a})\|\\}$.

######  Lemma 24.

For every formula $F(\vec{x})$ of ZF, there exist two proof-like terms
$\mathfrak{p}_{F},\mathfrak{p}^{\prime}_{F}$ of ${\mathcal{A}}$ such that:

i) $\xi\mbox{
$||-\,$}(p\raisebox{-0.86108pt}{\small$\;\Vdash\,$}F(\vec{a}))\Rightarrow(\mathfrak{p}_{F}\xi,p)\mbox{
$\||-\,$}(((F(\vec{a}))))$

ii) $(\xi,p)\mbox{
$\||-\,$}(((F(\vec{a}))))\Rightarrow\mathfrak{p}^{\prime}_{F}\xi\mbox{
$||-\,$}(p\raisebox{-0.86108pt}{\small$\;\Vdash\,$}F(\vec{a}))$

for every $\xi\in\Lambda$ and $p\in\mbox{\bf V}^{<\omega}$.

######  Proof 3.3.

By a well known property of forcing [Jec06, Kun92], the formula
$p\raisebox{-0.86108pt}{\small$\;\Vdash\,$}F(\vec{x})$ is equivalent, in ZFε,
to the formula $\forall q(\mathfrak{C}(pq)\to
q\raisebox{-0.86108pt}{\small$\;\nVdash\,$}\neg F(\vec{x}))$.

It follows that there are two proof-like terms
$\mathfrak{q}_{F},\mathfrak{q}_{F}^{\prime}$ such that:

(1) $\mathfrak{q}_{F}\mbox{
$||-\,$}(p\raisebox{-0.86108pt}{\small$\;\Vdash\,$}F(\vec{a}))\to\forall
q(\mathfrak{C}(pq)\to q\raisebox{-0.86108pt}{\small$\;\nVdash\,$}\neg
F(\vec{a}))$;

(2) $\mathfrak{q}^{\prime}_{F}\mbox{ $||-\,$}\forall q(\mathfrak{C}(pq)\to
q\raisebox{-0.86108pt}{\small$\;\nVdash\,$}\neg
F(\vec{a}))\to(p\raisebox{-0.86108pt}{\small$\;\Vdash\,$}F(\vec{a}))$.

  1. (i)

By applying (1) to the hypothesis, we obtain $\mathfrak{q}_{F}\xi\mbox{
$||-\,$}\forall q(\mathfrak{C}(pq)\to
q\raisebox{-0.86108pt}{\small$\;\nVdash\,$}\neg F(\vec{a}))$ that is:

$\forall\pi\forall q\forall\tau(\tau\mbox{
$||-\,$}\mathfrak{C}(pq),\pi\in\|q\raisebox{-0.86108pt}{\small$\;\nVdash\,$}\neg
F(\vec{a})\|\to\mathfrak{q}_{F}\xi\star\tau\,\mbox{\Large.}\,\pi\in\bot\bot)$.
It follows that:

$\forall\pi\forall q(\pi\in\|q\raisebox{-0.86108pt}{\small$\;\nVdash\,$}\neg
F(\vec{a})\|\to\forall\tau(\tau\mbox{
$||-\,$}\mathfrak{C}(pq)\to(\chi)(\mathfrak{q}_{F})\xi\star\pi^{\tau}\in\bot\bot))$.

Now $\pi\in\|q\raisebox{-0.86108pt}{\small$\;\nVdash\,$}\neg F(\vec{a})\|$ is
the same as $(\pi,q)\in(((F(\vec{a}))))$ and

$\forall\tau(\tau\mbox{
$||-\,$}\mathfrak{C}(pq)\to(\chi)(\mathfrak{q}_{F})\xi\star\pi^{\tau}\in\bot\bot)$
is the same as $(\mathfrak{p}_{F}\xi,p)\star(\pi,q)\in\bot\bot\bot$

with $\mathfrak{p}_{F}=\lambda x(\chi)(\mathfrak{q}_{F})x$. Thus we obtain
$(\mathfrak{p}_{F}\xi,p)\mbox{ $\||-\,$}(((F(\vec{a}))))$.

  2. (ii)

The hypothesis gives $\forall\pi\forall
q((\pi,q)\in(((F(\vec{a}))))\to(\xi\star\pi,pq)\in\bot\bot\bot)$ that is:

$\forall\pi\forall
q\forall\tau(\pi\in\|q\raisebox{-0.86108pt}{\small$\;\nVdash\,$}\neg
F(\vec{a})\|,\tau\mbox{
$||-\,$}\mathfrak{C}(pq)\to\xi\star\pi^{\tau}\in\bot\bot)$ and therefore:

$\forall\pi\forall q\forall\tau(\tau\mbox{
$||-\,$}\mathfrak{C}(pq),\pi\in\|q\raisebox{-0.86108pt}{\small$\;\nVdash\,$}\neg
F(\vec{a})\|\to\chi^{\prime}\xi\star\tau\,\mbox{\Large.}\,\pi\in\bot\bot)$.

It follows that $\chi^{\prime}\xi\mbox{ $||-\,$}\forall q(\mathfrak{C}(pq)\to
q\raisebox{-0.86108pt}{\small$\;\nVdash\,$}\neg F(\vec{a}))$ and therefore, by
(2):

$(\mathfrak{q}_{F}^{\prime})(\chi^{\prime})\xi\mbox{
$||-\,$}(p\raisebox{-0.86108pt}{\small$\;\Vdash\,$}F(\vec{a}))$. We set
$\mathfrak{p}^{\prime}_{F}=\lambda
x(\mathfrak{q}_{F}^{\prime})(\chi^{\prime})x$.

In the general theory of classical realizability, we define a truth value for
the formulas of ZFε and therefore, in particular, for the formulas of ZF. We
will define here directly a new truth value $\||F(a_{1},\ldots,a_{n})\||$ _for
a formula of ZF_ with parameters in ${\mathcal{M}}$ for the r.a.
${\mathcal{A}}_{1}$.

To this aim, we first define the truth values $\||a\notin b\||,\||a\subset
b\||$ of the atomic formulas of ZF; then that of $F(a_{1},\ldots,a_{n})$, by
induction on the length of the formula.

Theorem 2 (adequacy theorem) remains valid (cf. Remark 3):

$\||a\notin b\||=~{}(((a\notin b)))$; $\||a\subset b\||=(((a\subset b)))$;

$\||F\to F^{\prime}\||=\\{(\xi\,\mbox{\Large.}\,\pi,pq)\;;\;(\xi,p)\mbox{
$\||-\,$}F,(\pi,q)\in\||F^{\prime}\||\\}$;

$\||\forall
x\,F(x,a_{1},\ldots,a_{n})\||=\bigcup_{a}\||F(a,a_{1},\ldots,a_{n})\||$.

Of course  $\||-\,$ is defined by: $(\xi,p)\mbox{
$\||-\,$}F\Leftrightarrow(\forall(\pi,q)\in\||F\||)((\xi,p)\star(\pi,q)\in\bot\bot\bot)$.

######  Remark 25.

Be careful, as we said before, these are not the truth values, in the r.a.
${\mathcal{A}}_{1}$, of $a\notin b$ and $a\subset b$ _considered as formulas
of ZF ε_. We seek here to define directly the $C$-generic model on
${\mathcal{N}}_{\in}$ without going through a model of ZFε.

Theorem 26 below may be considered as a generalization of the well known
result about iteration of forcing: the r.a. ${\mathcal{A}}_{1}$, which is a
kind of product of ${\mathcal{A}}_{0}$ by $\mathfrak{C}$, gives the same r.m.
as the $\mathfrak{C}$-generic extension of ${\mathcal{N}}_{\in}$.

######  Theorem 26.

For each closed formula $F$ of ZF with parameters in the model
${\mathcal{N}}$, there exist two proof-like terms
$\chi_{{}_{F}},\chi^{\prime}_{{}_{F}}$, which only depend on the propositional
structure of $F$, such that we have, for every $\xi\in\Lambda$ and
$p\in\mbox{\bf V}^{<\omega}$:

$\xi\mbox{ $||-\,$}(p\raisebox{-0.86108pt}{\small$\;\Vdash\,$}F)$
$\Rightarrow$ $(\chi_{{}_{F}}\xi,p)\mbox{ $\||-\,$}F$ and $(\xi,p)\mbox{
$\||-\,$}F$ $\Rightarrow$ $\chi^{\prime}_{{}_{F}}\xi\mbox{
$||-\,$}(p\raisebox{-0.86108pt}{\small$\;\Vdash\,$}F)$.

The _propositional structure_ of $F$ is the propositional formula built with
the connective $\to$ and only two atoms $O_{\in},O_{\subset}$, which is
obtained from $F$ by deleting all quantifiers and by identifying all atomic
formulas $t\notin u,t\subset u$ respectively with $O_{\in},O_{\subset}$.

For instance, the propositional structure of the formula:

$\forall X(\forall x(\forall y((x,y)\notin Y\to y\notin X)\to x\notin
X)\to\forall x(x\notin X))$ is:

$((O_{\in}\to O_{\in})\to O_{\in})\to O_{\in}$.

######  Proof 3.4.

By recurrence on the length of $F$.

  * •

If $F$ is atomic, we have $F\equiv a\notin b$ or $a\subset b$. Apply Lemma 24
with $F(\vec{a})\equiv a\notin b$ or $F(\vec{a})\equiv a\subset b$.

  * •

If $F\equiv\forall x\,F^{\prime}$, then
$p\raisebox{-0.86108pt}{\small$\;\Vdash\,$}F\equiv\forall
x(p\raisebox{-0.86108pt}{\small$\;\Vdash\,$}F^{\prime})$. Therefore $\xi\mbox{
$||-\,$}p\raisebox{-0.86108pt}{\small$\;\Vdash\,$}F\equiv\forall x(\xi\mbox{
$||-\,$}(p\raisebox{-0.86108pt}{\small$\;\Vdash\,$}F^{\prime}))$.

Moreover, $(\xi,p)\mbox{ $\||-\,$}F\equiv\forall x((\xi,p)\mbox{
$\||-\,$}F^{\prime})$.

The result is immediate, from the recurrence hypothesis.

  * •

If $F\equiv F^{\prime}\to F^{\prime\prime}$, we have
$p\raisebox{-0.86108pt}{\small$\;\Vdash\,$}F\equiv\forall
q(q\raisebox{-0.86108pt}{\small$\;\Vdash\,$}F^{\prime}\to
pq\raisebox{-0.86108pt}{\small$\;\Vdash\,$}F^{\prime\prime})$ and therefore:

\raisebox{-0.6pt}{\footnotesize5}⃝\raisebox{-0.6pt}{\footnotesize5}⃝
$\xi\mbox{ $||-\,$}(p\raisebox{-0.86108pt}{\small$\;\Vdash\,$}F)$
$\Rightarrow$ $\forall\eta\forall q(\eta\mbox{
$||-\,$}(q\raisebox{-0.86108pt}{\small$\;\Vdash\,$}F^{\prime})\to\xi\eta\mbox{
$||-\,$}(pq\raisebox{-0.86108pt}{\small$\;\Vdash\,$}F^{\prime\prime}))$.

Suppose that $\xi\mbox{ $||-\,$}(p\raisebox{-0.86108pt}{\small$\;\Vdash\,$}F)$
and set $\chi_{F}=\lambda x\lambda
y(\chi_{F^{\prime\prime}})(x)(\chi^{\prime}_{F^{\prime}})y$.

We must show $(\chi_{F}\xi,p)\mbox{ $\||-\,$}F^{\prime}\to F^{\prime\prime}$;
thus, let $(\eta,q)\mbox{ $\||-\,$}F^{\prime}$ and
$(\pi,r)\in\||F^{\prime\prime}\||$.

We must show
$(\chi_{F}\xi,p)\star(\eta,q)\,\mbox{\Large.}\,(\pi,r)\in\bot\bot\bot$ that is
$(\chi_{F}\xi\star\eta\,\mbox{\Large.}\,\pi,pqr)\in\bot\bot\bot$.

Thus, let $\tau\mbox{ $||-\,$}\mathfrak{C}(pqr)$; we must show
$\chi_{F}\xi\star\eta\,\mbox{\Large.}\,\pi^{\tau}\in\bot\bot$ or else
$\chi_{F}\star\xi\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\pi^{\tau}\in\bot\bot$.

From the recurrence hypothesis applied to $(\eta,q)\mbox{
$\||-\,$}F^{\prime}$, we have $\chi^{\prime}_{F^{\prime}}\eta\mbox{
$||-\,$}(q\raisebox{-0.86108pt}{\small$\;\Vdash\,$}F^{\prime})$.

From \raisebox{-0.6pt}{\footnotesize5}⃝\raisebox{-0.6pt}{\footnotesize5}⃝, we
have therefore $(\xi)(\chi^{\prime}_{F^{\prime}})\eta\mbox{
$||-\,$}(pq\raisebox{-0.86108pt}{\small$\;\Vdash\,$}F^{\prime\prime})$.

Applying again the recurrence hypothesis, we get:

$((\chi_{F^{\prime\prime}})(\xi)(\chi^{\prime}_{F^{\prime}})\eta,pq)\mbox{
$\||-\,$}F^{\prime\prime}$. But since $(\pi,r)\in\||F^{\prime\prime}\||$, we
have:

$((\chi_{F^{\prime\prime}})(\xi)(\chi^{\prime}_{F^{\prime}})\eta,pq)\star(\pi,r)\in\bot\bot\bot$,
that is
$((\chi_{F^{\prime\prime}})(\xi)(\chi^{\prime}_{F^{\prime}})\eta\star\pi,pqr)\in\bot\bot\bot$.

Since $\tau\mbox{ $||-\,$}\mathfrak{C}(pqr)$, we have
$(\chi_{F^{\prime\prime}})(\xi)(\chi^{\prime}_{F^{\prime}})\eta\star\pi^{\tau}\in\bot\bot$.

But, by definition of $\chi_{F}$, we have
$\chi_{F}\star\xi\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\pi^{\tau}\succ(\chi_{F^{\prime\prime}})(\xi)(\chi^{\prime}_{F^{\prime}})\eta\star\pi^{\tau}$

which gives the desired result:
$\chi_{F}\star\xi\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\pi^{\tau}\in\bot\bot$.

Suppose now that $(\xi,p)\mbox{ $\||-\,$}F^{\prime}\to F^{\prime\prime}$; we
set $\chi^{\prime}_{F}=\lambda x\lambda
y(\chi^{\prime}_{F^{\prime\prime}})(x)(\chi_{F^{\prime}})y$.

We must show $\chi^{\prime}_{F}\xi\mbox{
$||-\,$}(p\raisebox{-0.86108pt}{\small$\;\Vdash\,$}F^{\prime}\to
F^{\prime\prime})$ that is $\forall q(\chi^{\prime}_{F}\xi\mbox{
$||-\,$}(q\raisebox{-0.86108pt}{\small$\;\Vdash\,$}F^{\prime}\to
pq\raisebox{-0.86108pt}{\small$\;\Vdash\,$}F^{\prime\prime}))$.

Thus, let $\eta\mbox{
$||-\,$}q\raisebox{-0.86108pt}{\small$\;\Vdash\,$}F^{\prime}$ and
$\pi\in\|pq\raisebox{-0.86108pt}{\small$\;\Vdash\,$}F^{\prime\prime}\|$; we
must show $\chi^{\prime}_{F}\xi\star\eta\,\mbox{\Large.}\,\pi\in\bot\bot$.

By the recurrence hypothesis, we have $(\chi_{F^{\prime}}\eta,q)\mbox{
$\||-\,$}F^{\prime}$, therefore $(\xi,p)(\chi_{F^{\prime}}\eta,q)\mbox{
$\||-\,$}F^{\prime\prime}$

or else, by definition of the algebra ${\mathcal{A}}_{1}$:
$((\xi)(\chi_{F^{\prime}})\eta,pq)\mbox{ $\||-\,$}F^{\prime\prime}$.

Applying again the recurrence hypothesis, we have
$(\chi^{\prime}_{F^{\prime\prime}})(\xi)(\chi_{F^{\prime}})\eta\mbox{
$||-\,$}(pq\raisebox{-0.86108pt}{\small$\;\Vdash\,$}F^{\prime\prime})$

and therefore
$(\chi^{\prime}_{F^{\prime\prime}})(\xi)(\chi_{F^{\prime}})\eta\star\pi\in\bot\bot$.
But we have, by definition of $\chi^{\prime}_{F}$:

$\chi^{\prime}_{F}\xi\star\eta\,\mbox{\Large.}\,\pi\succ\chi^{\prime}_{F}\star\xi\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\pi\succ(\chi^{\prime}_{F^{\prime\prime}})(\xi)(\chi_{F^{\prime}})\eta\star\pi$;

the desired result
$\chi^{\prime}_{F}\xi\star\eta\,\mbox{\Large.}\,\pi\in\bot\bot$ follows.

######  Theorem 27.

For each axiom $A$ of ZF, there exists a proof like term $\Theta\\!_{A}$ of
the r.a. ${\mathcal{A}}_{0}$ such that $(\Theta\\!_{A},\mathbf{1})\mbox{
$\||-\,$}A$.

######  Proof 3.5.

Indeed, if we denote by ${\mathcal{N}}_{\in}[G]$ the $C$-generic model over
${\mathcal{N}}_{\in}$, with $G\subseteq C$ being the generic set, we have
${\mathcal{N}}_{\in}[G]\models$ ZF. Therefore,
${\mathcal{N}}\models(\mathbf{1}\raisebox{-0.86108pt}{\small$\;\Vdash\,$}A)$,
which means that there is a proof-like term $\Theta^{\prime}\\!\\!_{A}$ such
that $\Theta^{\prime}\\!\\!_{A}\mbox{
$||-\,$}(\mathbf{1}\raisebox{-0.86108pt}{\small$\;\Vdash\,$}A)$. By Theorem
26, we can take $\Theta\\!_{A}=\chi_{A}\Theta^{\prime}\\!\\!_{A}$.

##  4\. The algebra $\mathfrak{A}_{0}$

We define a r.a. $\mathfrak{A}_{0}$ which gives a very interesting r.m.
${\mathcal{N}}$. In the following, we use only this r.a. and a generic
extension $\mathfrak{A}_{1}$.

The terms of $\mathfrak{A}_{0}$ are finite sequences of symbols:

$),(,\mbox{B},\mbox{C},\mbox{I},\mbox{K},\mbox{W},\mbox{\sf
cc},\mbox{a},\mbox{p},\gamma,\kappa,\mbox{\rm
e},\chi,\chi^{\prime},h_{0},h_{1},\ldots,h_{i},\ldots$

$\Lambda$ is the least set which contains these symbols (except parentheses)
and is such that:

$t,u\in\Lambda\Rightarrow(t)u\in\Lambda$.

A stack is a finite sequence of terms, separated by the symbol . and
terminated by the symbol $\pi_{0}$ _(the empty stack)_.

$\Pi$ is therefore the least set such that $\pi_{0}\in\Pi$ and
$t\in\Lambda,\pi\in\Pi\Rightarrow t\,\mbox{\Large.}\,\pi\in\Pi$.

$\mbox{k}_{\pi}$ is defined by recurrence: $\mbox{k}_{\pi_{0}}=\mbox{a}$;
$\mbox{k}_{t.\pi}=\lambda
x(\mbox{k}_{\pi})(x)t=((\mbox{C})(\mbox{B})\mbox{k}_{\pi})t$.

The application $(\tau,\pi)\mapsto\pi^{\tau}$ from $\Lambda\\!\times\\!\Pi$
into $\Pi$ consists in replacing $\pi_{0}$ by $\tau\,\mbox{\Large.}\,\pi_{0}$.

It is therefore recursively defined by:
$\pi_{0}^{\tau}=\tau\,\mbox{\Large.}\,\pi_{0}$;
$(t\,\mbox{\Large.}\,\pi)^{\tau}=t\,\mbox{\Large.}\,\pi^{\tau}$.

$\Lambda\star\Pi$ is $\Lambda\\!\times\\!\Pi$.

$\bot\bot$ is the least subset of $\Lambda\star\Pi$ satisfying the conditions:

  1. (1)

$\mbox{p}\star\pi\in\bot\bot$ for every stack $\pi\in\Pi$ _(stop)_ ;

  2. (2)

$\xi\star\pi_{0}\in\bot\bot\Rightarrow\mbox{a}\star\xi\,\mbox{\Large.}\,\pi\in\bot\bot$
for every $\xi\in\Lambda,\pi\in\Pi$ _(abort)_ ;

  3. (3)

If at least two out of $\xi\star\pi,\eta\star\pi,\zeta\star\pi$ are in
$\bot\bot$, then
$\gamma\star\xi\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\zeta\,\mbox{\Large.}\,\pi\in\bot\bot$
_(fork)_ ;

  4. (4)

$\xi\star\pi\in\bot\bot\Rightarrow\mbox{\rm e}\star
h_{i}\,\mbox{\Large.}\,h_{i}\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\xi\,\mbox{\Large.}\,\pi\in\bot\bot$
for every $\xi,\eta\in\Lambda$ and $i\in\mathbb{N}$ _(elimination of
constants)_ ;

  5. (5)

$\xi\star\pi\in\bot\bot\Rightarrow\mbox{\rm e}\star
h_{i}\,\mbox{\Large.}\,h_{j}\,\mbox{\Large.}\,\xi\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\pi\in\bot\bot$
for every $\xi,\eta\in\Lambda$ and $i,j\in\mathbb{N},i\neq j$ _(elimination of
constants)_ ;

  6. (6)

$\xi\star
h_{n}\,\mbox{\Large.}\,\pi\in\bot\bot\Rightarrow\kappa\star\xi\,\mbox{\Large.}\,\pi\in\bot\bot$
if $h_{n}$ does not appear in $\xi,\pi$ _(introduction of constants)_ ;

and also the general axiomatic conditions for
$\mbox{B},\mbox{C},\mbox{I},\mbox{K},\mbox{W},\mbox{\sf
cc},\chi,\chi^{\prime}$ and the application:

  1. (7)

$\xi\star\eta\,\mbox{\Large.}\,\pi\in\bot\bot\Rightarrow(\xi)\eta\star\pi\in\bot\bot$
_(push)_ ;

  2. (8)

$\xi\star\pi\in\bot\bot\Rightarrow\mbox{I}\star\xi\,\mbox{\Large.}\,\pi\in\bot\bot$
_(no operation)_ ;

  3. (9)

$\xi\star\pi\in\bot\bot\Rightarrow\mbox{K}\star\xi\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\pi\in\bot\bot$
_(delete)_ ;

  4. (10)

$\xi\star\eta\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\pi\in\bot\bot\Rightarrow\mbox{W}\star\xi\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\pi\in\bot\bot$
_(copy)_ ;

  5. (11)

$\xi\star\zeta\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\pi\in\bot\bot\Rightarrow\mbox{C}\star\xi\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\zeta\,\mbox{\Large.}\,\pi\in\bot\bot$
_(switch)_ ;

  6. (12)

$\xi\star(\eta)\zeta\,\mbox{\Large.}\,\pi\in\bot\bot\Rightarrow\mbox{B}\star\xi\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\zeta\,\mbox{\Large.}\,\pi\in\bot\bot$
_(apply)_ ;

  7. (13)

$\xi\star\mbox{k}_{\pi}\,\mbox{\Large.}\,\pi\in\bot\bot\Rightarrow\mbox{\sf
cc}\star\xi\,\mbox{\Large.}\,\pi\in\bot\bot$ _(save the stack)_ ;

  8. (14)

$\xi\star\tau\,\mbox{\Large.}\,\pi\in\bot\bot\Rightarrow\chi\star\xi\,\mbox{\Large.}\,\pi^{\tau}\in\bot\bot$
_(read the end of the stack)_ ;

  9. (15)

$\xi\star\pi^{\tau}\in\bot\bot\Rightarrow\chi^{\prime}\star\tau\,\mbox{\Large.}\,\xi\,\mbox{\Large.}\,\pi\in\bot\bot$
_(write at the end of the stack)_.

The property

$\xi\star\pi\in\bot\bot\Rightarrow\mbox{k}_{\pi}\star\xi\,\mbox{\Large.}\,\varpi\in\bot\bot$
_(restore the stack)_

now follows easily from the definition of $\mbox{k}_{\pi}$.

A term is defined to be _proof-like_ if it contains neither
$\mbox{a},\mbox{p}$ nor any $h_{i}$.

If $\xi\in$ PL (the set of proof-like terms), then the process
$\xi\star\pi_{0}$ does not contain the symbol p; thus
$\xi\star\pi_{0}\notin\bot\bot$. It follows that _the algebra
$\mathfrak{A}_{0}$ is coherent._

######  Theorem 28.

The Boolean algebra $\gimel 2$ has at most 4 elements.

######  Proof 4.1.

Let us show that $\gamma\mbox{ $||-\,$}\forall x^{\gimel 2}\forall y^{\gimel
2}(xy\neq 0,y\neq 1,xy\neq y\to\bot)$. This means exactly that $\gamma$
realizes the three formulas
$(\bot,\bot,\top\to\bot),\,(\bot,\top,\bot\to\bot)$ and
$(\top,\bot,\bot\to\bot)$, which follows immediately from rule 3 of the
definition of $\bot\bot$.

If $\gimel 2$ is trivial, everything in the following is also (cf. Remark 42).
Therefore, we now assume that $\gimel 2$ has 4 elements.

Let $a_{0},a_{1}$ be the atoms of $\gimel 2$. Then
${\mathcal{M}}_{a_{0}}=a_{0}{\mathcal{N}}$ and
${\mathcal{M}}_{a_{1}}=a_{1}{\mathcal{N}}$ are classes in the r.m.
${\mathcal{N}}$ respectively defined by the formulas $x=a_{0}x$ and
$x=a_{1}x$.

We define the binary functional $\sqcup$ in ${\mathcal{N}}$ as the extension
of the functional $(x,y)\mapsto x\cup y$ on ${\mathcal{M}}$. We do not use the
symbol $\cup$, because it already denotes the union. For instance, we have
$\gimel\\{0\\}\sqcup\gimel\\{1\\}=\gimel 2$ but
$\gimel\\{0\\}\cup\gimel\\{1\\}=\\{0,1\\}$.

The identity $x=a_{0}x\sqcup a_{1}x$ gives a bijection from ${\mathcal{N}}$
onto ${\mathcal{M}}_{a_{0}}\\!\times\\!{\mathcal{M}}_{a_{1}}$.

We have ${\mathcal{M}}\prec{\mathcal{M}}_{a_{0}},{\mathcal{M}}_{a_{1}}$. Let
us show that one of them, say ${\mathcal{M}}_{a_{0}}$, is well founded in
${\mathcal{N}}$ and therefore:

${\mathcal{M}}_{a_{0}}={\mathcal{M}}_{\mathcal{D}}$ and the class of ordinals
On is defined in ${\mathcal{N}}$.

######  Lemma 29.

The relation $\langle x\in y\rangle=1$ is well founded.

######  Proof 4.2.

We show $\mbox{\sf Y}\mbox{ $||-\,$}\forall y(\forall x(\langle x\in
y\rangle=1\hookrightarrow F(x))\to F(y))\to\forall y\,F(y)$ for any formula
$F$ of ZFε. Let $\xi\mbox{ $||-\,$}\forall y(\forall x(\langle x\in
y\rangle=1\hookrightarrow F(x))\to F(y))$. We show, by induction on
$\mbox{rk}(y_{0})$ that $\mbox{\sf Y}\xi\mbox{ $||-\,$}F(y_{0})$. Thus we have
$(\forall x\in y_{0})(\mbox{\sf Y}\xi\mbox{ $||-\,$}F(x))$ i.e. $\mbox{\sf
Y}\xi\mbox{ $||-\,$}\forall x(\langle x\in y_{0}\rangle=1\hookrightarrow
F(x))$ and therefore $(\xi)(\mbox{\sf Y})\xi\mbox{ $||-\,$}F(y_{0})$ by
hypothesis on $\xi$. Hence the result since $\mbox{\sf
Y}\xi\succ(\xi)(\mbox{\sf Y})\xi$.

Now, the relation $\langle x\in y\rangle=1$ is the product of the relations
$\langle a_{0}x\in a_{0}y\rangle=a_{0}$ and $\langle a_{1}x\in
a_{1}y\rangle=a_{1}$ respectively defined on $a_{0}{\mathcal{N}}$ and
$a_{1}{\mathcal{N}}$. Since their product is well founded, one of them must
be.

######  Remark 30.

If the ground model ${\mathcal{M}}$ satisfies V = L, then
${\mathcal{M}}_{a_{0}}={\mathcal{M}_{\mathcal{D}}}$ is isomorphic to
L${}^{{\mathcal{N}}_{\in}}$, the class of constructible sets of
${\mathcal{N}}_{\in}$.

### Execution of processes

If a given process $\xi\star\pi$ is in $\bot\bot$, it is obtained by applying
precisely one of the rules of definition of $\bot\bot$: if $\xi$ is an
application, it is rule 7, else $\xi$ is an instruction and there is one and
only one corresponding rule.

In this way, we get a finite tree, which is the proof that
$\xi\star\pi\in\bot\bot$; it is linear, except in the case of rule 3
(instruction $\gamma$) where there is a triple branch. This tree is called
_the execution of the process $\xi\star\pi$_.

We can, of course, build this tree for any process; it may then be infinite.

### Computing with the instruction $\gamma\gamma$

Let us consider, in the ground model ${\mathcal{M}}$, some functions
$f_{i}:\mathbb{N}^{k_{i}}\to\mathbb{N}$, satisfying a set of axioms of the
form:

$(\forall\vec{x}\in\mathbb{N}^{k})(t_{0}[\vec{x}]=u_{0}[\vec{x}],\ldots,t_{n-1}[\vec{x}]=u_{n-1}[\vec{x}]\to
t[\vec{x}]=u[\vec{x}])$
where $t_{i},u_{i}$ are terms built with the symbols $f_{i}$ and the variables
$\vec{x}$.

Moreover, one of these axioms concerns a particular function $f$, and says
that $f$ has at most one zero: $(\forall x,y\in\mathbb{N})(f[x]=f[y]=0\to
x=y)$.

These function symbols are also interpreted in ${\mathcal{N}}$ where we have
$f_{i}:\gimel\mathbb{N}^{k_{i}}\to\gimel\mathbb{N}$ and in this way, we have a
set ${\mathcal{E}}$ of realized axioms:

$\mbox{I}\mbox{
$||-\,$}\forall\vec{x}^{\gimel\mathbb{N}^{k}}(t_{0}[\vec{x}]=u_{0}[\vec{x}],\ldots,t_{n-1}[\vec{x}]=u_{n-1}[\vec{x}]\hookrightarrow
t[\vec{x}]=u[\vec{x}])$

and in particular:

$\mbox{I}\mbox{ $||-\,$}\forall x^{\gimel\mathbb{N}}\forall
y^{\gimel\mathbb{N}}(f[x]=0,f[y]=0\hookrightarrow x=y)$.

Now suppose that, with the axioms ${\mathcal{E}}$ and some other axioms
realized in ${\mathcal{N}}\\!$, which do not contain the symbols $f_{i}$, like
for instance:

${\mathcal{E}}$ \+ ZFε\+ _$\gimel 2$ has at most 4 elements_ \+
_$\gimel\mathbb{N}$ is countable + $\cdots$_

we can prove $\exists n^{\mbox{\footnotesize int}}(f[n]=0)$. Since all these
axioms are realized, we get, by Theorem 2, a proof-like term $\theta$ such
that $\theta\mbox{ $||-\,$}\forall n^{\mbox{\footnotesize int}}(f[n]\neq
0)\to\bot$ and $\theta$ may contain the instructions $\mbox{\rm e},\kappa$
and, above all, $\gamma$.

We shall show how $\theta$ allows to compute the (unique) solution $n_{0}$ of
the equation $f[n]=0$.

Note that _we do not assume that the $f_{i}$ (in particular $f$) are
recursive_ (in fact, it is not even necessary that their domain or range is
$\mathbb{N}$). On the other hand, we may add symbols for all recursive
functions, since they are defined by axiom systems of this form.

Let us add a term constant $\delta$ and the rule
$\delta\star\underline{n}_{0}\,\mbox{\Large.}\,\pi\in\bot\bot$ in the
definition of $\bot\bot$ (of course, without knowing the actual value of
$n_{0}$). Thus, we have $\delta\mbox{ $||-\,$}\forall n^{\mbox{\footnotesize
int}}(f[n]\neq 0)$ and therefore
$\theta\star\delta\,\mbox{\Large.}\,\pi_{0}\in\bot\bot$.

But any process $\xi\star\pi\in\bot\bot$ which does not contain p (but
possibly containing $\delta$) computes $n_{0}$. We show this by recurrence on
the number of applications of rules for $\bot\bot$ used to build it:

If this number is 1, the process is
$\delta\star\underline{n}_{0}\,\mbox{\Large.}\,\pi$. Else, the only non
trivial case is when the process is
$\gamma\star\xi\,\mbox{\Large.}\,\eta\,\mbox{\Large.}\,\zeta\,\mbox{\Large.}\,\pi$
and when two out of the three processes
$\xi\star\pi,\eta\star\pi,\zeta\star\pi$ are in $\bot\bot$ (but we do not know
which). By the recurrence hypothesis, at least two of them will give the
integer $n_{0}$ which is therefore determined as the only integer obtained at
least two times. Example:
$\gamma\star(((\gamma)(\delta)\underline{n})(\delta)\underline{n})(\delta)\underline{n}_{0}\,\mbox{\Large.}\,(((\gamma)(\delta)\underline{n}_{0})(\delta)\underline{n})(\delta)\underline{n}_{0}\,\mbox{\Large.}\,(((\gamma)(\delta)\underline{n})(\delta)\underline{n}_{0})(\delta)\underline{n}_{0}\,\mbox{\Large.}\,\pi$.

######  Remark 31.

Since $f$ is not supposed recursive, the trivial method to find $n_{0}$ by
trying $0,1,2,\ldots$ may not be available. A working algorithm is by proving
$f[n_{0}]=0$ by equational deduction from ${\mathcal{E}}$. Both are, in
general, very heavy or totally impracticable. Moral: it is better to use the
powerful set theoretical axioms than only the weak equational ones to get a
working program.

If $f$ may have several zeroes, we can easily define $f^{\prime}$ by a system
of equations such that $f^{\prime}$ has only one zero which is the first zero
of $f$, and apply the method to $f^{\prime}$. This supposes $f$ to be
recursive.

###  $\gimel\gimel$2 is not (always) trivial

Although this will not be used in the following, it is interesting to show
that there is a r.m. of $\mathfrak{A}_{0}$ in which $\gimel 2$ is not trivial
and is therefore the 4-elements Boolean algebra.

######  Lemma 32.

If $\theta\mbox{ $||-\,$}\forall x^{\gimel 2}(x\neq 0,x\neq 1\to\bot)$ then,
for any formulas $F,G$:

$\theta^{\prime}\mbox{ $||-\,$}F,G\to F$ and $\theta^{\prime}\mbox{
$||-\,$}F,G\to G$ with $\theta^{\prime}=\lambda x\lambda y(\mbox{\sf
cc})\lambda k((\theta)(k)x)(k)y$.

######  Proof 4.3.

The hypothesis means that $\theta\mbox{ $||-\,$}\bot,\top\to\bot$ and
$\theta\mbox{ $||-\,$}\top,\bot\to\bot$.

We have $x:F,y:G,k:\neg F\vdash
kx:\bot,(\theta)(k)x:\top\to\bot,((\theta)(k)x)(k)y:\bot$.

It follows that $(\mbox{\sf cc})\lambda k((\theta)(k)x)(k)y:F$ hence the first
result.

We have $x:F,y:G,k:\neg G\vdash
ky:\bot,(\theta)(k)x:\bot\to\bot,((\theta)(k)x)(k)y:\bot$.

It follows that $(\mbox{\sf cc})\lambda k((\theta)(k)x)(k)y:G$ hence the
second result.

Suppose that, in every r.m. for the r.a. $\mathfrak{A}_{0}$, the Boolean
algebra $\gimel 2$ is trivial.

Then the hypothesis of Lemma 32 is satisfied for some proof-like term
$\theta$.

Choose the formulas $F\equiv\exists n^{\mbox{\footnotesize int}}(n=0)$ and
$G\equiv\exists n^{\mbox{\footnotesize int}}(n=1)$. Then, we have $\lambda
x\,x\underline{0}\mbox{ $||-\,$}F$ and $\lambda x\,x\underline{1}\mbox{
$||-\,$}G$. By Lemma 32, it follows that
$\theta^{\prime\prime}=((\theta^{\prime})\lambda x\,x\underline{0})\lambda
x\,x\underline{1}\mbox{ $||-\,$}F$ and also $\mbox{ $||-\,$}G$.

Then, by the algorithm given above, the proof-like term
$\theta^{\prime\prime}$ computes simultaneously $0$ and $1$, which is a
contradiction.

###  $\gimel\gimel\mathbb{N}\mathbb{N}$ is countable

We define two sets, in the ground model ${\mathcal{M}}$:

$\mathbb{H}=\\{h_{i}\;;\;i\in\mathbb{N}\\}$,
$\mbox{H}=\\{(h_{i},h_{i}\,\mbox{\Large.}\,\pi)\;;\;i\in\mathbb{N},\pi\in\Pi\\}$
and also the bijection $\mbox{h}:\mathbb{N}\to\mathbb{H}$ such that
$\mbox{h}[i]=h_{i}$ for every $i\in\mathbb{N}$.

This bijection extends to the model ${\mathcal{N}}$ into a bijection
$\mbox{h}:\gimel\mathbb{N}\to\gimel\mathbb{H}$. Moreover, we have trivially
$\mbox{ $||-\,$}\mbox{H}\subseteq\gimel\mathbb{H}$; in fact $\mbox{I}\mbox{
$||-\,$}\forall x(x\,\varepsilon\\!\\!\\!/\,\gimel\mathbb{H}\to
x\,\varepsilon\\!\\!\\!/\,\mbox{H}$).

######  Lemma 33.

$\mbox{ $||-\,$}\forall i^{\gimel\mathbb{N}}\forall
j^{\gimel\mathbb{N}}(\mbox{h}[i]\,\varepsilon\,\mbox{H},\mbox{h}[j]\,\varepsilon\,\mbox{H},\langle
i=j\rangle\neq 0\to i=j)$.

######  Proof 4.4.

By definition of H, we have
$\|\mbox{h}[i]\,\varepsilon\\!\\!\\!/\,\mbox{H}\|=\|\\{h_{i}\\}\to\bot\|$.

Therefore, it suffices to show that $\mbox{\rm e}\mbox{
$||-\,$}\\{h_{i}\\},\\{h_{j}\\},\langle i=j\rangle\neq 0,i\neq j\to\bot$.

Let $t\mbox{ $||-\,$}\langle i=j\rangle\neq 0$ and $u\mbox{ $||-\,$}i\neq j$.
We must show $\mbox{\rm e}\star
h_{i}\,\mbox{\Large.}\,h_{j}\,\mbox{\Large.}\,t\,\mbox{\Large.}\,u\,\mbox{\Large.}\,\pi\in\bot\bot$,
which follows immediately from the execution rule of e.

Thus we have ${\mathcal{N}}\models\forall i^{\gimel\mathbb{N}}\forall
j^{\gimel\mathbb{N}}(\mbox{h}[i]\,\varepsilon\,\mbox{H},\mbox{h}[j]\,\varepsilon\,\mbox{H},ia_{0}=ja_{0}\to
i=j)$. It follows that:

${\mathcal{N}}\models$ _( H is countable)_.

Indeed, if $i\,\varepsilon\,\gimel\mathbb{N}$ and
$\mbox{h}[i]\,\varepsilon\,\mbox{H}$, then $i$ is determined by $ia_{0}$,
which is an integer of ${\mathcal{M}}_{a_{0}}$ and therefore an integer of
${\mathcal{N}}$.

Define the function symbols pr0, pr${}_{1}:\mathbb{N}\to\mathbb{N}$ by:

$n=\mbox{pr}_{1}[n]+\frac{1}{2}(\mbox{pr}_{0}[n]+\mbox{pr}_{1}[n])(\mbox{pr}_{0}[n]+\mbox{pr}_{1}[n]+1)$
(bijection from $\mathbb{N}^{2}$ onto $\mathbb{N}$).

######  Theorem 34.

i) $\kappa\mbox{ $||-\,$}\forall\nu^{\gimel\mathbb{N}}\exists
n^{\gimel\mathbb{N}}\\{\mbox{h}[n]\,\varepsilon\,\mbox{H},\nu=\mbox{pr}_{1}[n]\\}$.

ii) $\mbox{ $||-\,$}\gimel\mathbb{N}$ is countable.

######  Proof 4.5.

i) Let $\nu\in\mathbb{N},\pi\in\Pi$ and $\xi\mbox{ $||-\,$}\forall
n^{\gimel\mathbb{N}}\\{\nu=\mbox{pr}_{1}[n]\hookrightarrow\mbox{h}[n]\,\varepsilon\\!\\!\\!/\,\mbox{H}\\}$.
Therefore, we have $\xi\star h_{n}\,\mbox{\Large.}\,\pi\in\bot\bot$ for all
$n\in\mathbb{N}$ such that $\nu=\mbox{pr}_{1}[n]$. There is an infinity of
such $n$, so that we can choose one such that $h_{n}$ does not appear in
$\xi,\pi$. It follows that $\kappa\star\xi\,\mbox{\Large.}\,\pi\in\bot\bot$.

ii) Since $\mbox{h}:\gimel\mathbb{N}\to\gimel\mathbb{H}$ is a bijection, we
obtain a surjection from H onto $\gimel\mathbb{N}$. It follows that
${\mathcal{N}}\models$ (_$\gimel\mathbb{N}$ is countable_).

######  Theorem 35.

${\mathcal{N}}\models$ NEPC (the non extensional principle of choice).

This means that for any formula $R(x,y)$ of ZFε, there is a binary relation
$\Phi(x,y)$ such that:

$\mbox{ $||-\,$}\forall x\forall y\forall
y^{\prime}(\Phi(x,y),\Phi(x,y^{\prime})\to y=y^{\prime})$ (functional
relation);

$\mbox{ $||-\,$}\forall x\forall y(R(x,y)\to\exists
y^{\prime}\\{R(x,y^{\prime}),\Phi(x,y^{\prime})\\})$ (choice).

This does not give the usual principle of choice in the model
${\mathcal{N}}_{\in}$ of ZF because, even if $R$ is compatible with the
extensional equivalence $=_{\in}$, $\Phi$ is not necessarily so.

######  Proof 4.6.

By Lemma 18, we have $\mbox{ $||-\,$}\forall x\forall
y(R(x,y)\to\exists\varpi^{\gimel\Pi}R(x,f[x,\varpi]))$ where $f$ is a
functional symbol defined in ${\mathcal{M}}$. Now, $\Pi$ is countable in
${\mathcal{M}}$, thus $\gimel\Pi$ is equipotent to $\gimel\mathbb{N}$ and
therefore countable by Theorem 34. Therefore, we can define $\Phi(x,y)$ as
“$y=f[x,\varpi]$ for the first $\varpi\,\varepsilon\,\gimel\Pi$ such that
$R(x,f[x,\varpi])$”.

By the results of [Kri18], it follows also that ${\mathcal{N}}\models$
(_$\mathbb{R}$ is not well orderable_).

Note that these results do not use the instruction $\gamma$ and therefore are
valid for any $\gimel 2$.

On the other hand, the following result uses $\gamma$, i.e. the fact that
$\gimel 2$ is finite:

######  Theorem 36.

${\mathcal{N}}\models$ the axiom of well ordered choice (WOC) i.e.: The
product of a family of non void sets indexed by a well ordered set is non
void.

######  Proof 4.7.

This follows immediately from NEPC and the fact that On is isomorphic to a
class of ${\mathcal{N}}$.

######  Remark 37.

In fact, since ${\mathcal{N}}$ satisfies NEPC, it also satisfies the well
ordered principle of choice (WOPC).

Theorem 36 has two interesting consequences:

  1. (1)

There exists a proof-like term $\Theta_{WOC}\mbox{ $||-\,$}{\,}$WOC which
means that we now have a program for the axiom WOC, which is a $\lambda$-term
with the instructions $\gamma,\kappa,\mbox{\rm e}$.

  2. (2)

This gives a new proof that AC (and even _“ $\,\mathbb{R}$ is well
orderable”_) is not a consequence of ZF +WOC [Jec73].

##  5\. The algebra $\mathfrak{A}_{1}$ and a program for AC (and others)

######  Lemma 38.

Let $R(x,y)$ be a formula of ZFε such that $R(a_{0}x,a_{1}y)$ defines, in
${\mathcal{N}}$, a functional from ${\mathcal{M}}_{a_{0}}$ into
${\mathcal{M}}_{a_{1}}$ or from ${\mathcal{M}}_{a_{1}}$ into
${\mathcal{M}}_{a_{0}}$. Then, this functional has a countable image.

Remember that ${\mathcal{M}}_{a_{i}}(i=0,1)$ is the class defined by
$a_{i}x=x$.

######  Proof 5.1.

Suppose, for instance, that $R(x,y)$ defines a functional from
${\mathcal{M}}_{a_{0}}$ into ${\mathcal{M}}_{a_{1}}$ i.e.:

${\mathcal{N}}\models\forall x\forall y\forall
y^{\prime}(R(a_{0}x,a_{1}y),R(a_{0}x,a_{1}y^{\prime})\to
a_{1}y=a_{1}y^{\prime})$.

Applying Lemma 18 to the formula $\neg R(a_{0}x,a_{1}y)$, we obtain:

$\mbox{I}\,\mbox{ $||-\,$}\forall\varpi^{\gimel\Pi}\neg
R(a_{0}x,a_{1}f[a_{0}x,\varpi])\to\forall y\neg R(a_{0}x,a_{1}y)$

for some functional $f:{\mathcal{M}}\\!\times\\!\Pi\to{\mathcal{M}}$ _defined
in ${\mathcal{M}}$_.

By Lemma 11, we have $a_{1}f[a_{0}x,\varpi]=a_{1}f[a_{1}a_{0}x,\varpi]$. Since
$a_{1}a_{0}=0$, we get:

$\mbox{I}\,\mbox{ $||-\,$}\forall\varpi^{\gimel\Pi}\neg
R(a_{0}x,a_{1}f[\emptyset,\varpi])\to\forall y\neg R(a_{0}x,a_{1}y)$.

Now $\Pi$ is countable (in ${\mathcal{M}}$), thus $\gimel\Pi$ is equipotent to
$\gimel\mathbb{N}$; therefore $\gimel\Pi$ is countable (in ${\mathcal{N}}$) by
Theorem 34. Hence we have, for some surjection $g$ from $\mathbb{N}$ onto
$\\{f[\emptyset,\varpi]\;;\;\varpi\,\varepsilon\,\gimel\Pi\\}$:

$\mbox{ $||-\,$}\forall n^{\mbox{\footnotesize int}}\neg
R(a_{0}x,a_{1}g(n))\to\forall y\neg R(a_{0}x,a_{1}y)$.

Thus, we have $\mbox{ $||-\,$}\exists y\,R(a_{0}x,a_{1}y)\to\exists
n^{\mbox{\footnotesize int}}R(a_{0}x,a_{1}g(n))$. It follows that $a_{1}g$ is
a surjection from $\mathbb{N}$ onto the image of $R$.

######  Remark 39.

This shows that ${\mathcal{M}}_{a_{0}}$ and ${\mathcal{M}}_{a_{1}}$ cannot be
both well founded: otherwise, their classes of ordinals would be isomorphic,
which is excluded by Lemma 38 and Theorem 21. Much more general results are
given in [Kri18, Kri15].

In order to simplify a little, we suppose that the ground model
${\mathcal{M}}$ satisfy V = L. This is not really necessary: the important
point is the _principle of choice (PC): there is a bijective functional
between ${\mathcal{M}}$ and_ On.

We denote by On${}_{a_{0}}$ the class of ordinals of ${\mathcal{M}}_{a_{0}}$,
which is order isomorphic to the class On of ordinals of
${\mathcal{N}}_{\in}$.

######  Lemma 40.

${\mathcal{N}}\models\exists X\forall x\exists y\\{x=_{\in}y,\langle a_{1}y\in
a_{1}X\rangle\geq a_{1}\\}$.

######  Proof 5.2.

For each $\alpha$ in On${}_{a_{0}}$, we can choose, by WOPC, an element
$W_{\alpha}$ of the class of sets extensionally equivalent to $V_{\alpha}$.
Now, the functional $\alpha\mapsto a_{1}W_{\alpha}$ from On${}_{a_{0}}$ into
${\mathcal{M}}_{a_{1}}$ has a countable image by Lemma 38. It follows that
there exists $\alpha_{0}$ such that $a_{1}W_{\alpha}=a_{1}W_{\alpha_{0}}$ for
an unbounded class $U$ of $\alpha$ in On${}_{a_{0}}$.

Now, we have $\forall x\exists\alpha\\{U(\alpha),x\in W_{\alpha}\\}$ (in any
model of ZF, every set belongs to some $V_{\alpha}$) and therefore $\forall
x\exists y\exists\alpha\\{U(\alpha),x=_{\in}y,y\,\varepsilon\,W_{\alpha}\\}$.
By Lemma 16, it follows that:

$\forall x\exists y\exists\alpha\\{U(\alpha),x=_{\in}y,\langle
y\in\mbox{Cl}[W_{\alpha}]\rangle=1\\}$. But, by Lemma 11, we have:

$a_{1}=a_{1}\langle y\in\mbox{Cl}[W_{\alpha}]\rangle=a_{1}\langle a_{1}y\in
a_{1}\mbox{Cl}[a_{1}W_{\alpha}]\rangle$ and, by $U(\alpha)$,
$a_{1}W_{\alpha}=a_{1}W_{\alpha_{0}}$.

Therefore, we have $\forall x\exists
y\exists\alpha\\{U(\alpha),x=_{\in}y,a_{1}\langle a_{1}y\in
a_{1}\mbox{Cl}[a_{1}W_{\alpha_{0}}]\rangle=a_{1}\\}$.

Hence the result, with $X=\mbox{Cl}[a_{1}W_{\alpha_{0}}]$.

######  Theorem 41.

There exists a generic extension ${\mathcal{N}}_{\in}[G]$ of
${\mathcal{N}}_{\in}$ which satisfies AC.

######  Proof 5.3.

Let $Y=\\{a_{1}y\;;\;\langle a_{1}y\in a_{1}X\rangle\geq a_{1}\\}$: such a set
exists in ${\mathcal{N}}$ by Lemma 17.

By Lemma 40, $(a_{0}x,a_{1}y)\mapsto a_{0}x\sqcup a_{1}y$ is a surjective
functional from ${\mathcal{M}}_{a_{0}}\\!\times\\!Y$ onto the whole model
${\mathcal{N}}_{\in}$ of ZF.

Since ${\mathcal{M}}_{a_{0}}\models$ V = L, there exists a surjective
functional $\Psi:\mbox{On}\\!\times\\!Y\to{\mathcal{N}}_{\in}$ and therefore
${\mathcal{N}}_{\in}$ is the union of the $Z_{\alpha}$ with $\alpha$ in On,
where $Z_{\alpha}$ is the image by $\Psi$ of $\\{\alpha\\}\\!\times\\!Y$.

Let us consider, for each ordinal $\alpha$ of ${\mathcal{N}}_{\in}$, the
equivalence relation $\simeq_{\alpha}$ on $Y$ defined by
$y\simeq_{\alpha}y^{\prime}\Leftrightarrow\Psi(\alpha,y)=_{\in}\Psi(\alpha,y^{\prime})$.
These equivalence relations form a set (included in ${\mathcal{P}}(Y^{2})$).
Thus, there exist an ordinal $\alpha_{0}$ and for all $\beta$, a surjection
$S_{\beta}:Z\to Z_{\beta}$ with $Z=\bigcup_{\alpha<\alpha_{0}}Z_{\alpha}$.

Finally, using NEPC (non extensional principle of choice) we get a surjective
functional from $\mbox{On}\\!\times\\!Z$ onto ${\mathcal{N}}_{\in}$ (note
that, by definition, $Z$ is a set of ${\mathcal{N}_{\in}}$).

Let us now make $Z$ countable (or even only well ordered) by means of a
generic $G$ on ${\mathcal{N}}_{\in}$; then ${\mathcal{N}}_{\in}[G]\models$ AC.

In the following, we take for $(C,\leq)$ the set of conditions of
${\mathcal{N}}_{\in}$ given by Theorem 41. Applying the constructions of
Section 3, we obtain a r.a. $\mathfrak{A}_{1}$ and a generic model
${\mathcal{N}}_{\in}[G]$ which satisfies AC by Theorem 41. Therefore, we have
${\mathcal{N}}_{\in}\models(\mathbf{1}\raisebox{-0.86108pt}{\small$\;\Vdash\,$}\mbox{AC})$.

######  Remark 42.

The formula $\mathfrak{C}(u)$ which defines the forcing must specify that, if
$\gimel 2$ is the 2-elements Boolean algebra, the set of forcing conditions is
trivial (for instance a singleton). Indeed, in this case,
${\mathcal{N}}={\mathcal{M}}_{\mathcal{D}}$ is well ordered, therefore
${\mathcal{N}}_{\in}\models$ AC, and there is no need to extend it.

It follows that $\mbox{
$||-\,$}(\mathbf{1}\raisebox{-0.86108pt}{\small$\;\Vdash\,$}\mbox{AC})$ and
finally  $\||-\,$AC by Theorem 26. Hence the:

######  Theorem 43.

There exists a proof-like term $\Theta\\!_{AC}$ of the r.a. $\mathfrak{A}_{0}$
such that $(\Theta\\!_{AC},\mathbf{1})\mbox{ $\||-\,$}\mbox{AC}$.

More generally by Theorem 27, it follows that for each axiom $A$ of ZFC, there
exists a proof-like term $\Theta\\!_{A}$ of the r.a. $\mathfrak{A}_{0}$ such
that $(\Theta\\!_{A},\mathbf{1})\mbox{ $\||-\,$}A$. Note that $\Theta\\!_{AC}$
is the only one which contains the instructions $\gamma,\kappa,\mbox{\rm e}$.

### Example of computation with $\Theta\\!_{AC}\Theta\\!_{AC}$

Consider a function $f:\mathbb{N}\to 2$ such that we have a proof of $\exists
n^{\mbox{\footnotesize int}}(f[n]=0)$ in the theory ZF + AC + ${\mathcal{E}}$
where ${\mathcal{E}}$ is a set of axioms of the form:

$(\forall\vec{x}\in\mathbb{N}^{k})(t_{0}[\vec{x}]=u_{0}[\vec{x}],\ldots,t_{n-1}[\vec{x}]=u_{n-1}[\vec{x}]\to
t[\vec{x}]=u[\vec{x}])$
(cf. Section 4, _Computing with the instruction $\gamma$_).

We denote by ${\mathcal{E}}_{\in}$ the conjunction of the corresponding set,
written in the language of ${\mathcal{N}}_{\in}$:

$(\forall\vec{x}\in\mathbb{N}^{k})(t_{0}[\vec{x}]=_{\in}u_{0}[\vec{x}],\ldots,t_{n-1}[\vec{x}]=_{\in}u_{n-1}[\vec{x}]\to
t[\vec{x}]=_{\in}u[\vec{x}])$.

This proof gives a term $\Phi$ written with the only combinators
$\mbox{B},\mbox{C},\mbox{I},\mbox{K},\mbox{W},\mbox{\sf cc}$ such that:

$\vdash\Phi:\mbox{ZFC}_{0},{\mathcal{E}}_{\in}\to(\exists
n\in\mathbb{N})(f[n]=_{\in}0)$
for some finite conjunction ZFC0 of axioms of ZFC.

Therefore, by theorems 2, 27 and 43, we have in the r.a. $\mathfrak{A}_{1}$:

$(\Phi^{*}\Theta_{ZFC_{0}},\mathbf{1})\mbox{
$\||-\,$}({\mathcal{E}}_{\in}\to(\exists n\in\mathbb{N})(f[n]=_{\in}0))$
(remember that if $t\in\Lambda$, we obtain $t^{*}$ replacing
$\mbox{C},\mbox{K},\mbox{W},\mbox{\sf cc}$ by
$\mbox{C}^{*},\mbox{K}^{*},\mbox{W}^{*},\mbox{\sf cc}^{*}$).

By Theorem 26 applied with $F\equiv{\mathcal{E}}_{\in}\to(\exists
n\in\mathbb{N})(f[n]=_{\in}0)$, it follows that:

$(\chi^{\prime}_{F})(\Phi^{*})\Theta_{ZFC_{0}}\mbox{
$||-\,$}\big{(}\mathbf{1}\raisebox{-0.86108pt}{\small$\;\Vdash\,$}({\mathcal{E}}_{\in}\to(\exists
n\in\mathbb{N})(f[n]=_{\in}0))\big{)}$.

Since $\;\Vdash\,$ is a forcing on ${\mathcal{N}}_{\in}$, and $F$ is
arithmetical, we have:

ZFε
$\vdash\big{(}\mathbf{1}\raisebox{-0.86108pt}{\small$\;\Vdash\,$}({\mathcal{E}}_{\in}\to(\exists
n\in\mathbb{N})(f[n]=_{\in}0))\big{)}\to\big{(}{\mathcal{E}}\to\exists
n^{\mbox{\footnotesize int}}(f[n]=0)\big{)}$.

Hence, there is a proof-like term $\Xi$ in the r.a. $\mathfrak{A}_{0}$ such
that:

$(\Xi)(\chi^{\prime}_{F})(\Phi^{*})\Theta_{ZFC_{0}}\mbox{
$||-\,$}{\mathcal{E}}\to\exists n^{\mbox{\footnotesize int}}(f[n]=0)$.

Now we can apply the algorithm of Section 4, _Computing with the instruction
$\gamma$_.

### Programs for other axioms

Consider an axiom $A$ that we can prove consistent with ZFC by forcing. Let
$C_{0}$ be the set of conditions given by Theorem 41 and take for $(C,\leq)$
the set of conditions which gives the iterated forcing for $A$ over $C_{0}$.
Applying the constructions of Section 3, we obtain a r.a. $\mathfrak{A}_{1}$
and a generic model ${\mathcal{N}}_{\in}[G]$ which satisfies $A$. It follows
that $\mbox{ $||-\,$}(\mathbf{1}\raisebox{-0.86108pt}{\small$\;\Vdash\,$}A)$
and finally $\mbox{ $\||-\,$}A$ by Theorem 26. Hence:

######  Theorem 44.

For every formula $A$ of the language of ZF which can be proved consistent
with ZFC by forcing, there exists a proof-like term $\Theta_{A}$ of the r.a.
$\mathfrak{A}_{0}$ such that $(\Theta_{A},\mathbf{1})\mbox{ $\||-\,$}F$.

Then we can use $\Theta_{A}$ in computations as explained above.

######  Remark 45.

In the introdution, I said we consider the problem of turning proofs in ZFC
into programs. But we must be more precise because this may seem rather easy
by means of classical realizability; indeed, here is an algorithm to transform
a proof in ZFC of an arithmetical formula $A$ into a program: first, transform
it into a proof of ZF $\vdash A$ by restricting its quantifiers to L or HOD.
Then, get a program from this new proof using c.r.

The problem solved in the present article is more difficult and is much more
interesting from the point of view of computer science: consider the program P
obtained from a proof of ZF $\vdash(AC\to A$) and, _forgetting this proof_ ,
transform directly the program P. This is more difficult because the program P
contains much less information than the proof which gave it. In fact, the
interesting point is that this is possible.

You may compare with the problem of modifying a program, knowing its source
code or only its compiled code. It is well known that the first situation is
(very) much easier.

## References

  * [BBC98] S. Berardi, M. Bezem, and T. Coquand.  On the computational content of the axiom of choice.  J. Symb. Logic, 63(2):600–622, 1998.
  * [BO05] U. Berger and P. Oliva.  Modified bar recursion and classical dependent choice.  In Proc. Logic Colloquium ’01, pages 89–107. A K Peters, 2005.
  * [CF58] H.B. Curry and R. Feys.  Combinatory Logic.  North-Holland, 1958.
  * [FG20] L. Fontanella and G. Geoffroy.  Preserving cardinals and weak forms of Zorn’s lemma in realizability models.  Math. Struct. in Comp. Sc., 30:976–996, 2020.
  * [Geo18] G. Geoffroy.  Classical realizability as a classifier for nondeterminism.  In Proc. LICS ’18, pages 462–471, 2018.
  * [Gri90] T. Griffin.  A formulæ-as-type notion of control.  In Conf. record 17th A.C.M. Symp. on Principles of Progr. Languages, POPL ’90, pages 47–57, 1990.
  * [How80] W. Howard.  The formulas–as–types notion of construction.  In Essays on combinatory logic, $\lambda$-calculus and formalism, J.P. Seldin and J.R. Hindley ed., pages 479–490. Acad. Press, 1980.
  * [Jec73] T.J. Jech.  The axiom of choice.  North Holland, 1973.
  * [Jec06] T.J. Jech.  Set theory.  Springer, 2006.
  * [Kar19] A. Karagila.  Realizing realizability results with classical constructions.  Bull. Symb. Log., 25:429–445, 2019.
  * [Kre51] G. Kreisel.  On the interpretation of non-finitist proofs I.  J. Symb. Log., 16(4):241–267, 1951.
  * [Kre52] G. Kreisel.  On the interpretation of non-finitist proofs II.  J. Symb. Log., 17(1):43–58, 1952.
  * [Kri09] J.-L. Krivine.  Realizability in classical logic.  In Panoramas et synthèses, Société Mathématique de France, volume 27, pages 197–229, 2009.
  * [Kri12] J.-L. Krivine.  Realizability algebras II: new models of ZF + DC.  Log. Methods Comp. Sc., 8(1:10):1–28, 2012.
  * [Kri15] J.-L. Krivine.  On the structure of classical realizability models of ZF.  In Proc. TYPES ’14 - LIPIcs, volume 39, pages 146–161, 2015.
  * [Kri16] J.-L. Krivine.  Bar recursion in classical realizability: dependent choice and continuum hypothesis.  In Proc. CSL ’16, LIPIcs, volume 62, pages 25:1–25:11, 2016.
  * [Kri18] J.-L. Krivine.  Realizability algebras III: some examples.  Math. Struct. in Comp. Sc., 28(1):45–76, 2018.
  * [Kun92] K. Kunen.  Set theory. An introduction to independence proofs.  North Holland, 1992.
  * [Miq11] A. Miquel.  Forcing as a program transformation.  In Proc. LICS ’11, pages 197–206, 2011.
  * [Spe62] C. Spector.  Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics.  In Recursive function theory: Proc. Symp. in pure math. vol. 5, Amer. Math. Soc., pages 1–27, 1962.
  * [Str17] T. Streicher.  A classical realizability model arising from a stable model of untyped $\lambda$-calculus.  Log. Methods Comp. Sc., 13(4), 2017.