# Two-point distortion theorems for harmonic mappings

V. Bravo and R. Hernández and O. Venegas  Facultad de Ingeniería y Ciencias
Universidad Adolfo Ibáñez
Av. Padre Hurtado 750, Viña del Mar, Chile<EMAIL_ADDRESS>Facultad de
Ingeniería y Ciencias
Universidad Adolfo Ibáñez
Av. Padre Hurtado 750, Viña del Mar, Chile<EMAIL_ADDRESS>Departamento de Ciencias Matemáticas y Físicas. Facultad de Ingeniería
Universidad Católica de Temuco, Chile<EMAIL_ADDRESS>
###### Abstract.

We establish two-point distortion theorems for sense-preserving planar
harmonic mappings $f=h+\overline{g}$ which satisfies the univalence criteria
in the unit disc such that, Becker’s and Nehari‘s harmonic version. In
addition, we find the sharp two-point distortion theorem when $h$ is a convex
function, and normalized mappings such that $h({\mathbb{D}})$ is a
$c$-linearly connected domain. To do this, we use the order of this family.

The authors were partially supported by Fondecyt Grants # 1190756. Key words:
Two-point distortion, harmonic mappings, univalence criterion. 2020 AMS
Subject Classification. Primary: 30C45, 30C99; Secondary: 31C05.

##  1\. Introduction

To a large extent, the two-point distortion theorems provide us quantitative
information on “how injective” a conformal function is, in the sense of
estimating the distance between the images of any two points, respect to the
distance (Euclidean or Hyperbolic) of these two points. That is, we seek lower
and upper bounds for the distance between $f(a)$ and $f(b)$ for all $a$ and
$b$ in the unit disc ${\mathbb{D}}$ and that involves in some sense
$\rho(a,b)=\mid(a-b)/(1-\overline{a}b)\mid$ and the derivative of the function
$f$. The first two-point distortion theorem was introduced by C. Blatter in
[2] and proved that if $f$ is a conformal mapping, then

$\mid
f(a)-f(b)\mid^{2}\geq\frac{\sinh^{2}(2d(a,b))}{8(\cosh(4d(a,b)))}\left(R(a)^{2}+R(b)^{2}\right).$

Here $d(a,b)=\tanh^{-1}(\rho(a,b))$, and $R(z)=(1-|z|^{2})|f^{\prime}(z)|$.
Moreover, for different subclasses of univalent functions, such as convex,
starlike, etc., there are two-point distortion theorems in which the bounds
are more accurate. In particular, if $f$ conformally maps the disk onto a
convex domain, Kim and Minda in [12] proved the following result:

Theorem A. Let $f:{\mathbb{D}}\to{\mathbb{C}}$ be a conformal convex mapping,
then for all $p>1$ and all $a$, $b$ in ${\mathbb{D}}$ we have that

(1)
$|f(a)-f(b)|\geq\frac{\sinh(d(a,b))}{2(\cosh(pd(a,b)))^{1/p}}\left(R(a)^{p}+R(b)^{p}\right)^{1/p}.$

On the other hand, univalence criteria involving both the pre-Schwarzian and
Schwarzian derivatives of locally univalent functions defined in
${\mathbb{D}}$ are well known, which also provide their own two-point
distortion theorems. Let $f$ be a locally univalent mapping, its Schwarzian
derivative is defined by:

(2)
$Sf=\left(\frac{f^{\prime\prime}}{f^{\prime}}\right)^{\prime}-\frac{1}{2}\left(\frac{f^{\prime\prime}}{f^{\prime}}\right)^{2}=Pf^{\prime}-\frac{1}{2}Pf^{2},$

here $Pf=f^{\prime\prime}/f^{\prime}$ is named Pre-Schwarzian derivative of
$f$. Nehari in [15] showed that
$\|Sf\|=\sup\\{|Sf(z)|(1-|z|^{2})^{2}:z\in{\mathbb{D}}\\}\leq 2$ implies that
$f$ is univalent in ${\mathbb{D}}$. To see more univalence criteria that
involves the Schwarzian derivative, we can see the $p$-criterion due by Nehari
in [16]. In this context, Chuaqui and Pommerenke [4] gave a quantitative
version of Nehari’s theorem by showing that the condition $\|Sf\|\leq 2$
implies that $f$ has the two-point distortion property

(3) $|f(a)-f(b)|\geq d(a,b)\sqrt{R(a)R(b)}.$

This result was extended to the $p$-criterion by Ma, Mejía and Minda in [14].

This paper aims to obtain two-point distortion theorems associated with
different univalence criteria for complex harmonic functions defined in
${\mathbb{D}}$. These injectivity criteria are associated with both the Pre-
Schwarzian and Schwarzian derivatives, but also to harmonic functions whose
analytic part is convex, see [3]. The manuscript is organized as follows: In
Section 2 deals with the preliminaries on complex harmonic mappings and
includes the above univalence criteria, called Theorem B, Theorem C, and
Theorem D. Subsections 3.1 and 3.2 are devoted to the two-point distortion
theorems associated with the Becker and Nehari criteria respectively, but in
their complex harmonic versions. Special attention will be paid in subsection
3.3 since we not only deal with the case when the analytic part is convex but
also when it conformally maps the disk into a linearly connected domain which
means geometrically that it has no inward cusps. Indeed, we prove that these
functions form a linearly invariant family which follows the two-point
distortion theorem found in this manuscript.

##  2\. Preliminaries

A complex-valued harmonic function $f$ in a simply connected domain $\Omega$
are those who satisfies that $\Delta f=\partial^{2}f/\partial
z\partial\overline{z}=0$, which is equivalent to $f=u+iv$ where $u$ and $v$
are real harmonic mappings defined in $\Omega$. A straightforward calculation
give that this functions has a canonical representation $f=h+\overline{g}$,
where $h$ and $g$ are analytic functions in $\Omega$, that is unique up to an
additive constant. When $\Omega={\mathbb{D}}$ it is convenient to choose the
additive constant so that $g(0)=0$. The representation $f=h+\overline{g}$ is
then unique and is called the canonical representation of $f$. A result of
Lewy [13] states that $f$ is locally univalent if and only if its Jacobian
$J_{f}=|h^{\prime}|^{2}-|g^{\prime}|^{2}$ does not vanish in $\Omega$. Thus,
harmonic mappings are either sense-preserving or sense-reversing depending on
the conditions $J_{f}>0$ or $J_{f}<0$ throughout the domain $\Omega$ where $f$
is locally univalent, respectively. Since $J_{f}>0$ if and only if
$J_{\overline{f}}<0,$ throughout this work we will consider sense-preserving
mappings in ${\mathbb{D}}.$ In this case the analytic part $h$ is locally
univalent in ${\mathbb{D}}$ since $h^{\prime}\neq 0$, and the second complex
dilatation of $f$, $\omega=g^{\prime}/h^{\prime}$, is an analytic function in
${\mathbb{D}}$ with $|\omega|<1$. The reader can be found in [5] a elegant
reference for this topic.

Duren, Hamada & Kohr in [7] showed, among other results, that
$f=h+\overline{g}$ univalent harmonic mapping and normalized to $h(0)=g(0)=0$,
and $h^{\prime}(0)=1$, and let $\alpha$ the order of this family, which is the
supremum of the absolute value of the second Taylor coefficient of $h$, then

$|f(a)-f(b)|\geq\frac{1}{2\alpha}(1-\exp(-2\alpha
d(a,b)))\max\\{R(a),R(b)\\},$

where $R(z)=(1-|z|^{2})(|h^{\prime}(z)|-|g^{\prime}(z)|).$ Moreover, they also
proved that

$|f(a)-f(b)|\leq\frac{1}{2\alpha}(\exp(2\alpha d(a,b)-1))\min\\{Q(a),Q(b)\\},$

where $Q(z)=(1-|z|^{2})(|h^{\prime}(z)|+|g^{\prime}(z)|)$. Which represent the
harmonic version of Blatter’s Theorem. Note that in the analytic case,
$\alpha=2$, however, in the harmonic case, the size of $\alpha$ is unknown.

Hernández and Martín [8], defined the harmonic pre-Schwarzian and Schwarzian
derivatives for sense-preserving harmonic mappings $f=h+\overline{g}$. Using
those definitions, they generalized different results regarding analytic
functions to the harmonic case [8, 9, 10, 11]. The pre-Schwarzian and
Schwarzian derivatives of a sense-preserving harmonic function $f$ are
corresponding defined by

$P_{f}=\frac{h^{\prime\prime}}{h^{\prime}}-\frac{\bar{\omega}\omega^{\prime}}{1-|\omega|^{2}}=Ph-\frac{\bar{\omega}\omega^{\prime}}{1-|\omega|^{2}}=\frac{\partial}{\partial
z}\log(J_{f}),$

