# Implicative models of set theory

Samuele Maschio  Alexandre Miquel  Dipartimento di Matematica “Tullio Levi-
Civita”
Università di Padova, Padova, Italy  Instituto de Matemática y Estadística
“Rafael Laguardia”,
Facultad de Ingeniería, Universidad de la República, Montevideo, Uruguay.

###### Abstract

In this paper we show that using implicative algebras one can produce models
of set theory generalizing Heyting/Boolean-valued models and realizability
models of $\mathbf{(I)ZF}$, both in intuitionistic and classical logic. This
has as consequence that any topos which is obtained from a
$\mathbf{Set}$-based tripos as the result of the tripos-to-topos construction
hosts a model of intuitionistic or classical set theory, provided a large
enough strongly inaccessible cardinal exists.

###### keywords:

Implicative algebra, intuitionistic and classical set theory, tripos.

††volume: NN††journal: Electronic Notes in Theoretical Informatics and
Computer Science††volume: NN††thanks: Email<EMAIL_ADDRESS>Email<EMAIL_ADDRESS>
##  1 Introduction

Implicative algebras were introduced by the second author [12] in order to
provide a common foundation for the model-theoretic constructions underlying
forcing and realizability.

Forcing was first introduced by Cohen [3] in the 60’s to prove the
independence of the Continuum Hypothesis with respect to $\mathbf{ZFC}$ and it
is the main technique used in set theory to obtain relative consistency
results. From an algebraic point of view, the technique of forcing amounts to
the construction of a Boolean-valued model of the considered theory, and this
construction can be further generalized to intuitionistic theories by
considering Heyting-valued models. On the other hand, realizability has been
introduced by Kleene [6] in the 40’s to interpret the computational content of
intuitionistic proofs. For a long time, this technique was limited to
intuitionistic theories, but in the mid-90’s Krivine [8] showed how to
reformulate its very principles to make them compatible with classical logic.

In order to compare forcing and realizability, Hyland, Johnstone and Pitts
introduced the notion of tripos [5], that can be seen as a categorical model
of higher-order logic. Such triposes may be constructed from complete Heyting
algebras, thus yielding forcing triposes, or from partial combinatory
algebras, thus yielding intuitionistic realizability triposes. More recently,
Streicher [15] showed how to turn an abstract Krivine structure into a tripos,
thus describing classical realizability in categorical terms. All these
triposes $\mathsf{P}$ can then be turned into toposes
$\mathbf{Set}[\mathsf{P}]$ by applying the tripos-to-topos construction [5].

In [12] the second author showed that forcing and realizability triposes are
instances of a more general notion of tripos induced by an implicative algebra
(which is called _implicative tripos_). Later, in [13], he proved that every
$\mathbf{Set}$-based tripos is in fact (isomorphic to) an implicative tripos.
These triposes include those arising from many different variants of
realizability, such as modified realizability triposes, relative realizability
triposes, classical realizability triposes and so on.

However, it is worth recalling that, from a proof-theoretic perspective, topos
theory is much weaker than set theory. Indeed, the internal theory of a topos
with a natural numbers object is strictly weaker than (intuitionistic or
classical) Zermelo set theory (IZ/Z), that is itself much weaker than
(intuitionistic or classical) Zermelo-Fraenkel set-theory (IZF/ZF).
Intuitively, the main difference is that in topos theory, one can only
quantify over the elements of a given set or object (i.e. bounded
quantification), whereas in set theory, one can also quantify over all
sets/objects (i.e. unbounded quantification).

In this paper we shall see how implicative algebras can be used to construct
_implicative_ models of intuitionistic and classical set theory (depending on
whether the underlying implicative algebra is intuitionistic or classical). We
will then see that our implicative models of set theory encompass
Heyting/Boolean-valued models for $\mathbf{(I)ZF}$ [1, 2] and, up to logical
equivalence, Friedman/Rosolini/McCarty realizability models for $\mathbf{IZF}$
[4, 14, 11] as well as the classical realizability models of $\mathbf{ZF}$
introduced by Krivine [7, 10].

Finally, in the last section, we will use the relationship between the logic
of a tripos $\mathsf{P}$ and the internal logic of the corresponding topos
$\mathbf{Set}[\mathsf{P}]$ to show that our implicative models of
$\mathbf{(I)ZF}$ can be seen as internal models of set theory in the toposes
constructed from implicative triposes. Since the second author proved [13]
that every $\mathbf{Set}$-based tripos is an implicative tripos (up to
isomorphism), we can conclude that every topos induced by a
$\mathbf{Set}$-based tripos hosts an internal model of set theory (provided a
large enough cardinal exists).

##  2 Intuitionistic and classical set theory

In the language of Zermelo-Fraenkel set theory the only terms are variables
and there are two binary predicate symbols: equality $=$ and membership $\in$.
As usual in the language of set theory $\forall x\in y\,\varphi$ is a
shorthand for $\forall x(x\in y\rightarrow\varphi)$ and $\exists x\in
y\,\varphi$ is a shorthand for $\exists x(x\in y\wedge\varphi)$, while
$x\subseteq y$ is a shorthand for $\forall z\in x\,(z\in y)$.

The theories $\mathbf{ZF}$ and $\mathbf{IZF}$ have both the following axioms,
but the logic underlying the former is classical, while it is intuitionistic
for the latter:

  1. $\mathbf{Ext})$

$\forall x\forall y\,(x\subseteq y\wedge y\subseteq x\rightarrow x=y)$

  2. $\mathbf{Pair})$

$\forall x\forall y\exists z\,(x\in z\wedge y\in z)$

  3. $\mathbf{Union})$

$\forall x\exists u\forall y\in x\forall z\in y\,(z\in u)$

  4. $\mathbf{Pow})$

$\forall x\exists z\forall y\,(y\subseteq x\rightarrow y\in z)$

  5. $\mathbf{Inf})$

$\exists u\mathbf{Inf}(u)$ where $\mathbf{Inf}(u)$ is the conjunction of the
formulas $\mathbf{Inf}_{1}(u):\equiv\exists x\in u\forall y\in x\,\bot$ and
$\mathbf{Inf}_{2}(u):\equiv\forall x\in u\exists y\in u(x\subseteq y\wedge
x\in y\wedge\forall z\in y(z\in x\vee z=x))$

  6. $\mathbf{Sep}_{\varphi})$

$\forall w_{1}....\forall w_{n}\forall x\exists y\left(\forall z\in y\,(z\in
x\wedge\varphi)\wedge\forall z\in x\,(\varphi\rightarrow z\in y)\right)$ for
all formulas $\varphi[w_{1},...w_{n},x,z]$ in context.

  7. $\mathbf{Col}_{\varphi})$

$\forall w_{1}....\forall w_{n}\forall y\left(\forall x\in y\exists
z\,\varphi\rightarrow\exists u\forall x\in y\exists z\in u\,\varphi\right)$
for all formulas in context $\varphi[w_{1},...w_{n},x,y,z]$.

  8. $\mathbf{\in\textrm{-}Ind}_{\varphi})$

$\forall w_{1}...\forall w_{n}(\forall x(\forall y\in
x\,\varphi[y/x]\rightarrow\varphi)\rightarrow\forall x\,\varphi)$ for all
formulas in context $\varphi[w_{1},...,w_{n},x]$.

##  3 Implicative algebras and implicative triposes

An _implicative algebra_ is a $4$-tuple
$\mathbb{A}=(A,\leq,\rightarrow,\Sigma)$ where

  1. (1)

$(A,\leq)$ is a complete lattice;

  2. (2)

$\rightarrow:A\times A\rightarrow A$ is a function which is monotone in the
second component and anti-monotone in the first component, and which satisfies
the following condition

$a\rightarrow\bigwedge_{i\in I}b_{i}=\bigwedge_{i\in I}\left(a\rightarrow
b_{i}\right)$

for every indexed family $(b_{i})_{i\in I}$ of elements of $A$ and every $a\in
A$;

  3. (3)

$\Sigma\subseteq A$ is upward closed, it contains $b$ as soon as it contains
$a\rightarrow b$ and $a$, and it contains $\mathbf{K}:=\bigwedge_{a,b\in
A}(a\rightarrow(b\rightarrow a))$ and $\mathbf{S}:=\bigwedge_{a,b\in
A}((a\rightarrow(b\rightarrow c))\rightarrow((a\rightarrow
b)\rightarrow(a\rightarrow c)))$.

Every complete Heyting algebra $(H,\leq)$ with Heyting implication
$\rightarrow$ gives rise to an implicative algebra
$(H,\leq,\rightarrow,\\{\top\\})$. Moreover, every total combinatory algebra
$(R,\cdot)$ gives rise to an implicative algebra
$(\mathcal{P}(R),\subseteq,\Rightarrow,\mathcal{P}(R)\setminus\\{\emptyset\\})$,
where $A\Rightarrow B:=\\{r\in R|\;r\cdot a\in B\textrm{ for every }a\in A\\}$
for every $A,B\subseteq R$. Other examples can be found in [12]. In the case
of a partial combinatory algebra $(R,\cdot)$, the $4$-uple
$(\mathcal{P}(R),\subseteq,\Rightarrow,\mathcal{P}(R)\setminus\\{\emptyset\\})$
is not in general an implicative algebra, but a quasi-implicative algebra (see
[12]). However, there is a standard way to transform it into an implicative
algebra in such a way that the tripos one obtains from it is equivalent to the
realizability tripos built from $(R,\cdot)$ (for details, see [12]).

An implicative algebra $\mathbb{A}=(A,\leq,\rightarrow,\Sigma)$ is _classical_
if $\bigwedge_{a,b\in A}(((a\rightarrow b)\rightarrow a)\rightarrow
a)\in\Sigma$. Complete Boolean algebras give rise to classical implicative
algebras following the recipe used for complete Heyting algebras. Last but not
least, classical implicative algebras can also be constructed from Abstract
Krivine Structures [15], the algebraic structure underlying classical
realizability [9].

Closed $\lambda$-terms with constant parameters in an implicative algebra
$\mathbb{A}$ can be encoded as elements of $\mathbb{A}$ itself as follows:
$a^{\mathbb{A}}:=a$ for every $a\in A$,
$(ts)^{\mathbb{A}}:=t^{\mathbb{A}}\cdot s^{\mathbb{A}}$ and $(\lambda
x.t)^{\mathbb{A}}:=\bigwedge_{a\in
A}\left(a\rightarrow(t[a/x])^{\mathbb{A}}\right)$ where the application
$\cdot$ is defined as follows for every $a,b\in A$:

$a\cdot b:=\bigwedge\\{x\in A|\,a\leq b\rightarrow x\\}$

If we define the combinators $\mathbf{k}$ as $\lambda x.\lambda y.x$ and
$\mathbf{s}$ as $\lambda x.\lambda y.\lambda z.xz(yz)$ as usual, one can show
(see [12]) that $\mathbf{K}=\mathbf{k}^{\mathbb{A}}$ and
$\mathbf{S}=\mathbf{s}^{\mathbb{A}}$.

Useful properties of the encoding of $\lambda$-terms in $\mathbb{A}$ are the
following:

  1. (1)

if $t$ $\beta$-reduces to $s$, then $t^{\mathbb{A}}\leq s^{\mathbb{A}}$;

  2. (2)

if $t$ is a pure $\lambda$-term with free variables $x_{1},...,x_{n}$ and
$a_{1},...,a_{n}\in\Sigma$, then
$(t[x_{1}:a_{1},...,x_{n}:a_{n}])^{\mathbb{A}}\in\Sigma$111We denote with
$t[x_{1}:a_{1},...,x_{n}:a_{n}]$ the $\lambda$-term obtained from $t$ by
substituting the variables $x_{1},...,x_{n}$ with $a_{1},...,a_{n}$,
respectively.; in particular the encodings of closed pure $\lambda$-terms are
elements of $\Sigma$.

In what follows we will remove the superscript $\mathbb{A}$ from the encoding
of $\lambda$-terms in order to lighten the notation.

For $a,b\in A$, we write $a\vdash_{\Sigma}b$ if $a\rightarrow b\in\Sigma$,
while we write $a\equiv_{\Sigma}b$ if $a\vdash_{\Sigma}b$ and
$b\vdash_{\Sigma}a$, moreover for every $a,b\in A$ following [12] we define:

$a\times b:=\bigwedge_{x\in A}\left((a\rightarrow(b\rightarrow x))\rightarrow
x\right)$ $a+b:=\bigwedge_{x\in A}\left((a\rightarrow
x)\rightarrow((b\rightarrow x)\rightarrow x)\right)$

and for every set indexed family $(a_{i})_{i\in I}$ we define

${{{\forall}}}_{i\in I}a_{i}:=\bigwedge_{i\in
I}a_{i}\qquad\qquad{{{\exists}}}_{i\in I}a_{i}:=\bigwedge_{x\in
A}\left(\bigwedge_{i\in I}\left(a_{i}\rightarrow x\right)\rightarrow x\right)$

Note that the operations $a\times b$ (implicative conjunction) and $a+b$
(implicative disjunction) are in general not associative, commutative or
idempotent on the nose (think of intuitionistic or classical realizability),
but they clearly are up to the equivalence $\equiv_{\Sigma}$ (logical
equivalence modulo the separator $\Sigma$). Also note that unlike universal
quantifications (that are simply interpreted as meets), existential
quantifications are not interpreted here as joins (as one would expect in
forcing or in intuitionistic realizability), but they are rather interpreted
using the standard second-order encoding of $\exists$ in minimal second-order
logic (thus using the same trick as in classical realizability). The reason is
that in the framework of implicative algebras (that contains classical
realizability as a particular case), joins do not satisfy the elimination rule
of existential quantification, except in particular cases that will be
discussed in Section 5.2. However, the price to pay for this encoding is that
the corresponding realizers are in general more complex.

We also introduce shorthands for some $\lambda$-terms:
$\overline{\mathbf{k}}:=\lambda x.\lambda y.y$, $\mathbf{p}:=\lambda x.\lambda
y.\lambda z.zxy$, $\mathbf{p}_{1}:=\lambda u.u\mathbf{k}$,
$\mathbf{p}_{2}:=\lambda v.v\overline{\mathbf{k}}$, $\mathbf{j}_{1}:=\lambda
x.\lambda z.\lambda w.zx$, $\mathbf{j}_{2}:=\lambda x.\lambda z.\lambda w.wx$,
$\mathbf{e}:=\lambda x.\lambda z.zx$. Notice that (the encodings of) all of
them belong to the separator $\Sigma$.

If $\Gamma$ is a finite list of variable assignments
$x_{1}:a_{1},...,x_{n}:a_{n}$ with $a_{1},...,a_{n}\in A$ and
$x_{1},...,x_{n}$ distinct variables, and $t$ is a $\lambda$-term with
parameters in $A$ and free variables among $x_{1},..,x_{n}$, we write
$\Gamma\vdash t:a$ as a shorthand for $t[\Gamma]^{\mathbb{A}}\leq a$ (where
$t[\Gamma]$ is the result of the substitution corresponding to $\Gamma$
applied to $t$) and the following rules are sound (this is a little variation
on the system of rules presented in [12]):

