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

HAL
open science

# Stateful Realizers for Nonstandard Analysis

Bruno Dinis, Étienne Miquey

► To cite this version:

Bruno Dinis, Étienne Miquey. Stateful Realizers for Nonstandard Analysis. Logical Methods in Computer Science, 2023, Volume 19, Issue 2, 10.46298/LMCS-19(2:7)2023. [https://hal.science/hal-04053612](https://hal.science/hal-04053612)

HAL Id: hal-04053612

https://hal.science/hal-04053612

Submitted on 31 Mar 2023

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_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
STATEFUL REALIZERS FOR NONSTANDARD ANALYSIS

BRUNO DINIS ◦ª AND ÉTIENNE MIQUEY ◦ᵇ

ª Escola de Ciência e Tecnologia, Universidade de Évora
*e-mail address:* bruno.dinis@uevora.pt

ᵇ Aix-Marseille Université, I2M, CNRS, Marseille, France
*e-mail address:* etienne.miquey@univ-amu.fr

ABSTRACT. In this paper we propose a new approach to realizability interpretations for nonstandard arithmetic. We deal with nonstandard analysis in the context of (semi) intuitionistic realizability, focusing on the Lightstone-Robinson construction of a model for nonstandard analysis through an ultrapower. In particular, we consider an extension of the λ-calculus with a memory cell, that contains an integer (the state), in order to indicate in which slice of the ultrapower $M^ι$ the computation is being done. We pay attention to the nonstandard principles (and their computational content) obtainable in this setting. In particular, we give non-trivial realizers to Idealization and a non-standard version of the LLPO principle. We then discuss how to quotient this product to mimic the Lightstone-Robinson construction.

# 1. INTRODUCTION

In this paper we propose a new approach to realizability interpretations for nonstandard arithmetic. On the one hand, we deal with nonstandard analysis in the context of (semi) intuitionistic realizability. On the other hand, we focus on Lightstone and Robinson's construction of a model for nonstandard analysis through an ultrapower [LR75]. This paper is an extended version of [DM21]. The main novelties here are in Section 4.4, where we establish a connection with evidenced frames [CMT21], and in Section 6, where we give a realizer for a nonstandard version of the Lesser Limited Principle of Omniscience (LLPO). We also now have a better understanding of why performing a quotient leads to some counter-intuitive properties (cf. Section 7).

Throughout the history of mathematics, infinitesimals were crucial for the intuitive development of mathematical knowledge by authors such as Archimedes, Stevin, Fermat,

*Key words and phrases:* realizability, nonstandard arithmetic, stateful computations, ultrafilters, glueing.

The authors would like to thank Alexandre Miquel for suggesting several ideas at the root of this work and Valentin Blot and Mikhail Katz, as well as the anonymous reviewers of [DM21], for their accurate remarks and suggestions. The first author was supported by FCT - Fundação para a Ciência e a Tecnologia, and the research centers CMAFcIO - Centro de Matemática, Aplicações Fundamentais e Investigação Operacional and CIMA - Centro de Investigação em Matemática e Aplicações – under the projects UIDB/04561/2020, UIDP/04561/2020 and UIDP/04674/2020.
Leibniz, Euler and Cauchy, to name but a few (see e.g. [KS13, BBE$^+$18, BBG$^+$20]). In particular, in Leibniz's Calculus one may recognize calculation rules – sometimes called the *Leibniz rules* [Lut87, Cal92, DvdB19] – which correspond to heuristic intuitions for how the infinitesimals should operate under calculations: the sum and product of infinitesimals is infinitesimal, the product of a limited number (i.e. not infinitely large) with an infinitesimal is infinitesimal,...

In [Rob61, Rob66] Robinson showed that, in the setting of model theory, it is possible to extend usual mathematical sets ($\mathbb{N}$, $\mathbb{R}$, etc.) witnessing the existence of new elements, the so-called *nonstandard* individuals. In this way, it is possible to deal consistently with infinitesimal and infinitely large numbers via ultraproducts and ultrapowers, in a way that is consistent with the Leibniz rules. Since the extended structures are nonstandard models of the original structures, this new setting was dubbed *nonstandard analysis*.

These constructions are meant to simplify doing mathematics: notions like limits or continuity can for instance be given a simpler form in nonstandard analysis. Later in the 70s, Nelson developed a syntactical approach to nonstandard analysis, introducing in particular three key principles: Idealization, Standardization and Transfer [Nel77]. The validity of these principles for constructive mathematics has been studied in different settings, in particular, following some pioneer work by Moerdijk, Palmgren and Avigad [Moe95, MP97, Avi05] in nonstandard intuitionistic arithmetic, several recent works, inspired by Nelson's approach, lead to interpretations of nonstandard theories in intuitionistic realizability models [BBS12, DF17, HvdB17, DG18].

The very first ideas of realizability are to be found in the Brouwer-Heyting-Kolmogorov interpretation [Hey34, Kol32], which identifies evidences and computing proofs (the realizers). Realizability was designed by Kleene to interpret the computational content of the proofs of Heyting arithmetic [Kle45], and was later extended to more expressive frameworks [Gö58, Kre51, Kri09]. While the Curry-Howard isomorphism focuses on a syntactical correspondence between proofs and programs, realizability rather deals with the (operational) semantics of programs: a *realizer* of a formula *A* is a program which *computes* adequately with the specification that *A* provides. As such, realizability constitutes a technique to develop new models of a wide class of theories (from Heyting arithmetic to Zermelo-Fraenkel set theory), whose algebraic structures has been studied in [vO08, Kri16, Miq20].

With the development of his classical realizability, Krivine evidences the fact that extending the $\lambda$-calculus with new programming instructions may result in getting new reasoning principles: *call/cc* to get classical logic [Gri90, Kri09], *quote* for dependent choice [Kri01], etc. In this paper, we follow this path to show how the addition of a monotonic reference allows us to get a realizability interpretation for nonstandard analysis. The realizability interpretation proposed here can be understood as a computational interpretation of the ultraproduct construction in [LR75], where the value of the reference indicates the slice of the product in which the computation takes place. In particular, we obtain a realizer for the Idealization principle whose computational behaviour increases the reference in the manner of a diagonalization process. Our setting turns out to be semi-intuitionistic since it allows to deduce a rather non-trivial realizer for a nonstandard version of the nonconstructive Lesser Limited Principle of Omniscience [BR87].

**Outline.** We start this paper by recalling the main ideas of the ultraproduct construction (Section 2) and the definition of a standard realizability interpretation for second-order Heyting arithmetic (Section 3). We then introduce stateful computations and our notion of
realizability with slices in Section 4. We also show that our stateful interpretation induces an evidenced frame thus providing a connection with the usual algebraic tools to deal with realizability interpretations. As shown in Section 5 and Section 6, this interpretation provides us with realizers for several nonstandard reasoning principles. We discuss the possibility of taking a quotient for this interpretation in Section 7. We conclude the paper in Section 8 with a comparison to related work and with some questions left for future work.

## 2. THE ULTRAPOWER CONSTRUCTION

The main contribution of this paper consists in defining a realizability interpretation to give a computational content to the ultrapower construction of Robinson and Lightstone in [LR75]. We shall begin by briefly explaining how this construction works in the realm of model theory.

Let us start by recalling some definitions.

**Definition 2.1.** Let $I$ be a set. We say that $\mathcal{F} \subset \mathcal{P}(I)$ is a filter over $I$ if:

(i) $\mathcal{F}$ is non empty and $\emptyset \notin \mathcal{F}$ (non triviality)

(ii) for all $F_1, F_2 \in \mathcal{F}, F_1 \cap F_2 \in \mathcal{F}$ (closure under intersection)

(iii) for any $F, G \in \mathcal{P}(I)$, if $F \in \mathcal{F}$ and $F \subset G$, then $G \in \mathcal{F}$ (upwards closure)

An *ultrafilter* is a filter $\mathcal{U}$ such that for any $F \in \mathcal{P}(I)$, either $F$ or its complement $\bar{F}$ are in $\mathcal{U}$.

For instance, the set of cofinite subsets of $\mathbb{N}$ defines the so-called *Fréchet filter*, which is not an ultrafilter since it contains neither the set of even natural numbers nor the set of odd natural numbers. Nonetheless, it is well-known that any filter $\mathcal{F}$ over an infinite set $I$ is contained in an ultrafilter $\mathcal{U}$ over $I$: this is the so-called *ultrafilter principle*. An ultrafilter that contains the Fréchet filter is called a *free ultrafilter*. The existence of free ultrafilters was proved by Tarski in 1930 [Tar30] and is in fact a consequence of the Axiom of Choice.

**Definition 2.2.** Given two sets $V$ and $I$ and an ultrafilter $\mathcal{U}$ over $I$, we can define an equivalence relation $\cong_{\mathcal{U}}$ over $V^I$ by $u \cong_{\mathcal{U}} v \triangleq \{i \in I : u_i = v_i\} \in \mathcal{U}$. We write $V^I/\mathcal{U}$ for the set obtained by performing a quotient on the set $V^I$ by this equivalence relation, which is called an *ultrapower*.

Consider a theory $\mathcal{T}$ (say ZFC) and its language $\mathcal{L}$, for which we assume the existence of a model $\mathcal{M}$. The goal is to build a nonstandard model $\mathcal{M}^*$ of the theory $\mathcal{T}$ that validates new principles. Let us denote by $\mathcal{V}$ the set which interprets individuals in $\mathcal{M}$, and let us fix a free ultrafilter $\mathcal{U}$ over $\mathbb{N}$. Roughly speaking, the new model $\mathcal{M}^*$ is defined as the ultrapower $\mathcal{M}^N/\mathcal{U}$. Individuals are interpreted by functions in $\mathcal{V}^N$ while the validity of a relation $R(x_1, ..., x_k)$ (where the $x_i$ are interpreted by $f_i$, for $i \in \{1, ..., k\}$) is defined by

$$ \mathcal{M}^* \models R(f_1, ..., f_k) \quad \text{iff} \quad \{n \in \mathbb{N} : \mathcal{M} \models R(f_1(n), ..., f_k(n))\} \in \mathcal{U}. $$

We can now extend the language with a new predicate $\mathrm{st}(x)$ to express that $x$ is *standard*. Standard elements are defined as the ones that, with respect to $\cong_{\mathcal{U}}$, are equivalent to constant functions, i.e. $\mathcal{M}^* \models \mathrm{st}(f)$ if and only if there exists $p \in \mathbb{N}$ such that $\{n \in \mathbb{N} : f(n) = p\} \in \mathcal{U}$.

$$ \mathcal{M}^* \models \mathrm{st}(f) \quad \text{iff} \quad \exists p \in \mathbb{N}. \{n \in \mathbb{N} : f(n) = p\} \in \mathcal{U}. $$

Formulas that involve this new predicate are called *external*, while formulas of the original language $\mathcal{L}$ are called *internal*.
Lightstone and Robinson's construction relies on the well-known Loś' theorem [Lo60] which states that if $\varphi$ is an internal formula (with parameters in $V^N$), then $M^* \models \varphi$ if and only $\{n \in N : M \models \bar{\varphi}^n\} \in U$, where $\bar{\varphi}^n$ refers to the formula $\varphi$ whose parameters have been replaced by their values in $n$. This construction indeed defines a model of $\mathcal{T}$ which satisfies other relevant properties, namely Transfer, Idealization and Standardization. As a consequence of Loś' theorem, to see that an internal formula $\varphi(x)$ holds for all elements, it is enough to see that it holds for all standard elements: this is the Transfer principle. In our setting, *Idealization* amounts to a diagonalization process: it is for instance easy to see that if one defines $\delta : n \mapsto n$ (where we, with abuse of notation, write $n$ for both the natural number $n$ and its interpretation in $V$), then $M^* \models \forall x.(\mathrm{st}(x) \to x < \delta)$. Finally, *Standardization* is a sort of "comprehension scheme" which states that we can specify subsets of standard sets by giving a membership criterion for standard elements (by means of an internal formula).

### 3. REALIZABILITY IN A NUTSHELL

**3.1. Heyting second-order arithmetic.** We start by introducing the terms and formulas of Heyting second-order arithmetic (HA2), for which we follow Miquel's presentation [Miq11a]. Second-order formulas are built on top of first-order arithmetical expressions, by means of logical connectives, first- and second-order quantifications and primitive predicates. We use upper case letters for second-order variables and lower case letters for first-order ones. We use a primitive predicate Nat($e$) to denote that $e$ is a natural number (0 then has type Nat(0) and the term $st$ has type Nat($S(e)$)) provided that $t$ has type Nat($e$)). We consider the usual $\lambda$-calculus terms extended with pairs, projections (written $\pi_i$), natural numbers and a recursion operator:

<table><tr><td><b>1st-order expressions</b></td><td>$e ::= x | 0 | S(e) | f(e<sub>1</sub>, ..., e<sub>n</sub>)$</td></tr><tr><td><b>Formulas</b></td><td>$A, B ::= \mathrm{Nat}(e) | X(e<sub>1</sub>, ..., e<sub>n</sub>) | A \to B | A \wedge B$<br/>$| \forall x.A | \exists x.A | \forall X.A | \exists X.A$</td></tr><tr><td><b>Terms</b></td><td>$t, u ::= x | 0 | s | \mathrm{rec} | \lambda x.t | t u | (t, u) | \pi_1(t) | \pi_2(t)$</td></tr></table>

where $f : N^n \to N$ is any arithmetical function. We write $\Lambda$ for the set of all closed $\lambda$-terms.

Note that we did not include disjunctions as formulae. In fact, for most of our purposes, disjunctions are not needed. The only exception is Section 6 where we interpret a nonstandard version of the Lesser Limited Principle of Omniscience. It is however possible to include disjunctions all the way but, since this would mostly only add some unnecessary technicalities to all our proofs, we delay the introduction of disjunction until Section 6.

To simplify the use of existential quantifiers, as in [Miq11a], we introduce a congruence relation on formulas defined by the following rules

$$ (\exists x.A) \to B \cong \forall x.(A \to B) \qquad (\exists X.A) \to B \cong \forall X.(A \to B) \qquad (3.1) $$

This congruence relation allows us to, given any typed term, to (re)type it with any formula congruent to the original one. In particular, this means that we do not need the elimination rules for the existential quantifiers, which results in a simplified type system. This type system, which is given in Figure 1, corresponds to the usual rules of natural deduction. The reader may observe that we do not give computational content to quantifications.
$$
\begin{array}{l}
\textbf{Natural numbers} \qquad \overline{\Gamma \vdash 0 : \mathrm{Nat}(0)}^{(0)} \qquad \overline{\Gamma \vdash s : \forall^{\mathbb{N}} x. \mathrm{Nat}(S(x))}^{(S)} \\
\qquad \qquad \qquad \overline{\Gamma \vdash \mathrm{rec} : \forall Z.Z(0) \to (\forall^{\mathbb{N}} y.(Z(y) \to Z(S(y)))) \to \forall^{\mathbb{N}} x.Z(x)}^{(\mathrm{rec})}
\end{array}
$$

$$
\begin{array}{l@{\qquad}l@{\qquad}l}
\textbf{Logical rules} & \displaystyle \frac{(x : A) \in \Gamma}{\Gamma \vdash x : A} & \displaystyle \frac{\Gamma \vdash t : A \to B \quad \Gamma \vdash u : A}{\Gamma \vdash t u : B} \xrightarrow{\to E} \\[1.5ex]
& \Gamma, x : A \vdash t : B & \frac{\Gamma \vdash t : A \quad \Gamma \vdash u : B}{\Gamma \vdash (t, u) : A \wedge B} \xrightarrow{\wedge I} \\[1.5ex]
& \frac{\Gamma \vdash t : A \wedge B}{\Gamma \vdash \pi_2(t) : B} \xrightarrow{\wedge_2^2} & \frac{\Gamma \vdash t : A[x := n]}{\Gamma \vdash t : \exists x.A} \xrightarrow{\exists I} \frac{\Gamma \vdash t : \forall x.A \wedge B}{\Gamma \vdash \pi_1(t) : A} \xrightarrow{\wedge_1^1} \\[1.5ex]
& \frac{\Gamma \vdash t : A \quad x \notin FV(\Gamma)}{\Gamma \vdash t : \forall x.A} \xrightarrow{\forall I} & \frac{\Gamma \vdash t : A[X(x_1, \dots, x_n) := B]}{\Gamma \vdash t : \exists X.A} \xrightarrow{\exists I} \frac{\Gamma \vdash t : A \wedge \forall x.FV(\Gamma)}{\Gamma \vdash t : \forall X.A} \xrightarrow{\forall I} \\[1.5ex]
& \frac{\Gamma \vdash t : \forall X.A}{\Gamma \vdash t : A[X(x_1, \dots, x_n) := B]} \xrightarrow{\forall E^2} & \frac{\Gamma \vdash t : A \quad X \notin FV(\Gamma)}{\Gamma \vdash t : \forall X.A} \xrightarrow{\forall I} \frac{\Gamma \vdash t : A' \quad A \cong A'}{\Gamma \vdash t : A} \xrightarrow{\cong} \\
\end{array}
$$

$$
\frac{\Gamma \vdash t : \forall X.A}{\Gamma \vdash t : A[X(x_1, \dots, x_n) := B]} \xrightarrow{\forall E^2} \frac{\Gamma \vdash t : A \quad X \notin FV(\Gamma)}{\Gamma \vdash t : \forall X.A} \xrightarrow{\forall I} \frac{\Gamma \vdash t : A' \quad A \cong A'}{\Gamma \vdash t : A} \xrightarrow{\cong} \frac{\Gamma \vdash t : \forall x.A'}{\Gamma \vdash t : A}
$$

<caption>Figure 1: Type system</caption>

In the sequel, we make use of the following usual abbreviations:

$$
\begin{array}{l@{\qquad}l@{\qquad}l}
\mathbf{s}^{n+1}0 & \triangleq & \mathbf{s}(\mathbf{s}^n0) & \multicolumn{1}{c|}{\top \triangleq \exists X.X} & e = e' \triangleq \forall Z.(Z(e) \to Z(e')) \\
\bar{\mathbf{n}} & \triangleq & \mathbf{s}^n0 & \multicolumn{1}{c|}{\bot \triangleq \forall X.X} & \forall^{\mathbb{N}}x.A \triangleq \forall x.(\mathrm{Nat}(x) \to A) \\
& & & \multicolumn{1}{c|}{\neg A \triangleq A \to \bot} & \exists^{\mathbb{N}}x.A \triangleq \exists x.(\mathrm{Nat}(x) \wedge A) \\
\end{array}
$$

It is well-known that the above definition of equality (often called Leibniz law) enjoys the usual expected properties (reflexivity, symmetry, transitivity) and allows to perform substitution of equal terms. The quantifications $\forall^{\mathbb{N}}x.A$ and $\exists^{\mathbb{N}}x.A$ are often said to be *relativized* to natural numbers.

The one-step (weak) reduction over terms is defined by the following rules:

$$
\begin{array}{ccc}
\overline{(\lambda x.t)u \succcurlyeq \beta t[u/x]} & \overline{\mathrm{rec} \, u_0 \, u_1 \, 0 \succcurlyeq \beta u_0} & \overline{\mathrm{rec} \, u_0 \, u_1 \, (s \, t) \succcurlyeq \beta u_1 \, t \, (\mathrm{rec} \, u_0 \, u_1 \, t)} \\
\overline{\pi_1(t, u) \succcurlyeq \beta t} & & \overline{\pi_2(t, u) \succcurlyeq \beta u}
\end{array}
$$

We write $\to_\beta$ for the congruent reflexive-transitive closure of $\succcurlyeq_\beta$. The reduction $\to_\beta$ is known to be confluent, type-preserving and normalizing on typed terms [Bar92].

3.2. **Realizability interpretation of HA2.** In this subsection we define the realizability interpretation of the type system defined in Figure 1, in which formulas are interpreted as *saturated sets of terms*, i.e. as sets of closed terms $S \subseteq \Lambda$ such that $t \to_\beta t'$ and $t' \in S$ imply that $t \in S$. We write **SAT** to denote the set of all saturated sets and, given a formula $A$, we call *truth value* its realizability interpretation.
**Definition 3.1 (Valuation).** A valuation is a function $\rho$ that associates a natural number $\rho(x)$ to every first-order variable $x$ and a truth value function $\rho(X)$, i.e. a function in $\mathbb{N}^k \to \mathbf{SAT}$ to every second-order variable $X$ of arity $k$.

(1) Given a valuation $\rho$, a first-order variable $x$ and a natural number $n$, we denote by $\rho, x \mapsto n$ the valuation defined by $(\rho, x \mapsto n) \triangleq \rho|_{\text{dom}(\rho)\setminus\{x\}} \cup \{x \mapsto n\}$.

(2) Given a valuation $\rho$, a second-order variable $X$ of arity $k$ and a truth value function $F: \mathbb{N}^k \to \mathbf{SAT}$, the valuation defined by $(\rho, X \mapsto F) \triangleq \rho|_{\text{dom}(\rho)\setminus\{X\}} \cup \{X \mapsto F\}$ will be denoted by $\rho, X \mapsto F$.

We say that a valuation $\rho$ is *closing* the formula $A$ if $FV(A) \subseteq \text{dom}(\rho)$.

**Definition 3.2 (Realizability interpretation).** We interpret closed arithmetical expressions $e$ in the standard model of first-order Peano arithmetic $\mathbb{N}$. Given a valuation $\rho$ and a first-order expression $e$ (whose variables are in the domain of $\rho$) we denote its interpretation by $[e]_{\rho}$. The interpretation of a formula $A$ together with a valuation $\rho$ closing $A$ is the set $|A|_{\rho}$ defined inductively according to the following clauses:

$$
\begin{align*}
|\text{Nat}(e)|_{\rho} &\triangleq \{t \in \Lambda : t \to_{\beta} \mathbf{s}^n 0, \text{ where } n = [e]_{\rho}\} \\
|X(e_1, \dots, e_n)|_{\rho} &\triangleq \rho(X)([e_1]_{\rho}, \dots, [e_n]_{\rho}) \\
|A \to B|_{\rho} &\triangleq \{t \in \Lambda : \forall u \in |A|_{\rho}. (t u \in |B|_{\rho})\} \\
|A_1 \wedge A_2|_{\rho} &\triangleq \{t \in \Lambda : \pi_1(t) \in |A_1|_{\rho} \wedge \pi_2(t) \in |A_2|_{\rho}\} \\
|\forall x.A|_{\rho} &\triangleq \bigcap_{n \in \mathbb{N}} |A|_{\rho, x \mapsto n} \\
|\exists x.A|_{\rho} &\triangleq \bigcup_{n \in \mathbb{N}} |A|_{\rho, x \mapsto n} \\
|\forall X.A|_{\rho} &\triangleq \bigcap_{F: \mathbb{N}^k \to \mathbf{SAT}} |A|_{\rho, X \mapsto F} \\
|\exists X.A|_{\rho} &\triangleq \bigcup_{F: \mathbb{N}^k \to \mathbf{SAT}} |A|_{\rho, X \mapsto F}
\end{align*}
$$

Observe that in the previous definition, the universal quantifications cannot be seen as generalized conjunctions. Indeed, the conjunction is given computational content through pairs, while the universal quantifications are defined as intersections of truth values.

It is easy to see that for any formula $A$ and any valuation $\rho$ closing $A$, one has $|A|_{\rho} \in \mathbf{SAT}$. As it turns out, the congruences defined by Equation 3.1 are sound w.r.t. the interpretation.

**Proposition 3.3 [Miq11a].** If $A$ and $A'$ are two formulas of HA2 such that $A \cong A'$, then for all valuations $\rho$ closing both $A$ and $A'$ we have $|A|_{\rho} = |A'|_{\rho}$.

*Proof.* By induction on $A \cong A'$. Congruence easily goes through by induction, we only prove the first-order case (the second-order case is analogous):

$$
\begin{align*}
| (\exists x.A) \to B |_{\rho} &= \{ t \in \Lambda : \forall u \in |\exists x.A|_{\rho}, t u \in |B|_{\rho} \} \\
&= \{ t \in \Lambda : \forall u \in \bigcup_{n \in \mathbb{N}} |A|_{\rho, x \mapsto n}, t u \in |B|_{\rho} \} \\
&= \{ t \in \Lambda : \forall u, (\exists n, u \in |A|_{\rho, x \mapsto n}) \to t u \in |B|_{\rho} \} \\
&= \{ t \in \Lambda : \forall u, \forall n, (u \in |A|_{\rho, x \mapsto n} \to t u \in |B|_{\rho}) \} \\
&= \bigcap_{n \in \mathbb{N}} \{ t : \forall u, u \in |A|_{\rho, x \mapsto n} \to t u \in |B|_{\rho} \} \\
&= |\forall x.(A \to B)|_{\rho}
\end{align*}
\hfill $\square$
$$

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

In order to show that the realizability interpretation is sound with respect to the type system we need the following preliminary notions.
**Definition 3.4 (Substitution).** A *substitution* is a finite function $\sigma$ from $\lambda$-variables to closed $\lambda$-terms. Given a substitution $\sigma$, a $\lambda$-variable $x$ and a closed $\lambda$-term $u$, we denote by $(\sigma, x := u)$ the substitution defined by $(\sigma, x := u) \triangleq \sigma|_{\text{dom}(\sigma)\setminus\{x\}} \cup \{x := u\}$.

**Definition 3.5.** Given a context $\Gamma$ and a valuation $\rho$ closing the formulas in $\Gamma$, we say that a substitution $\sigma$ realizes $\rho(\Gamma)$ and write $\sigma \Vdash \rho(\Gamma)$ if $\text{dom}(\Gamma) \subseteq \text{dom}(\sigma)$ and $\sigma(x) \in |A|_{\rho}$ for every declaration $(x : A) \in \Gamma$.