$S_{f}=\frac{\partial}{\partial
z}P_{f}-\frac{1}{2}(P_{f})^{2}=Sh+\frac{\overline{\omega}}{1-|\omega|^{2}}\left(\omega^{\prime}\frac{h^{\prime\prime}}{h^{\prime}}-\omega^{\prime\prime}\right)-\frac{3}{2}\left(\frac{\omega^{\prime}\overline{\omega}}{1-|\omega|^{2}}\right)^{2},$

where $Ph$ and $Sh$ are the standard Pre-Schwarzian and Schwarzian derivative
respectively, which is given by equation (2). It is easy to see that if $f$ is
analytic ($f=h$ and $\omega=0$) then $P_{f}=h^{\prime\prime}/h^{\prime}$ and
$S_{f}=Sh$, recovering the classical definition of this operators. In [8] the
authors proved that $S_{f}=0$ if and only if $f$ is a Möbius harmonic
transformation, which is given by $f=h+\alpha\overline{h}$ with
$\alpha\in{\mathbb{D}}$ and $h$ is a Möbius analytic function. To motivate the
two-point distortion theorems associated to univalence criteria, those
harmonic Möbius mappings satisfies that

$|f(a)-f(b)|=\sqrt{|h^{\prime}(a)||h^{\prime}(b)|}|a-b||1+\lambda\alpha|,\quad\lambda=\frac{\overline{h(a)-h(b)}}{h(a)-h(b)}\,,\quad
a\neq b.$

Thus, we can re-write this equation to get

$|f(a)-f(b)|=\sqrt{R_{h}(a)R_{h}(b)}\sinh(d(a,b))|1+\lambda\alpha|,\quad
R_{h}(z)=|h^{\prime}(z)|(1-|z|^{2}).$

In addition, for any $a\in{\mathbb{D}}$, the authors also proved that
$P_{f+\overline{af}}=P_{f}$ which is the key to prove the extension of
Becker’s criterion of univalence for harmonic mappings. This is contained in
the following theorem:

Theorem B. Let $f=h+\overline{g}$ be a sense-preserving harmonic function in
the unit disc ${\mathbb{D}}$ with dilatation $\omega$. If for all
$z\in{\mathbb{D}}$

$(1-|z|^{2})|zP_{f}(z)|+\frac{|z\omega^{\prime}(z)|(1-|z|^{2})}{1-|\omega(z)|^{2}}\leq
1,$

then $f$ is univalent. The constant 1 is sharp.

The classical Becker’s criterion can be found in [1] and the extension to
harmonic mapping appear in [8].

Observe that using the Schwarz-Pick lemma,
$\omega:{\mathbb{D}}\to{\mathbb{D}}$ satisfies that

(4)
$\|\omega^{*}\|=\sup_{z\in{\mathbb{D}}}\dfrac{|\omega^{\prime}(z)|(1-|z|^{2})}{1-|\omega(z)|^{2}}\leq
1.$

In addition, we consider
$\|\omega\|=\sup\\{|\omega(z)|:\,z\in{\mathbb{D}}\\}=\|\omega\|_{\infty}$. In
[11] the authors proved, using that for all $a\in{\mathbb{D}}$,
$S_{f+\overline{af}}=S_{f}$, the following generalization of Nehari’s
classical univalence criterion:

Theorem C. Let $f=h+\overline{g}$ be a sense-preserving harmonic function in
the unit disc ${\mathbb{D}}$ with dilatation $\omega$. Then, there exists
$\varepsilon>0$ such that

$(1-|z|^{2})^{2}|S_{f}(z)|\leq\varepsilon$

implies that $f$ is univalent.

Obviously, the classical result is obtained taking $\omega=0$, but in this
case, $\varepsilon=2$. Unfortunately, the value of $\varepsilon$ is still
unknown for the planar harmonic mappings setting. From the proof of this
theorem, we can see that this value $\varepsilon$ is small enough to
$\|Sh\|\leq 2$, i.e. $h$ satisfies the Nehari’s classical univalence
criterion. Moreover, since $S_{f}$ is invariant under pre-composition of
affine mapping, we have that $h+ag$ satisfies the Nehari’s criterion for all
$a\in\overline{{\mathbb{D}}}$.

The last criterion that we will consider in this manuscript appears in [3] and
says the following:

Theorem D. Let $f=h+\overline{g}$ be a sense-preserving harmonic function in
the unit disc ${\mathbb{D}}$ with dilatation $\omega$. If $h$ is a convex
mapping, then $f$ is univalent. In fact, when $h({\mathbb{D}})$ is
$c-$linearly connected domain, if $\|\omega\|_{\infty}<1/c$, then $f$ is also
univalent in the unit disc.

Thus, the principal goal of this notes is give to measure of the univalence of
functions that satisfies this inyectivity criteria of the form of two-point
distortion theorems. Generalizing the classical results for holomorphic
mappings.

##  3\. Results

Troughs the section, we set $\varphi$ as a locally univalent analytic, and
$f=h+\overline{g}$ be a sense-preserving harmonic mapping with dilatation
$\omega$ defined in the unit disc. Recall that the fact that $f$ is sense-
preserving, implies that $h^{\prime}\neq 0$ and
$\omega({\mathbb{D}})\subset{\mathbb{D}}$. Additionally, we call
$R_{\varphi}(z)=(1-|z^{2}|)|\varphi^{\prime}(z)|$ and
$R(z)=(1-|z|^{2})(|h^{\prime}(z)|-|g^{\prime}(z)|)$, and
$Q(z)=(1-|z|^{2})(|h^{\prime}(z)|+|g^{\prime}(z)|)$ its harmonic version of
this quantity.

###  3.1. The Becker’s criterion case

Let $\varphi$ be a normalized locally univalent analytic function defined in
${\mathbb{D}}$. Its order is given by

$\mbox{ord}\langle\varphi\rangle=\sup_{z\in{\mathbb{D}}}\left|\frac{1}{2}\frac{\varphi^{\prime\prime}}{\varphi^{\prime}}(z)(1-|z|^{2})-\overline{z}\right|=\sup_{a\in{\mathbb{D}}}\left\\{\frac{1}{2}|\varphi_{a}^{\prime\prime}(0)|:\varphi_{a}(z)=\dfrac{\varphi\left(\dfrac{z+a}{1-\overline{a}z}\right)-\varphi(a)}{(1-|a|^{2})\varphi^{\prime}(a)}\right\\},$

which is basically the supremum of second Taylor coefficient of $\varphi_{a}$,
for all $a\in{\mathbb{D}}$. A well-known result (see [17]) asserts that if
$\varphi$ is univalent mapping defined in the unit disk, normalized to
$\varphi(0)=0$ and $\varphi^{\prime}(0)=1$, and its order is $\alpha,$ then

(5)
$\frac{1}{2\alpha}\left(\left(\frac{1+|z|}{1-|z|}\right)^{\alpha}-1\right)\geq|\varphi(z)|\geq\frac{1}{2\alpha}\left(1-\left(\frac{1-|z|}{1+|z|}\right)^{\alpha}\right),\quad\quad
z\in{\mathbb{D}}.$

Thus, the following Theorem is an application of this when $\varphi$ satisfies
the classical univalence criterion due by Becker in [2]. Actually, we haven’t
been able to find any reference on this, so we include a proof.

######  Theorem 1.

Let $\varphi:{\mathbb{D}}\to{\mathbb{C}}$ be a locally univalent normalized as
before such that $|P\varphi(z)|(1-|z|^{2})\leq 1$. Then for all
$a,b\in{\mathbb{D}}$ we have that

(6)
$\frac{\exp(3d(a,b))-1}{3}\sqrt{R_{\varphi}(a)R_{\varphi}(b)}\geq|\varphi(a)-\varphi(b)|\geq\dfrac{1-\exp(-3d(a,b))}{3}\sqrt{R_{\varphi}(a)R_{\varphi}(b)}.$

###### Proof.

We note that

$\alpha=\mbox{ord}\langle\varphi\rangle=\sup_{z\in{\mathbb{D}}}\left|\dfrac{1}{2}(1-|z|^{2})\dfrac{\varphi^{\prime\prime}}{\varphi^{\prime}}(z)-\overline{z}\right|\leq\dfrac{1}{2}+|z|\leq\dfrac{3}{2},$

then $\varphi_{a}$ satisfies inequality (5). Taking
$b=\dfrac{z+a}{1-\overline{a}z}$ which is equivalent to
$z=\dfrac{b-a}{1-\overline{a}b}$ we obtain

$\left|\dfrac{\varphi(b)-\varphi(a)}{(1-|a|^{2})|\varphi^{\prime}(a)|}\right|\geq\dfrac{1}{2\alpha}\left[1-\left(\dfrac{1-\left|\dfrac{b-a}{1-\overline{a}b}\right|}{1+\left|\dfrac{b-a}{1-\overline{a}b}\right|}\right)^{\alpha}\right]\geq\dfrac{1}{3}\left[1-\left(\dfrac{1-\left|\dfrac{b-a}{1-\overline{a}b}\right|}{1+\left|\dfrac{b-a}{1-\overline{a}b}\right|}\right)^{3/2}\right].$