$\cfrac{x:a\in\Gamma}{\Gamma\vdash x:a}\;\qquad\cfrac{}{\Gamma\vdash
a:a}\qquad\cfrac{\Gamma\vdash t:a\qquad a\leq b}{\Gamma\vdash
t:b}\qquad\cfrac{\Gamma^{\prime}\leq\Gamma\qquad\Gamma\vdash
t:a}{\Gamma^{\prime}\vdash t:a}$ $\cfrac{\Gamma\vdash t:\bot}{\Gamma\vdash
t:a}\qquad\cfrac{\Gamma\vdash t:a}{\Gamma\vdash
t:\top}\qquad\cfrac{\Gamma\vdash t:a\rightarrow b\qquad\Gamma\vdash
s:a}{\Gamma\vdash ts:b}\qquad\cfrac{\Gamma,x:a\vdash t:b}{\Gamma\vdash\lambda
x.t:a\rightarrow b}$ $\cfrac{\Gamma\vdash t:a\qquad\Gamma\vdash
s:b}{\Gamma\vdash\mathbf{p}ts:a\times b}\qquad\cfrac{\Gamma\vdash t:a\times
b}{\Gamma\vdash\mathbf{p}_{1}t:a}\qquad\cfrac{\Gamma\vdash t:a\times
b}{\Gamma\vdash\mathbf{p}_{2}t:b}$ $\cfrac{\Gamma\vdash
t:a}{\Gamma\vdash\mathbf{j}_{1}t:a+b}\;\;\cfrac{\Gamma\vdash
t:b}{\Gamma\vdash\mathbf{j}_{2}t:a+b}\;\;\cfrac{\Gamma\vdash
t:a+b\qquad\Gamma,x:a\vdash u:c\qquad\Gamma,y:b\vdash v:c}{\Gamma\vdash
t(\lambda x.u)(\lambda y.v):c}$ $\cfrac{\Gamma\vdash t:a_{i}\,(\textrm{for all
}i\in I)}{\Gamma\vdash t:{{{\forall}}}_{i\in I}a_{i}}\qquad\cfrac{\Gamma\vdash
t:{{{\forall}}}_{i\in I}a_{i}}{\Gamma\vdash
t:a_{\overline{i}}}\;\overline{i}\in I$ $\cfrac{\Gamma\vdash
t:a_{\overline{i}}}{\Gamma\vdash\mathbf{e}t:{{{\exists}}}_{i\in
I}a_{i}}\;\overline{i}\in I\qquad\cfrac{\Gamma\vdash t:{{{\exists}}}_{i\in
I}a_{i}\qquad\Gamma,x:a_{i}\vdash u:b\,(\textrm{ for all }i\in
I)}{\Gamma\vdash t(\lambda x.u):b}$

where $\Gamma^{\prime}\leq\Gamma$ means that for every declaration $x:a$ in
$\Gamma$ we have $x:b$ in $\Gamma^{\prime}$ for some $b\leq a$.

As shown in [12], to every implicative algebra $\mathbb{A}$ can be associated
a tripos (see [5] or [16])

$\mathsf{P}_{\mathbb{A}}:\mathbf{Set}^{op}\rightarrow\mathbf{Heyt}$

by sending every set $I$ to the posetal reflection of the preordered set
$(A^{I},\vdash_{\Sigma[I]})$ where $\varphi\vdash_{\Sigma[I]}\psi$ if and only
if $\bigwedge_{i\in I}(\varphi(i)\rightarrow\psi(i))\in\Sigma$ (we will write
$\varphi\equiv_{\Sigma[I]}\psi$ if $\varphi\vdash_{\Sigma[I]}\psi$ and
$\psi\vdash_{\Sigma[I]}\varphi$) and every function $f:I\rightarrow J$ to the
function induced by the pre-composition function $(-)\circ f:A^{J}\rightarrow
A^{I}$. Componentwise use of $\times$, $+$ and $\rightarrow$ defines a Heyting
prealgebra structure (which needs not to be complete) on every preorder
$(A^{I},\vdash_{\Sigma[I]})$, which is preserved by pre-composition.
${{{\exists}}}$ and ${{{\forall}}}$ are used to produce left and right
adjoints to reindexing maps satisfying Beck-Chevalley condition, while a
generic predicate is given by (the equivalence class of) the identity function
on $A$.

A remarkable result in [13] is the following:

######  Theorem 3.1.

Let $\mathsf{P}:\mathbf{Set}^{op}\rightarrow\mathbf{Heyt}$ be a tripos. Then,
there exists an implicative algebra $\mathbb{A}$ such that $\mathsf{P}$ is
isomorphic to $\mathsf{P}_{\mathbb{A}}$.

Recall also (see e.g. [16]) that to every tripos $\mathsf{P}$ over
$\mathbf{Set}$ is associated an elementary topos $\mathbf{Set}[\mathsf{P}]$
obtained by means of the so-called “tripos-to-topos” construction (see [5])
whose internal logic can be reduced to that of the corresponding tripos as
shown e.g. in [16].

##  4 Implicative models of $\mathbf{(I)ZF}$

To define our implicative models we work in $\mathbf{ZFC}$ as metatheory and
for our convenience (see Remark 4.1) we further assume a strongly inaccessible
cardinal $\kappa$ to exist. Let now $\mathbb{A}$ be a fixed implicative
algebra with $|A|<\kappa$.

We define the following hierarchy of sets indexed by ordinals:

$W_{\alpha}^{\mathbb{A}}:=\begin{cases}\emptyset\textrm{ if }\alpha=0\\\
\mathsf{Part}(W_{\beta}^{\mathbb{A}},A)\textrm{ if }\alpha=\beta+1\\\
\bigcup_{\beta<\alpha}W_{\beta}^{\mathbb{A}}\textrm{ if }\alpha\textrm{ is a
limit ordinal}\\\ \end{cases}$

where $\mathsf{Part}(X,Y)$ denotes the set of partial functions from $X$ to
$Y$. We take $\mathbf{W}$ to be $W^{\mathbb{A}}_{\kappa}$. Since
$W_{\alpha}^{\mathbb{A}}\subseteq W_{\beta}^{\mathbb{A}}$ if $\alpha<\beta$,
one can assign a rank in the hierarchy to every element of $\mathbf{W}$ in the
obvious way. In particular, we can define simultaneously, by recursion on
rank, two functions
$\in_{\mathbf{W}},=_{\mathbf{W}}:\mathbf{W}\times\mathbf{W}\rightarrow A$:

  1. (1)

$\alpha\in_{\mathbf{W}}\beta:={{{\exists}}}_{t\in\partial_{0}(\beta)}\left(\beta(t)\times(t=_{\mathbf{W}}\alpha)\right)$222We
denote with $\partial_{0}(f)$ the domain of a partial function $f$, that is
the set of those $x$ for which $f(x)$ is defined.

  2. (2)

$\alpha=_{\mathbf{W}}\beta:=(\alpha\subseteq_{\mathbf{W}}\beta)\times(\beta\subseteq_{\mathbf{W}}\alpha)$
where
$\alpha\subseteq_{\mathbf{W}}\beta:={{{\forall}}}_{t\in\partial_{0}(\alpha)}\left(\alpha(t)\rightarrow
t\in_{\mathbf{W}}\beta\right)$.

We interpret the language of set theory in such a way that to every formula in
context $\varphi[x_{1},...,x_{n}]$ we associate a function

$\left\|\varphi[x_{1},...,x_{n}]\right\|:\mathbf{W}^{n}\rightarrow A$

by recursion on complexity of formulas as follows:

  1.   2. (1)

$\left\|x_{i}\in
x_{j}\,[x_{1},...,x_{n}]\right\|(\alpha_{1},...,\alpha_{n}):\equiv\alpha_{i}\in_{\mathbf{W}}\alpha_{j}$

  3. (2)

$\left\|x_{i}=x_{j}\,[x_{1},...,x_{n}]\right\|(\alpha_{1},...,\alpha_{n}):\equiv\alpha_{i}=_{\mathbf{W}}\alpha_{j}$

  4. (3)

$\left\|\bot[\underline{x}]\right\|(\underline{\alpha}):\equiv\bot$

  5. (4)

$\left\|\varphi\wedge\psi[\underline{x}]\right\|(\underline{\alpha}):\equiv\left\|\varphi[\underline{x}]\right\|(\underline{\alpha})\times\left\|\psi[\underline{x}]\right\|(\underline{\alpha})$

  6. (5)

$\left\|\varphi\vee\psi[\underline{x}]\right\|(\underline{\alpha}):\equiv\left\|\varphi[\underline{x}]\right\|(\underline{\alpha})+\left\|\psi[\underline{x}]\right\|(\underline{\alpha})$

  7. (6)

$\left\|\varphi\rightarrow\psi[\underline{x}]\right\|(\underline{\alpha}):\equiv\left\|\varphi[\underline{x}]\right\|(\underline{\alpha})\rightarrow\left\|\psi[\underline{x}]\right\|(\underline{\alpha})$

  8. (7)

$\left\|\exists
y\,\varphi\,[\underline{x}]\right\|(\underline{\alpha}):\equiv{{{\exists}}}_{\beta\in\mathbf{W}}\left(\left\|\varphi\,[\underline{x},y]\right\|(\underline{\alpha},\beta)\right)$

  9. (8)

$\left\|\forall
y\,\varphi\,[\underline{x}]\right\|(\underline{\alpha}):\equiv{{{\forall}}}_{\beta\in\mathbf{W}}\left(\left\|\varphi\,[\underline{x},y]\right\|(\underline{\alpha},\beta)\right)$444In
clauses (vii) and (viii), we assume, without loss of generality, that $y$ is
not a variable in the context $[\underline{x}]$.

  10.

We write $\mathbf{W}\vDash\varphi\,[\underline{x}]$ for
$\bigwedge_{\underline{\alpha}\in\mathbf{W}^{n}}\left(\left\|\varphi\,[\underline{x}]\right\|(\underline{\alpha})\right)\in\Sigma$
when $[\underline{x}]$ has length $n>0$, and for every closed formula
$\varphi$ we write $\mathbf{W}\vDash\varphi$ for
$\left\|\varphi\,[\,]\right\|\in\Sigma$. Thus,
$\mathbf{W}\vDash\varphi\,[\underline{x}]$ just means that
$\left\|\varphi[\underline{x}]\right\|$ is in the maximal class of
$\mathsf{P}_{\mathbb{A}}(\mathbf{W}^{n})$, where $n$ is the length of the
context of variables $[\underline{x}]$. We will often write
$\left\|\varphi\right\|$ instead of $\left\|\varphi[\,]\right\|$.

######  Remark 4.1.

Note that here, we chose to construct the model $\mathbf{W}$ as a set, so that
we can use it later (together with the suitable $\mathbb{A}$-equivalence) as
an object of the topos $\mathbf{Set}[\mathsf{P}_{\mathbb{A}}]$ induced by the
implicative algebra $\mathbb{A}$ (cf Section 6). However, if one is only
interested in the set-theoretic part of the work, it is actually simpler to
construct the model $\mathbf{W}$ as a proper class (as it is traditionally
done in forcing or in intuitionistic or classical realizability), thus
removing the need of assuming the existence of an inaccessible cardinal
$\kappa$ (whose only purpose is to make the model $\mathbf{W}$ fit into a
set).

###  4.1 Useful lemmas

######  Lemma 4.2.

There exist
$\mathbf{\rho},\mathbf{j},\mathbf{\sigma},\mathbf{s}_{1},\mathbf{s}_{2},\mathbf{s}_{3}\in\Sigma$
such that

  1. (1)

$\mathbf{\rho}\leq\bigwedge_{\alpha\in\mathbf{W}}\left(\alpha=_{\mathbf{W}}\alpha\right)$

  2. (2)

$\mathbf{j}\leq\bigwedge_{\alpha\in\mathbf{W}}\bigwedge_{u\in\partial_{0}(\alpha)}\left(\alpha(u)\rightarrow
u\in_{\mathbf{W}}\alpha\right)$

  3. (3)

$\mathbf{\sigma}\leq\bigwedge_{\alpha,\beta\in\mathbf{W}}\left(\alpha=_{\mathbf{W}}\beta\rightarrow\beta=_{\mathbf{W}}\alpha\right)$

  4. (4)

$\mathbf{s}_{1}\leq\bigwedge_{\alpha,\beta,\gamma\in\mathbf{W}}\left(\alpha=_{\mathbf{W}}\beta\times\gamma\in_{\mathbf{W}}\alpha\rightarrow\gamma\in_{\mathbf{W}}\beta\right)$

  5. (5)

$\mathbf{s}_{2}\leq\bigwedge_{\alpha,\beta,\gamma\in\mathbf{W}}\left(\alpha=_{\mathbf{W}}\beta\times\alpha\in_{\mathbf{W}}\gamma\rightarrow\beta\in_{\mathbf{W}}\gamma\right)$

  6. (6)

$\mathbf{s}_{3}\leq\bigwedge_{\alpha,\beta,\gamma\in\mathbf{W}}\left(\alpha=_{\mathbf{W}}\beta\times\gamma=_{\mathbf{W}}\alpha\rightarrow\gamma=_{\mathbf{W}}\beta\right)$

######  Proof 4.3.

  1. (1)

Let $\mathbf{\rho}$ be $\mathbf{y}f\in\Sigma$ where $f:=\lambda
r.\mathbf{p}(\lambda x.\mathbf{e}(\mathbf{p}xr))(\lambda
x.\mathbf{e}(\mathbf{p}xr))$ and $\mathbf{y}$ is a pure closed $\lambda$-term
which is a fixed point operator such that $\mathbf{y}f$ $\beta$-reduces to
$f(\mathbf{y}f)$ for every $f$ (see e.g. [16]). We claim that
$\mathbf{\rho}\leq\alpha=_{\mathbf{W}}\alpha$ for every $\alpha\in\mathbf{W}$.
Let $\alpha$ be an arbitrary element of $\mathbf{W}$ and let us assume that
$\mathbf{\rho}\leq\beta=_{\mathbf{W}}\beta$ for every $\beta\in\mathbf{W}$
with rank in the hierarchy strictly less than that of $\alpha$ (and thus in
particular for every element of the domain of $\alpha$). Then we can consider
the following derivation tree in which we used only rules from the previous
section.

