# Apartness and the elimination of strong forms of extensionality

Benno van den Berg1 1 ILLC, Universiteit van Amsterdam, P.O. Box 94242, 1090
GE Amsterdam, the Netherlands. E-mail<EMAIL_ADDRESS>
###### Abstract.

We introduce a new version of arithmetic in all finite types which extends the
usual versions with primitive notions of extensionality and extensional
equality. This new hybrid version allows us to formulate a strong form of
extensionality, which we call converse extensionality. Inspired by Brouwer’s
notion of apartness, we show that converse extensionality can be eliminated in
a way which improves on results from our previous work. We also explain how
standard proof-theoretic interpretations, like realizability and functional
interpretations, can be extended to such hybrid systems, and how that might be
relevant to proof-mining.

##  1\. Introduction

The standard approach towards the semantics of constructive logic is to
explain the meaning of a mathematical statement in terms of what counts as
evidence in its favour. This idea is the starting point for the Brouwer-
Heyting-Kolmogorov interpretation, various realizability interpretations and
type theory.

However, occasionally one also finds the idea of explaining the meaning of a
proposition in terms of “counter-evidence”: a piece of data that serves as
evidence _against_ a proposition. Examples of this are Brouwer’s notion of
apartness and Gödel’s Dialectica interpretation.

Brouwer came up with his notion of apartness in order to explain what it means
that two real numbers $r$ and $s$ are equal. This is not so easy; however,
saying what is needed to show that they are distinct (apart, in Brouwer’s
terminology) is much easier. Indeed, this one does by providing two non-
overlapping intervals with rational endpoints $q_{0},q_{1},q_{2},q_{3}$ such
that $r\in[q_{0},q_{1}]$ and $s\in[q_{2},q_{3}]$. Brouwer then defines
equality of two reals as the impossibility of obtaining evidence for their
apartness.

With respect to (extensional) equality of functions, we are in a similar
situation. It is easy to see what should be a counterargument against their
equality, and much less clear how one provides an argument in favour of their
equality. Indeed, to give a counterargument against the equality of functions
$f$ and $g$ means to point to an input on which they yield distinct outputs.
Given this, equality of the functions $f$ and $g$ can then be defined as the
impossibility of any counterargument against their equality.

If one takes the idea of counter-evidence seriously, it is natural to say that
for an implication $\varphi\to\psi$ to be valid, not only should evidence for
$\varphi$ give rise to evidence for $\psi$ (as in the traditional account),
but counter-evidence for $\psi$ should also give rise to counter-evidence for
$\varphi$. And this is what happens in Gödel’s Dialectica interpretation. One
can see this clearly when one looks at the Dialectica interpretation of the
following extensionality principle:

(1) $\displaystyle\forall f:(\sigma\to 0)\to(\tau\to 0).\forall x,y:\sigma\to
0.$ $\displaystyle\big{(}\,(\forall u:\sigma.xu=_{0}yu)\to(\forall
v:\tau.fxv=_{0}fyv)\,\big{)}.$

(Here 0 stands for the type of natural numbers.) This says that the functional
$f$ preserves extensional equality: if you give it functions $x$ and $y$ as
input and these are extensionally equal, then the outputs should also be
extensionally equal. Note that counter-evidence against the equality of $x$
and $y$ is a $u:\sigma$ such that $xu\not=_{0}yu$ and counter-evidence against
the equality of $fx$ and $fy$ is a $v:\tau$ such that $fxv\not=_{0}fyv$. So if
counter-evidence flows backwards along an implication, it should be possible
to find such a $u$ from such a $v$. That is, there should be a functional $Z$
such that

(2) $\displaystyle\forall f:(\sigma\to 0)\to(\tau\to 0).\forall x,y:\sigma\to
0.\forall v:\tau.$ $\displaystyle fxv\not=_{0}fyv\to
x(Zfxyv)\not=_{0}y(Zfxyv);$

this is essentially the Dialectica interpretation of the original statement.
(Indeed, it is equivalent to it, since $=_{0}$ is decidable.) In earlier work
we referred to (2) as a _converse extensionality principle_. It is a strong
form of extensionality, which implies, but is not implied by, the
extensionality principle (1). This means that if we wish to Dialectica
interpret extensionality, we are asked to witness converse extensionality,
which is not always possible. Indeed, one can find some striking limitative
results in the appendix of [5], written by W.A. Howard.

What is not excluded by these results, however, is that converse
extensionality can be eliminated in a manner similar to the well-known
elimination of extensionality due to Gandy and Luckhardt (see [4, Section
10.4]); by this we mean that we can interpret systems with such extensonality
principles in systems which do not possess them. Indeed, the main contribution
of this paper is to show that that is indeed possible for converse
extensionality using precisely Brouwer’s notion of apartness: this elimination
procedure will be called the _$\alpha$ -translation_ ($\alpha$ for apartness).

This is not the first time that the we have looked at apartness and converse
extensionality. Indeed, the contents of this paper are similar to that of [2],
written together with Robert Passmann. In the conclusion to that paper we
suggested that it might be possible to obtain stronger results if one could
have non-extensional witnesses for principles like converse extensionality. In
this paper we show that that is indeed the case. As a result, we manage to
eliminate converse extensionality for all finite types, instead of for very
low types only; in addition, we will do this without using continuity
principles.

The main obstacle that we needed to overcome in order to have non-extensional
witnesses for converse extensionality is that we had to find a good setting
where extensional and non-extensional objects can peacefully co-exist. To do
this, we will introduce a hybrid system for arithmetic. By this we mean an
extension of a neutral system like ${\textsf{HA}}^{\omega}$ with primitive
notions of extensionality and extensional equality for which we postulate some
axioms. Since the principle of converse extensionality is most naturally
understood as talking about the interaction between extensional and non-
extensional objects, this will be the right setting to formulate it.

The contents of this paper are therefore as follows. We will introduce our
hybrid system in Section 2. In Section 3 we will present a useful technical
result concerning the extensionality axiom. In Section 4 we will show that
Gandy and Luckhardt’s elimination of extensionality can be seen as a two-step
process with our hybrid system as an intermediate destination. In Section 5 we
will present our $\alpha$-translation and show how it eliminates converse
extensionality. In Section 6 we will briefly discuss how proof-theoretic
interpretations like modified realizability and functional interpretations can
be extended to hybrid systems. Finally, we conclude the paper with some
discussion and directions for future research in Section 7.

##  2\. A hybrid system for arithmetic

In this section we will introduce our hybrid system for arithmetic in finite
types. It extends the standard system ${\textsf{HA}}^{\omega}$ (as in [8])
with primitive notions of extensionality and extensional equality for which we
add some axioms.111Similar hybrid systems can be built on top of other
versions of arithmetic in finite types. We wil be using that there is a notion
of equality for all finite for which the congruence laws hold, so, as matter
stand, this might not be possible for the system ${\textsf{WE-HA}}^{\omega}$,
as in [4]. If one still wants to have a version which allows for Gödel’s
Dialectica interpretation, an good option is the system
${\textsf{HA}}_{0}^{\omega}$ from [1].

The system ${\textsf{HA}}^{\omega}$ is based on multi-sorted intuitionistic
logic, where the sorts are the finite types, as generated by the following
grammar:

$\mbox{type}=0\,|\,\mbox{type}\times\mbox{type}\,|\,\mbox{type}\to\mbox{type}.$

We will use small Greek letters as variables to range over the finite types.
The finite type 0 stands for the type of natural numbers and the finite types
are closed under product and function types. We use the convention that
$\times$ (and $\land$) binds stronger than $\to$ and that $\to$ associates to
the right, so $\rho\to\sigma\to\tau$ stands for $\rho\to(\sigma\to\tau)$.

Table 1. The combinators
$\begin{array}[]{ll}\mathsf{k}:&\rho\to\sigma\to\rho\\\
\mathsf{s}:&(\rho\to\sigma\to\tau)\to(\rho\to\sigma)\to(\rho\to\tau)\\\
\mathsf{pair}:&\sigma\to\tau\to\sigma\times\tau\\\
\mathsf{fst}:&\sigma\times\tau\to\sigma\\\
\mathsf{snd}:&\sigma\times\tau\to\tau\\\ 0:&0\\\ S:&0\to 0\\\
\mathsf{R}:&\sigma\to(0\to\sigma\to\sigma)\to(0\to\sigma)\end{array}$

For all types $\rho,\sigma$ and $\tau$, the language contains the constants
that can be found in Table 1, together with their types. If we were being
absolutely precise, we should say that for every pair of types $\rho$ and
$\sigma$, we have a combinator $\mathsf{k}_{\rho,\sigma}$ of type
$\rho\to\sigma\to\rho$, and similarly for the other combinators; however, we
will never write these indices and the reader is asked to infer these from the
context. We will use ${\bf c}$ as a metavariable ranging over all combinators.
Terms are built from these combinators and variables using application: that
is, if $s$ is a term of type $\sigma\to\tau$ and $t$ as term of type $\sigma$,
then the result of applying $s$ to $t$, written as $st$, is a term of type
$\tau$. Application associates to the left, and therefore $rst$ stands for
$(rs)t$.

The system ${\textsf{HA}}^{\omega}$ has a primitive notion of equality at each
type $\sigma$, which we will write $\equiv_{\sigma}$ or $\equiv$ when $\sigma$
is understood. It includes axioms stating that it is an equivalence relation
at each type, as well as a congruence:

$\begin{array}[]{c}x\equiv_{\sigma}x,\quad x\equiv_{\sigma}y\to
y\equiv_{\sigma}x,\quad x\equiv_{\sigma}y\to y\equiv_{\sigma}z\to
x\equiv_{\sigma}z,\\\ x\equiv_{\sigma\to\tau}x^{\prime}\to
y\equiv_{\sigma}y^{\prime}\to xy\equiv_{\tau}x^{\prime}y^{\prime}\end{array}$

We will assume the standard axioms for the combinators:

$\displaystyle\mathsf{k}xy$ $\displaystyle\equiv$ $\displaystyle x$
$\displaystyle\mathsf{s}xyz$ $\displaystyle\equiv$ $\displaystyle xz(yz)$
$\displaystyle\mathsf{fst}(\mathsf{pair}\,xy)$ $\displaystyle\equiv$
$\displaystyle x$ $\displaystyle\mathsf{snd}(\mathsf{pair}\,xy)$
$\displaystyle\equiv$ $\displaystyle y$ $\displaystyle\mathsf{R}xy0$
$\displaystyle\equiv$ $\displaystyle x$ $\displaystyle\mathsf{R}xy(Sm)$
$\displaystyle\equiv$ $\displaystyle ym(\mathsf{R}xym)$

We will not use that pairing is surjective (that is, that
$\mathsf{pair}(\mathsf{fst}\,x)(\mathsf{snd}\,x)\equiv x$ holds).

Finally, ${\textsf{HA}}^{\omega}$ contains the Peano axioms

$\begin{array}[]{c}Sx\equiv_{0}Sy\to x\equiv_{0}y,\quad
Sx\not\equiv_{0}0,\end{array}$

as well as the induction axiom for all formulas in the language of
${\textsf{HA}}^{\omega}$:

$\varphi(0)\to\forall x:0.\big{(}\,\varphi(x)\to\varphi(Sx)\,\big{)}\to\forall
x:0.\varphi(x).$

Let us also recall that ${\textsf{E-HA}}^{\omega}$ is the extension of
${\textsf{HA}}^{\omega}$ with the following extensionality principles:

$x\equiv_{\sigma\times\tau}y\leftrightarrow\mathsf{fst}\,x\equiv_{\sigma}\mathsf{fst}\,y\land\mathsf{snd}\,x\equiv_{\tau}\mathsf{snd}\,y,\quad
f\equiv_{\sigma\to\tau}g\leftrightarrow\forall x:\sigma.fx\equiv_{\tau}gx.$

The following well-known properties of ${\textsf{HA}}^{\omega}$ will be used
repeatedly in what follows.

######  Lemma 2.1.

For any finite type $\sigma$ there is a closed term $0_{\sigma}:\sigma$.

###### Proof.

We define $0_{\sigma}$ by induction on type structure of $\sigma$:

$\displaystyle 0_{0}$ $\displaystyle:\equiv$ $\displaystyle 0,$ $\displaystyle
0_{\sigma\times\tau}$ $\displaystyle:\equiv$
$\displaystyle\mathsf{pair}\,0_{\sigma}\,0_{\tau},$ $\displaystyle
0_{\sigma\to\tau}$ $\displaystyle:\equiv$ $\displaystyle\mathsf{k}\,0_{\tau}.$

∎

######  Proposition 2.2.

Let $t$ be a term of type $\tau$ and $x$ be a variable of type $\sigma$. Then
there is a term $\lambda x:\sigma.t$ of type $\sigma\to\tau$, whose free
variables are those of $t$ minus $x$, such that for any term $s$ of type
$\sigma$ we have ${\textsf{HA}}^{\omega}\vdash(\lambda x:\sigma.t)s\equiv
t[s/x]$.

###### Proof.

(See [4, Lemma 3.15] or [8, Proposition 9.1.8]) We define $\lambda x:\sigma.t$
by induction on the structure of the term $t$, as follows:

$\displaystyle\lambda x:\sigma.x$ $\displaystyle:\equiv$
$\displaystyle\mathsf{s}\,\mathsf{k}\,\mathsf{k},$ $\displaystyle\lambda
x:\sigma.y$ $\displaystyle:\equiv$ $\displaystyle\mathsf{k}\,y\quad\mbox{if
$y$ is a variable distinct from $x$},$ $\displaystyle\lambda x:\sigma.{\bf c}$
$\displaystyle:\equiv$ $\displaystyle\mathsf{k}\,{\bf c}\quad\mbox{if ${\bf
c}$ is one of the combinators from Table \ref{combinators}},$
$\displaystyle\lambda x:\sigma.st$ $\displaystyle:\equiv$
$\displaystyle\mathsf{s}\,(\lambda x:\sigma.s)\,(\lambda x:\sigma.t).$

∎

On top of this neutral theory we build a axiomatic theory of extensionality
and extensional equality, which we will denote by ${\textsf{H-HA}}^{\omega}$.
To formulate this hybrid version of arithmetic, we extend the language of
${\textsf{HA}}^{\omega}$ with a new unary predicate ${\textsf{ext}}_{\sigma}$
and a new binary predicate $=_{\sigma}$ for each finite type $\sigma$. This
means that if $s$ and $t$ are terms of type $\sigma$, then we have new atomic
formulas ${\textsf{ext}}_{\sigma}(t)$ for “$t$ is extensional” and
$s=_{\sigma}t$ for “$s$ and $t$ are extensionally equal”, where we will often
drop the type symbol $\sigma$. We will use the following abbreviations:

$\displaystyle\forall^{{\textsf{ext}}{}}\\!x:\sigma.\varphi$
$\displaystyle:\equiv$ $\displaystyle\forall
x:\sigma.(\,{\textsf{ext}}_{\sigma}(x)\to\varphi\,)$
$\displaystyle\exists^{{\textsf{ext}}{}}\\!x:\sigma.\varphi$
$\displaystyle:\equiv$ $\displaystyle\exists
x:\sigma.(\,{\textsf{ext}}_{\sigma}(x)\land\varphi\,)$

######  Definition 2.3.

The system ${\textsf{H-HA}}^{\omega}$ is theory which is formulated in this
extended language and which contains, besides the axiom of
${\textsf{HA}}^{\omega}$ previously mentioned, the following axioms for all
types $\sigma,\tau$:

$\displaystyle x=_{0}y\leftrightarrow x\equiv_{0}y,\quad\forall
x:0.\,{\textsf{ext}}_{0}(x),$ $\displaystyle
x=_{\sigma\times\tau}y\leftrightarrow\mathsf{fst}\,x=_{\sigma}\mathsf{fst}\,y\land\mathsf{snd}\,x=_{\tau}\mathsf{snd}\,y,\quad{\textsf{ext}}_{\sigma\times\tau}(x)\leftrightarrow{\textsf{ext}}_{\sigma}(\mathsf{fst}\,x)\land{\textsf{ext}}_{\tau}(\mathsf{snd}\,x)$
$\displaystyle
f=_{\sigma\to\tau}g\leftrightarrow\forall^{{\textsf{ext}}{}}\\!x:\sigma.fx=_{\tau}gx,\quad{\textsf{ext}}_{\sigma\to\tau}(f)\to{\textsf{ext}}_{\sigma}(x)\to{\textsf{ext}}_{\tau}(fx)$
$\displaystyle
x\equiv_{\sigma}y\to{\textsf{ext}}_{\sigma}(x)\to{\textsf{ext}}_{\sigma}(y),\quad{\textsf{ext}}({\bf
c}),$

where $\bf c$ is any of the combinators from Table 1. In addition,
${\textsf{H-HA}}^{\omega}$ has the induction axiom for all formulas in the
extended language.

The system ${\textsf{HE-HA}}^{\omega}$ is the extension of
${\textsf{H-HA}}^{\omega}$ that we obtain by adding the following
_extensionality axiom_ :

$\displaystyle\mathsf{EXT}:\quad{\textsf{ext}}_{\sigma\to\tau}(f)\to{\textsf{ext}}_{\sigma}(x)\to{\textsf{ext}}_{\sigma}(y)\to
x=_{\sigma}y\to fx=_{\tau}fy.$

######  Remark 2.4.

Despite being very natural, we have decided not to include the axiom
$x=_{\sigma}y\to{\textsf{ext}}_{\sigma}(x)\to{\textsf{ext}}_{\sigma}(y)$.
While almost all results in this paper would still have gone through if we had
included this axiom, there is one crucial exception, which we will discuss in
Subsection 6.2 below.

######  Remark 2.5.

If we assume surjectivity of pairing (that is,
$\mathsf{pair}(\mathsf{fst}\,x)(\mathsf{snd}\,x)\equiv x$), then the axiom
${\textsf{ext}}_{\sigma\times\tau}(x)\leftrightarrow{\textsf{ext}}_{\sigma}(\mathsf{fst}\,x)\land{\textsf{ext}}_{\tau}(\mathsf{snd}\,x)$
is redundant. Indeed, the left-to-right direction follows from the fact that
$\mathsf{fst}$ and $\mathsf{snd}$ are extensional in combination with the
axiom saying that extensional functions send extensional input to extensional
output. The right-to-left direction follows from the same axiom in combination
with extensionality of $\mathsf{pair}$ and surjectivity of pairing.

######  Remark 2.6.

We will often consider extensional equality $=_{\sigma}$ as an abbreviation.
Indeed, by repeatedly replacing the left-hand side of the equivalences

$\displaystyle x=_{0}y$ $\displaystyle\leftrightarrow$ $\displaystyle
x\equiv_{0}y,$ $\displaystyle x=_{\sigma\times\tau}y$
$\displaystyle\leftrightarrow$
$\displaystyle\mathsf{fst}\,x=_{\sigma}\mathsf{fst}\,y\land\mathsf{snd}\,x=_{\tau}\mathsf{snd}\,y,$
$\displaystyle f=_{\sigma\to\tau}g$ $\displaystyle\leftrightarrow$
$\displaystyle\forall^{{\textsf{ext}}{}}\\!x:\sigma.fx=_{\tau}gx,$

with its right-hand side, we can rewrite any formula containing the symbol for
extensional equality into an equivalent one that no longer uses that symbol.

######  Lemma 2.7.

  1. (i)

${\textsf{H-HA}}^{\omega}\vdash x=_{\sigma}x$ and, more generally,
${\textsf{H-HA}}^{\omega}\vdash x\equiv y\to x=y$.

  2. (ii)

${\textsf{H-HA}}^{\omega}\vdash x=_{\sigma}y\to y=_{\sigma}x$

  3. (iii)

${\textsf{H-HA}}^{\omega}\vdash x=_{\sigma}y\to y=_{\sigma}z\to x=_{\sigma}z$

###### Proof.

All these statements are proven by induction on the type structure, using the
axioms mentioned in Remark 2.6 above. ∎