**Definition 3.6.** A typing judgement $\Gamma \vdash t : A$ is *adequate* if for all valuations $\rho$ closing $A$ and $\Gamma$ and for all substitutions $\sigma \Vdash \rho(\Gamma)$ we have $\sigma(t) \in |A|_{\rho}$. More generally, we say that an inference rule $\frac{J_1 \quad \dots \quad J_n}{J_0}$ is adequate if the adequacy of all typing judgements $J_1, \dots, J_n$ implies the adequacy of the typing judgement $J_0$.

**Theorem 3.7 (Adequacy [Miq11a])**. *The typing rules of Figure 1 are adequate.*

*Proof.* The proof is standard, by case analysis. We draw the reader's attention to the particular case of the second-order elimination rule

$$ \frac{\Gamma \vdash t : \forall X.A \quad (\forall E^2)}{\Gamma \vdash t : A[X(x_1, \dots, x_n) := B]} $$

which relies on the fact that the truth value of any formula (here $B$) is a saturated set. To prove that this rule is indeed adequate, let us consider a valuation $\rho$ closing $\forall X.A$, $B$ and $\Gamma$ and a substitution $\sigma \Vdash \rho(\Gamma)$ such that $\sigma(t) \in |\forall X.A|_{\rho}$. By definition, this implies that for any function $F : \mathbb{N}^k \to \text{SAT}$ (where $k$ is the arity of $X$), we have $\sigma(t) \in |A|_{\rho, X \mapsto F}$. To conclude, it suffices to see that the function $n_1, \dots, n_n \mapsto |B|_{\rho, x_1 \mapsto n_1, \dots, x_k \mapsto n_k}$ is indeed in $\mathbb{N}^k \to \text{SAT}$.

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

**Corollary 3.8.** If $\Gamma \vdash t : A$ is derivable, then it is adequate.

The adequacy theorem is the key result when defining realizability interpretations in that fundamental properties stem from it. For example, we have the following corollary.

**Corollary 3.9 (Consistency).** There is no proof term $t$ such that $\vdash t : \perp$.

*Proof.* The proof is by *reductio ad absurdum*. If $\vdash t : \perp$, then by Theorem 3.7 one has $t \in |\perp| = |\forall X.X| = \bigcap_{S \in \text{SAT}} S = \emptyset$. To see that this intersection is indeed empty, one can take for example $S_0 = \{t \in \Lambda : t \to_{\beta} 0\} \in \text{SAT}$ and $S_1 = \{t \in \Lambda : t \to_{\beta} s0\} \in \text{SAT}$, then clearly $S_0 \cap S_1 = \emptyset$.

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

We would like to point out that the proof of adequacy is very flexible. Indeed, if one wants to add a new instruction to the language of terms via its typing rule, it is enough to check that this typing rule is adequate while the remainder of the proof is exactly the same.

**3.3. Introducing value restriction.** The realizability interpretation of Definition 3.2 is also flexible regarding the set of formulas that are interpreted. We illustrate this point here by introducing a new construction extending formulas which we shall use in the sequel to enforce value restriction in presence of stateful computations. This will allow us to get a better handle on the operational semantics, which will be crucial afterwards since stateful computations break the confluence of the reduction system (see Example 4.1). Such a
technique is reminiscent from ML value restriction that was introduced to circumvent the incompatibility of Curry-style polymorphism and side-effects (see for instance [Zei09]).

We start by defining the subset $\mathcal{V} \subseteq \Lambda$ of values by the following grammar:

$$ \mathbf{Values} \quad V ::= 0 \mid sV \mid \lambda x.t \mid (V_1, V_2) $$

Observe that variables are not values, otherwise the system would not be stable by substitution. In the remainder of this paper, we adopt the convention that $\lambda$-terms are denoted by lowercase letters $t, u, ...$ while uppercase letters $V, W, ...$ refer to values.

Distinguishing the set of values allows for instance to restrict the $\beta$-reduction rule to applications of functions to values:

$$ \overline{(\lambda x.t)V \triangleright_v t[V/x]} \qquad \frac{t \triangleright_v t'}{t u \triangleright_v t' u} \qquad \frac{u \triangleright_v u'}{V u \triangleright_v V u'} $$

The reflexive transitive closure $\rightarrow_v$ of the one-step reduction $\triangleright_v$ is known as the (left-to-right) *call-by-value* evaluation strategy. While it is well-known that the reduction system of the $\lambda$-calculus is confluent, so that the choice of a particular evaluation strategy does not have any consequence in terms of expressiveness, this is no longer the case when side effects (such as stateful computations in the next sections) come into play.

To enforce value restriction, let us now extend the language of formulas with a new construction:

$$ \mathbf{Formulas} \quad A, B ::= \dots | \{A\} \mapsto B $$

and the realizability interpretation accordingly by

$$ |\{A\} \mapsto B|_{\rho} \triangleq \{t \in \Lambda : \forall V \in |A|_{\rho}. (t V \in |B|_{\rho})\} $$

In particular, we have

$$ \begin{aligned} |\{\mathrm{Nat}(e)\} \mapsto B|_{\rho} &= \{t \in \Lambda : t \bar{n} \in |B|_{\rho} \text{ where } n = [[e]]_{\rho}\} \\ |\{A_1 \wedge A_2\} \mapsto B|_{\rho} &= \{t \in \Lambda : \forall V_1 \in |A_1|_{\rho}, V_2 \in |A_2|_{\rho}. t(V_1, V_2) \in |B|_{\rho} \text{ where } n = [[e]]_{\rho}\} \end{aligned} $$

It is easy to check that for any formulas $A$ and $B$, $|\{A\} \mapsto B|_{\rho}$ is a saturated set, and the adequacy of the $(\forall_E^2)$-rule is thus preserved.

While there is currently no rule to type a term $t$ with a formula of the shape $\{A\} \mapsto B$, we can nonetheless extend the type system with any rule as long as it is adequate with respect to the realizability interpretation. Indeed, here the flexibility of the interpretation comes again into play, in the sense that once the realizability interpretation of a new construct has been defined, one could extend the type system with any rule related with that construct as long as it is adequate. For instance, the rules $(\mapsto_I)$ and $(\mapsto_E)$ below are adequate.

**Proposition 3.10.** *The following typing rules are adequate:*

$$ \frac{\Gamma \vdash t : A \rightarrow B \quad (\mapsto_I)}{\Gamma \vdash t : \{A\} \mapsto B} \qquad \frac{\Gamma \vdash t : \{A\} \mapsto B \quad \Gamma \vdash V : A \quad (\mapsto_E)}{\Gamma \vdash t V : B} $$

*Proof.* For the first rule it suffices to see that for any valuation $\rho$, we have

$$ \{t \in \Lambda : \forall u \in |A|_{\rho}. (t u \in |B|_{\rho})\} \subseteq \{t \in \Lambda : \forall V \in |A|_{\rho}. (t V \in |B|_{\rho})\} $$

As for the second one, if $\rho$ is a valuation and $\sigma$ a substitution such that $\sigma(V) \in |A|_{\rho}$, $\sigma \models \rho(\Gamma)$, and $\sigma(t) \in |\{A\} \mapsto B|_{\rho}$. Then, by the definition of $|\{A\} \mapsto B|_{\rho}$, we have that $\sigma(t) \sigma(V) = \sigma(t V) \in |B|_{\rho}$ (because $\sigma(V)$ is necessarily a value). $\square$
We can also extend, maintaining the adequacy of the interpretation of {$A$} $\mapsto B$, the congruence relation with the following rules:

$$ \{\exists x.A\} \mapsto B \cong \forall x.\{A\} \mapsto B \qquad \{\exists X.A\} \mapsto B \cong \forall X.\{A\} \mapsto B $$

**Proposition 3.11.** For any formulas A and B, we have

$$ (1) \quad |\{\exists x.A\} \mapsto B|_{\rho} = |\forall x.\{A\} \mapsto B|_{\rho} $$

$$ (2) \quad |\{\exists X.A\} \mapsto B|_{\rho} = |\forall X.\{A\} \mapsto B|_{\rho} $$

*Proof.* The proof is analogous to the proof of Proposition 3.3, for instance for the first part, we have:

$$ \begin{align*} |\{\exists x.A\} \mapsto B|_{\rho} &= \{t \in \Lambda : \forall V \in |\exists x.A|_{\rho}, t V \in |B|_{\rho}\} \\ &= \{t \in \Lambda : \forall V \in \bigcup_{n \in \mathbb{N}} |A|_{\rho, x \mapsto n}, t V \in |B|_{\rho}\} \\ &= \{t \in \Lambda : \forall V, (\exists n, V \in |A|_{\rho, x \mapsto n}) \Rightarrow t V \in |B|_{\rho}\} \\ &= \{t \in \Lambda : \forall V, \forall n, (V \in |A|_{\rho, x \mapsto n} \Rightarrow t V \in |B|_{\rho})\} \\ &= \bigcap_{n \in \mathbb{N}} \{t : \forall V, \in |A|_{\rho, x \mapsto n} \Rightarrow t V \in |B|_{\rho}\} \\ &= |\forall x.\{A\} \mapsto B|_{\rho} \end{align*} \quad \square $$

We will make use of the following abbreviations:

$$ \forall^{\mathbb{N}} x.A \triangleq \forall x.(\{\mathrm{Nat}(x)\} \mapsto A) \qquad \exists^{\mathbb{N}} x.A \triangleq \forall X.(\forall^{\mathbb{N}} x.(A \to X)) \to X $$

While the first definition is natural, the second one may be a bit more puzzling at first sight. As we saw, the truth value of any formula has to be a saturated set. However, given a formula $A(x)$, the set $\{(\bar{n}, t) : t \in |A(n)|_{\rho}\}$ is not saturated, and so we cannot define a formula $\exists x.\{\mathrm{Nat}(x)\} \land A(x)$ whose realizers would be this set. Nonetheless, the definition of $\exists^{\mathbb{N}}x.A$ is somehow doing the trick in continuation-passing style, in the sense that we have:

**Proposition 3.12.** For any formula A, any valuation $\rho$ and any term $t$, if $t \in |\exists^{\mathbb{N}}x.A|_{\rho}$ then there exists a natural number $n \in \mathbb{N}$ and a term $u \in |A[x := n]|_{\rho}$ s.t.: $t(\lambda xy.(x, y)) \to_{\beta} (\bar{n}, u)$.

*Proof.* Let $t$ be a term such that $t \in |\exists^{\mathbb{N}}x.A|_{\rho}$. By definition, for any $X \in \mathbf{SAT}$ and any $v \in |\forall^{\mathbb{N}}x.(A \to X)|_{\rho, X \mapsto X}$, we have that $tv \in X$. Let us define the set

$$ X = \{w \in \Lambda : \exists n, u.w \to_{\beta} (\bar{n}, u) \land u \in |A[x := n]|_{\rho}\}, $$

which is obviously saturated. It is clear that $\lambda xy.(x, y) \in |\forall^{\mathbb{N}}x.(A \to X)|_{\rho, X \mapsto X}$ since for any $n \in \mathbb{N}$ and any $u \in |A[x := n]|_{\rho}$ one has $(\lambda xy.(x, y)) \bar{n} u \to_{\beta} (\bar{n}, u) \in X$. We conclude that $t(\lambda xy.(x, y)) \to_{\beta} (\bar{n}, u)$. $\square$

**Definition 3.13.** We define $T \triangleq \lambda zx.(\mathrm{rec}(\lambda y.y0)(\lambda xyz.y(\lambda x.z(sx))))z$.

The next proposition relates these new quantifications with the relativized quantifications $\forall^{\mathbb{N}}x.A$ and $\exists^{\mathbb{N}}x.A$ using the term $T$.

**Proposition 3.14.** We have

$$ (1) \quad T \Vdash \forall^{\mathbb{N}} x.A \to \forall^{\mathbb{N}} x.A $$

$$ (2) \quad \lambda x.x \Vdash \forall^{\mathbb{N}} x.A \to \forall^{\mathbb{N}} x.A $$

$$ (3) \quad \lambda z.z \lambda xy.(x, y) \Vdash \exists^{\mathbb{N}} x.A \to \exists^{\mathbb{N}} x.A $$

$$ (4) \quad \lambda xy.T y \pi_1(x) \pi_2(x) \Vdash \exists^{\mathbb{N}} x.A \to \exists^{\mathbb{N}} x.A $$

*Proof.* (1) Let $t$ be a term in $|\forall^{\mathbb{N}}x.A|$, $n \in \mathbb{N}$ a natural number and $u$ a term in $|\mathrm{Nat}(n)|$. To prove the result, since $|A[x := n]|$ is saturated, it suffices to prove that:

$$ (\mathrm{rec}(\lambda y.y0)(\lambda xyz.z(sx)))u \Vdash A[x := n] $$
Let us define the formula $B(z) \triangleq (\forall^{\mathbb{N}}x.A) \rightarrow A[x := z]$. It is straightforward to check that:

* $\lambda y.y 0 \models B(0)$

* $\lambda xyz.y (\lambda x.z(sx)) \models \forall^{\mathbb{N}}x.B(x) \rightarrow B(S(x))$

Using the adequacy of the (rec)-rule, we deduce that

$$ \mathrm{rec}(\lambda y.y 0)(\lambda xyz.z(sx))u \models B(n) $$

and the result follows from the hypothesis that $t \in |\forall^{\mathbb{N}}x.A|$.

(2) Follows directly from Proposition 3.10.

(3) Follows directly from Proposition 3.12.

(4) Let $t$ be a term in $|\exists^{\mathbb{N}}x.A|$, $\mathcal{X} \in \mathbf{SAT}$ be a predicate and $u$ a term in $|\forall^{\mathbb{N}}x.(A \rightarrow X)|_{X \mapsto \mathcal{X}}$. By assumption, there exists a natural number $n$ and two terms $t_1$ and $t_2$ such that $t_1 \in \mathrm{Nat}(n)$, $t_2 \in |A[x := n]|$ and $t \rightarrow_{\beta} (t_1, t_2)$. Then

$$ (\lambda xy.T y \pi_1(x) \pi_2(x))tu \rightarrow_{\beta} Tu \pi_1(t) \pi_2(t) \rightarrow_{\beta} Tut_1t_2 $$

From part 1 we know that $Tu$ is in $|\forall^{\mathbb{N}}x.(A \rightarrow X)|_{X \mapsto \mathcal{X}}$, hence $Tu t_1 t_2 \in \mathcal{X}$ and the result follows from the fact that $\mathcal{X}$ is saturated. $\square$

The term $T$, which forces the evaluation of an argument of type $\mathrm{Nat}(n)$ to get the underlying value $\bar{n}$ to make it compatible with a function $\forall^{\mathbb{N}}x.A$, is somehow simulating a call-by-value evaluation (for natural numbers). Such a term is usually called a *storage operator* [Kri09].

While Proposition 3.14 indicates that the different ways of relativizing the quantifiers are equivalent (in the sense that one admits a realizer if and only if the other does), it is important to keep in mind that this result is peculiar to the current effect-free settings. In particular, this result no longer holds once stateful computations are allowed.

## 4. REALIZABILITY WITH SLICES

In this section, we extend the realizability interpretation introduced in Section 3 by taking into account stateful computations. The states will be the key ingredient to give computational content to the Lightstone-Robinson construction described in Section 2. The advantage of this extended setting will become clearer in Section 5, since it allows to realize some new reasoning principles, after we investigate the status of natural numbers in Section 5.1.

### 4.1. Stateful computations.
The first step in the Lightstone-Robinson construction aims at getting a product $M^{\mathbb{N}}$ of the (initial) model $M$. In order to achieve this goal in our setting, we add a memory cell to our calculus that contains an integer, which we call the *state*. The purpose of the state is to keep track of which “slice” of the product is the interpretation being done. This product allows us to interpret first-order individuals as functions in $N^{\mathbb{N}}$, so that the interpretation accounts for new elements – the so-called nonstandard elements – for instance the diagonal function (see Proposition 5.5).

In our extended calculus, the first-order expressions are the same, while second-order formulas now use a value restriction for natural numbers and include a predicate $\mathrm{st}(e)$, as per usual in nonstandard analysis, denoting that the expression $e$ is standard. This means that in our framework we will also have two types of nonstandard quantifications: the usual $\forall^{\mathrm{st}}$, $\exists^{\mathrm{st}}$ and the relativized $\forall^{\{\mathrm{st}\}}$, $\exists^{\{\mathrm{st}\}}x$. We say that a formula is *internal* if it does not contain the predicate $\mathrm{st}(\cdot)$, and *external* otherwise. Terms are extended with two new instructions
**4.2. Stateful realizability interpretation.** The fact that our syntax now includes states allows us to interpret formulas as terms-with-states<fnref n="2" />. Truth values are then defined as saturated sets in $\mathcal{P}(\Lambda \times \mathfrak{S})$. Individuals are now individuals with states, so elements of $\mathbb{N}^{\mathfrak{S}}$, and similarly predicates of arity $k$ are elements of the set of functions from $\mathbb{N}^k$ to $\mathcal{P}(\Lambda \times \mathfrak{S})$. This creates a mismatch in the sense that predicates are no longer shaped to be applied to individuals<fnref n="3" />. In order to define our interpretation, we need to deal with this mismatch between the structure of individuals and the one of predicates, by defining a suitable notion of application.

**Definition 4.2.** Let $F : \mathbb{N}^k \to \mathcal{P}(\Lambda \times \mathfrak{S})$ be a predicate. We define the application of $F$ to individuals $f_1, \dots, f_k \in \mathbb{N}^{\mathfrak{S}}$ by $F@ (f_1, \dots, f_k) \triangleq \{(t; \mathfrak{s}) : (t; \mathfrak{s}) \in F(f_1(\mathfrak{s}), \dots, f_k(\mathfrak{s}))\}$.

**Definition 4.3.** An individual $f \in \mathbb{N}^{\mathfrak{S}}$ is said to be *standard* if it is a constant function, i.e. if there exists $n \in \mathbb{N}$ such that $\forall \mathfrak{s} \in \mathfrak{S}. (f(\mathfrak{s}) = n)$. We then write $f = n^*$.

**Definition 4.4.** We define saturated sets with respect to the stateful reduction to be sets $S \in \Lambda \times \mathfrak{S}$ s.t. for any terms $t, t' \in \Lambda$ and any states $\mathfrak{s}, \mathfrak{s}' \in \mathfrak{S}$, if $(t'; \mathfrak{s}') \in S$ and $t^s \downarrow^{\mathfrak{s}'} t'$ then $(t; \mathfrak{s}) \in S$. With abuse of notation we denote the set of these saturated sets by **SAT**.

In the realizability interpretation with slices below, truth values are defined as saturated sets. This allows us to reason by *anti-reduction* (sometimes also called *expansion*) in any fixed state. By anti-reduction, we mean that to show that a term $t$ together with a state $\mathfrak{s}$ belongs to such a saturated set $S$, it is enough to find $\mathfrak{s}'$ and $t'$ such that $t^s \downarrow^{\mathfrak{s}'} t'$ and $(t'; \mathfrak{s}') \in S$.

We now consider valuations which are functions that associate a function in $\mathbb{N}^{\mathfrak{S}}$ to every first-order variable $x$ and a truth value function from $\mathbb{N}^k$ to **SAT** to every second-order variable $X$ of arity $k$. Again, with abuse of notation we denote such valuation by $\rho$.

We also extend the usual interpretation of first-order expressions to range over $\mathbb{N}^{\mathfrak{S}}$. To that end, we simply define arithmetical functions pointwise on the domain. For instance, if $f \in \mathbb{N}^{\mathfrak{S}}$, we write $S^*(f)$ for the function $\mathfrak{s} \mapsto (S(f(\mathfrak{s})))$. When it is clear from the context, we abuse the notation (even more) by writing $0, S, [[\cdot]]_\rho, \text{etc. instead of } 0^*, S^*, [[\cdot]]_\rho^*$.

<footnote n="2">²A realizability interpretation with a similar structure, although with a different notion of state, can be found in [MH18]. The perspective of the latter is also different in that it aims at proving the normalization of a classical call-by-need calculus.</footnote>

<footnote n="3">³This phenomenon also occurs in the Lightstone-Robinson construction of an ultrapower [LR75].</footnote>
**Definition 4.5** (Realizability with slices). The interpretation of a formula $A$ together with a valuation $\rho$ closing $A$ is the set $|A|_{\rho}^{\mathcal{S}}$ defined inductively according to the following clauses:

$$
\begin{align*}
|\mathrm{st}(e)|_{\rho}^{\mathcal{S}} &\triangleq \begin{cases} \Lambda \times \mathcal{S} & \text{if } [[e]]_{\rho} \text{ is standard} \\ \emptyset & \text{otherwise} \end{cases} \\
|X(e_1, \dots, e_n)|_{\rho}^{\mathcal{S}} &\triangleq \rho(X)@([e_1]_{\rho}, \dots, [e_n]_{\rho}) \\
|\{\mathrm{Nat}(e)\} \mapsto A|_{\rho}^{\mathcal{S}} &\triangleq \{(t; \mathfrak{s}) \in \Lambda \times \mathcal{S} : (t \bar{n}; \mathfrak{s}) \in |A|_{\rho}^{\mathcal{S}}, \text{ where } n = [[e]]_{\rho}(\mathfrak{s})\} \\
|A \to B|_{\rho}^{\mathcal{S}} &\triangleq \{(t; \mathfrak{s}) \in \Lambda \times \mathcal{S} : \forall u. ((u; \mathfrak{s}) \in |A|_{\rho}^{\mathcal{S}} \Rightarrow (t u; \mathfrak{s}) \in |B|_{\rho}^{\mathcal{S}})\} \\
|A_1 \wedge A_2|_{\rho}^{\mathcal{S}} &\triangleq \{(t; \mathfrak{s}) \in \Lambda \times \mathcal{S} : (\pi_1(t); \mathfrak{s}) \in |A_1|_{\rho}^{\mathcal{S}} \wedge (\pi_2(t); \mathfrak{s}) \in |A_2|_{\rho}^{\mathcal{S}})\} \\
|\forall x.A|_{\rho}^{\mathcal{S}} &\triangleq \bigcap_{f \in \mathbb{N}^{\mathcal{S}}} |A|_{\rho, x \mapsto f}^{\mathcal{S}} \\
|\forall X.A|_{\rho}^{\mathcal{S}} &\triangleq \bigcap_{F: \mathbb{N}^k \to \mathrm{SAT}} |A|_{\rho, X \mapsto F}^{\mathcal{S}} \\
|\exists x.A|_{\rho}^{\mathcal{S}} &\triangleq \bigcup_{f \in \mathbb{N}^{\mathcal{S}}} |A|_{\rho, x \mapsto f}^{\mathcal{S}} \\
|\exists X.A|_{\rho}^{\mathcal{S}} &\triangleq \bigcup_{F: \mathbb{N}^k \to \mathrm{SAT}} |A|_{\rho, X \mapsto F}^{\mathcal{S}}.
\end{align*}
$$

We write $(t; s) \Vdash A$ (resp. $t \Vdash_A A$) to denote that $(t; s) \in |A|^{\mathcal{S}}$ (resp. $\forall \mathfrak{s} \in \mathcal{S}. (t; \mathfrak{s}) \in |A|^{\mathcal{S}}$). Realizers of the type $t \Vdash A$ are called *universal*.

Observe that this stateful interpretation has the structure of a product of the interpretation given by Definition 3.2. The interpretation corresponding to a given state can thus be seen as a *slice* of this product. However, it is important to keep in mind that the *set* instruction still allows terms to change the value of the state, therefore the slices are not completely independent. We write $|A|_{\rho}^{\mathcal{S}}$ to denote the truth value $\{(t; \mathfrak{s}) \in |A|_{\rho}^{\mathcal{S}}\}$ in the slice induced by $\mathfrak{s}$.

We first verify that truth values are indeed saturated sets and that the interpretation validates the congruence rules.

**Proposition 4.6.** Let $A$ be a formula and $\rho$ a valuation closing $A$. Then $|A|_{\rho}^{\mathcal{S}} \in \mathbf{SAT}$.

*Proof.* By a straightforward induction on the structure of $A$. Observe for instance that the case $\mathrm{st}(f)$ follows from the definition and that the case $X(e_1, \dots, e_n)$ follows from the fact that, by definition, $\rho(X)$ takes values in $\mathbf{SAT}$. $\square$

By induction on the structure of $A$. The case $\mathrm{st}(f)$ is clear from the definition and the case $X(e_1, \dots, e_n)$ follows from the fact that, by definition, $\rho(X)$ takes values in $\mathbf{SAT}$.

$\underline{A \to B}$. Let $t, t'$ be two terms such that $(t'; s') \in |A \to B|_{\rho}^{\mathcal{S}}$ and $t \succ_{\mathfrak{s}'}^{s} t'$ for some states $\mathfrak{s}, \mathfrak{s}'$. Let $(u; s') \in |A|_{\rho}^{\mathcal{S}}$. We have that $t u \succ_{\mathfrak{s}'}^{s} t' u$, which by definition belongs to $|B|_{\rho}^{\mathcal{S}}$. We conclude the result by the induction hypothesis for $B$. The same proof applies to the case $\{\mathrm{Nat}(e)\} \mapsto A$.