Since $\rho(a,b)=\left|\dfrac{b-a}{1-\overline{a}b}\right|$ from the last
inequality we obtain

$|\varphi(a)-\varphi(b)|^{2}\geq\dfrac{(1-|a|^{2})(1-|b|^{2})|\varphi^{\prime}(a)||\varphi^{\prime}(b)|}{9}\left[1-\left(\dfrac{1-\rho(a,b)}{1+\rho(a,b)}\right)^{3/2}\right]^{2}.$

But,

$d(a,b)=\frac{1}{2}\log\left(\dfrac{1+\rho(a,b)}{1-\rho(a,b)}\right),$

therefore taking square root we obtain the lower bound.

Since the real function $(\xi^{\alpha}-1)/\alpha$ is growing in $\alpha$ for
any $\xi>1$, using $\alpha\leq 3/2$ and [17, Staz 1.1] again, we have that

$|\varphi(a)-\varphi(b)|\leq\frac{\sqrt{(1-|a|^{2})(1-|b|^{2})|\varphi^{\prime}(a)||\varphi^{\prime}(b)|}}{3}\left[\left(\dfrac{1+\rho(a,b)}{1-\rho(a,b)}\right)^{3/2}-1\right],$

which ends the proof. ∎

Note that, under the hypothesis of Theorem B, the analytic part of
$f=h+\overline{g}$ satisfies that $|Ph(z)|(1-|z|^{2})\leq 1$ then satisfies
the Becker’s univalence criterion for analytic mappings in ${\mathbb{D}}$.
Since $P_{f+\lambda\overline{f}}=P_{f}$ then $\varphi_{\lambda}=h+\lambda g$
satisfies the Becker’s univalence criterion for all $\lambda\in{\mathbb{D}}$,
moreover, taking limits when $|\lambda|\to 1$, we can asserts that Becker’s
criterion holds for $|\lambda|\leq 1$, which is the key for the following
theorem:

######  Theorem 2.

Let $f=h+\overline{g}$ be a sense-preserving harmonic mapping defined in
${\mathbb{D}}$, such that satisfies the hypothesis of Theorem B, then

$\frac{1}{3}(\exp(3d(a,b))-1)\sqrt{Q(a)Q(b)}\geq|f(a)-f(b)|\geq\frac{1}{3}(1-\exp(-3d(a,b)))\sqrt{R(a)R(b)}.$

###### Proof.

For $a$ and $b$ in ${\mathbb{D}}$, it follows that
$f(a)-f(b)=h(a)-h(b)+\overline{(g(a)-g(b))}$, thus, if $g(a)\neq g(b)$ there
exists an unimodular constant $\lambda$ such that
$f(a)-f(b)=\varphi_{\lambda}(a)-\varphi_{\lambda}(b)$. In the case when
$g(a)=g(b)$ we can consider $\lambda=0$. In any case, $\varphi_{\lambda}$
satisfies the Becker’s criterion, thus we can apply inequality (6) and the
fact that
$|h^{\prime}|+|g^{\prime}|\geq|\varphi^{\prime}_{\lambda}|\geq|h^{\prime}|-|g^{\prime}|$
to obtain that

$|f(a)-f(b)|^{2}\leq\frac{1}{3}\left[\left(\frac{1+\rho(a,b)}{1-\rho(a,b)}\right)^{3/2}-1\right]Q(a)Q(b),$

and

$|f(a)-f(b)|^{2}\geq\frac{1}{3}\left[1-\left(\frac{1-\rho(a,b)}{1+\rho(a,b)}\right)^{3/2}\right]R(a)R(b).$

∎

###  3.2. The Nehari’s criterion case

Let $f=h+\overline{g}$ be a sense-preserving harmonic mapping. In [8] the
authors shows that there exists $\varepsilon>0$ such that if
$\|S_{f}\|=\sup\\{(1-|z|^{2})^{2}|S_{f}(z)|:z\in{\mathbb{D}}\\}\leq\varepsilon$,
then $f$ is univalent in ${\mathbb{D}}$. Moreover, is deduce that there exists
a constant $k>0$ such that

$\|Sh\|\leq\varepsilon+kW_{\varepsilon}+\frac{3}{2}W_{\varepsilon}^{2},$

where $W_{\varepsilon}=\sup\\{\|\omega^{\ast}\|:\omega\in A_{\varepsilon}\\}$.
We say that an analytic mapping $\omega$ belongs to $A_{\varepsilon}$ if and
only there exist $f=h+\overline{g}$ with dilatation $\omega$ and
$\|S_{f}\|\leq\varepsilon$. In the same paper, has been proved that
$W_{\varepsilon}\to 0$ when $\varepsilon\to 0$. We can assume that
$\varepsilon$ is given by

$\varepsilon=\sup\\{\delta:\delta+kW_{\delta}+\frac{3}{2}W_{\delta}^{2}\leq
2\\},$

thus the Theorem C asserts that $\|S_{f}\|\leq\varepsilon$ is a univalence
criterion for sense-preserving harmonic mappings. From the proof of Theorem C
it follows that for $\lambda\in{\mathbb{D}}$, the locally univalent analytic
mapping $\varphi_{\lambda}=h+\lambda g$, satisfies that
$\|S\varphi_{\lambda}\|\leq\varepsilon$ since
$f_{\lambda}=f+\lambda\overline{f}$ has the same Schwarzian derivative. Thus
we can asserts the following lemma:

######  Lemma 3.

Let $f=h+\overline{g}$ be a sense-preserving harmonic mapping defined in
${\mathbb{D}}$ such that $\|S_{f}\|\leq\varepsilon$, then for any
$\lambda\in{\mathbb{D}}$, the corresponding mapping $\varphi_{\lambda}$
satisfies that $\|S\varphi_{\lambda}\|\leq 2$.

In [14, Thm. 1.1 part a)] the authors proved that if $\|S\varphi\|\leq 2t$
with $t\in[0,1]$ then

(7)
$|\varphi(a)-\varphi(b)|\leq\sqrt{\dfrac{R_{\varphi}(a)R_{\varphi}(b)}{1+t}}\sinh\left({\sqrt{1+t}\,d(a,b)}\right),$

which is, together [4, Thm. 2] the key inequalities for the following theorem.

######  Theorem 4.

Let $f=h+\overline{g}$ be a sense-preserving harmonic mapping defined in
${\mathbb{D}}$. If $\|S_{f}\|\leq\varepsilon$ where $\varepsilon$ as in
Theorem B, then

$\sqrt{\frac{Q(a)Q(b)}{2}}\sinh\left(\sqrt{2}\,d(a,b)\right)\geq|f(a)-f(b)|\geq
d(a,b)\sqrt{R(a)R(b)}.$

###### Proof.

For any $a$ and $b$ in the unit disk, it follows that
$f(a)-f(b)=h(a)-h(b)+\overline{(g(a)-g(b))}$, thus, if $g(a)\neq g(b)$ there
exists an unimodular constant $\lambda$ such that
$f(a)-f(b)=\varphi_{\lambda}(a)-\varphi_{\lambda}(b)$. In the case when
$g(a)=g(b)$ we can consider $\lambda=0$. But, using Theorem 2 in [4] (equation
3) and inequality (7) we have that

$\frac{R_{\varphi_{\lambda}}(a)R_{\varphi_{\lambda}}(b)}{2}\sinh^{2}\left(\sqrt{2}\,d(a,b)\right)\geq|\varphi_{\lambda}(a)-\varphi_{\lambda}(b)|^{2}\geq
d(a,b)^{2}R_{\varphi_{\lambda}}(a)R_{\varphi_{\lambda}}(b),$

but
$|h^{\prime}|+|g^{\prime}|\geq|\varphi_{\lambda}^{\prime}|\geq|h^{\prime}|-|g^{\prime}|$
which completes the proof. ∎

Note that if $f$ is analytic, which is the case when $\omega=0$, then
$W_{\varepsilon}=0$ and $\varepsilon=2$, thus, the last theorem is a
generalization of [4, Thm. 2].

###  3.3. When the analytic part is a convex function

We known that $f=h+\overline{g}$ is univalent in the unit disk when $h$ is a
convex mapping (by [3, Thm. 1]). Moreover, the result can be extended to the
case when $h$ maps conformally ${\mathbb{D}}$ onto a linearly connected
domain, which is the matter in sub-section 3.1.1.

######  Theorem 5.

Let $f=h+\overline{g}$ be a sense-preserving harmonic mapping defined in
${\mathbb{D}}$ such that $h$ is a convex function. Then for all
$a,b\in{\mathbb{D}}$

$|f(a)-f(b)|\leq(1+\|\omega\|_{\infty})\left|\dfrac{a-b}{1-\overline{a}b}\right|\left(\dfrac{R_{h}(a)+R_{h}(b)}{2}\right),$