In ${\textsf{H-HA}}^{\omega}$ the $\eta$-axiom and surjectivity of pairing
hold with respect to extensional equality, in the following way.

######  Lemma 2.8.

${\textsf{H-HA}}^{\omega}\vdash\forall f:\alpha\to\beta.f=\lambda x:\alpha.fx$
and
${\textsf{H-HA}}^{\omega}\vdash\mathsf{pair}(\mathsf{fst}\,x)(\mathsf{snd}\,x)=x$.

######  Proposition 2.9.

If $t$ is a term of ${\textsf{H-HA}}^{\omega}$ of type $\sigma$ and the free
variables of the term $t$ are $x_{1},\ldots,x_{n}$ of types
$\sigma_{1},\ldots,\sigma_{n}$, respectively, then

${\textsf{H-HA}}^{\omega}\vdash{\textsf{ext}}_{\sigma_{1}}(x_{1})\to\ldots\to{\textsf{ext}}_{\sigma_{n}}(x_{n})\to{\textsf{ext}}_{\sigma}(t).$

In particular, we have
${\textsf{H-HA}}^{\omega}\vdash{\textsf{ext}}_{\sigma}(t)$ if $t$ is closed.

###### Proof.

By induction on the structure of the term $t$. ∎

######  Remark 2.10.

Our treatment of the ext-predicate might remind the reader of the
$E$-predicate from $E$-logic (see, for instance, [7, Section 2.2]), where it
is read as “existence” or as “being defined”. However, there are some striking
differences. First of all, we allow quantifiers and free variables to range
over non-extensional objects. In addition, we do not insist on “strictness”:
in particular, we do not require
$x=y\to{\textsf{ext}}(x)\land{\textsf{ext}}(y)$. Indeed, every object, even
the non-extensional ones, will be extensionally equal to itself (see Lemma
2.7(i)). In this respect the current paper differs from [2], where we did
insist on strictness, because that was what matched the categorical semantics
in that paper.

##  3\. A closer look at extensionality

In this section we will take a closer look at the extensionality axiom
$\mathsf{EXT}$ in ${\textsf{H-HA}}^{\omega}$, which says that for all finite
types $\sigma$ and $\tau$ we have:

$\mathsf{EXT}_{\sigma,\tau}:\quad{\textsf{ext}}_{\sigma\to\tau}(f)\to{\textsf{ext}}_{\sigma}(x)\to{\textsf{ext}}_{\sigma}(y)\to
x=y\to fx=fy.$

Our goal in this section is to show that if this axiom holds in
${\textsf{H-HA}}^{\omega}$ for types $\sigma$ and $\tau$ of the form
$\sigma^{\prime}\to 0$ and $\tau^{\prime}\to 0$, respectively, then it holds
for all types $\sigma$ and $\tau$.

The reason this is useful is that it allows us to reformulate the axiom
$\mathsf{EXT}$ in a way which no longer uses the notion of extensional
equality. Of course, we have seen in Remark 2.6 a general method for
eliminating extensional equality, but if the type $\sigma$ is very complicated
(for instance, if it contains many nested function types), the formula which
this produces for $x=_{\sigma}y$ may also be very complicated. However, the
formula $f=_{\tau\to 0}g$ is equivalent to
$\forall^{{\textsf{ext}}{}}\\!x:\tau.fx\equiv_{0}gx$, which is rather simple.
So it follows from the results in this section that in
${\textsf{H-HA}}^{\omega}$ the axiom $\mathsf{EXT}$ is equivalent to the
following principle:

$\displaystyle\mathsf{EXT}^{\prime}:\quad{\textsf{ext}}_{(\sigma\to
0)\to(\tau\to 0)}(f)\to{\textsf{ext}}_{\sigma\to
0}(x)\to{\textsf{ext}}_{\sigma\to 0}(y)\to$
$\displaystyle\forall^{{\textsf{ext}}{}}\\!u:\sigma.xu\equiv_{0}yu\to\forall^{{\textsf{ext}}{}}\\!v:\tau.fxv\equiv_{0}fyv.$

The point is that $\mathsf{EXT}^{\prime}$ is a simple reformulation of
$\mathsf{EXT}$ which no longer uses the notion of extensional equality.

For the transparent presentation of our result, we will work in
${\textsf{H-HA}}^{\omega}$ and use a tiny bit of category theory. We will
write $\mathcal{C}$ for the following category:

Objects:

The objects of $\mathcal{C}$ are the finite types.

Morphisms:

The morphisms $\alpha\to\beta$ in $\mathcal{C}$ are equivalence classes of
closed terms $t$ of type $\alpha\to\beta$; here we regard
$t,t^{\prime}:\alpha\to\beta$ as equivalent if ${\textsf{H-HA}}^{\omega}\vdash
t=t^{\prime}$ (which is equivalent to
${\textsf{H-HA}}^{\omega}\vdash\forall^{{\textsf{ext}}{}}\\!x:\alpha.tx=_{\beta}tx^{\prime}$).

Note that we always have ${\textsf{H-HA}}^{\omega}\vdash{\textsf{ext}}(t)$ for
any morphism $t$ in this category, by Proposition 2.9. The identities
$\alpha\to\alpha$ are given by $\lambda x:\alpha.x$, while the composition of
$s:\alpha\to\beta$ and $t:\beta\to\gamma$ is $\lambda x:\alpha.t(sx)$. The
axioms of a category are easily verified.

A morphism $t:\alpha\to\beta$ in this category will be called _strong_ if

${\textsf{H-HA}}^{\omega}\vdash{\textsf{ext}}_{\alpha}(x)\to{\textsf{ext}}_{\alpha}(y)\to
x=_{\alpha}y\to tx=_{\beta}ty$

(note that this independent of the choice of representative, and
$\mathsf{EXT}$ implies that every morphism is strong). Clearly, identities are
strong and the strong maps are closed under composition, so we obtain a
subcategory $\mathcal{S}$ of $\mathcal{C}$ having the same objects as
$\mathcal{C}$ and whose morphisms are the strong morphisms of $\mathcal{C}$.

Let us first investigate to which extent these categories are cartesian
closed.

######  Lemma 3.1.

The type $\alpha\times\beta$ is the categorical product of the types $\alpha$
and $\beta$ in both $\mathcal{C}$ and $\mathcal{S}$.

###### Proof.

The projection maps are $\mathsf{fst}:\alpha\times\beta\to\alpha$ and
$\mathsf{snd}:\alpha\times\beta\to\beta$, respectively. The axiom
$x=_{\sigma\times\tau}y\leftrightarrow\mathsf{fst}\,x=_{\sigma}\mathsf{fst}\,y\land\mathsf{snd}\,x=_{\tau}\mathsf{snd}\,y$
implies that both maps are strong.

If $s:\gamma\to\alpha$ and $t:\gamma\to\beta$ are morphisms in $\mathcal{C}$,
then so is

$(s,t):\equiv\lambda
x:\sigma.\mathsf{pair}(sx)(tx):\gamma\to\alpha\times\beta.$

We have $\mathsf{fst}\circ(s,t)=s$ and $\mathsf{snd}\circ(s,t)=t$ as morphisms
in $\mathcal{C}$.

It remains to show that $(s,t):\gamma\to\alpha\times\beta$ is the unique
morphism with these properties and that $(s,t)$ will be strong as soon as $s$
and $t$ are. However, all of this follows from the axiom
$x=_{\sigma\times\tau}y\leftrightarrow\mathsf{fst}\,x=_{\sigma}\mathsf{fst}\,y\land\mathsf{snd}\,x=_{\tau}\mathsf{snd}\,y$.
∎

######  Lemma 3.2.

The type $\alpha\to\beta$ is the categorical exponential of the types $\alpha$
and $\beta$ in $\mathcal{C}$ if we assume surjectivity of pairing; if we
assume $\mathsf{EXT}_{\alpha,\beta}$, then it is the exponential in
$\mathcal{S}$.

###### Proof.

We have a morphism ${\rm ev}:(\alpha\to\beta)\times\alpha\to\beta$ in
$\mathcal{C}$ given by

$\lambda x:(\alpha\to\beta)\times\alpha.(\mathsf{fst}\,x)(\mathsf{snd}\,x).$

If $h:\gamma\times\alpha\to\beta$ is a morphism in $\mathcal{C}$, then we
obtain a morphism $H:\gamma\to(\alpha\to\beta)$ in $\mathcal{C}$ by:

$\lambda x:\gamma.\lambda y:\alpha.h(\mathsf{pair}\,x\,y).$

If we assume surjectivity of pairing or if $h$ is strong, then we have ${\rm
ev}\circ(H\times 1_{\alpha})=h$. If $H^{\prime}$ has the same property, then

$Hxy\equiv{\rm ev}\circ(H\times
1)(\mathsf{pair}\,x\,y)=h(\mathsf{pair}\,x\,y)={\rm ev}\circ(H^{\prime}\times
1)(\mathsf{pair}\,x\,y)=H^{\prime}xy$

for any extensional $x:\gamma$ and extensional $y:\alpha$; hence
$H=H^{\prime}$.

It remains to show that ${\rm ev}$ is strong and that $H$ will be strong as
soon as $h$ is. The fact that ${\rm ev}$ is strong follows from the axiom of
extensionality $\mathsf{EXT}$ for the types $\alpha$ and $\beta$, as in Lemma
4.2.

Finally, suppose that $h$ is strong and $x,x^{\prime}:\gamma$ are extensional
and satisfy $x=x^{\prime}$. To show that $Hx=Hx^{\prime}$, we let $y:\alpha$
be an arbitrary extensional element and derive that $Hxy=Hx^{\prime}y$. Note
that $\mathsf{pair}\,x\,y=\mathsf{pair}\,x\,y^{\prime}$ with
${\textsf{ext}}(\mathsf{pair}\,x\,y)={\textsf{ext}}(\mathsf{pair}\,x\,y^{\prime})$.
Because $h$ is strong, this implies that

$Hxy=h(\mathsf{pair}\,x\,y)=h(\mathsf{pair}\,x^{\prime}\,y)=Hx^{\prime}y;$

we conclude that $H$ is strong as well. ∎

The following technical definition is our most important tool in this section.

######  Definition 3.3.