$A_1 \wedge A_2$. Let $t, t'$ be two terms such that $(t'; s') \in |A_1 \wedge A_2|_{\rho}^{\mathcal{S}}$ and $t \succ_{\mathfrak{s}'}^{s} t'$ for some states $\mathfrak{s}, \mathfrak{s}'$. For any $i \in \{1, 2\}$, we have that $\pi_i(t) \succ_{\mathfrak{s}'}^{s} \pi_i(t')$, which by definition belongs to $|A_1|_{\rho}^{\mathcal{S}}$. We conclude the result by the induction hypothesis for $A_i$. The proof for the case $A_1 \vee A_2$ is analogous.
∀x.A. Let $t, t'$ be two terms such that $(t'; \mathfrak{s}') \in |\forall x.A|_{\rho}^{\mathfrak{G}}$ and $t \succ_{\mathfrak{s}'} t'$ for some state $\mathfrak{s}, \mathfrak{s}'$. By definition, for any $f \in \mathbb{N}^{\mathfrak{G}}$, it holds that $(t'; \mathfrak{s}') \in |A|_{\rho, x \mapsto f}^{\mathfrak{G}}$. Hence by the induction hypothesis for $A$, we get that $(t; \mathfrak{s}) \in |A|_{\rho, x \mapsto f}^{\mathfrak{G}}$. This being true for any $f \in \mathbb{N}^{\mathfrak{G}}$, we deduce that $(t; \mathfrak{s}) \in |\forall x.A|_{\rho}^{\mathfrak{G}}$. The cases for the other quantifiers are similar.

**Proposition 4.7.** If $A$ and $A'$ are two formulas of HA2 such that $A \cong A'$, then for all valuations $\rho$ closing both $A$ and $A'$ we have $|A|_{\rho}^{\mathfrak{G}} = |A'|_{\rho}^{\mathfrak{G}}$.

*Proof.* The proof, by induction on $A \cong A'$, is similar to the proof of Proposition 3.3. Congruence easily goes through by induction, and again we have

$$ \begin{align*} |(\exists x.A) \to B|_{\rho}^{\mathfrak{G}} &= \{(t; \mathfrak{s}) \in \Lambda \times \mathfrak{G} : \forall u.(u; \mathfrak{s}) \in |\exists x.A|_{\rho}^{\mathfrak{G}} \Rightarrow (t u; \mathfrak{s}) \in |B|_{\rho}^{\mathfrak{G}}\} \\ &= \{(t; \mathfrak{s}) \in \Lambda \times \mathfrak{G} : \forall u.(u; \mathfrak{s}) \in \bigcup_{n \in \mathbb{N}} |A|_{\rho, x \mapsto n} \Rightarrow (t u; \mathfrak{s}) \in |B|_{\rho}^{\mathfrak{G}}\} \\ &= \{(t; \mathfrak{s}) \in \Lambda \times \mathfrak{G} : \forall u.(\exists n.(u; \mathfrak{s}) \in |A|_{\rho, x \mapsto n}) \Rightarrow (t u; \mathfrak{s}) \in |B|_{\rho}^{\mathfrak{G}}\} \\ &= \{(t; \mathfrak{s}) \in \Lambda \times \mathfrak{G} : \forall u, n.((u; \mathfrak{s}) \in |A|_{\rho, x \mapsto n}) \Rightarrow (t u; \mathfrak{s}) \in |B|_{\rho}^{\mathfrak{G}})\} \\ &= \bigcap_{n \in \mathbb{N}} \{(t; \mathfrak{s}) : \forall u.(u; \mathfrak{s}) \in |A|_{\rho, x \mapsto n} \Rightarrow (t u; \mathfrak{s}) \in |B|_{\rho}^{\mathfrak{G}}\} \\ &= |\forall x.(A \to B)|_{\rho}^{\mathfrak{G}} \end{align*} $$

The proofs for second-order quantifiers and value restrictions are analogous.

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

In order to prove the adequacy theorem in this setting we need to adapt a few definitions.

**Definition 4.8.** Given a context $\Gamma$, a state $\mathfrak{s}$ and a valuation $\rho$ closing the formulas in $\Gamma$, we say that a substitution $\sigma$ realizes $\rho(\Gamma)$ in the state $\mathfrak{s}$ and write $(\sigma; \mathfrak{s}) \Vdash \rho(\Gamma)$ if $\mathrm{dom}(\rho(\Gamma)) \subseteq \mathrm{dom}(\sigma)$ and $(\sigma(x); \mathfrak{s}) \in |A|_{\rho}^{\mathfrak{G}}$, for every declaration $(x : A) \in \Gamma$.

**Definition 4.9.** We say that a typing judgement $\Gamma \vdash t : A$ is *adequate* w.r.t. a state $\mathfrak{s}$ in the stateful system if for any valuation $\rho$ closing $A$ and $\Gamma$ and any substitution $(\sigma; \mathfrak{s}) \Vdash \rho(\Gamma)$ we have $(\sigma(t); \mathfrak{s}) \in |\rho(A)|$. An inference rule is *adequate* w.r.t. a state $\mathfrak{s}$ if the adequacy (w.r.t. $\mathfrak{s}$) of all its premises implies the adequacy (w.r.t. $\mathfrak{s}$) of its conclusion.

We are now able to show that, with the exception of the $(\forall_E^2)/(\exists_I^2)$-rules, our logical rules are adequate. The $(\forall_E^2)/(\exists_I^2)$-rules are shown to be adequate, for internal formulas only, in Proposition 4.17. The status of natural numbers will be investigated in Section 5.1.

**Theorem 4.10 (Adequacy).** *The logical rules of Figure 1, except the $(\forall_E^2)/(\exists_I^2)$-rules, are adequate.*

*Proof.* The proof, by case analysis, is essentially the same as the usual adequacy proof for HA2, since none of the instructions involved in the typing rules allows to change the value of the state.

In each case, we write $\Gamma$ for the typing context, $\rho$ for a valuation closing all the considered formulas, $\mathfrak{s}$ for the considered state and $\sigma$ for a substitution such that $(\sigma; \mathfrak{s}) \Vdash \rho(\Gamma)$.

$(\mathrm{Ax}).$ Directly from the assumption that $(\sigma; \mathfrak{s}) \Vdash \rho(\Gamma)$.

$(\to_I).$ By assumption, for any substitution $\sigma'$ such that $(\sigma'; \mathfrak{s}) \Vdash \rho(\Gamma)$, $x : \rho(A)$, we have that $(\sigma(t); \mathfrak{s}) \in |B|_{\rho}^{\mathfrak{G}}$. We have to prove that $(\lambda x.\sigma(t); \mathfrak{s}) \in |A \to B|_{\rho}^{\mathfrak{G}}$. Let then $u$ be a term such that $(u; \mathfrak{s}) \in |A|_{\rho}^{\mathfrak{G}}$. By definition, we have $\lambda x.\sigma(t) u \stackrel{s}{\downarrow}^{\mathfrak{s}} \sigma(t)[u/x]$. Since $\sigma(t)[u/x] = (\sigma, x := u)(t)$ and $(\sigma, x := u; \mathfrak{s}) \Vdash \rho(\Gamma, x : A)$, we obtain $(\sigma(t)[u/x]; \mathfrak{s}) \in |B|_{\rho}^{\mathfrak{G}}$. We conclude that $(\lambda x.\sigma(t) u; \mathfrak{s}) \in |B|_{\rho}^{\mathfrak{G}}$ by anti-reduction.
(→<sub>E</sub>). By assumption, we have that (σ(t); s) ∈ |A → B|<sub>ρ</sub><sup>S</sup> and (σ(u); s) ∈ |A|<sub>ρ</sub><sup>S</sup>. By the definition of |A → B|<sub>ρ</sub><sup>S</sup>, we obtain that σ(tu) = σ(t) σ(u) ∈ |B|<sub>ρ</sub><sup>S</sup>.

(∧<sub>I</sub>). By assumption, (σ(t<sub>1</sub>); s) ∈ |A<sub>1</sub>|<sub>ρ</sub><sup>S</sup> and (σ(t<sub>2</sub>); s) ∈ |A<sub>2</sub>|<sub>ρ</sub><sup>S</sup>. For any i ∈ {1, 2} we have that π<sub>i</sub>(σ(t<sub>1</sub>, t<sub>2</sub>)) = π<sub>i</sub>(σ(t<sub>1</sub>), σ(t<sub>2</sub>)) s↓<sup>s</sup> σ(t<sub>i</sub>), where the latter belongs to |A<sub>i</sub>|<sub>ρ</sub><sup>S</sup>. Then, by anti-reduction π<sub>i</sub>(σ(t<sub>1</sub>, t<sub>2</sub>)) ∈ |A<sub>i</sub>|<sub>ρ</sub><sup>S</sup> and hence σ(t<sub>1</sub>, t<sub>2</sub>) ∈ |A<sub>1</sub> ∧ A<sub>2</sub>|<sub>ρ</sub><sup>S</sup>.

(∧<sup>1</sup><sub>E</sub>). By assumption, we have that (t; s) ∈ |A<sub>1</sub> ∧ A<sub>2</sub>|<sub>ρ</sub><sup>S</sup>, which entails by definition that (π<sub>1</sub>(t); s) ∈ |A<sub>1</sub>|<sub>ρ</sub><sup>S</sup>. The case (∧<sup>2</sup><sub>E</sub>) is similar.

(∃<sup>1</sup><sub>I</sub>). By assumption, there exists n ∈ N such that (t; s) ∈ |A[x := n]|<sub>ρ</sub><sup>S</sup> = |A|<sub>ρ, x ↦→ n*</sub>. The result then follows from the fact that |A|<sub>ρ, x ↦→ n*</sub> ⊆ ⋃<sub>f ∈ N<sup>S</sup></sub> |A|<sub>ρ, x ↦→ f</sub> = |∃x.A|<sub>ρ</sub><sup>S</sup>.

(∀<sup>1</sup><sub>E</sub>). By assumption, (t; s) ∈ ⋂<sub>f ∈ N<sup>S</sup></sub> |A|<sub>ρ, x ↦→ f</sub>. The result follows directly from the fact that ⋂<sub>f ∈ N<sup>S</sup></sub> |A|<sub>ρ, x ↦→ f</sub> ⊆ |A|<sub>ρ, x ↦→ n*</sub>.

(∀<sup>1</sup><sub>I</sub>). By assumption, (t; s) ∈ |A|<sub>ρ'</sub> for any valuation ρ' closing A which, since x does not occur in Γ, can freely map x to any individual in N<sup>S</sup>. In other words, (t; s) ∈ ⋂<sub>f ∈ N<sup>S</sup></sub> |A|<sub>ρ, x ↦→ f</sub>. The case for (�forall<sup>2</sup><sub>I</sub>) is similar.

(=). Directly from Proposition 4.7.

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

**Remark 4.11.** Let us explain why the (�forall<sup>2</sup><sub>E</sub>)-rule is not adequate in general (the same argument applies to the (�exists<sup>2</sup><sub>I</sub>)-rule). As emphasized at the beginning of this section, we interpret predicates by functions from N<sup>k</sup> to **SAT**, while the truth values of formulas may vary in the set of functions from (N<sup>S</sup>)<sup>k</sup> to **SAT**. Theorem 4.16 will make this more precise: internal formulas correspond to functions from N<sup>k</sup> to **SAT** while external formulas correspond to functions from (N<sup>S</sup>)<sup>k</sup> to **SAT**. Therefore, in general we cannot substitute a second-order variable by any formula. Indeed, in the second-order elimination rule (for universal quantifiers) variables can only be instantiated by internal formulas. Moreover, if the formula *B* that we want to substitute is a proposition (i.e. if its arity *k* is equal to 0), then the substitution is valid since the interpretations of internal and external formulas coincide. This means that we could have chosen to work with impredicative encodings of the conjunction (or other connectives) as in the Russell-Prawitz translation [Pra65]. Indeed, such an encoding relies on the use of propositions, which are thus compatible with the elimination rule:

$$A \wedge B \triangleq \forall X.(A \rightarrow B \rightarrow X) \rightarrow X.$$

**Remark 4.12.** We would like to attract the reader's attention to the fact that our realizability interpretation is grounded in the elimination rules for the connectives. While this choice may not be so meaningful in a pure intuitionistic setting, here the fact that our realizers may perform some effectful computations makes this choice relevant. Indeed, the other possibility would have been to require from a realizer of A ∧ B to be a term reducing to a pair of realizers, forcing the effectful computations to be done “right away”, which could in particular make the value of the state evolve. In turn, our definition delays such computations further, which allows us to reason within the same state before eventually reducing the term (and thus
performing the effect). This technicality turns out to be crucial in some proofs in the sequel, in particular for defining the realizer of LLPO<sup>st</sup> in Section 6.

We show that rec realizes a formula that emulates its former typing rule by using quantifiers relativized with a value restriction.

**Proposition 4.13.** We have rec $\Vdash \forall X.X(0) \to \forall^{\{\mathfrak{N}\}}x.(X(x) \to X(S(x))) \to \forall^{\{\mathfrak{N}\}}x.X(x)$.

*Proof.* Let $\mathcal{X}: \mathbb{N} \to \mathbf{SAT}$ be a predicate, $\mathfrak{s} \in \mathcal{S}$ be a state, $f \in \mathbb{N}^{\mathcal{S}}$ be a natural number, $u_0$ and $u_S$ be terms and $V$ be a value such that

- $(u_0; \mathfrak{s}) \in \mathcal{X}(0)$,

- $(u_S; \mathfrak{s}) \in |\forall^{\mathbb{N}}y.(X(y) \to X(S(y)))|_{\mathcal{X} \to \mathcal{X}}^{\mathcal{S}}$

- $(V; \mathfrak{s}) \in |\mathrm{Nat}(f)|^{\mathcal{S}}$.

The latter implies that $V = s^n 0$ where $n = f(\mathfrak{s})$. Besides, recall that by definition we have $|X(f)|_{\mathcal{X} \to \mathcal{X}}^{\mathcal{S}} = \mathcal{X}@\langle f \rangle = \{(t; \mathfrak{s}) \in \mathcal{X}(f(\mathfrak{s}))\} = \mathcal{X}(n)$. Let us prove, by induction on $n$, that $\mathrm{rec} \ u_0 \ u_S \ \overline{n} \in \mathcal{X}(n)$.

* If $n = 0$, then we have that $\mathrm{rec} \ u_0 \ u_S \ t^s \downarrow^s \mathrm{rec} \ u_0 \ u_S \ \overline{0}^s \downarrow^s \ u_0$, the result follows by anti-reduction from the hypothesis on $u_0$.

* If $n = S(m)$, then we have that $\mathrm{rec} \ u_0 \ u_S \ (\mathfrak{s} \overline{m})^s \downarrow^s \ u_S \ \overline{m} \ (\mathrm{rec} \ u_0 \ u_S \ \overline{m})$. By induction hypothesis, we have that $(\mathrm{rec} \ u_0 \ u_S \ \overline{m}; \mathfrak{s}) \in \mathcal{X}(m)$. The result thus follows (by anti-reduction) from the hypothesis on $u_S$. $\square$

**Remark 4.14.** Regarding the necessity of restricting the relativization of quantifiers to values, the proof of Proposition 4.13 is enlightening. Indeed, if instead of a value $V$ we were only given a term in $|\mathrm{Nat}(f)|_{\rho}^{\mathfrak{s}}$, by definition this term may change the value of the state, say to some $\mathfrak{s}'$, before reducing to the value of $f(\mathfrak{s}')$. This would break the proof since nothing is assumed on the realizers $u_0$ and $u_S$ in this new state $\mathfrak{s}'$.

**4.3. Glueing.** An important property of our interpretation (which also reflects a similar property in the Lightstone-Robinson construction) is that the interpretation of internal formulas can be decomposed as the product of its slices (Theorem 4.16). In other words, internal formulas can only access information in the current state. In particular, and as expected, this means that it is impossible to express standardness by means of internal formulas. To state this formally, we first define the restriction of formulas and truth values with respect to a slice.

**Definition 4.15.** Given an internal formula $A$, we define $\overline{A}^5$ as the formula whose individuals are all applied in $\mathfrak{s}$. Formally, it amounts to replacing each individual by the standard individual with which it coincides in the state $\mathfrak{s}$:

$$ \begin{array}{ccc} \overline{X(e_1, \dots, e_k)}^5 \triangleq X((e_1(\mathfrak{s}))^*, \dots, (e_k(\mathfrak{s}))^*) & \mid & \overline{A \wedge B}^5 \triangleq \overline{A}^5 \wedge \overline{B}^5 \\ \overline{A} \to \overline{B}^5 \triangleq \overline{A}^5 \to \overline{B}^5 & & \overline{\exists} x. \overline{A}^5 \triangleq \exists x. \overline{A}^5 \\ \overline{\{\mathrm{Nat}(e)\}} \mapsto \overline{B}^5 \triangleq \{\mathrm{Nat}((e(\mathfrak{s}))^*)\} \mapsto \overline{B}^5 & & \overline{\forall} x. \overline{A}^5 \triangleq \forall x. \overline{A}^5 \\ & & \exists x. \overline{A}^5 \triangleq \exists x. \overline{A}^5 \end{array} $$

**Theorem 4.16 (Glueing).** For any internal formula $A$ and valuation $\rho$ closing $A$, we have that $(t; \mathfrak{s}) \in |A|_{\rho}^{\mathcal{S}} \Leftrightarrow t \in |\overline{A}^5|_{\rho}^{\mathfrak{s}}$.

*Proof.* The proof is by induction on the structure of $A$.
$X(e_1, ..., e_k)$. By Definition 4.2, we have

$$ (t; \mathfrak{s}) \in |X(e_1, ..., e_k)|_{\rho}^{\mathfrak{s}} \iff (t; \mathfrak{s}) \in \rho(X)@([\![e_1]\!]_{\rho}, ..., [\![e_k]\!]_{\rho}) \\ \iff t \in (\rho(X))_{\mathfrak{s}}([\![e_1]\!]_{\rho}(\mathfrak{s}), ..., [\![e_k]\!]_{\rho}(\mathfrak{s})) \\ \iff t \in |X((e_1(\mathfrak{s}))^*, ..., (e_k(\mathfrak{s}))^*)|_{\rho}^{\mathfrak{s}} \iff t \in |\overline{X(e_1, ..., e_k)}|_{\rho}^{\mathfrak{s}}. $$

$A \to B$. We have

$$ (t; \mathfrak{s}) \in |A \to B|_{\rho}^{\mathfrak{S}} \iff \forall (u; \mathfrak{s}) \in |A|_{\rho}^{\mathfrak{S}}. (t u; \mathfrak{s}) \in |B|_{\rho}^{\mathfrak{S}} \\ \qquad \stackrel{(\text{HI})}{\iff} \forall u \in |\overline{A}|_{\rho}^{\mathfrak{s}}. t u \in |\overline{B}|_{\rho}^{\mathfrak{s}} \iff t \in |\overline{A \to B}|_{\rho}^{\mathfrak{s}}. $$

$\{\text{Nat}(e)\} \mapsto B$. The proof is similar to the case $A \to B$.

$$ (t; \mathfrak{s}) \in |\{\text{Nat}(e)\} \to B|_{\rho}^{\mathfrak{S}} \iff (t \bar{n}; \mathfrak{s}) \in |B|_{\rho}^{\mathfrak{S}} \text{ where } n = e(\mathfrak{s}) \\ \qquad \stackrel{(\text{HI})}{\iff} (t \bar{n}; \mathfrak{s}) \in |\overline{B}|_{\rho}^{\mathfrak{s}} \text{ where } n = e(\mathfrak{s}) \iff t \in |\{\text{Nat}(e)\} \to B|_{\rho}^{\mathfrak{s}}. $$

$A_1 \wedge A_2$. We have

$$ (t; \mathfrak{s}) \in |A_1 \wedge A_2|_{\rho}^{\mathfrak{S}} \iff (\pi_1(t); \mathfrak{s}) \in |A_1|_{\rho}^{\mathfrak{S}} \wedge (\pi_2(t); \mathfrak{s}) \in |A_2|_{\rho}^{\mathfrak{S}} \\ \qquad \stackrel{(\text{HI})}{\iff} (\pi_1(t); \mathfrak{s}) \in |\overline{A_1}|_{\rho}^{\mathfrak{s}} \wedge (\pi_2(t); \mathfrak{s}) \in |\overline{A_2}|_{\rho}^{\mathfrak{S}} \\ \qquad \iff (t; \mathfrak{s}) \in |\overline{A_1} \wedge \overline{A_2}|_{\rho}^{\mathfrak{S}}. $$

$\forall x.A$. We have

$$ (t; \mathfrak{s}) \in |\forall x.A|_{\rho}^{\mathfrak{S}} \iff \forall f \in \mathbb{N}^{\mathfrak{S}}. (t; \mathfrak{s}) \in |A|_{\rho}^{\mathfrak{S}} \stackrel{(\text{HI})}{\iff} \forall f \in \mathbb{N}^{\mathfrak{S}}. t \in |\overline{A}|_{\rho}^{\mathfrak{s}} \iff t \in |\overline{\forall x.A}|_{\rho}^{\mathfrak{s}}. $$

$\exists x.A$. We have

$$ (t; \mathfrak{s}) \in |\exists x.A|_{\rho}^{\mathfrak{S}} \iff \exists f \in \mathbb{N}^{\mathfrak{S}}. (t; \mathfrak{s}) \in |A|_{\rho}^{\mathfrak{S}} \stackrel{(\text{HI})}{\iff} \exists f \in \mathbb{N}^{\mathfrak{S}}. t \in |\overline{A}|_{\rho}^{\mathfrak{s}} \iff t \in |\overline{\exists x.A}|_{\rho}^{\mathfrak{s}}. $$

The cases of the second-order quantifiers are similar to the corresponding first-order quantifiers. $\square$

Let $B(x)$ be a formula whose only free variable is $x$, and $\rho$ a valuation closing $B$. In general, the function $\mathcal{F}_B$ that associates to any individual $f$ the truth value $|B(f)|_{\rho}^{\mathfrak{S}}$ is a function from $\mathbb{N}^{\mathfrak{S}}$ to **SAT**. If $B$ is internal, by the glueing theorem, to determine $\mathcal{F}_B$ it is enough to know its value for standard individuals. This means that we only need to know a function from $\mathbb{N}$ to **SAT**. As such, we can now formally state the intuition developed in Remark 4.11.

**Proposition 4.17.** The elimination rule for the 2nd-order universal quantification and the introduction rule for the 2nd-order existential quantification

$$ \frac{\Gamma \vdash t : \forall X.A}{\Gamma \vdash t : A[X(x_1, ..., x_k) := B]} \stackrel{(\forall E^2)}{\Rightarrow} \frac{\Gamma \vdash t : A[X(x_1, ..., x_n) := B]}{\Gamma \vdash t : \exists X.A} \stackrel{(\exists I^2)}{\Rightarrow} $$

are adequate for any internal formula $B$ whose only free variables are $(x_1, ..., x_k)$.
**Proof.** This essentially follows from the glueing theorem and Definition 4.2. Indeed, recall that by definition we have $|\forall X.A|_{\rho}^{\mathcal{S}} = \bigcap_{F:N^k \to \mathbf{SAT}} |A|_{\rho, X \mapsto F}^{\mathcal{S}}$. Let us define the following function from $N^k$ to **SAT**:

$$ \mathcal{F} : (n_1, \dots, n_k) \mapsto |B[x_1 := n_1^*, \dots, x_k := n_k^*]|_{\rho}^{\mathcal{S}} $$