$\cfrac{\cfrac{\cfrac{\cfrac{\cfrac{\cfrac{}{x:\alpha(u)\vdash
x:\alpha(u)\;(\textrm{for all
}u\in\partial_{0}(\alpha))}\qquad\cfrac{}{x:\alpha(u)\vdash\mathbf{\rho}:u=_{\mathbf{W}}u\;(\textrm{for
all
}u\in\partial_{0}(\alpha))}}{x:\alpha(u)\vdash\mathbf{p}x\mathbf{\rho}:\alpha(u)\times
u=_{\mathbf{W}}u\;(\textrm{for all
}u\in\partial_{0}(\alpha))}}{x:\alpha(u)\vdash\mathbf{e}(\mathbf{p}x\mathbf{\rho}):u\in_{\mathbf{W}}\alpha\;(\textrm{for
all }u\in\partial_{0}(\alpha))}}{\vdash\lambda
x.\mathbf{e}(\mathbf{p}x\mathbf{\rho}):\alpha(u)\rightarrow
u\in_{\mathbf{W}}\alpha\;(\textrm{for all
}u\in\partial_{0}(\alpha))}}{\vdash\lambda
x.\mathbf{e}(\mathbf{p}x\mathbf{\rho}):\alpha\subseteq_{\mathbf{W}}\alpha}}{\vdash\mathbf{p}(\lambda
x.\mathbf{e}(\mathbf{p}x\mathbf{\rho}))(\lambda
x.\mathbf{e}(\mathbf{p}x\mathbf{\rho})):\alpha=_{\mathbf{W}}\alpha}$

The last $\lambda$-term in the deduction tree is a $\beta$ reduction of
$\mathbf{\rho}$. Thus we can conclude that
$\mathbf{\rho}\leq\alpha=_{\mathbf{W}}\alpha$.

  2. (2)

Let $\mathbf{j}$ be defined as $\lambda
x.\mathbf{e}(\mathbf{p}x\mathbf{\rho})\in\Sigma$. Assume $\alpha\in\mathbf{W}$
and $u\in\partial_{0}(\alpha)$. Then
$x:\alpha(u)\vdash\mathbf{p}x\mathbf{\rho}:\alpha(u)\times u=_{\mathbf{W}}u$ .
Hence,
$x:\alpha(u)\vdash\mathbf{e}(\mathbf{p}x\mathbf{\rho}):u\in_{\mathbf{W}}\alpha$.
Thus

$\mathbf{j}\leq\bigwedge_{\alpha\in\mathbf{W}}\bigwedge_{u\in\partial_{0}(\alpha)}\left(\alpha(u)\rightarrow
u\in_{\mathbf{W}}\alpha\right)$

  3. (3)

$\mathbf{\sigma}$ can be just defined as $\lambda
x.\mathbf{p}(\mathbf{p}_{2}x)(\mathbf{p}_{1}x)\in\Sigma$

  4. (iv),(v),(vi)

Assume $\mathbf{s}_{3}$ to exist.

Let $\alpha,\beta,\gamma\in\mathbf{W}$ and let $\Gamma(u)$ be a shorthand for

$x:\alpha=_{\mathbf{W}}\beta\times\alpha\in_{\mathbf{W}}\gamma,y:\gamma(u)\times
u=_{\mathbf{W}}\alpha$

where $u$ an arbitrary element of the domain of $\gamma$. Since

$\vdash\mathbf{s}_{3}:\alpha=_{\mathbf{W}}\beta\times
u=_{\mathbf{W}}\alpha\rightarrow u=_{\mathbf{W}}\beta$

we obtain
$\Gamma(u)\vdash\mathbf{p}(\mathbf{p}_{1}y)(\mathbf{s}_{3}(\mathbf{p}(\mathbf{p}_{1}x)(\mathbf{p}_{2}y))):\gamma(u)\times
u=_{\mathbf{W}}\beta$ from which it follows that

$\Gamma(u)\vdash\mathbf{e}(\mathbf{p}(\mathbf{p}_{1}y)(\mathbf{s}_{3}(\mathbf{p}(\mathbf{p}_{1}x)(\mathbf{p}_{2}y)))):\beta\in_{\mathbf{W}}\gamma$

Since
$x:\alpha=_{\mathbf{W}}\beta\times\alpha\in_{\mathbf{W}}\gamma\vdash\mathbf{p}_{2}x:\alpha\in_{\mathbf{W}}\gamma$,
we get

$x:\alpha=_{\mathbf{W}}\beta\times\alpha\in_{\mathbf{W}}\gamma\vdash(\mathbf{p}_{2}x)(\lambda
y.\mathbf{e}(\mathbf{p}(\mathbf{p}_{1}y)(\mathbf{s}_{3}(\mathbf{p}(\mathbf{p}_{1}x)(\mathbf{p}_{2}y))))):\beta\in_{\mathbf{W}}\gamma$

from which it follows that

$\vdash\lambda x.(\mathbf{p}_{2}x)(\lambda
y.(\mathbf{e}(\mathbf{p}(\mathbf{p}_{1}y)(\mathbf{s}_{3}(\mathbf{p}(\mathbf{p}_{1}x)(\mathbf{p}_{2}y)))))):\alpha=_{\mathbf{W}}\beta\times\alpha\in_{\mathbf{W}}\gamma\rightarrow\beta\in_{\mathbf{W}}\gamma$

From this it follows that $\mathbf{s}_{2}$ can be defined as $\lambda
x.(\mathbf{p}_{2}x)(\lambda
y.(\mathbf{e}(\mathbf{p}(\mathbf{p}_{1}y)(\mathbf{s}_{3}(\mathbf{p}(\mathbf{p}_{1}x)(\mathbf{p}_{2}y))))))$.

Assume now $\mathbf{s}_{2}$ to exist and consider $\Gamma^{\prime}(u)$ a
shorthand for

$x:\alpha=_{\mathbf{W}}\beta\times\gamma\in_{\mathbf{W}}\alpha,y:\alpha(u)\times
u=_{\mathbf{W}}\gamma$

where $u$ is an arbitrary element of the domain of $\alpha$. We easily see
that

$\Gamma^{\prime}(u)\vdash\mathbf{p}(\mathbf{p}_{2}y)((\mathbf{p_{1}}(\mathbf{p}_{1}x))(\mathbf{p}_{1}y)):u=_{\mathbf{W}}\gamma\times
u\in_{\mathbf{W}}\beta$

Thus

$\Gamma^{\prime}(u)\vdash\mathbf{s}_{2}(\mathbf{p}(\mathbf{p}_{2}y)((\mathbf{p_{1}}(\mathbf{p}_{1}x))(\mathbf{p}_{1}y))):\gamma\in_{\mathbf{W}}\beta$

Since
$x:\alpha=_{\mathbf{W}}\beta\times\gamma\in_{\mathbf{W}}\alpha\vdash\mathbf{p}_{2}x:\gamma\in_{\mathbf{W}}\alpha$,
we have that

$x:\alpha=_{\mathbf{W}}\beta\times\gamma\in_{\mathbf{W}}\alpha\vdash(\mathbf{p}_{2}x)(\lambda
y.\mathbf{s}_{2}(\mathbf{p}(\mathbf{p}_{2}y)((\mathbf{p_{1}}(\mathbf{p}_{1}x))(\mathbf{p}_{1}y)))):\gamma\in_{\mathbf{W}}\beta$

from which it follows that

$\vdash\lambda x.(\mathbf{p}_{2}x)(\lambda
y.\mathbf{s}_{2}(\mathbf{p}(\mathbf{p}_{2}y)((\mathbf{p_{1}}(\mathbf{p}_{1}x))(\mathbf{p}_{1}y)))):\alpha=_{\mathbf{W}}\beta\times\gamma\in_{\mathbf{W}}\alpha\rightarrow\gamma\in_{\mathbf{W}}\beta$

Thus $\mathbf{s}_{1}$ can be defined as $\lambda x.(\mathbf{p}_{2}x)(\lambda
y.\mathbf{s}_{2}(\mathbf{p}(\mathbf{p}_{2}y)((\mathbf{p_{1}}(\mathbf{p}_{1}x))(\mathbf{p}_{1}y))))$.

Similarly, one can prove that if $\mathbf{s}_{1}$ is assumed to exist, then
one can define $\mathbf{s}_{3}$ as a $\lambda$-term containing
$\mathbf{s}_{1}$ as the unique parameter.

The idea is now to compose this mutual dependences to define, by a fix point
$\mathbf{y}g$, one among $\mathbf{s}_{1}$, $\mathbf{s}_{2}$ and
$\mathbf{s}_{3}$, and then define the other two using that one. So for
example, if we define $\mathbf{s}_{3}$ as a fixpoint, we can then define
$\mathbf{s}_{2}$ using $\mathbf{s}_{3}$ and then $\mathbf{s}_{1}$ using
$\mathbf{s}_{2}$. This works well since composing the proofs above one can see
that
$\mathbf{s}_{3}\leq\bigwedge_{\alpha,\beta,\gamma\in\mathbf{W}}\left(\alpha=_{\mathbf{W}}\beta\times\gamma=_{\mathbf{W}}\alpha\rightarrow\gamma=_{\mathbf{W}}\beta\right)$
whenever $\mathbf{s}_{3}\leq u=_{\mathbf{W}}v\times
w=_{\mathbf{W}}u\rightarrow w=_{\mathbf{W}}v$ for every $u,v,w$ with rank
strictly less than the maximum of the ranks of $\alpha$, $\beta$ and $\gamma$.

Given two lists of parameters
$\underline{\alpha}=\alpha_{1},\ldots,\alpha_{n}\in\mathbf{W}^{n}$ and
$\underline{\beta}=\beta_{1},\ldots,\beta_{n}\in\mathbf{W}^{n}$ (for $n\geq
0$), we write

$\underline{\alpha}=_{\mathbf{W}}\underline{\beta}~{}:=~{}(\cdots((\alpha_{1}=_{\mathbf{W}}\beta_{1}\times\alpha_{2}=_{\mathbf{W}}\beta_{2})\times\alpha_{3}=_{\mathbf{W}}\beta_{3})\cdots)\times\alpha_{n}=_{\mathbf{W}}\beta_{n}$
$None$

simply letting $\underline{\alpha}=_{\mathbf{W}}\underline{\beta}:=\top$ in
the particular case where $n=0$. Note that the element
$\underline{\alpha}=_{\mathbf{W}}\underline{\beta}$ ($\in A$) depends on the
order of the parameters $\underline{\alpha}=\alpha_{1},\ldots,\alpha_{n}$ and
$\underline{\beta}=\beta_{1},\ldots,\beta_{n}$ (and on the choice to associate
$\times$’s to the left) when considered on the nose, but up to the equivalence
$\equiv_{\Sigma}$, it is of course invariant under any (common) permutation of
the parameters $\underline{\alpha}$ and $\underline{\beta}$.

######  Lemma 4.4.

For every formula in context $\varphi\,[\underline{x}]$ where $\underline{x}$
has length $n>0$, there exists $\mathbf{r}^{\varphi[\underline{x}]}\in\Sigma$
such that

$\mathbf{r}^{\varphi[\underline{x}]}\leq\bigwedge_{\underline{\alpha}\in\mathbf{W}^{n}}\bigwedge_{\underline{\beta}\in\mathbf{W}^{n}}\left(\underline{\alpha}=_{\mathbf{W}}\underline{\beta}\times\left\|\varphi\,[\underline{x}]\right\|(\underline{\alpha})\rightarrow\left\|\varphi\,[\underline{x}]\right\|(\underline{\beta})\right)\,.$

######  Proof 4.5.

By induction on complexity of formulas by using the previous lemma for the
atomic cases.

Also the following lemma can be easily proved as a consequence of the previous
results and of the rules in the previous section.

######  Lemma 4.6.

Let $\varphi[\underline{x}]$ and $\psi[\underline{x}]$ be formulas in context
in the language of set theory and let $n$ be the length of $[\underline{x}]$.
If $\varphi\vdash^{\underline{x}}_{\mathbf{IL}^{=}}\psi$, then
$\left\|\varphi\,[\underline{x}]\right\|\vdash_{\Sigma[\mathbf{W}^{n}]}\left\|\psi\,[\underline{x}]\right\|$
(where with $\mathbf{IL}^{=}$ we denote first-order intuitionistic logic with
equality on the language of $\mathbf{(I)ZF}$). In the case in which
$\mathbb{A}$ is a classical implicative algebra, if
$\varphi\vdash^{\underline{x}}_{\mathbf{CL}^{=}}\psi$, then
$\left\|\varphi\,[\underline{x}]\right\|\vdash_{\Sigma[\mathbf{W}^{n}]}\left\|\psi\,[\underline{x}]\right\|$
(where with $\mathbf{CL}^{=}$ we denote first-order classical logic with
equality on the language of $\mathbf{(I)ZF}$).

######  Lemma 4.7.

If $[\underline{x}]$ has length $n$, then

$\left\|\exists z\in
y\,\varphi\,[\underline{x},y]\right\|\equiv_{\Sigma[\mathbf{W}^{n+1}]}\Lambda\underline{\alpha}.\Lambda\beta.{{{\exists}}}_{u\in\partial_{0}(\beta)}\left(\beta(u)\times\left\|\varphi\,[\underline{x},y,z]\right\|(\underline{\alpha},\beta,u)\right)$
$\left\|\forall z\in
y\,\varphi\,[\underline{x},y]\right\|\equiv_{\Sigma[\mathbf{W}^{n+1}]}\Lambda\underline{\alpha}.\Lambda\beta.{{{\forall}}}_{u\in\partial_{0}(\beta)}\left(\beta(u)\rightarrow\left\|\varphi\,[\underline{x},y,z]\right\|(\underline{\alpha},\beta,u)\right)$

######  Proof 4.8.

We consider the case of the existential quantifier and we leave the analogous
proof of the universal case to the reader. We also restrict to the case in
which $\underline{x}$ is empty. The general case is analogous, but only
heavier in notation. By definition of the interpretation we have that
$\left\|\exists z\in y\,\varphi\,[y]\right\|(\beta)$ is

$\eta:={{{\exists}}}_{\gamma\in\mathbf{W}}\left({{{\exists}}}_{u\in\partial_{0}(\beta)}(\beta(u)\times
u=_{\mathbf{W}}\gamma)\times\left\|\varphi\,[y,z]\right\|(\beta,\gamma)\right)$

We denote with $\eta_{1}(\gamma)$ the scope of the quantifier
${{{\exists}}}_{\gamma\in\mathbf{W}}$, while we denote with
$\eta_{2}(u,\gamma)$ the scope of the quantifier
${{{\exists}}}_{u\in\partial_{0}(\beta)}$. It is immediate to check that the
following sequent holds for every $\beta,\gamma\in\mathbf{W}$ and every
$u\in\partial_{0}(\beta)$:

$x:\eta,y:\eta_{1}(\gamma),z:\eta_{2}(u,\gamma)\vdash\mathbf{l}:(\beta=_{\mathbf{W}}\beta\times\gamma=_{\mathbf{W}}u)\times\left\|\varphi\,[y,z]\right\|(\beta,\gamma))$

where
$\mathbf{l}:=\mathbf{p}(\mathbf{p}\rho(\sigma(\mathbf{p}_{2}z)))(\mathbf{p}_{2}y)$.