Let $\alpha$ and $\beta$ be finite types. We will say that $\alpha$ is a
_strong retract_ of $\beta$ if there are strong maps $i:\alpha\to\beta$ and
$r:\beta\to\alpha$ such that $r\circ i=1_{\alpha}$.

Our next goal is to show that any type $\sigma$ is a strong retract of one of
the form $\tau\to 0$. The proof relies on the following lemma.

######  Lemma 3.4.

  1. (i)

If $\alpha$ is a strong retract of $\beta$ and $\beta$ is a strong retract of
$\gamma$, then $\alpha$ is a strong retract of $\gamma$.

  2. (ii)

If $\alpha_{0}$ is a strong retract of $\beta_{0}$ and $\alpha_{1}$ of
$\beta_{1}$, then $\alpha_{0}\times\alpha_{1}$ is a strong retract of
$\beta_{0}\times\beta_{1}$.

  3. (iii)

If $\alpha$ is a strong retract of $\beta$, then $\gamma\to\alpha$ is a strong
retract of $\gamma\to\beta$.

  4. (iv)

If $\alpha$ is strongly isomorphic to $\beta$, then $\gamma\to\alpha$ is
strongly isomorphic to $\gamma\to\beta$.

  5. (v)

$(\alpha\to\beta)\times(\gamma\to\delta)$ is a strong retract of
$\alpha\times\beta\to\gamma\times\delta$.

  6. (vi)

$\alpha\to\beta\to\gamma$ is a strong retract of $\alpha\times\beta\to\gamma$.

###### Proof.

Points (i) and (ii) are simple exercises in category theory, with (ii) using
Lemma 3.1.

(iii): If $i:\alpha\to\beta$ and $r:\beta\to\alpha$ are strong maps such that
$r\circ i=1$, then

$i^{\prime}:\equiv\lambda x:\gamma\to\alpha.\lambda y:\gamma.i(xy)$

and

$r^{\prime}:\equiv\lambda x:\gamma\to\beta.\lambda y:\gamma.r(xy)$

define strong maps $i^{\prime}:(\gamma\to\alpha)\to(\gamma\to\beta)$ and
$r^{\prime}:(\gamma\to\beta)\to(\gamma\to\alpha)$ such that $r^{\prime}\circ
i^{\prime}=1$. Indeed, if we have extensional $x,x^{\prime}:\gamma$ such that
$x=x^{\prime}$, then $i^{\prime}x=i^{\prime}x^{\prime}$ will follow as soon as
we have $i^{\prime}xy=i^{\prime}x^{\prime}y$ for any extensional $y:\gamma$.
We have $xy=x^{\prime}y$ because $x=x^{\prime}$ and $y$ is extensional, and

$i^{\prime}xy\equiv i(xy)=i(x^{\prime}y)\equiv i^{\prime}x^{\prime}y,$

because $i$ is strong. So $i^{\prime}$ is strong and a similar argument shows
that $r^{\prime}$ is strong as well.

To show $r^{\prime}\circ i^{\prime}=1$, we pick extensional
$x:\gamma\to\alpha$ and $y:\gamma$ and show that $(r^{\prime}\circ
i^{\prime})xy=xy$. But we have

$(r^{\prime}\circ i^{\prime})xy\equiv r((i^{\prime}x)y)\equiv r(i(xy))=xy,$

using that $xy$ is extensional and $r\circ i=1$.

(iv): By $\alpha$ and $\beta$ being strongly isomorphic, we mean that they are
isomorphic in the category $\mathcal{S}$. If in the situation as in (iii)
above, we also have $i\circ r=1$, then we must have $i^{\prime}\circ
r^{\prime}=1$ as well, by symmetry.

(v): In the forward directon there is:

$i:\equiv\lambda h:(\alpha\to\beta)\times(\gamma\to\delta).\lambda
y:\alpha\times\beta.\mathsf{pair}((\mathsf{fst}\,h)(\mathsf{fst}\,y))((\mathsf{snd}\,h)(\mathsf{snd}\,y)),$

while in the backward direction there is:

$r:\equiv\lambda
k:\alpha\times\beta\to\gamma\times\delta.\mathsf{pair}(\lambda
x:\alpha.\mathsf{fst}(k(\mathsf{pair}\,x\,0)))(\lambda
z:\beta.\mathsf{snd}(k(\mathsf{pair}\,0\,z)),$

where $0$ is a closed term as in Lemma 2.1. By arguments similar to those that
we have seen before, both operations can be shown to be strong, while $r\circ
i=1$.

(vi): In the forward directon there is:

$i:\equiv\lambda f:\alpha\to\beta\to\gamma.\lambda
x:\alpha\times\beta.f(\mathsf{fst}\,x)(\mathsf{snd}\,x),$

while in the backward direction there is:

$r:\equiv\lambda g:\alpha\times\beta\to\gamma.\lambda x:\alpha.\lambda
y:\beta.g(\mathsf{pair}\,x\,y).$

Both operations can be shown to be strong, while $r\circ i=1$. (Note that if
we had surjectivity of pairing, we could show $i\circ r=1$ as well.) ∎

######  Proposition 3.5.

Every type $\sigma$ is a strong retract of one of the form $\tau\to 0$.

###### Proof.

We prove this statement by induction on the structure of $\sigma$, using the
properties of strong retracts established in the previous lemma. In addition,
we use that we can code pairs of natural numbers as a single natural number:
in particular, we have a strong isomorphism $0\times 0\to 0$.

For type 0, we have maps $i:0\to(0\to 0)$ and $r:(0\to 0)\to 0$ given by
$\lambda x:0.\lambda y:0.x$ and $\lambda f:0\to 0.f0$, respectively. Clearly,
both are strong morphisms and $r\circ i=1$.

If $\sigma_{0}$ is a strong retract of $\tau_{0}\to 0$ and $\sigma_{1}$ of
$\tau_{1}\to 0$, then $\sigma_{0}\times\sigma_{1}$ is a strong retract of
$(\tau_{0}\to 0)\times(\tau_{1}\to 0)$, which in turn is a strong retract of
$\tau_{0}\times\tau_{1}\to 0\times 0$, which is strongly isomorphic to
$\tau_{0}\times\tau_{1}\to 0$.

Finally, if $\sigma$ is a strong retract of $\tau\to 0$, then $\rho\to\sigma$
is a strong retract of $\rho\to(\tau\to 0)$, which is a strong retract of
$(\rho\times\tau)\to 0$. ∎

######  Proposition 3.6.

In ${\textsf{H-HA}}^{\omega}$, if we have $\mathsf{EXT}_{\tau_{0}\to
0,\tau_{1}\to 0}$ for all finite types $\tau_{0},\tau_{1}$, then we have
$\mathsf{EXT}_{\sigma_{0},\sigma_{1}}$ for all finite types
$\sigma_{0},\sigma_{1}$.

###### Proof.

We reason in ${\textsf{H-HA}}^{\omega}$ and assume we are given a map
$f:\sigma_{0}\to\sigma_{1}$. We have to show that $f$ is strong under the
assumption that $\mathsf{EXT}_{\tau_{0}\to 0,\tau_{1}\to 0}$ holds for all
finite types $\tau_{0},\tau_{1}$. Using the previous proposition, we can
exhibit $\sigma_{k}$ as a strong retract of $\tau_{k}$ via strong maps
$i_{k}:\sigma_{k}\to(\tau_{k}\to 0)$ and $r_{k}:(\tau_{k}\to 0)\to\sigma_{k}$
such that $r_{k}\circ i_{k}=1$ for $k\in\\{0,1\\}$. Let us write $g:\equiv
i_{1}\circ f\circ r_{0}$, as in the diagram below.

${\sigma_{0}}$${\sigma_{1}}$${\tau_{0}\to 0}$${\tau_{1}\to
0}$$\scriptstyle{i_{0}}$$\scriptstyle{f}$$\scriptstyle{i_{1}}$$\scriptstyle{g}$$\scriptstyle{r_{0}}$$\scriptstyle{r_{1}}$

By assumption, $g$ is strong. Because strong maps are closed under composition
and $r_{1}\circ g\circ i_{0}=f$, the map $f$ is strong as well. ∎

######  Corollary 3.7.

Over ${\textsf{H-HA}}^{\omega}$ the extensionality axiom $\mathsf{EXT}$ is
equivalent to

$\displaystyle\mathsf{EXT}^{\prime}:\quad{\textsf{ext}}_{(\sigma\to
0)\to(\tau\to 0)}(f)\to{\textsf{ext}}_{\sigma\to
0}(x)\to{\textsf{ext}}_{\sigma\to 0}(y)\to$
$\displaystyle\forall^{{\textsf{ext}}{}}\\!u:\sigma.xu\equiv_{0}yu\to\forall^{{\textsf{ext}}{}}\\!v:\tau.fxv\equiv_{0}fyv.$

The previous corollary is important for us because it implies that the
following converse extensionality principle $\mathsf{CEXT}$ implies
$\mathsf{EXT}$.

$\displaystyle\mathsf{CEXT}:\quad\exists
Z.\,\forall^{\textsf{ext}}f:(\sigma\to 0)\to(\tau\to
0).\,\forall^{\textsf{ext}}x,y:\sigma\to 0.\,\forall^{\textsf{ext}}v:\tau.$
$\displaystyle\big{(}\,fxv\not\equiv_{0}fyv\to{\textsf{ext}}(Zfxyv)\land
x(Zfxyv))\not\equiv_{0}y(Zfxyv)\,\big{)}.$

Note that this is indeed a converse extensionality principle as in (2) from
the introduction. As discussed there as well, it will be crucial that we do
not demand that the functional $Z$ in $\mathsf{CEXT}$ witnessing this strong
form of extensionality is extensional itself.

######  Corollary 3.8.

${\textsf{H-HA}}^{\omega}\vdash\mathsf{CEXT}\to\mathsf{EXT}^{\prime}$ and
therefore ${\textsf{H-HA}}^{\omega}\vdash\mathsf{CEXT}\to\mathsf{EXT}$.

##  4\. Hybrid arithmetic as an intermediate system

