# Classical realizability and arithmetical formulæ

Mauricio Guillermo, Étienne Miquey

► To cite this version:

Mauricio Guillermo, Étienne Miquey. Classical realizability and arithmetical formulæ. Mathematical Structures in Computer Science, 2016, 10.1017/S0960129515000559. hal-01247989

HAL Id: hal-01247989

https://inria.hal.science/hal-01247989

Submitted on 30 Mar 2016

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
CLASSICAL REALIZABILITY AND ARITHMETICAL FORMULÆ

MAURICIO GUILLERMO AND ÉTIENNE MIQUEY

ABSTRACT. In this paper we treat the specification problem in Krivine classical realizabil-
ity (Krivine 2009), in the case of arithmetical formulæ. In the continuity of previous works
from Miquel and the first author (Guillermo 2008; Guillermo and Miquel 2011), we char-
acterize the universal realizers of a formula as being the winning strategies for a game
(defined according to the formula). In the first section we recall the definition of classical
realizability, as well as a few technical results. In Section 5, we introduce in more details
the specification problem and the intuition of the game-theoretic point of view we adopt
later. We first present a game $\mathbb{G}^1$, that we prove to be adequate and complete if the language
contains no instructions ‘quote’ (Krivine 2003), using interaction constants to do substi-
tution over execution threads. We then show that as soon as the language contain ‘quote’,
the game is no more complete, and present a second game $\mathbb{G}^2$ that is both adequate and
complete in the general case. In the last Section, we draw attention to a model-theoretic
point of view and use our specification result to show that arithmetical formulæ are abso-
lute for realizability models.

1. INTRODUCTION

The so called *Curry-Howard correspondence* constituted an important breakthrough in
proof theory, by evidencing a strong connection between the notions of functional pro-
gramming and proof theory (Curry and Feys 1958; Howard 1969; Girard, Lafont, and Tay-
lor 1989). For a long time, this correspondence has been limited to intuitionistic proofs and
constructive mathematics, so that classical reasonings, that are omnipresent in mathemat-
ics, could only be retrieved through negative translations to intuitionistic logic (Friedman
1978) or to linear logic (Girard 2006).

In 1990, Griffin discovered that the control operator *call/cc* (for *call with current continuation*) of the Scheme programming language could be typed by Peirce's law ((*A* → *B*) → *A*) → *A*), this way extending the formuæ-as-types interpretation (Howard 1969).
As Peirce's law is known to imply, in an intuitionistic framework, all the other forms of
classical reasoning (excluded middle, *reductio ad absurdum*, double negation elimination,
etc.), this discovery opened the way for a direct computational interpretation of classical
proofs, using control operators and their ability to *backtrack*. Several calculi were born
from this idea, such as Parigot's *λμ*-calculus (Parigot 1997), Barbanera and Berardi's sym-
metric *λ*-calculus (Barbanera and Berardi 1996), Krivine's *λ<sub>c</sub>*-calculus (Krivine 2009) or
Curien and Herbelin's *λμ̄*-calculus (Curien and Herbelin 2000).

Nonetheless, some difficulties quickly appeared in the analysis of the computational be-
haviour of programs extracted from classical proofs. One reason for these difficulties was
precisely the presence of control operators, whose ability to backtrack breaks the linear-
ity of the execution of programs. More importantly, the formulæ-as-types interpretation
suffered from the lack of a theory connecting the point of view of typing with the point
of view of computation. Realizability was designed by Kleene to interpret the computa-
tional contents of the proofs of Heyting arithmetic (Kleene 1945), and even if it has been
extended later to more general frameworks (like intuitionistic set theories (Myhill 1973;
Friedman 1973; McCarty 1984)), it is intrinsically incompatible with classical reasoning:
the negation of the middle excluded principle is realizable.
1.1. **Classical realizability.** To address this problem, Krivine introduced in the middle of the 90s the theory of *classical realizability* (Krivine 2009), which is a complete reformulation of the very principles of realizability to make them compatible with classical reasoning. (As noticed in several articles (Oliva and Streicher 2008; Miquel 2010), classical realizability can be seen as a reformulation of Kleene's realizability through Friedman's A-translation (Friedman 1978).) Although it was initially introduced to interpret the proofs of classical second-order arithmetic, the theory of classical realizability can be scaled to more expressive theories such as Zermelo-Fraenkel set theory (Krivine 2001) or the calculus of constructions with universes Miquel 2007.

As in intuitionistic realizability, every formula $A$ is interpreted in classical realizability as a set $|A|$ of programs called the *realizers* of $A$, that share a common computational behaviour dictated by the structure of the formula $A$. This point of view is related to the point of view of deduction (and of typing) via the property of *adequacy*, that expresses that any program extracted from a proof of $A$—that is: any program of type $A$—realizes the formula $A$, and thus has the computational behaviour expected from the formula $A$.

However the difference between intuitionistic and classical realizability is that in the latter, the set of realizers of $A$ is defined indirectly, that is from a set $||A||$ of execution contexts (represented as argument stacks) that are intended to challenge the truth of $A$. Intuitively, the set $||A||$—which we shall call the *falsity value of A*—can be understood as the set of all possible counter-arguments to the formula $A$. In this framework, a program realizes the formula $A$—i.e. belongs to the *truth value* $|A|$—if and only if it is able to defeat all the attempts to refute $A$ using a stack in $||A||$. (The definition of the classical notion of a realizer is also parameterized by a *pole* representing a particular challenge, that we shall define and discuss in Section 4.1.1.)

By giving an equal importance to programs—or terms—that ‘defend’ the formula $A$, and to execution contexts—or stacks—that ‘attack’ the formula $A$, the theory of classical realizability is therefore able to describe the interpretation of classical reasoning in terms of manipulation of whole stacks (as first class citizens) using control operators.

1.2. **Krivine $\lambda_c$-calculus.** The programming language commonly used in classical realizability is Krivine's $\lambda_c$-calculus, which is an extension of Church's $\lambda$-calculus (Church 1941) containing an instruction $\mathcal{C}$ (representing the control operator `call/cc`) and continuation constants embedding stacks. Unlike the traditional $\lambda$-calculus, the $\lambda_c$-calculus is parameterized by a particular execution strategy —corresponding to the Krivine Abstract Machine (Krivine 2004)— so that the notion of confluence—which is central in traditional $\lambda$-calculi, does not make sense anymore. The property of confluence is replaced by the property of determinism, which is closer from the point of view of real programming languages.

A pleasant feature of this calculus is that it can be enriched with *ad hoc* extra instructions. For instance, a `print` instruction might be added to trace an execution, as well as extra instructions manipulating primitive numerals to do some code optimization (Miquel 2010). In some situations, extra instructions can also be designed to realize reasoning principles, the standard example being the instruction `quote` that computes the Gödel code of a stack, used for instance to realize the axiom of dependent choice (Krivine 2003). In this paper, we shall consider this instruction together with `eq`, that tests the syntactic equality between two $\lambda_c$-terms.