With the notation from Lemma 4.4, we can conclude that

$x:\eta,y:\eta_{1}(\gamma),z:\eta_{2}(u,\gamma)\vdash\mathbf{r}^{\varphi[y,z]}\mathbf{l}:\left\|\varphi\,[y,z]\right\|(\beta,u)$

Thus
$x:\eta,y:\eta_{1}(\gamma),z:\eta_{2}(u,\gamma)\vdash\mathbf{p}(\mathbf{p}_{1}z)(\mathbf{r}^{\varphi[y,z]}\mathbf{l}):\beta(u)\times\left\|\varphi\,[y,z]\right\|(\beta,u)$.
Hence

$x:\eta,y:\eta_{1}(\gamma),z:\eta_{2}(u,\gamma)\vdash\mathbf{e}(\mathbf{p}(\mathbf{p}_{1}z)(\mathbf{r}^{\varphi[y,z]}\mathbf{l})):\exists_{w\in\partial_{0}(\beta)}(\beta(w)\times\left\|\varphi\,[y,z]\right\|(\beta,w))$

Using the rules of elimination of existential quantification, one can conclude
that

$\eta\rightarrow\exists_{w\in\partial_{0}(\beta)}(\beta(w)\times\left\|\varphi\,[y,z]\right\|(\beta,w))\geq\mathbf{l}^{\prime}\in\Sigma$

where $\mathbf{l}^{\prime}:=\lambda x.x\lambda y.(\mathbf{p}_{1}y)(\lambda
z.\mathbf{e}(\mathbf{p}(\mathbf{p}_{1}z)(\mathbf{r}^{\varphi[y,z]}\mathbf{l})))$.

It is easier to show that for every $\beta\in\mathbf{W}$

$\exists_{w\in\partial_{0}(\beta)}(\beta(w)\times\left\|\varphi\,[y,z]\right\|(\beta,w))\rightarrow\eta\geq\lambda
x.x\lambda
y.\mathbf{e}(\mathbf{p}(\mathbf{e}(\mathbf{p}(\mathbf{p}_{1}y)\rho))(\mathbf{p}_{2}y))\in\Sigma$

One can in fact write a deduction tree in which the existential quantifiers of
the consequent are both witnessed by a $w\in\partial_{0}(\beta)$ for which
$\beta(w)\times\left\|\varphi\,[y,z]\right\|(\beta,w)$ is assumed to hold.

######  Corollary 4.9.

$\left\|x\subseteq
y\,[x,y]\right\|\equiv_{\Sigma[\mathbf{W}^{2}]}\Lambda\alpha.\Lambda\beta.\left(\alpha\subseteq_{\mathbf{W}}\beta\right)$.

###  4.2 Validity of axioms

In this subsection we show that the interpretation we gave is in fact a model
of $\mathbf{IZF}$ (when $\mathbb{A}$ is not classical) or a model of
$\mathbf{ZF}$ (when $\mathbb{A}$ is classical), that is, if
$\mathbf{(I)ZF}\vdash\varphi$, then $\mathbf{W}\vDash\varphi$. In order to
show this we prove that every axiom of $\mathbf{(I)ZF}$ is valid in the
interpretation.

####  4.2.1 Extensionality

Thanks to Corollary 4.9 we know that

$\left\|\mathbf{Ext}\right\|\equiv_{\Sigma}{{{\forall}}}_{\alpha\in\mathbf{W}}{{{\forall}}}_{\beta\in\mathbf{W}}\left(\alpha\subseteq_{\mathbf{W}}\beta\times\beta\subseteq_{\mathbf{W}}\alpha\rightarrow\alpha=_{\mathbf{W}}\beta\right)\geq\lambda
x.x\in\Sigma$

Thus, $\mathbf{W}\vDash\mathbf{Ext}$.

####  4.2.2 Pair

$\left\|\mathbf{Pair}\right\|\equiv{{{\forall}}}_{\alpha\in\mathbf{W}}{{{\forall}}}_{\beta\in\mathbf{W}}{{{\exists}}}_{\gamma\in\mathbf{W}}\left(\alpha\in_{\mathbf{W}}\gamma\times\beta\in_{\mathbf{W}}\gamma\right)$

Let us consider arbitrary $\alpha,\beta\in\mathbf{W}$ and the partial function
$\eta_{\alpha,\beta}\in\mathbf{W}$ defined as follows:
$\partial_{0}(\eta_{\alpha,\beta})=\\{\alpha,\beta\\}$ and
$\eta_{\alpha,\beta}(u)=\top$ for every $u$ in the domain. By Lemma 4.2,
$\vdash\mathbf{\rho}:\alpha=_{\mathbf{W}}\alpha$, from which it follows that

$\vdash\mathbf{q}:=\mathbf{e}(\mathbf{p}\top\rho):\exists_{t\in\\{\alpha,\beta\\}}\left(\top\times
t=_{\mathbf{W}}\alpha\right)=\alpha\in_{\mathbf{W}}\eta_{\alpha,\beta}$

In the same way, we can show that
$\vdash\mathbf{q}:\beta\in_{\mathbf{W}}\eta_{\alpha,\beta}$. As a consequence

$\vdash\mathbf{q}^{\prime}:=\mathbf{p}\mathbf{q}\mathbf{q}:\alpha\in_{\mathbf{W}}\eta_{\alpha,\beta}\times\beta\in_{\mathbf{W}}\eta_{\alpha,\beta}$

Thus,
$\vdash\mathbf{e}\mathbf{q}^{\prime}:{{{\exists}}}_{\gamma\in\mathbf{W}}\left(\alpha\in_{\mathbf{W}}\gamma\times\beta\in_{\mathbf{W}}\gamma\right)$.
Since $\mathbf{e}\mathbf{q}^{\prime}$ does not depend on $\alpha$ and $\beta$
and belongs to $\Sigma$,

$\vdash\mathbf{e}\mathbf{q}^{\prime}:{{{\forall}}}_{\alpha\in\mathbf{W}}{{{\forall}}}_{\beta\in\mathbf{W}}{{{\exists}}}_{\gamma\in\mathbf{W}}\left(\alpha\in_{\mathbf{W}}\gamma\times\beta\in_{\mathbf{W}}\gamma\right)$

Hence $\mathbf{W}\vDash\mathbf{Pair}$.

####  4.2.3 Union

Thanks to Lemma 4.7 we know that

$\left\|\mathbf{Union}\right\|\equiv_{\Sigma}{{{\forall}}}_{\alpha\in\mathbf{W}}{{{\exists}}}_{\beta\in\mathbf{W}}{{{\forall}}}_{u\in\partial_{0}(\alpha)}\left(\alpha(u)\rightarrow{{{\forall}}}_{w\in\partial_{0}(u)}\left(u(w)\rightarrow
w\in_{\mathbf{W}}\beta\right)\right)$

Let us fix now an arbitrary $\alpha\in\mathbf{W}$ and let us define
$\zeta_{\alpha}\in\mathbf{W}$ as follows. The domain of $\zeta_{\alpha}$ is
$\bigcup_{u\in\partial_{0}(\alpha)}\partial_{0}(u)$ and for every element of
such domain $\zeta_{\alpha}(u)=\top$.

Let $w\in\bigcup_{u\in\partial_{0}(\alpha)}\partial_{0}(u)$, then
$\vdash\mathbf{p}\top\mathbf{\rho}:\top\times w=_{\mathbf{W}}w$ (we are using
Lemma 4.2), from which it follows that
$\vdash\mathbf{e}(\mathbf{p}\top\mathbf{r})):w\in_{\mathbf{W}}\zeta_{\alpha}$.
From this it follows that

$\vdash\lambda v^{\prime}.\lambda
v.\mathbf{e}(\mathbf{p}\top\mathbf{r})):{{{\forall}}}_{u\in\partial_{0}(\alpha)}\left(\alpha(u)\rightarrow{{{\forall}}}_{w\in\partial_{0}(u)}\left(u(w)\rightarrow
w\in_{\mathbf{W}}\zeta_{\alpha}\right)\right)$

and thus that

$\vdash\mathbf{e}(\lambda v^{\prime}.\lambda
v.\mathbf{e}(\mathbf{p}\top\mathbf{r}))):{{{\exists}}}_{\beta\in\mathbf{W}}{{{\forall}}}_{u\in\partial_{0}(\alpha)}\left(\alpha(u)\rightarrow{{{\forall}}}_{w\in\partial_{0}(u)}\left(u(w)\rightarrow
w\in_{\mathbf{W}}\beta\right)\right)$

Since $\mathbf{e}(\lambda v^{\prime}.\lambda
v.\mathbf{e}(\mathbf{p}\top\mathbf{r})))$ does not depend on $\alpha$ and it
is an element of $\Sigma$, we have

$\vdash\mathbf{e}(\lambda v^{\prime}.\lambda
v.\mathbf{e}(\mathbf{p}\top\mathbf{r}))):{{{\forall}}}_{\alpha\in\mathbf{W}}{{{\exists}}}_{\beta\in\mathbf{W}}{{{\forall}}}_{u\in\partial_{0}(\alpha)}\left(\alpha(u)\rightarrow{{{\forall}}}_{w\in\partial_{0}(u)}\left(u(w)\rightarrow
w\in_{\mathbf{W}}\beta\right)\right)$

and $\mathbf{W}\vDash\mathbf{Union}$.

####  4.2.4 Powerset

Using Corollary 4.9,
$\left\|\mathbf{Pow}\right\|\equiv_{\Sigma}{{{\forall}}}_{\alpha\in\mathbf{W}}{{{\exists}}}_{\beta\in\mathbf{W}}{{{\forall}}}_{\gamma\in\mathbf{W}}\left(\gamma\subseteq_{\mathbf{W}}\alpha\rightarrow\gamma\in_{\mathbf{W}}\beta\right)$.

Let us consider an arbitrary $\alpha\in\mathbf{W}$ and define
$\pi_{\alpha}\in\mathbf{W}$ as that partial function having domain
$A^{\partial_{0}(\alpha)}$ and for which $\pi_{\alpha}(u)=\top$ for every $u$
in the domain.

For every $\gamma\in\mathbf{W}$ we also define $\gamma_{\alpha}\in\mathbf{W}$
as follows. The domain of $\gamma_{\alpha}$ is $\partial_{0}(\alpha)$ and
$\gamma_{\alpha}(u):=u\in_{\mathbf{W}}\alpha\times u\in_{\mathbf{W}}\gamma$
for every $u$ in the domain.

We now use Lemma 4.2 and its notation. Let $u\in\partial_{0}(\gamma)$ and
$t\in\partial_{0}(\alpha)$. Then:

  1. (1)

$x:\gamma\subseteq_{\mathbf{W}}\alpha,y:\gamma(u),z:\alpha(t)\times
t=_{\mathbf{W}}u\vdash\mathbf{j}(\mathbf{p}_{1}z):t\in_{\mathbf{W}}\alpha$

  2. (2)

$x:\gamma\subseteq_{\mathbf{W}}\alpha,y:\gamma(u),z:\alpha(t)\times
t=_{\mathbf{W}}u\vdash\mathbf{p}_{2}z:t=_{\mathbf{W}}u$

  3. (3)

$x:\gamma\subseteq_{\mathbf{W}}\alpha,y:\gamma(u),z:\alpha(t)\times
t=_{\mathbf{W}}u\vdash\mathbf{s}_{2}(\mathbf{p}(\sigma(\mathbf{p}_{2}z))(\mathbf{j}y)):t\in_{\mathbf{W}}\gamma$

From this it follows that

$x:\gamma\subseteq_{\mathbf{W}}\alpha,y:\gamma(u),z:\alpha(t)\times
t=_{\mathbf{W}}u\vdash\widetilde{\mathbf{r}}:=\mathbf{e}(\mathbf{p}(\mathbf{p}(\mathbf{j}(\mathbf{p}_{1}z))(\mathbf{s}_{2}(\mathbf{p}(\sigma(\mathbf{p}_{2}z))(\mathbf{j}y))))(\mathbf{p}_{2}z)):u\in_{\mathbf{W}}\gamma_{\alpha}$

Since

$x:\gamma\subseteq_{\mathbf{W}}\alpha,y:\gamma(u)\vdash
xy:u\in_{\mathbf{W}}\alpha$

then

$x:\gamma\subseteq_{\mathbf{W}}\alpha,y:\gamma(u)\vdash xy(\lambda
z.\widetilde{\mathbf{r}}):u\in_{\mathbf{W}}\gamma_{\alpha}$

From this it follows that

$x:\gamma\subseteq_{\mathbf{W}}\alpha\vdash\lambda y.(xy(\lambda
z.\widetilde{\mathbf{r}})):\gamma\subseteq_{\mathbf{W}}\gamma_{\alpha}$

One can also easily show that $\vdash\lambda
z.(\mathbf{p}_{2}z):\gamma_{\alpha}\subseteq_{\mathbf{W}}\gamma$. Thus

$x:\gamma\subseteq_{\mathbf{W}}\alpha\vdash\overline{\mathbf{r}}:=\mathbf{p}\top(\mathbf{p}(\lambda
z.(\mathbf{p}_{2}z))(\lambda y.(xy(\lambda
z.\widetilde{\mathbf{r}})))):\top\times\gamma_{\alpha}=_{\mathbf{W}}\gamma$

Since $\gamma_{\alpha}$ is in the domain of $\pi_{\alpha}$ we hence have that

$x:\gamma\subseteq_{\mathbf{W}}\alpha\vdash\mathbf{e}\overline{\mathbf{r}}:\gamma\in\pi_{\alpha}$

We can thus conclude that $\vdash\lambda
x.\mathbf{e}\overline{\mathbf{r}}:\gamma\subseteq_{\mathbf{W}}\alpha\rightarrow\gamma\in_{\mathbf{W}}\pi_{\alpha}$.
Since $\lambda x.\mathbf{e}\overline{\mathbf{r}}$ and $\mathbf{e}(\lambda
x.\mathbf{e}\overline{\mathbf{r}})$ do not depend on $\gamma$ and $\alpha$ we
get,

$\vdash\mathbf{e}(\lambda
x.\mathbf{e}\overline{\mathbf{r}}):{{{\forall}}}_{\alpha\in\mathbf{W}}{{{\exists}}}_{\beta\in\mathbf{W}}{{{\forall}}}_{\gamma\in\mathbf{W}}\left(\gamma\subseteq_{\mathbf{W}}\alpha\rightarrow\gamma\in_{\mathbf{W}}\beta\right)$

Since $\mathbf{e}(\lambda x.\mathbf{e}\overline{\mathbf{r}})\in\Sigma$, we can
conclude that $\mathbf{W}\vDash\mathbf{Pow}$.

####  4.2.5 Infinity