In this section we will show that there are natural interpretations
${\textsf{E-HA}}^{\omega}\to{\textsf{HE-HA}}^{\omega}$ and ${\textsf{HE-
HA}}^{\omega}\to{\textsf{HA}}^{\omega}$, respectively. Let us start with the
former.

######  Theorem 4.1.

Let $\varphi$ be a formula in the language of ${\textsf{E-HA}}^{\omega}$ with
free variables $x_{1},\ldots,x_{n}$ of types $\sigma_{1},\ldots,\sigma_{n}$,
respectively, and let $\varphi^{*}$ be the formula in ${\textsf{HE-
HA}}^{\omega}$ obtained from $\varphi$ by replacing $\equiv$ with $=$,
$\forall x$ with $\forall^{{\textsf{ext}}{}}\\!x$ and $\exists x$ with
$\exists^{{\textsf{ext}}{}}\\!x$. Then

${\textsf{E-HA}}^{\omega}\vdash\varphi\quad\mbox{if and ony
if}\quad{\textsf{HE-
HA}}^{\omega}\vdash{\textsf{ext}}_{\sigma_{1}}(x_{1})\to\ldots\to{\textsf{ext}}_{\sigma_{n}}(x_{n})\to\varphi^{*}.$

###### Proof.

The direction from left to right is shown by induction on the derivation of
${\textsf{E-HA}}^{\omega}\vdash\varphi$, using Proposition 2.9 and the lemma
below. The direction from right to left follows from the fact that there is an
interpretation of ${\textsf{HE-HA}}^{\omega}$ into ${\textsf{E-HA}}^{\omega}$
obtained by declaring every element to be extensional and interpreting
extensional equality = as equality $\equiv$. ∎

######  Lemma 4.2.

${\textsf{HE-
HA}}^{\omega}\vdash\forall^{{\textsf{ext}}{}}\\!f,g\,\forall^{{\textsf{ext}}{}}\\!x,y\,(x=y\land
f=g\to fx=gy)$.

###### Proof.

The extensionality axiom $\mathsf{EXT}$ applied to $f$ gives us that $fx=fy$.
From $f=g$ we obtain $fy=gy$ and therefore $fx=gy$. ∎

######  Theorem 4.3.

There is a proof-theoretic interpretation ${\textsf{HE-
HA}}^{\omega}\to{\textsf{HA}}^{\omega}$ which is the identity on
${\textsf{HA}}^{\omega}$-formulas. Therefore ${\textsf{HE-HA}}^{\omega}$ is a
conservative extension of ${\textsf{HA}}^{\omega}$.

###### Proof.

The idea behind the interpretation of ${\textsf{HE-HA}}^{\omega}$ into
${\textsf{HA}}^{\omega}$ is to regard $=_{\sigma}$ and
${\textsf{ext}}_{\sigma}$ as abbreviations defined by induction on $\sigma$,
as follows.

$\displaystyle{\textsf{ext}}_{0}(x)$ $\displaystyle:\equiv$
$\displaystyle\top$ $\displaystyle x=_{0}y$ $\displaystyle:\equiv$
$\displaystyle x\equiv_{0}y$
$\displaystyle{\textsf{ext}}_{\sigma\times\tau}(x)$ $\displaystyle:\equiv$
$\displaystyle{\textsf{ext}}_{\sigma}(\mathsf{fst}\,x)\land{\textsf{ext}}_{\tau}(\mathsf{snd}\,x)$
$\displaystyle x=_{\sigma\times\tau}y$ $\displaystyle:\equiv$
$\displaystyle\mathsf{fst}\,x=_{\sigma}\mathsf{fst}\,y\land\mathsf{snd}\,x=_{\tau}\mathsf{snd}\,y$
$\displaystyle{\textsf{ext}}_{\sigma\to\tau}(f)$ $\displaystyle:\equiv$
$\displaystyle\forall
x:\sigma\,\big{(}\,{\textsf{ext}}_{\sigma}(x)\to{\textsf{ext}}_{\tau}(fx)\,\big{)}\land$
$\displaystyle\forall
x,y:\sigma\,\big{(}\,x=_{\sigma}y\to{\textsf{ext}}_{\sigma}(x)\to{\textsf{ext}}_{\sigma}(y)\to
fx=_{\tau}fy\,\big{)}$ $\displaystyle f=_{\sigma\to\tau}g$
$\displaystyle:\equiv$ $\displaystyle\forall
x:\sigma\,\big{(}\,{\textsf{ext}}_{\sigma}(x)\to fx=_{\tau}gx\,\big{)}$

To verify the soundness of this interpretation, we only need to check that it
soundly interprets the axioms of ${\textsf{HE-HA}}^{\omega}$. This is trivial
for most of them, the axioms of the form ${\textsf{ext}}({\bf c})$ for the
various combinators ${\bf c}$ being the exception; we will only discuss this
for the $\mathsf{s}$-combinator, as the argument for the other combinators is
similar.

We start by showing that ${\bf s}xy$ will be extensional whenever $x$ and $y$
are. This involves two things: showing that ${\bf s}xyz$ is extensional
whenever $z$ is, and showing that ${\bf s}xyz={\bf s}xyz^{\prime}$ whenever
$z,z^{\prime}$ are extensional and $z=z^{\prime}$.

The former follows because $xy(xz)$ will be extensional as soon as $x,y,z$ are
and ${\bf s}xyz\equiv xy(xz)$. Similarly, if $z=z^{\prime}$ and $z$ and
$z^{\prime}$ are extensional, then ${\bf s}xyz\equiv
xy(xz)=xy(xz^{\prime})\equiv{\bf s}xyz^{\prime}$, because $x$ and $xy$ are
extensional.

The next step is to show that ${\bf s}x$ is extensional whenever $x$ is. For
that we need to show that ${\bf s}xy={\bf s}xy^{\prime}$ whenever $y$ and
$y^{\prime}$ are extensional and $y=y^{\prime}$; in other words, we should
show that ${\bf s}xyz={\bf s}xy^{\prime}z$ whenever $z$ extensional. However,
we have $xy=xy^{\prime}$, because $x$ is extensional, and therefore ${\bf
s}xyz\equiv xy(xz)=xy^{\prime}(xz)={\bf s}xy^{\prime}z$, because $xz$ is
extensional.

It remains to show that ${\bf s}x={\bf s}x^{\prime}$ whenever $x=x^{\prime}$
and $x$ and $x^{\prime}$ are extensional, which can be done in a way similar
to what we have seen before. ∎

######  Remark 4.4.

Note that this translation also validates
$x=y\to{\textsf{ext}}(x)\to{\textsf{ext}}(y)$, which we can show by induction
on the type $\sigma$.

######  Remark 4.5.

The composed translation ${\textsf{E-HA}}^{\omega}\to{\textsf{HE-
HA}}^{\omega}\to{\textsf{HA}}^{\omega}$ is nothing but Gandy and Luckhardt’s
elimination of extensionality. So what we have done is factor this translation
as a composition of two translations with ${\textsf{HE-HA}}^{\omega}$ as the
intermediate system.

##  5\. The $\alpha$-translation

The interpretation of ${\textsf{HE-HA}}^{\omega}$ into
${\textsf{HA}}^{\omega}$ that we presented in the previous section is in many
ways the canonical one. In this section, which is the heart of this paper, we
will present an alternative: the $\alpha$-translation, inspired by Brouwer’s
notion of apartness. The main benefit of this translation is that it allows us
to eliminate the strong extensionality principle $\mathsf{CEXT}$, that we
introduced in Section 3.

Table 2. Auxiliary definitions for the $\alpha$-translation $\displaystyle
0^{+}$ $\displaystyle:\equiv$ $\displaystyle 0$ $\displaystyle 0^{-}$
$\displaystyle:\equiv$ $\displaystyle 0$ $\displaystyle{\rm dom}_{0}$
$\displaystyle:\equiv$ $\displaystyle\top$ $\displaystyle{\rm app}_{0}$
$\displaystyle:\equiv$ $\displaystyle x\not\equiv_{0}y$
$\displaystyle(\sigma\times\tau)^{+}$ $\displaystyle:\equiv$
$\displaystyle\sigma^{+}\times\tau^{+}$ $\displaystyle(\sigma\times\tau)^{-}$
$\displaystyle:\equiv$ $\displaystyle(\sigma^{-}\times\tau^{-})\times 0$
$\displaystyle{\rm dom}_{\sigma\times\tau}$ $\displaystyle:\equiv$
$\displaystyle{\rm dom}_{\sigma}(\mathsf{fst}\,x)\land{\rm
dom}_{\tau}(\mathsf{snd}\,x)$ $\displaystyle{\rm app}_{\sigma\times\tau}$
$\displaystyle:\equiv$ $\displaystyle\big{(}\,\mathsf{snd}\,z\equiv 0\to{\rm
app}_{\sigma}(\mathsf{fst}\,x,\mathsf{fst}\,y,\mathsf{fst}(\mathsf{fst}\,z))\,\big{)}\land$
$\displaystyle\big{(}\,\,\mathsf{snd}\,z\not\equiv 0\to{\rm
app}_{\sigma}(\mathsf{snd}\,x,\mathsf{snd}\,y,\mathsf{snd}(\,\mathsf{fst}\,z))\,\big{)}$
$\displaystyle(\sigma\to\tau)^{+}$ $\displaystyle:\equiv$
$\displaystyle(\sigma^{+}\to\tau^{+})\times(\sigma^{+}\to\sigma^{+}\to\tau^{-}\to\sigma^{-})$
$\displaystyle(\sigma\to\tau)^{-}$ $\displaystyle:\equiv$
$\displaystyle\sigma^{+}\times\tau^{-}$ $\displaystyle{\rm
dom}_{\sigma\to\tau}$ $\displaystyle:\equiv$ $\displaystyle\forall
u:{\sigma^{+}}(\,{\rm dom}_{\sigma}(u)\to{\rm
dom}_{\tau}((\mathsf{fst}\,x)u)\,)\land\forall
u:{\sigma^{+}},v:{\sigma^{+}},w:{\tau^{-}}\,$ $\displaystyle\big{(}\,{\rm
dom}_{\sigma}(u)\to{\rm dom}_{\tau}(v)\to{\rm
app}_{\tau}((\mathsf{fst}\,x)(u),(\mathsf{fst}\,x)(v),w)\to$
$\displaystyle{\rm app}_{\sigma}(u,v,(\mathsf{snd}\,x)uvw)\,\big{)}$
$\displaystyle{\rm app}_{\sigma\to\tau}$ $\displaystyle:\equiv$
$\displaystyle{\rm dom}_{\sigma}(\mathsf{fst}\,z)\land{\rm
app}_{\tau}((\mathsf{fst}\,x)(\mathsf{fst}\,z),(\mathsf{fst}\,y)(\mathsf{fst}\,z),\mathsf{snd}\,z)$