and

$|f(a)-f(b)|\geq(1-\|\omega\|_{\infty})\left|\dfrac{a-b}{1-\overline{a}b}\right|\left(\dfrac{R_{h}(a)+R_{h}(b)}{2}\right).$

###### Proof.

We note that

(8)
$\displaystyle|h(a)-h(b)|+|g(a)-g(b)|\geq|f(a)-f(b)|\geq|h(a)-h(b)|-|g(a)-g(b)|.$

Considering the curve $\gamma=h^{-1}(R),$ where $R$ is the segment joining
$h(a)$ and $h(b)$, then for $\zeta=h^{-1}(w)$ we have that
$d\zeta=\dfrac{1}{h^{\prime}(h^{-1}(w))}dw$ and

$|g(a)-g(b)|=\left|\int_{\gamma}g^{\prime}(\zeta)\,d\zeta\right|=\left|\int_{R}\dfrac{g^{\prime}(\zeta)}{h^{\prime}(\zeta)}dw\right|\leq\|\omega\|_{\infty}\int_{R}|dw|=\|\omega\|_{\infty}|h(a)-h(b)|.$

Hence, substituting this last inequality in (8) we obtain

$(1+\|\omega\|_{\infty})|h(a)-h(b)|\geq|f(a)-f(b)|\geq(1-\|\omega\|_{\infty})|h(a)-h(b)|.$

Therefore, using Theorem A follows the result. ∎

####  3.3.1. When the analytic part $h$ is $c$-linearly connected

We will pay special attention to the case where $h({\mathbb{D}})$ is a
linearly connected domain, which means that for any $a$ and $b$ in
${\mathbb{D}}$ there exists a curve $\gamma$ that joined $h(a)$ with $h(b)$,
such that its length satisfies that

(9) $\ell_{\gamma}\leq c|h(a)-h(b)|.$

In this case, we say that $f$ is a $c$-linearly connected. Observed that
$c\geq 1$ and $c=1$ if and only if $h({\mathbb{D}})$ is a convex domain. Was
proved in [3] that if $h({\mathbb{D}})$ is a linearly connected domain with
constant $c$ and $|\omega|<1/c$ then $f$ is univalent in the unit disc.

######  Theorem 6.

Let $\varphi:{\mathbb{D}}\to{\mathbb{C}}$ be a conformal and $c$-linearly
connected mapping defined in ${\mathbb{D}}$, then

$\varphi_{a}(z)=\dfrac{\varphi\left(\dfrac{z+a}{1+\overline{a}z}\right)-\varphi(a)}{(1-|a|^{2})\varphi^{\prime}(a)}$

is a $c$-linearly connected mapping.

Moreover, it is known that the set $\mathcal{F}$, of normalized functions by
$\varphi(0)=0$ and $\varphi^{\prime}(0)=1$ such that for any
$a\in{\mathbb{D}}$, $\varphi_{a}$ belongs to $\mathcal{F}$ is called linearly
invariant family, and has been largely studied by Ch. Pommerenke, for instance
[17]. One of the most famous families is the conformal, called $S$. It is
well-known that the order of $S$ is less or equal than 2. By the last Theorem,
given $c\geq 1$ the set $K_{c}=\\{\varphi\in S:\varphi({\mathbb{D}})\,\mbox{is
$c$-linearly connected}\\}$ is a linearly invariant family. Recall that
$K_{1}$ is the classical family of convex mappings $K$ (see [6]). Let $\beta$
the order of $K_{c}$, which depends of $c$ and tends to 2 when $c$ goes to
$\infty$ and since $K_{c}\subset S$, then $\beta<2$.

######  Theorem 7.

Let $f=h+\overline{g}$ be a sense-preserving harmonic mapping defined in
${\mathbb{D}}$ such that $h$ is a $c$-linearly connected mapping and its
dilatation satisfies that $\|\omega\|_{\infty}<1/c$, then for any $a$ and $b$
in ${\mathbb{D}}$