We can prove by an easy induction on $A$ that $|A|_{\rho, X \mapsto \mathcal{F}}^{\mathcal{S}} = |A[X(x_1, \dots, x_k) := B]|_{\rho}^{\mathcal{S}}$, from which the proposition follows trivially. The only interesting case is when $A \equiv X(x_1, \dots, x_n)$. Let us write $f_1, \dots, f_k$ for $[[\rho(x_1)], \dots, [[\rho(x_k)]]$. We have:

$$
\begin{align*}
|X(x_1, \dots, x_n)|_{\rho, X \mapsto \mathcal{F}}^{\mathcal{S}}
  &= \mathcal{F}@(f_1, \dots, f_k) \\
  &= \{(t; \mathfrak{s}) : t \in \mathcal{F}_{\mathfrak{s}}(f_1(\mathfrak{s}), \dots, f_k(\mathfrak{s}))\} \tag{by Def. 4.2} \\
  &= \bigcup_{\mathfrak{s} \in \mathcal{S}} \mathcal{F}_{\mathfrak{s}}(f_1(\mathfrak{s}), \dots, f_k(\mathfrak{s})) \times \{\mathfrak{s}\} \\
  &= \bigcup_{\mathfrak{s} \in \mathcal{S}} |B[x_1 := f_1, \dots, x_k := f_k]|_{\rho}^{\mathcal{S}} \times \{\mathfrak{s}\} \tag{by def. of $\mathcal{F}$} \\
  &= |B[x_1 := f_1, \dots, x_k := f_k]|_{\rho}^{\mathcal{S}} = |B|_{\rho}^{\mathcal{S}} \tag{by Prop. 4.16}
\end{align*}
$$

□

**Remark 4.18.** Observe that external formulas such as $\mathrm{st}(x) \to \bot$ cannot be defined by glueing. Consider for instance a nonstandard element $\tau$. Then $|\mathrm{st}(\tau) \to \bot|^{\mathcal{S}} = \Lambda \times \mathcal{S}$, while for any state $\mathfrak{s} \in \mathcal{S}$ we have $|\mathrm{st}(\tau) \to \bot|^{\mathfrak{s}} = |\mathrm{st}(\tau(\mathfrak{s})^*) \to \bot|^{\mathfrak{s}} = |\top \to \bot|^{\mathfrak{s}} = \emptyset$.

It is well-known that the comprehension scheme $CA_B \triangleq \exists X.\forall x.(X(x) \Leftrightarrow B)$ is a logical consequence of the elimination principle $Elim_A^B \triangleq (\forall X.A) \Rightarrow A[X(x) := B]$ (by taking $A = \exists Y.\forall x.(Y(x) \Leftrightarrow X(x)))$. Since we have the $(\forall_E^2)$-rule restricted to internal formulas $B$, the comprehension scheme is also valid for these formulas. In particular, this implies Standardization for internal formulas, i.e. for $B$ an internal formula, the following holds

$$ \forall^{\mathrm{st}} X. \exists^{\mathrm{st}} Y. \forall^{\mathrm{st}} z. (Y(z) \Leftrightarrow X(z) \wedge B(z)). $$

Of course, the comprehension scheme does not hold for external formulas, so the relativization on the quantifiers in Standardization is in this sense necessary. We will come back to Standardization in Section 7.1.

**4.4. The induced evidenced frame.** Before studying the properties of this interpretation, we shall connect it with the usual algebraic tools to deal with realizability interpretation, in order to better emphasize its structure and peculiarities. In recent work, Cohen et al. have been introducing a new framework to capture the algebraic structure of realizability interpretations, which they named *evidenced frames* [CMT21]. These have the benefit of being generic enough to easily encompass effectful interpretation, while uniformly inducing triposes (and thus toposes), hence a model of higher-order logic. We show here how our interpretation fits the picture, hinting in particular at the possibility to extend our interpretation to deal with higher-order logic (which is out of the scope of this paper, as here we want to focus on the second-order fragment only).

We start by recalling the definition of evidenced frame.

**Definition 4.19 ([CMT21]).** An *evidenced frame* is a triple $(\Phi, E, \cdot \to \cdot)$, where $\Phi$ is a set of propositions, $E$ is a collection of evidence, and $\phi_1 \xrightarrow{e} \phi_2$ is a ternary evidence relation on $\Phi \times E \times \Phi$, along with the following:

*Reflexivity:* There exists evidence $e_{id} \in E$:
$$ - \forall \phi. \phi \xrightarrow{e_{\mathrm{id}}} \phi $$

*Transitivity:* There exists an operator $\cdot; \cdot \in E \times E \to E$:

$$ - \forall \phi_1, \phi_2, \phi_3, e, e'. \phi_1 \xrightarrow{e} \phi_2 \wedge \phi_2 \xrightarrow{e'} \phi_3 \implies \phi_1 \xrightarrow{e; e'} \phi_3 $$

*Top:* A proposition $\top \in \Phi$ such that there exists evidence $e_{\top} \in E$:

$$ - \forall \phi. \phi \xrightarrow{e_{\top}} \top $$

*Conjunction:* An operator $\wedge \in \Phi \times \Phi \to \Phi$ such that there exists evidence $e_{\mathrm{fst}}, e_{\mathrm{snd}} \in E$ and an operator $\langle \cdot, \cdot \rangle \in E \times E \to E$:

$$ - \forall \phi_1, \phi_2. \phi_1 \wedge \phi_2 \xrightarrow{e_{\mathrm{fst}}} \phi_1 \qquad - \forall \phi, \phi_1, \phi_2, e_1, e_2. \phi \xrightarrow{e_1} \phi_1 \wedge \phi \xrightarrow{e_2} \phi_2 \implies \phi \xrightarrow{\langle e_1, e_2 \rangle} \phi_1 \wedge \phi_2 $$

$$ - \forall \phi_1, \phi_2. \phi_1 \wedge \phi_2 \xrightarrow{e_{\mathrm{snd}}} \phi_2 $$

*Universal Implication:* An operator $\supset \in \Phi \times \mathcal{P}(\Phi) \to \Phi$ such that there exists an operator $\lambda \in E \to E$ and evidence $e_{\mathrm{eval}} \in E$:

$$ - \forall \phi_1, \phi_2, \vec{\phi}, e. (\forall \phi \in \vec{\phi}. \phi_1 \wedge \phi_2 \xrightarrow{e} \phi) \implies \phi_1 \xrightarrow{\lambda e} \phi_2 \supset \vec{\phi} $$

$$ - \forall \phi_1, \vec{\phi}, \phi \in \vec{\phi}. (\phi_1 \supset \vec{\phi}) \wedge \phi_1 \xrightarrow{e_{\mathrm{eval}}} \phi $$

The definition of the evidenced frame induced by our stateful interpretation better highlights its core structure. First, as shown by the interpretation of second-order variables, propositions are defined as truth values, that is as saturated sets of terms-with-states. Evidences, in turn, are defined as universal realizers, i.e. $\lambda$-terms, with the corresponding evidence relation

$$ S_1 \xrightarrow{t} S_2 \triangleq t \Vdash \forall (u; \mathfrak{s}) \in S_1.(t u; \mathfrak{s}) \in S_2 \qquad (S_1, S_2 \in \mathbf{SAT}, t \in \Lambda) $$

**Proposition 4.20.** *The tuple (SAT, $\Lambda$, $\cdot \to \cdot$) defines an evidenced frame.*

*Proof.* We give the evidence and constructors on propositions for each case. We mostly follow the realizability interpretation given in Definition 4.5

*Reflexivity:* It is clear that $e_{\mathrm{id}} \triangleq \lambda x.x \Vdash S \to S$ for any $S \in \mathbf{SAT}$.

*Transitivity:* For any $S_1, S_2, S_3 \in \mathbf{SAT}$ if $t_1 \Vdash S_1 \to S_2$ and $t_2 \Vdash S_2 \to S_3$, it is clear that $t_1; t_2 \triangleq \lambda x.t_2 (t_1 x) \Vdash S_1 \to S_3$.

*Top:* Let $\top \triangleq \Lambda \times \mathfrak{G} \in \mathbf{SAT}$. Then we have $e_{\top} \triangleq \lambda x.x \Vdash S \to \top$ for any $S \in \mathbf{SAT}$.

*Conjunction:* Let $S_1 \wedge S_2 \triangleq \{(t; \mathfrak{s}) \in \Lambda \times \mathfrak{G} : (\pi_1(t); \mathfrak{s}) \in S_1 \wedge (\pi_2(t); \mathfrak{s}) \in S_2\}$ for $S_1, S_2 \in \mathbf{SAT}$. Then it is then straightforward to check that $\langle e_1, e_2 \rangle \triangleq \lambda x.(e_1 x, e_2 x)$, where $e_{\mathrm{fst}} \triangleq \pi_1, e_{\mathrm{snd}} \triangleq \pi_2$ define the expected evidences.

*Universal Implication:* For $S_1 \in \mathbf{SAT}$ and $\vec{S} \in \mathcal{P}(\mathbf{SAT})$, we define the implication of propositions by $S_1 \supset \vec{S} \triangleq \{(t; \mathfrak{s}) \in \Lambda \times \mathfrak{G} : \forall u.((u; \mathfrak{s}) \in S_1 \Rightarrow (t u; \mathfrak{s}) \in \bigcap_{S \in \vec{S}} S)\}$. Let $\lambda e \triangleq \lambda xy.e(x, y)$ and $e_{\mathrm{eval}} \triangleq \lambda x.(\pi_1(x))(\pi_2(x))$. Let $S_1, S_2 \in \mathbf{SAT}$ and $\vec{S} \in \mathcal{P}(\mathbf{SAT})$ be saturated sets. It is straightforward to show that $e_{\mathrm{eval}} \Vdash (S_1 \supset \vec{S}) \wedge S_1 \to S$ for any $S \in \vec{S}$. We prove that if $e \in \Lambda$ is such that $(\forall S \in \vec{S}. e \Vdash S_1 \wedge S_2 \to S)$ then $\lambda e \Vdash S_1 \to (S_2 \supset \vec{S})$. Let $(t_1; \mathfrak{s}) \in S_1$, then $\lambda e t_1 \mathfrak{s} \downarrow^s \lambda y.e(x, y)$. Clearly, if $(t_2; \mathfrak{s}) \in S_2$, $\lambda y.e(x, y) t_2 \mathfrak{s} \downarrow^s e (t_1, t_2)$. Since for any $S \in \vec{S}$ the last term belongs to $S$, we can conclude by anti-reduction that $\lambda e \Vdash S_1 \to (S_2 \supset \vec{S})$. $\square$

Proposition 4.20 implies, in particular, that our interpretation also induces a tripos and a topos, by following the method described in [CMT21]. In the following sections, we pay attention to nonstandard reasoning principles for which we can define universal realizers, as these are the evidences for our interpretation (as shown by Proposition 4.20).
## 5. NONSTANDARD PRINCIPLES IN REALIZABILITY WITH SLICES

**5.1. Natural numbers.** In Section 4, we considered a setting with a value restricted variant of the Nat(·) predicate. Nonetheless, we can still assert that an expression is a natural number through the formula

$$ \mathrm{Nat}'(e) \triangleq \forall X. (\{\mathrm{Nat}(e)\} \mapsto X) \rightarrow X. $$

As seen below, realizers of this formula will give access to the expected computations for natural numbers.

**Remark 5.1.** Observe that the language of HA2 does not express the existence of specific nonstandard elements, e.g. $\delta$ is not in the language. However, to refer to some nonstandard element $\tau$, we can always consider a valuation that maps a variable $x$ to $\tau$. With abuse of notation, in the remainder of this paper, we will write nonstandard elements directly in formulas as if they were in the language. Also, we will use the notation $\dagger$ to refer to an arbitrary $\lambda$-term with no further assumption.

Using an argument similar to Proposition 3.12, one can show that for any individual $f \in \mathbb{N}^{\mathcal{G}}$, if $t$ is a term such that $(t; \mathfrak{s}) \in |\mathrm{Nat}'(f)|^{\mathcal{G}}$, then one can actually compute out of $t$ (without changing the value of the state) the value of $f(\mathfrak{s}) \in \mathbb{N}$. In other words, $t$ is an effect-free term producing $\overline{f}(\mathfrak{s})$. This is to be compared with $\mathrm{Nat}(f)$, for which the requirement for its truth value to be saturated would have entailed its interpretation to reduce to a natural number $f(\mathfrak{s}')$ in a possibly different state.

**Proposition 5.2.** Let $f \in \mathbb{N}^{\mathcal{G}}$ and $\mathfrak{s} \in \mathcal{G}$. If $t$ is a term such that $(t; \mathfrak{s}) \in |\mathrm{Nat}'(f)|^{\mathcal{G}}$, then $t \lambda x.x^s \downarrow^s \overline{n}$, where $n = f(\mathfrak{s})$.

*Proof.* Let us define $\mathbb{X} \triangleq \{(t; \mathfrak{s}') : t^s \downarrow^{s'} \mathfrak{s} \overline{n}\}$. This set is clearly saturated, and it is easy to see that $(\lambda x.x; \mathfrak{s}) \in |\{\mathrm{Nat}(f)\} \mapsto \mathbb{X}|^{\mathcal{G}}$ (since $\lambda x.x \overline{n}^s \downarrow^s \overline{n}$). Therefore, we have that $t \in |(\{\mathrm{Nat}(f)\} \mapsto \mathbb{X}) \rightarrow \mathbb{X}|^{\mathcal{G}}$ and then $(t \lambda x.x; \mathfrak{s}) \in \mathbb{X}$, that is $t \lambda x.x^s \downarrow^s \overline{n}$. $\square$

We now show that (by-value) natural numbers, i.e. $\mathrm{Nat}'$, contain 0, and are closed under the successor and recursion for internal formulas.

**Proposition 5.3.** Let A be an internal formula. We have

(1) $\lambda x.x 0 \Vdash \mathrm{Nat}'(0)$

(2) $\lambda xy.y(\mathfrak{s}x) \Vdash \forall^{\mathbb{N}} x. \mathrm{Nat}'(S(x))$

(3) $\mathrm{rec} \Vdash A(0) \rightarrow (\forall^{\mathbb{N}} y.(A(y) \rightarrow A(Sy))) \rightarrow \forall^{\mathbb{N}} x.A(x)$

*Proof.* Easy realizability proofs by anti-reduction.

(1) Follows from the definition of $\mathrm{Nat}'(0)$: if $\mathbb{X} \in \mathbf{SAT}$ is a saturated set, $\mathfrak{s}$ a state and $t$ a term such that $(t; \mathfrak{s}) \in |\{\mathrm{Nat}(0)\} \mapsto \mathbb{X}|^{\mathcal{G}}$, we have $(\lambda x.x 0) t^s \downarrow^s t 0 \in \mathbb{X}$. Since $\mathbb{X}$ is saturated, we conclude by anti-reduction.

(2) Let $f \in \mathbb{N}^{\mathcal{G}}$, $\mathbb{X}$ be a saturated set, $\mathfrak{s}$ be a state and $t$ be a term such that $(t; \mathfrak{s}) \in |\{\mathrm{Nat}(Sf)\} \mapsto \mathbb{X}|^{\mathcal{G}}$. Let us write $n \triangleq f(\mathfrak{s})$. Then $(\lambda xy.y(\mathfrak{s}x)) \overline{n}^t \downarrow^s t(\mathfrak{s}\overline{n})$. Since $\mathfrak{s}\overline{n} = \overline{n} + 1 = \overline{S(f)(\mathfrak{s})}$, we get that $t(\mathfrak{s}\overline{n}) \in \mathbb{X}$ and we conclude by anti-reduction.

(3) Directly from Propositions 4.13 and 4.17. $\square$
The interpretation now witnesses the existence of new elements. The canonical example is the *diagonal*, i.e. the function $\delta: n \mapsto n$. Indeed, the diagonal is a nonstandard natural number which is realized by the *get* instruction. We first show a lemma concerning the storage operator *T* (from Definition 3.13) in this new context.

**Lemma 5.4.** Let $\mathfrak{s} \in \mathfrak{S}$ and $t, u$ be terms.

(1) For any $n \in \mathbb{N}$, if $u^s \downarrow^s \bar{n}$, then $Ttu^s \downarrow^s t\bar{n}$.

(2) For any $f \in \mathbb{N}^{\mathfrak{S}}$, if $u^s \downarrow^s \overline{f(\mathfrak{s})}$ and $(t; \mathfrak{s}) \in |\forall^{\mathbb{N}}x.A(x)|^{\mathfrak{S}}$, then $Ttu \in |A(f)|^{\mathfrak{S}}$.

*Proof.* The first part is an easy induction on $n$, and the second part follows from the first by anti-reduction.

(1) By induction on $n$.

* If $n = 0$, we have

$$ 
\begin{align*}
Ttu^s \downarrow^s \operatorname{rec}(\lambda y.y 0) (\lambda xyz.y (\lambda x.z(sx))) ut \\
\qquad s \downarrow^s \operatorname{rec}(\lambda y.y 0) (\lambda xyz.y (\lambda x.z(sx))) 0t \\
\qquad s \downarrow^s (\lambda y.y 0) t s \downarrow^s t 0.
\end{align*}
$$

* If $\mathfrak{s} = S(n)$, we have

$$ 
\begin{align*}
Ttu^s \downarrow^s \operatorname{rec}(\lambda y.y 0) (\lambda xyz.y (\lambda x.z(sx))) ut \\
\qquad s \downarrow^s \operatorname{rec}(\lambda y.y 0) (\lambda xyz.y (\lambda x.z(sx))) s\bar{n}t \\
\qquad s \downarrow^s (\lambda xyz.y (\lambda x.z(sx))) \bar{n} (\operatorname{rec}(\lambda y.y 0) (\lambda xyz.y (\lambda x.z(sx)))) \bar{n}) t \\
\qquad s \downarrow^s (\operatorname{rec}(\lambda y.y 0) (\lambda xyz.y (\lambda x.z(sx)))) \bar{n} (\lambda x.t(sx)) \\
\qquad s \downarrow^s (\lambda x.t(sx)) \bar{n} s \downarrow^s t s\bar{n},
\end{align*}
$$

where we used the induction hypothesis to obtain the penultimate reduction.

(2) By definition, it holds that $(t; \mathfrak{s}) \in |\{\operatorname{Nat}(f)\} \mapsto A(f)|^{\mathfrak{S}}$. By part 1, we obtain that $Ttu^s \downarrow^s \overline{f(s)}$, hence the result follows by anti-reduction. $\square$

**Proposition 5.5 (ENS₀).** We have that

(1) $\vdash \mathbf{||\vdash} \neg \operatorname{st}(\delta)$

(2) $\vdash \mathbf{||\vdash} \exists x. \neg \operatorname{st}(x)$

(3) $\lambda x.T x \ \mathbf{get} \ \mathbf{||\vdash} \ \operatorname{Nat}'(\delta)$

(4) $\lambda x.T x \ \mathbf{get} \ \vdash \mathbf{||\vdash} \ \exists^{\mathbb{N}} x. \neg \operatorname{st}(x)$

*Proof.* (1) By definition, $|\operatorname{st}(\delta)| \mapsto \perp|^{\mathfrak{S}} = \Lambda \times \mathfrak{S}$, which entails the result.

(2) Obvious from part 1.

(3) Follows from the fact that $\delta(\mathfrak{s}) = \mathfrak{s}$ and that by part 1 of Lemma 5.4, for any $t$.

$$ (\lambda x.T x \ \mathbf{get}) t^s \downarrow^s Tt \ \mathbf{get}^s t \bar{s} $$

(4) The proof is similar to the proof of Proposition 3.14. Let $\mathbb{X} \in \mathbf{SAT}$ be a predicate and $u$ be a term such that $(u; \mathfrak{s}) \in |\forall^{\mathbb{N}}x. \neg \operatorname{st}(x) \to \mathbb{X}|^{\mathfrak{S}}$. In particular, the latter implies that for any term $t$, it holds that $(u \mathfrak{s} t; \mathfrak{s}) \in \mathbb{X}$. Since $\mathbb{X}$ is saturated, the result then follows from the fact that $Tu \ \mathbf{get}^s t^s \downarrow^s u \bar{s} t$ which is a consequence of part 1 of Lemma 5.4. $\square$

Part 2 in Proposition 5.5 is sometimes referred to as the ENS₀ (existence of nonstandard elements) principle (e.g. in [BBS12]). As a consequence of Proposition 4.17, Leibniz equality is only compatible with the $(\forall_E^2)$-rule restricted to internal formulas. In our setting, this encoding only reflects equality in the current state, i.e. a local knowledge of individuals
(slice by slice), while the usual notion of equality (for $\mathbb{N}^{\mathfrak{S}}$) requires a global knowledge (on all the slices). If $A(x)$ is an external formula, we cannot hope to have an internal definition of equality such that its elimination principle $x = y \to A(x) \to A(y)$ is valid.

**Example 5.6.** Consider an individual $f$, equal to 1 everywhere except for some state $\mathfrak{s}_0$ where it is equal to 0.

For any state $\mathfrak{s} \neq \mathfrak{s}_0$, we have $(\lambda x.x; \mathfrak{s}) \Vdash 1^* = f$. However, if we consider the formula $A(x) \triangleq (\mathrm{st}(x) \to \bot) \to \bot$, then, for $\mathfrak{s} \neq \mathfrak{s}_0$, we have $(\lambda x.x^\dagger; \mathfrak{s}) \in |A(1)|$ and $|A(f)|_\mathfrak{s} = |(\bot \to \top) \to \bot|_\mathfrak{s}$. Thus, if $(t; \mathfrak{s})$ is a realizer of

$$ \forall Z.(Z(1^*) \to Z(f)) \to A(1^*) \to A(f), $$

we immediately get that $(t(\lambda x.x)(\lambda x.x)(\lambda x.x^\dagger); \mathfrak{s}) \Vdash \bot$.

Nonetheless, the elimination of Leibniz equality is realizable for standard individuals or for internal formulas.

**Proposition 5.7.** Let $f$ and $g$ be individuals in $\mathbb{N}^{\mathfrak{S}}$ and let $A(x)$ be a formula. Then

(1) $\lambda xyz.z \Vdash \mathrm{st}(f) \to \mathrm{st}(g) \to (\forall Z.(Z(f) \to Z(g))) \to A(f) \to A(g)$

(2) If $A(x)$ is internal, then $\lambda x.x \Vdash (\forall Z.(Z(f) \to Z(g))) \to A(f) \to A(g)$

*Proof.* (1) If either $f$ or $g$ is not standard, the result is trivial. Assume that $f$ and $g$ are standard. The case $f = g$ is trivial, and if $f \neq g$, we have $|(\forall Z.(Z(f) \mapsto Z(g)))|^{\mathfrak{S}} = |\top \mapsto \bot|^{\mathfrak{S}}$.

(2) The result easily follows from Proposition 4.17. $\square$

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

**5.2. Nonstandard reasoning principles.** In this section, we prove some properties which are usual in frameworks that use nonstandard analysis: Transfer, Overspill, External Induction, Idealization, etc.

Theorem 5.8 below indicates that the Transfer property (for internal formulas) is devoid of computational content. This is a somewhat reassuring fact: properties that are true for standard individuals are automatically true for all individuals.

**Theorem 5.8 (Transfer).** For any internal formula $A$ we have:

(1) $\bigcap_{f \in \mathbb{N}^{\mathfrak{S}}} |A|_{x \to f}^{\mathfrak{S}} = \bigcap_{n \in \mathbb{N}} |A|_{x \to n^*}^{\mathfrak{S}}$

(2) $\lambda xy.x \Vdash \forall x.A(x) \to \forall^{\mathrm{st}}x.A(x)$

(3) $\lambda x.x^\dagger \Vdash \forall^{\mathrm{st}}x.A(x) \to \forall x.A(x)$

(4) $\bigcup_{f \in \mathbb{N}^{\mathfrak{S}}} |A|_{x \to f}^{\mathfrak{S}} = \bigcup_{n \in \mathbb{N}} |A|_{x \to n^*}^{\mathfrak{S}}$

(5) $\lambda x.(\dagger, x) \Vdash \exists x.A(x) \to \exists^{\mathrm{st}}x.A(x)$

(6) $\lambda x.\pi_2(x) \Vdash \exists^{\mathrm{st}}x.A(x) \to \exists x.A(x)$

*Proof.* Parts 1 and 4 follow from the glueing theorem. Indeed, we have:

$$ \bigcap_{f \in \mathbb{N}^{\mathfrak{S}}} |A|_{x \to f}^{\mathfrak{S}} = \bigcap_{f \in \mathbb{N}^{\mathfrak{S}}} \bigcup_{s \in \mathfrak{S}} |\overline{A}^s|_{x \to f}^{\mathfrak{S}} \times \{\mathfrak{s}\} \quad \text{(by glueing)} $$

$$ = \bigcap_{f \in \mathbb{N}^{\mathfrak{S}}} \bigcup_{s \in \mathfrak{S}} |\overline{A}^s|_{x \to (f(\mathfrak{s}))^*}^{\mathfrak{S}} \times \{\mathfrak{s}\} \quad \text{(by def. of $\overline{\cdot}^s$)} $$

$$ = \bigcap_{n \in \mathbb{N}} \bigcup_{s \in \mathfrak{S}} |\overline{A}^s|_{x \to n^*}^{\mathfrak{S}} \times \{\mathfrak{s}\} $$

$$ = \bigcap_{n \in \mathbb{N}} |A|_{x \to n^*}^{\mathfrak{S}} \quad \text{(by glueing)} $$

The proof for part 4 is analogous.

Parts 2 and 3 (resp. 5, 6) are direct consequences of the first (resp. fourth) part. For instance, for part 3, let $\mathfrak{s}$ be a state and $u$ be a term such that $(u; \mathfrak{s}) \in |\forall^{\mathrm{st}}x.A(x)|^{\mathfrak{S}}$.
Recalling that $|\mathrm{st}(n^*)|^\mathfrak{G} = \Lambda \times \mathfrak{G}$ for any $n \in \mathbb{N}$, we have:

$$
\begin{align*}
\forall f \in \mathbb{N}^{\mathfrak{G}}, v \in \Lambda.(v; \mathfrak{s}) \in |\mathrm{st}(f)|^{\mathfrak{G}} &\Rightarrow (uv; \mathfrak{s}) \in |A(x)|^{\mathfrak{G}}_{x \to f} \\
&\Rightarrow \forall n \in \mathbb{N}, v \in \Lambda.(uv; \mathfrak{s}) \in |A(x)|^{\mathfrak{G}}_{x \to n^*} \\
&\Rightarrow \forall v \in \Lambda.(uv; \mathfrak{s}) \in \bigcap_{n \in \mathbb{N}} |A(x)|^{\mathfrak{G}}_{x \to n^*} \\
&\Rightarrow \forall v \in \Lambda.(uv; \mathfrak{s}) \in \bigcap_{f \in \mathbb{N}^S} |A(x)|^{\mathfrak{G}}_{x \to f}
\end{align*}
$$

where the last implication is obtained using part 1. In particular, $(ut; \mathfrak{s})$ belongs to $|\forall x.A(x)|^{\mathfrak{G}}$
and by anti-reduction, so does $((\lambda x.x t)u; \mathfrak{s})$. $\square$

As expected, Transfer does not hold for all formulas. A counter-example is given in the
next proposition by the external formula stating that all individuals are (not not) standard.

**Proposition 5.9.** Let $A(x)$ denote the formula $\neg\mathrm{st}(x)$. Then, there is no realizer for the formulas $\forall^{\mathrm{st}}x.\neg A(x) \to \forall x.\neg A(x)$ and $\exists x.A(x) \to \exists^{\mathrm{st}}x.A(x)$.

Proof. Both statements follow from the definitions. For instance, for the second formula,
observe that

$$
\bigcup_{f \in \mathbb{N}^{\mathfrak{G}}} \{(t; \mathfrak{s}) : (\pi_1(t); \mathfrak{s}) \in |\mathrm{st}(f)|^{\mathfrak{G}} \wedge (\pi_2(t); \mathfrak{s}) \in |\neg\mathrm{st}(f)|^{\mathfrak{G}}\} = \emptyset
$$

since for any $f \in \mathbb{N}^{\mathfrak{G}}$, either $|\mathrm{st}(f)|^{\mathfrak{G}}$ or $|\neg\mathrm{st}(f)|^{\mathfrak{G}}$ is empty. Consequently, we have
$|\exists^{\mathrm{st}}x.A(x)|^{\mathfrak{G}} = \emptyset$ while $|\exists x.A(x)|^{\mathfrak{G}} = |\top|^{\mathfrak{G}} = \Lambda \times \mathfrak{G}$. $\square$