For every $n\in\omega$, we define $\widehat{n}\in\mathbf{W}$ as follows:
$\partial_{0}(\widehat{n})=\\{\widehat{m}|\,m<n\\}$ and
$\widehat{n}(\widehat{m}):=\overline{m}$ where $\overline{m}\in\Sigma$ is
Church’s encoding of the natural number $m$666$\overline{0}:=\lambda x.\lambda
y.x$ and $\overline{n+1}:=\overline{s}\,\overline{n}$ where
$\overline{s}:\lambda z.\lambda x.\lambda y.y(zxy)$. We define
$\widehat{\omega}$ as the element of $\mathbf{W}$ with domain
$\\{\widehat{n}|\,n\in\omega\\}$ and defined by
$\widehat{\omega}(\widehat{n}):=\overline{n}$.

First, if we consider $\widehat{0}=\emptyset$ and we use Lemma 4.7, we can
easily see that

$\vdash\mathbf{e}(\mathbf{p}\overline{0}\top):{{{\exists}}}_{n\in\omega}(\widehat{\omega}(\widehat{n})\times{{{\forall}}}_{m<n}(\widehat{n}(\widehat{m})\rightarrow\bot))\equiv_{\Sigma}\left\|\mathbf{Inf}_{1}(u)[u]\right\|(\widehat{\omega})$

Moreover, one can construct a closed $\lambda$-term $f$ whose interpretation
is in $\Sigma$ such that for every $n,m\in\omega$

$\begin{cases}f\overline{n}\,\overline{m}\twoheadrightarrow_{\beta}\mathbf{j}_{1}(\mathbf{e}(\mathbf{p}\overline{m}\rho))\textrm{
if }\overline{m}\neq\overline{n}\\\
f\overline{n}\,\overline{m}\twoheadrightarrow_{\beta}\mathbf{j}_{2}\rho\textrm{
if }\overline{m}=\overline{n}\end{cases}$

Then, for every $n\in\omega$

$\vdash\lambda
u.f\overline{n}u:{{{\forall}}}_{i<n}(\widehat{n+1}(\widehat{i})\rightarrow((\widehat{i}\in_{\mathbf{W}}\widehat{n})+(\widehat{i}=_{\mathbf{W}}\widehat{n})))$

Moreover

$\vdash\lambda
x.\mathbf{e}(\mathbf{p}x\rho):\widehat{n}\subseteq_{\mathbf{W}}\widehat{n+1}$
$\vdash\mathbf{e}(\mathbf{p}\overline{n}\rho):\widehat{n}\in_{\mathbf{W}}\widehat{n+1}$

Using these facts, Lemma 4.7 and Corollary 4.9, one can easily show that
$\left\|\mathbf{Inf}_{2}(u)[u]\right\|(\widehat{\omega})\in\Sigma$.

Thus we can conclude that $\mathbf{W}\vDash\mathbf{Inf}$.

####  4.2.6 Separation

Assume $\varphi\,[\underline{w},x,z]$ be a formula in context with
$\underline{w}$ a list of variable of length $n$.

$\left\|\mathbf{Sep}_{\varphi}\right\|\equiv_{\Sigma}{{{\forall}}}_{\underline{\omega}\in\mathbf{W}^{n}}{{{\forall}}}_{\alpha\in\mathbf{W}}{{{\exists}}}_{\beta\in\mathbf{W}}\Big{(}{{{\forall}}}_{u\in\partial_{0}(\beta)}(\beta(u)\rightarrow
u\in_{\mathbf{W}}\alpha\times\left\|\varphi\,[\underline{w},x,z]\right\|(\underline{\omega},\alpha,u))\times$
${{{\forall}}}_{u^{\prime}\in\partial_{0}(\alpha)}(\alpha(u^{\prime})\rightarrow(\left\|\varphi\,[\underline{w},x,z]\right\|(\underline{\omega},\alpha,u^{\prime})\rightarrow
u^{\prime}\in_{\mathbf{W}}\beta))\Big{)}$

For an arbitrary $\alpha\in\mathbf{W}$ and
$\underline{\omega}\in\mathbf{W}^{n}$ we define
$\alpha_{\varphi}^{\underline{\omega}}\in\mathbf{W}$ as follows: its domain is
equal to the domain of $\alpha$, while
$\alpha_{\varphi}^{\underline{\omega}}(u):=\alpha(u)\times\left\|\varphi\,[\underline{w},x,z]\right\|(\underline{\omega},\alpha,u)$.
In order to show that $\mathbf{W}\vDash\mathbf{Sep}_{\varphi}$, it is
sufficient to find a $t\in\Sigma$ not depending on $\overline{\omega}$ and
$\alpha$ such that

$\vdash
t:{{{\forall}}}_{u\in\partial_{0}(\alpha)}(\alpha_{\varphi}^{\overline{\omega}}(u)\rightarrow
u\in_{\mathbf{W}}\alpha\times\left\|\varphi\,[\underline{w},x,z]\right\|(\underline{\omega},\alpha,u))\times$
${{{\forall}}}_{u^{\prime}\in\partial_{0}(\alpha)}(\alpha(u^{\prime})\rightarrow(\left\|\varphi\,[\underline{w},x,z]\right\|(\underline{\omega},\alpha,u^{\prime})\rightarrow
u^{\prime}\in_{\mathbf{W}}\alpha_{\varphi}^{\underline{\omega}}))$

But this is immediate to prove, since using Lemma 4.2

$\vdash\lambda
x.\mathbf{p}(\mathbf{j}(\mathbf{p}_{1}x))(\mathbf{p}_{2}x):{{{\forall}}}_{u\in\partial_{0}(\alpha)}(\alpha_{\varphi}^{\overline{\omega}}(u)\rightarrow
u\in_{\mathbf{W}}\alpha\times\left\|\varphi\,[\underline{w},x,z]\right\|(\underline{\omega},\alpha,u))$
$\vdash\lambda x.\lambda
y.\mathbf{e}(\mathbf{p}(\mathbf{p}xy)\mathbf{\rho}):{{{\forall}}}_{u^{\prime}\in\partial_{0}(\alpha)}(\alpha(u^{\prime})\rightarrow(\left\|\varphi\,[\underline{w},x,z]\right\|(\underline{\omega},\alpha,u^{\prime})\rightarrow
u^{\prime}\in_{\mathbf{W}}\alpha_{\varphi}^{\overline{\omega}}))$

####  4.2.7 $\in$-Induction

We now consider the axiom schema of $\in$-induction and we restrict to the
case of a formula in context $\varphi[x]$ since the general case is analogous,
but just heavier in notation. Let $\mathbf{y}$ be the fix-point operator we
have already used in the proof of Lemma 4.2 such that $\mathbf{y}f$
$\beta$-reduces to $f(\mathbf{y}f)$ for every $f$ and consider

$\mathbf{h}:=\mathbf{y}(\lambda h.\lambda x.x(\lambda y.hx))\in\Sigma$

in such a way that $\mathbf{h}\leq(\lambda h.\lambda x.x(\lambda
y.hx))\mathbf{h}\leq\lambda x.x(\lambda y.\mathbf{h}x)$.

Fix an arbitrary $\overline{\alpha}$ and assume that

$\mathbf{h}\leq{{{\forall}}}_{\alpha\in\mathbf{W}}\left({{{\forall}}}_{u\in\partial_{0}(\alpha)}(\alpha(u)\rightarrow\left\|\varphi[x]\right\|(u))\rightarrow\left\|\varphi[x]\right\|(\alpha)\right)\rightarrow\left\|\varphi[x]\right\|(\beta)$

for every $\beta$ with rank strictly less than that of $\overline{\alpha}$.
Let us use $\varepsilon^{\alpha}$ as a shorthand for

${{{\forall}}}_{u\in\partial_{0}(\alpha)}(\alpha(u)\rightarrow\left\|\varphi[x]\right\|(u))\rightarrow\left\|\varphi[x]\right\|(\alpha)$

and $\varepsilon$ as a shorthand for
${{{\forall}}}_{\alpha\in\mathbf{W}}\varepsilon^{\alpha}$.

If we consider the following derivation tree

$\cfrac{\cfrac{\cfrac{x:\varepsilon\vdash x:\varepsilon}{x:\varepsilon\vdash
x:\varepsilon^{\overline{\alpha}}}\qquad\cfrac{\cfrac{\cfrac{\cfrac{\cfrac{\vdash\mathbf{h}:\varepsilon\rightarrow\left\|\varphi\,[x]\right\|(u)\,(\textrm{
for every
}u\in\partial_{0}(\overline{\alpha}))}{x:\varepsilon\vdash\mathbf{h}:\varepsilon\rightarrow\left\|\varphi\,[x]\right\|(u)(\textrm{
for every }u\in\partial_{0}(\overline{\alpha}))}\qquad x:\varepsilon\vdash
x:\varepsilon}{x:\varepsilon\vdash\mathbf{h}x:\left\|\varphi\,[x]\right\|(u)(\textrm{
for every
}u\in\partial_{0}(\overline{\alpha}))}}{x:\varepsilon,y:\overline{\alpha}(u)\vdash\mathbf{h}x:\left\|\varphi\,[x]\right\|(u)(\textrm{
for every }u\in\partial_{0}(\overline{\alpha}))}}{x:\varepsilon\vdash\lambda
y.\mathbf{h}x:\overline{\alpha}(u)\rightarrow\left\|\varphi\,[x]\right\|(u)(\textrm{
for every }u\in\partial_{0}(\overline{\alpha}))}}{x:\varepsilon\vdash\lambda
y.\mathbf{h}x:{{{\forall}}}_{u\in\partial_{0}(\overline{\alpha})}(\overline{\alpha}(u)\rightarrow\left\|\varphi\,[x]\right\|(u))}}{x:\varepsilon\vdash
x(\lambda
y.\mathbf{h}x):\left\|\varphi[x]\right\|(\overline{\alpha})}}{\vdash\lambda
x.x(\lambda
y.\mathbf{h}x):\varepsilon\rightarrow\left\|\varphi[x]\right\|(\overline{\alpha})}$

we can conclude that
$\mathbf{h}\leq\varepsilon\rightarrow\left\|\varphi[x]\right\|(\overline{\alpha})$.

By transfinite induction we can hence conclude that

$\mathbf{h}\leq{{{\forall}}}_{\alpha\in\mathbf{W}}(\varepsilon\rightarrow\left\|\varphi[x]\right\|(\alpha))$

Since $\mathbf{h}\in\Sigma$ and, by using lemmas 4.6 and 4.7,
${{{\forall}}}_{\alpha\in\mathbf{W}}(\varepsilon\rightarrow\left\|\varphi[x]\right\|(\alpha))\equiv_{\Sigma}\left\|\in\textrm{-}\mathbf{Ind}_{\varphi}\right\|$,
we can conclude that $\mathbf{W}\vDash\in\textrm{-}\mathbf{Ind}_{\varphi}$.

####  4.2.8 Collection

In order to lighten the notation we will consider $\mathbf{Col}_{\varphi}$ for
a formula $\varphi$ in context $[x,y]$ (so without any additional parameter).
Moreover we will write $\varphi(a,b)$ instad of
$\left\|\varphi\,[x,y]\right\|(a,b)$.

Assume $\alpha\in\mathbf{W}$ and $u\in\partial_{0}(\alpha)$. Since $\kappa$ is
inaccessible, $|A|<\kappa$ and
$\\{\varphi(u,\gamma)|\,\gamma\in\mathbf{W}\\}\subseteq A$, there exists
$\eta<\kappa$ such that
${{{\exists}}}_{\gamma\in\mathbf{W}}(\top\times\varphi(u,\gamma))={{{\exists}}}_{\gamma\in
W^{\mathbb{A}}_{\eta}}(\top\times\varphi(u,\gamma))$. We define $\eta_{u}$ to
be the minimum such an $\eta$ and we define
$\overline{\eta}_{\alpha}:=\bigvee\\{\eta_{u}|\,u\in\partial_{0}(\alpha)\\}$
which is strictly less than $\kappa$, since the cardinality of
$\partial_{0}(\alpha)$ is strictly less than $\kappa$ (because $\kappa$ is
strongly inaccessible). We define $\beta_{\alpha}\in\mathbf{W}$ as the
constant function with value $\top$ and domain
$W^{\mathbb{A}}_{\overline{\eta}_{\alpha}}$. Using the calculus we can show
that there is an element $r\in\Sigma$ not depending on $\alpha$ such that

$\vdash
r:{{{\forall}}}_{u\in\partial_{0}(\alpha)}\left(\alpha(u)\rightarrow{{{\exists}}}_{\gamma\in\mathbf{W}}\varphi(u,\gamma)\right)\rightarrow$
$\qquad\qquad\qquad\qquad\qquad\qquad\qquad{{{\forall}}}_{u\in\partial_{0}(\alpha)}\left(\alpha(u)\rightarrow{{{\exists}}}_{w\in\partial_{0}(\beta_{\alpha})}(\beta_{\alpha}(w)\times\varphi(u,w))\right)$

and using this fact one can easily show that $\mathbf{Col}_{\varphi}$ is
validated in the model.

##  5 Relationship with forcing and realizability models of set theory

In this section, we show that the implicative models of $\mathbf{(I)ZF}$
constructed in the previous section encompass Heyting/Boolean-valued models
for $\mathbf{(I)ZF}$ [1, 2] and, up to logical equivalence,
Friedman/Rosolini/McCarty realizability models for $\mathbf{IZF}$ [4, 14, 11]
as well as Krivine’s realizability models of $\mathbf{ZF}$ [7, 10].

###  5.1 The case of forcing

When the parameterizing implicative algebra $\mathbb{A}$ of our model is a
complete Heyting/Boolean algebra (with a separator reduced to $\\{\top\\}$),
existential quantifications ${{{\exists}}}_{i\in I}a_{i}$ coincide with
suprema $\bigvee_{i\in I}a_{i}$ whereas implicative conjunctions $a\times b$
coincide with binary meets $a\wedge b$, as shown in [12]. So that in this
case, our implicative model of set theory boils down to the Heyting/Boolean-
valued model of $\mathbf{(I)ZF}$ induced by $\mathbb{A}$, such as described
e.g. in [1, 2]. Therefore forcing models of set theory (both in intuitionistic
and classical logic) appear to be instances of our construction.

###  5.2 The case of intuitionistic realizability

The case of intuitionistic realizability corresponds to the implicative
algebras $\mathbb{A}$ that are _compatible with joins_ , namely: the
implicative algebras satisfying the additional requirement that

$\bigwedge_{i\in I}(a_{i}\rightarrow b)=\Bigl{(}\bigvee_{i\in
I}a_{i}\Bigr{)}\rightarrow b$

for every family $(a_{i})_{i\in I}$ of elements of $\mathbb{A}$ and for every
$b$ in $\mathbb{A}$.