As a first step towards defining the $\alpha$-translation, we define for each
finite type $\sigma$ two finite types $\sigma^{+}$ and $\sigma^{-}$, as well
as two formulas ${\rm dom}_{\sigma}$ and ${\rm app}_{\sigma}$ in the language
of ${\textsf{HA}}^{\omega}$. The formula ${\rm dom}_{\sigma}$ will have one
free variable $x$ of type $\sigma^{+}$ and ${\rm app}_{\sigma}$ has free
variables $x,y,z$ of types $\sigma^{+},\sigma^{+}$ and $\sigma^{-}$,
respectively. Borrowing from the categorical analysis of modified
realizability the distinction between potential and actual realizers, we can
give the following intuition for these definitions:

  1. (1)

The elements of type $\sigma^{+}$ stand for elements of type $\sigma$ together
with an argument (potential realizer) for their extensionality.

  2. (2)

The predicate ${\rm dom}_{\sigma}$ holds if that argument is successful (if
the potential realizer is an actual realizer).

  3. (3)

Elements of type $\sigma^{-}$ are arguments (potential realizers) for the
statement that two elements of type $\sigma$ are apart from each other.

  4. (4)

The predicate ${\rm app}_{\sigma}$ holds if that argument is successful (that
potential realizer is an actual realizer).

  5. (5)

Crucially, potential realizers always exist, because for any type $\sigma$
there is a closed term $0:\sigma$. Of course, these need not be actual
realizers.

The clauses can be found in Table 2. Note that if $s:(\sigma\to\tau)^{+}$ and
$t:\sigma^{+}$, then $(\mathsf{fst}\,s)t:\tau^{+}$. In what follows we will
write $s*t$ for $(\mathsf{fst}\,s)t$, so that $s*t:\tau^{+}$.

######  Lemma 5.1.

The following statements are provable in ${\textsf{HA}}^{\omega}$ for each
type $\sigma$:

  1. (1)

There is no $z$ such that ${\rm app}_{\sigma}(x,x,z)$.

  2. (2)

There is a functional $s:\sigma^{+}\to\sigma^{+}\to\sigma^{-}\to\sigma^{-}$,
such that if ${\rm app}_{\sigma}(x,y,z)$, then ${\rm app}_{\sigma}(y,x,sxyz)$.

  3. (3)

There is a functional
$t:\sigma^{+}\to\sigma^{+}\to\sigma^{+}\to\sigma^{-}\to\sigma^{-}\times 0$,
which given $x,y,z:\sigma^{+}$ and $u:\sigma^{-}$ such that ${\rm
app}_{\sigma}(x,y,u)$, computes an element $t=txyzu$ such that ${\rm
app}_{\sigma}(x,z,\mathsf{fst}\,t)$ whenever $\mathsf{snd}\,t\equiv_{0}0$ and
${\rm app}_{\sigma}(y,z,\mathsf{snd}\,t)$ whenever
$\mathsf{snd}\,t\not\equiv_{0}0$.

######  Proposition 5.2.

For each combinator ${\bf c}:\sigma$ as in Table 1 there is a combinator ${\bf
c}^{\alpha}:\sigma^{+}$ with ${\textsf{HA}}^{\omega}\vdash{\rm dom}({\bf
c}^{\alpha})$, which, provably in ${\textsf{HA}}^{\omega}$, satisfies the
defining equation for that combinator with respect to $*$. For instance, for
each pair of finite types $\sigma,\tau$ there is a combinator ${\bf
k}^{\alpha}:(\sigma\to\tau\to\sigma)^{+}$ such that
${\textsf{HA}}^{\omega}\vdash{\rm dom}({\bf k}^{\alpha})$ and
${\textsf{HA}}^{\omega}\vdash{\bf k}^{\alpha}*x*y\equiv x$.

###### Proof.

Let us treat the combinators $\mathsf{fst},\mathsf{snd},\mathsf{pair}$ first.
We need a combinator

$\mathsf{fst}^{\alpha}:(\sigma\times\tau\to\tau)^{+}=(\sigma^{+}\times\tau^{+}\to\sigma^{+})\times(\sigma\times\tau\to\sigma\times\tau\to\sigma^{-}\to(\sigma^{-}\times\tau^{-})\times
0).$

We put $\mathsf{fst}^{\alpha}:\equiv\mathsf{pair}\,\mathsf{fst}\,(\lambda
x,x^{\prime}:\sigma\times\tau.\lambda
e:\sigma^{-}.\mathsf{pair}(\mathsf{pair}\,e\,0)\,0))$. Note what the second
component does: given $x,x^{\prime}:\sigma\times\tau$ and a potential realizer
$e$ for the apartness of $\mathsf{fst}^{\alpha}*x$ and
$\mathsf{fst}^{\alpha}*x^{\prime}$, it computes a potential realizer of the
apartness of $x$ and $x^{\prime}$; this is done in such a way that if $e$ is
an actual realizer for the apartness of $\mathsf{fst}^{\alpha}*x$ and
$\mathsf{fst}^{\alpha}*x^{\prime}$, then the potential realizer thus obtained
is an actual realizer for the apartness of $x$ and $y$. In a similar fashion,
we put $\mathsf{snd}^{\alpha}:\equiv\mathsf{pair}\,\mathsf{snd}\,(\lambda
x,x^{\prime}:\sigma\times\tau.\lambda
e:\tau^{-}.\mathsf{pair}(\mathsf{pair}\,0\,e)\,(S0))$.

Next, we need a combinator $\mathsf{pair}^{\alpha}$ having type
$(\sigma\to\tau\to\sigma\times\tau)^{+}$, which is

$\displaystyle\big{(}\,\sigma^{+}\to(\tau^{+}\to\sigma^{+}\times\tau^{+})\times(\tau^{+}\to\tau^{+}\to(\sigma^{-}\times\tau^{-})\times
0\to\tau^{-})\,\big{)}\times$
$\displaystyle\big{(}\,\sigma^{+}\to\sigma^{+}\to(\tau^{+}\times((\sigma^{-}\times\tau^{-})\times
0))\to\sigma^{-}\,\big{)}$

This really consists of three parts: from $x:\sigma^{+},y:\tau^{+}$ we should
compute an element of type $(\sigma\times\tau)^{+}=\sigma^{+}\times\tau^{+}$,
for which we take $\mathsf{pair}\,x\,y$. Secondly, for any
$x:\sigma^{+},y,y^{\prime}:\tau^{+}$ and a potential realizer $e$ of the
apartness of $\mathsf{pair}\,x\,y$ and $\mathsf{pair}\,x\,y^{\prime}$ we
compute a potential realizer of the apartness of $y$ and $y^{\prime}$. For
that we choose $\mathsf{snd}\,(\mathsf{fst}\,e)$. This has the additional
property that if $e$ was an actual realizer, then so is
$\mathsf{snd}\,(\mathsf{fst}\,e)$; to see this, note that there is never an
actual realizer for the apartness of $x$ with itself, by item (1) from Lemma
5.1. Thirdly, for any $x,x^{\prime}:\sigma^{+},y:\tau^{+}$ and potential
realizer $e$ of the apartness of $\mathsf{pair}\,x\,y$ and
$\mathsf{pair}\,x^{\prime}\,y$ we need to compute a potential realizer of the
apartness of $x$ and $x^{\prime}$: for that we take
$\mathsf{fst}(\,\mathsf{fst}\,e)$. Again, this will be actual realizer
whenever $e$ is.

We see here the pattern that repeats itself for the other combinators: in each
case, we define a certain function $f(x_{1},\ldots,x_{n})$. In addition, we
should show that if we have a value $f(x_{1},\ldots,x_{n})$ and we change the
input on one entry, say we change $x_{i}$ to $x_{i}^{\prime}$, then from the
inputs and a potential realizer of the apartness of the outputs
$f(x_{1},\ldots,x_{n})$ and
$f(x_{1},\ldots,x_{i-1},x_{i}^{\prime},x_{i+1},\ldots x_{n})$, we are able to
compute a potential realizer of the apartness of $x_{i}$ and $x_{i}^{\prime}$;
this needs to be done in such a way that if the potential realizer of the
apartness of the outputs was an actual realizer, then so is the potential
realizer of the apartness of $x_{i}$ and $x_{i}^{\prime}$ that we compute.

To define the combinator ${\bf k}^{\alpha}$ we therefore need to supply three
functions. First of all, given $x:\sigma^{+}$ and $y:\tau^{+}$, we output
$f(x,y):\equiv x$. Secondly, given $x,x^{\prime},y$ and a potential realizer
$e$ of the apartness of $f(x,y)=x$ and $f(x^{\prime},y)=x^{\prime}$, we output
$e$ as a potential realizer of the apartness of $x$ and $x^{\prime}$. Thirdly,
given $x,y,y^{\prime}$ and a potential realizer of the apartness of $f(x,y)=x$
and $f(x,y^{\prime})=x$, we output $0$ as a potential realizer of the
apartness of $y$ and $y^{\prime}$. (Note that $e$ will never be an actual
realizer, again by item (1) from Lemma 5.1.)

To define the combinator ${\bf s}^{\alpha}$, we need to supply four functions.

  1. (i)

Given $x:(\rho\to\sigma\to\tau)^{+}$, $y:(\rho\to\sigma)^{+}$ and
$z:\rho^{+}$, we have $f(x,y,z)=x*z*(y*z):\tau^{+}$.

  2. (ii)