The principle of External Induction [Nel87] allows to prove that a certain property
is valid for all standard natural numbers. For instance, the assertion stating that every
nonstandard element is larger than all standard natural numbers<fnref n="4" />. We show that in our
context, this principle can be realized using the *rec* instruction.

**Proposition 5.10 (External induction).** For any formula $A(x)$ whose only free variable is $x$
$\mathrm{rec} \Vdash A(0^*) \to \forall^{\{\mathrm{st}\}}x.(A(x) \to A(S(x))) \to \forall^{\{\mathrm{st}\}}x.A(x)$.

Proof. Let $\mathfrak{s}$ be a state, $n \in \mathbb{N}$ be a natural number and $u_0$, $u_S$ be terms and $V$ be a value such that $(u_0; \mathfrak{s}) \in |A(0^*)|^\mathfrak{G}$, $(u_S; \mathfrak{s}) \in |\forall^{\mathrm{st}}y.(A(y) \to A(S(y)))|^\mathfrak{G}$ and $(V; \mathfrak{s}) \in |\mathrm{Nat}(n^*)|^\mathfrak{G}$. The latter implies that $V = \bar{n}$. Let us prove, by induction on $n$, that

$$
\mathrm{rec} \ u_0 \ u_S \ \bar{n} \in |A(n^*)|^\mathfrak{G}
$$

* If $n = 0$, then we have that $\mathrm{rec} \ u_0 \ u_S \ \bar{0}^s \downarrow^s \ u_0$, the result follows by anti-reduction from the hypothesis on $u_0$.

* If $n = S(m)$, then we have that $\mathrm{rec} \ u_0 \ u_S (s \bar{m})^s \downarrow^s u_S \bar{m}$ ($\mathrm{rec} \ u_0 \ u_S \bar{m}$). By induction hypothesis, we have that $(\mathrm{rec} \ u_0 \ u_S \bar{m}; \mathfrak{s}) \in |A(m)|^{\mathfrak{G}}$. The result thus follows (by anti-reduction) from the hypothesis on $u_S$. $\square$

The next two propositions show that one cannot separate standard natural numbers
from nonstandard natural numbers using an internal formula [Rob66]. This fact is usually
formalized by the properties of Overspill and Underspill. We first show that, in our context,
Overspill can be *realized* by combining the realizers for ENS₀ and for the Transfer principle.

**Proposition 5.11 (Overspill).** For any internal formula $A$, we have

$$
\lambda x.(\dagger, x \dagger) \Vdash \forall^{\mathrm{st}} x.A(x) \to \exists x.(\neg\mathrm{st}(x) \wedge A(x)).
$$

<footnote n="4">⁴Actually, this requires to consider a quotiented definition of the standardness predicate, see Proposition 7.1.</footnote>
**Proof.** Let $(u; \mathfrak{s}) \Vdash \forall^{\text{st}}x.A(x)$. Let us show that $((\lambda x.(t, x t))u; \mathfrak{s}) \Vdash \exists x.(\neg \text{st}(x) \land A(x))$. Following the proof of part 3 in Theorem 5.8, we obtain $(ut; \mathfrak{s}) \Vdash \forall x.A(x)$ and therefore $(ut; \mathfrak{s}) \Vdash A(\delta)$. By ENS$_0$ (Proposition 5.5), we have $(t; \mathfrak{s}) \Vdash \neg \text{st}(\delta)$. Finally, we obtain that $((t, ut); \mathfrak{s}) \Vdash \exists x.(\neg \text{st}(x) \land A(x))$ and we can conclude by anti-reduction. $\square$

The usual proof of Underspill is by contradiction, hence using classical logic, which we do not have here. Nevertheless, we can obtain the following version in which a double-negation occurs.

**Proposition 5.12 (Underspill).** For any internal formula A, we have

$$ \lambda xy.(\lambda z.y(\dagger, z))(x \dagger) \Vdash (\forall x.\neg\text{st}(x) \rightarrow A(x)) \rightarrow \neg\neg\exists^{\text{st}}x.A(x). $$

**Proof.** Let $\mathfrak{s}$ be a state, and $u, v$ be terms such that $(u; \mathfrak{s}) \Vdash \forall x.\neg\text{st}(x) \rightarrow A(x)$ and $(v; \mathfrak{s}) \Vdash \neg\exists^{\text{st}}x.A(x)$. Using the adequacy of congruence rules (Proposition 4.7), observe that $(v; \mathfrak{s}) \Vdash \forall x.((\text{st}(x) \land A(x)) \rightarrow \bot)$, and by currying

$$ (\lambda wz.v(w, z); \mathfrak{s}) \Vdash \forall^{\text{st}}x.A(x) \rightarrow \bot $$

Since A is internal, by Transfer, we get

$$ (\lambda z.v(t, z); \mathfrak{s}) \Vdash \forall x.A(x) \rightarrow \bot $$

By the hypothesis on $u$ and ENS$_0$, we have $(ut; \mathfrak{s}) \Vdash A(\delta)$, hence

$$ (\lambda z.v(t, z))(ut); \mathfrak{s}) \Vdash \bot, $$

and we can conclude by anti-reduction. $\square$

**5.3. Idealization.** We first extend the realizability interpretation to take into account relations $R: \mathbb{N}^2 \rightarrow \mathbb{N}$ on the natural numbers:

$$ |R(e_1, e_2)|_{\mathfrak{S}} \triangleq \{(t; \mathfrak{s}) : R(\llbracket e_1 \rrbracket_{\rho}(\mathfrak{s}), \llbracket e_2 \rrbracket_{\rho}(\mathfrak{s})) \text{ holds}\}. $$

This coincides with the interpretation of the relation $R$ through a second-order variable and the corresponding semantic relation from $\mathbb{N}^2$ to **SAT** in the interpretation.

Let us now briefly illustrate the main idea behind the proof of Idealization by showing that there exists a (nonstandard) natural number greater than or equal to any standard number. The usual proof relies on the fact that $\delta$ is such a number, since for any standard number $n$, in any slice greater than or equal to $n$, the relation $n \le \delta$ holds. In our setting, we use the set instruction to reach such a state.

**Proposition 5.13 (Diagonalization).** We have $\lambda z.T z \text{ get } (\lambda xy.\text{set } y \dagger) \Vdash \exists^{\{\mathbb{N}\}}x.\forall^{\{\text{st}\}}y.y \le x$.

**Proof.** Let $\mathfrak{s}$ be an arbitrary state. Following the proof of part 2 of Lemma 5.4, it is clearly enough to prove that $(\lambda xy.\text{set } y \dagger; \mathfrak{s}) \Vdash \forall^{\{\text{st}\}}y.y \le \delta$ (the rest of the proof is exactly the same replacing $\neg\text{st}(\delta)$ with $\forall^{\{\text{st}\}}y.y \le \delta$). Let $n \in \mathbb{N}$ and $t$ an arbitrary term. Then

$$ (\lambda xy.\text{set } y t) t \bar{n} \mathfrak{s} \downarrow^{\mathfrak{s}} \text{set } \bar{n} t \mathfrak{s} \downarrow^{\mathfrak{s}'} t $$

where $\mathfrak{s}' = \max(n, \mathfrak{s})$. In particular, $n \le \delta(\mathfrak{s}')$ holds, hence $(t; \mathfrak{s}') \in |n \le \delta|^{\mathfrak{S}}$ and we can conclude by anti-reduction. $\square$
Consider a term loop$^+$ such that$^5$ for any state $\mathfrak{s} \in \mathfrak{S}$ it holds that loop$^+ \mathfrak{s} \downarrow^s \text{ incr loop}^+$, where incr $\triangleq \lambda x. \text{set} (\mathfrak{s} \text{ get}) x$. Then for any natural number $n \in \mathbb{N}$ and any state $\mathfrak{s} \in \mathfrak{S}$, loop$^+ \mathfrak{s} \downarrow^s \text{ loop}^+$ where $\mathfrak{s}' \ge n$. Since for any $\mathfrak{s}' \ge n$, $(\dagger; \mathfrak{s}') \in |n < \delta|^{\mathfrak{S}}$, by anti-reduction we obtain the following Proposition.

**Proposition 5.14.** We have $\lambda w. loop^+ \models \forall^{\text{st}} x.x < \delta$.

Observe that here the value of $n$ is not required, so the quantifier does not need to be relativized. Yet, the computation never terminates and we do not even know when the computation reaches a correct state.

As mentioned above, the idea to prove the general case of Idealization is very similar. If for any $n \in \mathbb{N}$ there exists $\tau_n \in \mathbb{N}$ such that for any $m \le n$, $R(\tau_n, m)$ holds, we can consider the nonstandard natural number $\tau \triangleq (\tau_\mathfrak{s})_{\mathfrak{s} \in \mathfrak{S}} \in \mathbb{N}^{\mathfrak{S}}$. Using a witness extraction mechanism, as provided by the next proposition, we can compute $\tau$ from any realizer of $\forall^{\text{st}}_n \exists^{\text{st}}_x. \forall^{\text{st}}_y. (y \le n \to R(x, y))$.

**Proposition 5.15 (Witness extraction).** For any formula $A$, any valuation $\rho$ closing $\exists x.A$, any state $\mathfrak{s}$ and any term $t$ such that $(t; \mathfrak{s}) \in |\exists^{\mathbb{N}} x.A|^{\mathfrak{S}}$, there exists a natural number $f \in \mathbb{N}^{\mathfrak{S}}$ and a term $u$ such that $(u; \mathfrak{s}) \in |A|^{\mathfrak{S}}_{\rho, x \mapsto f}$ and $t (\lambda xy.(x, y)) \mathfrak{s} \downarrow^s (f(\mathfrak{s}), u)$.

*Proof.* Assume that $(t; \mathfrak{s}) \in |\exists^{\mathbb{N}} x.A|^{\mathfrak{S}}$. By definition, for any $\mathfrak{X} \in \mathbf{SAT}$ and any $(v; \mathfrak{s}) \in |\forall^{\mathbb{N}} x.(A \to X)|_{\rho, X \to \mathfrak{X}}$, we have that $(tv; \mathfrak{s}) \in \mathfrak{X}$. Let us define the set

$$ \mathfrak{X} \triangleq \{(w; \mathfrak{s}') \in \Lambda \times \mathfrak{S} : \exists f \in \mathbb{N}^{\mathfrak{S}}. \exists u \in \Lambda. w^{\mathfrak{s}'} \downarrow^{\mathfrak{s}} (\overline{f(\mathfrak{s})}, u) \wedge (u; \mathfrak{s}) \in |A|^{\mathfrak{S}}_{\rho, x \mapsto f}\}, $$

which is obviously saturated. Clearly $(\lambda xy.(x, y); \mathfrak{s}) \in |\forall^{\mathbb{N}} x.(A \to X)|^{\mathfrak{S}}_{\rho, X \to \mathfrak{X}}$ since for any $f \in \mathbb{N}^{\mathfrak{S}}$ and any $(u; \mathfrak{s}) \in |A|^{\mathfrak{S}}_{\rho, x \mapsto f}$, it holds that $(\lambda xy.(x, y)) f(\mathfrak{s}) u^{\mathfrak{s}} \downarrow^{\mathfrak{s}} (\overline{f(\mathfrak{s})}, u) \in \mathfrak{X}$. We conclude that $(t (\lambda xy.(x, y)); \mathfrak{s}) \in \mathfrak{X}$, i.e. $t (\lambda xy.(x, y)) \mathfrak{s} \downarrow^s (f(\mathfrak{s}), u)$. $\square$

The term

$$ \text{ideal} \triangleq \lambda x. \lambda y. T y (\pi_1(T(x \dagger) \text{ get} (\lambda xy.(x, y)))) (\lambda yz. \text{set } z y) $$

is a realizer for the Idealization principle. Indeed, in any state $\mathfrak{s}$ the first component of ideal computes $\tau(\mathfrak{s})$ (using Proposition 5.15), while the second component increases the state to ensure the validity of the relation (as in Proposition 5.13).

**Theorem 5.16 (Idealization).** We have:

$$ \text{ideal} \models \forall^{\text{st}}_n \exists^{\mathbb{N}} x. \forall^{\text{st}}_y y. (y \le n \to R(x, y)) \to \exists^{\mathbb{N}} x. \forall^{\text{st}}_y y. R(x, y). $$

*Proof.* Let $\mathfrak{s}$ be any state and $u$ a term such that

$$ (u; \mathfrak{s}) \in |\forall^{\text{st}}_n \exists^{\mathbb{N}} x. \forall^{\text{st}}_y y. (y \le n \to R(x, y))|^{\mathfrak{S}}. $$

By part 2 of Lemma 5.4, this entails that

$$ (T(u \dagger) \text{ get}; \mathfrak{s}) \in |\exists^{\mathbb{N}} x. \forall^{\text{st}}_y y. (y \le \mathfrak{s} \to R(x, y))|^{\mathfrak{S}}. $$

By Proposition 5.15, we know that there exists a natural number $f_\mathfrak{s} \in \mathbb{N}^{\mathfrak{S}}$ and a term $v_\mathfrak{s} \in \Lambda$ such that $T(u \dagger) \text{ get} (\lambda xy.(x, y)) \mathfrak{s} \downarrow^s (f_\mathfrak{s}(\mathfrak{s}), v_\mathfrak{s})$ and $(v_\mathfrak{s}; \mathfrak{s}) \in |\forall^{\text{st}}_y y. (y \le \mathfrak{s} \to R(f_\mathfrak{s}, y))|^{\mathfrak{S}}$. The latter implies that for any $m \in \mathbb{N}$ such that $m \le \mathfrak{s}$ and any term $t$, it

<footnote>$^5$For instance, we can define loop$^+ \triangleq Y \text{ incr}$, where $Y$ is the usual fixed-point combinator of the $\lambda$-calculus.</footnote>
holds that $(v_s t \bar{m} t; s) \in |R(f_s, m)|^{\mathcal{G}}$ and hence $R(f_s(s), m)$ holds (since $|R(f_s, m)|_s = \{(t; s) : R(f_s(s), m) \text{ holds}\})$.

Consider the (possibly nonstandard) individual $\tau \in \mathbb{N}^{\mathcal{G}}$ defined by $\tau(s) = f_s(s)$.

We have

$$ \text{ideal } u \overset{s}{\downarrow}^{s} \lambda y.T y (\pi_1(T(u\dagger) \text{get} (\lambda xy.(x, y)))) (\lambda yz.\text{set } z y) $$

hence, by part 2 of Lemma 5.4, to conclude by anti-reduction it suffices to prove that

(1) $\pi_1(T(u\dagger) \text{get} (\lambda xy.(x, y))) \overset{s}{\downarrow}^{s} \tau(s)$. Indeed, we know that this term reduces as follows:

$$ \pi_1(T(u\dagger) \text{get} (\lambda xy.(x, y))) \overset{s}{\downarrow}^{s} \pi_1(\overline{f_s(s)}, v_s) \overset{s}{\downarrow}^{s} \overline{f_s(s)} $$

and by definition $\tau(s) = f_s(s)$.

(2) $(\lambda yz.\text{set } z y; s) \Vdash \forall^{\{st\}} y.R(\tau, y)$. To prove this, it suffices to show that for any $m \in \mathbb{N}$ and any $t \in \Lambda$, we have $((\lambda yz.\text{set } z y) t \bar{m}; s) \Vdash R(\tau, m^*)$. With $s' \triangleq \max(s, m)$, we have that $(\lambda yz.\text{set } z y) t \bar{m} \overset{s}{\downarrow}^{s} \text{set } \bar{m} t \overset{s}{\downarrow}^{s'} t$. By construction, since $m \le s'$, we know that $R(\tau(s'), m)$ holds, hence $(t; s') \in |R(\tau(s'), m)|_{\rho}^{\mathcal{G}}$ and we conclude by anti-reduction. $\square$

## 6. LLPO

In this section we give a realizer for a nonstandard version of the *Lesser Limited Principle of Omniscience*:

$$ \text{LLPO} := \forall x.\forall y.(A(x) \lor B(y)) \rightarrow (\forall x.A(x) \lor \forall y.B(y)) $$

This principle is a semi-intuitionistic principle, in the sense that it is seen as being nonconstructive (it is indeed provably false in some intuitionistic theories, cf. [BR87, p. 4]) while still being weaker than the full law of excluded middle.

**6.1. LLPO in nonstandard arithmetic.** We will consider a variant of the LLPO principle in our setting, where the quantifiers are restricted to standard elements and the formulas A and B are internal (where $x$ (resp. $y$) does not occur in $B$ (resp. in $A$)):

$$ \text{LLPO}^{\text{st}} := \forall^{\{st\}} x.\forall^{\{st\}} y.(A(x) \lor B(y)) \rightarrow (\forall^{\{st\}} x.A(x) \lor \forall^{\{st\}} y.B(y)) $$

Let us give an overview of our computational interpretation for this principle, which will rely on the several realizers introduced in Section 6.3 and described in Figure 2. Assume that we are given, in a certain state, a realizer of the hypothesis

$$ H_{A,B} \triangleq \forall^{\{st\}} x.\forall^{\{st\}} y.(A(x) \lor B(y)). $$

The main idea consists in turning this term into a realizer of

$$ \forall^{\{st\}} z.(A_{\le z} \lor B_{\le z}), $$

where $A_{\le z} \triangleq \forall^{\{\mathbb{N}\}} x. x \le z \rightarrow A(x)$.

Indeed, observing that the formula $A_{\le z}$ is internal, by Transfer and instantiation with $\delta$ (or any other nonstandard element), the proposition $x \le \delta$ becomes trivially true for any standard $x$ and we get the expected conclusion

$$ (\forall^{\{st\}} x.A(x)) \lor (\forall^{\{st\}} y.B(y)). $$

In fact, this last step is the only step where we actually use nonstandard principles (here Transfer and the existence of nonstandard elements). The rest of the proof, forgetting
all the relativizations to standard elements, would be valid in standard arithmetic. This is reflected by the fact that we only use External Induction and properties of the disjunction. In terms of realizers, this means that we will only use universal realizers that will never manipulate the state.

To get a realizer of $\forall^{\{st\}}z.(A_{\le z} \lor B_{\le z})$, we rely on External Induction (as the term $t_{aux}$ shows), the main difficulty lying in proving the induction step

$$ \forall^{\{st\}}x. (A_{\le x} \lor B_{\le x} \rightarrow A_{\le S(x)} \lor B_{\le S(x)}). $$

To illustrate this step, let us consider the case where $A_{\le x}$ holds. To obtain the expected conclusion, it is sufficient to show that $A(S(x)) \lor B_{\le S(x)}$ holds. This leads us to break the symmetry between A and B by considering the formula

$$ \Phi_{A,B}(x, y) \triangleq A(x) \lor B_{\le y}. $$

But using our starting assumption, namely a realizer of $\forall^{\{st\}}x.\forall^{\{st\}}y.(A(x) \lor B(y))$, for any standard $x$ we can easily get $\forall^{\{st\}}y.\Phi_{A,B}(x, y)$ by external induction, and thus $\forall^{\{st\}}x.\forall^{\{st\}}y.\Phi_{A,B}(x, y)$ which is enough to conclude the whole proof. For the inductive step $\forall^{\{st\}}y. (\Phi_{A,B}(x, y) \rightarrow \Phi_{A,B}(x, S(y)))$ of the latter induction, we reason by cases on the induction hypothesis:

* if $A(x)$ holds then the conclusion follows immediately,

* if $B_{\le y}$ holds, then we use the assumption to get either $A(x)$ or $B(S(y))$, and again, in both cases the conclusion follows.

This proof is a variation of [BBS12, Prop. 3.4], the main difference being that in our context, we have access to concrete nonstandard elements (namely $\delta$), and we can instantiate a certain formula with $\delta$ instead of using the Idealization principle.

## 6.2. Disjunction.
In order to define a realizer for LLPO<sup>st</sup>, we first need to extend our language with disjunctions. We choose to rely on a primitive disjunction rather than on a second-order impredicative encoding of disjunction as the latter would make the task of finding realizers much more difficult without bringing additional strength to our setting.

We thus extend the languages of terms and formulas as follows:

$$ \begin{array}{lll} \textbf{Formulas} & A, B ::= \dots | A \lor B & \\ \textbf{Terms} & t, u ::= \dots | \iota_1(t) | \iota_2(t) | \text{case } t \{\iota_1(x_1) \mapsto t_1 | \iota_2(x_2) \mapsto t_2\} & \end{array} $$

and the type system accordingly

$$ \frac{\Gamma \vdash t : A_1 \qquad (\forall I_1)}{\Gamma \vdash \iota_1(t) : A_1 \lor A_2} \qquad \frac{\Gamma \vdash t : A_2 \qquad (\forall I_2)}{\Gamma \vdash \iota_2(t) : A_1 \lor A_2} $$

$$ \frac{\Gamma \vdash t : A_1 \lor A_2 \qquad \Gamma, x_i : A_i \vdash t_i : C}{\Gamma \vdash \text{case } t \{\iota_1(x_1) \mapsto t_1 | \iota_2(x_2) \mapsto t_2\} : C} \quad (\forall_E) $$

We also extend the reduction system with one extra case to define contexts

$$ C[\iota] ::= \dots | \text{case } [\iota_1(x_1) \mapsto t_1 | \iota_2(x_2) \mapsto t_2] $$

and one additional reduction rule for this new operations

$$ \frac{\text{case } \iota_i(t) \{\iota_1(x_1) \mapsto t_1 | \iota_2(x_2) \mapsto t_2\} \triangleright \beta t_i[t/x_i]}{\iota_i(x_i)} $$
Finally, we extend the realizability interpretation to include the case of disjunction. We base the definition on the elimination rule of the disjunction (see Remark 4.12), as has been done before for the other connectives:

$$|A_1 \lor A_2|_{\rho}^{\mathcal{G}} \triangleq \{(t; \mathfrak{s}) \in \Lambda \times \mathcal{G} : \forall t_1, t_2, S \in \mathbf{SAT}. \\ (\forall i \in \{1, 2\}. \forall (u_i; \mathfrak{s}) \in |A_i|_{\rho}^{\mathcal{G}}. (t_i[u_i/x_i]; \mathfrak{s}) \in S) \Rightarrow \\ (\text{case } t \{\iota_1(x_1) \mapsto t_1 | \iota_2(x_2) \mapsto t_2\}; \mathfrak{s}) \in S\}$$

Observe that glueing still holds by simply defining $\overline{A \lor B}^s \triangleq \overline{A}^s \lor \overline{B}^s$.

Once more, we take advantage of the modularity of the realizability interpretation to get the adequacy with respect with the type system extended with disjunction by only proving the adequacy of the new typing rules (see Definition 4.8).

**Proposition 6.1.** *The rules $(\vee_I^1)$, $(\vee_I^2)$ and $(\vee_E)$ are adequate.*

*Proof.* The adequacy of the rule $(\vee_E)$ follows directly from the definition, by considering the particular set $S = |C|_{\rho}^{\mathcal{G}}$.

We now prove adequacy of the rule $(\vee_I^1)$. Assume that the typing judgment $\Gamma \vdash t : A_1$ is adequate with respect to some state $\mathfrak{s} \in \mathcal{S}$. To prove that the conclusion is adequate with respect to the same state, let us consider $\rho$ a valuation closing $A_1 \lor B_2$ and $\Gamma$, $\sigma$ a substitution such that $(\sigma; \mathfrak{s}) \models \rho(\Gamma)$ and let $t_1, t_2$ be two terms and $S \in \mathbf{SAT}$ be such that for any $(u_i; \mathfrak{s}) \in |A_i|_{\rho}^{\mathcal{G}}$ we have that $(t_i[u_i/x_i]; \mathfrak{s}) \in S$. Since $\sigma(\iota_1(t)) = \iota_1(\sigma(t))$, we have

$$\text{case } (\sigma(\iota_1(t))) \{\iota_1(x_1) \mapsto t_1 | \iota_2(x_2) \mapsto t_2\} \stackrel{s\downarrow s}{\Rightarrow} t_1[\sigma(t)/x_1].$$

Using the hypotheses, we have that $(\sigma(t); \mathfrak{s}) \in |A_1|_{\rho}^{\mathcal{G}}$ and therefore $(t_1[\sigma(t)/x_1]; \mathfrak{s}) \in S$. We can conclude by anti-reduction. $\square$

As an illustration of the use of disjunction, we define below a term allowing us to commute $A$ and $B$ in the premise of LLPO$^{st}$. This term will be useful afterwards since the proof mostly relies on two External Inductions in which the formulas $A$ and $B$ have asymmetric roles.

**Lemma 6.2.** *For any formulas $A$ and $B$ we have*

$$t_{\vee} \mathrel{||\vdash} (\forall^{\{st\}} x. \forall^{\{st\}} y. (A(x) \lor B(y))) \rightarrow \forall^{\{st\}} x. \forall^{\{st\}} y. (B(x) \lor A(y))$$

where $t_{\vee} \triangleq \lambda h z x w y. \text{case } (h \ z \ x \ w \ y) \{\iota_1(h_1) \mapsto \iota_2(h_1)|\iota_2(h_2) \mapsto \iota_1(h_2)\}$.

*Proof.* Let $\mathfrak{s} \in \mathcal{S}$ be a state, $(h; \mathfrak{s}) \models \forall^{\{st\}} x \forall^{\{st\}} y. (A(x) \lor B(y))$ and $n, m \in \mathbb{N}$ be two natural numbers. We have

$$t_{\vee} h \dagger \bar{n} \dagger \bar{m} \stackrel{s\downarrow s}{\Rightarrow} \text{case } (h \dagger \bar{n} \dagger \bar{m}) \{\iota_1(h_1) \mapsto \iota_2(h_1)|\iota_2(h_2) \mapsto \iota_1(h_2)\}$$