Typical examples of implicative algebras that are compatible with joins are
the ones coming from forcing (i.e. complete Heyting/Boolean algebras with a
separator reduced to $\\{\top\\}$) as well as the implicative algebras induced
by _combinatory algebras_ (CAs) or by _ordered combinatory algebras_ (OCAs).
On the other hand, the implicative algebras coming from classical
realizability are in general not compatible with joins. Note that unlike
(possibly ordered) combinatory algebras, _partial combinatory algebras_ (PCAs)
do not induce (full) implicative algebras, but _quasi-implicative algebras_
[12], in which one may have $(\top\rightarrow\top)\neq\top$. However, as shown
in [12], it is always possible to complete a quasi-implicative algebra into an
implicative algebra, simply by adding an extra top element, and without
changing the underlying logic. (Indeed, the triposes associated to a quasi-
implicative algebra and to its completion are isomorphic.) Moreover, when
applying this completion mechanism to a quasi-implicative algebra that comes
from a PCA, the resulting implicative algebra is always compatible with joins.

In an implicative algebra $\mathbb{A}$ that is compatible with joins,
existential quantification ${{{\exists}}}$ may not coincide with supremum
$\bigvee$, but both constructions are logically equivalent in the sense that

$\bigwedge_{(b_{i})_{i\in I}}\\!\\!\left(\mathop{{{{\exists}}}}\limits_{i\in
I}b_{i}\rightarrow\bigvee_{i\in
I}b_{i}\right)~{}\in~{}\Sigma\qquad\textrm{and}\qquad\bigwedge_{(b_{i})_{i\in
I}}\\!\\!\left(\bigvee_{i\in
I}b_{i}\rightarrow\mathop{{{{\exists}}}}\limits_{i\in
I}b_{i}\right)~{}\in~{}\Sigma$

Now, if we define on $\mathbf{W}$ a new interpretation
$\left\|-\right\|^{\mathsf{J}}$ of the language of set theory replacing
${{{\exists}}}$ by $\bigvee$ in the definition of the interpretation
$\left\|-\right\|$, we easily show (by a straightforward induction) that for
all formulas in context $\varphi\,[\underline{x}]$, both denotations
$\left\|\varphi\,[\underline{x}]\right\|$ and
$\left\|\varphi\,[\underline{x}]\right\|^{\mathsf{J}}$ are equivalent, in the
sense that

$\left\|\varphi\,[\underline{x}]\right\|~{}\vdash_{\Sigma[\mathbf{W}^{n}]}~{}\left\|\varphi\,[\underline{x}]\right\|^{\mathsf{J}}\qquad\text{and}\qquad\left\|\varphi\,[\underline{x}]\right\|^{\mathsf{J}}~{}\vdash_{\Sigma[\mathbf{W}^{n}]}~{}\left\|\varphi\,[\underline{x}]\right\|\,,$

where $n$ is the length of $\underline{x}$. The main interest of the new
interpretation is that when the implicative algebra $\mathbb{A}$ comes from a
CA, an OCA, or even a PCA through the completion mechanism mentioned above,
the alternative interpretation $\left\|-\right\|^{\mathsf{J}}$ coincides
exactly with the Friedman/Rosolini/McCarty realizability interpretation [4,
14, 11]. Therefore, intuitionistic realizability models appear to be
equivalent to some instances of our construction.

###  5.3 The case of classical realizability

As shown by Krivine [7, 10], classical realizability models of $\mathbf{ZF}$
can be constructed from _classical realizability algebras_ [9], or from the
(slightly simpler) _abstract Krivine structures_ (AKSs) introduced by
Streicher in [15]. Again, both structures are easily reformulated as
implicative algebras [12], which makes possible to compare Krivine’s model
construction with ours. Moreover, it has been shown in [12] that every
classical implicative algebra is equivalent (from the point of view of the
induced triposes) to some Streicher’s AKS, which shows that —at least from a
conceptual point of view— the models arising from classical implicative
algebras are essentially the same as the ones arising from classical
realizability. However, the relationship between Krivine’s classical
realizability models of ZF and our implicative models of ZF is much more
intricate than in the intuitionistic case, due to reasons of _polarity_ we now
need to explain.

For that, let us first recall that in our construction, a name in $\mathbf{W}$
is a partial function $\alpha\in\mathsf{Part}(\mathbf{W},A)$ associating to
each name $\beta\in\partial_{0}(\alpha)$ (in the domain of $\alpha$) a truth
value $\alpha(\beta)\in A$ that intuitively expresses ‘how much $\beta$
belongs to $\alpha$’. So that when $\beta\notin\partial_{0}(\alpha)$, it is
convenient to think that such a truth value implicitly defaults to $\bot$
(that is: ‘$\beta$ does not belong to $\alpha$’).

As a matter of fact, Krivine’s classical realizability interpretation of ZF
can be carried out entirely within the same universe $\mathbf{W}$ as our
interpretation—under the hypothesis that the parameterizing implicative
algebra $\mathbb{A}$ is classical, of course. However, the crucial point is
that in Krivine’s framework, the elements of $\mathbf{W}$ have definitely not
the same meaning as in ours, since for any two names $\alpha\in\mathbf{W}$ and
$\beta\in\partial_{0}(\alpha)$, the truth value $\alpha(\beta)\in A$ expresses
‘how much $\beta$ _does not_ belong to $\alpha$’ (according to Krivine). So
that when $\beta\notin\partial_{0}(\alpha)$, such a truth value now implicitly
defaults to $\top$.

Formally, Krivine’s classical realizability interpretation, written
$\left\|-\right\|^{\mathsf{K}}$, takes place in a variant of the language of
set theory where the membership predicate $\in$ has been replaced by a
_negated membership predicate_ $\notin$, from which the usual membership
predicate is defined by $x\in y:\equiv\lnot(x\notin y)$. To each pair of names
$\alpha,\beta\in\mathbf{W}$, Krivine associates two truth values
$\alpha\notin_{\mathbf{W}}^{\mathsf{K}}\beta$ and
$\alpha=_{\mathbf{W}}^{\mathsf{K}}\beta$, that are defined (again) by
induction on the ranks of $\alpha$ and $\beta$, letting:

$\begin{array}[]{r@{~{}~}c@{~{}~}l}\alpha\notin_{\mathbf{W}}^{\mathsf{K}}\beta~{}{}&:=\hfil~{}{}&{{{\forall}}}_{t\in\partial_{0}(\beta)}(t=_{\mathbf{W}}^{\mathsf{K}}\alpha\to\beta(t))\\\
\alpha=_{\mathbf{W}}^{\mathsf{K}}\beta~{}{}&:=\hfil~{}{}&(\alpha\subseteq_{\mathbf{W}}^{\mathsf{K}}\beta)\times(\beta\subseteq_{\mathbf{W}}^{\mathsf{K}}\alpha),\quad\textrm{where:}\quad(\alpha\subseteq_{\mathbf{W}}^{\mathsf{K}}\beta)~{}:=~{}{{{\forall}}}_{t\in\partial_{0}(\alpha)}(t\notin_{\mathbf{W}}^{\mathsf{K}}\beta\to\alpha(t))\\\
\end{array}$

Notice that Krivine’s definition of
$\alpha\notin_{\mathbf{W}}^{\mathsf{K}}\beta$ corresponds to the negation of
our definition of $\alpha\in_{\mathbf{W}}\beta$, whereas his definition of
$\alpha\subseteq_{\mathbf{W}}^{\mathsf{K}}\beta$ is exactly the contraposition
of our definition of $\alpha\subseteq_{\mathbf{W}}\beta$—keeping in mind that
in Krivine’s setting, $\beta(t)$ and $\alpha(t)$ have the same meaning as
$\lnot\beta(t)$ and $\lnot\alpha(t)$ in ours888The main benefit of focusing on
$\notin$ rather than on $\in$ is that the recursive interpretations of
$\notin$ and $\subseteq$ only rely on universal quantification, whose
interpretation is way simpler than existential quantification. The cost of
such a design is that it relies on many contrapositions, that require
classical reasoning.. Once the three primitive relations
$\alpha\notin_{\mathbf{W}}^{\mathsf{K}}\beta$,
$\alpha\subseteq_{\mathbf{W}}^{\mathsf{K}}\beta$ and
$\alpha=_{\mathbf{W}}^{\mathsf{K}}\beta$ have been recursively defined, the
usual notion of membership is then recovered letting
$\alpha\in_{\mathbf{W}}^{\mathsf{K}}\beta:=\lnot(\alpha\notin_{\mathbf{W}}^{\mathsf{K}}\beta)$,
and the rest of the interpretation (written $\left\|-\right\|^{\mathsf{K}}$)
is defined the same way as in our framework (cf Section 4).

Now if we want to relate Krivine’s interpretation with ours, we need to
formalize the fact that the same name $\alpha\in\mathbf{W}$ has different
meanings according to Krivine and according to us. For that, we introduce a
_set-negation operator_
$(\alpha\mapsto\tilde{\alpha}):\mathbf{W}\to\mathbf{W}$ that is defined by
induction on the rank of $\alpha\in\mathbf{W}$, letting:

$\tilde{\alpha}~{}:=~{}\bigl{\\{}\bigl{(}\tilde{\beta},\lnot\alpha(\beta)\bigr{)}~{}:~{}\beta\in\partial_{0}(\alpha)\bigr{\\}}$

Intuitively, this operator associates to each name $\alpha\in\mathbf{W}$
another name $\tilde{\alpha}\in\mathbf{W}$ that has the same meaning in our
framework (resp. in Krivine’s framework) as $\alpha$ in Krivine’s (resp. in
ours). In what follows, it is also convenient to consider set-negation as a
unary function symbol as well, that is written and interpreted as the set-
negation operator $(\alpha\mapsto\tilde{\alpha}):\mathbf{W}\to\mathbf{W}$.

Using the fact that the parameterizing implicative algebra $\mathbb{A}$ is
classical, we easily check that set-negation is involutive (w.r.t. both
interpretations), in the sense that:

$\|\forall
x\,(x=\tilde{\tilde{x}})\|~{}\in~{}\Sigma\qquad\textrm{and}\qquad\|\forall
x\,(x=\tilde{\tilde{x}})\|^{\mathsf{K}}~{}\in~{}\Sigma\,.$

We can now prove that both interpretations $\|{-}\|$ and
$\|{-}\|^{\mathsf{K}}$ are equivalent _up to set-negation of parameters_ , in
the sense that for all formulas in context $\varphi\,[\underline{x}]$, we
have:

$\left\|\varphi\,[\underline{\tilde{x}}]\right\|~{}\vdash_{\Sigma[\mathbf{W}^{n}]}~{}\left\|\varphi\,[\underline{x}]\right\|^{\mathsf{K}}\qquad\text{and}\qquad\left\|\varphi\,[\underline{x}]\right\|^{\mathsf{K}}~{}\vdash_{\Sigma[\mathbf{W}^{n}]}~{}\left\|\varphi\,[\underline{\tilde{x}}]\right\|\,,$

where $n$ is the length of $\underline{x}$, and writing
$\varphi[\underline{\tilde{x}}]$ for
$(\varphi[\underline{\tilde{x}}/\underline{x}])[\underline{x}]$. In
particular, for each closed formula $\varphi$ of ZF, we have:

$\left\|\varphi\right\|~{}\vdash_{\Sigma}~{}\left\|\varphi\right\|^{\mathsf{K}}\qquad\text{and}\qquad\left\|\varphi\right\|^{\mathsf{K}}~{}\vdash_{\Sigma}~{}\left\|\varphi\right\|\,.$

So that classical realizability models of ZF are also equivalent to some
instances of our construction.

##  6 Models of $\mathbf{(I)ZF}$ in a class of toposes

In any elementary topos $\mathcal{E}$ one can interpret first-order languages
using the doctrine of subobjects. In particular, an interpretation of the
language of $\mathbf{(I)ZF}$ is given by an object $V$ of $\mathcal{E}$ which
interprets the universe of sets and by a subobject $\varepsilon$ of $V\times
V$ which interprets the membership relation. Equality is always interpreted as
the diagonal subobject of $V\times V$. If all axioms of $\mathbf{(I)ZF}$ are
validated by the interpretation (that is, if every axiom is interpreted as the
maximum subobject) then we get a model of $\mathbf{IZF}$ which is in fact a
model of $\mathbf{ZF}$ when $\mathcal{E}$ is boolean.

When the topos $\mathcal{E}$ is obtained as the result of the tripos-to-topos
construction from a tripos $\mathsf{P}$, the internal logic of $\mathcal{E}$
can be reduced to the logic of the tripos $\mathsf{P}$ as explained in detail
in [16]. Indeed, in this case the objects of $\mathcal{E}$ are pairs
$(A,\rho)$ where $A$ is an object of the domain of $\mathsf{P}$ and
$\rho\in\mathsf{P}(A\times A)$ is a partial equivalence relation on $A$ with
respect to the logic of $\mathsf{P}$, and the subobjects of $(A,\rho)$
correspond to the predicates $\psi\in\mathsf{P}(A)$ which respect the relation
$\rho$. Such correspondence extends to a correspondence of connectives and
quantifiers between the logics of $\mathsf{P}$ and $\mathcal{E}$.

The implicative model we produced in the previous section using an implicative
algebra $\mathbb{A}$ can be seen as a model of $\mathbf{(I)ZF}$ in the
corresponding implicative tripos $\mathsf{P}_{\mathbb{A}}$. Moreover, since
$\mathbf{W}$ is a set and $[=_{\mathbf{W}}]$ is an equivalence relation on
$\mathbf{W}$ with respect to the logic of $\mathsf{P}_{\mathbb{A}}$ by Lemma
4.2 (i),(iii),(vi), we have that the pair $(\mathbf{W},[=_{\mathbf{W}}])$ is
an object of the topos $\mathbf{Set}[\mathsf{P}_{\mathbb{A}}]$. Finally, as a
consequence of Lemma 4.2 (iv),(v), the relation $[\in_{\mathbf{W}}]$ gives
rise to a subobject $\varepsilon_{\mathbf{W}}$ of
$(\mathbf{W},[=_{\mathbf{W}}])\times(\mathbf{W},[=_{\mathbf{W}}])$ in
$\mathbf{Set}[\mathsf{P}_{\mathbb{A}}]$. By reducing the internal logic of
$\mathbf{Set}[\mathsf{P}_{\mathbb{A}}]$ to that of $\mathsf{P}_{\mathbb{A}}$
one obtains that the object $(\mathbf{W},[=_{\mathbf{W}}])$ and the subobject
$\varepsilon_{\mathbf{W}}$ define an interpretation of the language of
$\mathbf{(I)ZF}$ in $\mathbf{Set}[\mathsf{P}_{\mathbb{A}}]$ which is a model
of set theory in there. We thus have proved the following:

######  Theorem 6.1.

Every topos $\mathcal{E}$ obtained from an implicative tripos by means of the
tripos-to-topos construction from an implicative algebra
$\mathbb{A}=(A,\leq,\rightarrow,\Sigma)$ such that $|A|<\kappa$ for some
strongly inaccessible cardinal $\kappa$ hosts a model of $\mathbf{IZF}$. If
$\mathbb{A}$ is classical, then $\mathcal{E}$ hosts a model of $\mathbf{ZF}$.