If $e:\tau^{-}$ is a potential realizer of the apartness of $f(x,y,z)$ and
$f(x^{\prime},y,z)$, then
$\mathsf{pair}\,z\,(\mathsf{pair}\,(y*z)\,e):\rho^{+}\times(\sigma^{+}\times\tau^{-})$
is a potential realizer of the apartness of $x$ and $x^{\prime}$.

  3. (iii)

Suppose $e:\tau^{-}$ is a potential realizer of the apartness of $f(x,y,z)$
and $f(x,y^{\prime},z)$. Note that from $x$ we can extract a function
$a:\rho^{+}\to\sigma^{+}\to\sigma^{+}\to\tau^{-}\to\sigma^{-}$ such that if
$d$ is a potential realizer of the apartness of $x*u*v$ and $x*u*v^{\prime}$,
then $auvv^{\prime}d$ is a potential realizer of the apartness of $v$ and
$v^{\prime}$. Therefore $az(y*z)(y^{\prime}*z)$ is a potential realizer of the
apartness of $y*z$ and $y^{\prime}*z$, which implies that
$\mathsf{pair}\,z\,(az(y*z)(y^{\prime}*z))$ is a potential realizer of the
apartness of $y$ and $y^{\prime}$.

  4. (iv)

Suppose we are given a potential realizer of the apartness of $f(x,y,z)$ and
$f(x,y,z^{\prime})$. Let us first of all note that from elements
$f,f^{\prime}:(\sigma\to\tau)^{+}$ and $u,u^{\prime}:\sigma^{+}$ and a
potential realizer of the apartness of $f*u$ and $f^{\prime}*u^{\prime}$ we
can compute a potential realizer of the apartness of $f$ and $f^{\prime}$ or a
potential realizer of the apartness of $u$ and $u^{\prime}$; indeed, using
item (iii) from the previous lemma we can compute from a potential realizer of
the apartness of $f*u$ and $f^{\prime}*u^{\prime}$ a potential realizer of the
apartness of $f*u$ and $f^{\prime}*u$ or a potential realizer of the apartness
of $f^{\prime}*u$ and $f^{\prime}*u^{\prime}$. In the former case the pair
consisting of $u$ and that potential realizer is a potential realizer of the
apartness of $f$ and $f^{\prime}$; in the latter case we can use the second
component of $f^{\prime}$ to give us a potential realizer of the apartness of
$u$ and $u^{\prime}$. In the case at hand this means that we find either a
potential realizer of the apartness of $x*z$ and $x*z^{\prime}$ or a potential
realizer of the apartness of $y*z$ and $y*z^{\prime}$. In the first case we
use the second component of $x$ and in the second case the second component of
$y$ to give us a potential realizer of the apartness of $z$ and $z^{\prime}$.

For the arithmetical part, we need terms $0^{\alpha}:0^{+}=0$ as well as
$S^{\alpha}:(0\to 0)^{+}=(0\to 0)\to(0\to 0\to 0\to 0)$, for which we choose
$0^{\alpha}:\equiv 0$ and $S^{\alpha}:\equiv\mathsf{pair}\,S\,(\lambda
x,y,z:0.z)$. Finally, we need a term
$\mathsf{R}^{\alpha}:(\sigma\to(0\to\sigma\to\sigma)\to 0\to\sigma))^{+}$, for
which we need to supply four functions:

  1. (i)

Given $x:\sigma^{+}$, $y:(0\to\sigma\to\sigma)^{+}$ and $n:0$, we need an
element $f(x,y,n)$ of type $\sigma^{+}$, for which we choose
$f(x,y,n):\equiv\mathsf{R}\,x\,(\lambda m:0.\lambda z:\sigma^{+}.y*m*z)\,n$.

  2. (ii)

Next, suppose we are given a potential realizer of the apartness of $f(x,y,n)$
and $f(x^{\prime},y,n)$. If $n\equiv 0$, then this also a potential realizer
of teh apartness of $x$ and $x^{\prime}$. If $f\equiv Sm$, then we can use the
second component of $y$ to compute from this a potential realizer of the
apartness of $f(x,y,m)$ and $f(x^{\prime},y,m)$. This procedure we repeat
until we are in the first case.

  3. (iii)

Next, suppose we are given a potential realizer of the apartness of $f(x,y,n)$
and $f(x,y^{\prime},n)$. If $n\equiv 0$, then this is a potential realizer of
the apartness of $x$ with itself; such an element is never an actual realizer,
so when we can simply choose $0$ as the potential realizer of the apartness of
$y$ and $y^{\prime}$. If $n\equiv Sm$, then we are given a potential realizer
of the apartness of $y*m*f(x,y,m)$ and $y^{\prime}*m*f(x,y^{\prime},m)$. Using
the remark from (iv) above, we obtain from this (1) a potential realizer of
the apartness of $y$ and $y^{\prime}$, or (2) a potential realizer of the
apartness of $m$ with itself, or (3) a potential realizer of the apartness of
$f(x,y,m)$ and $f(x,y^{\prime},m)$. In the first case we are finished; in the
second case we output 0 as a potential realizer of the apartness of $y$ and
$y^{\prime}$; in the third case, we repeat the algorithm for $m$.

  4. (iv)

Finally, suppose we are given a potential realizer of the apartness of
$f(x,y,n)$ and $f(x,y,n^{\prime})$. We need a potential realizer of the
apartness of $n$ and $n^{\prime}$, for which we simply choose 0.

The remaining verifications are not too difficult and left to the reader. ∎

In what follows we assume that we have fixed the terms ${\bf c}^{\alpha}$ as
in the proof of the previous proposition. We wish to extend this to a
translation $t^{\alpha}$ for any term $t$. In order to do so, we will assume
in addition that we have assigned to each variable $x$ of type $\sigma$ a
variable $x^{\alpha}$ of type $\sigma^{+}$ in such a way that for any pair of
distinct variables $x,y$ of type $\sigma$ the variables $x^{\alpha}$ and
$y^{\alpha}$ are distinct as well.

######  Definition 5.3.

To each term $t$ of ${\textsf{HE-HA}}^{\omega}$ of type $\sigma$ with free
variables $x_{1},\ldots,x_{n}$ of types $\sigma_{1},\ldots,\sigma_{n}$,
respectively, we associate a term $t^{\alpha}$ of ${\textsf{HA}}^{\omega}$ of
type $\sigma^{+}$ with free variables $x_{1}^{\alpha},\ldots,x_{n}^{\alpha}$
of types $\sigma^{+}_{n},\ldots,\sigma^{+}_{n}$, respectively, as follows:

$\displaystyle x^{\alpha}$ $\displaystyle:\equiv$ $\displaystyle x^{\alpha},$
$\displaystyle{\bf c}^{\alpha}$ $\displaystyle:\equiv$ $\displaystyle{\bf
c}^{\alpha},$ $\displaystyle(s\,t)^{\alpha}$ $\displaystyle:\equiv$
$\displaystyle s^{\alpha}*t^{\alpha}.$

######  Definition 5.4.

To each formula $\varphi$ of ${\textsf{HE-HA}}^{\omega}$ with free variables
$x_{1},\ldots,x_{n}$ of types $\sigma_{1},\ldots,\sigma_{n}$, respectively, we
associate a formula $\varphi^{\alpha}$ of ${\textsf{HA}}^{\omega}$ with free
variables $x_{1}^{\alpha},\ldots,x_{n}^{\alpha}$ of types
$\sigma^{+}_{n},\ldots,\sigma^{+}_{n}$, respectively, as follows:

$\displaystyle\big{(}\,{\textsf{ext}}_{\sigma}(t)\,\big{)}^{\alpha}$
$\displaystyle:\equiv$ $\displaystyle{\rm dom}_{\sigma}(t^{\alpha})$
$\displaystyle\big{(}\,s\equiv_{\sigma}t\,\big{)}^{\alpha}$
$\displaystyle:\equiv$ $\displaystyle s^{\alpha}\equiv_{\sigma^{+}}t^{\alpha}$
$\displaystyle\big{(}\,s=_{\sigma}t\,\big{)}^{\alpha}$ $\displaystyle:\equiv$
$\displaystyle\lnot\exists x:{\sigma^{-}}.\,{\rm
app}(s^{\alpha},t^{\alpha},x)$ $\displaystyle\bot^{\alpha}$
$\displaystyle:\equiv$ $\displaystyle\bot$
$\displaystyle\big{(}\,\varphi\Box\psi\,\big{)}^{\alpha}$
$\displaystyle:\equiv$ $\displaystyle\varphi^{\alpha}\Box\psi^{\alpha}\mbox{
for }\Box\in\\{\lor,\land,\to\\}$ $\displaystyle\big{(}\,\exists
x:\sigma.\,\varphi\,\big{)}^{\alpha}$ $\displaystyle:\equiv$
$\displaystyle\exists x:{\sigma^{+}}.\,\varphi^{\alpha}$
$\displaystyle\big{(}\,\forall x:\sigma.\,\varphi\,\big{)}^{\alpha}$
$\displaystyle:\equiv$ $\displaystyle\forall
x:{\sigma^{+}}.\,\varphi^{\alpha}$

######  Theorem 5.5.

If ${\textsf{HE-HA}}^{\omega}\vdash\varphi$, then
${\textsf{HA}}^{\omega}\vdash\varphi^{\alpha}$.

###### Proof.

By induction on the derivation of ${\textsf{HE-HA}}^{\omega}\vdash\varphi$. ∎

######  Theorem 5.6.

${\textsf{HA}}^{\omega}\vdash\mathsf{CEXT}^{\alpha}$.

###### Proof.

Recall that

$\displaystyle\mathsf{CEXT}:\quad\exists
Z.\,\forall^{\textsf{ext}}f:(\sigma\to 0)\to(\tau\to
0).\,\forall^{\textsf{ext}}x,y:\sigma\to 0.\,\forall^{\textsf{ext}}v:\tau.$
$\displaystyle\big{(}\,fxv\not\equiv_{0}fyv\to{\textsf{ext}}(Zfxyv)\land
x(Zfxyv))\not\equiv_{0}y(Zfxyv)\,\big{)}.$

Therefore we would like to have