The assumption on $h$ gives us that $(h \dagger \bar{n} \dagger \bar{m}; \mathfrak{s}) \in |A \lor B|_{\rho}^{\mathcal{G}}$. Since it is clear that for any $(t_A; \mathfrak{s}) \in |A|_{\rho}^{\mathcal{G}}$, $(\iota_2(t_A); \mathfrak{s}) \in |B \lor A|_{\rho}^{\mathcal{G}}$ (and vice-versa with $(t_B; \mathfrak{s}) \in |B|_{\rho}^{\mathcal{G}}$ and $\iota_1(t_B)$), by definition of $|A \lor B|_{\rho}^{\mathcal{G}}$ we have that the right-hand side terms belongs to $|B \lor A|_{\rho}^{\mathcal{G}}$ and we can conclude by anti-reduction. $\square$
$$ t_{\text{LLPO}} \Vdash \text{LLPO}^{\text{st}} \equiv \underbrace{\forall^{\{\text{st}\}} x. \forall^{\{\text{st}\}} y. (A(x) \lor B(y))}_{H_{A,B}} \rightarrow (\forall^{\{\text{st}\}} x. A(x) \lor \forall^{\{\text{st}\}} y. B(y)) \quad (\text{Thm. 6.13}) $$

$$ t_{\delta} \Vdash (\forall^{\{\mathcal{N}\}} y. y \le \delta \rightarrow A(y)) \rightarrow \forall^{\{\text{st}\}} y. A(y) \quad (\text{Lem. 6.5}) $$

$$ t_{\text{aux}} \Vdash H_{A,B} \rightarrow \forall^{\{\text{st}\}} x. \underbrace{ (\forall^{\{\mathcal{N}\}} z. z \le x \rightarrow A(z))}_{A \le x} \lor \underbrace{ (\forall^{\{\mathcal{N}\}} z. z \le x \rightarrow B(z))}_{B \le x} \quad (\text{Cor. 6.12}) $$

$$ u_0 \Vdash H_{A,B} \rightarrow A \leq_0 \lor B \leq_0 \quad (\text{Lem. 6.10}) $$

$$ u_s \Vdash H_{A,B} \rightarrow \forall^{\{\text{st}\}} x. (A \leq_x \lor B \leq_x \rightarrow A \leq_{S(x)} \lor B \leq_{S(x)}) \quad (\text{Lem. 6.11}) $$

$$ t_{\Delta} \Vdash H_{A,B} \rightarrow \forall^{\{\text{st}\}} x. (A \leq_x \rightarrow A \leq_{S(x)} \lor B \leq_{S(x)}) \quad (\text{Lem. 6.9}) $$

$$ t_{\Phi} \Vdash H_{A,B} \rightarrow \forall^{\{\text{st}\}} x \forall^{\{\text{st}\}} y. \underbrace{(A(x) \lor B \leq_y)}_{\Phi_{A,B}(x,y)} \quad (\text{Cor. 6.8}) $$

$$ t_0 \Vdash H_{A,B} \rightarrow \forall^{\{\text{st}\}} x. \Phi_{A,B}(x, 0) \quad (\text{Lem. 6.6}) $$

$$ t_s \Vdash H_{A,B} \rightarrow \forall^{\{\text{st}\}} x. \forall^{\{\text{st}\}} y. (\Phi_{A,B}(x, y) \rightarrow \Phi_{A,B}(x, S(y))) \quad (\text{Lem. 6.7}) $$

$$ t_{\le 0} \Vdash A(0) \rightarrow A \le 0 \quad (\text{Lem. 6.3}) $$

$$ t_{\le s} \Vdash \forall x. (A \le x \rightarrow A(S(x)) \rightarrow A \le S(x)) \quad (\text{Lem. 6.4}) $$

$$ t_{\vee} \Vdash H_{A,B} \rightarrow H_{B,A} \quad (\text{Lem. 6.2}) $$

where A and B are internal formulas.

<caption>Figure 2: Terms used to realize LLPO<sup>st</sup></caption>

**6.3. A realizer for LLPO<sup>st</sup>.** We shall now detail the definition of a realizer for LLPO<sup>st</sup>. Its definition follows the intuition of the proof sketched in Section 6.1. To that end, we require several terms meant to be realizers corresponding to the different steps of the proof, as described in Figure 2.

Recall that the ordering $\cdot < \cdot$ and $\cdot \le \cdot$ are interpreted as any relations $R : \mathbb{N}^2 \rightarrow \mathbb{N}$ following the definition given in Section 5.3:

$$ |R(e_1, e_2)|_{\mathcal{S}} \triangleq \{(t; \mathfrak{s}) : R(\llbracket e_1 \rrbracket_{\mathcal{S}}), \llbracket e_2 \rrbracket_{\mathcal{S}}(\mathfrak{s})\} \text{ holds}\}. $$

We start by showing how a realizer of $A_{\le n}$ can be obtained from realizers of the different $A(m)$ for $m \le n$.

**Lemma 6.3.** For any internal formula A, we have

$$ t_{\le 0} \Vdash A(0) \rightarrow A \le 0, $$

where $t_{\le 0} \triangleq \lambda xny.x$.

*Proof.* Recall that $A_{\le 0} \triangleq \forall^{\{\mathcal{N}\}} x. x \le 0 \rightarrow A(x)$. Let $\mathfrak{s} \in \mathcal{S}$ be a state, $f \in \mathbb{N}^{\mathcal{S}}$ be an individual and $u, v$ be terms such that $(u; \mathfrak{s}) \in |A(0)|_{\mathcal{S}}^{\mathcal{S}}$, $(v; \mathfrak{s}) \in |f \le 0|_{\mathcal{S}}^{\mathcal{S}}$. In particular, the latter entails that $f(\mathfrak{s}) = 0$. Therefore, since A is internal, we get that $(u; \mathfrak{s}) \in |A(f)|_{\mathcal{S}}^{\mathcal{S}}$ by glueing. By construction, we have that

$$ t_{\le 0} u \bar{0} v^{\mathfrak{s} \downarrow^{\mathfrak{s}}} u $$

and we can conclude by anti-reduction. $\square$
In the next lemma, we write if $\bar{n} = \bar{m}$ then $t$ else $u$ (where $n, m \in \mathbb{N}$ and $t, u \in \Lambda$) for a term that reduces to $t$ if $n = m$ and to $u$ otherwise (defining such a term using the rec operator is an easy programming exercise, which we would rather not bother the reader with).

**Lemma 6.4.** For any internal formula $A$ and any natural number $n \in \mathbb{N}$, we have

$$t_{\le s} \bar{n} \Vdash A_{\le n} \rightarrow A(S(n)) \rightarrow A_{\le S(n)},$$

where $t_{\le s} \triangleq \lambda nxymz$. if $m = sn$ then $y$ else $(xmz)$.

*Proof.* Recall that $A_{\le n} \triangleq \forall^{\mathbb{N}} x.x \le n \rightarrow A(x)$. Let $s \in \mathfrak{S}$ be a state, $n \in \mathbb{N}$ be a natural number, $f \in \mathbb{N}^{\mathfrak{S}}$ be an individual, and $u, v, w \in \Lambda$ be terms such that $(u; \mathfrak{s}) \in |A_{\le n}|_{\rho}^{\mathfrak{S}}$, $(v; \mathfrak{s}) \in |A(S(n))|_{\rho}^{\mathfrak{S}}$ and $(w; \mathfrak{s}) \in |f \le S(n)|_{\rho}^{\mathfrak{S}}$. Putting $m \triangleq f(\mathfrak{s})$, the latter entails that $m \le S(n)$. By construction, we have

$$t_{\le s} \bar{n} u v \bar{m} w \stackrel{s\downarrow}{\Vdash} \mathfrak{s} \text{ if } \bar{m} = \bar{s} \bar{n} \text{ then } v \text{ else } (u \bar{m} w).$$

Let us reason by case analysis:

* if $f(\mathfrak{s}) = m = S(n)$, then we have

$$\text{if } \bar{m} = \bar{s} \bar{n} \text{ then } v \text{ else } (u \bar{m} w) \stackrel{s\downarrow}{\Vdash} \mathfrak{s} \text{, } v,$$

and since $A$ is internal, we get that $(v; \mathfrak{s}) \in |A(f)|_{\rho}^{\mathfrak{S}}$ by glueing which allows us to conclude by anti-reduction.

* if $f(\mathfrak{s}) = m < S(n)$, then we have

$$\text{if } \bar{m} = \bar{s} \bar{n} \text{ then } v \text{ else } (u \bar{m} w) \stackrel{s\downarrow}{\Vdash} \mathfrak{s} \text{ } u \bar{m} w.$$

By assumption on $u$, we have that $(u \bar{m} w; \mathfrak{s}) \in |A(m)|_{\rho}^{\mathfrak{S}}$, and therefore $(u \bar{m} w; \mathfrak{s}) \in |A(f)|_{\rho}^{\mathfrak{S}}$ using glueing. We can thus conclude by anti-reduction. $\square$

If something is true below a certain nonstandard element, such as $\delta$, then it is true for any standard element. This is connected with Proposition 5.14 that states that $\delta$ is greater than any standard natural number, and is somewhat trivial in usual nonstandard settings (which is reflected here by the fact that the realizer is making a blind loop).

**Lemma 6.5.** For any formula $A$, we have

$$t_{\delta} \Vdash A_{\le \delta} \rightarrow \forall^{\{\text{st}\}} y.A(y),$$

where $t_{\delta} \triangleq \lambda xy.x \iota_2(\text{loop}^+)$.

*Proof.* Let $\mathfrak{s}$ be a state and $u$ be a term such that $(u; \mathfrak{s}) \Vdash \forall^{\mathbb{N}} y.y \le \delta \rightarrow A(y)$. We need to show that $(t_{\delta} u; \mathfrak{s}) \Vdash \forall^{\{\text{st}\}} y.A(y)$. Letting $n \in \mathbb{N}$ be a standard natural number, we have

$$t_{\delta} u \bar{n} \stackrel{s\downarrow}{\Vdash} \mathfrak{s} \text{ } u \bar{n} \iota_2(\text{loop}^+).$$

By Proposition 5.14, we know that $(\iota_2(\text{loop}^+); \mathfrak{s}) \Vdash n < \delta$, hence $u \bar{n} \iota_2(\text{loop}^+) \Vdash A(n)$ (using the hypotheses on $u$) and we can conclude by anti-reduction. $\square$

We now show how to build the different terms necessary to the first External Induction, allowing us to obtain a realizer for the formula $\forall^{\{\text{st}\}} x. \forall^{\{\text{st}\}} y. \Phi_{A,B}(x, y)$.

**Lemma 6.6.** For any internal formulas $A$ and $B$, we have

$$t_0 \Vdash (\forall^{\{\text{st}\}} x. \forall^{\{\text{st}\}} y. (A(x) \lor B(y))) \rightarrow \forall^{\{\text{st}\}} x. \Phi_{A,B}(x, 0),$$

where $t_0 \triangleq \lambda hwx. \text{ case } (h \dagger x \dagger 0) \{\iota_1(a) \mapsto \iota_1(a) | \iota_2(b) \mapsto t_{\le 0} b\}$.
*Proof.* Recall that $\Phi_{A,B}(x, y) = A(x) \lor B_{\le y}$. Let $\mathfrak{s} \in \mathfrak{S}$ be a state, $n \in \mathbb{N}$ be a natural number and $h \in \Lambda$ be a term such that $(h; \mathfrak{s}) \in |\forall^{\{\mathrm{st}\}}x.\forall^{\{\mathrm{st}\}}y.(A(x) \lor B(y))|_{\rho}^{\mathfrak{S}}$. We have

$$t_0 h \dagger \bar{n} \stackrel{\mathfrak{s}}{\downarrow} \text{ case } (h \dagger \bar{n} \dagger 0) \{\iota_1(a) \mapsto \iota_1(a) | \iota_2(b) \mapsto t_{\le 0} b\}.$$

Using the assumption on $h$, we have $((h \dagger \bar{n} \dagger 0); \mathfrak{s}) \in |A(x) \lor B(0)|_{\rho}^{\mathfrak{S}}$. We can thus conclude by anti-reduction using the adequacy of the $(\lor_E)$ rule and Lemma 6.3 for the $\iota_2(\cdot)$ case. $\square$

**Lemma 6.7.** For any internal formulas A and B, we have

$$t_s \Vdash (\forall^{\{\mathrm{st}\}}x.\forall^{\{\mathrm{st}\}}y.(A(x) \lor B(y))) \rightarrow \forall^{\{\mathrm{st}\}}x.\forall^{\{\mathrm{st}\}}y.(\Phi_{A,B}(x, y) \rightarrow \Phi_{A,B}(x, sy)),$$

where