$|f(a)-f(b)|\geq(1-c\|\omega\|_{\infty})\frac{1}{2\beta}(1-\exp(-2\beta
d(a,b))\sqrt{R_{h}(a)R_{h}(b)},$

and

$|f(a)-f(b)|\leq(1+c\|\omega\|_{\infty})\frac{1}{2\beta}(\exp(2\beta
d(a,b)-1)\sqrt{R_{h}(a)R_{h}(b)},$

where $\beta$ is the order of $h$.

###### Proof.

For any $a$ and $b$ in ${\mathbb{D}}$ exists a curve $\gamma\subset
h({\mathbb{D}})$ such that its large $\ell_{\gamma}$, satisfies (9). Let
$\Gamma=h^{-1}(\gamma)\subset{\mathbb{D}}$, thus, considering
$z=h^{-1}(\zeta)$ with $\zeta\in\gamma$, we have that

$|g(a)-g(b)|=\left|\int_{\Gamma}g^{\prime}(z)dz\right|\leq\int_{\gamma}\frac{|g^{\prime}(z)|}{|h^{\prime}(z)|}|d\zeta|\leq\|\omega\|_{\infty}\ell_{\gamma}\leq
c\|\omega\|_{\infty}|h(a)-h(b)|.$

Let $\beta$ the order of $h$, which is less than 2. Since
$|f(a)-f(b)|=|h(a)-h(b)+\overline{(g(a)-g(b))}|$, [17, Staz 1.1], and triangle
inequality, the proof is complete.

∎

Moreover, for any $\lambda$ with modulus 1, the corresponding analytic
function $\varphi_{\lambda}$ is also a linearly connected mapping with
constant $1-c\|\omega\|_{\infty}$. Since

$\frac{\varphi_{\lambda}^{\prime\prime}}{\varphi_{\lambda}^{\prime}}=\frac{h^{\prime\prime}}{h^{\prime}}+\frac{\lambda\omega^{\prime}}{1+\lambda\omega},$

the order of $\varphi_{\lambda}$ named $\beta_{\lambda}$ satisfies that
$\beta_{\lambda}=\min\\{2,\beta+\|\omega^{\ast}\|\\},$ where
$\|\omega^{\ast}\|$ given by equation (4). Thus, we can assert the following
corollary.

######  Corollary 1.

Let $f$ as previous theorem. Then, for any $a$ and $b$ in ${\mathbb{D}}$

$\frac{1}{2\beta_{\lambda}}(\exp(2\beta_{\lambda}d(a,b))-1)\sqrt{R(a)R(b)}\geq|f(a)-f(b)|\geq\frac{1}{2\beta_{\lambda}}(1-\exp(-2\beta_{\lambda}d(a,b)))\sqrt{R(a)R(b)}.$

## References

  * [1] Becker J., Löwnersche Differentialgleichung und quasi-konform forttsetzbare schlichte funktionen, J. Reine. Angew. Math., 225, 23–43 (1972).

  * [2] Blatter C., Ein verzerrungssatz für schlichte funktionen, Comment. Math. Helv. 53, 651–659 (1978).

  * [3] Chuaqui M. and Hernández R., Univalent harmonic mappings and linearly connected domains, JMAA 332, 1189–1194 (2007).

  * [4] Chuaqui M. and Pommerenke Ch., Characteristic properties of Nehari functions, Pacific J. Math. 188(1), 83–94 (1999).

  * [5] Duren P. L., Harmonic mappings in the plane, Cambridge University Press, (2004).

  * [6] Duren P. L., Univalent functions, Springer-Verlag, New York, (1983).

  * [7] Duren P., Hamada H. and Kohr G., Two-point distortion theorems for harmonic and pluriharmonic mappings, Trans. Amer. Math. Soc. 363 (12), 6197–6218 (2011).

  * [8] Hernández R. and Martín M. J., Pre-Schwarzian and Schwarzian derivatives of Harmonic Mappings, J. Geom. Anal., 25(1), 64–91 (2015).

  * [9] Hernández R. and Martín M. J., Stable geometric properties of analytic and harmonic functions, Math. Proc. Cambridge Philos. Soc., 155(2), 343–359 (2013).

  * [10] Hernández R. and Martín M. J., Quasi-conformal extensions of harmonic mappings in the plane, Ann. Acad. Sci. Fenn. Ser. A. I Math, 38, 617–630 (2013).

  * [11] Hernández R., and Martín M. J., Criteria for univalence and quasiconformal extension of harmonic mappings in terms of the Schwarzian derivative, Arch. Math. 104(1), 53–59 (2015).

  * [12] Kim, S. and Minda, D., Two-point distortion theorems for univalent functions, Pac. J. Math. 163(1), 137-157 (1994).

  * [13] Lewy H., On the non-vanishing of the Jacobian in certain one-to-one mappings, Bull. Amer. Math. Soc. 42, 689–692 (1936).

  * [14] Ma W., Mejía D. and Minda D., Two-point distortion for Nehari functions, Complex Anal. Oper. Theory. 8, 213–225 (2014).

  * [15] Nehari, Z., The Schwarzian derivative and schlicht functions. Bull. Am. Math. Soc. 55, 545–551 (1949).

  * [16] Nehari Z., Some criteria of univalence, Proc. Amer. Math. Soc. 5, 700–704 (1954).

  * [17] Pommerenke Ch., Linear-invariante familien analytischer funktionen I, Math. Ann. 155, 108–154 (1964).


B(y)|^{\mathfrak{S}}_{\rho}$. We have

$t_{0}\,h\,{\dagger}\,\bar{n}~{}\,{}^{{\mathfrak{s}}}\\!\\!\downarrow^{{\mathfrak{s}}}~{}\mathop{\mathsf{case}}\,({h}\,{\dagger}\,\bar{n}\,{\dagger}\,0)\,\\{\iota_{1}(a)\mapsto\iota_{1}(a)|\iota_{2}(b)\mapsto
t_{\leq 0}\,b\\}.$

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

######  Lemma 40.

For any internal formulas $A$ and $B$, we have

$t_{\mathsf{s}}\Vvdash\left(\forall^{\\{\\!\mathrm{st}\\!\\}}{\\!}{x}.\forall^{\\{\\!\mathrm{st}\\!\\}}{\\!}{y}.(A(x)\lor
B(y))\right)\to\forall^{\\{\\!\mathrm{st}\\!\\}}{\\!}{x}.\forall^{\\{\\!\mathrm{st}\\!\\}}{\\!}{y}.(\Phi_{A,B}(x,y)\to\Phi_{A,B}(x,{\mathsf{s}}y)),$

where

$\begin{array}[]{r@{}l}{t_{\mathsf{s}}}\triangleq\lambda{h}wxzyp.\mathop{\mathsf{case}}\,p\,\\{&\iota_{1}(p_{1})\mapsto\iota_{1}(p_{1})\\\
&\iota_{1}(p_{2})\mapsto\mathop{\mathsf{case}}\,({h}\,{\dagger}\,x\,{\dagger}\,({\mathsf{s}}y))\,\\{\iota_{1}(a)\mapsto\iota_{1}(a)|\iota_{2}(b)\mapsto\iota_{2}(t_{\leq{\mathsf{s}}}\,p_{2}\,b)\\}.\end{array}$

######  Proof 6.7.

Recall that $\Phi_{A,B}(x,y)=A(x)\lor B_{\leq 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)|^{\mathfrak{S}}_{\rho}$ and
$(u;{\mathfrak{s}})\in|\Phi_{A,B}(n,m)|^{\mathfrak{S}}_{\rho}=|A(n)\lor
B_{\leq m}|^{\mathfrak{S}}_{\rho}$. By construction, we have

${t_{\mathsf{s}}}\,h\,{\dagger}\,\bar{n}\,{\dagger}\,\bar{m}\,u~{}\,{}^{{\mathfrak{s}}}\\!\\!\downarrow^{{\mathfrak{s}}}~{}\begin{array}[]{r@{}l}\mathop{\mathsf{case}}\,u\,\\{&\iota_{1}(p_{1})\mapsto\iota_{1}(p_{1})\\\
&\iota_{1}(p_{2})\mapsto\mathop{\mathsf{case}}\,({h}\,{\dagger}\,\bar{n}\,{\dagger}\,({\mathsf{s}}\bar{m}))\,\\{\iota_{1}(a)\mapsto\iota_{1}(a)|\iota_{2}(b)\mapsto\iota_{2}(t_{\leq{\mathsf{s}}}\,p_{2}\,b)\\}.\end{array}$

To conclude by anti-reduction, we need to prove that the term on the right-
hand side is in $|A(n)\lor B_{\leq S(m)}|^{\mathfrak{S}}_{\rho}$, using the
assumption on $u$ and the adequacy of the ${\scriptstyle(\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_{\leq
m}|^{\mathfrak{S}}_{\rho}$ and prove that
$\mathop{\mathsf{case}}\,({h}\,{\dagger}\,\bar{n}\,{\dagger}\,({\mathsf{s}}\bar{m}))\,\\{\iota_{1}(a)\mapsto\iota_{1}(a)|\iota_{2}(b)\mapsto\iota_{2}(t_{\leq{\mathsf{s}}}\,u_{2}\,b)\\}\in|\Phi_{A,B}(n,S(m))|^{\mathfrak{S}}_{\rho}$.

Again, we use the assumption on $h$ and the adequacy of the
${\scriptstyle(\lor_{E})}$ rule to conclude. Let us consider a term $b$ such
that $(b;{\mathfrak{s}})\in|B(S(m))|^{\mathfrak{S}}_{\rho}$. It then follows
from the assumption on $u_{2}$ and 37 that
$(t_{\leq{\mathsf{s}}}\,u_{2}\,b;{\mathfrak{s}})\in|B_{\leq
S(m)}|^{\mathfrak{S}}_{\rho}$ and hence
$(\iota_{2}(t_{\leq{\mathsf{s}}}\,u_{2}\,b);{\mathfrak{s}})\in|A(n)\lor
B_{\leq S(m)}|^{\mathfrak{S}}_{\rho}$.

######  Corollary 41.

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

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

where ${t_{\Phi}}\triangleq{\lambda
hwx.\mathop{\mathsf{rec}}\,(t_{0}\,{h}\,w\,x)\,(t_{\mathsf{s}}\,{h}\,w\,x)}$.

######  Proof 6.8.

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

$t_{\Phi}\,h\,{\dagger}\,\bar{n}~{}\,{}^{{\mathfrak{s}}}\\!\\!\downarrow^{{\mathfrak{s}}}~{}\mathop{\mathsf{rec}}\,(t_{0}\,h\,{\dagger}\,\bar{n})\,(t_{\mathsf{s}}\,h\,{\dagger}\,\bar{n}).$

Then, the result follows directly from External Induction (27) and Lemmas 39
and 40.

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

######  Lemma 42.

For any internal formulas $A$ and $B$, we have:

$t_{\Delta}\Vvdash\left(\forall^{\\{\\!\mathrm{st}\\!\\}}{\\!}{x}.\forall^{\\{\\!\mathrm{st}\\!\\}}{\\!}{y}.(A(x)\vee
B(y))\right)\to\forall^{\\{\\!\mathrm{st}\\!\\}}{\\!}{x}.(A_{\leq x}\to
A_{\leq S(x)}\lor B_{\leq S(x)}),$

where
${t_{\Delta}}\triangleq{\lambda{h}wxv.\mathop{\mathsf{case}}\,\left(t_{\Phi}\,{h}\,\,{\dagger}\,({\mathsf{s}}x)\,{\dagger}\,({\mathsf{s}}x)\right)\,\\{\iota_{1}(c_{1})\mapsto\iota_{1}(t_{\leq{\mathsf{s}}}\,v\,c_{1})|\iota_{2}(c_{2})\mapsto\iota_{2}(c_{2})\\}}$.

######  Proof 6.9.

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}}_{\rho}$ and $(a;{\mathfrak{s}})\in|A_{\leq
n}|^{\mathfrak{S}}_{\rho}$. By construction, we have

$t_{\Delta}\,{\dagger}\,\bar{n}\,a~{}\,{}^{{\mathfrak{s}}}\\!\\!\downarrow^{{\mathfrak{s}}}~{}\mathop{\mathsf{case}}\,\left(t_{\Phi}\,{h}\,\,{\dagger}\,({\mathsf{s}}n)\,{\dagger}\,({\mathsf{s}}n)\right)\,\\{\iota_{1}(c_{1})\mapsto\iota_{1}(t_{\leq{\mathsf{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_{\leq S(n)}\lor B_{\leq S(n)}$. Using 41, we get that

$(t_{\Phi}\,{h}\,\,{\dagger}\,({\mathsf{s}}n)\,{\dagger}\,({\mathsf{s}}n);{\mathfrak{s}})A(S(n))\lor
B_{\leq S(n)}.$

Using the adequacy of the ${\scriptstyle(\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}})A(S(n))$,
$t_{\leq{\mathsf{s}}}\,a\,v;{\mathfrak{s}}A_{\leq S(n)}$. This follows from 37
and the assumptions on $a$ and $v$.

######  Lemma 43.

For any internal formulas $A$ and $B$, we have

$u_{0}\Vvdash\left(\forall^{\\{\\!\mathrm{st}\\!\\}}{\\!}{x}.\forall^{\\{\\!\mathrm{st}\\!\\}}{\\!}{y}.(A(x)\lor
B(y))\right)\to\big{(}A_{\leq 0}\lor B_{\leq 0}\big{)},$

where $u_{0}\triangleq\lambda
h.\mathop{\mathsf{case}}\,(h\,{\dagger}\,0\,{\dagger}\,0)\,\\{\iota_{1}(a)\mapsto\iota_{1}(t_{\leq
0}\,a)|\iota_{2}(b)\mapsto\iota_{1}(t_{\leq 0}\,b)\\}$.

######  Proof 6.10.

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~{}\,{}^{{\mathfrak{s}}}\\!\\!\downarrow^{{\mathfrak{s}}}~{}\mathop{\mathsf{case}}\,(h\,{\dagger}\,0\,{\dagger}\,0)\,\\{\iota_{1}(a)\mapsto\iota_{1}(t_{\leq
0}\,a)|\iota_{2}(b)\mapsto\iota_{1}(t_{\leq 0}\,b)\\}.$

The result easily follows by anti-reduction, using the adequacy of the
${\scriptstyle(\lor_{E})}$ rule and 36.

######  Lemma 44.

For any internal formulas $A$ and $B$, we have

$u_{\mathsf{s}}\Vvdash\left(\forall^{\\{\\!\mathrm{st}\\!\\}}{\\!}{x}.\forall^{\\{\\!\mathrm{st}\\!\\}}{\\!}{y}.(A(x)\lor
B(y))\right)\to\forall^{\\{\\!\mathrm{st}\\!\\}}{\\!}{x}.\left(\left(A_{\leq
x}\lor B_{\leq x}\right)\to\left(A_{\leq S(x)}\lor B_{\leq
S(x)}\right)\right),$

where ${u_{\mathsf{s}}}\triangleq{\lambda
hwxd.\mathop{\mathsf{case}}\,d\,\\{\iota_{1}(d_{1})\mapsto
t_{\Delta}\,{h}\,w\,x\,d_{1}|\iota_{2}(d_{2})\mapsto
t_{\Delta}\,(t_{\lor}\,{h})\,w\,x\,d_{2}\\}}$.

######  Proof 6.11.

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}})\forall^{\\{\\!\mathrm{st}\\!\\}}{\\!}{x}.\forall^{\\{\\!\mathrm{st}\\!\\}}{\\!}{y}.(A(x)\lor
B(y))$ and $(v;{\mathfrak{s}})A_{\leq n}\lor B_{\leq n}$. By construction, we
have

$u_{\mathsf{s}}\,h\,{\dagger}\,\bar{n}\,v~{}\,{}^{{\mathfrak{s}}}\\!\\!\downarrow^{{\mathfrak{s}}}~{}\mathop{\mathsf{case}}\,v\,\\{\iota_{1}(a)\mapsto
t_{\Delta}\,{h}\,{\dagger}\,\bar{n}\,a|\iota_{2}(b)\mapsto
t_{\Delta}\,(t_{\lor}\,{h})\,{\dagger}\,\bar{n}\,b\\}.$

To conclude by anti-reduction, we use the adequacy of the
${\scriptstyle(\lor_{E})}$ rule to prove that the reduced term belongs to
$|A_{\leq S(n)}\lor B_{\leq S(n)}|^{\mathfrak{S}}_{\rho}$. For the
$\iota_{1}(\cdot)$ case, if $w$ is a term such that $(w;{\mathfrak{s}})A_{\leq
S(n)}$, then $(t_{\Delta}\,{h}\,{\dagger}\,\bar{n}\,w;{\mathfrak{s}})A_{\leq
S(n)}\lor B_{\leq S(n)}$ by 42 as expected. The $\iota_{2}(\cdot)$ case is
symmetric, using $t_{\lor}$ and 35.

######  Corollary 45.

For any internal formulas $A$ and $B$, we have

$t_{\mathrm{aux}}\Vvdash\left(\forall^{\\{\\!\mathrm{st}\\!\\}}{\\!}{x}.\forall^{\\{\\!\mathrm{st}\\!\\}}{\\!}{y}.(A(x)\lor
B(y))\right)\to\forall^{\\{\\!\mathrm{st}\\!\\}}{\\!}{x}.\left(A_{\leq x}\lor
B_{\leq x})\right),$

where $t_{\mathrm{aux}}\triangleq{\lambda
h.\mathop{\mathsf{rec}}\,(u_{0}\,h)\,(u_{S}\,h)}$.

######  Proof 6.12.

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

$t_{\mathrm{aux}}\,h\,{}^{{\mathfrak{s}}}\\!\\!\downarrow^{{\mathfrak{s}}}\mathop{\mathsf{rec}}\,(u_{0}\,h)\,(u_{\mathsf{s}}\,h),$

so the result easily follows from 27 and Lemmas 43 and 44.

We are now ready to prove the main theorem of this section, by combining all
the terms into a realizer of LLPOst.

######  Theorem 46 (LLPOst).

Let $A$ and $B$ be internal formulas, we have

$t_{\mathrm{LLPO}}\Vvdash\forall^{\\{\\!\mathrm{st}\\!\\}}{\\!}{x}.\forall^{\\{\\!\mathrm{st}\\!\\}}{\\!}{y}.(A(x)\vee
B(y))\to(\forall^{\\{\\!\mathrm{st}\\!\\}}{\\!}{x}.A(x)\lor\forall^{\\{\\!\mathrm{st}\\!\\}}{\\!}{y}.B(y)),$

where $t_{\mathrm{LLPO}}\triangleq\lambda
h.\mathop{\mathsf{case}}\,(t_{\mathrm{aux}}\,h\,{\dagger}\,\mathop{\mathsf{get}})\,\\{\iota_{1}(x_{1})\mapsto\iota_{1}(t_{\delta}\,x_{1})|\iota_{2}(x_{2})\mapsto\iota_{1}(t_{\delta}\,x_{2})\\}$.

######  Proof 6.13.

For any natural number $n\in{\mathbb{N}}$, if
$(u;{\mathfrak{s}})\forall^{\\{\\!\mathrm{st}\\!\\}}{\\!}{x}\forall^{\\{\\!\mathrm{st}\\!\\}}{\\!}{y}(A(x)\lor
B(y))$ using 45 we get

$(t_{\mathrm{aux}}\,u;{\mathfrak{s}})\forall^{\\{\\!\mathrm{st}\\!\\}}{\\!}{x}.(\forall^{\\{\\!{\mathbb{N}}\\!\\}}\\!z.z\leq
x\to A(z))\lor(\forall^{\\{\\!{\mathbb{N}}\\!\\}}\\!z.z\leq x\to B(z)\big{)}.$

By Transfer (25), we then obtain

$(t_{\mathrm{aux}}\,u\,{\dagger};{\mathfrak{s}})\forall^{\\{\\!{\mathbb{N}}\\!\\}}\\!x.(\forall^{\\{\\!{\mathbb{N}}\\!\\}}\\!z.z\leq
x\to A(z))\lor(\forall^{\\{\\!{\mathbb{N}}\\!\\}}\\!z.z\leq x\to B(z)\big{)},$

and in particular,

$(t_{\mathrm{aux}}\,u\,{\dagger};{\mathfrak{s}})\\{{\rm
Nature}\delta\\}\mapsto(\forall^{\\{\\!{\mathbb{N}}\\!\\}}\\!z.z\leq\delta\to
A(z))\lor(\forall^{\\{\\!{\mathbb{N}}\\!\\}}\\!z.z\leq\delta\to B(z)\big{)}.$

Using 23, we get

$(t_{\mathrm{aux}}\,u\,{\dagger}\,\mathop{\mathsf{get}};{\mathfrak{s}})(\forall^{\\{\\!{\mathbb{N}}\\!\\}}\\!z.z\leq\delta\to
A(z))\lor(\forall^{\\{\\!{\mathbb{N}}\\!\\}}\\!z.z\leq\delta\to B(z)\big{)}.$

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

##  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._ 47). 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 50, 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^{\mathfrak{S}}$
defined by $f\cong
g\triangleq\\{{\mathfrak{s}}\in{\mathfrak{S}}:f({\mathfrak{s}})=g({\mathfrak{s}})\\}\in\mathcal{U}$.

First, we can, within the realizability with slices, change the way
$\mathrm{st}(f)$ is interpreted to consider standardness up to the
ultrafilter. In this way, $f\in{\mathbb{N}}^{\mathfrak{S}}$ 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 47.

$\lambda xy.\mathsf{loop}^{+}\Vvdash\forall
x,y.\neg\mathrm{st}(x)\to{\mathrm{st}(y)\to{y<x}}$

######  Proof 7.1.

If $f\in{\mathbb{N}}^{\mathfrak{S}}$ 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},...,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|\mathrm{st}(f)\to\bot|^{\mathfrak{S}}$ and
$(u;{\mathfrak{s}})\in|\mathrm{st}(g)|^{\mathfrak{S}}$, 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}}^{\prime}>{\mathfrak{s}}$ such that
${\mathfrak{s}}<f({\mathfrak{s}}^{\prime})$. The result then follows by anti-
reduction from the fact that
$\mathsf{loop}^{+}\,{}^{{\mathfrak{s}}}\\!\\!\downarrow^{{\mathfrak{s}}^{\prime}}\mathsf{loop}^{+}$.

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}$_.

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{S}}_{\rho}\\}\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{S}}_{\rho}\\}\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{S}}}|A|^{*}_{\rho,x\mapsto
f}$).