$Z*f*x*y*v\equiv\mathsf{fst}((\mathsf{snd}\,f)xy(\mathsf{pair}\,v\,0)).$

We can achieve this by putting

$Z:\equiv\mathsf{pair}(\lambda f.\mathsf{pair}(\lambda x.\mathsf{pair}(\lambda
y.\mathsf{pair}(\lambda
v.\mathsf{fst}((\mathsf{snd}\,f)xy(\mathsf{pair}\,v\,0)))\,0)\,0)\,0)\,0.$

∎

######  Remark 5.7.

By induction on the type structure of $\sigma$, one can also show that the
$\alpha$-translation interprets the principle
$x=_{\sigma}y\to{\textsf{ext}}_{\sigma}(x)\to{\textsf{ext}}_{\sigma}(y)$.

######  Remark 5.8.

The $\alpha$-translation that we presented in this section is a variation on
the $\alpha$-translation from the appendix to our paper [2]. A minor
difference is that the clauses there are a bit more complicated, because they
have been designed in such a way that ${\rm app}(x,y,z)$ implies ${\rm
dom}(x)$ and ${\rm dom}(y)$. We have dropped this strictness requirement here
(see Remark 2.10).

The crucial difference is that in the current paper the $\alpha$-translation
is an interpretation of the hybrid system ${\textsf{HE-HA}}^{\omega}$, instead
of ${\textsf{E-HA}}^{\omega}$. Indeed, without a hybrid system,
$\mathsf{CEXT}$ and Theorem 5.6 cannot even be formulated. Of course,
${\textsf{E-HA}}^{\omega}$ can be embedded into ${\textsf{HE-HA}}^{\omega}$,
as we showed in Theorem 4.1, but the principle $\mathsf{CEXT}$ lies outside
the image of this embedding.

##  6\. Realizability and functional interpretations for hybrid arithmetic

In this section we will indicate how interpretations like modified
realizability and the Diller-Nahm functional interpretation can be extended to
${\textsf{H-HA}}^{\omega}$. We will not discuss these matters in too much
detail; also, we will assume familiarity with the standard treatment of these
interpretations for ${\textsf{HA}}^{\omega}$ (for which, see [5], [8] or [4]).

###  6.1. Modified realizability

Kreisel’s modified realizability interpretation can be seen as an
interpretation of ${\textsf{HA}}^{\omega}$ into itself. This can be extended
to an interpretation of ${\textsf{H-HA}}^{\omega}$ into itself by adding the
following clauses:

$\displaystyle x\,{\textsf{mr}}\,{\textsf{ext}}(y)$ $\displaystyle:\equiv$
$\displaystyle{\textsf{ext}}(y),$ $\displaystyle x\,{\textsf{mr}}\,y=z$
$\displaystyle:\equiv$ $\displaystyle y=z.$

This interpret also validates principles like $\mathsf{EXT}$ or
$\mathsf{CEXT}$, assuming they hold in the interpreting system: in particular,
mr can also be extended to an interpretation of ${\textsf{HE-HA}}^{\omega}$
into itself.

###  6.2. A functional interpretation

It is also possible to set up a functional interpretation of
${\textsf{H-HA}}^{\omega}$ into itself. For this we choose the version of
${\textsf{H-HA}}^{\omega}$ without a primitive notion of extensional equality,
using Remark 2.6. In that case we only have ext as a new symbol, which we will
interpret as itself. For our functional interpretation, we choose the Diller-
Nahm variant of Gödel’s original Dialectica interpretation [3]: indeed, we
have to, because ext is an atomic formula which is not decidable.222Not to
mention that we have written this paper with ${\textsf{HA}}^{\omega}$ as our
base system, for which Gödel’s original interpretation does not work, because
for higher types $\sigma$ the equality predicate $\equiv_{\sigma}$ cannot be
shown to be decidable in ${\textsf{HA}}^{\omega}$. Indeed, for Gödel’s
Dialectica interpretation to work we need all atomic formulas to be decidable;
the benefit of the Diller-Nahm variant is that it also works when this is not
the case.

It is not hard to see that in this way the Diller-Nahm variant also works as
an interpretation of ${\textsf{H-HA}}^{\omega}$ into itself. Note, however,
that this interpretation need not interpret the formula

$x=y\to{\textsf{ext}}(x)\to{\textsf{ext}}(y).$

This has been our main reason for excluding this axiom from
${\textsf{H-HA}}^{\omega}$.

Let us what happens with extensionality, for which we take the formulation

$\displaystyle\mathsf{EXT}^{\prime}:\quad{\textsf{ext}}_{(\sigma\to
0)\to(\tau\to 0)}(f)\to{\textsf{ext}}_{\sigma\to
0}(x)\to{\textsf{ext}}_{\sigma\to 0}(y)\to$
$\displaystyle\forall^{{\textsf{ext}}{}}\\!u:\sigma.xu\equiv_{0}yu\to\forall^{{\textsf{ext}}{}}\\!v:\tau.fxv\equiv_{0}fyv,$

as in Corollary 3.7. The Diller-Nahm functional interpretation asks us in this
case to find a functional $E$, which given $f:(\sigma\to 0)\to(\tau\to
0),x,y:\sigma\to 0$ and $v:\tau$ computes a finite list $Efxyv$ such that if
$v$ is extensional and $xu\equiv_{0}xu$ for every extensional $u$ in the list
$Efxyv$, then $fxv\equiv_{0}fyv$. If our interpreting system includes

$\displaystyle\mathsf{CEXT}:\quad\exists
Z.\,\forall^{\textsf{ext}}f:(\sigma\to 0)\to(\tau\to
0).\,\forall^{\textsf{ext}}x,y:\sigma\to 0.\,\forall^{\textsf{ext}}v:\tau.$
$\displaystyle\big{(}\,fxv\not\equiv_{0}fyv\to{\textsf{ext}}(Zfxyv)\land
x(Zfxyv))\not\equiv_{0}y(Zfxyv)\,\big{)},$

then we can take $Efxyv$ to be the list consisting only of $Zfxyv$. Indeed,
$\mathsf{CEXT}$ is self-interpreting, in that if we assume it in the
interpreting system, then we can use that to show that the Diller-Nahm
interpretation validates that principle as well. So, in short, we have a
Diller-Nahm interpretation of ${\textsf{H-HA}}^{\omega}+\mathsf{CEXT}$ into
itself, while ${\textsf{H-HA}}^{\omega}\vdash\mathsf{CEXT}\to\mathsf{EXT}$, as
in Corollary 3.8; therefore we can also interpret ${\textsf{HE-HA}}^{\omega}$
into ${\textsf{HE-HA}}^{\omega}+\mathsf{CEXT}$ using the Diller-Nahm
interpretation.

##  7\. Conclusion

We have introduced hybrid systems for arithmetic, ${\textsf{H-HA}}^{\omega}$
and ${\textsf{HE-HA}}^{\omega}$, and shown how it can be used to formulate a
strong extensionality principle, which we have dubbed converse extensionality.
Inspired by Brouwer’s notion of apartness, we have defined a proof-theoretic
interpretation, which we have called the $\alpha$-translation, which can be
used to eliminate this converse extensionality principle.

One potential application of this work is in proof-mining [4], in particular,
in proof-mining arguments using extensionality principles. One standard way to
treat these is by first eliminating them using the elimination of
extensionality and then applying functional interpretation. This would
correspond to going from ${\textsf{E-HA}}^{\omega}$ to
${\textsf{HA}}^{\omega}$ along the top of the following (non-commuting)
diagram, combining elimination of extensionality (EE) and the (Diller-Nahm)
functional interpretation (DN).

${{\textsf{HA}}^{\omega}}$${{\textsf{E-HA}}^{\omega}}$${{\textsf{HE-
HA}}^{\omega}}$${{\textsf{HA}}^{\omega}}$${{\textsf{HE-
HA}}^{\omega}+\mathsf{CEXT}}$$\scriptstyle{\rm DN}$$\scriptstyle{\rm
Th.4.1}$$\scriptstyle{\rm EE}$$\scriptstyle{\rm Th.4.3}$$\scriptstyle{\rm
DN}$$\scriptstyle{\alpha}$

The $\alpha$-translation provides an alternative to this, by allowing us to go
along the bottom of the diagram above. Since the $\alpha$-translation of
equality statements looks easier than their functional interpretation, this
deserves further exploration.

In addition, the idea of a hybrid system to formulate and study hybrid
principles should be more widely applicable. For instance, there are
discontinuous functionals realizing continuity principles ([5, Theorem 2.6.7]
or [6]), and one could also imagine non-majorizable functionals realizing
majorizability statements. We believe this is another promising direction for
future research.

## References

  * [1] B. van den Berg.  A note on equality in finite-type arithmetic.  MLQ Math. Log. Q., 63(3-4):282–288, 2017.
  * [2] B. van den Berg and R. Paßmann.  Converse extensionality and apartness.  Log. Methods Comput. Sci., 18(4), 2022.
  * [3] J. Diller and W. Nahm.  Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen.  Arch. Math. Logik Grundlag., 16:49–66, 1974.
  * [4] U. Kohlenbach.  Applied proof theory: proof interpretations and their use in mathematics.  Springer Monographs in Mathematics. Springer-Verlag, Berlin, 2008.
  * [5] A. S. Troelstra, editor.  Metamathematical investigation of intuitionistic arithmetic and analysis.  Lecture Notes in Mathematics, Vol. 344. Springer-Verlag, Berlin-New York, 1973.
  * [6] A. S. Troelstra.  A note on non-extensional operations in connection with continuity and recursiveness.  Indag. Math., 39(5):455–462, 1977.  Nederl. Akad. Wetensch. Proc. Ser. A 80.
  * [7] A. S. Troelstra and D. van Dalen.  Constructivism in mathematics. Vol. I, volume 121 of Studies in Logic and the Foundations of Mathematics.  North-Holland Publishing Co., Amsterdam, 1988.
  * [8] A. S. Troelstra and D. van Dalen.  Constructivism in mathematics. Vol. II, volume 123 of Studies in Logic and the Foundations of Mathematics.  North-Holland Publishing Co., Amsterdam, 1988.