$$t_s \triangleq \lambda hwxzyp. \text{ case } p \{\iota_1(p_1) \mapsto \iota_1(p_1) \\ \phantom{t_s \triangleq \lambda hwxzyp. \text{ case } p \{\iota_1(p_1) \mapsto \iota_1(p_1) } \\ \iota_1(p_2) \mapsto \text{ case } (h \dagger x \dagger (sy)) \{\iota_1(a) \mapsto \iota_1(a) | \iota_2(b) \mapsto \iota_2(t_{\le s} p_2 b)\}}.$$

*Proof.* Recall that $\Phi_{A,B}(x, y) = A(x) \lor B_{\le y}$. Let $\mathfrak{s} \in \mathfrak{S}$ be a state, $n, m \in \mathbb{N}$ be natural numbers and $h, u \in \Lambda$ be terms such that $(h; \mathfrak{s}) \in |\forall^{\{\mathrm{st}\}}x.\forall^{\{\mathrm{st}\}}y.(A(x) \lor B(y))|_{\rho}^{\mathfrak{S}}$ and $(u; \mathfrak{s}) \in |\Phi_{A,B}(n, m)|_{\rho}^{\mathfrak{S}} = |A(n) \lor B_{\le m}|_{\rho}^{\mathfrak{S}}$. By construction, we have

$$t_s h \dagger \bar{n} \dagger \bar{m} u \stackrel{\mathfrak{s}}{\downarrow} \text{ case } u \{\iota_1(p_1) \mapsto \iota_1(p_1) \\ \phantom{t_s h \dagger \bar{n} \dagger \bar{m} u \stackrel{\mathfrak{s}}{\downarrow} \text{ case } u \{\iota_1(p_1) \mapsto \iota_1(p_1) } \\ \iota_1(p_2) \mapsto \text{ case } (h \dagger \bar{n} \dagger (s\bar{m})) \{\iota_1(a) \mapsto \iota_1(a) | \iota_2(b) \mapsto \iota_2(t_{\le s} p_2 b)\}}.$$

To conclude by anti-reduction, we need to prove that the term on the right-hand side is in $|A(n) \lor B_{\le S(m)}|_{\rho}^{\mathfrak{S}}$, using the assumption on $u$ and the adequacy of the $(\lor_E)$ rule. The $\iota_1(\cdot)$ case is immediate. For the $\iota_2(\cdot)$ case, let us consider a term $u_2$ such that $(u_2; \mathfrak{s}) \in |B_{\le m}|_{\rho}^{\mathfrak{S}}$ and prove that case $(h \dagger \bar{n} \dagger (s\bar{m})) \{\iota_1(a) \mapsto \iota_1(a) | \iota_2(b) \mapsto \iota_2(t_{\le s} u_2 b)\} \in |\Phi_{A,B}(n, S(m))|_{\rho}^{\mathfrak{S}}$.

Again, we use the assumption on $h$ and the adequacy of the $(\lor_E)$ rule to conclude. Let us consider a term $b$ such that $(b; \mathfrak{s}) \in |B(S(m))|_{\rho}^{\mathfrak{S}}$. It then follows from the assumption on $u_2$ and Lemma 6.4 that $(t_{\le s} u_2 b; \mathfrak{s}) \in |B_{\le S(m)}|_{\rho}^{\mathfrak{S}}$ and hence $(\iota_2(t_{\le s} u_2 b); \mathfrak{s}) \in |A(n) \lor B_{\le S(m)}|_{\rho}^{\mathfrak{S}}$. $\square$

**Corollary 6.8.** Let $A(x)$ and $B(x)$ be any formulas whose only free variable is $x$. Then

$$t_{\Phi} \Vdash (\forall^{\{\mathrm{st}\}}x.\forall^{\{\mathrm{st}\}}y.(A(x) \lor B(y))) \rightarrow \forall^{\{\mathrm{st}\}}x.\forall^{\{\mathrm{st}\}}y.\Phi_{A,B}(x, y),$$

where $t_{\Phi} \triangleq \lambda hwx. \text{ rec}(t_0 h w x)(t_s h w x)$.

*Proof.* Let $\mathfrak{s}$ be a state, $h$ be a term such that $(h; \mathfrak{s}) \Vdash \forall^{\{\mathrm{st}\}}x.\forall^{\{\mathrm{st}\}}y.(A(x) \lor B(y))$, and $n \in \mathbb{N}$ be a natural number. We want to show that $(t_{\Phi} h \dagger \bar{p}; \mathfrak{s}) \Vdash \forall^{\{\mathrm{st}\}}y.\Phi_{A,B}(p, y)$. By definition of $t_{\Phi}$, we have

$$t_{\Phi} h \dagger \bar{n} \stackrel{\mathfrak{s}}{\downarrow} \text{ rec } (t_0 h \dagger \bar{n}) (t_s h \dagger \bar{n}).$$

Then, the result follows directly from External Induction (Proposition 5.10) and Lemmas 6.6 and 6.7. $\square$

We can now take advantage of these terms to define the terms necessary to realize the formula $A_{\le x} \lor B_{\le x}$ where the role of A and B is now made symmetric again, using a second External Induction.

**Lemma 6.9.** For any internal formulas A and B, we have:

$$t_{\Delta} \Vdash (\forall^{\{\mathrm{st}\}}x.\forall^{\{\mathrm{st}\}}y.(A(x) \lor B(y))) \rightarrow \forall^{\{\mathrm{st}\}}x.(A_{\le x} \rightarrow A_{\le S(x)} \lor B_{\le S(x)}),$$

where $t_{\Delta} \triangleq \lambda hwxv. \text{ case } (t_{\Phi} h \dagger (sx) \dagger (sx)) \{\iota_1(c_1) \mapsto \iota_1(t_{\le s} v c_1) | \iota_2(c_2) \mapsto \iota_2(c_2)\}$.
**Proof.** Let $\mathfrak{s} \in \mathfrak{S}$ be a state, $n \in \mathbb{N}$ be a natural number and $h, v \in \Lambda$ two terms such that $(h; \mathfrak{s}) \in |\forall^{\{\mathrm{st}\}}x.\forall^{\{\mathrm{st}\}}y.(A(x) \lor B(y))|_{\mathfrak{S}}$ and $(a; \mathfrak{s}) \in |A_{\le n}|_{\mathfrak{S}}$. By construction, we have

$$t_{\Delta} \dagger \bar{n} a \stackrel{\mathfrak{s}\downarrow}{\searrow} \mathfrak{s} \quad \mathbf{case} \ (t_{\Phi} h \dagger (\mathfrak{sn}) \dagger (\mathfrak{sn})) \{\iota_1(c_1) \mapsto \iota_1(t_{\le \mathfrak{s}} a c_1)|\iota_2(c_2) \mapsto \iota_2(c_2)\}.$$

To conclude by anti-reduction, we need to show that the reduced term realizes $A_{\le S(n)} \lor B_{\le S(n)}$. Using Corollary 6.8, we get that

$$(t_{\Phi} h \dagger (\mathfrak{sn}) \dagger (\mathfrak{sn}); \mathfrak{s}) \Vdash A(S(n)) \lor B_{\le S(n)}.$$

Using the adequacy of the $(\lor_E)$ rule (for which the $\iota_2(\cdot)$ case is immediate), we now have to prove that for any term $v$ such that $(v; \mathfrak{s}) \Vdash A(S(n))$, $t_{\le \mathfrak{s}} av; \mathfrak{s} \Vdash A_{\le S(n)}$. This follows from Lemma 6.4 and the assumptions on $a$ and $v$. $\square$

**Lemma 6.10.** For any internal formulas A and B, we have

$$u_0 \Vdash \left( \forall^{\{\mathrm{st}\}} x. \forall^{\{\mathrm{st}\}} y. (A(x) \lor B(y)) \right) \rightarrow (A_{\le 0} \lor B_{\le 0}),$$

$$\text{where } u_0 \triangleq \lambda h. \mathbf{case} (h \dagger 0 \dagger 0) \{\iota_1(a) \mapsto \iota_1(t_{\le 0} a)|\iota_2(b) \mapsto \iota_1(t_{\le 0} b)\}.$$

**Proof.** Let $\mathfrak{s} \in \mathfrak{S}$ be a state and $h \in \Lambda$ a term such that $(h; \mathfrak{s}) \Vdash \forall^{\{\mathrm{st}\}} x \forall^{\{\mathrm{st}\}} y. (A(x) \lor B(y))$. By construction, we have

$$u_0 h \stackrel{\mathfrak{s}\downarrow}{\searrow} \mathfrak{s} \quad \mathbf{case} (h \dagger 0 \dagger 0) \{\iota_1(a) \mapsto \iota_1(t_{\le 0} a)|\iota_2(b) \mapsto \iota_1(t_{\le 0} b)\}.$$

The result easily follows by anti-reduction, using the adequacy of the $(\lor_E)$ rule and Lemma 6.3. $\square$

**Lemma 6.11.** For any internal formulas A and B, we have

$$u_{\mathfrak{s}} \Vdash \left( \forall^{\{\mathrm{st}\}} x. \forall^{\{\mathrm{st}\}} y. (A(x) \lor B(y)) \right) \rightarrow \forall^{\{\mathrm{st}\}} x. \left( (A_{\le x} \lor B_{\le x}) \rightarrow (A_{\le S(x)} \lor B_{\le S(x)}) \right),$$

$$\text{where } u_{\mathfrak{s}} \triangleq \lambda h w x d. \mathbf{case} d \{\iota_1(d_1) \mapsto t_{\Delta} h w x d_1|\iota_2(d_2) \mapsto t_{\Delta}(t_{\vee} h) w x d_2\}.$$

**Proof.** Let $\mathfrak{s} \in \mathfrak{S}$ be a state, $n \in \mathbb{N}$ a natural number and $h, v \in \Lambda$ be two terms such that $(h; \mathfrak{s}) \Vdash \forall^{\{\mathrm{st}\}} x.\forall^{\{\mathrm{st}\}} y.(A(x) \lor B(y))$ and $(v; \mathfrak{s}) \Vdash A_{\le n} \lor B_{\le n}$. By construction, we have

$$u_{\mathfrak{s}} h \dagger \bar{n} v \stackrel{\mathfrak{s}\downarrow}{\searrow} \mathfrak{s} \quad \mathbf{case} v \{\iota_1(a) \mapsto t_{\Delta} h \dagger \bar{n} a|\iota_2(b) \mapsto t_{\Delta}(t_{\vee} h) \dagger \bar{n} b\}.$$

To conclude by anti-reduction, we use the adequacy of the $(\lor_E)$ rule to prove that the reduced term belongs to $|A_{\le S(n)} \lor B_{\le S(n)}|_{\mathfrak{S}}$. For the $\iota_1(\cdot)$ case, if $w$ is a term such that $(w; \mathfrak{s}) \Vdash A_{\le S(n)}$, then $(t_{\Delta} h \dagger \bar{n} w; \mathfrak{s}) \Vdash A_{\le S(n)} \lor B_{\le S(n)}$ by Lemma 6.9 as expected. The $\iota_2(\cdot)$ case is symmetric, using $t_{\vee}$ and Lemma 6.2. $\square$

**Corollary 6.12.** For any internal formulas A and B, we have

$$t_{\mathrm{aux}} \Vdash \left( \forall^{\{\mathrm{st}\}} x. \forall^{\{\mathrm{st}\}} y. (A(x) \lor B(y)) \right) \rightarrow \forall^{\{\mathrm{st}\}} x. (A_{\le x} \lor B_{\le x}),$$

$$\text{where } t_{\mathrm{aux}} \triangleq \lambda h. \mathbf{rec} (u_0 h) (u_{\mathfrak{s}} h).$$

**Proof.** Let $\mathfrak{s}$ be a state, and $(h; \mathfrak{s}) \Vdash \forall^{\{\mathrm{st}\}} x \forall^{\{\mathrm{st}\}} y(A(x) \lor B(y))$. We have that

$$t_{\mathrm{aux}} h \stackrel{\mathfrak{s}\downarrow}{\searrow} \mathfrak{s} \quad \mathbf{rec} (u_0 h) (u_{\mathfrak{s}} h),$$

so the result easily follows from Proposition 5.10 and Lemmas 6.10 and 6.11. $\square$

We are now ready to prove the main theorem of this section, by combining all the terms into a realizer of LLPO$^{\mathrm{st}}$.
**Theorem 6.13 (LLPO<sup>st</sup>).* Let A and B be internal formulas, we have

$t_{\text{LLPO}} \Vdash \forall^{\{\text{st}\}}x. \forall^{\{\text{st}\}}y. (A(x) \lor B(y)) \rightarrow (\forall^{\{\text{st}\}}x.A(x) \lor \forall^{\{\text{st}\}}y.B(y)),$
where $t_{\text{LLPO}} \triangleq \lambda h. \text{case} (t_{\text{aux}} h \dagger \text{get}) \{\iota_1(x_1) \mapsto \iota_1(t_\delta x_1)|\iota_2(x_2) \mapsto \iota_1(t_\delta x_2)\}$.

*Proof.* For any natural number $n \in \mathbb{N}$, if $(u; \mathfrak{s}) \Vdash \forall^{\{\text{st}\}}x \forall^{\{\text{st}\}}y (A(x) \lor B(y))$ using Corollary 6.12 we get

$$ (t_{\text{aux}} u; \mathfrak{s}) \Vdash \forall^{\{\text{st}\}}x.(\forall^{\{\mathbb{N}\}}z.z \leq x \rightarrow A(z)) \lor (\forall^{\{\mathbb{N}\}}z.z \leq x \rightarrow B(z)). $$

By Transfer (Theorem 5.8), we then obtain

$$ (t_{\text{aux}} u \dagger; \mathfrak{s}) \Vdash \forall^{\{\mathbb{N}\}}x.(\forall^{\{\mathbb{N}\}}z.z \leq x \rightarrow A(z)) \lor (\forall^{\{\mathbb{N}\}}z.z \leq x \rightarrow B(z)), $$
and in particular,

$$ (t_{\text{aux}} u \dagger; \mathfrak{s}) \Vdash \{\text{Nat}(\delta)\} \mapsto (\forall^{\{\mathbb{N}\}}z.z \leq \delta \rightarrow A(z)) \lor (\forall^{\{\mathbb{N}\}}z.z \leq \delta \rightarrow B(z)). $$

Using Proposition 5.5, we get

$$ (t_{\text{aux}} u \dagger \text{get}; \mathfrak{s}) \Vdash (\forall^{\{\mathbb{N}\}}z.z \leq \delta \rightarrow A(z)) \lor (\forall^{\{\mathbb{N}\}}z.z \leq \delta \rightarrow B(z)). $$

Using Lemma 6.5

we indeed get a realizer of $\forall^{\{\text{st}\}}z.A(z) \lor \forall^{\{\text{st}\}}z.B(z)$.

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

## 7. A TAINTED QUOTIENT

In this section we explore the possibility of extending the work done above through a quotient, and the limitations of such construction. In Section 7.1, we explain how this quotient can be obtained in a way that maintains the analogy with the Lightstone-Robinson construction. The resulting theory is indeed an extension in which universal realizers for closed formulas are preserved and more principles are now realizable (e.g. Proposition 7.1). This makes it an even more convincing approach to nonstandard analysis from the point of the captured theory, but not in terms of realizability. Indeed, as we will see in Section 7.2, the terms witnessing the validity of formulas in the quotient can no longer be composed. On the other hand, as explained in Remark 7.6, if one tries to be more faithful to the spirit of realizability, then the connection with nonstandard analysis is less convincing as one loses compatibility with Łoś' theorem. Furthermore, the limitations do not seem to depend on the particular way one defines the quotient, as discussed in Section 7.3.

**7.1. Realizability up to an ultrafilter.** In order to fully mimic Lightstone and Robinson's construction, an extra step is required where one takes a quotient of the interpretation with slices. This step allows us to consider a more flexible notion of realizability where realizers are only required to be compatible with *almost all* states, in the sense that the set of compatible states belongs to the ultrafilter.

In order to simplify the discussion, and similarly to what was done in most of the paper, we don't include disjunction as a primitive connective.

Let us fix a free ultrafilter $\mathcal{U}$ over the set of states. Given any set $V$, we denote by $\cong$ the equivalence relation over $V^{\mathcal{G}}$ defined by $f \cong g \triangleq \{\mathfrak{s} \in \mathcal{G} : f(\mathfrak{s}) = g(\mathfrak{s})\} \in \mathcal{U}$.
First, we can, within the realizability with slices, change the way st(f) is interpreted to consider standardness up to the ultrafilter. In this way, $f \in \mathbb{N}^{\mathfrak{G}}$ is said to be standard if and only if there exists $n \in \mathbb{N}$ s.t. $f \cong n^*$. This allows to show, for instance, that nonstandard natural numbers are larger than standard ones.

**Proposition 7.1.** $\lambda xy.\mathit{loop}^+ \Vdash \forall x, y.\neg\mathit{st}(x) \to \mathit{st}(y) \to y < x$

*Proof.* If $f \in \mathbb{N}^{\mathfrak{G}}$ is a nonstandard individual and $n \in \mathbb{N}$ any natural number, one proves by contradiction that $S = \{\mathfrak{s} \in \mathfrak{S} : n < f(\mathfrak{s})\} \in \mathcal{U}$. Indeed, otherwise one would have $\bar{S} \in \mathcal{U}$.

For any $k \in \mathbb{N}$, let us write $S_k$ for the set $\{\mathfrak{s} \in \mathfrak{S} : f(\mathfrak{s}) = k\}$. Since the sets $S_0, \dots, S_n$ form a partition of $\bar{S}$, it is easy to see that (exactly) one of these sets, say $S_m$, belongs to $\mathcal{U}$. Then $f \cong m^*$, which contradicts the fact that $f$ is nonstandard.

In particular, for any individuals $f, g$, any state $\mathfrak{s}$, and any terms $t, u$ such that $(t; \mathfrak{s}) \in |\mathit{st}(f) \to \perp|^{\mathfrak{G}}$ and $(u; \mathfrak{s}) \in |\mathit{st}(g)|^{\mathfrak{G}}$, we have that $f$ is necessarily nonstandard and that there exists $n \in \mathbb{N}$ such that $g \cong n^*$. By the claim above, we know that there exists $\mathfrak{s}' > \mathfrak{s}$ such that $\mathfrak{s} < f(\mathfrak{s}')$. The result then follows by anti-reduction from the fact that $\mathit{loop}^{+}_{\mathfrak{s}} \downarrow^{\mathfrak{s}'} \mathit{loop}^+$. $\square$

We then need to define a new notion of realizability in which realizers are also considered up to the equivalence relations induced by $\mathcal{U}$. To that end, a natural attempt consists in considering Łoś' theorem as a guideline. For the sake of clarity, let us denote by $|A|^*$ the truth values in this interpretation, which we shall call *realizability up to* $\mathcal{U}$.

**Definition 7.2.** We say that a formula $A$ is *Łoś-reducible* if for any valuation $\rho$ closing $A$, $t \in |A|^*$ if and only if $\{\mathfrak{s} \in \mathfrak{S} : (t; \mathfrak{s}) \in |A|^{\mathfrak{G}}\} \in \mathcal{U}$.

We actually define the interpretation of connectives by this equivalence. For example, the interpretation $|A \to B|^*_{\rho}$ for the implication is defined by

$$ \{t \in \Lambda : \{\mathfrak{s} \in \mathfrak{S} : (t; \mathfrak{s}) \in |A \to B|^{\mathfrak{G}}\} \in \mathcal{U}\}, $$

while the interpretation of the quantifiers is still defined via intersections (resp. unions) over the same domain as in the interpretation with slices (e.g., $|\forall x.A|^*_{\rho} \triangleq \bigcap_{f \in \mathbb{N}^{\mathfrak{G}}} |A|^*_{\rho, x \mapsto f}$).

**Definition 7.3 (Realizability up to** $\mathcal{U}$). The interpretation of a formula $A$ together with a valuation $\rho$ closing $A$ is the set $|A|^*_{\rho}$ defined inductively according to the following clauses:

$$
\begin{align*}
|\mathit{st}(f)|^*_{\rho} &\triangleq \left\{ \begin{array}{ll} \Lambda & \text{if } f \cong n^*, \text{ for some } n \in \mathbb{N} \\ \emptyset & \text{otherwise} \end{array} \right. \\
|X(e_1, \dots, e_n)|^*_{\rho} &\triangleq \{t \in \Lambda : \{\mathfrak{s} \in \mathfrak{S} : (t; \mathfrak{s}) \in \rho(X) \@([e_1]_{\rho}, \dots, [e_n]_{\rho})\} \in \mathcal{U}\} \\
|\{\mathit{Nat}(e)\} \mapsto A|^*_{\rho} &\triangleq \{t \in \Lambda : \{\mathfrak{s} \in \mathfrak{S} : (t; \mathfrak{s}) \in |\{\mathit{Nat}(e)\} \mapsto A|^{\mathfrak{G}}\} \in \mathcal{U}\} \\
|A \to B|^*_{\rho} &\triangleq \{t \in \Lambda : \{\mathfrak{s} \in \mathfrak{S} : (t; \mathfrak{s}) \in |A \to B|^{\mathfrak{G}}\} \in \mathcal{U}\} \\
|A_1 \wedge A_2|^*_{\rho} &\triangleq \{t \in \Lambda : \{\mathfrak{s} \in \mathfrak{S} : (\pi_1(t); \mathfrak{s}) \in |A_1|^{\mathfrak{G}} \wedge (\pi_2(t); \mathfrak{s}) \in |A_2|^{\mathfrak{G}}\} \in \mathcal{U}\} \\
|\forall x.A|^*_{\rho} &\triangleq \bigcap_{f \in \mathbb{N}^{\mathfrak{G}}} |A|^*_{\rho, x \mapsto f} \\
|\exists x.A|^*_{\rho} &\triangleq \bigcup_{f \in \mathbb{N}^{\mathfrak{G}}} |A|^*_{\rho, x \mapsto f} \\
|\forall X.A|^*_{\rho} &\triangleq \bigcap_{F:\mathbb{N}^k \to \mathbf{SAT}} |A|^*_{\rho, X \mapsto F} \\
|\exists X.A|^*_{\rho} &\triangleq \bigcup_{F:\mathbb{N}^k \to \mathbf{SAT}} |A|^*_{\rho, X \mapsto F}
\end{align*}
$$

We write $t \Vdash^* A$ if $t \in |A|^*.$
As shown in the following theorem, first-order quantifiers behave well w.r.t. the ultrafilter.

**Theorem 7.4 (Loś' theorem).** *First-order internal formulas as well as arbitrary conjunctions and implications are Loś-reducible.*

*Proof.* The proof goes by induction on the structure of $A$. In the cases $\{\text{Nat}(e)\} \mapsto A$, $X(e_1, \dots, e_n)$, $A \to B$ and $A \wedge B$, the result follows directly from the definitions. The proof for the quantifiers is similar to the usual proof of Loś' theorem.

∃x.A. By the induction hypothesis, we have that for any $f \in \mathbb{N}^{\mathfrak{G}}$,

$$|A|_{\rho, x \to f}^* = \{t : \{s \in \mathfrak{G} : t; s \in |A|_{\rho, x \to f}^{\mathfrak{G}}\} \in \mathcal{U}\}.$$

By glueing, we have that $|A|_{\rho, x \to f}^{\mathfrak{G}} = |\overline{A}|_{\rho, x \to f}^{\mathfrak{G}} = |\overline{A}|_{\rho, x \to (f(\mathfrak{S}))^*}^{\mathfrak{G}}$. We want to prove that for any $t \in \Lambda$

$$\exists f \in \mathbb{N}^{\mathfrak{G}}. t \in |A|_{\rho, x \to f}^* \text{ iff } \{s \in \mathfrak{G} : t; s \in |\exists x. A|_{\rho}^{\mathfrak{G}}\} \in \mathcal{U}.$$

Observe that, by glueing, the right-hand side is equivalent to

$$\{s \in \mathfrak{G} : \exists n \in \mathbb{N}. t \in |A|_{\rho, x \to n}^{\mathfrak{G}}\} \in \mathcal{U}.$$

⇒ Assume that there exists $f \in \mathbb{N}^{\mathfrak{G}}$ such that $t \in |A|_{\rho, x \to f}^*$. Then it is easy to see that

$$\{s \in \mathfrak{G} : t \in |A|_{\rho, x \to (f(\mathfrak{S}))^*}^{\mathfrak{G}}\} \subseteq \{s \in \mathfrak{G} : \exists n \in \mathbb{N}. t \in |A|_{\rho, x \to n}^{\mathfrak{G}}\},$$

and hence the result follows from the upwards closure of the ultrafilter.

⇔ Assume now that $E \triangleq \{s \in \mathfrak{G} : \exists n \in \mathbb{N}. t \in |A|_{\rho, x \to n}^{\mathfrak{G}}\} \in \mathcal{U}$.

For any $s \in E$, using countable choice we can pick an integer $n_s$ such that $t \in |A|_{\rho, x \to n_s}^{\mathfrak{G}}$. We may then define the function $g \in \mathbb{N}^{\mathfrak{G}}$ by:

$$g(s) \triangleq \begin{cases} n_s & \text{if } s \in E \\ 0 & \text{otherwise} \end{cases}$$

By definition, $E \subseteq \{s \in \mathfrak{G} : t \in |A|_{\rho, x \to (g(\mathfrak{S}))^*}^{\mathfrak{G}}\}$, hence this set belongs to $\mathcal{U}$ by upwards closure. By induction hypothesis we conclude that $t \in |A|_{\rho, x \to f}^*$.

∀x.A. By the induction hypothesis, for any $f \in \mathbb{N}^{\mathfrak{G}}$,

$$|A|_{\rho, x \to f}^* = \{t : \{s \in \mathfrak{G} : t; s \in |A|_{\rho, x \to f}^{\mathfrak{G}}\} \in \mathcal{U}\}.$$

By glueing, $|A|_{\rho, x \to f}^{\mathfrak{G}} = |\overline{A}|_{\rho, x \to f}^{\mathfrak{G}} = |\overline{A}|_{\rho, x \to (f(\mathfrak{S}))^*}^{\mathfrak{G}}$. We want to prove that for any $t \in \Lambda$

$$\forall f \in \mathbb{N}^{\mathfrak{G}}. t \in |A|_{\rho, x \to f}^* \text{ iff } \{s \in \mathfrak{G} : t; s \in |\forall x. A|_{\rho}^{\mathfrak{G}}\} \in \mathcal{U}.$$

Observe that, by glueing, the right-hand side is equivalent to

$$S \triangleq \{s \in \mathfrak{G} : \forall n \in \mathbb{N}. t \in |A|_{\rho, x \to n}^{\mathfrak{G}}\} \in \mathcal{U}.$$

⇒ We easily see that for any $f \in \mathbb{N}^{\mathfrak{G}}$

$$S = \{s \in \mathfrak{G} : \forall f \in \mathbb{N}^{\mathfrak{G}}. t |A|_{\rho, x \to (f(\mathfrak{S}))^*}^{\mathfrak{G}}\} \subseteq \{s \in \mathfrak{G} : t \in |A|_{\rho, x \to (f(\mathfrak{S}))^*}^{\mathfrak{G}}\}$$

and by upwards closure we conclude that $t \in |A|_{\rho, x \to f}^*$.
By contraposition, assume that $\{\mathfrak{s} \in \mathfrak{S} : \forall n \in \mathbb{N}. t \in |A|_{\rho, x \mapsto n^*}^s\} \notin \mathcal{U}$ and let us show that there exists $f \in \mathbb{N}^{\mathfrak{S}}$ such that $t \notin |A|_{\rho, x \mapsto f}^s$. Because $\mathcal{U}$ is an ultrafilter, the assumption is equivalent to:

$$E = \overline{\{\mathfrak{s} \in \mathfrak{S} : \forall n \in \mathbb{N}. t \in |A|_{\rho, x \mapsto n^*}^s\}} = \{\mathfrak{s} \in \mathfrak{S} : \exists n \in \mathbb{N}. t \notin |A|_{\rho, x \mapsto n^*}^s\} \in \mathcal{U}.$$

We are essentially left with a situation similar to the existential case: for any $\mathfrak{s} \in E$, using countable choice we can pick an integer $n_\mathfrak{s}$ such that $t \notin |A|_{\rho, x \mapsto n_\mathfrak{s}}^s$. We can then define the function $g \in \mathbb{N}^{\mathfrak{S}}$ such that for any $\mathfrak{s} \in E$, $g(\mathfrak{s}) = n_\mathfrak{s}$. Hence $E \subseteq \{\mathfrak{s} \in \mathfrak{S} : t \notin |A|_{\rho, x \mapsto (g(\mathfrak{s}))^*}^s\}$, and we conclude that $t \notin |A|_{\rho, x \mapsto f}^*$. □

**Theorem 7.4** implies that if a term $t$ is a realizer of a first-order internal formula $A$ “often enough” in the interpretation with slices, then $t$ is still a realizer in the interpretation up to $\mathcal{U}$. Since all the realizers in Section 5 were universal, they are still realizers in this new setting, meaning that all the results from that section remain valid in the interpretation up to $\mathcal{U}$. In particular, Theorem 7.4 applies to Transfer, Idealization, Overspill or Underspill.

A simple example illustrating this new interpretation is the formula $\forall^{\text{st}}x.x < \delta$, which was realized by $\text{loop}^+$ in the interpretation with slices (see Proposition 5.14) and is now realized by any term (because for any $n \in \mathbb{N}$, the set of states such that $n < \delta$ is equal to $[n; +\infty[$ which belongs to $\mathcal{U}$). Similarly, $\text{loop}^+$ can be replaced by $\dagger$ in Proposition 7.1. More generally, such a quotient allows us to get realizers for principles that were inaccessible in the interpretation with slices (e.g., $\forall x, y. \neg \text{st}(x) \to \text{st}(y) \to y < x$) but are usually valid in nonstandard interpretations.

A more involved example concerns the Standardization principle: *prima facie* this principle does not seem to be realizable with the current definitions, but it is available for Łoś-reducible formulas that are specified by the previous theorem. Technically, to internalize this in our interpretation would require to go to higher-order logic in order to refer to standard predicates in the syntax. In fact, this should not be a problem, as shown by the fact that our interpretation induces an evidenced frame (see Section 4.4), which is known in turn to induce triposes, hence a model of higher-order logic.

For the sake of simplicity, we will just consider standard predicates through their semantical characterization, that is the ones induced by predicates in Definition 3.2, i.e. whose value is identical in each slice. Assume that we are given a Łoś-reducible formula $A(x)$, which we identify with the truth-value function it induces $A : n \in \mathbb{N} \mapsto |A(n)|_{\rho}^{\mathfrak{S}}$, together with a standard predicate $\mathbb{X}$ (which is then Łoś-reducible as well). Restricted to this setting, Standardization states that there exists a standard predicate $\mathbb{Y}$ such that for any standard natural number $n \in \mathbb{N}$, we have:

$$\exists t.t \Vdash^* \mathbb{Y}(n^*) \iff \exists t.t \Vdash^* \mathbb{X}(n^*) \wedge \mathbb{A}(n^*)$$

Since $\mathbb{A}$, $\mathbb{X}$ and arbitrary conjunctions are Łoś-reducible, it is enough to consider the following standard predicate (seen via the function from $\mathbb{N}$ to $\mathcal{A}$ inducing its actual value in the interpretation with slices):

$$\mathbb{Y}(n) \triangleq \{t \in \mathcal{A} : \{\mathfrak{s} \in \mathfrak{S} : t \Vdash \mathbb{X}(n^*) \wedge \mathbb{A}(n^*)\} \in \mathcal{U}\}$$

Before taking a quotient, the definitions in Section 4.2 gave us access to Standardization for internal formulas. In the current setting, the restriction to Łoś-reducible formulas is necessary to make it work with the quotient. This is to be compared with Lightstone-Robinson's
construction, where all internal formulas are Łoś-reducible, an analogous definition gives access to Standardization for these formulas. Nonetheless, to validate the unrestricted principle of Standardization (that is, where A is any formula), one usually needs to use a more involved construction of a model by means of an adequate ultralimit, and the proof that Standardization holds relies on transfinite reasoning and the full Axiom of Choice. None of these principles being computationally interpretable in our setting, it seems that the restricted statement above is the best we can do here.

**7.2. Limitations of the construction.** While the quotient from the previous subsection allows to capture a theory which is even closer to “usual” nonstandard analysis, it has some drawbacks with respect to its realizability facet. The main drawback, which is highlighted in Remark 7.6, concerns the interpretation of implication. First, let us connect the interpretation of implication through the quotient with the expected interpretation in usual realizability settings.

**Proposition 7.5.** For any internal formulas A and B, and any valuation $\rho$ closing both A and B, we have $|A \to B|_{\rho}^* \subseteq \{t : \forall u \in |A|_{\rho}^*. t u \in |B|_{\rho}^*\}$.

*Proof.* For any term $t$ and any formula A, let us denote by $S_t^A$ the set $\{\mathfrak{s} \in \mathfrak{G} : (t; \mathfrak{s}) \in |A|_{\rho}^{\mathfrak{G}}\}$. Let $t \in \Lambda$ be such that $S_t^{A \to B} \in \mathcal{U}$ and $u \in |A|_{\rho}^*$. By hypothesis, $S_u^A \in \mathcal{U}$. We need to show that $tu \in |B|_{\rho}^*$. Again, for any $\mathfrak{s} \in S_t^{A \to B} \cap S_u^A \in \mathcal{U}$, we have $tu; \mathfrak{s} \in |B|_{\rho}^{\mathfrak{G}}$. By upwards closure, we deduce that $\{\mathfrak{s} : (tu; \mathfrak{s}) \in |B|_{\rho}^{\mathfrak{G}}\} \in \mathcal{U}$, hence $tu \in |B|_{\rho}^*$, and the result follows from Theorem 7.4. By Theorem 7.4, we have

$$|A|_{\rho}^{*} = \{u \in \Lambda : \{\mathfrak{s} \in \mathfrak{G} : (u; \mathfrak{s}) \in |A|_{\rho}^{\mathfrak{G}}\} \in \mathcal{U}\} \quad \text{and} \\ |B|_{\rho}^{*} = \{v \in \Lambda : \{\mathfrak{s} \in \mathfrak{G} : (v; \mathfrak{s}) \in |B|_{\rho}^{\mathfrak{G}}\} \in \mathcal{U}\}.$$

For any term $t$ and any formula A, let us denote by $S_t^A$ the set $\{\mathfrak{s} \in \mathfrak{G} : (t; \mathfrak{s}) \in |A|_{\rho}^{\mathfrak{G}}\}$.

Let $t \in \Lambda$ be such that $S_t^{A \to B} \in \mathcal{U}$ and $u \in |A|_{\rho}^*$. By hypothesis, $S_u^A \in \mathcal{U}$. We need to show that $tu \in |B|_{\rho}^*$. Again, for any $\mathfrak{s} \in S_t^{A \to B} \cap S_u^A \in \mathcal{U}$, we have $tu; \mathfrak{s} \in |B|_{\rho}^{\mathfrak{G}}$. By upwards closure, we deduce that $\{\mathfrak{s} : (tu; \mathfrak{s}) \in |B|_{\rho}^{\mathfrak{G}}\} \in \mathcal{U}$, hence $tu \in |B|_{\rho}^*$, and the result follows. $\square$

**Remark 7.6.** One could have been tempted to define the truth value $|A \to B|_{\rho}^*$ as the set of terms $t$ such that for any $u \in |A|_{\rho}^*$, $tu \in |B|_{\rho}^*$, as is usual in realizability. Unfortunately, such a definition is incompatible with Theorem 7.4, as the other inclusion in Proposition 7.5 does not hold. To see this, let $A \triangleq \text{Nat}'(\tau)$ and $B \triangleq \perp$ where $\tau$ is a non-computable function$^6$ $\tau : \mathfrak{G} \to \mathbb{N}$ for which there is no term $u$ such that $\forall \mathfrak{s}. u^s \downarrow^s \tau(\mathfrak{s})$. By construction, we have that $|A|^* = \emptyset$, so that obviously for any $u \in |\text{Nat}'(\tau)|^*$, the function $(\lambda x.x) u \in |\perp|^*$. Yet, for each state $\mathfrak{s}$ the truth value $|\text{Nat}'(\tau)|_{\rho}^{\mathfrak{G}}$ is not empty (it contains at least $(\bar{n}, \mathfrak{s})$, for $n = \tau(\mathfrak{s})$) and therefore $(\lambda x.x; \mathfrak{s}) \notin |\text{Nat}'(\tau) \to \perp|_{\rho}^{\mathfrak{G}}$ (since for any $(u; \mathfrak{s}) \in |\text{Nat}'(\tau)|^{\mathfrak{G}}$, $((\lambda x.x) u; \mathfrak{s}) \notin |\perp|^*$).

As it turns out, Definition 7.3 is not as compositional as one would expect in realizability. Indeed, we can compose a realizer $t \in |A \to B|_{\rho}^*$ with a realizer in $u \in |A|_{\rho}^*$ to get $tu \in |B|_{\rho}^*$, but the $(\to_I)$-rule is not adequate when considering substitutions of variables by realizers in the quotiented truth values. In particular, Remark 7.6 emphasizes that the structure of

<footnote>$^6$To that end, one can for instance consider the function $\tau$ which to each $\mathfrak{s} \in \mathfrak{G}$ associates the smallest natural number $n \in \mathbb{N}$ such that there is no term of size smaller than or equal to $\mathfrak{s}$ that computes $n$ the state $\mathfrak{s}: \tau(\mathfrak{s}) \triangleq \inf\{n \in \mathbb{N} : \neg \exists t. |t| \le \mathfrak{s} \wedge t^s \downarrow^s \bar{n}\}$.</footnote>
this interpretation does not induce an evidenced frame, since it is not possible to define the function $\lambda : E \to E$ necessary to interpret implication.

**7.3. Stranger things.** As mentioned above, Remark 7.6 highlights the existence of “counter-intuitive” peculiarities of the interpretation up to $\mathcal{U}$ with respect to the quotient in the Lightstone-Robinson construction. The latter indeed appears to be more regular, seemingly for two main reasons.

First, while the Lightstone-Robinson construction is based on Boolean-valued models, realizability interpretations associate to each formula a set of realizers (instead of one unique Boolean). Besides, the use of relativized quantifiers (for instance in the statement for Idealization) forces us to use only computable functions<fnref n="7" />.

Second, as highlighted in Section 4, in the stateful interpretation the set instruction allows terms to change the value of the states during computations, and thus of the slices. This phenomenon does not occur in the Lightstone-Robinson construction where slices of the product are completely separated between them. In fact, the ability of reading the value of the slice already implies that propositional internal formulas do not induce standard truth values, which is counter-intuitive.

**Proposition 7.7.** There exists an internal propositional formula $A$, a term $t$ and two states $s_0, s_1$ such that $(t; s_0) \in |A|^\mathcal{S}$ but $(t; s_1) \notin |A|^\mathcal{S}$.

*Proof.* Take for instance $A \triangleq (A_1 \wedge \neg A_1) \to A_1$, $t \triangleq \text{rec}(\lambda x.\pi_1(x)) (\lambda xyz.\pi_2(z)) \text{get}$, $s_0 = 0$ and $s_1 = 1$. We have:

* $(t; 0) \in |A|^\mathcal{S}$: for any $(u; 0) \in |A_1 \wedge \neg A_1|^\mathcal{S}$, $u^0 \downarrow^s (u_1, u_2)$ with $(u_1; s) \in |A_1|^\mathcal{S}$, and $t^0 \downarrow^0 (\text{rec}(\lambda x.\pi_1(x)) (\lambda xyz.\pi_2(z)) 0) u^0 \downarrow^0 (\lambda x.\pi_1(x)) u^0 \downarrow^0 \pi_1(u) u_1^0 \downarrow^s u_1$.

The result follows by anti-reduction.

* $(t; 1) \notin |A|^\mathcal{S}$: for any $(u; 1) \in |A_1 \wedge A_2|^\mathcal{S}$, $u^1 \downarrow^s (u_1, u_2)$ with $(u_2; s) \in |\neg A_1|^\mathcal{S}$, and $t^1 \downarrow^1 (\text{rec}(\lambda x.\pi_1(x)) (\lambda xyz.\pi_2(z)) 1) u^1 \downarrow^1 (\lambda xyz.\pi_2(z)) 0 (\text{rec}...) u^1 \downarrow^1 \pi_2(u) u_2^1 \downarrow^s u_2$.

Since $(u_2; 1) \in |\neg A_1|^\mathcal{S}$, it cannot be the case that $(u_2; 1) \in |A_1|^\mathcal{S}$.

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

As explained above, the interpretation briefly introduced in Section 7.1 is an attempt to provide a quotient, guided by the rationale of Łoś' theorem. Nonetheless, there might be more refined ways to arrive at a satisfying definition of a quotient. In particular, Definition 7.3 does not take the computation into account when defining the quotient, which turns out to be problematic as Remark 7.6 shows. Therefore, it could be tempting to contemplate a notion of reduction up to $\mathcal{U}$ as follows

$$t \downarrow^l u \triangleq \{s \in \mathcal{S} : \exists s'. t^s \downarrow^{s'} u\} \in \mathcal{U}$$

Nonetheless, such a definition leaves us even further from our goal since the induced realizability interpretation would present a lot of counter-intuitive peculiarities. We illustrate some of these peculiarities in the following propositions, for which we consider a free ultrafilter $\mathcal{U}$ on $\mathcal{S}$ and, without loss of generality, assume that $\{s \in \mathcal{S} : \exists n \in \mathbb{N}. s = 2n\} \in \mathcal{U}$. In particular, this implies that $\{s \in \mathcal{S} : \exists n \in \mathbb{N}. s = 2n + 1\} \notin \mathcal{U}$. We will say that a property occurs *often enough* when the set of states for which it is valid belongs to $\mathcal{U}$.

<footnote n="7">⁷This is the reason why, for instance, the premise of Idealization needs to be restricted to the existence of a standard natural number $x$, instead of any natural number as is usually the case.</footnote>
The next proposition shows the existence of a formula A and two terms t and u such that u is often enough a realizer and t reduces often enough to u, but never to a slice in which it is a realizer.

**Proposition 7.8.** *There exist a formula A, a valuation $\rho$ closing A and two terms t, u such that*

$$ (1) \quad \{\mathfrak{s} \in \mathfrak{S} : (u; \mathfrak{s}) \in |A|_{\rho}^{\mathfrak{S}}\} \in \mathcal{U} $$

$$ (2) \quad \{\mathfrak{s} \in \mathfrak{S} : \exists \mathfrak{s}', t^s \downarrow^{s'} u\} \in \mathcal{U} $$

$$ (3) \quad \forall \mathfrak{s}, \mathfrak{s}', t^s \downarrow^{s'} u \Rightarrow (u; \mathfrak{s}') \notin |A|_{\rho}^{\mathfrak{S}}. $$

*Proof.* Consider the (nonstandard) individual $\tau$ defined by $\tau: n \in \mathbb{N} \mapsto n \bmod 2$ (i.e $\tau(2n) = 0$ and $\tau(2n+1) = 1$). By construction, we have

$$ |\tau = 0^*|^{\mathfrak{S}} = \{(t; \mathfrak{s}) \in \Lambda \times \mathfrak{S} : \exists n \in \mathbb{N}, \mathfrak{s} = 2n\}. $$

Let us now define a function $f$ which, given any integer $n \in \mathbb{N}$, computes the lowest odd number greater than or equal to $n$: $f(0) = 1$, $f(1) = 1$, $f(2) = 3$, etc. It is clear that this function is primitive recursive, hence there is a term `next odd` that computes it. We let $u \triangleq \lambda x.x$ and $t \triangleq \text{set}(\text{next odd get})u$. For any state $\mathfrak{s} \in \mathfrak{S}$, we then have

$$ t = \text{set}(\text{next\_odd get}) u^s \downarrow^s \text{set}(\text{next\_odd s}) u^s \downarrow^s \text{set} \overline{f(s)} u^s \downarrow^{f(s)} u, $$

where $f(s)$ is odd. Hence, if we define $A \triangleq x = 0^*$ and $\rho = x \mapsto \tau$, we have

$$ (1) \quad \{\mathfrak{s} \in \mathfrak{S} : (u; \mathfrak{s}) \in |\tau = 0^*|^{\mathfrak{S}}\} = \{\mathfrak{s} \in \mathfrak{S} : \exists n \in \mathbb{N}, \mathfrak{s} = 2n\} \in \mathcal{U} $$

$$ (2) \quad \{\mathfrak{s} \in \mathfrak{S} : \exists \mathfrak{s}', t^s \downarrow^{s'} u\} = \mathfrak{S} \in \mathcal{U} $$

$$ (3) \quad \text{for any } \mathfrak{s}, t^s \downarrow^{f(s)} u \text{ and } (u; f(\mathfrak{s})) \notin |A|^{\mathfrak{S}} \text{ since } f(\mathfrak{s}) \text{ is odd.} \quad \square $$

The next result shows that even if there are enough slices in which $t$ reduces to $u$ in a slice that makes it a realizer of some formula A, $u$ may not be a realizer of A often enough.

**Proposition 7.9.** *There exist an atomic formula A, a valuation $\rho$ closing A and two terms t, u such that*

$$ (1) \quad \{\mathfrak{s} \in \mathfrak{S} : \exists \mathfrak{s}', t^s \downarrow^{s'} u \wedge (u; \mathfrak{s}') \in |A|_{\rho}^{\mathfrak{S}}\} \in \mathcal{U} $$

$$ (2) \quad \{\mathfrak{s} \in \mathfrak{S} : (u; \mathfrak{s}) \in |A|_{\rho}^{\mathfrak{S}}\} \notin \mathcal{U}. $$

*Proof.* Take again the (nonstandard) individual $\tau$ defined by $\tau: n \in \mathbb{N} \mapsto n \bmod 2$, $\rho \triangleq x \mapsto \tau$ and $A \triangleq x = 1^*$. Let us define $u \triangleq \lambda x.x$, $\text{incr} \triangleq \lambda x.\text{set}(\mathfrak{s} \text{ get}) x t \triangleq \text{incr} u$. By construction, we have that $|\tau = 1|^{\mathfrak{S}} = \{(v; \mathfrak{s}) : \exists n \in \mathbb{N}, \mathfrak{s} = 2n + 1\}$ and $t = \text{set}(\text{get} + 1) u^s \downarrow^{s+1} u$. Hence

$$ (1) \quad \{\mathfrak{s} \in \mathfrak{S} : \exists \mathfrak{s}', t^s \downarrow^{s'} u \wedge (u; \mathfrak{s}') \in |A|_{\rho}^{\mathfrak{S}}\} = \{\mathfrak{s} \in \mathfrak{S} : \exists n. \mathfrak{s} = 2n\} \in \mathcal{U} $$

$$ (2) \quad \{\mathfrak{s} \in \mathfrak{S} : (u; \mathfrak{s}) \in |A|_{\rho}^{\mathfrak{S}}\} = \{\mathfrak{s} \in \mathfrak{S} : \exists n. \mathfrak{s} = 2n + 1\} \notin \mathcal{U}. \quad \square $$

## 8. RELATED AND FUTURE WORK

8.1. **Related work.** Some related works concern notions of realizability for nonstandard arithmetic which are variants of Kreisel's modified realizability [BBS12, DG18]. These notions of realizability are more inspired by Nelson's syntactical approach to nonstandard analysis. In particular, they rely on translations of formulas inducing conservative extensions of Heyting arithmetic. To draw a comparison with Van den Berg et al.'s work, it should be observed that they interpret standard elements as finite sequences that can be thought
of as a process of accumulating potential witnesses. In particular, their interpretation crucially relies on a monotonicity property for these sequences (regarding sequence inclusion), stating that realizers are provably upwards-closed [BBS12, Lemma 5.4]. This property has no counterpart in our setting. On the other hand, our interpretation is able to give computational content to nonstandard individuals, and even to give explicit nonstandard elements (such as the diagonal) with their corresponding realizers. This is, for example, what allows us to computationally interpret Idealization (see Theorem 5.16), whereas the functional interpretation for Idealization in [BBS12] is trivial in the sense that the interpretations of the premise and the conclusion of any instance of Idealization are identical. It could be interesting to better understand the relation between this approach and the approaches based on Kreisel's realizability. In particular, we would like to know whether we can obtain a preservation result for some class of formulas (e.g. internal, quantifier-free, $∃$-free formulas).

Similar ideas have been addressed by Aschieri. In [Asc17] the author uses a notion of state which allows to construct a forcing model. In particular, natural numbers are interpreted as functions from states to $N$. Yet, his work does not pay attention to the nonstandard principles that can be obtained in his setting but rather to forcing. It would be natural to investigate whether our setting also allows for forcing techniques. This connection with forcing is reinforced by the fact that in the realm of Krivine's realizability, which generalizes Cohen's forcing, the latter is given a computational content via the addition of a monotone memory cell to the abstract machine in order to store forcing conditions [Kri11, Miq11b]. Also, recent work of Powell has been focusing on a variant of Gödel's functional interpretation to take into account stateful computations [Pow18]. In addition to investigating the computational contents of the stateful programs obtained by extraction through this interpretation, the author proposes some problems that the reader might find interesting.

**8.2. Weak Kőnig's Lemma.** As shown in [DF17], $WKL_0$ (one of the Big Five systems from Reverse Mathematics) is interpretable, over a nonstandard version of primitive recursive arithmetic with extensionality, using a version of the Axiom of Choice and Idealization. It relies on distinguishing two sorts: the number sort is interpreted by the standard numbers, and the set sort is interpreted by bounded type 1 functionals (or by number codes, both standard and nonstandard, of finite sets of numbers, again both standard and nonstandard).

Recall that Weak Kőnig's Lemma states that every infinite binary tree has an infinite branch. As it turns out, in that context to say that $T$ is a tree is to say two things: (i) every standard natural number which is in the tree is the code of a binary sequence and (ii) if some standard $\sigma$ is in the tree and the binary sequence coded by a standard element $\tau$ is an initial segment of the binary sequence coded by $\sigma$, then $\tau$ is also on the tree. The interpretation of being infinite is a formula saying that for every standard natural number $\sigma$ there exists a standard element with length $w$ which is in the tree. The proof then relies on showing that an element $\alpha$, defined exactly as $\sigma$ below and at $w$ and 0 from there onwards can be turned into an infinite branch with the use of Idealization.

So, the interpretation of Weak Kőnig's Lemma crucially relies on the ability to manipulate trees and on Idealization. Of course, in our setting, we have an explicit (nontrivial) realizer for Idealization, so, in principle, it should be possible to give a realizer for Weak Kőnig's Lemma. However, that would require a whole reformulation of the framework in order to have an explicit access to trees instead of a noncomputational second-order quantification.
**Horizons.** The work done in this paper raises some natural questions of which we mention a few, as possible lines of investigation.

A first natural question comes from the fact that prior interpretations of nonstandard arithmetic, such as [BBS12, DG18, FG15] (and also [FO05] and [FN06] in a context that does not involve nonstandard arithmetic), restrict quantifiers by bounding the variables under their scope. It is then pertinent to ask whether this could be given a more computational interpretation as we do here, in order to see it as some kind of “computation up to (the bound)”.

A second possible path would be to reformulate our interpretations in order to account for classical logic by using control operators as is usual in Krivine’s realizability [Kri09]. Alas, our attempts in that direction have not been very fruitful, mostly because Krivine’s interpretation crucially relies on an orthogonality relation between terms and evaluations contexts (which is reminiscent of the duality of computation in classical logic [CH00]). In terms of the ultrafilter, this would require some sort of perfect balance to make the quotient compatible with this orthogonality relation which so far has eluded us. This is similar to the limitations pointed out in Section 7.2.

Thirdly, there is a very active line of research in realizability concerning the interpretation of various choice principles. In particular, the use of states or memoization has proven to be useful for interpreting dependent choice (e.g. in [BBC98], [Her12] or [CFT19], to name but a few) or Double Negation Shift (DNS) (in [Blo22], Blot uses an “update recursion” mechanism to realize DNS). At the same time, DNS is also interesting in itself as a non-intuitionistic principle. This is particularly relevant since our setting interprets (a version of) the LLPO principle, which means that we are somewhere between intuitionistic and classical logic. Furthermore, DNS is also known to be interpretable using bar recursion, which raises the question of knowing whether our interpretation could be compatible with such an operator.

Finally, we would like to mention that Brede and Herbelin’s [BH21] establishes a hierarchy of choice principles, relating in particular tree-based choices principles and their dual bar induction-based principles. Many of the principles they study are not attached to a precise computational content so far, and so it would be interesting to see if there exist specific interpretations that could capture exactly each of these principles, and, in particular, “lower” instances of their generalized dependent choice or generalized bar induction principles.

## REFERENCES

[Asc17] Federico Aschieri. Constructive forcing, CPS translations and witness extraction in interactive realizability. *Mathematical Structures in Computer Science*, 27(6):993–1031, 2017. doi:10.1017/S0960129515000468.

[Avi05] Jeremy Avigad. *Weak theories of nonstandard arithmetic and analysis*, page 19–46. Lecture Notes in Logic. Cambridge University Press, 2005. doi:10.1017/9781316755846.003.

[Bar92] Henk Barendregt. Lambda calculi with types. In S. Abramsky, Dov M. Gabbay, and S. E. Maibaum, editors, *Handbook of Logic in Computer Science (Vol. 2)*, pages 117–309. Oxford University Press, Inc., New York, NY, USA, 1992. doi:10.1017/CBO9781139032636.

[BBC98] Stefano Berardi, Marc Bezem, and Thierry Coquand. On the computational content of the axiom of choice. *J. Symb. Log.*, 63(2):600–622, 1998. URL: http://dx.doi.org/10.2307/2586854, doi:10.2307/2586854.

[BBE$^{+}$18] Jacques Bair, Piotr Blaszczyk, Robert Ely, Peter Heinig, and Mikhail Katz. Leibniz’s well-founded fictions and their interpretations. *Mat. Stud.*, 49(2):186–224, 2018. doi:10.15330/ms.49.2.186-224.
[BBG$^{+}$20] Jacques Bair, Piotr Błaszczyk, Elías Guillén, Peter Heinig, Vladimir Kanovei, and Mikhail G. Katz. Continuity between Cauchy and Bolzano: issues of antecedents and priority. *British Journal for the History of Mathematics*, pages 1–18, 2020. doi:10.1080/26375451.2020.1770015.

[BBS12] Benno van den Berg, Eyvind Briseid, and Pavol Safarik. A functional interpretation for nonstandard arithmetic. *Ann. Pure Appl. Logic*, 163(12):1962–1994, 2012. doi:10.1016/j.apal.2012.07.003.

[BH21] Nuria Brede and Hugo Herbelin. On the logical structure of choice and bar induction principles. In *2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, pages 1–13, 2021. doi:10.1109/LICS52264.2021.9470523.

[Blo22] Valentin Blot. A direct computational interpretation of second-order arithmetic via update recursion. In *Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '22*, New York, NY, USA, 2022. Association for Computing Machinery. doi: 10.1145/3531130.3532458.

[BR87] Douglas Bridges and Fred Richman. *Varieties of constructive mathematics*, volume 97 of *London Mathematical Society Lecture Note Series*. Cambridge University Press, Cambridge, 1987. doi: 10.1017/CBO9780511565663.

[Cal92] Jean-Louis Callot. Trois leçons d'analyse infinitésimale. In J.M. Salanskis and H. Sinaceur, editors, *Le labyrinthe du continu*, pages 369–381. Springer-Verlag, Paris, 1992.

[CFT19] Liron Cohen, Sofia Abreu Faro, and Ross Tate. The effects of effects on constructivism. *Electronic Notes in Theoretical Computer Science*, 347:87–120, 2019. Proceedings of the Thirty-Fifth Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXV). doi: 10.1016/j.entcs.2019.09.006.

[CH00] Pierre-Louis Curien and Hugo Herbelin. The duality of computation. In *Proceedings of ICFP 2000*, SIGPLAN Notices 35(9), pages 233–243. ACM, 2000. doi:10.1145/351240.351262.

[CMT21] Liron Cohen, Étienne Miquey, and Ross Tate. Evidenced frames: A unifying framework broadening realizability models. In *2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, pages 1–13, 2021. doi:10.1109/LICS52264.2021.9470514.

[DF17] Bruno Dinis and Fernando Ferreira. Interpreting weak König's lemma in theories of nonstandard arithmetic. *Mathematical Logic Quarterly*, 63(1-2):114–123, 2017. doi:10.1002/malq.201600066.

[DG18] Bruno Dinis and Jaime Gaspar. Intuitionistic nonstandard bounded modified realizability and functional interpretation. *Ann. Pure Appl. Logic*, 169(5):392–412, 2018. doi:10.1016/j.apal. 2017.12.004.

[DM21] Bruno Dinis and Étienne Miquey. Realizability with stateful computations for nonstandard analysis. In *29th EACSL Annual Conference on Computer Science Logic*, volume 183 of *LIPIcs. Leibniz Int. Proc. Inform.*, pages Art. No. 19, 23. Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2021. doi:10.4230/LIPIcs.CSL.2021.19.

[DvdB19] Bruno Dinis and Imme van den Berg. *Neutrices and external numbers: A flexible number system*. Monographs and Research Notes in Mathematics. CRC Press, Boca Raton, FL, 2019. With a foreword by Claude Lobry. doi:10.1201/9780429291456.

[FG15] Fernando Ferreira and Jaime Gaspar. Nonstandardness and the bounded functional interpretation. *Annals of Pure and Applied Logic*, 166(6):701–712, June 2015. doi:10.1016/j.apal.2015.02.001.

[FN06] Fernando Ferreira and Ana Nunes. Bounded modified realizability. *The Journal of Symbolic Logic*, 71(1):329–346, March 2006. doi:10.2178/jsl/1140641178.

[FO05] Fernando Ferreira and Paulo Oliva. Bounded functional interpretation. *Annals of Pure and Applied Logic*, 135(1-3):73–112, September 2005. doi:10.1016/j.apal.2004.11.001.

[Gri90] Timothy Griffin. A formulae-as-type notion of control. In *Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, POPL '90, pages 47–58, New York, NY, USA, 1990. ACM. doi:10.1145/96709.96714.

[Gö58] Kurt Gödel. Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. *Dialectica*, 12(3-4):280–287, 1958. doi:10.1111/j.1746-8361.1958.tb01464.x.

[Her12] Hugo Herbelin. A constructive proof of dependent choice, compatible with classical logic. In *Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012*, pages 365–374. IEEE Computer Society, 2012. URL: http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=6275587, doi: 10.1109/LICS.2012.47.
[Hey34] Arend Heyting. *Mathematische Grundlagenforschung. Intuitionismus. Beweistheorie*. Springer-Verlag, Berlin, 1934. doi:10.1007/978-3-642-65617-0.

[HvdB17] Amar Hadzihasanovic and Benno van den Berg. Nonstandard functional interpretations and categorical models. *ND Journal of Formal Logic*, 58(3), 2017. doi:10.1215/00294527-3870348.

[Kle45] Stephen Kleene. On the interpretation of intuitionistic number theory. *Journal of Symbolic Logic*, 10:109-124, 1945. doi:10.2307/2269016.

[Kol32] Andrey Kolmogorov. Zur Deutung der intuitionistischen Logik. *Mathematische Zeitschrift*, 35(1):58-65, 1932. doi:10.1007/BF01186549.

[Kre51] Georg Kreisel. On the interpretation of non-finitist proofs, I. *J. Symb. Log.*, 16:241-267, 1951. doi:10.2307/2267908.

[Kri01] Jean-Louis Krivine. Typed lambda-calculus in classical Zermelo-Fraenkel set theory. *Arch. Math. Log.*, 40(3):189-205, 2001. doi:10.1007/s001530000057.

[Kri09] Jean-Louis Krivine. Realizability in classical logic. In Interactive models of computation and program behaviour. *Panoramas et synthèses*, 27, 2009.

[Kri11] Jean-Louis Krivine. Realizability algebras: a program to well order $\mathbb{R}$. *Logical Methods in Computer Science*, 7(3), 2011. doi:10.2168/LMCS-7(3:2)2011.

[Kri16] Jean-Louis Krivine. Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis. In Jean-Marc Talbot and Laurent Regnier, editors, *25th EACSL Annual Conference on Computer Science Logic (CSL 2016)*, volume 62 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 25:1-25:11, Dagstuhl, Germany, 2016. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. doi:10.4230/LIPICs.CSL.2016.25.

[KS13] Mikhail Katz and David Sherry. Leibniz's infinitesimals: their fictionality, their modern implementations, and their foes from Berkeley to Russell and beyond. *Erkenntnis*, 78(3):571-625, 2013. doi:10.1007/s10670-012-9370-y.

[LR75] Albert Lightstone and Abraham Robinson. *Nonarchimedean Fields and Asymptotic Expansions*. North-Holland mathematical library. North-Holland, 1975. doi:10.1016/0001-8708(76)90162-6.

[Lut87] Robert Lutz. Rêveries infinitésimales. *Gazette des mathématiciens*, 34:79-87, 1987.

[MH18] Étienne Miquey and Hugo Herbelin. Realizability interpretation and normalization of typed call-by-need $\lambda$-calculus with control. In *Foundations of software science and computation structures*, volume 10803 of *Lecture Notes in Comput. Sci.*, pages 276-292. Springer, Cham, 2018. doi:10.1007/978-3-319-89366-2_1.

[Miq11a] Alexandre Miquel. Existential witness extraction in classical realizability and via a negative translation. *Logical Methods in Computer Science*, 7(2):188-202, 2011. doi:10.2168/LMCS-7(2:2)2011.

[Miq11b] Alexandre Miquel. Forcing as a program transformation. In *Proceedings of the 2011 IEEE 26th Annual Symposium on Logic in Computer Science*, LICS '11, page 197-206, USA, 2011. IEEE Computer Society. doi:10.1109/LICS.2011.47.

[Miq20] Alexandre Miquel. Implicative algebras: a new foundation for realizability and forcing. *Mathematical Structures in Computer Science*, 30(5):458-510, 2020. doi:10.1017/S0960129520000079.

[Moe95] Ieke Moerdijk. A model for intuitionistic non-standard arithmetic. *Ann. Pure Appl. Logic*, 73(1):37-51, 1995. A tribute to Dirk van Dalen. doi:10.1016/0168-0072(93)E0071-U.

[MP97] Ieke Moerdijk and Erik Palmgren. Minimal models of Heyting arithmetic. *J. Symbolic Logic*, 62(4):1448-1460, 1997. doi:10.2307/2275651.

[Nel77] Edward Nelson. Internal set theory: A new approach to nonstandard analysis. *Bull. Amer. Math. Soc*, 1977. doi:10.2307/2273684.

[Nel87] Edward Nelson. *Radically Elementary Probability Theory*. Annals of Mathematical Studies, vol. 117. Princeton University Press, Princeton, N. J., 1987.

[Pow18] Thomas Powell. A functional interpretation with state. In *Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science*, LICS '18, page 839-848, New York, NY, USA, 2018. Association for Computing Machinery. doi:10.1145/3209108.3209134.

[Pra65] Dag Prawitz. *Natural deduction. A proof-theoretical study*. Acta Universitatis Stockholmiensis. Stockholm Studies in Philosophy, No. 3. Almqvist & Wiksell, Stockholm, 1965. doi:10.2307/2271676.

[Rob61] Abraham Robinson. Non-standard analysis. *Indagationes Mathematicae (Proceedings)*, 64:432-440, 1961. doi:10.1016/S1385-7258(61)50044-3.
[Rob66] Abraham Robinson. *Non-standard analysis*. North-Holland Publishing Co., Amsterdam, 1966.

[Tar30] Alfred Tarski. Une contribution à la théorie de la mesure. *Fundamenta Mathematicae*, 15(1):42-50, 1930. URL: http://eudml.org/doc/212372.

[vO08] Jaap van Oosten. *Realizability: an introduction to its categorical side*, volume 152 of *Studies in Logic and the Foundations of Mathematics*. Elsevier B. V., Amsterdam, 2008.

[Zei09] Noam Zeilberger. Refinement types and computational duality. In *Proceedings of the 3rd Workshop on Programming Languages Meets Program Verification*, PLPV '09, page 15–26, New York, NY, USA, 2009. Association for Computing Machinery. doi:10.1145/1481848.1481852.

[Lo60] Jerzy Loś. Quelques remarques, théorèmes et problèmes sur les classes définissables d’algèbres. *Journal of Symbolic Logic*, 25(2):168–168, 1960. doi:10.2307/2964232.