1.3. **The specification problem.** A central problem in classical realizability is the *specification problem*, which is to find a characterization for the (universal) realizers of a formula by their computational behaviour. In intuitionistic logic, this characterization does not contain more information than the formula itself, so that this problem has been given little attention. For instance, the realizers of an existential formula $\exists^N x A(x)$ are exactly the ones reducing to a pair made of a witness $n \in \mathbb{N}$ and a proof term realizing $A(n)$ (Krivine 1993).
However, in classical realizability the situation appears to be quite different and the desired characterization is in general much more difficult to obtain. Indeed, owing to the presence of control operators in the language of terms, the realizers have the ability to backtrack at any time, making the execution harder to predict. Considering for instance the very same formula $∃$<sup>N</sup>xA(x), a classical realizer of it can give as many integers for x as it wants, using backtrack to make another try. Hence we can not expect from such a realizer to reduct directly to a witness (for an account of witness extraction techniques in classical realizability, see Miquel's article (Miquel 2010)). In addition, as we will see in Section 5.3, giving such a witness might be computationally impossible without backtrack, for example in the case of a formula relying on the Halting Problem. We will treat this particular example in Section 5.3.

Furthermore, as stated in the article on Peirce's Law (Guillermo and Miquel 2011), the presence of instructions such as *quote* (defined in Section 2.3) makes the problem still more subtle. We will deal with this particular case in Section 7.

## 1.4. Specifying arithmetical formulæ.
The architecture of classical realizability is centered around the opposition between falsity values (stacks) and truth values (terms). This opposition, as well as the underlying intuition (opponents vs. defenders), naturally leads us to consider the problem in a game-theoretic setting. Such a setting—namely realizability games— was defined by Krivine as a mean to prove that any arithmetical formula which is *universally realized* (i.e.: realized for all poles) is true in the ground model (often considered as the *standard full model of second order arithmetics*) (c.f.: theorem 16 of (Krivine 2003)). Thereafter, Krivine also proves the converse, which is that every arithmetical formula which is true in the ground model is realized by the term which implements the trivial winning strategy of the game associated to the formula (c.f.: theorem 21 of (Krivine 2009)). Those realizability games are largely inspired on the *non-counterexample interpretation* of Kreisel (Kreisel 1951), Kreisel 1952 and the subsequent developpement of game semantics for proofs by Coquand (Coquand 1995).

Our goal is to establish an operational description which characterize *all* the realizers of a given arithmetical formula. In particular, it does not suffice to find a realizer for any true arithmetical formula, but we want to explicit an operational sufficient condition to be a realizer.

In Coquand's games, the only atomic formulæ are $>$ and $\le$, therefore a strategy for a true atomic formula does nothing, as the game is already won by the defender. As a consequence, any "blind" enumeration of $\mathbb{N}^k$ is a winning strategy for every true $\Sigma_{2k}^0$-formulæ. Such a strategy, which is central in Krivine's proof that any true formula in the ground model is realized (Krivine 2009, Theorem 21), has no interesting computational content. Worse, it is not suitable for being a realizer in the general case where we use Leibniz equality. This remark will be discussed more consistently in Section 8.

The game developed by Krivine makes both players to use only constants. If the calcu-
lus does not contain instructions incompatible with substitution (like 'quote'), this game
is equivalent to the one we prove that specifies the arithmetical formulæ in the substitutive
case. However, Krivine's realizers are eventually intended to contain 'quote'. In this gen-
eral case, we prove that the specification is obtained from the first game by a relaxation of
the rules of $∃$.

Thus, both works left open the question of giving a precise specification for arithmetic
formulæ in the general case.

In this paper, we will restrict ourself to the setting where arithmetical formulæ have
been relativized to *canonical integers*, as we explained in Section 4.7. We will rephrase
the game-theoretic framework of the first author Ph.D. thesis (Guillermo 2008), to provide
a game-theoretic characterization $G^1$ that is both complete and adequate, in the particular
case where the underlying calculus contains infinitely many *interaction constants*. However, this hypothesis—that is crucial in our proof of completeness—is known to be incompatible with the presence of instructions such as *quote* or *eq* (Guillermo and Miquel 2011), which allow us to distinguish syntactically $\lambda_c$ terms that are computationally equivalent. We exhibit in Section 6.3 a *wild realizer* that uses these instructions and does not suit as a winning strategy for $\mathcal{G}^1$, proving that $\mathcal{G}^1$ is no more complete in this case.

Indeed, as highlighted in the article on Peirce's Law (Guillermo and Miquel 2011), the presence of such instructions introduces a new—and purely game-theoretic—form of backtrack that does not come from a control operator but from the fact that realizers, using a syntactic equality test provided by *quote*, can check whether a position has already appeared before. We present in Section 7 a second game $\mathcal{G}^2$ that allows this new form of backtrack, and captures the behaviour of our wild realizer. Then we prove that without any assumption on the set of instructions, this game is both adequate and complete, thus constituting the definitive specification of arithmetical formulæ.

## 1.5. Connexion with forcing.
In addition to the question of knowing how to specify arithmetical formulæ, this paper presents an answer to another question, which is to know whether arithmetical formulæ are *absolute* for realizability models. In set theory, a common technique to prove independence results in theory is to use forcing, that allows us to extend a model and add some specific properties to it. Yet, it is known $\Sigma_2^1$-formulæ are absolute for a large class of models, including those produced by forcing. This constitutes somehow a barrier to forcing, which does not permit to change the truth of formulæ that are below $\Sigma_1^1$ in the arithmetical hierarchy.

If classical realizability was initially designed to be a semantics for proofs of Peano second-order arithmetic, it appeared then to be scalable to build models for high-order arithmetic (Miquel 2011) or set theory Krivine 2011. Just like forcing techniques, these constructions rest upon a ground model and allow us to break some formulæ that were true in the ground model, say the continuum hypothesis or the axiom of choice (Krivine 2012). In addition, the absoluteness theorem of $\Sigma_1^2$ does not apply to realizability model. Hence it seems quite natural to wonder, as for forcing, whether realizability models preserve some formulæ. We will explain in Section 8 how the specification results allow us to show that arithmetical formulæ are absolute for realizability models.

## 2. THE LANGUAGE $\lambda_c$

A lot of the notions we use in this paper are the very same as in the article on Peirce's Law (Guillermo and Miquel 2011). We will recall them briefly, for a more gentle introduction, we advise the reader to refer to this paper.

### 2.1. Terms and stacks.
The $\lambda_c$-calculus distinguishes two kinds of syntactic expressions: *terms*, which represent programs, and *stacks*, which represent evaluation contexts. Formally, terms and stacks of the $\lambda_c$-calculus are defined (see Fig. 1) from three auxiliary sets of symbols, that are pairwise disjoint:

* A denumerable set $V_\lambda$ of $\lambda$-variables (notation: $x, y, z$, etc.)

* A countable set $C$ of instructions, which contains at least an instruction $\mathcal{O}$ ('call/cc', for: *call with current continuation*).

* A nonempty countable set $B$ of stack constants, also called stack bottoms (notation: $\alpha, \beta, \gamma$, etc.)

In what follows, we adopt the same writing conventions as in the pure $\lambda$-calculus, by considering that application is left-associative and has higher precedence than abstraction. We also allow several abstractions to be regrouped under a single $\lambda$, so that the closed term $\lambda x. \lambda y. \lambda z. ((zx)y)$ can be more simply written $\lambdaxyz. zxy$.

As usual, terms and stacks are considered up to $\alpha$-conversion (Barendregt 1984) and we denote by $t\{x := u\}$ the term obtained by replacing every free occurrence of the variable $x$
<figure><img src="image_2.png" /><figcaption>FIGURE 1. Definitions</figcaption></figure>

by the term $u$ in the term $t$, possibly renaming the bound variables of $t$ to prevent name clashes. The sets of all closed terms and of all (closed) stacks are respectively denoted by $\Lambda$ and $\Pi$.

**Definition 1** (Proof-like terms). – We say that a $\lambda_c$-term $t$ is *proof-like* if $t$ contains no continuation constant $k_\pi$. We denote by PL the set of all proof-like terms.

Finally, every natural number $n \in \mathbb{N}$ is represented in the $\lambda_c$-calculus as the closed proof-like term $\bar{n}$ defined by

$$ \bar{n} \equiv \bar{s}^n \bar{0} \equiv \bar{s}(\cdots(\bar{s}\bar{0})\cdots), $$

where $\bar{0} \equiv \lambda x f . x$ and $\bar{s} \equiv \lambda n x f . f(n x f)$ are Church's encodings of zero and the successor function in the pure $\lambda$-calculus. Note that this encoding slightly differs from the traditional encoding of numerals in the $\lambda$-calculus, although the term $\bar{n} \equiv \bar{s}^n \bar{0}$ is clearly $\beta$-convertible to Church's encoding $\lambda x f . f^n x$—and thus computationally equivalent. The reason for preferring this modified encoding is that it is better suited to the call-by-name discipline of Krivine's Abstract Machine (KAM) we will now present.
## 2.2. Krivine's Abstract Machine.
In the $\lambda_c$-calculus, computation occurs through the interaction between a closed term and a stack within Krivine's Abstract Machine (KAM). Formally, we call a *process* any pair $t \star \pi$ formed by a closed term $t$ and a stack $\pi$. The set of all processes is written $\Lambda \star \Pi$ (which is just another notation for the Cartesian product of $\Lambda$ by $\Pi$).

**Definition 2 (Relation of evaluation).** We call a relation of *one step evaluation* any binary relation $>_{1}$ over the set $\Lambda \star \Pi$ of processes that fulfils the following four axioms:

<table><tr><td>(PUSH)</td><td>tu ★ π &gt;<sub>1</sub></td><td>t ★ u · π</td></tr><tr><td>(GRAB)</td><td>(λx.t) ★ u · π &gt;<sub>1</sub></td><td>t{x := u} ★ π</td></tr><tr><td>(SAVE)</td><td>cc ★ t · π &gt;<sub>1</sub></td><td>t ★ k<sub>π</sub> · π</td></tr><tr><td>(RESTORE)</td><td>k<sub>π</sub> ★ t · π' &gt;<sub>1</sub></td><td>t ★ π</td></tr></table>

The reflexive-transitive closure of $>_{1}$ is written $>$.

One of the specificities of the $\lambda_c$-calculus is that it comes with a binary relation of (one step) evaluation $>_{1}$ that is not *defined*, but *axiomatized* via the rules (PUSH), (GRAB), (SAVE) and (RESTORE). In practice, the binary relation $>_{1}$ is simply another parameter of the definition of the calculus, just like the sets $C$ and $\mathcal{B}$. Strictly speaking, the $\lambda_c$-calculus is not a particular extension of the $\lambda$-calculus, but a family of extensions of the $\lambda$-calculus parameterized by the sets $\mathcal{B}$, $C$ and the relation of one step evaluation $>_{1}$. (The set $\mathcal{V}_{\lambda}$ of $\lambda$-variables—that is interchangeable with any other denumerable set of symbols—does not really constitute a parameter of the calculus.)

## 2.3. Adding new instructions.
The main interest of keeping open the definition of the sets $\mathcal{B}$, $C$ and of the relation evaluation $>_{1}$ (by axiomatizing rather than defining them) is that it makes possible to enrich the calculus with extra instructions and evaluation rules, simply by putting additional axioms about $C$, $\mathcal{B}$ and $>_{1}$. On the other hand, the definitions of classical realizability (Krivine 2009) as well as its main properties do not depend on the particular choice of $\mathcal{B}$, $C$ and $>_{1}$, although the fine structure of the corresponding realizability models is of course affected by the presence of additional instructions and evaluation rules.

For the needs of the discussion in Section 6, we shall sometimes consider the following extra instructions in the set $C$:

* The instruction *quote*, which comes with the evaluation rule

$$ (\text{QUOTE}) \qquad \text{quote} \star t \cdot \pi >_1 t \star \bar{n}_{\pi} \cdot \pi, $$

where $\pi \mapsto n_{\pi}$ is a recursive injection from $\Pi$ to $\mathbb{N}$. Intuitively, the instruction *quote* computes the ‘code’ $n_{\pi}$ of the stack $\pi$, and passes it (using the encoding $n \mapsto \bar{n}$ described in Section 2.1) to the term $t$. This instruction was originally introduced to realize the axiom of dependent choices (Krivine 2003).

* The instruction *eq*, which comes with the evaluation rule

$$ (\text{EQ}) \qquad \begin{array}{l} \text{eq} \star t_1 \cdot t_2 \cdot u \cdot v \cdot \pi >_1 \left\{ \begin{array}{ll} u \star \pi & \text{if } t_1 \equiv t_2 \\ v \star \pi & \text{if } t_1 \not\equiv t_2 \end{array} \right. \\ \text{eq-nat} \end{array} $$

Intuitively, the instruction *eq* tests the syntactic equality of its first two arguments $t_1$ and $t_2$ (up to $\alpha$-conversion), giving the control to the next argument $u$ if the test succeeds, and to the second next argument $v$ otherwise. In presence of the *quote* instruction, it is possible to implement a closed $\lambda_c$-term *eq'* that has the very same computational behaviour as *eq*, by letting

$$ \text{eq}' \equiv \lambda x_1 x_2 . \text{quote} (\lambda n_1 y_1 . \text{quote} (\lambda n_2 y_2 . \text{eq-nat} n_1 n_2) x_2) x_1, $$

where *eq_nat* is any closed $\lambda$-term that tests the equality between two numerals (using the encoding $n \mapsto \bar{n}$).
* The instruction $\hat{\mathfrak{h}}$ ('fork'), which comes with the two evaluation rules

$$ (\text{FORK}) \qquad \hat{\mathfrak{h}} \star t_0 \cdot t_1 \cdot \pi >_1 t_0 \star \pi \quad \text{and} \quad \hat{\mathfrak{h}} \star t_0 \cdot t_1 \cdot \pi >_1 t_1 \star \pi. $$

Intuitively, the instruction $\hat{\mathfrak{h}}$ behaves as a non deterministic choice operator, that indifferently selects its first or its second argument. The main interest of this instruction is that it makes evaluation non deterministic, in the following sense:

**Definition 3** (Deterministic evaluation). We say that the relation of evaluation $>_{1}$ is *deterministic* when the two conditions $p >_{1} p'$ and $p >_{1} p''$ imply $p' \equiv p''$ (syntactic identity) for all processes $p, p'$ and $p''$. Otherwise, $>_{1}$ is said to be *non deterministic*.

The smallest relation of evaluation, that is defined as the union of the four rules (PUSH), (GRAB), (SAVE) and (RESTORE), is clearly deterministic. The property of determinism still holds if we enrich the calculus with an instruction eq ($\neq \mathfrak{c}$) together with the aforementioned evaluation rules or with the instruction quote ($\neq \mathfrak{c}$).

On the other hand, the presence of an instruction $\hat{\mathfrak{h}}$ with the corresponding evaluation rules definitely makes the relation of evaluation non deterministic.

**2.4. The thread of a process and its anatomy.** Given a process $p$, we call the thread of $p$ and write $\mathbf{th}(p)$ the set of all processes $p'$ such that $p > p'$:

$$ \mathbf{th}(p) = \{p' \in \Lambda \star \Pi : p > p'\}. $$

This set has the structure of a finite or infinite (di)graph whose edges are given by the relation $>_{1}$ of one step evaluation. In the case where the relation of evaluation is deterministic, the graph $\mathbf{th}(p)$ can be either:

* *Finite and cyclic from a certain point*, because the evaluation of $p$ loops at some point. A typical example is the process $\mathbf{I} \star \delta\delta \cdot \alpha$ (where $\mathbf{I} \equiv \lambda x . x$ and $\delta \equiv \lambda x . xx$), that enters into a 2-cycle after one evaluation step:

$$ \mathbf{I} \star \delta\delta \cdot \alpha >_1 \delta\delta \star \alpha >_1 \delta \star \delta \cdot \alpha >_1 \delta\delta \star \alpha >_1 \dots $$

* *Finite and linear*, because the evaluation of $p$ reaches a state where no more rule applies. For example:

$$ \mathbf{II} \star \alpha >_1 \mathbf{I} \star \mathbf{I} \cdot \alpha >_1 \mathbf{I} \star \alpha. $$

* *Infinite and linear*, because $p$ has an infinite execution that never reaches twice the same state. A typical example is given by the process $\delta'\delta' \star \alpha$, where $\delta' \equiv \lambda x . x \mathbf{I}$:

$$ \delta'\delta' \star \alpha >_3 \delta'\delta' \star \mathbf{I} \cdot \alpha >_3 \delta'\delta' \star \mathbf{I} \cdot \mathbf{I} \cdot \alpha >_3 \delta'\delta' \star \mathbf{I} \cdot \mathbf{I} \cdot \mathbf{I} \cdot \alpha >_3 \dots $$

**2.5. Interaction constants.** The two examples of extra instructions quote and eq we gave in Section 2.3 have a strong impact on the potential behaviour of processes. Indeed, they are able to distinguish syntactically different terms that are computationally equivalent, such as the terms $\mathbf{I}$ and $\mathbf{II}$. To better understand the consequence of the presence of such extra instructions in the $\lambda_c$-calculus, we need to introduce the important notion of interaction constant. This definition relies on the notions of substitution over terms and stacks, that are defined in Fig. 1. Unlike the traditional form of substitution $t\{x := u\}$ (which is only defined for terms), the substitutions $t\{c := u\}$ and $\pi\{c := u\}$ also propagate through the continuation constants $k_\pi$.

**Definition 4.** A constant $\kappa \in C$ is said to be

* *inert* if for all $\pi \in \Pi$, there is no process $p$ such that $\kappa \star \pi >_1 p$;

* *substitutive* if for all $u \in \Lambda$ and for all processes $p, p' \in \Lambda \star \Pi$, $p >_1 p'$ implies $p\{\kappa := u\} >_1 p'\{\kappa := u\}$;

* *non generative* if for all processes $p, p' \in \Lambda \star \Pi$, $p >_1 p'$, the constant $\kappa$ cannot occur in $p'$ unless it already occurs in $p$.
A constant $κ ∈ C$ that is inert, substitutive and non generative is then called an *interaction constant*. Similarly, we say that a stack constant $α ∈ B$ is:

* substitutive if for all $π ∈ Π$ and for all processes $p, p' ∈ Λ \star Π, p >_1 p'$ implies $p\{α := π\} >_1 p'\{α := π\}$;

* non generative if for all processes $p, p' ∈ Λ \star Π, p >_1 p'$, the constant $α$ cannot occur in $p'$ unless it already occurs in $p$.

The main observation is that substitutive constants are incompatible with both instruction quote and eq (see (Guillermo and Miquel 2011) for a proof):

**Proposition 1.** If the calculus of realizers contains one of both instructions quote or eq, then none of the constants $κ ∈ C$ is substitutive.

The very same argument can be applied to prove the incompatibility of substitutive stack constants with the instruction *quote*. On the other hand, it is clear that if the relation of evaluation $>_1$ is only defined from the rules (GRAB),(PUSH),(SAVE) and (RESTORE) -and possibly: the rule (FORK)- then all the remaining constants $κ$ in $C$ (i.e. $κ \notin α$, $\emptyset$) are interaction constants (and thus substitutive), whereas all the stack constants in $B$ are substitutive and non generative. Substitutive (term and stack) constants are useful to analyze the computational behaviour of realizers in a uniform way. For instance, if we know that a closed term $t ∈ Λ$ is such that

$$t \star \kappa_1 \cdots \kappa_n \cdot \alpha > p$$

where $κ_1, \dots, κ_n$ are substitutive constants that do not occur in $t$, and where $α$ is a substitutive stack constant that does not occur in $t$ too, then we more generally know that

$$t \star u_1 \cdots u_n \cdot \pi > p\{\kappa_1 := u_1, \dots, \kappa_n := u_n, \alpha := \pi\}$$

for all terms $u_1, \dots, u_n ∈ Λ$ and for all stacks $π ∈ Π$. Intuitively, substitutive constants play in the $λ_c$-calculus the same role as free variables in the pure $λ$-calculus.

### 3. CLASSICAL SECOND-ORDER ARITHMETIC

In Section 2 we delt with the *computing facet* of the theory of classical realizability. In this section, we will now present its *logical facet* by introducing the language of classical second-order logic with the corresponding type system. In section 3.3, we will focus to the particular case of *second-order arithmetic* and present its axioms.

3.1. **The language of second-order logic.** The language of second-order logic distinguishes two kinds of expressions: *first-order expressions* representing individuals, and *formulæ*, representing propositions about individuals and sets of individuals (represented using second-order variables as we shall see below).

3.1.1. *First-order expressions.* First-order expressions are formally defined (see Fig. 1) from the following sets of symbols:

* A *first-order signature* $Σ$ defining *function symbols* with their arities, and considering *constant symbols* as function symbols of arity 0. We assume that the signature $Σ$ contains a constant symbol 0 ('zero'), a unary function symbol $s$ ('successor') as well as a function symbol $f$ for every primitive recursive function (including symbols $+$, $×$, etc.), each of them being given its standard interpretation in $Π$ (see Section 3.3).

* A denumerable set $V_1$ of *first-order variables*. For convenience, we shall still use the lowercase letters $x, y, z$, etc. to denote first-order variables, but these variables should not be confused with the $λ$-variables introduced in Section 2.

The set $FV(e)$ of all (free) variables of a first-order expression $e$ is defined as expected, as well as the corresponding operation of substitution, that we still write $e\{x := e'\}$.
3.1.2. Formulæ. Formulæ of second-order logic are defined (see Fig. 1) from an additional set of symbols $V_2$ of second-order variables (or predicate variables), using the uppercase letters X, Y, Z, etc. to represent such variables:

$$A, B ::= X(e_1, \dots, e_k) \mid A \Rightarrow B \mid \forall x A \mid \forall x A \quad (X \in V_2)$$

We assume that each second-order variable X comes with an arity $k \ge 0$ (that we shall often leave implicit since it can be easily inferred from the context), and that for each arity $k \ge 0$, the subset of $V_2$ formed by all second-order variables of arity $k$ is denumerable.

Intuitively, second-order variables of arity 0 represent (unknown) propositions, unary predicate variables represent predicates over individuals (or sets of individuals) whereas binary predicate variables represent binary relations (or sets of pairs), etc.

The set of free variables of a formula A is written $FV(A)$. (This set may contain both first-order and second-order variables.) As usual, formulæ are identified up to $\alpha$-conversion, neglecting differences in bound variable names. Given a formula A, a first-order variable $x$ and a closed first-order expression $e$, we denote by $A\{x := e\}$ the formula obtained by replacing every free occurrence of $x$ by the first-order expression $e$ in the formula A, possibly renaming some bound variables of A to avoid name clashes.

Lastly, although the formulæ of the language of second-order logic are constructed from atomic formulæ only using implication and first- and second-order universal quantifications, we can define other logical constructions (negation, conjunction disjunction, first- and second-order existential quantification as well as Leibniz equality) using the so called second-order encodings (cf Fig. 1).

3.1.3. *Predicates and second-order substitution.* We call a predicate of arity $k$ any expression of the form $P \equiv \lambda x_1 \cdots x_k C$ where $x_1, \dots, x_k$ are $k$ pairwise distinct first-order variables and where $C$ is an arbitrary formula. (Here, we (ab)use the $\lambda$-notation to indicate which variables $x_1, \dots, x_k$ are abstracted in the formula $C$).

The set of free variables of a $k$-ary predicate $P \equiv \lambda x_1 \cdots x_k C$ is defined by $FV(P) \equiv FV(C) \setminus \{x_1; \dots; x_k\}$, and the application of the predicate $P \equiv \lambda x_1 \cdots x_k C$ to a $k$-tuple of first-order expressions $e_1, \dots, e_k$ is defined by letting

$$P(e_1, \dots, e_k) \equiv (\lambda x_1 \cdots x_k C)(e_1, \dots, e_k) \equiv C\{x_1 := e_1; \dots; x_k := e_k\}$$

(by analogy with $\beta$-reduction). Given a formula A, a $k$-ary predicate variable $X$ and an actual $k$-ary predicate $P$, we finally define the operation of second-order substitution $A\{X := P\}$ as follows:

$$\begin{align*}
X(e_1, \dots, e_k)\{X := P\} &\equiv P(e_1, \dots, e_k) & (Y \not\equiv X) \\
Y(e_1, \dots, e_m)\{X := P\} &\equiv Y(e_1, \dots, e_m) & \\
(A \Rightarrow B)\{X := P\} &\equiv A\{X := P\} \Rightarrow B\{X := P\} & (Y \not\in FV(P)) \\
(\forall x A)\{X := P\} &\equiv \forall x A\{X := P\} & \\
(\forall X A)\{X := P\} &\equiv \forall X A & \\
(\forall Y A)\{X := P\} &\equiv \forall Y A\{X := P\} & (Y \not\equiv X, Y \notin FV(P))
\end{align*}$$

3.2. A type system for classical second-order logic. Through the formulæ-as-types correspondence (Howard 1969; Girard, Lafont, and Taylor 1989), we can see any formula A of second-order logic as a type, namely, as the type of its proofs. We shall thus present the deduction system of classical second-order logic as a type system based on a typing judgement of the form $\Gamma \vdash t : A$, where

* $\Gamma$ is a typing context of the form $\Gamma \equiv x_1 : B_1, \dots, x_n : B_n$, where $x_1, \dots, x_n$ are pairwise distinct $\lambda$-variables and where $B_1, \dots, B_n$ are arbitrary propositions;

* $t$ is a proof-like term, i.e. a $\lambda_c$-term containing no continuation constant $k_\pi$;

* A is a formula of second-order logic.
The type system of classical second-order logic is then defined from the typing rules of Fig. 1. These typing rules are the usual typing rules of AF2 (Krivine 1993), plus a specific typing rule for the instruction `α` which permits to recover the full strength of classical logic.

Using the encodings of second-order logic, we can derive from the typing rules of Fig. 1 the usual introduction and elimination rules of absurdity, conjunction, disjunction, (first- and second-order) existential quantification and Leibniz equality (Krivine 1993). The typing rule for call/cc (law of Peirce) allows us to construct proof-terms for classical reasoning principles such as the excluded middle, *reductio ad absurdum*, de Morgan laws, etc.

**3.3. Classical second-order arithmetic (PA2).** From now on, we consider the particular case of second-order arithmetic (PA2), where first-order expressions are intended to represent natural numbers. For that, we assume that every k-ary function symbol $f \in \Sigma$ comes with an interpretation in the standard model of arithmetic as a function $[[f]] : \mathbb{N}^k \to \mathbb{N}$, so that we can give a denotation $[[e]] \in \mathbb{N}$ to every closed first-order expression $e$. Moreover, we assume that each function symbol associated to a primitive recursive definition (cf Section 3.1.1) is given its standard interpretation in $\mathbb{N}$. In this way, every numeral $n \in \mathbb{N}$ is represented in the world of first-order expressions as the closed expression $s^n(0)$ that we still write $n$, since $[[s^n(0)]] = n$.

**3.3.1. Induction.** Following Dedekind's construction of natural numbers, we consider the predicate Nat($x$) (Girard, Lafont, and Taylor 1989; Krivine 1993) defined by

$$ \mathrm{Nat}(x) \equiv \forall Z(Z(0) \Rightarrow \forall y(Z(y) \Rightarrow Z(s(y))) \Rightarrow Z(x)), $$

that defines the smallest class of individuals containing zero and closed under the successor function. One of the main properties of the logical system presented above is that the axiom of induction, that we can write $\forall x \mathrm{Nat}(x)$, is not derivable from the rules of Fig. 1. As Krivine proved (Krivine 2009, Theorem 12), this axiom is not even (universally) realizable in general. To recover the strength of arithmetic reasoning, we need to relativize all first-order quantifications to the class Nat($x$) of Dedekind numerals using the shorthands for numeric quantifications

$$ \begin{aligned} \forall^{\mathrm{nat}} x A(x) &\equiv \forall x (\mathrm{Nat}(x) \Rightarrow A(x)) \\ \exists^{\mathrm{nat}} x A(x) &\equiv \forall Z (\forall x (\mathrm{Nat}(x) \Rightarrow A(x) \Rightarrow Z) \Rightarrow Z) \end{aligned} $$

so that the *relativized induction axiom* becomes provable in second-order logic (Krivine 1993):

$$ \forall Z(Z(0) \Rightarrow \forall^{\mathrm{nat}} x (Z(x) \Rightarrow Z(s(x)))) \Rightarrow \forall^{\mathrm{nat}} x Z(x)). $$

**3.3.2. The axioms of PA2.** Formally, a formula $A$ is a theorem of second-order arithmetic (PA2) if it can be derived (using the rules of Fig. 1) from the two axioms

* $\forall x \forall y (s(x) = s(y) \Rightarrow x = y)$ (Peano 3rd axiom)

* $\forall x \neg(s(x) = 0)$ (Peano 4th axiom)

expressing that the successor function is injective and not surjective, and from the definitional equalities attached to the (primitive recursive) function symbols of the signature:

* $\forall x (x + 0 = x), \quad \forall x \forall y (x + s(y) = s(x + y))$

* $\forall x (x \times 0 = 0), \quad \forall x \forall y (x \times s(y) = (x \times y) + x)$

* etc.

Unlike the non relativized induction axiom—that requires a special treatment in PA2—we shall see in Section 4.5 that all these axioms are realized by simple proof-like terms.
## 4. CLASSICAL REALIZABILITY SEMANTICS

**4.1. Generalities.** Given a particular instance of the $\lambda_c$-calculus (defined from particular sets $\mathcal{B}, \mathcal{C}$ and from a particular relation of evaluation $>_{1}$ as described in Section 2), we shall now build a classical realizability model in which every closed formula $A$ of the language of PA2 will be interpreted as a set of closed terms $|A| \subseteq \Lambda$, called the *truth value* of $A$, and whose elements will be called the *realizers* of $A$.

**4.1.1. Poles, truth values and falsity values.** Formally, the construction of the realizability model is parameterized by a pole $\perp$ in the sense of the following definition:

**Definition 5 (Poles).** — A pole is any set of processes $\perp \subseteq \Lambda \star \Pi$ which is closed under anti-evaluation, in the sense that both conditions $p > p'$ and $p' \in \perp$ together imply that $p \in \perp$ for all processes $p, p' \in \Lambda \star \Pi$.

We will mainly use one method to define a pole $\perp$. From an arbitrary set of processes $P$, we can define pole as the complement set of the union of all threads starting from an element of $P$, that is:

$$ \perp \equiv \left( \bigcup_{p \in P} \mathbf{th}(p) \right)^c \equiv \bigcap_{p \in P} (\mathbf{th}(p))^c. $$

It is indeed quite easy to check that $\perp$ is closed by anti-reduction, and it is also the largest pole that does not intersect $P$. We shall say that such a definition is *thread-oriented*.

Let us now consider a fixed pole $\perp$. We call a falsity value any set of stacks $S \subseteq \Pi$. Every falsity value $S \subseteq \Pi$ induces a truth value $S^{\perp} \subseteq \Lambda$ that is defined by

$$ S^{\perp} = \{t \in \Lambda : \forall \pi \in S (t \star \pi) \in \perp\}. $$

Intuitively, every falsity value $S \subseteq \Pi$ represents a particular set of tests, while the corresponding truth value $S^{\perp}$ represent the set of all programs that passes all tests in $S$ (w.r.t. the pole $\perp$, that can be seen as the *challenge*). From the definition of $S^{\perp}$, it is clear that the larger the falsity value $S$, the smaller the corresponding truth value $S^{\perp}$, and vice-versa.

**4.1.2. Formulæ with parameters.** In order to interpret second-order variables that occur in a given formula $A$, it is convenient to enrich the language of PA2 with a new predicate symbol $\dot{F}$ of arity $k$ for every falsity value function $F$ of arity $k$, that is, for every function $F : \mathbb{N}^k \to \mathfrak{F}(\Pi)$ that associates a falsity value $F(n_1, \dots, n_k) \subseteq \Pi$ to every $k$-tuple $(n_1, \dots, n_k) \in \mathbb{N}^k$. A formula of the language enriched with the predicate symbols $\dot{F}$ is then called a *formula with parameters*. Formally, this correspond to the formulæ defined by:

$$ A, B ::= X(e_1, \dots, e_k) \mid A \Rightarrow B \mid \forall x A \mid \forall x A \mid \dot{F}(e_1, \dots, e_k) \quad X \in \mathcal{V}_2, F \in \mathfrak{F}(\Pi)^{\mathbb{N}^k} $$

The notions of a *predicate with parameters* and of a *typing context with parameters* are defined similarly. The notations $FV(A)$, $FV(P)$, $FV(\Gamma)$, $\text{dom}(\Gamma)$, $A\{x := e\}$, $A\{X := P\}$, etc. are extended to all formulæ $A$ with parameters, to all predicates $P$ with parameters and to all typing contexts $\Gamma$ with parameters in the obvious way.

**4.2. Definition of the interpretation function.** The interpretation of the closed formulae with parameters is defined as follows:

**Definition 6 (Interpretation of closed formulæ with parameters).** — The falsity value $||A|| \subseteq \Pi$ of a closed formula $A$ with parameters is defined by induction on the number
of connectives/quantifiers in A from the equations

$$
\begin{align*}
\|\dot{F}(e_1, \dots, e_k)\| &= F(\llbracket e_1 \rrbracket, \dots, \llbracket e_k \rrbracket) \\
\|A \Rightarrow B\| &= |A| \cdot \|B\| = \{t \cdot \pi : t \in |A|, \pi \in \|B\|\} \\
\|\forall x A\| &= \bigcup_{n \in \mathbb{N}} \|A\{x := n\}\| \\
\|\forall X A\| &= \bigcup_{F : \mathbb{N}^k \to \mathfrak{F}(\Pi)} \|A\{X := \dot{F}\}\| \quad \text{(if X has arity } k\)
\end{align*}
$$

whereas its truth value $|A| \subseteq \Lambda$ is defined by $|A| = \|A\|^{\perp}$. Finally, defining $\tau \equiv \emptyset$ (recall
that we have $\perp \equiv \forall X.X$), one can check that we have :

$$
\|\tau\| = \emptyset \qquad |\tau| = \Lambda \qquad \|\perp\| = \Pi
$$

Since the falsity value ||A|| (resp. the truth value |A|) of A actually depends on the pole ⊥,
we shall write it sometimes ||A||⊥ (resp. |A|⊥) to recall the dependency. Given a closed
formula A with parameters and a closed term t ∈ Λ, we say that:

* t realizes A and write t ⊧ A when t ∈ |A|⊥.
  (This notion is relative to a particular pole ⊥.)

* t universally realizes A and write t ⊧ A when $t \in |A|_{\perp}$ for all poles $\perp$.

From these definitions, we have

**Lemma 1 (Law of Peirce).** — Let A and B be two closed formulæ with parameters:

(1) If $\pi \in \|A\|$, then $k_{\pi} \models A \Rightarrow B$.

(2) $\mathfrak{c} \models ((A \Rightarrow B) \Rightarrow A) \Rightarrow A$.

4.3. **Valuations and substitutions.** In order to express the soundness invariants relating the type system of Section 3 with the classical realizability semantics defined above, we need to introduce some more terminology.

**Definition 7 (Valuations).** — A valuation is a function $\rho$ that associates a natural number $\rho(x) \in \mathbb{N}$ to every first-order variable $x$ and a falsity value function $\rho(X) : \mathbb{N}^k \to \mathfrak{F}(\Pi)$ to every second-order variable $X$ of arity $k$.

* Given a valuation $\rho$, a first-order variable $x$ and a natural number $n \in \mathbb{N}$, we denote by $\rho$, $x \leftarrow n$ the valuation defined by:

$$
(\rho, x \leftarrow n) = \rho_{|\text{dom}(\rho)\setminus\{x\}|} \cup \{x \leftarrow n\}.
$$

* Given a valuation $\rho$, a second-order variable $X$ of arity $k$ and a falsity value function $F : \mathbb{N}^k \to \mathfrak{F}(\Pi)$, we denote by $\rho$, $X \leftarrow F$ the valuation defined by:

$$
(\rho, X \leftarrow F) = \rho_{|\text{dom}(\rho)\setminus\{X\}|} \cup \{X \leftarrow F\}.
$$

To every pair $(A, \rho)$ formed by a (possibly open) formula $A$ of PA2 and a valuation $\rho$,
we associate a *closed* formula with parameters $A[\rho]$ that is defined by

$$
A[\rho] \equiv A\{x_1 := \rho(x_1); \dots; x_n := \rho(x_n); X_1 := \dot{\rho}(X_1); \dots; X_m := \dot{\rho}(X_m)\}
$$

where $x_1, \dots, x_n, X_1, \dots, X_m$ are the free variables of A, and writing $\dot{\rho}(X_i)$ the predicate
symbol associated to the falsity value function $\rho(X_i)$. This operation naturally extends to
typing contexts by letting $(x_1 : A_1, \dots, x_n : A_n)[\rho] \equiv x_1 : A_1[\rho], \dots, x_n : A_n[\rho]$.

**Definition 8 (Substitutions).** — A substitution is a finite function $\sigma$ from $\lambda$-variables to closed $\lambda_c$-terms. Given a substitution $\sigma$, a $\lambda$-variable $x$ and a closed $\lambda_c$-term $u$, we denote by $\sigma, x := u$ the substitution defined by $(\sigma, x := u) \equiv \sigma|_{\text{dom}(\sigma)\setminus\{x\}} \cup \{x := u\}$.

Given an open $\lambda_c$-term $t$ and a substitution $\sigma$, we denote by $t[\sigma]$ the term defined by

$$
t[\sigma] \equiv t\{x_1 := \sigma(x_1); \dots; x_n := \sigma(x_n)\}
$$

where dom($\sigma$) = {$x_1, \dots, x_n$}. Notice that $t[\sigma]$ is closed as soon as $FV(t) \subseteq$ dom($\sigma$). We say that a substitution $\sigma$ realizes a closed context $\Gamma$ with parameters and write $\sigma \vdash \Gamma$ if:
• $\mathrm{dom}(\sigma) = \mathrm{dom}(\Gamma);$

• $\sigma(x) \models A$ for every declaration $(x : A) \in \Gamma$.

**4.4. Adequacy.** Given a fixed pole $\perp$, we say that:

• A typing judgement $\Gamma \vdash t : A$ is *adequate* (w.r.t. the pole $\perp$) if for all valuations $\rho$ and for all substitutions $\sigma \models \Gamma[\rho]$ we have $t[\sigma] \models A[\rho]$.

• More generally, we say that an inference rule

$$ \frac{J_1 \quad \dots \quad J_n}{J_0} $$

is adequate (w.r.t. the pole $\perp$) if the adequacy of all typing judgements $J_1, \dots, J_n$ implies the adequacy of the typing judgement $J_0$.

From the latter definition, it is clear that a typing judgement that is derivable from a set of adequate inference rules is adequate too.

**Proposition 2 (Adequacy).** *The typing rules of Fig. 1 are adequate w.r.t. any pole $\perp$, as well as all the judgements $\Gamma \vdash t : A$ that are derivable from these rules.*

*Proof.* We will only sketch the proof for the introduction and elimination rules for implication. The rule for $\Pi$ is obvious and the rule for $\sigma$ directly stems from Lemma 1, while introduction and elimination rules for universal quantifiers results from the definition of the corresponding falsity values. A more detailed proof can be found in Krivine's article (Krivine 2003).

$$ \frac{\Gamma \vdash t : A \Rightarrow B \qquad \Gamma \vdash t : A}{\Gamma \vdash tu : B} $$

• Case $\frac{\Gamma \vdash t : A \Rightarrow B \qquad \Gamma \vdash t : A}{\Gamma \vdash tu : B}$:

we assume that $\Gamma \vdash t : A \Rightarrow B$ and $\Gamma \vdash u : B$ are adequate w.r.t. $\perp$, and pick a valuation $\rho$ and a substitution $\sigma$ such that $\sigma \models \Gamma[\rho]$. We want to show that $(tu)[\sigma] \models B[\rho]$. It suffices to show that if $\pi \in \|B[\rho]\|$, then $(tu)[\sigma] \star \pi \in \perp$. Applying the PUSH rule, we get:

$$ (tu)[\sigma] \star \pi > t[\sigma] \star u[\sigma] \cdot \pi $$

By hypothesis, we have $u[\sigma] \models A[\rho]$ (and then $u[\sigma] \cdot \pi \in \|(A \Rightarrow B)[\rho]\|$), and $t[\sigma] \models (A \Rightarrow B)[\rho]$, so that $t[\sigma] \star u[\sigma] \cdot \pi$ belongs to $\perp$. We conclude by anti-reduction.

$$ \frac{\Gamma, x : A \vdash t : B}{\Gamma} $$

• Case $\Gamma \vdash \lambda x.t : A \Rightarrow B$:

we assume that $\Gamma, x : A \vdash t : B$ is adequate w.r.t. $\perp$. This means that for any valuation $\rho$, any $u \models A[\rho]$ and any $\sigma \models \Gamma[\rho]$, denoting by $\sigma'$ the substitution $\sigma, x := u$, we have $t[\sigma'] \models B[\rho]$. Let us pick a valuation $\rho$ and a substitution $\sigma$ such that $\sigma \models \Gamma[\rho]$. We want to show that $(\lambda x.t)[\sigma] \models (A \Rightarrow B)[\rho]$. Let $u \cdot \pi$ be a stack in $\|(A \Rightarrow B)[\rho]\|$. Applying the GRAB rule, we have:

$$ (\lambda x.t)[\sigma] \star u \cdot \pi > t[\sigma, x := u] \star \pi $$

By hypothesis, we have $u \models A[\rho]$, and so $t[\sigma, x := u] \models B[\rho]$. Thus $t[\sigma, x := u] \star \pi$ belongs to $\perp$. and we conclude by anti-reduction. $\square$

Since the typing rules of Fig. 1 involve no continuation constant, every realizer that comes from a proof of second order logic by Prop. 2 is thus a proof-like term.

**4.5. Realizing the axioms of PA2.** Let us recall that in PA2, Leibniz equality $e_1 = e_2$ is defined by $e_1 = e_2 \equiv \forall Z(Z(e_1) \Rightarrow Z(e_2))$.

**Proposition 3 (Realizing Peano axioms (Krivine 2009)).** :

(1) $\lambda z . z \Vdash \forall x \forall y (s(x) = s(y) \Rightarrow x = y)$

(2) $\lambda z . z u \Vdash \forall x (s(x) = 0 \Rightarrow \perp)$ (where $u$ is any term such that $FV(u) \subseteq \{z\}$).
(3) $\lambda z . z \mathrel{||\neg} \forall x_1 \cdots \forall x_k (e_1(x_1, \dots, x_n) = e_2(x_1, \dots, x_k))$
for all arithmetic expressions $e_1(x_1, \dots, x_n)$ and $e_2(x_1, \dots, x_k)$ such that
$\mathbb{N} \models \forall x_1 \cdots \forall x_k (e_1(x_1, \dots, x_n) = e_2(x_1, \dots, x_k))$.

From this we deduce the main theorem:

**Theorem 1** (Realizing the theorems of PA2). — If A is a theorem of PA2 (in the sense defined in Section 3.3.2), then there is a closed proof-like term t such that $t \mathrel{||\neg} A$.

*Proof.* Immediately follows from Prop. 2 and 3. □

**4.6. The full standard model of PA2 as a degenerate case.** It is easy to see that when the pole $\perp$ is empty, the classical realizability model defined above collapses to the full standard model of PA2, that is: to the model (in the sense of Tarski) where individuals are interpreted by the elements of $\mathbb{N}$ and where second-order variables of arity $k$ are interpreted by all the subsets of $\mathbb{N}^k$. For that, we first notice that when $\perp = \emptyset$, the truth value $S^{\perp}$ associated to an arbitrary falsity value $S \subseteq \Pi$ can only take two different values: $S^{\perp} = \Lambda_c$ when $S = \emptyset$, and $S^{\perp} = \emptyset$ when $S \neq \emptyset$. Moreover, we easily check that the realizability interpretation of implication and universal quantification mimics the standard truth value interpretation of the corresponding logical construction in the case where $\perp = \emptyset$. Writing $\mathcal{M}$ for the full standard model of PA2, we thus easily show that:

**Proposition 4.** — If $\perp = \emptyset$, then for every closed formula $A$ of PA2 we have

$$|A| = \begin{cases} \Lambda & \text{if } \mathcal{M} \models A \\ \emptyset & \text{if } \mathcal{M} \not\models A \end{cases}$$

*Proof.* We more generally show that for all formulæ $A$ and for all valuations $\rho$ closing $A$ (in the sense defined in section 4.2) we have

$$|A[\rho]| = \begin{cases} \Lambda & \text{if } \mathcal{M} \models A[\bar{\rho}] \\ \emptyset & \text{if } \mathcal{M} \not\models A[\bar{\rho}] \end{cases}$$

where $\tilde{\rho}$ is the valuation in $\mathcal{M}$ (in the usual sense) defined by

* $\tilde{\rho}(x) = \rho(x)$ for all first-order variables $x$;

* $\tilde{\rho}(X) = \{(n_1, \dots, n_k) \in \mathbb{N}^k : \rho(X)(n_1, \dots, n_k) = \emptyset\}$ for all second-order variables $X$ of arity $k$.

(This characterization is proved by a straightforward induction on $A$.) □

An interesting consequence of the above lemma is the following:

**Corollary 1.** — If a closed formula $A$ has a universal realizer $t \mathrel{||\neg} A$, then $A$ is true in the full standard model $\mathcal{M}$ of PA2.

*Proof.* If $t \mathrel{||\neg} A$, then $t \in |A|_{\emptyset}$. Therefore $|A|_{\emptyset} = \Lambda$ and $\mathcal{M} \models A$. □

However, the converse implication is false in general, since the formula $\forall x \mathrm{Nat}(x)$ (cf Section 3.3.1) that expresses the induction principle over individuals is obviously true in $\mathcal{M}$, but it has no universal realizer when evaluation is deterministic (Krivine 2009, Theorem 12).

**4.7. Relativization to canonical integers.** We previously explained in Section 3.3.1 that we needed to relativize first-order quantifications to the class $\mathrm{Nat}(x)$. If we have as expected $\tilde{n} \mathrel{||\neg} \mathrm{Nat}(n)$ for any $n \in \mathbb{N}$, there are realizers of $\mathrm{Nat}(n)$ different from $\tilde{n}$. Intuitively, a term $t \mathrel{||\neg} \mathrm{Nat}(n)$ represents the integer $n$, but $n$ might be present only as a computation, and not directly as a computed value.

The usual technique to retrieve $\tilde{n}$ from such a term consist in the use of a storage operator $T$, which simulates a call-by-value reduction (for integers) on the first argument on the stack. While such a term is easy to define, its use would make our definition of game
harder. Rather than that, we define a new asymmetrical implication where the left member must be an integer value (somehow forcing call-by-value reduction on all integers), and the interpretation of this new implication.

$$ \mathbf{Formulæ} \qquad A, B ::= \dots | \{e\} \Rightarrow A $$

$$ \mathbf{Falsity value} \qquad \|\{e\} \Rightarrow A\| = \{\tilde{n} \cdot \pi : \llbracket e \rrbracket = n \land \pi \in \|A\|\} $$

We finally define the corresponding shorthands for relativized quantifications:

$$ \forall^{\mathbb{N}} x A(x) \equiv \forall x (\{x\} \Rightarrow A(x)) $$

$$ \exists^{\mathbb{N}} x A(x) \equiv \forall Z (\forall x (\{x\} \Rightarrow A(x) \Rightarrow Z) \Rightarrow Z) $$

It is easy to check that this relativization of first-order quantification is equivalent (in terms of realizability) to the one defined in Section 3.3.1 and that the relativized principle of induction holds.

**Proposition 5.** Let $T$ be a storage operator. The following holds for any formula $A(x)$:

(1) $\lambda x.x \mathbf{III}- \forall^{\mathbb{N}} x \mathrm{Nat}(x)$

(2) $\lambda x.x \mathbf{III}- \forall^{\mathrm{nat}} x.A(x) \Rightarrow \forall^{\mathbb{N}} x.A(x)$

(3) $\lambda x.T x \mathbf{III}- \forall^{\mathbb{N}} x.A(x) \Rightarrow \forall^{\mathrm{nat}} x.A(x)$

For an arithmetic formula $\Phi$, we denote by $\Phi^{\mathrm{N,nat}}$ the formula $\Phi$ where every existential quantifier $\exists x$ has been relativized to $\exists^{\mathbb{N}} x$, and every universal quantifier $\forall y$ to $\forall^{\mathbb{N}} y$. We let the reader check that if we define the following $\lambda_c$-terms :

$$ \begin{array}{lcl} \xi_0 := \lambda tu.t (Tu) & | & \chi_0 := \lambda tu.t (\lambda xy.u x (Ty)) \\ \xi_n := \lambda tu.t (\lambda xy.(Tu) x (\xi_{n-1} y)) & | & \chi_n := \lambda tu.t (\lambda xy.u x (T(\chi_{n-1} y))) \end{array} $$

we get the following proposition.

**Proposition 6.** Given a pole $\perp$, the following holds for all $n \in \mathbb{N}$ and any $\Sigma_{2n}^0$-formula $\Phi_n$:

(1) If $t \Vdash \Phi_n^{\mathrm{N,nat}}$ then $t \Vdash \Phi_n^{\mathrm{N,N}}$.

(2) If $t \Vdash \Phi_n^{\mathrm{N,nat}}$ then $t \Vdash \Phi_n^{\mathrm{nat,nat}}$.

(3) If $t \Vdash \Phi_n^{\mathrm{nat,nat}}$ then $\xi_n t \Vdash \Phi_n^{\mathrm{N,N}}$.

(4) If $t \Vdash \Phi_n^{\mathrm{N,N}}$ then $\chi_n t \Vdash \Phi_n^{\mathrm{nat,nat}}$.

In the case of arithmetical formulæ, we can then easily transform a realizer for one relativization into a realizer for the other one. In the authors' opinion, this enhances the fact that the choice of a relativization is more a question of convenience than a choice having a deep impact on the behaviour of the realizers.

For further details about the relativization and storage operator, please refer to Section 2.9 and 2.10.1 of Rieg's Ph.D. thesis (Rieg 2014).

**4.8. Leibniz equality.** Before going further, we would like to draw the reader's attention to the treatment that is given to equality, which is crucial in what follows. We recall that the equality of two arithmetical expressions $e_1$ and $e_2$ is defined by the 2nd-order encoding

$$ e_1 = e_2 \equiv \forall W(W(e_1) \Rightarrow W(e_2)) $$

Unfolding the definitions of falsity values, we easily get the following lemma:

**Lemma 2.** Given a pole $\perp$, if $e_1, e_2$ are arithmetical expressions, we have

$$ \|e_1 = e_2\| = \begin{cases} \|\forall X(X \Rightarrow X)\| & \text{if } \mathcal{M} \models e_1 = e_2 \\ \|\tau \Rightarrow \perp\| & \text{if } \mathcal{M} \models e_1 \neq e_2 \end{cases} $$

The following corollaries are straightforward but will be very useful in Sections 5-7, so it is worth mentioning them briefly now.

**Corollary 2.** Let $\perp$ be a fixed pole, $e_1, e_2$ some arithmetical expressions, $u \in \Lambda$ a closed term and $\pi \in \Pi$ a stack such that $u \cdot \pi \in \|e_1 = e_2\|$. If $\mathcal{M} \models e_1 = e_2$ then $u \star \pi \in \perp$.
*Proof.* By Lemma 2 we have

$$u \cdot \pi \in \|\forall X(X \Rightarrow X)\| = \{u \cdot \pi : \exists S \in \mathfrak{P}(\Pi), \pi \in S \wedge u \in |\dot{S}|\}$$

so that $u \in S^{\perp}$ and $u \star \pi \in \perp$

□

**Corollary 3.** Given a pole $\perp$, if $e_1, e_2$ are arithmetical expressions, and $u \in \Lambda, \pi \in \Pi$ are such that $u \cdot \pi \notin \|e_1 = e_2\|$, then

(1) $M \models e_1 = e_2$

(2) $u \star \pi \notin \perp$

*Proof.* (1) By contraposition: if $M \models e_1 \neq e_2$, by Lemma 2 we have $\|e_1 = e_2\| = \|\top \Rightarrow \perp\| = \Lambda \times \Pi$, hence $u \cdot \pi \in \|e_1 = e_2\|$.

(2) By (1) we have $\|e_1 = e_2\| = \|\forall X(X \Rightarrow X)\| = \bigcup_{S \in \mathfrak{P}(\Pi)} \|\dot{S} \Rightarrow \dot{S}\|$, hence $u \cdot \pi \notin \|e_1 = e_2\|$ implies that if $S = \{\pi\}$, $u \cdot \pi \notin \|\dot{S} \Rightarrow \dot{S}\|$, i.e. $u \not\models S$, so $u \star \pi \notin \perp$. □

## 5. THE SPECIFICATION PROBLEM

**5.1. The specification problem.** In the continuity of the work done for Peirce's Law (Guillermo and Miquel 2011), we are interested in the specification problem, which is to give a purely computational characterization of the universal realizers of a given formula $A$. As mentioned in this paper, this problem is much more subtle than in the case of intuitionistic realizability, what could be justified, amongst other things, by the presence of extra instructions that do not exist in the pure $\lambda$-calculus and by the ability of a realizer to backtrack at any time. Some very simple case, as the identity-type ($\forall X(X \Rightarrow X)$) or the boolean-type ($\forall X(X \Rightarrow X \Rightarrow X)$), are quite easy to specify, but more interestingly, it turns out that some more complex formulæ, for instance the Law of Peirce, can also be fully specified (Guillermo and Miquel 2011). In the following, we will focus on the generic case of arithmetical formulæ. A premise of this work was done by the first author for the particular case of formulæ of the shape $\exists^N n \forall^N y(f(x, y) = 0)$ (Guillermo 2008). In the general case (that is with a finite alternation of quantifiers) an attempt to characterize the threads of universal realizers is also given in an article of Krivine (Krivine 2003), but in the end it only provides us with the knowing of the final state, whereas we are here interested in a specification of the full reduction process. As in (Guillermo 2008), our method will rely on game-theoretic interpretation of the formulæ. Before going more into details, let us first look at the easiest example of specification.

**Example 1** (Identity type). In the language of second-order logic, the identity type is described by the formula $\forall X(X \Rightarrow X)$. A closed term $t \in \Lambda$ is said to be identity-like if $t \star u \cdot \pi > u \star \pi$ for all $u \in \Lambda$ and $\pi \in \Pi$. Examples of identity-like terms are of course the identity function $I \equiv \lambda x.x$, but also terms such as $II$, $\delta I$ (where $\delta \equiv \lambda x.xx$), $\lambda x.\mathfrak{c}(\lambda k.x)$, $\mathfrak{c}(\lambda k.k\delta k)$, etc.

**Proposition 7** ((Guillermo and Miquel 2011)). For all terms $t \in \Lambda$, the following asser-
tions are equivalent:

(1) $t \Vdash \forall X(X \Rightarrow X)$

(2) $t$ is identity-like

The interesting direction of the proof is (1) $\Rightarrow$ (2). We prove it with the methods of threads, that we use later in Section 6. Assume $t \Vdash \forall X(X \Rightarrow X)$, and consider $u \in \Lambda, \pi \in \Pi$. We want to prove that $t \star u \cdot \pi > u \star \pi$. We define the pole

$$\perp \equiv (\mathbf{th}(t \star u \cdot \pi))^c \equiv \{p \in \Lambda \star \Pi : (t \star u \cdot \pi \not\approx p)\}$$

as well as the falsity value $S = \{\pi\}$. From the definition of $\perp$, we know that $t \star u \cdot \pi \notin \perp$. As $t \Vdash \dot{S} \Rightarrow \dot{S}$ and $\pi \in \|\dot{S}\|$, we get $u \not\models S$. This means that $u \star \pi \notin \perp$, that is $t \star u \cdot \pi > u \star \pi$.
5.2. **Arithmetical formulæ.** In this paper, we want to treat the case of first-order arithmetical formulæ, that are $\Sigma_n^0$-formulæ. As we explained in Section 3.3.1, in order to recover the strength of arithmetical reasoning, we will relativize all first-order quantifications to the class $N\mathfrak{a}(x)$. Besides, relativizing the quantifiers make the individuals visible in the stacks: indeed, a stack belonging to $\|\forall^N x A(x)\|$ is of the shape $\bar{n} \cdot \pi$ with $\pi \in \|A(n)\|$, whereas a stack of $\|\forall x A(x)\|$ is of the form $\pi \in \|A(n)\|$ for some $n \in N$ that the realizers do not have any physical access to.

**Definition 9.** We define inductively the following classes of formulæ:

* $\Sigma_0^0$- and $\Pi_0^0$-formulæ are the formulæ of the form $f(\vec{e}) = 0$ where $f$ is a primitive recursive function and $\vec{e}$ a list of first-order expressions.

* $\Pi_{n+1}^0$-formulæ are the formulæ of the form $\forall^N x F$, where $F$ is a $\Sigma_n^0$-formula.

* $\Sigma_{n+1}^0$-formulæ are the formulæ of the form $\exists^N x F$, where $F$ is a $\Pi_n^0$-formula.

In the ground model $\mathcal{M}$, any closed $\Sigma_n^0$- or $\Pi_n^0$-formula $\Phi$ naturally induces a game between two players $\exists$ and $\forall$, that we shall name Eloise and Abelard from now on. Both players instantiate the corresponding quantifiers in turns, Eloise for defending the formula and Abelard for attacking it. The game, whose depth is bounded by the number of quantifications, proceeds as follows:

* When $\Phi$ is $\exists x \Phi'$, Eloise has to give an integer $m \in N$, and the game goes on over the closed formula $\Phi'\{x := m\}$.

* When $\Phi$ is $\forall y \Phi'$, Abelard has to give an integer $n \in N$, and the game goes on over the closed formula $\Phi'\{y := n\}$.

* When $\Phi$ is atomic and $\mathcal{M} \models \Phi$ ($\Phi$ is true), Eloise wins, otherwise Abelard wins.

We say that a player has a winning strategy if (s)he has a way of playing that ensures him/her the victory independently of the opponent moves. It is obvious from Tarski's definition of truth that a closed arithmetical formula $\Phi$ is true in the ground model if and only if Eloise has a winning strategy.

The problem with this too simple definition is that there exists true formulæ whose game only has non-computable winning strategies (as we shall see below), so that they cannot be implemented by $\lambda$-terms. This is why in classical logic, we will need to relax the rules of the above game to allow backtracking.

5.3. **The Halting problem or the need of backtrack.** For instance, let us consider one of the primitive recursive functions $f: N^3 \to N$ such that

$$f(m, n, p) = 0 \quad \text{iff} \quad (n > 0 \land \text{Halt}(m, n)) \lor (n = 0 \land \neg \text{Halt}(m, p))$$

where $\text{Halt}(m, n)$ is the primitive recursive predicate expressing that the $m^{\text{th}}$ Turing machine has stopped before $n$ evaluation steps (in front of the empty tape). From this we consider the game on the formula

$$\Phi_H \equiv \forall^N x \exists^N y \forall^N z (f(x, y, z) = 0)$$

that expresses that any Turing machine terminates or does not terminate. (Intuitively $y$ equals $0$ when the machine $x$ does not halt, and it represents a number larger than the execution length of $x$ otherwise.) Yet, there is no pure $\lambda$-term that can compute directly from an $m \in N$ an integer $n_m$ such that $\forall^N z (f(m, n_m, z) = 0)$ (such a term would break the halting problem). However, $\Phi_H$ could be classically realized, using the $\mathcal{c}$ instruction. Let $\Theta$ be a $\lambda$-term such that:

$$\Theta \star \bar{m} \cdot \bar{n} \cdot t_0 \cdot t_1 \cdot \pi > \begin{cases} t_0 \star \pi & \text{if the } m^{\text{th}} \text{ Turing machine stops before } n \text{ steps} \\ t_1 \star \pi & \text{otherwise} \end{cases}$$

and let $t_H$ be the following term:

$$T[m, u, k] \equiv \lambda pv. \Theta m p (k (u p \lambda pv.v)) v$$

$$t_H \equiv \lambda mu. \mathcal{c} (\lambda k. u \bar{0} T[m, u, k])$$
If we think of $t_H$ as a strategy for Eloise with backtrack allowed, we can analyze its computational behaviour this way:

* First Eloise receives the code $m$ of a Turing machine $\mathcal{M}$, and chooses to play $n = 0$, that is "$\mathcal{M}$ never stops".

* Then Abelard answers a given number of steps $p$, and Eloise checks if $\mathcal{M}$ stops before $p$ steps and distinguishes two cases:

- either $\mathcal{M}$ is still running after $p$ steps, hence $f(m, 0, p) = 0$ and Eloise wins.

- either $\mathcal{M}$ does stop before $p$ steps, then Eloise backtracks to the previous position and instead of 0, it plays $p$, that is "$\mathcal{M}$ stops before $p$ steps", which ensures him victory whatever Abelard plays after.

**Proposition 8.** $t_H \Vdash \Phi_H$

*Proof.* Let us consider a fixed pole $\perp$ and let $m \in \mathbb{N}$ be an integer, $\mathcal{M}$ be the $m^{\text{th}}$ Turing machine, and a stack $u \cdot \pi \in \|\exists^{\mathbb{N}}y\forall^{\mathbb{N}}z(f(m, y, z) = 0)\|$, and let us prove that $t_H \star \bar{m} \cdot u \cdot \pi \in \perp$. We know that

$$t_H \star \bar{m} \cdot u \cdot \pi > u \star \bar{0} \cdot T[\bar{m}, u, \mathbf{k}_\pi] \cdot \pi$$

by anti-reduction, it suffices to prove that $T[\bar{m}, u, \mathbf{k}_\pi] \Vdash \forall^{\mathbb{N}}z(f(m, 0, z) = 0)$. Thus let us consider $p \in \mathbb{N}$ and a stack $u' \cdot \pi' \in \|f(m, 0, p) = 0\|$. We distinguish two cases:

* $\mathcal{M}$ is still running after $p$ steps (that is $\mathcal{M} \Vdash \neg \text{Halt}(m, p)$). In this case, we have $f(m, 0, p) = 0$, and so by Corollary 2, $u' \star \pi' \in \perp$. Furthermore, by definition of $\Theta$, we have

$$T[\bar{m}, u, \mathbf{k}_\pi] \star \bar{p} \cdot u' \cdot \pi' > u' \star \pi' \in \perp$$

which concludes the case by anti-reduction.

* $\mathcal{M}$ stops before $p$ steps ($\mathcal{M} \Vdash \text{Halt}(m, p)$). By definition of $\Theta$, we have in this case

$$T[\bar{m}, u, \mathbf{k}_\pi] \star \bar{p} \cdot u' \cdot \pi' > \mathbf{k}_\pi \star (u \bar{p} (\lambda pv.v)) \cdot \pi' > u \star \bar{p} \cdot \lambda pv.v \cdot \pi$$

hence it suffices to show that $\lambda pv.v \Vdash \forall^{\mathbb{N}}z(f(m, p, z) = 0)$. But this is clear, as $\mathcal{M} \Vdash \text{Halt}(m, p)$, we have for any $s \in \mathbb{N}$, $\mathcal{M} \Vdash f(m, p, s) = 0$. Therefore if we consider any integer $s \in \mathbb{N}$ and any stack $u'' \cdot \pi'' \in \|f(m, p, s) = 0\|$, as in the previous case, from Corollary 2 we get $u'' \star \pi'' \in \perp$ and

$$\lambda pv.v \star \bar{s} \cdot u'' \cdot \pi'' > u'' \star \pi'' \in \perp \quad \square$$

This leads us to define a new notion of game with backtrack over arithmetical formulæ.

**5.4. $\mathbb{G}_\Phi^0$: a first game with backtrack.** From now on, to simplify our work, we will always consider $\sum_{2h}^0$-formulæ, that is of the form:

$$\exists^{\mathbb{N}}x_1 \forall^{\mathbb{N}}y_1 \dots \exists^{\mathbb{N}}x_h \forall^{\mathbb{N}}y_h f(\vec{x}_h, \vec{y}_h) = 0$$

where $h \in \mathbb{N}$ and the notation $\vec{x}_i$ refers to the tuple $(x_1, \dots, x_i)$ (we will denote the concatenation by $\cdot : \vec{x}_i \cdot x_{i+1} = \vec{x}_{i+1}$). It is clear that any arithmetical formulæ can be written equivalently in that way, adding some useless quantifiers if needed.

Given such a formula $\Phi$, we define a game $\mathbb{G}_\Phi^0$ between Eloise and Abelard whose rules are basically the same as they were before, except that we will keep track of all the former $\exists$-positions, allowing Eloise to backtrack. This corresponds to the definition of Coquand's game (Coquand 1995). We call an $\exists$-position of size $i \in [0, h]$ a pair of tuple of integers $(\vec{m}_i, \vec{n}_i)$ standing for the instantiation of the variables $\vec{x}_i, \vec{y}_i$, while a $\forall$-position will be a pair of the form $(\vec{m}_{i+1}, \vec{n}_i)$. We call history of a game and note $H$ the set of every former $\exists$-positions. The game starts with an empty history ($H = \{0\}$) and proceeds as follows:

* $\exists$-move: Eloise chooses a position $(\vec{m}_i, \vec{n}_i) \in H$ for some $i \in [0, h-1]$, and proposes $m_{i+1} \in \mathbb{N}$, so that $(\vec{m}_{i+1}, \vec{n}_i)$ becomes the current $\forall$-position.

* $\forall$-move: Abelard has to answer with some $n_{i+1} \in \mathbb{N}$ to complete the position.
If $i+1=h$ and $f(\vec{m}_h, \vec{n}_h) = 0$, then Eloise wins and the game stops. Otherwise, we simply add the new $\exists$-position $(\vec{m}_{i+1}, \vec{n}_{i+1})$ to $H$, and the game goes on. We say that Abelard wins if the game goes on infinitely, that is if Eloise never wins.

Given a set $H$ of former $\exists$-positions, we will say that Eloise has a *winning strategy* and write $H \in W_{\Phi}^{0}$ if she has a way of playing that ensures her a victory, independently of future Abelard moves.

Formally, we define the set $W_{\Phi}^{0}$ by induction with the two following rules:

(1) If there exists $(\vec{m}_h, \vec{n}_h) \in H$ such that $M \models f(\vec{m}_h, \vec{n}_h) = 0$:

$$H \in W_{\Phi}^{0} \quad (\text{Win})$$

(2) For all $i < h$, $(\vec{m}_i, \vec{n}_i) \in H$ and $m \in N$

$$\frac{H \cup \{(\vec{m}_i \cdot m, \vec{n}_i \cdot n)\} \in W_{\Phi}^{0} \quad \forall n \in N}{H \in W_{\Phi}^{0}} \quad (\text{Play})$$

Given a formula $\Phi$, the difference between this game and the one we defined in Section 5.2 is that this one allows Eloise to make some wrong tries before ending on a winning position. This means for Abelard that its winning condition changes from *knowing one position* on which Eloise is not winning (the play ends on a false atomic formula) to always be able to find one (the play never ends), that is *Eloise is not knowing* any.

Clearly, there is a winning strategy for $G_{\Phi}^{0}$ if and only if there was one in the previous game<fnref n="1" />. It is even easy to see that for any formula $\Phi$, we have

**Proposition 9.** $M \models \Phi \iff \emptyset \in W_{\Phi}^{0}$

Given a formula $\Phi$, in both games the existence of a winning strategy is equivalent to the truth in the model, hence such a definition does not carry anything new from an outlook of model theory, the interest of this definition is fundamentally computational. For instance, for the halting problem, this will now allow Eloise to use the strategy we described in the previous section.

Besides, it is worth noting that in general, the match somehow grows among a tree of height $h$, as we shall see in the following example.

**Example 2.** We define the following function

$$g: \begin{cases} N^2 & \rightarrow N \\ (x, y) & \mapsto x + (1 \div x)y \end{cases}$$

where $\div$ refers to the truncated subtraction. Notice that $g(x, \cdot)$ is clearly bounded if $x \neq 0$. Then we consider $f$ a function such that

$$f(x_1, y_1, x_2, y_2) = 0 \text{ if and only if } (x_1 = y_1 \lor g(x_1, x_2) > g(y_1, y_2))$$

Finally, we define the formula $\varphi \in \Sigma_{4}^{0}$

$$\varphi \equiv \exists^{N} x_1 \forall^{N} y_1 \exists^{N} x_2 \forall^{N} y_2 (f(x_1, y_1, x_2, y_2) = 0)$$

which expresses that there exists $x_1$ (in fact 0) such that $g(y_1, \cdot) : z \mapsto g(y_1, z)$ is bounded for every $y_1 \neq x_1$. The shortest strategy for Eloise to win that game would be to give 0 for $x_1$, wait for an answer $m$ for $y_1$, and give $m+1$ for $x_2$. But we can also imagine that Eloise might try 0 first, receive Abelard answer, and then change her mind, start from the beginning with 1, try several possibilities before going back to the winning position. If we observe the positions Eloise will reach for such a match, we remark it draws a tree (see Figure 2). We shall formalize this remark later, but we strongly advise the reader to keep this representation in mind all along the next section.

<footnote n="1">¹It suffices to remove the "bad tries" to keep only the winning move</footnote>
<table><thead><tr><th>Start</th><th>Eloise move</th><th>Abelard</th><th>new ∃-position</th></tr></thead><tbody><tr><td>0, 0</td><td>0</td><td>1</td><td>0, 1</td></tr><tr><td>0, 0</td><td>1</td><td>0</td><td>1, 0</td></tr><tr><td>1, 0</td><td>1</td><td>1</td><td>1, 0, 1</td></tr><tr><td>1, 0</td><td>2</td><td>2</td><td>1, 0, 2</td></tr><tr><td>0, 0</td><td>2</td><td>0</td><td>2, 0</td></tr><tr><td>0, 1</td><td>2</td><td>1</td><td>0, 2, 1, 1</td></tr><tr><td>0, 2, 1, 1</td><td>Eloise wins</td><td>/</td><td>/</td></tr></tbody></table>

<figure><img src="image_3.png" /><figcaption>FIGURE 2. Example of a match for $\mathbb{G}_{\Phi}^0$</figcaption></figure>

## 6. IMPLEMENTING THE GAME

6.1. **Substitutive Game:** $\mathbb{G}_{\Phi}^1$. Now that we have at our disposal a notion of game that seems to be suitable to capture computational content of classical theorems, we shall adapt it to play with realizers. Considering a formula $\Phi \equiv \exists^N x_1 \forall^N y_1 \dots \exists^N x_h \forall y_h (f(\vec{x}_h, \vec{y}_h) = 0)$ we will have to consider sub-formulæ of $\Phi$ to write down proofs about $\Phi$. Therefore we give the following abbreviations that we will use a lot in the following:

$$E_i \equiv \forall X_{i+1} (A_{i+1} \Rightarrow X_{i+1}) \qquad (\forall i \in [0, h-1])$$

$$A_i \equiv \forall^N x_i (\forall^N y_i E_i \Rightarrow X_i) \qquad (\forall i \in [1, h])$$

$$E_h \equiv \forall W(W(f(\vec{x}_h, \vec{y}_h)) \Rightarrow W(0))$$

One can easily check that $E_0 \equiv \Phi$ and that the other definitions correspond to the unfolding of the quantifiers.

In order to play using realizers, we will slightly change the setting of $\mathbb{G}_{\Phi}^0$, adding processes. One should notice that we only add more information, so that the game $\mathbb{G}_{\Phi}^1$ is somehow a “decorated” version of $\mathbb{G}_{\Phi}^0$.

To describe the match, we use $\exists$-positions—which are just processes— and $\forall$-positions—which are 4-uples of the shape $(\vec{m}_i, \vec{n}_i, u, \pi) \in \mathbb{N}^{\le h} \times \mathbb{N}^{\le h} \times \Lambda_c \times \Pi$. If $i = h$, we say that the move is *final* or *complete*. In a given time $j$, the set of all $\forall$-positions reached before is called the *history* and is denoted as $H_j$. At each time $j$, the couple given by the current $\exists$-position $p_j$ and the history $H_j$ is called the $j$-th state. The state evolves throughout the match according to the following rules:

(1) Eloise proposes a term $t_0 \in \text{PL}$ supposed to defend $\Phi$ and Abelard proposes a stack $u_0 \cdot \pi_0$ supposed to attack the formula $\Phi$. We say that at time 0, the process $p_0 := t_0 \star u_0 \cdot \pi_0$ is the current $\exists$-position and $H_0 := \{(\emptyset, \emptyset, u_0, \pi_0)\}$ is the current history. This step defines the initial state $\langle p_0, H_0 \rangle$.

(2) Assume $\langle p_j, H_j \rangle$ is the $j$-th state. Starting from $p_j$ Eloise evaluates $p_j$ in order to reach one of the following situations:

* $p_j > u \star \pi$ for some (final) $\forall$-position $(\vec{m}_h, \vec{n}_h, u, \pi) \in H_j$. In this case, Eloise wins if $M \models f(\vec{m}_h, \vec{n}_h) = 0$.

* $p_j > u \star \bar{m} \cdot t \cdot \pi$ for some (not final) $\forall$-position $(\vec{m}_i, \vec{n}_i, u, \pi) \in H_j$ where $i < h$. If so, Eloise can decide to play by communicating her answer $(t, m)$ to Abelard and standing for his answer, and Abelard must answer a new integer $n$ together with a new stack $u' \cdot \pi'$. The $\exists$-position becomes $p_{j+1} := t \star \bar{n} \cdot u' \cdot \pi'$ and we add the $\forall$-position to the history: $H_{j+1} := H_j \cup \{(\vec{m}_i \cdot m, \vec{n}_i \cdot n, u', \pi')\}$. This step defines the next state $\langle p_{j+1}, H_{j+1} \rangle$.

If none of the above moves is possible, then Abelard wins.

Intuitively, a state $\langle p, H \rangle$ is winning for Eloise if and only if she can play in such a way that Abelard will lose anyway, independently of the way he might play.
Start with a term *t* is a “good move” for Eloise if and only if, proposed as a defender of the formula, *t* defines an initial winning state (for Eloise), independently from the initial stack proposed by Abelard. In this case, adopting the point of view of Eloise, we just say that *t* is a winning strategy for the formula Φ.

Since our characterization of realizers will be in terms of winning strategies, we might formalize this notion. We define inductively the set of winning states –which is a syntactic object– by means of a deductive system:

* if ∃(m̃h, ñh, u, π) ∈ H s.t. p > u ⋆ π and M ⊢ f(m̃h, ñh) = 0 :

$$ \overline{\langle p, H \rangle \in W_{\Phi}^{1}} \text{ (Win)} $$

* for every (m̃i, ñi, u, π) ∈ H, m ∈ N s.t. p > u ⋆ m̃ ⋅ t ⋅ π :

$$ \frac{\langle t \star \bar{n} \cdot u' \cdot \pi', H \cup \{(m_i \cdot m, n_i \cdot n, u', \pi')\} \rangle \in W_{\Phi}^1 \quad \forall (n', u', \pi') \in \mathbb{N} \times \Lambda \times \Pi}{\langle p, H \rangle \in W_{\Phi}^1} \quad (\text{Play}) $$

A term *t* is said to be a winning strategy for Φ if for any handle (u, π) ∈ Λ × Π, we have
$\langle t \star u \cdot \pi, \{(\emptyset, \emptyset, u, \pi)\} \rangle \in W_{\Phi}^1$.

**Proposition 10 (Adequacy).** If *t* is a winning strategy for $\mathbb{G}_{\Phi}^1$, then $t \Vdash \Phi$

*Proof.* We will see a more general game in the following section for which we will prove the adequacy property (Proposition 15) and which admits any winning strategy of this game as a winning strategy (Proposition 14), thus proving the adequacy in the current case. Furthermore, the proof we give for Proposition 15 is suitable for this game too. □

**6.2. Completeness of $\mathbb{G}_{\Phi}^1$ in presence of interaction constants.** In this section we will show the completeness of $\mathbb{G}_{\Phi}^1$ by substitution over the thread of execution of a universal realizer of Φ. As observed in section 5.4, the successive $∃$-positions form a tree. We give thereafter a formal statement for this observation, which will allow us to prove the completeness of this game. We shall now give a formal definition of a tree.

**Definition 10.** A (finite) tree $\mathcal{T}$ is a (finite) subset<fnref n="2" /> of $\mathbb{N}^{<\omega}$ such that if $\tau \cdot c \in \mathcal{T}$ and $c \in \mathbb{N}$, then $\tau \in \mathcal{T}$ and $\forall c' < c, \tau \cdot c' \in \mathcal{T}$, where the $\cdot$ operator denotes the concatenation. If $\tau = c_0 \cdots c_k$, we use the notation $\tau|_i = c_0 \cdots c_i$, and we note $\tau \sqsubseteq \sigma$ ($\sigma$ extends $\tau$) when :

$$ \tau \sqsubseteq \sigma \equiv \sigma|_k = c_0 \cdots c_k = \tau $$

We call characteristic function of a tree $\mathcal{T}$ any partial function $\varphi : \mathbb{N} \to \mathcal{P}(\mathbb{N}^{<\omega})$ such that:

(1) $\forall n \in \text{dom}(\varphi), \{\varphi(m) : m \le n\}$ is a tree

(2) $\varphi(|\mathcal{T}|) = \mathcal{T}$

**Lemma 3.** Assume the calculus of realizers is deterministic, and let $t_0$ be a universal realizer of $\Phi \in \Sigma_{2h}^0$. Consider $(n_j)_{j \in \mathbb{N}}$ an infinite sequence of integers, $(\kappa_j)_{j \in \mathbb{N}}$ an infinite sequence of (pairwise distinct) interaction constants that do not occur in $t_0$ and if $(\alpha_j)_{j \in \mathbb{N}}$ is an infinite sequence of substitutive and non-generative stack constants. Then there exists two integers $f, s \in \mathbb{N}$, two finite sequences $t_0, \dots, t_f \in \Lambda$ and $m_1, \dots, m_f \in \mathbb{N}$ as well as a tree characteristic function $\varphi : \llbracket 0, f \rrbracket \to \mathbb{N}^{<\omega}$ such that:

$$ \left. \begin{array}{l} t_0 \star \kappa_0 \cdot \alpha_0 > \kappa_0 \star \bar{m}_1 \cdot t_1 \cdot \alpha_0 \\[1em] \forall i \in \llbracket 1, f-1 \rrbracket \quad t_i \star \bar{n}_i \cdot \kappa_i \cdot \alpha_i > \kappa_j \star \bar{m}_{i+1} \cdot t_{i+1} \cdot \alpha_j \\[1em] t_f \star \bar{n}_f \cdot \kappa_f \cdot \alpha_f > \kappa_s \star \alpha_s \end{array} \right\} \quad \left( \begin{array}{l} \text{with } j \le i \\ \varphi(j) \sqsubseteq \varphi(i+1) \end{array} \right) $$

where $|\varphi(s)| = h$ and $M \vdash f(\bar{m}_{\varphi(s)}, \bar{n}_{\varphi(s)}) = 0$

<footnote n="2">²Observe that $|\mathcal{T}|$ (the cardinality of $\mathcal{T}$) coincides with the usual definition of the size of $\mathcal{T}$.</footnote>
**Example 3.** Before doing the proof, let us have a look at an example of such a thread scheme for a formula $\Phi \in \Sigma_4^0$ (as we considered in Example 2) and to the corresponding tree and characteristic function.

<figure><img src="image_4.png" /><figcaption>FIGURE 3. A thread scheme for $\Phi \in \Sigma_4^0$</figcaption></figure>

We observe that we could actually labeled any node of the tree using its order of apparition in the enumeration of $\mathcal{T}$ with $\varphi$.

**Definition 11.** Given such a thread scheme and a path $\tau \in \mathcal{T}$, we define $m_{\tau} = m_{\varphi^{-1}(\tau)}$ (integer $m$ at the node $\tau$), $\vec{m}_{\tau} = (m_{\tau_1}, m_{\tau_2}, \dots, m_{\tau})$ (integers $m$ along the path) and the substitution along $\tau$ is :

$$ \sigma(\tau) = \{x_i := m_{\tau_i}\}_{i=1}^{\lfloor \tau \rfloor} \{y_i := n_{\tau_i}\}_{i=1}^{\lceil \tau \rceil} $$

For instance, in Figure 3, for $\tau = 1 \cdot 1$ (which corresponds to the choosen final position $\kappa_4 \star \alpha_4$), we have :

$$ \sigma(\tau) = \{x_1 := m_2, x_2 := m_4, y_1 := n_2, y_2 := n_4\} $$

*Proof of Lemma 3.* We build a sequence $(Q_i)_{i \in \mathbb{N}}$ of sets of processes and a sequence of characteristic functions $(\varphi_i)_{i \in \mathbb{N}}$ for some trees $(\mathcal{T}_i)_{i \in \mathbb{N}}$, such that at each step $i \in \mathbb{N}$, $Q_i$ is either empty or either of the form $\mathbf{th}(p)$ for some $p \in \Lambda \times \Pi$:

* $i = 0$: we set $Q_0 = \mathbf{th}(t_0 \star \kappa_0 \cdot \alpha_0)$ and $\varphi_0 := 0 \mapsto \emptyset$

* $i \in \mathbb{N}$: given $Q_i$ and $\varphi_i$, if there exist$^3$ $j \in \mathbb{N}$, $m_{i+1} \in \mathbb{N}$ and $t_{i+1} \in \Lambda$ such that $\kappa_j \star \overline{m_{i+1}} \cdot t_{i+1} \cdot \alpha_j \in Q_i$ we set:

$$ Q_{i+1} := \mathbf{th}(t_i \star \overline{n_{i+1}} \cdot \kappa_{i+1} \cdot \alpha_{i+1}) \qquad \varphi_{i+1} := \begin{cases} k \le i & \mapsto \varphi_i(k) \\ i+1 & \mapsto \varphi_i(j) \cdot c \end{cases} $$

where $c := \min\{n \in \mathbb{N} \mid \varphi_i(j) \cdot n \notin \mathcal{T}_i\}$. It is easy to check that if $\varphi_i$ is a characteristic function for $\mathcal{T}_i$, then so is $\varphi_{i+1}$ for $\mathcal{T}_i \cup \{\varphi_i(j) \cdot c\}$;

otherwise $Q_{i+1} := \emptyset$ and $\varphi_{i+1} := \varphi_i$. We define $Q_{\infty} := \bigcup_{i \in \mathbb{N}} Q_i$, $\perp := Q_{\infty}^c$ and $\varphi := \lim_{i \in \omega} \varphi_i$. We prove by induction that for any $0 \le i \le h$, the following statement holds:

$$ \exists j \in \mathbb{N}, |\varphi(j)| = i \text{ such that } \kappa_j \cdot \alpha_j \notin \|E_i[\sigma(\varphi(j))]\| \quad (\mathrm{IH}_i) $$

**IH$_0$:** From the definition of $\perp$, we have $t_0 \star \kappa_0 \cdot \alpha_0 \notin \perp$. Besides, we know that $t_0 \models E_0$, so that $\kappa_0 \cdot \alpha_0 \notin \|E_0\|$.

**IH$_{i+1}$:** Assume we have IH$_i$, for $0 \le i < h$, that is $\exists j_i \in \mathbb{N}, |\varphi(j_i)| = i$ such that

$$ \kappa_{j_i} \cdot \alpha_{j_i} \notin \|E_i[\sigma(\varphi(j_i))]\| $$

Recall that $E_i = \forall X_{i+1}(A_{i+1} \Rightarrow X_{i+1})$, hence $\kappa_{j_i} \not\models A_{i+1}[X_{i+1} := \dot{\alpha}_{\tau}][\sigma(\varphi_i(j_i))]$. Therefore there exists $m \in \mathbb{N}$ and $t \models \forall^N y_{i+1} E_{i+1}[\sigma(\varphi(j_i))]\{x_{i+1} := m\}$ such that $\kappa_{j_i} \star \overline{m} \cdot t \cdot \alpha_{j_i} \notin \perp$. By definition of $\perp$, it means that there is some $j \in \mathbb{N}$ such that this process belong to $Q_j$, so that by definition of $Q_{j+1}$ we have $t_{j+1} = t, m_{j+1} = m, \varphi(j+1)|_i = \varphi(j_i)$,

$$ t_{j+1} \star \overline{n_{j+1}} \cdot \kappa_{j+1} \cdot \alpha_{j+1} \notin \perp $$

<footnote>$^3$Note that as the calculus is deterministic and the constants $\kappa_j$ inert, if such $j, m_{i+1}, t_{i+1}$ exist, they are unique</footnote>
Using the fact that $t_{j+1} \models \forall^N y_{i+1} E_{i+1}[\sigma(\varphi(j_i))\{x_{i+1} := m\},$ we finally get that

$$ \kappa_{i+1} \cdot \alpha_{i+1} \notin \|E_{i+1}[\sigma(\varphi(j+1))]\| $$

since $\sigma(\varphi(j+1)) = \sigma(\varphi(j_i))\{x_{i+1} := m_{j+1}; y_{i+1} := n_{j+1}\}$.

We obtain then for $\mathrm{IH}_h$ the following statement :

$$ \exists s \in \mathbb{N}, |\varphi(s)| = h \text{ such that } \kappa_s \cdot \alpha_s \notin \|\forall W(f(\vec{m}_{\varphi(s)}, \vec{n}_{\varphi(s)})) \Rightarrow W(0)\| $$

Applying the lemma 3, we get that $M \models f(\vec{m}_{\sigma}, \vec{n}_{\sigma}) = 0$ and $\kappa_s \star \alpha_s \notin \perp$. Hence there exists $f \in \mathbb{N}$ such that $\kappa_s \star \alpha_s \in Q_f$, thus

$$ t_f \star \overline{m_f} \cdot \kappa_f \cdot \alpha_f > \kappa_s \star \alpha_s, \text{ with } M \models f(\vec{m}_{\sigma}, \vec{n}_{\sigma}) = 0 $$

that is the last line of the expected thread scheme.

Besides, by definition of $Q_f$ and $\varphi_f$, we clearly have that for any $i \in [0, f - 1]$, there exists $j \in \mathbb{N}$ such that $j \le i$ and

$$ t_i \star \overline{m_i} \cdot \kappa_i \cdot \alpha_i > \kappa_j \star \overline{m_{i+1}} \cdot t_{i+1} \cdot \alpha_j $$

□

Note that, as the constants $\kappa_i$ and $\alpha_i$ are substitutive, the function $\varphi$ and the integers $f$ and $s$ only depend on the sequence $(n_i)_{i \in \mathbb{N}}$. In other words, the threads scheme is entirely defined by this sequence.

**Proposition 11** (Completeness of $\mathbb{G}_{\Phi}^1$ in presence of interaction constants). *If the calculation of realizers is deterministic and contains infinitely many interaction constants as well as infinitely many substitutive and non generative stack constants, then every universal realizer of an arithmetical formula $\Phi \in \Sigma_h^0$ is a winning strategy for the game $\mathbb{G}_{\Phi}^1$*

*Proof.* Consider $\Phi \in \Sigma_h^0$ and a closed term $t_0 \models \Phi$. Given any infinite sequence of (pairwise distinct) non generative constants $(\kappa_i)_{i \in \mathbb{N}}$ that do not occur in $t_0$ and any sequence of stack constants $(\alpha_i)_{i \in \mathbb{N}}$, we have shown that for any sequence $(n_i)_{i \in \mathbb{N}}$ of integers, there exists two integers $f, s \in \mathbb{N}$, two finite sequences of integers $m_0, \dots, m_f \in \mathbb{N}$ and closed terms $t_0, \dots, t_f \in \Lambda$ and a finite tree $\mathcal{T}$ whose characteristic function $\varphi$ verifies $|\varphi(s)| = h$:

$$ \begin{array}{l@{\qquad}l@{\qquad}l} \forall i \in [1, f-1] & t_0 \star \kappa_0 \cdot \alpha_0 > \kappa_0 \star \overline{m_1} \cdot t_1 \cdot \alpha_0 & \\ & t_i \star \overline{n_i} \cdot \kappa_i \cdot \alpha_i > \kappa_j \star \overline{m_{i+1}} \cdot t_{i+1} \cdot \alpha_j & (\text{with } j \le i \text{ and } \varphi(j) \sqsubseteq \varphi(i+1)) \\ & t_f \star \overline{m_f} \cdot \kappa_f \cdot \alpha_f > \kappa_s \star \alpha_s & (\text{with } M \models f(\overline{m}_{\varphi(s)}, \overline{n}_{\varphi(s)}) = 0) \end{array} $$

We assume $t_0$ is not a winning strategy, that is there exists a term $u_0$ and a stack $\pi_0$ such that

$$ \langle t_0 \star u_0 \cdot \pi_0, \emptyset \rangle \notin W_{\Phi}^{1} $$

and try to reach a contradiction.

We build by induction four infinite sequences $(n_i)_{i \in \mathbb{N}}$, $(u_i)_{i \in \mathbb{N}}$, $(\pi_i)_{i \in \mathbb{N}}$, $(H_i)_{i \in \mathbb{N}}$ such that for any index $i \in \mathbb{N}$, we have $H_i = \bigcup_{j \le i} \{(\overline{m}_{\varphi(j)}, \overline{n}_{\varphi(j)}, u_j, \pi_j)\}$ and the following statement:

$$ \langle t_i \{\kappa_j := u_j, \alpha_j := \pi_j\}_{j=0}^{i-1} \star \overline{n_i} \cdot u_i \cdot \pi_i, H_i \rangle \notin W_{\Phi}^{1} \quad (\mathrm{IH}_i) $$

where $t_i$ is the term taken from the thread scheme we obtain for the sequence $(n_i)_{i \in \mathbb{N}}$.

* **$\mathrm{IH}_1$ :** by substitution over the first line of the scheme, we get

$$ t_0 \star u_0 \cdot \pi_0 > u_0 \star \overline{m_1} \cdot t_1 \{\kappa_0 := u_0, \alpha_0 := \pi_0\} \cdot \pi_0 $$

As $\langle t_0 \star u_0 \cdot \pi_0, \emptyset \rangle \notin W_{\Phi}^1$, that implies by the second rule of induction that there exists $n_1, u_1, \pi_1$ such that

$$ \langle t_1 \{\kappa_0 := u_0, \alpha_0 := \pi_0\} \star \overline{n_1} \cdot u_1 \cdot \pi_1, (\emptyset, \emptyset, u_0, \pi_0) \rangle \notin W_{\Phi}^1 $$
• **IH<sub>i+1</sub>**: assume we have built $n_j, u_j, \pi_j, H_j$ for all $0 \le j \le i$, such that IH<sub>j</sub> holds. Hence by hypothesis, we have

$$ \langle t_i \{\kappa_j := u_j, \alpha_j := \pi_j\}_{j=0}^{i-1} \star \bar{n}_i \cdot u_i \cdot \pi_i, H_i \rangle \notin W_{\Phi}^{1} $$

By substitution over the threads scheme, we get an index $j \le i$ such that:

$$ t_i \{\kappa_j := u_j, \alpha_j := \pi_j\}_{j=0}^{i-1} \star \bar{n}_1 \cdot u_i \cdot \pi_i > u_j \star \bar{m}_{i+1} \cdot t_{i+1} \{\kappa_j := u_j, \alpha_j := \pi_j\}_{j=0}^{i} \cdot \pi_j $$

Furthermore we know from the hypothesis IH<sub>i</sub> that there is a pair $(\vec{m}_{\varphi_i(j)}, \vec{n}_{\varphi_i(j)})$ such that $(\vec{m}_{\varphi_i(j)}, \vec{n}_{\varphi_i(j)}, u_j, \pi_j) \in H_i$. As the second rule of induction fails, it implies the existence of $n_j, u_j, \pi_j$ such that:

$$ \langle t_{i+1} \{\kappa_j := u_j, \alpha_j := \pi_j\}_{j=0}^{i} \star \bar{n}_{i+1} \cdot u_{i+1} \cdot \pi_{i+1}, H_{i+1} \rangle \notin W_{\Phi}^{1} $$

where, taking the very same definition of $\varphi_{i+1}$ we used in the proof of lemma 3, $H_{i+1} = H_i \cup \{(\vec{m}_{\varphi_{i+1}(i+1)}, \vec{n}_{\varphi_{i+1}(i+1)}), u_{i+1}, \pi_{i+1}\}$, so we prove IH<sub>i+1</sub>.

Now, if we consider the sequence $(n_i)_{i \in \mathbb{N}}$ we built, and define $\varphi = \lim_{i \in \mathbb{N}} \varphi_i$, it is clear that $\varphi$ is the very same function that we obtain by Lemma 3. Moreover, according to this Lemma we know there exists $f, s \in \mathbb{N}$ such that

$$ t_f \{\kappa_j := u_j, \alpha_j := \pi_j\}_{j=0}^{f} \star \bar{n}_f \cdot u_f \cdot \pi_f > u_s \star \pi_s $$

with $M \models f(\vec{m}_{\varphi(s)}, \vec{n}_{\varphi(s)}) = 0$. As $(\vec{m}_{\varphi(s)}, \vec{n}_{\varphi(s)}, u_s, \pi_s) \in H_f$, the first rule of $\mathcal{G}_{\Phi}^1$ applies, and

$$ \langle t_f \{\kappa_j := u_j, \alpha_j := \pi_j\}_{j=0}^{f-1} \star \bar{n}_f \cdot u_f \cdot \pi_f, H_f \rangle \in W_{\Phi}^{1} $$

which is obviously a contradiction with IH<sub>f</sub>. □

### 6.3. A wild realizer.
The previous section gives a specification of arithmetical formulæ in the particular case where the language of realizers is deterministic<fnref n="4" /> and provides infinitely many interaction constants and infinitely many substitutive and non generative stack constants. These assumptions are actually incompatible with the presence of instructions such as eq or quote, as stated by the Proposition 1, since this break the property of substitutivity. It would be pleasing to be able to extend such a characterization to a more general framework that would allow such instructions. Nevertheless, we know from (Guillermo and Miquel 2011) that it was not possible for the Law of Peirce, and it is not possible either in this case, for the very same reason: the instruction eq (that could be simulated with quote, see Section 2.3) allows to define some wild realizers for some formulæ, that is realizers of some $\Phi$ that are not winning strategies for the game $\mathcal{G}_{\Phi}^1$.

If we consider $f_{\le} : \mathbb{N}^2 \to \mathbb{N}$ such that $\forall x, y \in \mathbb{N}, (f_{\le}(x, y) = 0 \Leftrightarrow x \le y)$, and the formula $\Phi_{\le} \equiv \exists^\mathbb{N} x \forall^\mathbb{N} y (f_{\le}(x, y) = 0)$, here is an example of such a wild realizer. We define the following terms

$$ T_2[y, m] \equiv \text{quote} (\lambda nu.\text{eq\_nat} n m (\text{eq} u (y y) I u) u) $$

$$ T_1[u, m] \equiv \lambda y. u \bar{0} T_2[y, m] $$

$$ T_0[u, m] \equiv T_1[u, m] T_1[u, m] $$

$$ t_{\le} \equiv \lambda u.\text{quote} (\lambda m. T_0[u, m]) $$

From these definitions we get for all $u \in \Lambda$ and $\pi \in \Pi$:

$$ t_{\le} \star u \cdot \pi > T_0[u, \overline{n_{\pi}}] \star \pi > u \star \bar{0} \cdot T_2[T_1[u, \overline{n_{\pi}}], \overline{n_{\pi}}] \cdot \pi $$

and moreover, for all $n \in \mathbb{N}, u' \in \Lambda$ and $\pi' \in \Pi$:

$$ T_2[T_1[u, \overline{n_{\pi}}], \overline{n_{\pi}}] \star \overline{n} \cdot u' \cdot \pi' > \begin{cases} I \star \pi' & \text{if } u' \equiv T_0[u, \overline{n_{\pi}}] \text{ and } \pi \equiv \pi' \\ u' \star \pi' & \text{otherwise} \end{cases} $$

<footnote n="4">⁴Actually, this assumption is not necessary, and has been made only for convenience in the proof of Lemma 3. In fact, we could adapt this proof to a non-deterministic case, by defining $Q_{i+1}$ as the union of the threads $\text{th}(t_i \star \overline{n_{i+1}} \cdot \kappa_{i+1} \cdot \alpha_{i+1})$ for all $j \in \mathbb{N}, m_{i+1} \in \mathbb{N}$ and $t_{i+1} \in \Lambda$ such that $\kappa_j \star \overline{m_{i+1}} \cdot t_{i+1} \cdot \alpha_j \in Q_i$. But in this case the characteristic function of the tree describing the thread scheme is more subtle to construct.</footnote>
**Proposition 12.** $t_{\le} \Vdash \exists^{\mathbb{N}}x\forall^{\mathbb{N}}y(f_{\le}(x, y) = 0)$

*Proof.* Let us consider a fixed pole $\perp$ and a stack $u \cdot \pi \in \|\exists^{\mathbb{N}}x\forall^{\mathbb{N}}y(f_{\le}(x, y) = 0)\|$, that is a falsity value $S$ such that $\pi \in \|\dot{S}\|$ and $u \in |\forall^{\mathbb{N}}x(\forall^{\mathbb{N}}y(f_{\le}(x, y) = 0) \Rightarrow \dot{S})|$. We distinguish two cases:

* either $T_0[u, \overline{n_\pi}] \star \pi \in \perp$. As we have $t_{\le} \star u \cdot \pi > T_0[u, \overline{n_\pi}] \star \pi$, we get $t_{\le} \star u \cdot \pi \in \perp$ by anti-evaluation.

* either $T_0[u, \overline{n_\pi}] \star \pi \notin \perp$. In this case, we have $t_{\le} \star u \cdot \pi > u \star \overline{0} \cdot T_2[T_1[u, \overline{n_\pi}], \overline{n_\pi}] \cdot \pi$, hence it suffices to prove that $T_2[T_1[u, \overline{n_\pi}], \overline{n_\pi}] \Vdash \forall^{\mathbb{N}}y(f_{\le}(0, y) = 0)$. Let us then consider $n \in \mathbb{N}$ and a stack $u' \cdot \pi' \in \|\forall W(W(f_{\le}(0, n)) \Rightarrow W(0))\|$.
First remark that $f_{\le}(0, n) = 0$, hence by Corollary 3 $u' \star \pi' \in \perp$, thus by assumption, we know that $(u', \pi') \not\equiv (T_0[u, \overline{n_\pi}], \pi)$. Thus we have $T_2[T_1[u, \overline{n_\pi}], \overline{n_\pi}] \star \overline{n} \cdot u' \cdot \pi' > u' \star \pi' \in \perp$, which allows to conclude by anti-evaluation.
$\square$

Notice that the subterm $\mathbf{I}$ that appears in the definition of the term $T_2$ never comes to active position in the proof of Proposition 12, so that we could actually have chosen any other closed $\lambda_c$-term instead. The point is that it can only occur if $(u', \pi') \equiv (T_0[u, \overline{n_\pi}], \pi)$, and when it is the case, we are no more interested in the end of the execution of the process $T_0[u, \overline{n_\pi}] \star \pi$, that is in a way allowed to do anything in the rest of its execution. Before giving a game-theoretic interpretation of this phenomena, we first check that $t_{\le}$ is not a winning strategy for the game $\mathcal{G}_{\Phi_{\le}}^1$.

**Proposition 13.** Let us assume that the relation of one step evaluation $>_{1}$ is only defined from the rules (GRAB), (PUSH), (SAVE), (RESTORE), (QUOTE), (EQ). Then the universal realizer $t_{\le}$ of $\Phi_{\le}$ is not a winning strategy for the game $\mathcal{G}_{\Phi_{\le}}^1$.

*Proof.* The following is a valid match for $\mathcal{G}_{\Phi_{\le}}^1$ that Eloise loses :

* Abelard starts with the initial handle $(\mathbf{I}, \alpha)$ for the empty position, where $\alpha$ is a stack constant.

* The only pair $(m, t)$ such that $t_{\le} \star \mathbf{I} \cdot \alpha > \mathbf{I} \star \overline{m} \cdot t \cdot \alpha$ is $t_1 \equiv T_2[T_1[\mathbf{I}, \overline{n_\alpha}], \overline{n_\alpha}]$ and $m_1 = 0$. Thus Eloise is forced to play that pair $(0, t_1)$

* Abelard replies with $n_1 = 0$, $u_1 \equiv T_0[\mathbf{I}, \overline{n_\alpha}]$ and $\pi_1 \equiv \alpha$.

* Then Eloise loses, as the thread $\mathbf{th}(t_1 \star \overline{n_1} \cdot u_1 \cdot \pi_1)$ contains no process of the form $\mathbf{I} \star \overline{m} \cdot t \cdot \alpha$ (to continue to play) or of the form $u_1 \star \pi_1$ (to win the game). $\square$

## 7. NON-SUBSTITUTIVE CASE

### 7.1. $\mathcal{G}_{\Phi_{\le}}^2$: cumulative game.
Despite the wild realizer $t_{\le}$ of the formula $\Phi_{\le}$ is not a winning strategy for the corresponding game $\mathcal{G}_{\Phi_{\le}}^1$, we can still think its computational behaviour in game-theoretic terms as follows. If we observe closely what happens in the match we described in the proof of the previous Proposition, if Abelard starts with $(u, \pi)$, to which Eloise answers $(0, T_2[T_1[u, \overline{n_\pi}], \overline{n_\pi}$]), Eloise then does somehow the distinction between two cases over the next Abelard answer $(n_1, u_1, \pi_1)$.

* if $(u_1, \pi_1) \not\equiv (T_0[u, \overline{n_\pi}], \pi)$, Eloise simply pursues the execution to reach $u_1 \star \pi_1$, which is a final winning position, as $0 \le n_1$.

* if $(u_1, \pi_1) \equiv (T_0[u, \overline{n_\pi}], \pi)$, as no interesting move can be obtained from the current position, Eloise backtracks to the former $\exists$-position $t_{\le} \star u \cdot \pi$, and now wins since

$$t_{\le} \star u \cdot \pi > T_0[u, \overline{n_\pi}] \star \pi \equiv u_1 \star \pi_1$$

That is to say that the term $t_{\le}$ can still be seen as a winning strategy if we give the right to Eloise to compute its move from any former $\exists$-position. This gives us a new game $\mathcal{G}_{\Phi_{\le}}^2$, in which Eloise keeps track of all the previous $\exists$-positions encountered during the game.

We thus define a $\mathcal{G}_{\Phi_{\le}}^2$-state as a pair $\langle P, H \rangle$, where $P$ is now a finite set of processes (intuitively, all $\exists$-positions, including the current one), and $H$ is exactly as in $\mathcal{G}_{\Phi_{\le}}^1$. The set $W_{\Phi_{\le}}^2$ of winning positions is inductively defined as follows:
• if there is $p \in P$ and $(\vec{m}_h, \vec{n}_h, u, \pi) \in H$ such that $p > u \star \pi$ and $M \models f(\vec{m}_h, \vec{n}_h) = 0$
$$ \overline{\langle P, H \rangle \in W_{\Phi}^2} \quad (\text{Win}) $$

• if there is $p \in P$, $i < h$, $(\vec{m}_i, \vec{n}_i, u, \pi) \in H$ and $m' \in N$ such that $p > u \star \overline{m'} \cdot t \cdot \pi$:

$$ \frac{\langle P \cup \{t \star \overline{n'} \cdot u' \cdot \pi'\}, H \cup \{(\vec{m}_i \cdot m', \vec{n}_i \cdot n', u', \pi')\} \rangle \in W_{\Phi}^2 \quad \forall (n', u', \pi') \in N \times \Lambda \times \Pi}{\langle P, H \rangle \in W_{\Phi}^2} \quad (\text{Play}) $$

A term $t$ is said to be a winning strategy for $\mathbb{G}_{\Phi}^2$ if for any handle $(u, \pi) \in \Lambda \times \Pi$, we have $\langle \{t \star u \cdot \pi\}, \{(\emptyset, u, \pi)\} \rangle \in W_{\Phi}^2$.

## 7.2. Adequacy.

**Proposition 14.** A winning strategy for $\mathbb{G}_{\Phi}^1$ is also a winning strategy for $\mathbb{G}_{\Phi}^2$.

*Proof.* It suffices to prove that for any $\mathbb{G}_{\Phi}^1$ state $\langle p, H \rangle$, if we have $\langle p, H \rangle \in W_{\Phi}^1$, then $\langle \{p\}, H \rangle \in W_{\Phi}^2$. We do it by induction on the derivation of $\langle p, H \rangle \in W_{\Phi}^1$, observing for the second rules of $\mathbb{G}_{\Phi}^2$ that if $\langle P, H \rangle \in W_{\Phi}^2$ and $P \subset P'$, then $\langle P', H \rangle \in W_{\Phi}^2$ (which is also proved by induction). $\square$

**Proposition 15 (Adequacy).** If $t$ is a winning strategy for $\mathbb{G}_{\Phi}^2$, then $t \Vdash \Phi$

*Proof.* To make the proof easier, we will use the formulæ A and E that we previously defined in Section 6.1.

Let $\perp$ be a fixed pole, $S_1$ be a falsity value, $u_0 \Vdash \forall^N x_1(E_1 \Rightarrow \dot{S}_1)) \Rightarrow \dot{S}_1$ and $\pi_0 \in S_1$, and let us show that $t \star u_0 \cdot \pi_0 \in \perp$. For that, we more generally prove the following statement:

**Fact 1.** If $\langle P, H \rangle \in W_{\Phi}^2$ and $\forall (\vec{m}_i, \vec{n}_i, u_i, \pi_i) \in H, u_i \cdot \pi_i \in \|E_i\{x_j := m_j, y_j := n_j\}_{j=1}^i\|$ then $P \cap \perp \neq \emptyset$

In particular, we have $\langle \{t \star u_0 \cdot \pi_0\}, \{(\emptyset, \emptyset, u_0, \pi_0)\} \rangle \in W_{\Phi}^2$, $u_0 \cdot \pi_0 \in \|E_0\|$, hence we can deduce that $t \star u_0 \cdot \pi_0 \in \perp$.

$\square$

*Proof of Fact 1.* We proceed by induction on the derivation of $\langle P, H \rangle \in W_{\Phi}^2$, distinguishing two possible cases:

(1) $\langle P, H \rangle \in W_{\Phi}^2$ because of the first induction rule: there exists $(\vec{m}_h, \vec{n}_h, u, \pi) \in H$ and $p \in P$ such that $p > u \star \pi$ and $M \models f(\vec{m}_h, \vec{n}_h) = 0$. If we assume that $u \cdot \pi \in \|E_h\| = \|\forall W(W(f(\vec{m}_h, \vec{n}_h)) \Rightarrow W(0))\|$, as $M \models f(\vec{m}_h, \vec{n}_h) = 0$, we get that $u \star \pi \in \perp$ (Corollary 3) and by anti-reduction, $p \in \perp$.

(2) $\langle P, H \rangle \in W_{\Phi}^2$ because of the second induction rule : there is some $p_i \in P$, $(\vec{m}_i, \vec{n}_i, u_i, \pi_i) \in H$ and $m \in N$ such that $p_i > u_i \star \overline{m} \cdot \xi \cdot \pi_i$, and for any $(n, u, \pi)$, $\langle P \cup \{\xi \star \overline{n} \cdot u \cdot \pi\}, H \cup \{(\vec{m}_h, \vec{n}_h, u, \pi)\} \rangle \in W_{\Phi}^2$. We prove that we can not have $P \cap \perp = \emptyset$. Indeed, assuming it is the case, we can show that $u_i \star \overline{m} \cdot \xi \cdot \pi_i \in \perp$. Besides, we know by hypothesis that

$$ u_i \cdot \pi_i \in \|\forall X_{i+1}(\forall^N x_{i+1}(\forall^N y_{i+1} E_{i+1}\{x_j := m_j, y_j := n_j\}_{j=1}^i \Rightarrow X_{i+1}) \Rightarrow X_{i+1})\| $$

so that it is sufficient to prove that $\xi \Vdash \forall^N y_{i+1} E_{i+1}\{x_j := m_j, y_j := n_j\}_{j=1}^i \{x_{i+1} := m\}$ to conclude. So pick $n \in N$, $u \cdot \pi \in \|E_{i+1}\{x_j := m_j, y_j := n_j\}_{j=1}^i \{x_{i+1} := m\}\|$, and let us prove that $\xi \star \overline{n} \cdot u \cdot \pi \in \perp$. We have by hypothesis that

$$ \langle P \cup \{\xi \star \overline{n} \cdot u \cdot \pi\}, H \cup \{(\vec{m}_i \cdot m, \vec{n}_i \cdot n, u, \pi)\} \rangle \in W_{\Phi}^2 $$

from which we deduce by induction (the premises are verified) that

$$ (P \cup \{\xi \star \overline{n} \cdot u \cdot \pi\}) \cap \perp \neq \emptyset $$

As $P \cap \perp = \emptyset$, we get that $\xi \star \overline{n} \cdot u \cdot \pi \in \perp$, which conclude this case. $\square$

$\square$
### 7.3. Completeness of $\mathbb{G}_{\Phi}^2$.

**Proposition 16 (Completeness of $\mathbb{G}_{\Phi}^2$).** If $t \Vdash \Phi$ then $t$ is a winning strategy.

*Proof.* Let us reason by contradiction by assuming that there exists a handle $(u_0, \pi_0) \in \Lambda \times \Pi$ such that $\langle t \star u_0 \cdot \pi_0, \{(\emptyset, \emptyset, u_0, \pi_0)\} \rangle \notin W_{\Phi}^2$. We will construct an increasing sequence $(\langle P_j, H_j \rangle)_{j \in \mathbb{N}}$ such that for any $j \in \mathbb{N}$, $\langle P_j, H_j \rangle \notin W_{\Phi}^2$. For that, let us pick a fixed enumeration $\phi: N \to N \times \Lambda$ such that every pair $(m, t)$ appears infinitely many times in the range of $\phi$. The sequence $(\langle P_j, H_j \rangle)$ is then defined as follows:

* We set $P_0 = \{t \star u_0 \cdot \pi_0\}$ and $H_0 = \{(\emptyset, \emptyset, u_0, \pi_0)\}$.

* Assume we have built a state $\langle P_j, H_j \rangle \notin W_{\Phi}^2$. Writing $(m, t) = \phi(j)$, we distinguish the two following cases:

(1) Either there exists $p \in P_j$ and $(\langle \vec{m}_i, \vec{n}_i, u, \pi \rangle \in H_j)$ such that $p > u \star \bar{m} \cdot t \cdot \pi$. From the second rule of induction we get the existence of $n \in \mathbb{N}$, $u' \in \Lambda$, $\pi' \in \Pi$ such that $\langle P \cup \{t \star \bar{n} \cdot u' \cdot \pi'\}, H \cup \{(\vec{m}_i \cdot m, \vec{n}_i \cdot n, u', \pi')\} \rangle \notin W_{\Phi}^2$. We pick such a tuple $(n, u', \pi')$ and define $P_{j+1} = P_j \cup \{t \star \bar{n} \cdot u' \cdot \pi'\}$ and $H_{j+1} = H_j \cup \{(\vec{m}_i \cdot m, \vec{n}_i \cdot n, u', \pi')\}$.

(2) Either there is no such process, and we set $P_{j+1} = P_j$ and $H_{j+1} = H_j$.

In both cases, we have constructed $P_{j+1}$ and $H_{j+1}$ such that $P_j \subset P_{j+1}$, $H_j \subset H_{j+1}$ and $\langle P_{j+1}, H_{j+1} \rangle \notin W_{\Phi}^2$. We set $P_{\infty} = \cup_{j \in \mathbb{N}} P_j$, $Q = \cup_{p \in P_{\infty}} \mathbf{th}(p)$ and $\perp = Q^c$.

By construction, we have $t \star u_0 \cdot \pi_0 \notin \perp$, and as $t \Vdash \forall X(\forall^{\mathbb{N}}x_1(\forall^{\mathbb{N}}y_1E_1 \Rightarrow X) \Rightarrow X)$, we get $u_0 \Vdash \forall^{\mathbb{N}}x_1(\forall^{\mathbb{N}}y_1E_1 \Rightarrow \{\pi_0\})$. Thus there exists $m_1 \in \mathbb{N}$ and $\xi_1 \Vdash \forall^{\mathbb{N}}y_1E_1\{x_1 := m_1\}$ such that $u_0 \star \overline{m_1} \cdot \xi_1 \cdot \pi_0 \notin \perp$, that is exists an index $j \in \mathbb{N}$ and a process $p \in P_j$ such that $p > u_0 \star \overline{m_1} \cdot \xi_1 \cdot \pi_0$. Let $k \ge j$ be such that $\phi(k) = (m_1, \xi_1)$, then by construction there is some $\overline{n_1}, u_1, \pi_1$ such that $P_{k+1} = P_k \cup \{\xi_1 \star \overline{n_1} \cdot u_1 \cdot \pi_1\}$ and $H_{k+1} = H_k \cup \{(m_1, n_1, u_1, \pi_1)\}$

As $\xi_1 \Vdash \forall^{\mathbb{N}}y_1E_1\{x_1 := m_1\} \equiv \forall^{\mathbb{N}}y_1\forall X((\forall^{\mathbb{N}}x_2\forall^{\mathbb{N}}y_2E_2\{x_1 := m_1\} \Rightarrow X) \Rightarrow X)$ and $\xi_1 \star \overline{n_1} \cdot u_1 \cdot \pi_1 \notin \perp$, we deduce than $u_1 \Vdash \forall^{\mathbb{N}}x_2\forall^{\mathbb{N}}y_2E_2\{x_1 := m_1, y_1 := n_1\} \Rightarrow \{\pi_1\})$.

Iterating this very same reasoning, we obtain that for every $i \in [1, h]$, there exists an index $k_i \in \mathbb{N}$ and a closed term $\xi_i \in \Lambda$, such that $H_{k_i}$ contains a tuple $(\vec{m}_i, \vec{n}_i, u_i, \pi_i)$, with $\xi_i \star \overline{n_i} \cdot u_i \cdot \pi_i \notin \perp$ and $\xi_i \Vdash \forall^{\mathbb{N}}y_iE_i\{x_j := m_j\}_{j=1}^{i-1}\{y_j := n_j\}_{j=1}^{i-1}$.

For $i = h$, we get then an index $k_h \in \mathbb{N}$ and a closed term $\xi_h$, such that $H_{k_h}$ contains a tuple $(\vec{m}_h, \vec{n}_h, u_h, \pi_h)$, with $\xi_h \star \overline{n_h} \cdot u_h \cdot \pi_h \notin \perp$ and $\xi_h \Vdash \forall^{\mathbb{N}}y_h\forall W(W(f(\vec{m}_h, \vec{n}_{h-1} \cdot y_h)) \Rightarrow W(0))$.

If we consider the following predicate

$$ \Delta: \left\{ \begin{array}{ll} N & \rightarrow \mathfrak{B}(\Pi) \\ 0 & \mapsto \{\pi_h\} \\ n \ge 1 & \mapsto \emptyset \end{array} \right. $$

we get in particular that $\xi_h \Vdash \{n_h\} \Rightarrow \Delta(f(\vec{m}_h, \vec{n}_h)) \Rightarrow \Delta(0)$, from which we deduce that $u_h \cdot \pi_h \notin \|\Delta(f(\vec{m}_h, \vec{n}_h))\| \Rightarrow \Delta(0)\|$. Obviously $\pi_h \in \|\Delta(0)\|$, so that necessarily we have $u_h \Vdash \Delta(f(\vec{m}_h, \vec{n}_h))$. Hence there exists $\pi \in \|\Delta(f(\vec{m}_h, \vec{n}_h))\|$, which implies that $\pi = \pi_h$ and $M \Vdash f(\vec{m}_h, \vec{n}_h) = 0$, such that $u_h \star \pi_h \notin \perp$, that is to say there is some $j \in \mathbb{N}$ and $p \in P_j$ such that $p > u_h \star \pi_h$. Taking $l = \max(j, k_h)$, this contradicts the fact that $(P_l, H_l) \notin W_{\Phi}^2$ because of the first rule of induction. $\square$

**Theorem 2.** If $\Phi$ is an arithmetical formula, there exists $t \Vdash \Phi$ if and only if $t$ implements a winning strategy for $\mathbb{G}_{\Phi}^2$.

## 8. A BARRIER FOR REALIZABILITY MODELS

8.1. **A universal realizer for every formulæ.** We show here that if an arithmetic formula $\Phi \equiv \exists^{\mathbb{N}}x_1 \dots \forall^{\mathbb{N}}y_h f(\vec{m}_h, \vec{n}_h) = 0$ is true in the ground model, as soon as we dispose of a term computing $f$, we can implement a winning strategy, hence a universal realizer. The idea of the strategy for Eloise is to enumerate "smartly" $N^h$, in the following sense: when playing a tuple $\vec{m}_h$, we first look as deep as possible in the tree of formers positions for the
tuple $\vec{m}_i$, and then go with corresponding Abelard answer. In doing so we ensure that any tuple $\vec{m}_i$ will always be played with the same answers $\vec{n}_i$. Then it is clear that is $M \models \Phi$, we will reach sooner or later a winning position.

To implement such a strategy, we consider a term computing $f$ on a given position :

$$ \Theta_f \star \langle \vec{m} \rangle_h \cdot t_1 \cdot t_2 \cdot \pi > \begin{cases} t_1 \star \pi & \text{if } M \models f(\vec{m}, \vec{n}) = 0 \\ t_2 \star \pi & \text{if } M \models f(\vec{m}, \vec{n}) \neq 0 \end{cases} $$

where $\langle \vec{m} \rangle_i$ is a $\lambda_c$-implementation<fnref n="5" /> for the tuple $\vec{m}_i$, and that we also have a term next acting as a successor for $N^h$.

$$ \text{next} \star \langle \vec{m} \rangle_h^i \cdot t \cdot \pi > t \star \langle \vec{m} \rangle_h^{i+1} \cdot \pi $$

where $\vec{m}_h^0 = (0, \dots, 0)$ and the sequence $(\vec{m}_h^i)_{i \in N}$ is an enumeration of $N^h$. We also define the relation $\vec{m}_h^i \le_h \langle m \rangle_h^j \equiv i \le j$, which is total on $N^h$. Furthermore, we assume that we dispose of a $\lambda_c$-implementation of histories as lists of tuples, and for a given history $H$, we will denote by $\hat{H}$ its implementation<fnref n="6" />.

**Definition 12.** We say that a history $H$ is *functional* if for any $\vec{m}_i$, there exists at most one tuple $(\vec{n}_i, u, \pi)$ such that $(\vec{m}_i, \vec{n}_i, u, \mathbf{k}_\pi) \in H$.

Then we build<fnref n="7" /> several $\lambda_c$-terms according to their reductions rules. These terms will all take as parameter a $\lambda_c$-history $\hat{H}$. For $1 \le i < h$, we define a term $T_i$ who is intended to get Abelard's $i^{th}$ answer $(n_i, u_i, \pi_i)$, save it in $\hat{H}$ and plays the next integer with $T_{i+1}$:

$$ T_i[\vec{m}_h, \vec{n}_{i-1}, \hat{H}] \star \bar{n}_i \cdot u_i \cdot \pi_1 > u_i \star \bar{m}_{i+1} \cdot T_{i+1}[\vec{m}_h, \vec{n}_i, \hat{H}^{(i)}] \cdot \pi_i $$

where $\hat{H}^i \equiv [\vec{m}_1, \vec{n}_i, u_i, \mathbf{k}_{\pi_i}] \cdot \hat{H}$. The term $T_h$ gets Abelard's answer as $T_i$ does, but then computes $f$ to know if it has reached a winning position or should either initiate the next step of enumeration:

$$ T_h[\vec{m}_h, \vec{n}_{h-1}, \hat{H}] \star \bar{n}_h \cdot u_h \cdot \pi_h > \Theta_f \star \langle m \rangle_h \cdot \langle n \rangle_h \cdot u_h \cdot N[\vec{m}_h, \hat{H}^{(h)}] \cdot \pi_h $$

with $\hat{H}^h \equiv [\vec{m}_h, \vec{n}_h, u_h, \mathbf{k}_{\pi_h}] \cdot \hat{H}$. Then $N$ computes the next tuple in the enumeration and $L$ looks in the tree for the maximum former partial position similar to an initial segment of this tuple:

$$ N[\langle m \rangle_h, \hat{H}] \star \pi > \text{next} \star \langle m \rangle_h \cdot (\lambda m'_1 \cdots m'_h \cdot L[\langle m' \rangle_h, \hat{H}]) \cdot \pi \\ L[\langle m \rangle_h, \hat{H}] \star \pi > u_i \star \bar{m}_{i+1} \cdot T_{i+1}[\langle m \rangle_h, \langle n \rangle_i, \hat{H}] \cdot \pi_i $$

with $(\langle m \rangle_i, \langle n \rangle_i, u_i, \mathbf{k}_{\pi_i}) \in \hat{H}$ and $\forall j > i, \forall \vec{n}_j \in N^j, \forall u \in \Lambda, \forall \pi \in \Pi((\langle m \rangle_j, \langle n \rangle_j, u, \mathbf{k}_\pi) \notin \hat{H})$. Finally we consider $t_\Phi$ that would be the winning strategy, such that:

$$ t_\Phi \star u_0 \cdot \pi_0 > u_0 \star \bar{0} \cdot T_1[\langle 0 \rangle_h, \langle \cdot \rangle, \hat{H}_0] \cdot \pi_0 $$

with $H_0 \equiv (\cdot, \cdot, u_0, \mathbf{k}_{\pi_0})$

**Proposition 17.** If $M \models \Phi$, then $t_\Phi$ is a winning strategy for $\mathbb{G}_\Phi^1$.

The proof does neither present any conceptual difficulty nor any interest in itself, but still remains quite technical. The idea is to propagate the contradiction along the enumeration of $N^h$ in order to contradict $M \models \Phi$ at the limit. To do so, we define the proposition $\mathbf{P}(i, \vec{m}_h, H)$ as the following statement :

$\mathbf{P}(i, \vec{m}_h, H)$ : "there exists $\vec{n}_i \in N^i, u_i \in \Lambda, \pi_i \in \Pi$ such that

* $\{(\vec{m}_i, \vec{n}_i, u_i, \pi_i)\} \cup H$ is functional

* $\langle T_i[\langle m \rangle_h, \langle n \rangle_{i-1}, \hat{H}] \star \bar{n}_i \cdot u_i \cdot \pi_i, \{(\vec{m}_i, \vec{n}_i, u_i, \pi_i)\} \cup H \rangle \notin W_\Phi^1$"

<footnote n="5">⁵We could chose for instance to use a list representation for tuples, in which case $\langle \vec{m} \rangle_i \equiv [\vec{m}_1, \dots, \vec{m}_i]$, but here the data-type would not be relevant, we only pay attention to some "big" steps of reduction independently of technical representation of data</footnote>

<footnote n="6">⁶$H \cup \{(\vec{m}_i, \vec{n}_i, u, \pi)\}$ will so correspond to $[\langle \vec{m} \rangle_i, \langle \vec{n} \rangle_i, u, k_\pi] \cdot \hat{H}$.</footnote>

<footnote n="7">⁷We let the reader check the existence of such terms, which is a straightforward $\lambda_c$-calculus exercise</footnote>
and prove two technical lemmas.

**Lemma 4.** For any $i \in [1, h]$, $\vec{m}_h \in \mathbb{N}^h$ and any history $H$, $\mathbf{P}(i, \vec{m}_h, H)$ implies there exists an history $H'$ such that $H \subset H'$ and $\mathbf{P}(h, \vec{m}_h, H')$

*Proof.* It suffices to see that because of the reduction rule defining $T_i$, if $\mathbf{P}(i, \vec{m}_h, H)$ holds then the second rule of $\mathbb{G}_\Phi^1$ has to fail, hence there exists $n_{i+1}, u_{i+1} \in \Lambda, \pi_{i+1} \in \Pi$ such that

$$ \langle T_{i+1}[(\langle m \rangle_h, \langle n \rangle_i, \hat{H}^i] \star \bar{n}_{i+1} \cdot u_{i+1} \cdot \pi_{i+1}, \{(\vec{m}_{i+1}, \vec{n}_{i+1}, u_{i+1}, \pi_{i+1})\} \cup H^i \rangle \notin W_\Phi^1 $$

where $H^i = \{(\vec{m}_1, \vec{n}_i, u_i, \mathbf{k}_{\pi_i})\cup H$, which is still a functional environment. Therefore $\mathbf{P}(i, \vec{m}_h, H) \Rightarrow \mathbf{P}(i+1, \vec{m}_h, H^i)$, and $\mathbf{P}(i, \vec{m}_h, H) \Rightarrow \mathbf{P}(h, \vec{m}_h, H')$) follows by easy decreasing induction on $i \in [1, h]$. $\square$

**Lemma 5.** For any history $H$, $\mathbf{P}(h, \vec{m}_h^j, H)$ implies that

(1) there exists $\vec{n}_h \in \mathbb{N}^h$ such that $M \not\models f(\vec{m}_h^j, \vec{n}_h) = 0$

(2) there exists a history $H'$ such that $H \subset H'$ and $\mathbf{P}(h, \vec{m}_h^{j+1}, H')$

*Proof.* Given a history $H$, if $\mathbf{P}(h, \vec{m}_h^j, H)$ holds, then it means that the first rule of induction of $\mathbb{G}^1$ fails, hence necessarily $M \not\models f(\vec{m}_h^j, \vec{n}_h) = 0$ and by definition of $T_h$, using the notations $H^h = \{(\vec{m}_h^j, \vec{n}_h, u_h, \pi_h)\} \cup H$ and $\langle m' \rangle_h = \langle m \rangle_h^{j+1}$, we get that

$$ T_h[\langle m \rangle_h^j, \langle n \rangle_{h-1}, \hat{H}] \star \bar{n}_h \cdot u_h \cdot \pi_h > u_i \star \vec{m}'_{i+1} \cdot T_{i+1}[\langle m' \rangle_h, \langle n' \rangle_i, \hat{H}^h] \cdot \pi_i $$

with $(\langle m' \rangle_i, \langle n' \rangle_i, u_i, \mathbf{k}_{\pi_i}) \in \hat{H}$ and $\forall j > i, \forall (\vec{n}_j, u, \pi) \in \mathbb{N}^j \times \Lambda \times \Pi(\langle m' \rangle_j, \langle n \rangle_j, u, \mathbf{k}_{\pi}) \notin \hat{H}$. Note that this condition ensures the functionality of $H^h \cup \{(\vec{m}_h^{j+1}, \vec{n}_i, u_i, \pi_i)\}$. From $\mathbf{P}(h, \vec{m}_h^j, H)$ once more, we get that the second rule of induction of $\mathbb{G}^1$ fails too, and so that $\mathbf{P}(i+1, \vec{m}_h^{j+1}, H^h)$. Hence by Lemma 4 we get the existence of $H'$ such that $H \subset H^h \subset H'$ and $\mathbf{P}(h, \vec{m}_h^{j+1}, H')$ holds. $\square$

*Proof of Proposition 17.* By contraposition. We show that if $t_\Phi$ is not a winning strategy, then there exists a growing sequence of history $(H_j)_{j \in \mathbb{N}}$ such that for all $j \in \mathbb{N}$, $\mathbf{P}(h, \vec{m}_h^j, H_j)$ holds.

Indeed, assume $t_\Phi$ is not a winning strategy, that is to say there is $u_0 \in \Lambda, \pi_0 \in \Pi$ such that $\langle t_\Phi \star u_0 \cdot \pi_0, \emptyset \rangle \notin W_\Phi^1$. Then because of the reduction rule of $t_\Phi$, it means that the second rule of $\mathbb{G}_\Phi^1$ fails, thus there exists $(n_1, u_1, \pi_1 \in \mathbb{N} \times \Lambda \times \Pi$, such that

$$ \langle T_1[\langle 0 \rangle_h, \langle \cdot \rangle, \hat{H}] \star \bar{n}_1 \cdot u_1 \cdot \pi_1, \{(\vec{m}_1, \vec{n}_1, u_1, \pi_1)\} \cup H \rangle \notin W_\Phi^1 $$

with $H = (\cdot, \cdot, u_0, \pi_0)$, that is $\mathbf{P}(1, \vec{m}_h^0, H)$. Then by Lemma 4 we get that there exists $H_0$ such that $\mathbf{P}(h, \vec{m}_h^0, H_0)$ holds, and the claim follows by easy induction. Then we set $\mathcal{H} = \cup_{j \in \mathbb{N}} H_j$, that is functional (because each $H_j$ is, and $H_j \subset H_{j+1}$).

Applying the first clause of Lemma 5, we get that for all $j \in \mathbb{N}$, there exists $\vec{n}_h^j$ such that $(\vec{m}_h^j, \vec{n}_h^j, u, \pi) \in \mathcal{H}$ for some $u \in \Lambda$ and $\pi \in \Pi$ and $M \not\models f(\vec{m}_h^j, \langle n \rangle_h^j) = 0$.

Furthermore, as $\mathcal{H}$ is functional, it easily implies that:

$$ \forall m_1 \exists n_1 \dots \forall m_h \exists n_h (M \not\models f(\vec{m}_h, \vec{n}_h) = 0) $$

and thus we finally get $M \not\models \Phi$.

$\square$

Combining the results we obtained at this point, we get the following theorem:

**Theorem 3.** If $\Phi$ is an arithmetical formula, then $M \models \Phi$ if and only if there exists $t \vdash \Phi$.

*Proof.* The first direction is a consequence of Propositions 17 and 15, the reverse directly comes from Proposition 4. $\square$
## 8.2. Leibniz equality vs primitive non-equality.
Here we have chosen to consider formulæ based on equalities, and we should wonder what happens if we use instead formulæ based on disequalities:

$$ \exists x_1 \forall y_1 \dots \exists x_n \forall y_n f(\vec{x}_n, \vec{y}_n) \neq 0. $$

We know that both definitions are equivalent from a model-theoretic point of view. Indeed, if we define the following function $h$:

$$ h = \begin{cases} x \mapsto 1 & \text{if } x = 0 \\ x \mapsto 0 & \text{otherwise} \end{cases} $$

then for all $\vec{x} \in \mathbb{N}^n$, $M \models f(\vec{x}) = 0$ if and only if $M \models (h \circ f)(\vec{x}) \neq 0$. In other words, formulæ based on a non-equality have the same expressiveness, and we also might have chosen it as definition for the arithmetical formulæ (see Definition 9).

In classical realizability the disequality can be given a simple semantic:

$$ \|e_1 \neq e_2\| = \begin{cases} \|\tau\| & \text{if } M \models e_1 \neq e_2 \\ \|\perp\| & \text{otherwise} \end{cases} $$

which is equivalent to the negation of equality. Indeed, one can easily check that we have $\lambda x.t.(x) \models e_1 \neq e_2 \Rightarrow \neg(e_1 = e_2)$ and $\lambda t.(t)I \models \neg(e_1 = e_2) \Rightarrow e_1 \neq e_2$.

Yet using these definitions, the rules of the game would have slightly changed. Indeed, if we observe closely what happens at the last level of the game (with every variable already instantiated but the one of the last universal quantifier), that is a formula $\forall^N y(f(y) \neq 0)$, if the formula is true in the model, then the falsity value is empty, so that the opponent can not give any answer:

$$ \|\forall y(f(y) \neq 0)\| = \bigcup_{n \in \mathbb{N}} \|f(n) \neq 0\| = \|\tau\| = 0 \quad (\forall n \in \mathbb{N}, M \models f(n) \neq 0) $$

Hence Eloise does not have to compute the formula $f$ to know whether she can win or not, she only has to wait for a potential answer of Abelard, and keep on playing if she eventually gets one.

We shall bring the reader to notice two important facts. Firstly, it is clear that as Eloise has no need to compute $f$, she only needs to do somehow a “blind” enumeration, hence we can build the very same realizer we built in Proposition 17 without using a term computing $f$. In fact, such a realizer would be suitable for any $f$, even not computable, that is :

**Proposition 18.** (Krivine 2009) For all $n \in \mathbb{N}$, there exists $t_n \in \Lambda_c$ such that for any $f$ :
$N^{2n} \to \mathbb{N}$, if $M \models \exists x_1 \forall y_1 \dots \exists x_n \forall y_n f(\vec{x}_n, \vec{y}_n) \neq 0$, then $t_n \models \exists^N x_1 \forall^N y_1 \dots \exists^N x_n \forall^N y_n f(\vec{x}_n, \vec{y}_n) \neq 0$.

Secondly, such a result it obviously false if we use equality instead of non-equality. Going back to the halting problem, if we consider one of the functions $f: N^2 \to \mathbb{N}$ such that

$$ f(m, n) = 0 \quad \text{iff} \quad (n = 0 \land \exists^N p(\text{Halt}(m, p))) \lor (n \neq 0 \land \forall^N p(\neg\text{Halt}(m, p))) $$

it is clear that $f$ is not computable and that $M \models \forall y \exists x (f(y, x) = 0)$ (that only says that a Turing machine stops or does not stop). We know by Proposition 18 that there is a term $u \in \Lambda_c$ such that $u \models \forall^N y \exists^N x (h \circ f)(y, x) \neq 0$, but there is no term $t$ such that $t \models \forall^N y \exists^N xf(y, x) = 0$, and thus no term $t'$ such that $t' \models (\forall^N y \exists^N x (h \circ f)(y, x) \neq 0) \Rightarrow (\forall^N y \exists^N xf(y, x) = 0)$. This phenomena is quite strange$^9$, as both formulæ were perfectly equivalent in the ground model. As we explained, a game-theoretic interpretation of this fact is based on the idea on the idea that the use of a non-equality leaves the computation

<footnote>$^8$Otherwise, using a witness extraction method for $\Sigma_0^1$-formulæ (Miquel 2010), we would be able for all $m \in \mathbb{N}$ to compute $n_m \in \mathbb{N}$ such that $f(m, n_m) = 0$, breaking the halting problem.</footnote>

<footnote>$^9$In fact, it already appears when considering the formula $\forall x(x = 0 \iff h(x) \neq 0)$ that is not realized if not relativized to naturals.</footnote>
to the opponent, and making so the game easier. However, in the author's opinion this does not furnish a satisfying enough explanation for the model-theoretic point of view, and it might be interesting to deal with this phenomena more deeply.

**8.3. Connection with forcing.** In this paper, we only considered the *standard realizability models* of PA2 (following the terminology of (Krivine 2011)), that is: the realizability models parameterized on tuples of the form $(\Lambda, \Pi, >, \perp)$, where $(\Lambda, \Pi, >)$ is a particular instance of the $\lambda_c$-calculus, and where $\perp$ is a pole. The strong separation between the calculus (on one side) and the pole (on the other side) is essential to define the notion of universal realizability, which is at the heart of the specification problem studied in this paper.

However, the definitions of classical realizability can be extended in many different ways. First, we may replace second-order arithmetic (PA2) by Zermelo-Fraenkel set theory (ZF), using a model-theoretic construction (Krivine 2000; Krivine 2012) that is reminiscent from the construction of forcing models and of Boolean-valued models of ZF. *Mutatis mutandis*, all the results presented in this paper remain valid in the framework of classical realizability models of ZF, provided we consider a representation of arithmetic formulæ in the language of set theory that preserves their computational interpretation in the sense of PA2 (see (Krivine 2012)).

Second, we may replace the terms and stacks of the $\lambda_c$-calculus by the $\mathcal{A}$-terms and $\mathcal{A}$-stacks of an arbitrary *classical realizability algebra* $\mathcal{A}$, as shown by Krivine (Krivine 2011; Krivine 2012). Intuitively, classical realizability algebras generalize $\lambda_c$-calculi (with poles) the same way as partial combinatory algebras (J. R. B. Cockett 2006) generalize the $\lambda$-calculus (or Gödel codes for partial recursive functions) in the framework of intuitionistic realizability. This broad generalization of classical realizability—in a framework where terms and stacks are not necessarily of a combinatorial nature—is essential, since it allows us to make the connection between forcing and classical realizability explicit. Indeed, any complete Boolean algebra can be presented as a classical realizability algebra, so that all Boolean-valued models of ZF (or forcing models) can actually seen as particular cases of classical realizability models of ZF. (In this setting, the combination of realizability and forcing presented in (Krivine 2011; Miquel 2011) can be seen as a generalization of the method of iterated forcing.)

In the general framework of classical realizability algebras, the specification problem studied in this paper does not make sense anymore (due to the loss of the notion of universal realizability), but we can still use the $\lambda_c$-terms presented in Section 8.1 to show more generally that every arithmetic formula that is true in the ground model is realized by a proof-like term.

**Theorem 4.** Let $\mathcal{M}$ be a Tarski model of ZFC, $\mathcal{A}$ a classical realizability algebra taken as a point of $\mathcal{M}$, and $\mathcal{M}^\mathcal{A}$ the classical realizability model of ZF built from the ground model $\mathcal{M}$ and the classical realizability algebra $\mathcal{A}$. Then for every closed arithmetical formula $\phi$ (expressed in the language of ZF) such that $\mathcal{M} \models \phi$, there exists a proof-like term $\theta \in \mathcal{A}$ such that $\theta \Vdash_{\mathcal{A}} \phi$.

This shows that arithmetical formulæ remain absolute in the framework of classical realizability models of set theory, which generalizes a well-known property of forcing models to classical realizability. Actually, recent work of Krivine (Krivine 2014) shows that this result extends to the class of $\Sigma_2^1$- and $\Pi_2^1$-formulæ as well. By discovering the existence of an ultrafilter for the characteristic Boolean algebra $\mathfrak{Z_2}$ (Krivine 2012) of the realizability model $\mathcal{M}^\mathcal{A}$, Krivine succeeded to construct (by quotient and extensional collapse) a proper class $\mathcal{M}' \subseteq \mathcal{M}^\mathcal{A}$ that constitutes a transitive model of ZF elementarily equivalent to $\mathcal{M}$, and that contains the same ordinals as $\mathcal{M}^\mathcal{A}$. Hence the Levy-Schoenfield theorem (Jech 2013, Theorem 25.20) applies to $\mathcal{M}, \mathcal{M}'$ and $\mathcal{M}^\mathcal{A}$, thus proving the absoluteness of $\Sigma_2^1$-and $\Pi_2^1$-formulæ.
*Acknowledgements*. The authors wish to thank Alexandre MIQUEL, who provided valuable assistance to the writing of the connection between the specification results and forcing in Section 8.3, the anonymous reviewers for their constructive comments, as well as Marjolaine LACOMBE, who was of great help in correcting numerous english mistakes.

## REFERENCES

Barbanera, F. and S. Berardi (1996). "A Symmetric Lambda Calculus for Classical Program Extraction". In: *Inf. Comput.* 125.2, pp. 103–117.

Barendregt, H. (1984). *The Lambda Calculus: Its Syntax and Semantics*. Vol. 103. Studies in Logic and The Foundations of Mathematics. North-Holland.

Church, A. (1941). *The calculi of lambda-conversion*. Vol. 6. Annals of Mathematical Studies. Princeton.

Coquand, Thierry (1995). "A Semantics of Evidence for Classical Arithmetic". In: *J. Symb. Log.* 60.1, pp. 325–337. DOI: 10.2307/2275524. URL: http://dx.doi.org/10.2307/2275524.

Curien, P.-L. and H. Herbelin (2000). "The duality of computation". In: *ICFP*, pp. 233–243.

Curry, H. B. and R. Feys (1958). *Combinatory Logic*. Vol. 1. North-Holland.

Friedman, H. (1973). "Some applications of Kleene's methods for intuitionistic systems". In: *Cambridge Summer School in Mathematical Logic*. Vol. 337. Springer Lecture Notes in Mathematics. Springer-Verlag, pp. 113–170.

- (1978). "Classically and intuitionistically provably recursive functions". In: *Higher Set Theory*. Lecture Notes in Mathematics 669, pp. 21–28.

Girard, J.-Y. (2006). *Le point aveugle – Cours de logique – Volume I – vers la perfection*. Hermann.

Girard, J.-Y., Y. Lafont, and P. Taylor (1989). *Proofs and Types*. Cambridge University Press.

Guillermo, M. (2008). "Jeux de réalisabilité en arithmétique classique". PhD thesis. Université Paris 7.

Guillermo, M. and A. Miquel (2011). "Specifying Peirce's law in classical realizability". Submitted.

Howard, W. A. (1969). "The formulae-as-types notion of construction". Privately circulated notes.

J. R. B. Cockett, P. J. W. Hofstra (2006). "An introduction to partial lambda algebras".

Jech, T. (2013). *Set Theory: The Third Millennium Edition, Revised and Expanded*. Springer Monographs in Mathematics. Springer. ISBN: 9783642078996. URL: http://books.google.com.uy/books?id=70N-cgAACAAJ.

Kleene, S. C. (1945). "On the interpretation of intuitionistic number theory". In: *Journal of Symbolic Logic* 10, pp. 109–124.

Kreisel, G. (1951). "On the interpretation of non-finitist proofs, I." In: *J. Symb. Log.* 16, pp. 241–267.

- (1952). "On the interpretation of non-finitist proofs, II." In: *J. Symb. Log.* 17, pp. 43–58.

Krivine, J.-L. (1993). *Lambda-calculus, types and models*. Masson.

- (2000). "The Curry-Howard Correspondence in Set Theory". In: *LICS*. IEEE Computer Society, pp. 307–308. ISBN: 0-7695-0725-5.

- (2001). "Typed lambda-calculus in classical Zermelo-Fraenkel set theory". In: *Arch. Math. Log.* 40(3), pp. 189–205.

- (2003). "Dependent choice, 'quote' and the clock". In: *Th. Comp. Sc.* 308, pp. 259–276.

- (2004). "A call-by-name lambda-calculus machine". In: *Higher Order and Symbolic Computation*.
- (2009). "Realizability in classical logic. In Interactive models of computation and program behaviour". In: *Panoramas et synthèses* 27.

- (2011). "Realizability algebras: a program to well order R". In: *Logical Methods in Computer Science* 7.3.

- (2012). "Realizability algebras II : new models of ZF + DC". In: *Logical Methods in Computer Science* 8.1. 28 p., p. 10.

- (2014). *Quelques propriétés des modèles de réalisabilité de ZF*. http://hal.archives-ouvertes.fr/hal-00940254. url: http://hal.archives-ouvertes.fr/hal-00940254.

McCarty, D. (1984). "Realizability and Recursive Mathematics". PhD thesis. Carnegie-Mellon University.

Miquel, A. (2007). "Classical Program Extraction in the Calculus of Constructions". In: *Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings*. Vol. 4646. Lecture Notes in Computer Science. Springer, pp. 313–327.

- (2010). "Existential witness extraction in classical realizability and via a negative translation". In: *Logical Methods for Computer Science*.

- (2011). "Forcing as a Program Transformation". In: *LICS*. IEEE Computer Society, pp. 197–206. ISBN: 978-0-7695-4412-0.

Myhill, J. (1973). "Some properties of intuitionistic Zermelo-Fraenkel set theory". In: *Lecture Notes in Mathematics* 337, pp. 206–231.

Oliva, P. and T. Streicher (2008). "On Krivine's Realizability Interpretation of Classical Second-Order Arithmetic". In: *Fundam. Inform.* 84.2, pp. 207–220.

Parigot, M. (1997). "Proofs of Strong Normalisation for Second Order Classical Natural Deduction". In: *J. Symb. Log.* 62.4, pp. 1461–1479.

Rieg, Lionel (2014). "On Forcing and Classical Realizability". Theses. Ecole normale supérieure deyon-ENS LYON. url: https://tel.archives-ouvertes.fr/tel-01061442.

(MAURICIO GUILLERMO), UNIVERSIDAD DE LA REPÚBLICA, IMERL, FACULTAD DE INGENIERÍA, MONTEVIDEO, URUGUAY
*E-mail address:* mguille@fing.edu.uy

(ÉTIENNE MIQUEY), PPS LABORATORY, UNIV PARIS DIDEROT, TEAM PiR2, INRIA
UNIVERSIDAD DE LA REPÚBLICA, IMERL, FACULTAD DE INGENIERÍA, MONTEVIDEO, URUGUAY
*E-mail address:* etienne.miquey@ens-lyon.fr