Now, as a consequence of Theorem 3.1, we obtain the following:

######  Corollary 6.2.

If for every cardinal $\kappa^{\prime}$ there exists a strongly inaccessible
cardinal $\kappa$ such that $\kappa^{\prime}<\kappa$, then every topos
obtained from a $\mathbf{Set}$-based tripos by means of the tripos-to-topos
construction hosts a model of $\mathbf{IZF}$ (which is a model of
$\mathbf{ZF}$ when the topos is boolean).

#### Acknowledgements

The authors would like to acknowledge T. Streicher and F. Ciraulo for useful
discussions.

## References

  * [1] Bell, J., “Boolean-valued models and independence proofs,” Clarendon Press, Oxford, 1977, xviii+126 pp.
  * [2] Bell, J., “Intuitionistic set theory,” Studies in Logic (London) 50, College Publications, London, 2014, viii+120 pp.
  * [3] Cohen, P., _The independence of the continuum hypothesis_ , Proc. Nat. Acad. Sci. U.S.A. 50 (1963), pp. 1143–1148.
URL https://doi.org/10.1073/pnas.50.6.1143

  * [4] Friedman, H., _Some applications of Kleene’s methods for intuitionistic systems_ , in: _Cambridge Summer School in Mathematical Logic (Cambridge, 1971)_ , Lecture Notes in Math., Vol. 337, Springer, Berlin, 1973 pp. 113–170.
  * [5] Hyland, J., P. Johnstone and A. Pitts, _Tripos theory_ , Math. Proc. Cambridge Philos. Soc. 88 (1980), pp. 205–231.
URL https://doi.org/10.1017/S0305004100057534

  * [6] Kleene, S., _On the interpretation of intuitionistic number theory_ , J. Symbolic Logic 10 (1945), pp. 109–124.
URL https://doi.org/10.2307/2269016

  * [7] Krivine, J.-L., _Typed lambda-calculus in classical Zermelo-Frænkel set theory_ , Arch. Math. Logic 40 (2001), pp. 189–205.
URL https://doi.org/10.1007/s001530000057

  * [8] Krivine, J.-L., _Realizability in classical logic_ , in: _Interactive models of computation and program behavior_ , Panoramas & Synthèses 27, Soc. Math. de France, Paris, 2009 pp. 197–229.
  * [9] Krivine, J.-L., _Realizability algebras: a program to well order R_ , Logical Methods in Computer Science Volume 7, Issue 3 (2011).
URL https://lmcs.episciences.org/1070

  * [10] Krivine, J.-L., _Realizability algebras II : new models of ZF + DC_ , Logical Methods in Computer Science Volume 8, Issue 1 (2012).
URL http://lmcs.episciences.org/1072

  * [11] McCarty, D., “Realizability and Recursive Mathematics,” Ph.D. thesis, Oxford University (1984).
  * [12] Miquel, A., _Implicative algebras: a new foundation for realizability and forcing_ , Math. Structures Comput. Sci. 30 (2020), pp. 458–510.
URL https://doi.org/10.1017/s0960129520000079

  * [13] Miquel, A., _Implicative algebras ii: completeness w.r.t. set-based triposes_ (2020), arXiv:2011.09085.
  * [14] Rosolini, G., _Un modello per la teoria intuizionista degli insiemi_ , in: _Atti degli Incontri di Logica Matematica_ , Università di Siena. Scuola di Specializzazione in Logica Matematica, 1982 pp. 227–230.
  * [15] Streicher, T., _Krivine’s classical realisability from a categorical perspective_ , Math. Structures Comput. Sci. 23 (2013), pp. 1234–1256.
URL https://doi.org/10.1017/S0960129512000989

  * [16] van Oosten, J., “Realizability: an introduction to its categorical side,” Studies in Logic and the Foundations of Mathematics 152, Elsevier B. V., Amsterdam, 2008, xvi+310 pp.


11institutetext: Institute of Physics, University of Graz, NAWI Graz,
Universitätsplatz 5, 8010 Graz, Austria 22institutetext: Instituto de Física y
Matemáticas, Universidad Michoacana de San Nicolás de Hidalgo,
Morelia, Michoacán 58040, Mexico 33institutetext: Silicon Austria Labs GmbH,
Inffeldgasse 25F, 8010 Graz, Austria

# Elucidating the $\rho$-meson’s role as intermediate resonance in the time-
like electromagnetic pion form factor

Reinhard Alkofer 11<EMAIL_ADDRESS>Ángel S. Miramontes 22 angel-
<EMAIL_ADDRESS>Hèlios Sanchis Alepuz 33 helios.sanchis-alepuz@silicon-
austria.com

###### Abstract

Motivated by the planned measurements of the time-like electromagnetic proton
form factors an exploratory study of the time-like electromagnetic pion form
factor is presented in a formalism which describes mesons as Poincaré-
invariant bound states. In the respective quark interaction kernel, beyond the
gluon-intermediated interactions for valence-type quarks, non-valence effects
are included by allowing the pions to couple back in a self-consistent manner
to the quarks. Consequently, the opening of the dominant $\rho$ decay channel,
$\rho\to\pi\pi$, and the presence of a multi-particle branch cut, setting in
when the two-pion threshold is crossed, are included consistently, first in
the correspondingly calculated quark-photon vertex, and then consequently in
the time-like electromagnetic pion form factor. The obtained results are in
agreement with the available experimental data and provide further evidence
for the efficacy of a vector-meson dominance model. Effects of going beyond
the here employed isospin-symmetric limit are discussed. Last but not least,
an outlook is provided on how to include in Poincaré-covariant Faddeev
approaches the effects of intermediate resonances in the calculation of baryon
properties.

##  1 Introduction

Quantum Chromodynamics (QCD) provides the basis for our current understanding
of hadron physics. Perturbative as well as non-perturbative QCD calculations
have become impressively successful in the last decades. From a theoretical
point of view, QCD is a model Quantum Field Theory. It realises locality and
unitarity, and being asymptotically free QCD is an ultraviolet complete
Quantum Field Theory. The latter property quite obviously underlies the
success of perturbative calculations for hard hadronic and semi-hadronic
processes.

The perturbative description of elementary particles is essentially based on
the field-particle duality which means that each field in a Quantum Field
Theory is associated with a physical particle. Quite obviously, this is not
the case for the elementary fields of QCD, the quarks and gluons. First of
all, QCD being a gauge theory, together with the fact that only gauge-
invariant quantities can be observables, rules already out that quarks and
gluons can be directly observed. In a gauge theory, the rôle of fields is to
implement the principle of locality. The types of different elementary fields
needed in the theory is related to the structure of the gauge group, it is
not, at least not directly, related to the empirical spectrum of particles.
Second, what is usually referred to as “confinement” is obviously going beyond
the mere issue of “only-gauge-invariant-observables”, respectively, colour
confinement (see, e.g., refs. Greensite:2011zz ; Alkofer:2006fu ), and an
especially puzzling aspect is the following: As only hadrons are produced from
processes involving hadronic initial states, one has to explain that the only
thresholds in hadronic amplitudes are due to the productions of other hadronic
states. Consequently, singularities occurring in the amplitudes of hadronic
and thus composite states are exclusively due to their hadronic substructure,
or phrased otherwise, due to virtual fluctuations to hadronic resonances.

This implies not only that hadron spectroscopy and hadron structure are
strongly interrelated, but, in particular, that a microscopic understanding of
the effect of resonances on form factors, structure functions, etc., will shed
light on the precise working of quark-hadron duality. Compelling evidence for
the consequences of this duality on the qualitative as well as the semi-
quantitative level has been found (for a review see, e.g., Ref.
Melnitchouk:2005zr ) and contributed to a verification of this duality which
is, beyond the trivial fact of the absence of coloured states, the clearest
experimental signature for confinement. The attributed perfect orthogonality
of the quark and gluon degrees of freedom on the one hand and hadronic states
on the other hand, and thus the perfect absence of ââdouble-countingââ when
doing calculations either with quarks and gluons within QCD or within purely
hadronic descriptions, is nothing else but another way to express central
aspects of confinement. Basing a (confessedly impossible) exact calculation
for a hadronic or semi-hadronic scattering process either on elementary QCD
correlation functions or only on hadronic correlations functions needs to lead
to the same result by the virtue of colour confinement, the latter being a
consequence of gauge invariance. The way by which the hadronic amplitudes
become effectively independent of the singularities of the elementary
correlation functions is then an imprint of the dynamical realisation of
confinement.

The formation of an excited hadronic bound state, being an unstable resonance,
is closely related to the open decay channels. This is most evident from the
analysis of time-like form factors in kinematic regions close to a resonance.
To capture this interplay correctly in a QCD-based calculation of a hadron
form factor, the in- (respectively, out-) going hadron and the hadronic
resonance which is apparent in the form factor have to be described both in a
mutual consistent manner as composite objects of quarks and gluons. Thus, a
calculation of a time-like form factor from QCD, or from a microscopic model
based on QCD degrees of freedom, has to overcome the challenge to treat all
necessary elements on the same basis and to a sufficient degree of
sophistication. Only then the result will allow conclusions on the hadron
structure encoded in such a form factor.

It should be emphasised that the presented study aims for comprehending the
interplay of the different features of the form factor and as they arise from
the QCD degrees of freedom. It is also designed such that it can be
generalised to an investigation of baryon form factors, and hereby especially
the nucleons’ time-like form factor. (NB: Different space-like baryon form
factors have been calculated in this approach, see, e.g., Refs.
Eichmann:2016yit ; Nicmorus:2010sd ; Eichmann:2011vu ; Eichmann:2011pv ;
Sanchis-Alepuz:2013iia ; Sanchis-Alepuz:2017mir  for some recent respective
work.) A thorough understanding of the proton time-like form factor at very
low $Q^{2}$ is a very timely subject as the upcoming PANDA experiment
possesses the unique possibility to measure the proton’s electromagnetic form
factors in the so-called unphysical region through the process $\bar{p}p\to
l^{+}l^{-}\pi^{0}$, $l=e,\mu$ Fischer:2021kcr . At large $Q^{2}$ the question
of the onset of the convergence scale between the space-like and the time-like
form factors arises.

In this talk an exploratory study of the time-like pion electromagnetic form
factor employing a combination of Bethe-Salpeter and Dyson-Schwinger equations
Miramontes:2021xgn  will be discussed, and its results will be presented. To
obtain the most important features of the pions’ time-like form factor one
needs to take into account
(i) the pion as bound state of quark and antiquark thereby at the same
accommodating its special role as would-be Goldstone boson of the dynamically
broken chiral symmetry of QCD,
(ii) the mixing of the $\rho$-meson, being determined consistently as a quark-
antiquark bound state, with a virtual photon when this photon is in turn
coupled to a quark-antiquark pair via the fully renormalised quark-photon
vertex, and
(iii) the dominant decay channel of the $\rho$-meson, namely, $\rho\to\pi\pi$.

Before presenting how to combine these in our study a few general remarks
about the time-like pion electromagnetic form factor are in order.

##  2  The time-like electromagnetic pion form factor: General aspects

Figure 1: Electron-positron pair annihilating to a virtual photon with time-
like momentum which then decays to a pion pair.
$\gamma^{\star}$$e^{-}$$e^{+}$$F_{\pi}$$\pi^{+}$$\pi^{-}$

Experimentally the time-like electromagnetic pion form factor is typically
determined from electron-positron pair annihilation into a pion pair, see Fig.
1. In the physical region above the two-pion production threshold the
corresponding amplitude possesses a cut, and thus the time-like pion form
factor has to be treated as a complex quantity.

The pion form factor contains all kind of processes turning a virtual photon
into a pion pair, cf. Fig. 1. Using that in the interesting kinematic regime
strong-interaction processes dominate by orders of magnitude against
electroweak processes, an important first ingredient to the pion form factor
is how the virtual photon couples to a quark via all possible QCD processes.
The corresponding amplitude is nothing else than the full quark-photon vertex
which includes, at least in principle, the information about the virtual
photon’s hadronic substructure. The two more further ingredients are the quark
propagator and the pion bound state amplitude.

The presented study is performed in the isospin symmetric limit.111Isospin
breaking and thus the effect of $\rho$-$\omega$ mixing on the pion form factor
in the presented approach is currently under investigation. Corresponding
first results on electromagnetic and strong isospin breaking effects on the
mass splittings of light pseudo-scalar and vector mesons calculated from
Bethe-Salpeter and Dyson-Schwinger equations became recently available
Miramontes:2022mex . As isospin breaking is clearly visible in the time-like
pion form factor, in particular through $\rho$-$\omega$ mixing, a vector meson
dominance (VMD) based fit is used to extract the expected form of the pion
form factor without this mixing effect, see Fig. 2.

Figure 2: Absolute value of the pion form factor in the time-like ($Q^{2}<0$)
domain from the VMD-based fit given in ref. OConnell:1995nse  (full line) in
comparison to the experimental data Akhmetshin:2006bx . The dashed line is
based on the same expression but without $\rho$-$\omega$ mixing, i.e., the
mixing matrix element is put to zero.

As can be seen from Fig. 2 the VMD model of ref. OConnell:1995nse  describe
the experimental data precisely. But how does it arise from the dynamics of
QCD degrees of freedom?

##  3 Interactions in Dyson-Schwinger and Bethe-Salpeter equations

The interactions used in the exploratory study Miramontes:2021xgn  have been a
gluon exchange (in the form of the Maris-Tandy model Maris:1997tm ;
Maris:1999nt ) as well as a pion exchange and $s$\- and $u$-channel pion decay
contributions, see Fig. 3, the latter both in self-consistent manner. Here the
following disclaimer is in order: To keep this calculation feasible a number
of technically motivated approximations have been made. It has been checked
that these had only a minor impact on the results, for further details see
Ref. Miramontes:2021xgn .

Figure 3: Truncations used herein for the Bethe-Salpeter interaction kernel
$K$ (upper diagram) and the quark Dyson-Schwinger equation (lower diagram). In
the upper diagram, the terms on the right-hand side correspond to the gluon,
pion exchange, and s- and u-channel pion decay contributions to the
truncation, respectively. The s- and u-channel pion decay terms do not
contribute to the quark Dyson-Schwinger equation.

As already stated the quark-photon vertex is a decisive element in the
presented calculation. It has been determined with the above mentioned
interactions in Ref. Miramontes:2019mco . The Dirac structure of the vertex
can be expanded in a basis consisting of twelve elements, and all of them are
taken into account to obtain the below displayed results. In addition, out of
these twelve structure eight are transverse to the photon’s momentum. These
transverse amplitudes display a pole at the (calculated) $\rho$-meson mass and
multi-pion cut above the two-pion threshold.222This quark-photon vertex has
been recently used in a calculation of the pion and the kaon box contribution
to $a_{\mu}^{\text{HLbL}}$ Miramontes:2021exi  demonstrating its usability
also in the context of hadronic contributions to light-light scattering.