[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{array}[]{rcl}|\mathrm{st}(f)|_{\rho}^{*}&\triangleq&\left\\{\begin{array}[]{ll}\Lambda&\text{
if $f\cong n^{*}$, for some $n\in{\mathbb{N}}$}\\\
\emptyset&\text{otherwise}\end{array}\right.\\\\[5.69054pt]
|X(e_{1},\dots,e_{n})|_{\rho}^{*}&\triangleq&\\{t\in\Lambda:\\{{\mathfrak{s}}\in{\mathfrak{S}}:(t;{\mathfrak{s}})\in\rho(X)@(\llbracket
e_{1}\rrbracket_{\rho},\dots,\llbracket
e_{n}\rrbracket_{\rho})\\}\in\mathcal{U}\\}\\\\[5.69054pt] |\\{{\rm
Nature}e\\}\mapsto
A|_{\rho}^{*}&\triangleq&\\{t\in\Lambda:\\{{\mathfrak{s}}\in{\mathfrak{S}}:(t;{\mathfrak{s}})\in|\\{{\rm
Nature}{e}\\}\mapsto
A|^{\mathfrak{S}}_{\rho}\\}\in\mathcal{U}\\}\\}\\\\[5.69054pt] |A\rightarrow
B|_{\rho}^{*}&\triangleq&\\{t\in\Lambda:\\{{\mathfrak{s}}\in{\mathfrak{S}}:(t;{\mathfrak{s}})\in|A\to
B|^{\mathfrak{S}}_{\rho}\\}\in\mathcal{U}\\}\\\ |A_{1}\land
A_{2}|_{\rho}^{*}&\triangleq&\\{t\in\Lambda:\\{{\mathfrak{s}}\in{\mathfrak{S}}:(\pi_{1}(t);{\mathfrak{s}})\in|A_{1}|^{\mathfrak{S}}_{\rho}\land(\pi_{2}(t);{\mathfrak{s}})\in|A_{2}|^{\mathfrak{S}}_{\rho}\\}\in\mathcal{U}\\}\\\\[5.69054pt]
|\forall
x.A|_{\rho}^{*}&\triangleq&\bigcap_{f\in{\mathbb{N}}^{\mathfrak{S}}}|A|^{*}_{\rho,x\mapsto
f}\\\\[5.69054pt] |\exists
x.A|_{\rho}^{*}&\triangleq&\bigcup_{f\in{\mathbb{N}}^{\mathfrak{S}}}|A|^{*}_{\rho,x\mapsto
f}\\\\[5.69054pt] |\forall
X.A|_{\rho}^{*}&\triangleq&\bigcap_{F:{\mathbb{N}}^{k}\to\text{{\bf
SAT}}}|A|^{*}_{\rho,X\mapsto F}\\\\[5.69054pt] |\exists
X.A|_{\rho}^{*}&\triangleq&\bigcup_{F:{\mathbb{N}}^{k}\to\text{{\bf
SAT}}}|A|^{*}_{\rho,X\mapsto F}\end{array}$

We write $t\Vdash^{\\!\\!\raisebox{0.2pt}{\scriptsize*}}A$ if $t\in|A|^{*}$.

As shown in the following theorem, first-order quantifiers behave well w.r.t.
the ultrafilter.

######  Theorem 48 (Łoś ’ theorem).

First-order internal formulas as well as arbitrary conjunctions and
implications are Łoś -reducible.

######  Proof 7.2.

The proof goes by induction on the structure of $A$. In the cases $\\{{\rm
Nature}{e}\\}\mapsto A$, $X(e_{1},\dots,e_{n})$, $A\rightarrow B$ and $A\land
B$, the result follows directly from the definitions. The proof for the
quantifiers is similar to the usual proof of Łoś ’ theorem.

####  $\exists x.A$

By the induction hypothesis, we have that for any
$f\in{\mathbb{N}}^{\mathfrak{S}}$,

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

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

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

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

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

$\underline{\Rightarrow}\\!\raisebox{0.875pt}{$\rfloor$}~{}$Assume that there
exists $f\in{\mathbb{N}}^{\mathfrak{S}}$ such that $t\in|A|^{*}_{\rho,x\mapsto
f}$. Then it is easy to see that

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

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

$\underline{\Leftarrow}\\!\raisebox{0.875pt}{$\rfloor$}~{}$Assume now that
$E\triangleq\\{{\mathfrak{s}}\in{\mathfrak{S}}:\exists
n\in{\mathbb{N}}.t\in|A|^{\mathfrak{s}}_{\rho,x\mapsto
n^{*}}\\}\in\mathcal{U}.$

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

$g({\mathfrak{s}})\triangleq\left\\{\begin{array}[]{rl}n_{\mathfrak{s}}&\text{if
}{\mathfrak{s}}\in E\\\ 0&\text{otherwise}\\\ \end{array}\right.$

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

####  $\forall x.A$

By the induction hypothesis, for any $f\in{\mathbb{N}}^{\mathfrak{S}}$,

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

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

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

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

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

$\underline{\Rightarrow}\\!\raisebox{0.875pt}{$\rfloor$}~{}$We easily see that
for any $f\in{\mathbb{N}}^{\mathfrak{S}}$

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

and by upwards closure we conclude that $t\in|A|^{*}_{\rho,x\mapsto f}$.

$\underline{\Leftarrow}\\!\raisebox{0.875pt}{$\rfloor$}~{}$By contraposition,
assume that $\\{{\mathfrak{s}}\in{\mathfrak{S}}:\forall
n\in{\mathbb{N}}.t\in|A|^{\mathfrak{s}}_{\rho,x\mapsto
n^{*}}\\}\notin\mathcal{U}$ and let us show that there exists
$f\in{\mathbb{N}}^{\mathfrak{S}}$ such that
$t\notin|A|^{\mathfrak{s}}_{\rho,x\mapsto f}$. 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|^{\mathfrak{s}}_{\rho,x\mapsto
n^{*}}\\}}=\\{{\mathfrak{s}}\in{\mathfrak{S}}:\exists
n\in{\mathbb{N}}.t\notin|A|^{\mathfrak{s}}_{\rho,x\mapsto
n^{*}}\\}\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|^{\mathfrak{s}}_{\rho,x\mapsto
n_{\mathfrak{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|^{\mathfrak{s}}_{\rho,x\mapsto(g({\mathfrak{s}}))^{*}}\\}$,
and we conclude that $t\notin|A|^{*}_{\rho,x\mapsto f}$.

48 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, 48 applies to Transfer,
Idealization, Overspill or Underspill.

A simple example illustrating this new interpretation is the formula
$\forall^{\mathrm{st}}{x}.x<\delta$, which was realized by $\mathsf{loop}^{+}$
in the interpretation with slices (see 31) 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,
$\mathsf{loop}^{+}$ can be replaced by ${\dagger}$ in 47. 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\mathrm{st}(x)\to{\mathrm{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
subsection 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
$\mathbb{A}:n\in{\mathbb{N}}\mapsto|A(n)|^{\mathfrak{S}}_{\rho}$, 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^{\\!\\!\raisebox{0.2pt}{\scriptsize*}}\mathbb{Y}(n^{*})~{}~{}\Leftrightarrow~{}~{}\exists
t.t\Vdash^{\\!\\!\raisebox{0.2pt}{\scriptsize*}}\mathbb{X}(n^{*})\land\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 $\Lambda$ inducing its actual value in
the interpretation with slices):

$\mathbb{Y}(n)\triangleq\\{t\in\Lambda:\\{{\mathfrak{s}}\in{\mathfrak{S}}:t\mathbb{X}(n^{*})\land\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 50, 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 49.

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

######  Proof 7.3.

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

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

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

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

######  Remark 50.

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}^{*}$,
$t\,u\in|B|_{\rho}^{*}$, as is usual in realizability. Unfortunately, such a
definition is incompatible with 48, as the other inclusion in 49 does not
hold. To see this, let $A\triangleq\mathrm{Nat^{\prime}}(\tau)$ and
$B\triangleq\bot$ where $\tau$ is a non-computable function666To that end, one
can for instance consider the function $\tau$ which to each
${\mathfrak{s}}\in{\mathfrak{S}}$ 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|\leq{\mathfrak{s}}\land
t\,{}^{{\mathfrak{s}}}\\!\\!\downarrow^{{\mathfrak{s}}}\overline{n}\\}$ .
$\tau:{\mathfrak{S}}\to{\mathbb{N}}$ for which there is no term $u$ such that
$\forall{\mathfrak{s}}.u\,{}^{{\mathfrak{s}}}\\!\\!\downarrow^{{\mathfrak{s}}}\tau({\mathfrak{s}})$.
By construction, we have that $|A|^{*}=\emptyset$, so that obviously for any
$u\in|\mathrm{Nat^{\prime}}(\tau)|^{*}$, the function $(\lambda
x.x)\,u\in|\bot|^{*}$. Yet, for each state ${\mathfrak{s}}$ the truth value
$|\mathrm{Nat^{\prime}}(\tau)|^{\mathfrak{S}}_{\rho}$ is not empty (it
contains at least $(\overline{n},{\mathfrak{s}})$, for
$n=\tau({\mathfrak{s}})$) and therefore $(\lambda
x.x;{\mathfrak{s}})\notin|\mathrm{Nat^{\prime}}(\tau)\to\bot|^{\mathfrak{S}}_{\rho}$
(since for any
$(u;{\mathfrak{s}})\in|\mathrm{Nat^{\prime}}(\tau)|^{\mathfrak{S}}$,
$((\lambda x.x)\,u;{\mathfrak{s}})\notin|\bot|^{*}$).

As it turns out, 7.1 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 $t\,u\in|B|_{\rho}^{*}$, but
the $(\rightarrow_{I})$-rule is not adequate when considering substitutions of
variables by realizers in the quotiented truth values. In particular, 50
emphasizes that the structure of 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, 50 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 functions777This 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..

Second, as highlighted in Section 4, in the stateful interpretation the
$\mathop{\mathsf{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 51.

There exists an internal propositional formula $A$, a term $t$ and two states
${\mathfrak{s}}_{0},{\mathfrak{s}}_{1}$ such that
$(t;{\mathfrak{s}}_{0})\in|A|^{\mathfrak{S}}$ but
$(t;{\mathfrak{s}}_{1})\notin|A|^{\mathfrak{S}}$.

######  Proof 7.4.

Take for instance $A\triangleq(A_{1}\land\neg A_{1})\to A_{1}$,
$t\triangleq\mathop{\mathsf{rec}}\,(\lambda x.\pi_{1}(x))\,(\lambda
xyz.\pi_{2}(z))\,\mathop{\mathsf{get}}$, ${\mathfrak{s}}_{0}=0$ and
${\mathfrak{s}}_{1}=1$. We have:

  * •

$(t;0)\in|A|^{\mathfrak{S}}$: for any $(u;0)\in|A_{1}\land\neg
A_{1}|^{\mathfrak{S}}$,
$u\,{}^{0}\\!\\!\downarrow^{{\mathfrak{s}}}(u_{1},u_{2})$ with
$(u_{1};{\mathfrak{s}})\in|A_{1}|^{\mathfrak{S}}$, and

$t~{}~{}\,{}^{0}\\!\\!\downarrow^{0}~{}~{}(\mathop{\mathsf{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)~{}~{}\,{}^{0}\\!\\!\downarrow^{{\mathfrak{s}}}~{}~{}u_{1}.$

The result follows by anti-reduction.

  * •

$(t;1)\notin|A|^{\mathfrak{S}}$: for any $(u;1)\in|A_{1}\land
A_{2}|^{\mathfrak{S}}$,
$u\,{}^{1}\\!\\!\downarrow^{{\mathfrak{s}}}(u_{1},u_{2})$ with
$(u_{2};{\mathfrak{s}})\in|\neg A_{1}|^{\mathfrak{S}}$, and

$t~{}~{}\,{}^{1}\\!\\!\downarrow^{1}~{}~{}(\mathop{\mathsf{rec}}\,(\lambda
x.\pi_{1}(x))\,\lambda
xyz.\pi_{2}(z)\,1)\,u~{}~{}\,{}^{1}\\!\\!\downarrow^{1}~{}~{}(\lambda
xyz.\pi_{2}(z))0\,(\mathop{\mathsf{rec}}...)\,u~{}~{}\,{}^{1}\\!\\!\downarrow^{1}~{}~{}\pi_{2}(u)~{}~{}\,{}^{1}\\!\\!\downarrow^{{\mathfrak{s}}}~{}~{}u_{2}.$

Since $(u_{2};1)\in|\neg A_{1}|^{\mathfrak{S}}$, it cannot be the case that
$(u_{2};1)\in|A_{1}|^{\mathfrak{S}}$.

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, 7.1 does not take the computation
into account when defining the quotient, which turns out to be problematic as
50 shows. Therefore, it could be tempting to contemplate a notion of reduction
up to $\mathcal{U}$ as follows

$t\downarrow^{\mathcal{U}}u~{}~{}\triangleq~{}~{}\\{{\mathfrak{s}}\in{\mathfrak{S}}:\exists{\mathfrak{s}}^{\prime}.t\,{}^{{\mathfrak{s}}}\\!\\!\downarrow^{{\mathfrak{s}}^{\prime}}u\\}\in\mathcal{U}$

Nonetheless, such a definition leaves us even further form 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
${\mathfrak{S}}$ and, without loss of generality, assume that
$\\{{\mathfrak{s}}\in{\mathfrak{S}}:\exists
n\in{\mathbb{N}}.{\mathfrak{s}}=2n\\}\in\mathcal{U}$. In particular, this
implies that $\\{{\mathfrak{s}}\in{\mathfrak{S}}:\exists
n\in{\mathbb{N}}.{\mathfrak{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}$.

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 52.

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

  1. (1)

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

  2. (2)

$\\{{\mathfrak{s}}\in{\mathfrak{S}}:\exists{\mathfrak{s}}^{\prime}.t\,{}^{{\mathfrak{s}}}\\!\\!\downarrow^{{\mathfrak{s}}^{\prime}}u\\}\in\mathcal{U}$

  3. (3)

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

######  Proof 7.5.

Consider the (nonstandard) individual $\tau$ defined by
$\tau:n\in{\mathbb{N}}\mapsto n\mod 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 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 $\mathsf{next\\_odd}$ that computes it. We
let $u\triangleq\lambda x.x$ and
$t\triangleq\mathop{\mathsf{set}}\,(\mathsf{next\\_odd}\mathop{\mathsf{get}})\,u$.
For any state ${\mathfrak{s}}\in{\mathfrak{S}}$, we then have

$t~{}=~{}\mathop{\mathsf{set}}\,(\mathsf{next\\_odd}\mathop{\mathsf{get}})\,u~{}~{}\,{}^{{\mathfrak{s}}}\\!\\!\downarrow^{{\mathfrak{s}}}~{}~{}\mathop{\mathsf{set}}\,(\mathsf{next\\_odd}\,{\mathfrak{s}})\,~{}~{}\,{}^{{\mathfrak{s}}}\\!\\!\downarrow^{{\mathfrak{s}}}~{}~{}\mathop{\mathsf{set}}\,\overline{f({\mathfrak{s}})}\,u~{}~{}\,{}^{{\mathfrak{s}}}\\!\\!\downarrow^{f({\mathfrak{s}})}~{}~{}u,$

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

  1. (1)

$\\{{\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. (2)

$\\{{\mathfrak{s}}\in{\mathfrak{S}}:\exists{\mathfrak{s}}^{\prime}.t\,{}^{{\mathfrak{s}}}\\!\\!\downarrow^{{\mathfrak{s}}^{\prime}}u\\}={\mathfrak{S}}\in\mathcal{U}$

  3. (3)

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

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 53.

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

  1. (1)

$\\{{\mathfrak{s}}\in{\mathfrak{S}}:\exists{\mathfrak{s}}^{\prime}.t\,{}^{{\mathfrak{s}}}\\!\\!\downarrow^{{\mathfrak{s}}^{\prime}}u\land(u;{\mathfrak{s}}^{\prime})\in|A|^{\mathfrak{S}}_{\rho}\\}\in\mathcal{U}$

  2. (2)

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

######  Proof 7.6.

Take again the (nonstandard) individual $\tau$ defined by
$\tau:n\in{\mathbb{N}}\mapsto n\mod 2$, $\rho\triangleq x\mapsto\tau$ and
$A\triangleq x=1^{*}$. Let us define $u\triangleq\lambda x.x$,
$\mathop{\mathsf{incr}}\triangleq\lambda
x.\mathop{\mathsf{set}}\,({\mathsf{s}}\,\mathop{\mathsf{get}})\,x$
$t\triangleq\mathop{\mathsf{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=\mathop{\mathsf{set}}\,(\mathop{\mathsf{get}}+1)\,u\,{}^{{\mathfrak{s}}}\\!\\!\downarrow^{{\mathfrak{s}}+1}u$.
Hence

  1. (1)

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

  2. (2)

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

##  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 33), 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, $\exists$-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 ${\mathbb{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], $\mathrm{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.

###  8.3. 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.  doi:10.2307/2586854.
  * [BBE+18] Jacques Bair, Piotr Błaszczyk, Robert Ely, Peter Heinig, and Mikhail Katz.  Leibniz’s well-founded fictions and their interpetations.  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 realisability 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.
  * [Ło60] Jerzy Łoś.  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.