The Dyson-Schwinger and Bethe-Salpeter equations are integral equations which
are solved numerically. Hereby, for the presented calculation the major
technical challenge arises from the singularities of the integrands. This
implies that one has to find integration contours in presence of cuts
generated by quark propagator poles and the pion propagator pole as well as
two-pion cuts and the $\rho$ pole, the latter two also arising in the quark-
photon vertex. To this end one has to determine, typically by resolving
respective conditions numerically, the location of poles and cuts of the
integrand. Then the integration contour is deformed such no cuts are crossed
and no residues of poles are inadvertently picked up. Fig. 4 shows an example
of such a contour deformation. Note that different contour deformations have
to be done for different external momenta.

Figure 4: Shown is the complex $p^{2}$ plane such that time-like momenta
correspond to the left real half-axis. Without singularities in the integrand
the integration would be performed over space-like momenta, i.e., over the
right real half-axis. In the presented example this is not possible due to the
pion cut represented by the red fill line. Correspondingly, the integration
contour is deformed to the dashed blue line. The singularities of the quark
propagator are all to the left of the displayed parabola, and therefore do not
necessitate further contour deformations.

##  4 Results

For the presented exploratory calculation, the parameters are adjusted in a
simple manner, especially as we aim at a qualitative understanding of the
physical mechanisms involved in determining the shape of the pion form factor,
and not so much at achieving an accurate quantitative agreement with
experiment. As the pion-decay kernels will not only move the $\rho$-meson pole
into the complex plane but also shift down its real value a precise fit of the
two (effective) parameters of the Maris-Tandy model to reproduce the meson
masses would have required quite some computational resources. In addition,
only a reasonably accurate value for the pion decay constant, namely
$f_{\pi}$= 138 MeV has resulted. Although this value is a few percent larger
than the experimental one, $f^{expt.}_{\pi}=130.5$ MeV, we have adopted it in
view of a compromise in the effort needed for the parameter determination and
the related accuracy. In table 1 the determined meson masses as well as the
pion decay constant are shown.

Table 1:  The pion mass $m_{\pi}$, the pion decay constant $f_{\pi}$, the $\rho$-meson and $\omega$-meson masses $m_{\rho}$ and $m_{\omega}$ for the two different used parameterisations of the model (labeled with $\eta$) and for the case with gluon- and pion-exchange kernels but without decay kernels are shown. The current quark mass has been set to $m_{q}=6.8\leavevmode\nobreak\ $MeV. The two rightmost, separated, columns display for the case when including the decay kernels the extracted $\rho$-meson pole position defined as $M_{pole}^{2}=M_{\rho}^{2}-iM_{\rho}\Gamma_{\rho}$. All values for dimensionful quantities are given in GeV. $\Lambda=0.78$ | $m_{\pi}$ | $f_{\pi}$ | $m_{\rho}$ | $m_{\omega}$ | $M_{\rho}$ | $\Gamma_{\rho}$
---|---|---|---|---|---|---
$\eta=1.5$ | 0.139 | 0.138 | 0.768 | 0.778 | 0.750 | 0.100
$\eta=1.6$ | 0.126 | 0.138 | 0.774 | 0.784 | 0.759 | 0.105

The pion exchange kernels lift the otherwise present degeneracy in between the
iso-vector $\rho$\- and the iso-singlet $\omega$-meson. These interactions
induce a mass splitting $m_{\omega}-m_{\rho}=10$ MeV which compares favourably
with the experimental splitting of 7 - 8 MeV.

Fig. 5 displays our results for the space-like form factor from which we also
extract the result for the pion radius, $\sqrt{\langle r_{\pi}^{2}\rangle}=$
0.68 fm. It is reassuring that the space-like form factor, including the pion
radius, shows a very good agreement with experimental data. As we included the
most important physical processes with effects in the time-like regime we take
this as evidence that the imaginary part in the time-like region is precisely
enough reproduced to provide very good results for the space-like form factor.

Figure 5: Pion form factor in the spacelike $Q^{2}>0$ domain for the model
parameters $\eta=1.5$ and $\eta=1.6$. (The inset illustrates the impact of one
of the technically motivated approximations.) Figure 6: Absolute value of the
pion form factor in the time-like $Q^{2}<0$ domain for the model parameters
$\eta=1.5$ and $\eta=1.6$ as described in the text and compared to
experimental data Akhmetshin:2006bx .

The results for the absolute value of the pion form factor for time-like
($Q^{2}<0$) virtualities are displayed in Figs. 6. As a consequence of the
decay kernels, the pion form factor (as well as the quark-photon vertex)
possess a cut along the real negative axis starting at the two-pion threshold
$Q^{2}=-4m_{\pi}^{2}$, and therefore also an imaginary part contributes
significantly to the absolute value.

With decay kernels included, the $\rho$-meson pole, present in the quark-
photon vertex, moves into the complex plane, and consequently the pion form
factor develops a bump-like shape with approximately correct height and width.
Therefore the presented calculation corrects a deficiency of earlier
respective studies of the time-like pion form factor, without or even with the
pion exchange term, for which the form factor diverges at the $Q^{2}$-value
corresponding to the $\rho$-meson mass.

Table 2:  The coefficients of the rational fits to the pion form factor as discussed in the text. All values for dimensionful quantities are given in GeV. |  $\eta$ =1.5 |  $\eta$ =1.6 | VMD expression |  |  $\eta$ =1.5 |  $\eta$ =1.6 | VMD expression
---|---|---|---|---|---|---|---
$a_{1}$ | 0.5587 | 0.4149 | 0.72 | $c_{1}$ | 0.0591 | 0.0997 | 0
$a_{2}$ | 0.8828 | 0.6827 | 1.2 | $c_{2}$ | 0.1295 | 0.2383 | 0.2308
$b_{0}$ | 0.3600 | 0.3600 | 0.36 | $d_{0}$ | 0.3600 | 0.3600 | 0.36
$b_{1}$ | 1.2307 | 1.2517 | 1.2 | $d_{1}$ | 1.1924 | 1.2464 | 1.2
$b_{2}$ | 1.0722 | 1.1000 | 1.037 | $d_{2}$ | 0.9973 | 1.0916 | 1.037

In order to provide a measure for the proximity of our results to the VMD
predictions we performed rational fits (Padé fits) to the results for the real
part and for the imaginary part of the form factor and compare the
coefficients to the VMD expression without $\rho$-$\omega$ mixing. To stay as
general as possible we used first an ansatz with twelve parameters in total:

$\displaystyle Re\,F_{\pi}(Q^{2})-F_{\pi}(0)$ $\displaystyle\approx$
$\displaystyle-\frac{a_{0}+a_{1}Q^{2}+a_{2}(Q^{2})^{2}+a_{3}(Q^{2})^{3}}{b_{0}+b_{1}Q^{2}+b_{2}(Q^{2})^{2}+b_{3}(Q^{2})^{3}}$
$\displaystyle Im\,F_{\pi}(Q^{2})$ $\displaystyle\approx$
$\displaystyle\frac{c_{0}+c_{1}Q^{2}+c_{2}(Q^{2})^{2}+c_{3}(Q^{2})^{3}}{d_{0}+d_{1}Q^{2}+d_{2}(Q^{2})^{2}+d_{3}(Q^{2})^{3}}\,.$

We obtained almost vanishing values for the coefficients $a_{0}$, $a_{3}$,
$b_{3}$, $c_{0}$, $c_{3}$ and $d_{3}$. Phrased otherwise, the fit confirms the
structure expected from the VMD expression. Based on this, the fits have been
repeated for

$\displaystyle Re\,F_{\pi}(Q^{2})-F_{\pi}(0)$ $\displaystyle\approx$
$\displaystyle-\frac{a_{1}Q^{2}+a_{2}(Q^{2})^{2}}{b_{0}+b_{1}Q^{2}+b_{2}(Q^{2})^{2}}\,,$
$\displaystyle\quad Im\,F_{\pi}(Q^{2})$ $\displaystyle\approx$
$\displaystyle\frac{c_{1}Q^{2}+c_{2}(Q^{2})^{2}}{d_{0}+d_{1}Q^{2}+d_{2}(Q^{2})^{2}}\,.$
(2)

The coefficients resulting from these fitting ansätze as well as the ones
resulting from VMD expression are given in table 2. Note that the expression
based on the VMD hypothesis is an astonishingly good representation of the
results based on the microscopic model of QCD degrees of freedom: Other terms
than VMD-predicted ones are tiny, and the elaborated calculation yields within
error margin the VMD predicted functional form.

Another remark applies to the fact that there is no significant impact from
quark propagator poles on the pion form factor. As discussed in the
Introduction this is a wanted feature in the view of confinement, however, it
should be understood why this happens in the presented study which contains,
despite its quite high level of sophistication, not all QCD features.

Reassuring is nevertheless that the resulting time-like pion form factor in
the kinematic region $0>Q^{2}>0.8$GeV2 is determined by the $\rho$-meson pole
and the two-pion cut despite basing the calculation on QCD degrees of freedom.

##  5 Conclusions and Outlook

The main message of the presented study is the feasibility of studying time-
like quantities in a Dyson-Schwinger–Bethe-Salpeter approach including
intermediate resonances and thus decay channels in the interaction kernels.
Despite the applied modelling (which can be overcome in future investigations)
and the technical limitations inherent to the approach we found a remarkable
agreement with the experimental data.

As a side result we provided a detailed quantitative verification of the VMD
model for the pion form factor. In view of the fact that the $\rho$-meson pole
and the two-pion cut are determining the prominent features of the pion form
factor it might be considered expected that the VMD hypothesis should be, at
least, qualitatively correct. Therefore, the more surprising, and definitely
positive, aspect is that a microscopic model built on QCD degrees of freedom
provide a pion form factor shaped by the hadron substructure of the virtual
photon.

One obvious way to improve the presented study is to take isospin breaking via
the different quark masses and electric charges into account. First steps in
this direction have been undertaken Miramontes:2022mex , however, a
microscopic description for $\rho$-$\omega$-mixing including the decay
channels for these vector mesons, and its implementation into a calculation of
the pion form factor, is still a task to be performed yet.

It would be also worth to extend the presented study to calculate the $\gamma$
$\pi$ $\pi$ $\pi$ form factor which is only non-vanishing due to the chiral
anomaly. How in such a form factor, whose soft-point value is fixed due to the
anomaly and thus easily understood from the perspective of QCD, the hadron
resonances are determining the prominent time-like features will be of general
interest.

Last but not least, the question of the accessibility of the nucleons’ time-
like form factors arises. The presented study paves the way for an analogous
inclusion of decay kernels into baryon bound state equations. To this end we
note that a functional approach based on Dyson-Schwinger and bound-state
equations allows for a unified description of mesons and baryons, see, e.g.,
Ref. Eichmann:2016yit , which quite successfully describes the hadron spectrum
and space-like form factors. However, exactly these studies provide an
estimate about the dramatic increase in complexity when dealing with baryon
instead of meson bound state equations and a respective calculation of form
factors based on these equations. Nevertheless, given the increased effort
from the experimental side and the resulting anticipated highly precise data
over a large kinematical region certainly justifies the correspondingly
increased effort on the theoretical side.

## Acknowledgements

We are grateful to the organisers of the International Conference on Exotic
Atoms and Related Topics (EXA21) for all their efforts which made eventually
this (online) conference possible.
This work was partially supported by the the Austrian Science Fund (FWF) under
project number P29216-N36.
A.S. Miramontes acknowledges CONACyT for financial support.
The numerical computations have been performed at the high-performance compute
cluster of the University of Graz.

## References

  * (1) J. Greensite, An introduction to the confinement problem, Lect. Notes Phys. 972, 2nd ed., 2020.
  * (2) R. Alkofer and J. Greensite, J. Phys. G 34 (2007) S3 [arXiv:hep-ph/0610365 [hep-ph]].
  * (3) W. Melnitchouk, R. Ent and C. Keppel, Phys. Rept. 406 (2005) 127 [arXiv:hep-ph/0501217 [hep-ph]].
  * (4) Á. Miramontes, H. Sanchis-Alepuz and R. Alkofer, Phys. Rev. D 103 (2021) 116006 [arXiv:2102.12541 [hep-ph]].
  * (5) G. Eichmann, H. Sanchis-Alepuz, R. Williams, R. Alkofer and C. S. Fischer, Prog. Part. Nucl. Phys. 91 (2016) 1 [arXiv:1606.09602 [hep-ph]].
  * (6) D. Nicmorus, G. Eichmann and R. Alkofer, Phys. Rev. D 82 (2010) 114017 [arXiv: 1008.3184 [hep-ph]].
  * (7) G. Eichmann, Phys. Rev. D 84 (2011) 014014 [arXiv:1104.4505 [hep-ph]].
  * (8) G. Eichmann and C. S. Fischer, Eur. Phys. J. A 48 (2012) 9 [arXiv:1111.2614 [hep-ph]].
  * (9) H. Sanchis-Alepuz, R. Williams and R. Alkofer, Phys. Rev. D 87 (2013) 096015 [arXiv:1302.6048 [hep-ph]].
  * (10) H. Sanchis-Alepuz, R. Alkofer and C. S. Fischer, Eur. Phys. J. A 54 (2018) 41 [arXiv:1707.08463 [hep-ph]].
  * (11) G. Barucca et al. [PANDA], [arXiv:2101.11877 [hep-ex]].
  * (12) B. Ananthanarayan, I. Caprini and D. Das, Phys. Rev. D 102 (2020) 096003 [arXiv: 2008.00669 [hep-ph]].
  * (13) H. B. O’Connell, B. C. Pearce, A. W. Thomas and A. G. Williams, Prog. Part. Nucl. Phys. 39 (1997) 201 [arXiv:hep-ph/9501251 [hep-ph]].
  * (14) R. R. Akhmetshin et al. [CMD-2], Phys. Lett. B 648 (2007) 28 [arXiv:hep-ex/0610021 [hep-ex]].
  * (15) Á. S. Miramontes, R. Alkofer, C. S. Fischer and H. Sanchis-Alepuz, [arXiv:2202.04618 [hep-ph]].
  * (16) P. Maris and C. D. Roberts, Phys. Rev. C 56 (1997) 3369 [nucl-th/9708029].
  * (17) P. Maris and P. C. Tandy, Phys. Rev. C 60 (1999) 055214 [nucl-th/9905056].
  * (18) Á. S. Miramontes and H. Sanchis-Alepuz, Eur. Phys. J. A 55 (2019) 170 [arXiv: 1906.06227 [hep-ph]].
  * (19) Á. Miramontes, A. Bashir, K. Raya and P. Roig, arXiv:2112.13916 [hep-ph].