# Arrow algebras

Benno van den Berg and Marcus Briët

###### Abstract.

In this paper we introduce arrow algebras, simple algebraic structures which
induce elementary toposes through the tripos-to-topos construction. This
includes localic toposes as well as various realizability toposes, in
particular, those realizability toposes which are obtained from partial
combinatory algebras. Since there are many examples of arrow algebras and
arrow algebras have a number of closure properties, including a notion of
subalgebra given by a nucleus, arrow algebras provide a flexible tool for
constructing toposes; we illustrate this by providing some general tools for
creating toposes for Kreisel’s modified realizability.

##  1\. Introduction

The purpose of this paper is to introduce _arrow algebras_ : an arrow algebra
is a simple and flexible algebraic structure, generalising that of a complete
Heyting algebra (or locale), which induces an elementary topos through the
tripos-to-topos construction. Besides localic toposes, the toposes constructed
in this way include many realizability toposes.

For that reason our work on arrow algebras is similar to the work on evidenced
frames [3], basic combinatory objects [6, 15] or implicative algebras [11].
Indeed, our arrow algebras originated as a modification of Alexandre Miquel’s
notion of an implicative algebra and this is how we will introduce them in
this paper. However, in comparison with these other concepts the main
advantages of arrow algebras are the number of naturally occurring examples
and the number of interesting closure properties. In particular, we will show
that arrow algebras are closed under a notion of “subalgebra” given by nuclei.
For this reason we believe that our arrow algebras provide a flexible and
fruitful tool for analysing and constructing new toposes; we will illustrate
this by constructing a number of toposes for Kreisel’s modified realizability.

The main contributions of this paper are therefore as follows:

  1. (1)

We introduce the notion of an arrow algebra and give numerous examples.

  2. (2)

We show how for each arrow algebra one can construct an associated _arrow
topos_. This construction goes via the tripos-to-topos construction [8, 14],
so, in fact, what we do is construct an associated _arrow tripos_.

  3. (3)

We show that arrow algebras are closed under a notion of a subalgebra given by
_nuclei_. This is inspired by locale theory where there is a correspondence
between sublocales of a locale $A$ and nuclei on a locale $A$. We define a
notion of a nucleus on arrow algebra and we show how such a nucleus gives rise
to another arrow algebra (which should be thought of as a “subalgebra”). This
is an example of a construction which fails for implicative algebras.

  4. (4)

We illustrate the flexibility of the theory of arrow algebras by showing how
they can be used to construct various toposes for Kreisel’s modified
realizability.

The precise contents of our paper are as follows. In Section 2 we recall
Miquel’s notion of an implicative algebra as well as the notion of a tripos
and a partial combinatory algebra. In Section 3 we introduce the notion of an
arrow algebra, give a range of examples and show that they are closed under a
notion of subalgebra induced by a nucleus. In Section 4 we show how one can
interpret $\lambda$-terms from the untyped $\lambda$-calculus in arrow
algebras. This will be used in Section 5, where we show how one can construct
triposes from arrow algebras. In Section 6 we will show how the tripos
obtained from a subalgebra of an arrow algebra is a subtripos of the tripos
obtained from the original algebra. In Section 7 we will use the theory we
have developed to construct various toposes for modified realizability. In the
conclusion, Section 8, we will comment on related work and indicate some
directions for future research.

The contents of this paper are based on the MSc thesis of the second author
supervised by the first author.

##  2\. Implicative algebras

As said, our arrow algebras originated as a modification of Miquel’s notion of
an implicative algebra, as introduced in [11]. For that reason we will start
by recapitulating Miquel’s theory. While doing so, we will also recall the
notions of a tripos and a partial combinatory algebra which will become
important in the later sections. The main references for this section are [11,
14, 18].

###  2.1. Definition

In order to define implicative algebras, we first need to define implicative
structures.

######  Definition 2.1.

An _implicative structure_ is a complete poset $(A,\preccurlyeq)$ together
with a binary operation $\to:A\times A\to A$ satisfying the following two
conditions:

  1. (1)

If $a^{\prime}\preccurlyeq a$ and $b\preccurlyeq b^{\prime}$ then $a\to
b\preccurlyeq a^{\prime}\to b^{\prime}$.

  2. (2)

For all $a\in A$ and subsets $B\subseteq A$ we have

$a\to\bigcurlywedge_{b\in B}b=\bigcurlywedge_{b\in B}(a\to b).$

######  Remark 2.2.

We think of the elements of $A$ as _truth values_ or _pieces of evidence_.
However, we should _not_ think of $\preccurlyeq$ as giving us the logical
ordering of these truth values: the logical ordering will be a derived
concept. In many examples the ordering $\preccurlyeq$ is closer to a notion of
_subtyping_ or an _information ordering_ : one could say that $a\preccurlyeq
b$ means that any evidence contained in $a$ is also contained in $b$, making
$b$ less informative than $a$. We will occasionally refer to this ordering as
the _evidential ordering_.

The next step is that we single out those bits of evidence that we regard as
conclusive: or those “designated” truth values that we consider to be true.
This we do by choosing a _separator_.

######  Definition 2.3.

Let $A=(A,\preccurlyeq,\to)$ be an implicative structure. A _separator_ on $A$
is a subset $S\subseteq A$ such that the following are satisfied:

  1. (1)

If $a\in S$ and $a\preccurlyeq b$, then $b\in S$.

  2. (2)

If $a\to b\in S$ and $a\in S$, then $b\in S$.

  3. (3)

Both $\mathbf{k}$ and $\mathbf{s}$ belong to $S$.

Here ${\bf k}$ and ${\bf s}$ are defined as follows:

$\displaystyle{\bf k}$ $\displaystyle:=$ $\displaystyle\bigcurlywedge_{a,b\in
A}a\to b\to a$ $\displaystyle{\bf s}$ $\displaystyle:=$
$\displaystyle\bigcurlywedge_{a,b,c\in A}(a\to b\to c)\to(a\to b)\to(a\to c)$

######  Definition 2.4.

An _implicative algebra_ is a quadruple $(A,\preccurlyeq,\to,S)$ consisting of
an implicative structure $(A,\preccurlyeq,\to)$ and a separator $S$ on that
implicative structure.

######  Remark 2.5.

We are using the convention that the operation $\to$ associates to the right,
and hence $a\to b\to c$ has to be read as $a\to(b\to c)$. In addition, $\to$
binds stronger than $\bigcurlywedge$ and hence the scope of the occurrences of
$\bigcurlywedge$ in the definitions of $\bf k$ and $\bf s$ above is both times
the entire formula.

###  2.2. Examples

Although the main emphasis in this paper will be on the more general arrow
algebras that will be defined below, it is still good to see a number of
examples of implicative algebras.

####  2.2.1. Locales

Any locale (or complete Heyting algebra) $L$ is an example of an implicative
structure. If we choose the “canonical” separator $S=\\{\top\\}$, consisting
only of the top element of the locale, then we obtain an implicative algebra.
However, on a locale separators coincide with filters, so any filter on a
locale equips the locale with the structure of an implicative algebra.

####  2.2.2. Total combinary algebras

For the next example, we need to give a summary of the theory of partial and
total combinatory algebras. This will provide us with some genuine examples of
arrow algebras as well. For this summary we will follow the definitions and
conventions of Jetze Zoethout’s PhD thesis [18]. The reader should be warned
that these are not standard; however, they are quite convenient for our
purposes and that is why we shall follow them here.

######  Definition 2.6.

A _partial applicative poset_ is a triple $(P,\cdot,\leq)$ where $(P,\leq)$ is
a poset and $\cdot$ is a partial binary operation $\cdot\,:A\times
A\rightharpoonup A$ called _application_ which has downwards closed domain and
is monotone on its domain. In other words:

> if $a^{\prime}\cdot b^{\prime}$ is defined and $a\leq a^{\prime}$ and $b\leq
> b^{\prime}$, then $a\cdot b$ is defined and $a\cdot b\leq a^{\prime}\cdot
> b^{\prime}$.

We say that $P$ is _total_ is the application operation is total, and $P$ is
_discrete_ if the order $\leq$ is a discrete order.

######  Remark 2.7.

Most of the time the symbol for the application operation will be omitted, so
that the result of applying $a$ to $b$ will be denoted $ab$ instead of $a\cdot
b$. To indicate that $ab$ is defined, we will write $ab\downarrow$ (and
$ab\uparrow$ if it is not defined). Furthermore, the convention is that
application associates to the left, so $abc$ has to be read as $(ab)c$.

######  Definition 2.8.

Let $(P,\cdot,\leq)$ be a partial applicative poset. A _filter_ $P^{\\#}$ on
$P$ is a subset $P^{\\#}\subseteq P$ such that:

  1. (i)

if $a,b\in P^{\\#}$ and $ab$ is defined, then $ab\in P^{\\#}$.

  2. (ii)

if $a\leq b$ and $a\in P^{\\#}$, then $b\in P^{\\#}$.

A quadruple $(P,\cdot,\leq,P^{\\#})$ consisting of a partial applicative poset
$(P,\cdot,\leq)$ together with a filter $P^{\\#}$ on it will be called a
_partial applicative structure_. A partial applicative structure will be
called _absolute_ if $P^{\\#}=P$.

######  Definition 2.9.

A partial applicative structure $(P,\cdot,\leq,P^{\\#})$ will be called a
_partial combinatory algebra_ (or _pca_ for short) if there are elements
$\mathbf{k},\mathbf{s}\in P^{\\#}$ satisfying:

  1. (1)

both $\mathbf{k}a$ and $\mathbf{k}ab$ are defined and $\mathbf{k}ab=a$;

  2. (2)

$\mathbf{s}ab\downarrow$;

  3. (3)

if $ac(bc)$ is defined, then so is $\mathbf{s}abc$ and $\mathbf{s}abc\leq
ac(bc)$,

for all $a,b,c\in P$. A partial combinatory algebra will be called _total_ or
_discrete_ if the underlying partial applicative poset is; and _absolute_ if
it is absolute as a partial applicative structure.

A fundamental result in the theory of pcas is that they are _combinatory
complete_. To state this property, we need the following definition.

######  Definition 2.10.

The _terms_ over a pca $P$ is the smallest collection of formal expressions
satisfying the following properties:

  1. (i)

any element of $P$ is a term over $P$.

  2. (ii)

any variable is a term over $P$.

  3. (iii)

if $s,t$ are terms over $P$, then so is $st$.

######  Theorem 2.11.

(Combinatory completeness) Let $P$ be a pca. There exists an operation which
given a non-empty sequence of distinct variables
$\overline{x}=x_{1},\ldots,x_{n}$, a variable $y$ and a term
$t(\overline{x},y)$ over $P$ with all free variables among $\overline{x},y$,
produces an element $\lambda^{*}\overline{x},y.t\in P$, which satisfies:

  1. (i)

for any $\overline{a}\in P^{n}$, the expression
$(\lambda^{*}\overline{x},y.t)\overline{a}$ is defined.

  2. (ii)

for any $\overline{a}\in P^{n}$ and $b\in P$, if the expression
$t(\overline{a},b)$ is defined, then so is
$(\lambda^{*}\overline{x},y.t)\overline{a}b$ and

$(\lambda^{*}\overline{x},y.t)\overline{a}b\leq t(\overline{a},b).$

  3. (iii)

if all constants of $t$ are elements of $P^{\\#}$, then also
$\lambda^{*}\overline{x},y.t\in P^{\\#}$.

###### Proof.

In Zoethout’s PhD thesis [18], this is Proposition 2.1.24. ∎

Next, let us briefly give some examples of pcas. For more examples (and
theory), the reader is referred to [18, 14].

######  Example 2.12.

  1. (1)

Let $\mathbb{N}$ be the set of natural numbers and $\varphi_{e}$ be the $e$th
partial recursive function under some coding of the partial recursive
functions. Then we can define an application operation, _Kleene application_ ,
on $\mathbb{N}$, by defining $m\cdot n=\varphi_{m}(n)$, the result of the
$m$th partial recursive function on input $n$, whenever defined. This gives us
an example of an absolute and discrete partial combinatory algebra, which is
denoted by $K_{1}$, Kleene’s first algebra.

  2. (2)

On the set $\mathbb{N}\to\mathbb{N}$ of functions from the natural numbers to
the natural numbers we can also define a partial application function. To
explain how, we need to establish some notation.

Let us fix some recursive coding of finite sequences with
$[a_{0},a_{1},\ldots,a_{n-1}]$ in $\mathbb{N}$ being a code for the finite
sequence $<a_{0},a_{1},\ldots,a_{n-1}>$. If $\alpha\in\mathbb{N}^{\mathbb{N}}$
and $n\in\mathbb{N}$, then we will write $\alpha|_{n}$ for
$[\alpha(0),\ldots,\alpha(n-1)]$ and $[n]*\alpha$ for the function
$\alpha^{\prime}$ defined by $\alpha^{\prime}(0)=n$ and
$\alpha^{\prime}(i+1)=\alpha(i)$. For $\alpha\in\mathbb{N}^{\mathbb{N}}$ let
us define a partial function
$F_{\alpha}:\mathbb{N}^{\mathbb{N}}\rightharpoonup\mathbb{N}$ by setting
$F_{\alpha}(\beta)=m$ if and only if there exists an $n\in\mathbb{N}$ such
that:

    1. (i)

for all $i\mathchar 12604\relax n$, we have $\alpha(\beta|_{i})=0$;

    2. (ii)

$\alpha(\beta|_{n})=m+1$.

Then the application $\alpha\beta$ for
$\alpha,\beta\in\mathbb{N}^{\mathbb{N}}$ in Kleene’s second model $K_{2}$ is
defined as follows: we have $\alpha\beta\downarrow$ if $F_{\alpha}([n]*\beta)$
is defined for all $n\in\mathbb{N}$, in which case
$(\alpha\beta)(n)=F_{\alpha}([n]*\beta)$. In this way we obtain an absolute
and discrete pca. We can make it “relative” by choosing the set of total
computable functions as a separator.

  3. (3)

As an example of a total combinatory algebra, we can consider the set of
$\lambda$-terms modulo $\beta$-equivalence. This gives one an example of an
absolute and discrete total combinatory algebra. We can also consider the
terms of the lambda calculus with $M\leq N$ if $M\twoheadrightarrow_{\beta}N$,
that is, if $M$ reduces to $N$ in a finite number of $\beta$-reduction steps.
In that case we obtain an example of an absolute total combinatory algebra.

######  Theorem 2.13.

Let $(P,\leq,\cdot,P^{\\#})$ be a _total_ combinatory algebra. Then the
collection $DP$ of downwards closed subsets of $P$ ordered by inclusion can be
equipped with an implicative structure as follows:

$X\to Y:=\\{z\in P\,:\,(\forall x\in X)\,zx\in Y\\}.$

The downsets $X\in DP$ containing an element from the filter form a separator
on this implicative structure and hence we obtain an implicative algebra.

###### Proof.

The proof is not difficult: the reader can have a look at the proof of Theorem
3.9 below for the idea. ∎

Unfortunately, this result does not apply to partial combinatory algebras that
are not total and this will be one reason for wanting to generalise the theory
of implicative algebras.

###  2.3. Implicative triposes

A crucial result in the theory of implicative algebras is that each
implicative algebra gives rise to a tripos (the “implicative tripos”), from
which a topos can be built using the tripos-to-topos construction (see [8,
14]). Let us start by defining triposes.

######  Definition 2.14.

A _preHeyting algebra_ is a preorder whose poset reflection is a Heyting
algebra. Put differently, it is a preorder which has finite products and
coproducts and is cartesian closed as a category. We will write ${\bf
preHeyt}$ for the 2-category of preHeyting algebras: its objects are
preHeyting algebras, its 1-cells are functors preserving products, coproducts
and exponentials and its 2-cells are natural transformations between those.
Note that any two parallel 2-cells are identical, and ${\bf preHeyt}$ is
preorder-enriched.

######  Definition 2.15.

A _${\bf Set}$ -based tripos_ is a pseudofunctor $P:{\bf Set}^{\rm op}\to{\bf
preHeyt}$ satisfying the following requirements:

  1. (1)

For any function $f:J\to I$ the map $Pf:PI\to PJ$ has both a left adjoint
$\exists_{f}$ and a right adjoint $\forall_{f}$ in the category of preorders.
That is, for any $\alpha\in PJ$ we have elements
$\exists_{f}(\alpha),\forall_{f}(\alpha)\in PI$ such that for any $\beta\in
PI$ we have:

$\displaystyle\exists_{f}(\alpha)\leq\beta$ $\displaystyle\Longleftrightarrow$
$\displaystyle\alpha\leq Pf(\beta)$
$\displaystyle\beta\leq\forall_{f}(\alpha)$ $\displaystyle\Longleftrightarrow$
$\displaystyle Pf(\beta)\leq\alpha$

  2. (2)

Moreover, these adjoints satisfy the _Beck-Chevalley condition_. This
condition holds if for every pullback square

${L}$${K}$${J}$${I}$$\scriptstyle{g}$$\scriptstyle{m}$$\scriptstyle{n}$$\scriptstyle{f}$

in ${\bf Set}$, the square

(1)
${PL}$${PK}$${PJ}$${PI}$$\scriptstyle{\forall_{g}}$$\scriptstyle{\forall_{f}}$$\scriptstyle{Pm}$$\scriptstyle{Pn}$

commutes in ${\bf preHeyt}$ up to natural isomorphism.

  3. (3)

There is a some set $\Sigma$ an element $\sigma\in P\Sigma$ such that for any
set $I$ and any element $\varphi\in PI$ there exists a function
$[\varphi]:I\to\Sigma$ such that $\varphi\cong P[\varphi](\sigma)$. Such an
element $\sigma$ is called a _generic element_.

######  Remark 2.16.

In diagram (1), we have stated the Beck-Chevalley condition for the universal
quantifier; by taking the left adjoints of all the functors in this diagram,
one can show that the corresponding Beck-Chevalley condition for the
existential quantifier follows from that for the universal quantifier (indeed,
they are equivalent).

######  Proposition 2.17.

Let $A=(A,\preccurlyeq,\to,S)$ be an implicative algebra. If we preorder $A$
as follows:

$a\vdash b:\Longleftrightarrow a\to b\in S,$

then $(A,\vdash)$ carries the structure of a preHeyting algebra, with $\to$
being the Heyting implication in this preHeyting algebra.

###### Proof.

See [11, Proposition 3.21]. We will prove a more general statement in
Proposition 5.1 below. ∎

######  Remark 2.18.

We refer to $\vdash$ as the _logical ordering_ on $A$, as opposed to the
evidential ordering $\preccurlyeq$. As mentioned before, the logical ordering
is a derived, and weaker, concept. It is weaker is because one can show that
${\bf i}=\bigcurlywedge_{a\in A}a\to a\in S$ (see Corollary 3.7 below).
Therefore $a\to a\in S$ for any $a\in A$, and, because $\to$ is monotone in
the second argument, we have that $a\preccurlyeq b$ implies $a\to
a\preccurlyeq a\to b\in S$.

If $A=(A,\preccurlyeq,\to)$ is an implicative structure and $I$ is a set, then
we can give $A^{I}$, the set of functions from $I$ to $A$, an implicative
structure by choosing the pointwise ordering and implication. If $S$ is a
separator on $A$, then we can define two separators on $A^{I}$:

$\displaystyle\varphi:I\to A\in S_{I}$ $\displaystyle:\Leftrightarrow$
$\displaystyle(\forall i\in I)\,\varphi(i)\in S$ $\displaystyle\varphi:I\to
A\in S^{I}$ $\displaystyle:\Leftrightarrow$ $\displaystyle\bigcurlywedge_{i\in
I}\varphi(i)\in S$

Clearly, $S^{I}\subseteq S_{I}$, since separators are upwards closed. For our
purposes, the second separator $S^{I}$ is the relevant one. Indeed, this is
the one which is used in the following fundamental result about implicative
algebras.

######  Theorem 2.19.

(Implicative tripos) Let $A=(A,\preccurlyeq,\to,S)$ be an implicative algebra.
If to each set $I$ we assign the preHeyting algebra
$PI=(A^{I},\vdash_{S^{I}})$, while to each function $f:J\to I$ we assign the
mapping $PI\to PJ$ sending a function $\varphi:I\to A$ to the composition
$\varphi\circ f:J\to A$, then $P$ is a functor $P:{\bf Set}^{\rm op}\to{\bf
preHeyt}$. Indeed, $P$ is a tripos whose generic element is the identity
function $1_{A}:A\to A\in PA$.

###### Proof.

See [11, Theorem 4.11]. We will prove a more general statement in Theorem 5.2
below. ∎

##  3\. Arrow algebras

Alexandre Miquel has shown that every ${\bf Set}$-based tripos is equivalent
to an implicative tripos [12]. This is a beautiful result, which may lead one
to think that for the purpose of constructing triposes there is no need for
further generalising the concept of an implicative algebra.

However, we feel differently. The reason is that there are many naturally
occurring examples of objects which come close to being implicative algebras
and which also lead to triposes, but fail to satisfy all the axioms for an
implicative algebra. So while it must be the case that for each of these
examples an (in some sense) equivalent implicative algebra must exist,
Miquel’s proof constructs this implicative algebra by taking two iterations of
the powerset operation (among other things). We fear that the resulting
structure is simply too complicated to work with and do calculations in, while
at the same time not being the structure which is naturally there.111Another
worry is that Miquel’s proof uses the Axiom of Choice and Law of Excluded
Middle in ${\bf Set}$, so may not generalise to triposes over other base
toposes. Therefore we take a different approach here and define an algebraic
structure which is closer to the examples.

The reason why these examples are not implicative algebras is that they do not
satisfy the second axiom for an implicative structure:

$a\to\bigcurlywedge_{b\in B}b=\bigcurlywedge_{b\in B}(a\to b),$

if $a\in A,B\subseteq A$. Since

(2) $a\to\bigcurlywedge_{b\in B}b\preccurlyeq\bigcurlywedge_{b\in B}(a\to b)$

holds as soon as $\to$ is monotone in the second argument (a property which we
wish to preserve), the second axiom is equivalent to the inequality:

(3) $\bigcurlywedge_{b\in B}(a\to b)\preccurlyeq a\to\bigcurlywedge_{b\in
B}b.$

We will modify this axiom by making two changes to it:

  1. (i)

We only require that the inequality (3) holds for the logical ordering.

  2. (ii)

We require that all the elements in $B$ are implications (that is, of the form
$x\to y$ for some $x,y\in A$).

So what we will do is that first we will define a new combinator:

$\displaystyle{\bf a}$ $\displaystyle:=$ $\displaystyle\bigcurlywedge_{a\in
A,B\subseteq{\rm Im}(\to)}(\bigcurlywedge_{b\in B}a\to b)\to
a\to\bigcurlywedge_{b\in B}b$ $\displaystyle=$
$\displaystyle\bigcurlywedge_{x,I,(y_{i})_{i\in I},(z_{i})_{i\in
I}}\big{(}\,\bigcurlywedge_{i\in I}x\to y_{i}\to z_{i}\,\big{)}\to
x\to\big{(}\,\bigcurlywedge_{i\in I}y_{i}\to z_{i}\,\big{)}$

where ${\rm Im}(\to)$ stands for the image of the implication operation
$A\times A\to A$. Then we will drop the second axiom for an implicative
structure and replace this with the requirement that ${\bf a}\in S$.

######  Remark 3.1.

We will say more about our reasons for making the second modification (ii) in
Remark 3.15 below.

###  3.1. Definition

These ideas lead to the following definitions.

######  Definition 3.2.

An _arrow structure_ is a complete poset $(A,\preccurlyeq)$ together with a
binary operation $\to:A\times A\to A$ which is anti-monotone in the first and
monotone in the second argument. That is, it satisfies the following
condition:

> If $a^{\prime}\preccurlyeq a$ and $b\preccurlyeq b^{\prime}$ then $a\to
> b\preccurlyeq a^{\prime}\to b^{\prime}$.

######  Definition 3.3.

Let $A=(A,\preccurlyeq,\to)$ be an arrow structure. A _separator_ on $A$ is a
subset $S\subseteq A$ such that the following are satisfied:

  1. (1)

(Upwards closed) If $a\in S$ and $a\preccurlyeq b$, then $b\in S$.

  2. (2)

(Closure under modus ponens) If $a\to b\in S$ and $a\in S$, then $b\in S$.

  3. (3)

$S$ contains the combinators ${\bf k}$, ${\bf s}$ and ${\bf a}$.

######  Definition 3.4.

An _arrow algebra_ is a quadruple $(A,\preccurlyeq,\to,S)$ where
$(A,\preccurlyeq,\to)$ is an arrow structure and $S$ is a separator on that
arrow structure.

A fundamental property of arrow algebras is the following:

######  Proposition 3.5.

Let $A$ be an arrow algebra with separator $S$. Suppose $\varphi$ is an
propositional formula built from propositional variables $p_{1},\dots,p_{n}$
and implications only. If $\varphi$ is an intuitionistic tautology, then for
any separator $S$ we have

$\bigcurlywedge_{p_{1},\dots,p_{n}\in A}\varphi\in S.$

The proof of this proposition relies on the following lemma, which also has
many other useful applications and uses the assumption that the combinator
$\bf a$ belongs to the separator.

######  Lemma 3.6.

Suppose $A$ is an arrow algebra with separator $S$ and

$(x_{i})_{i\in I},(y_{i})_{i\in I},(z_{i})_{i\in I}$

are $I$-indexed families of elements from $A$. If

> $\bigcurlywedge_{i\in I}x_{i}\to y_{i}\to z_{i}\in S$ and
> $\bigcurlywedge_{i\in I}x_{i}\in S$,

then also $\bigcurlywedge_{i\in I}y_{i}\to z_{i}\in S$.

###### Proof.

Suppose $\bigcurlywedge_{i\in I}x_{i}\to y_{i}\to z_{i}\in S$ and
$\bigcurlywedge_{i\in I}x_{i}\in S$. Because $\bigcurlywedge_{i\in
I}x_{i}\preccurlyeq x_{i}$ for each $i\in I$ and separators are upwards
closed, the first assumption implies that

$\bigcurlywedge_{i\in I}(\bigcurlywedge_{i\in I}x_{i})\to y_{i}\to z_{i}\in
S.$

In addition, we have

$\mathbf{a}\preccurlyeq\big{(}\bigcurlywedge_{i\in I}(\bigcurlywedge_{i\in
I}x_{i})\to y_{i}\to z_{i}\big{)}\to(\bigcurlywedge_{i\in
I}x_{i})\to\bigcurlywedge_{i\in I}y_{i}\to z_{i}\in S.$

Therefore we obtain the desired result by using that separators are closed
under modus ponens. ∎

###### Proof.

(Of Proposition 3.5.) Note that the axioms $A\to(B\to A)$, $(A\to B\to
C)\to(A\to B)\to(A\to C)$, together with modus ponens are complete for the
implicative intuitionistic fragment [16, Theorem 5.1.10].

We prove the statement by induction on the number of applications of modus
ponens used in the derivation of the tautology $\varphi$. Note that no
propositional variable is a tautology, and therefore any tautology must be an
implication $\varphi=\alpha\to\beta$.

For the base case we are done by observing that $\mathbf{k},\mathbf{s}\in S$.

So suppose $\varphi=\alpha\to\beta$ was constructed from the tautologies
$\psi$ and $\psi\to\alpha\to\beta$. The induction hypothesis gives us that
$\bigcurlywedge_{\overline{p}\in A}\psi,\bigcurlywedge_{\overline{p}\in
A}\psi\to\alpha\to\beta\in S$. Therefore the desired result follows from Lemma
3.6. ∎

######  Corollary 3.7.

Let $S$ be a separator in an arrow algebra $A$. Then the following combinators
belong to $S$:

$\displaystyle{\bf i}$ $\displaystyle:=$ $\displaystyle\bigcurlywedge_{a\in
A}a\to a$ $\displaystyle{\bf b}$ $\displaystyle:=$
$\displaystyle\bigcurlywedge_{a,b,c\in A}(b\to c)\to(a\to b)\to(a\to c)$

Many arrow algebras satisfy the following additional property.

######  Definition 3.8.

Let $(A,\preccurlyeq,\to)$ be an arrow structure. If for any $a\in A$ and
$B\subseteq A$, the equation

$(\bigcurlyvee_{b\in B}b)\to a=\bigcurlywedge_{b\in B}(b\to a)$

holds, we say that the arrow structure is _compatible with joins_. An arrow
algebra is _compatible with joins_ if its underlying arrow structure is.

Although the theory of arrow algebras works perfectly well without assuming
that they are compatible with joins, it is still worthwhile to mention this
property because it is satisfied in many examples (such as locales) and it can
occassionally lead to some simplifications (see Lemma 5.3 below).

###  3.2. Examples

Let us now give some examples of arrow algebras.

####  3.2.1. Implicative algebras

Every implicative algebra is also an arrow algebra. The reason is that in an
implicative algebra the inequality (3) holds and therefore we have that:

${\bf i}=\bigcurlywedge_{c\in A}c\to c\preccurlyeq\bigcurlywedge_{c,d\in
A,c\preccurlyeq d}c\to d\preccurlyeq\bigcurlywedge_{a\in A,B\subseteq{\rm
Im}(\to)}(\bigcurlywedge_{b\in B}a\to b)\to a\to\bigcurlywedge_{b\in B}b={\bf
a}\in S.$

That is to say that for implicative structures any separator in the sense of
Definition 2.3 also contains the ${\bf a}$-combinator; therefore Definition
2.3 is consistent with Definition 3.3 and any implicative algebra is also an
arrow algebra.

####  3.2.2. Pcas

Since every implicative algebra is an arrow algebra, we know that the downsets
in a total combinatory algebra form an arrow algebra. However, we are now also
able to cover the partial case.

######  Theorem 3.9.

Let $(P,\leq,\cdot,P^{\\#})$ be a partial combinatory algebra. Then the
collection $DP$ of downwards closed subsets of $P$ ordered by inclusion can be
equipped with an arrow structure as follows:

$X\to Y:=\\{z\in P\,:\,(\forall x\in X)\,zx\downarrow\mbox{ and }zx\in
Y\,\\}.$

The downsets $X\in DP$ containing an element from the filter form a separator
on this arrow structure and hence we obtain an arrow algebra. This arrow
algebra is compatible with joins.

###### Proof.

That $\to$ defines an arrow structure which is compatible with joins is easy
to see; therefore we only show that

$S:=\\{X\in DP\,:\,(\exists x\in X)\,x\in P^{\\#}\\}$

defines a separator.

  1. (1)

$S$ is clearly upwards closed.

  2. (2)

$S$ is closed under modus ponens: Suppose $X\to Y,X\in S$. Then there exist
$x,z\in P^{\\#}$ with $x\in X$ and $z\in X\to Y$. By the definition of
implication, $zx\downarrow$ and $zx\in Y$ and by the definition of a filter,
$zx\in P^{\\#}$. Hence $Y\in S$.

  3. (3)

So it remains to show that the combinators ${\bf k},{\bf s},{\bf a}\in S$. Let
$\underline{k},\underline{s}\in P^{\\#}$ be the combinators from the pca $P$
as in Definition 2.9. Then $\underline{k}\in{\bf k}$, because:

$\displaystyle\mathbf{k}$ $\displaystyle=$ $\displaystyle\bigcap_{X,Y\in
DP}X\to(Y\to X)$ $\displaystyle=$ $\displaystyle\bigcap_{X,Y\in DP}\\{z\in
P\mid\forall x\in X(zx\downarrow\text{and }zx\in Y\to X)\\}$ $\displaystyle=$
$\displaystyle\bigcap_{X,Y\in DP}\\{z\in P\mid\forall x\in
X(zx\downarrow\text{and }zx\in\\{q\in P\mid\forall y\in
Y(qy\downarrow\text{and }qy\in X)\\})\\}$ $\displaystyle\ni$
$\displaystyle\underline{k}$

In a similar way one can show that $\underline{s}\in\mathbf{s}$.

To prove $\mathbf{a}\in S$ we use Theorem 2.11. We take

$t:=\lambda^{*}uv,w.uvw\in P^{\\#}$

and claim $t\in\mathbf{a}$. This holds iff for all $I,X,(Y_{i})_{i\in
I},(Z_{i})_{i\in I}\in DP$ and for all $s\in\bigcap_{i}X\to Y_{i}\to Z_{i}$,
we have $ts\downarrow$ and $ts\in X\to\bigcap_{i}Y_{i}\to Z_{i}$.

Let $s\in\bigcap_{i}X\to Y_{i}\to Z_{i}$ and $x\in X$. We have $ts\downarrow$
and $tsx\downarrow$. Moreover, for any $i\in I$ and $y\in Y_{i}$ we have
$sxy\downarrow$, so $tsxy\leq sxy\in Z_{i}$. Because $Z_{i}$ is downwards
closed, we have $tsxy\in Z_{i}$ and we are done.

∎

####  3.2.3. PERs

The downset construction we saw above is the simplest way of constructing an
arrow algebra out of a pca. However, there are many more. We will discuss one
more example here, that of PERs (partial equivalence relations) over a pca
$P$.

If $P$ is a partial applicative poset, then so is $P\times P$ and therefore
$D(P\times P)$ is an arrow structure. More explicitly, the elements of
$D(P\times P)$ are downwards closed binary relations on $P$ which are ordered
by inclusion and carry the following implication:

$R\to S:=\\{\,(x,x^{\prime})\in P^{2}\,\mid\,\forall(y,y^{\prime})\in
R\,\big{(}\,xy\downarrow,x^{\prime}y^{\prime}\downarrow,(xy,x^{\prime}y^{\prime})\in
S\,\big{)}\,\\}.$

######  Theorem 3.10.

Let $(P,\cdot,\leq)$ be a partial applicative poset and write

${\rm PER}(P):=\\{\,R\in D(P\times P)\,\mid\,R\text{ is symmetric and
transitive}\,\\}$

for the set of all binary relations on $P$ which are downwards closed,
symmetric and transitive. If we order ${\rm PER}(P)$ by inclusion with given
by intersection and implication as above, we obtain a arrow structure which is
compatible with joins. Moreover if $(P,P^{\\#},\cdot,\leq)$ is a PCA, defining

$S:=\\{\,R\in{\rm PER}(P)\,\mid\,\exists(x,y)\in R\,\big{(}\,x,y\in
P^{\\#}\,\big{)}\,\\}$

gives us a separator on this arrow structure.

###### Proof.

First of all, since symmetric and transitive relations are closed under
implication and arbitrary intersections, we can conclude that ${\rm PER}(P)$
does indeed carry an arrow structure.

To see that it is compatible with joins, we first observe that the join is
given by the transitive closure of the union. We only need to show

$(\bigcurlyvee_{i\in I}R_{i})\to S\succcurlyeq\bigcurlywedge_{i\in I}(R_{i}\to
S)$

as the other inequality is always true. So let $(x,x^{\prime})\in\bigcap_{i\in
I}(R_{i}\to S)$ and $(a,a^{\prime})\in\bigcurlyvee_{i\in I}R_{i}$. There are
elements $a_{0},a_{1},\dots,a_{n}\in A$ such that $(a_{k},a_{k+1})\in
R_{i_{k}}$ for $i_{k}\in I$, $k\mathchar 12604\relax n$ and additionally
$a_{0}=a$ and $a_{n}=a^{\prime}$. By symmetry and transitivity
$(x^{\prime},x^{\prime})\in\bigcurlywedge_{i\in I}(R_{i}\to S)$, so
$(xa_{0},x^{\prime}a_{1}),(x^{\prime}a_{k},x^{\prime}a_{k+1})\in S$. By
transitivity now $(xa,x^{\prime}a^{\prime})=(xa_{0},x^{\prime}a_{n})\in S$.

It remains to prove that $S$ is a separator. The argument is similar to that
of Theorem 3.9 with $(\underline{k},\underline{k})\in\mathbf{k}$,
$(\underline{s},\underline{s})\in\mathbf{s}$ and $(t,t)\in\mathbf{a}$. ∎

###  3.3. Nuclei

The previous examples are not just as examples of arrow algebras, but also of
what Miquel calls _quasi-implicative algebras_. In fact, Miquel observes that
much of his theory also goes through for quasi-implicative algebras, where we
require the law

$a\to\bigcurlywedge_{b\in B}b=\bigcurlywedge_{b\in B}(a\to b)$

for elements $a\in A$ and _inhabited_ subsets $B$ of $A$ (see [11, Sections
4.6 and 4.7] for details). So the question arises why we have not chosen to
work with his theory of quasi-implicative algebras. The reason is that they do
not seem to be closed under the construction of “subalgebras” through nuclei,
as we will now explain.

######  Definition 3.11.

Let $A=(A,\preccurlyeq,\to,S)$ be an arrow algebra. A mapping $j:A\to A$ will
be called a _nucleus_ if the following three properties are satisfied:

  1. (1)

$a\preccurlyeq b$ implies $ja\preccurlyeq jb$ for all $a,b\in A$.

  2. (2)

$\bigcurlywedge_{a\in A}a\to ja\in S$.

  3. (3)

$\bigcurlywedge_{a,b\in A}(a\to jb)\to(ja\to jb)\in S$.

######  Example 3.12.

Let $A$ be an arrow algebra and $c\in A$. It follows from Proposition 3.5 that
the following define nuclei on $A$:

  1. (i)

$jx=c\to x$.

  2. (ii)

$jx=(x\to c)\to c$.

  3. (iii)

$jx=(x\to c)\to x$.

(See [1] for more information.)

######  Lemma 3.13.

Let $j$ be a nucleus on an arrow algebra $A$ with separator $S$. Then we have
the following:

  1. (i)

$\bigcurlywedge_{a\in A}jja\to ja\in S$.

  2. (ii)

$\bigcurlywedge_{a,b\in A}(a\to b)\to(ja\to jb)\in S$.

  3. (iii)

$\bigcurlywedge_{a,b\in A}j(a\to b)\to(ja\to jb)\in S$.

###### Proof.

  1. (i)

$\bigcurlywedge_{a}ja\to ja\in S$ and $\bigcurlywedge_{a}(ja\to ja)\to(jja\to
ja)\in S$ together with Lemma 3.6 gives $\bigcurlywedge_{a}jja\to ja\in S$.

  2. (ii)

Because $\mathbf{b}\in S$ we get

$\bigcurlywedge_{a,b\in A}((a\to b)\to(a\to jb))\to((a\to jb)\to(ja\to
jb))\to((a\to b)\to(ja\to jb))\in S$

Therefore $\bigcurlywedge(a\to b)\to(ja\to jb)\in S$ will follow as soon as we
can show that $\bigcurlywedge(a\to b)\to(a\to jb)\in S$ and
$\bigcurlywedge(a\to jb)\to(ja\to jb)\in S$. The latter is true by definition.
For the former we note that $\bigcurlywedge_{a,b}(b\to jb)\to(a\to b)\to(a\to
jb)\in S$ by Proposition 3.5 and $\bigcurlywedge_{b\in B}b\to jb\in S$.
Therefore the desired result follows from Lemma 3.6.

  3. (iii)

We derive:

$\displaystyle\bigcurlywedge(a\to b)\to(ja\to jb)\in S$
$\displaystyle\Rightarrow$ $\displaystyle\bigcurlywedge ja\to(a\to b)\to jb\in
S$ $\displaystyle\Rightarrow$ $\displaystyle\bigcurlywedge ja\to j(a\to b)\to
jb\in S$ $\displaystyle\Rightarrow$ $\displaystyle\bigcurlywedge j(a\to
b)\to(ja\to jb)\in S.$

∎

This notion of nucleus generalises the notion from locale theory. In locale
theory we would obtain a new locale (a sublocale) by restricting to the
elements $a\in A$ for which $ja=a$. For arrow algebras, however, we can say
the following:

######  Proposition 3.14.

Let $(A,\preccurlyeq,\to,S)$ be an arrow algebra and $j:A\to A$ be a nucleus
on it. Then $A_{j}=(A,\preccurlyeq,\to_{j},S_{j})$ with

$\displaystyle a\to_{j}b$ $\displaystyle:\equiv$ $\displaystyle a\to jb$
$\displaystyle a\in S_{j}$ $\displaystyle:\Leftrightarrow$ $\displaystyle
ja\in S$

is also an arrow algebra. If $A$ is compatible with joins, then so is $A_{j}$.

###### Proof.

  1. (1)

$\to_{j}$ defines an arrow structure: This follows from the monotonicity of
$j$.

  2. (2)

$S_{j}$ is upwards closed: Follows easily from the definition.

  3. (3)

$S_{j}$ is closed under modus ponens: Suppose $a\to_{j}b\in S_{j}$ and $a\in
S_{j}$. Then $j(a\to jb)\in S$ and $ja\in S$. With (iii) of Lemma 3.13 we see
$ja\to jjb\in S$. Because $S$ is closed under modus ponens we have $jjb\in S$.
By (i) of the same lemma we get $jb\in S$, and thus $b\in S_{j}$.

  4. (4)

$S_{j}$ contains the combinators: Note that we have $S\subseteq S_{j}$.

First of all, we need to show

$\mathbf{k}_{j}:=\bigcurlywedge_{a,b}a\to_{j}(b\to_{j}a)\in S_{j}.$

However, from $\mathbf{k}\in S$, the laws for a nucleus and “intuitionistic
reasoning”, it follows that $\mathbf{k}_{j}\in S$. Hence $\mathbf{k}_{j}\in
S_{j}$ holds as well.

We define similarly

$\displaystyle\mathbf{s}_{j}$
$\displaystyle:=\bigcurlywedge_{a,b,c}(a\to_{j}b\to_{j}c)\to_{j}(a\to_{j}b)\to_{j}a\to_{j}c.$

From the properties of a nucleus, we obtain

$(a\to j(b\to jc))\to(a\to jb\to jc)\in S.$

Since also $\mathbf{s}\in S$, we obtain $\mathbf{s}_{j}\in S$ and hence
$\mathbf{s}_{j}\in S_{j}$ as well.

Finally, we define

$\displaystyle\mathbf{a}_{j}:=$
$\displaystyle\bigcurlywedge_{x,I,(y_{i})_{i\in I},(z_{i})_{i\in
I}}(\bigcurlywedge_{i\in
I}x\to_{j}y_{i}\to_{j}z_{i})\to_{j}x\to_{j}(\bigcurlywedge_{i\in
I}y_{i}\to_{j}z_{i})$ $\displaystyle=$
$\displaystyle\bigcurlywedge_{x,I,(y_{i})_{i\in I},(z_{i})_{i\in
I}}\big{(}\bigcurlywedge_{i\in I}x\to j(y_{i}\to jz_{i})\big{)}\to
j\big{(}x\to j(\bigcurlywedge_{i\in I}y_{i}\to jz_{i})\big{)}$

We will again show that $\mathbf{a}_{j}\in S$, from which the desired
$\mathbf{a}_{j}\in S$ follows.

By repeatedly applying Lemma 3.13, we see that $\mathbf{a}_{j}\in S$ follows
from

$\bigcurlywedge_{x,I,(y_{i})_{i\in I},(z_{i})_{i\in I}}(\bigcurlywedge_{i\in
I}x\to jy_{i}\to jz_{i})\to x\to\bigcurlywedge_{i\in I}jy_{i}\to jz_{i}\in S.$

But because $\mathbf{a}\in S$ and

$\displaystyle\mathbf{a}\preccurlyeq$
$\displaystyle\bigcurlywedge_{x,I,(y_{i})_{i\in I},(z_{i})_{i\in
I}}(\bigcurlywedge_{i\in I}x\to jy_{i}\to jz_{i})\to x\to\bigcurlywedge_{i\in
I}jy_{i}\to jz_{i}\in S,$

the desired result follows.

∎

######  Remark 3.15.

We are now in a position to address the question why we are making not just
the first modification (i), but also the second modification (ii) to the
definition of an implicative algebra (see the discussion preceding Definition
3.2). Concretely, the question would be why we require ${\bf a}$ to belong to
the separator, instead of requiring that for

$\mathbf{a}^{\prime}:=\bigcurlywedge_{a\in A,B\subseteq
A}(\bigcurlywedge_{b\in B}a\to b)\to a\to\bigcurlywedge_{b\in B}b.$

There are two reasons for this. The first is that we are not able to prove
that $\mathbf{a}^{\prime}\in S$ for the example of pcas (see Theorem 3.9). In
that case we do not have that $t^{\prime}=\lambda^{*}u,v.uv\in{\bf
a}^{\prime}$. For a counterexample, consider $B=\emptyset$ and $a=\top$. If
$x$ is an element in a pca like $K_{1}$ such that $xy$ is never defined, then
$x\in\bigcurlywedge_{b\in B}a\to b=\top$ but $t^{\prime}x\not\in
a\to\bigcurlywedge_{b\in B}b=\top\to\top$. The second reason is that in the
proof of the preceding proposition, Proposition 3.14, we are unable to show
that ${\bf a}^{\prime}_{j}\in S_{j}$ if ${\bf a}^{\prime}\in S$.

It has to be admitted that the situation is not entirely clear-cut. The reason
is that both in the case of pcas and in the case of subalgebras we do not have
counterexamples showing that ${\bf a^{\prime}}\in S$ fails in general; we are
only saying that we are unable to prove that it is true.

##  4\. The interpretation of $\lambda$-terms

One of the main results for arrow algebras is that each arrow algebra gives
rise to a tripos, and hence a topos. For that result we need some more tools
for showing that elements belong to a separator, and that is what we will do
in this section. Indeed, we will show how $\lambda$-terms can be interpreted
in an arrow algebra. The main result of this chapter is that the
interpretation of a closed $\lambda$-term belongs to any separator. It should
be noted that Miquel proves a similar result (see [11, Proposition 3.4]);
however, our interpretation of $\lambda$-terms differs significantly from his.
We will say more about this at the end of this section.

###  4.1. The main result

We remind the reader that $\lambda$-terms are defined as follows.

######  Definition 4.1.

The collection of _$\lambda$ -terms_ is the smallest collection of formal
expressions satisfying the following:

  1. (1)

Each variable is a $\lambda$-term.

  2. (2)

(Application) If $M$ and $N$ are $\lambda$-terms, then so is $MN$.

  3. (3)

(Abstraction) If $M$ is a $\lambda$-term and $x$ is a variable, then $\lambda
x.M$ is a $\lambda$-term.

In order to interpret $\lambda$-terms, we need to interpret both application
and abstraction. We start with the former. In what follows $A$ will be an
arbitrary arrow structure.

######  Definition 4.2.

(Application) For all $a,b\in A$ we define

$U_{a,b}:=\\{c\to d\in A\mid a\preccurlyeq b\rightarrow c\to d\\}$

and the _application_

$ab:=\bigcurlywedge U_{a,b}$

######  Lemma 4.3.

For any arrow structure, the application has the following properties:

  1. (1)

If $a\preccurlyeq a^{\prime}$ and $b\preccurlyeq b^{\prime}$, then
$ab\preccurlyeq a^{\prime}b^{\prime}$.

  2. (2)

$(a\to b\to c)a\preccurlyeq b\to c$.

  3. (3)

$(a\to\bigcurlywedge_{i\in I}b_{i}\to c_{i})a\preccurlyeq\bigcurlywedge_{i\in
I}b_{i}\to c_{i}$.

###### Proof.

  1. (1)

Because the implication is antitone in its first operand we get
$U_{a^{\prime},b^{\prime}}\subseteq U_{a,b}$.

  2. (2)

Note $b\to c\in U_{a\to b\to c,a}$. So $\bigcurlywedge U_{a\to b\to
c,a}\preccurlyeq b\to c$.

  3. (3)

Because $\to$ is monotone in its second operand and using (1) and (2) we see

$(a\to\bigcurlywedge_{i\in I}b_{i}\to c_{i})a\preccurlyeq(a\to b_{i}\to
c_{i})a\preccurlyeq b_{i}\to c_{i}$

for every $i\in I$, so the statement follows.

∎

Next, we define abstraction for arrow structures.

######  Definition 4.4.

(Abstraction) Let $A$ be an arrow structure and $f:A\to A$ a function. Then we
define

$\lambda f:=\bigcurlywedge_{x\in A}x\to\partial f(x)\in A,$

where

$\partial a:=\top\to a.$

######  Remark 4.5.

At this point we will fix some important notational conventions. Point (1) of
Lemma 4.3 implies that each arrow structure can be considered as a _total_
applicative poset (see Definition 2.6). For arrow structures we use the same
notational conventions as for applicative posets; in particular, we will use
the convention that application associates to the left, meaning that $abc$
stands for $(ab)c$.

To further reduce clutter we will say that in the following list the
operations to the left bind stronger than the operation to the right:

$\cdot\mbox{ (application)}\quad\to\quad\partial\quad\bigcurlywedge$

So, in particular, $a\to bc$ is shorthand for $a\to(bc)$, $\partial ab$ stands
for $\partial(ab)$ and $\partial a\to b$ is supposed to mean $\top\to a\to b$,
and not $(\top\to a)\to b$.

######  Lemma 4.6.

Let $f,g:A\to A$ be functions, then we have the following properties:

  1. (1)

If $f(a)\preccurlyeq g(a)$ for all $a\in A$, then $\lambda
f\preccurlyeq\lambda g$.

  2. (2)

$(\lambda f)a\preccurlyeq\partial f(a)$ for all $a\in A$.

###### Proof.

  1. (1)

By monotonicity in the second component of the implication we see

$\lambda f=\bigcurlywedge_{a}a\to\partial
f(a)\preccurlyeq\bigcurlywedge_{a}a\to\partial g(a)=\lambda g$

  2. (2)

$(\bigcurlywedge_{x}x\to\partial f(x))a\preccurlyeq(a\to\partial
f(a))a\preccurlyeq\partial f(a)$ by Lemma 4.3.

∎

Now that we have defined an interpretation for application and abstraction, we
can recursively define an interpretation in an arrow structure for each
$\lambda$-term.

######  Definition 4.7.

Let $A$ be an arrow structure and $M$ a $\lambda$-term with free variables
among $x_{1},\dots,x_{n}$. The _interpretation_ $M^{A}:A^{n}\to A$ of the
$\lambda$-term $M$ in $A$ will recursively be defined as

  1. (1)

If $M=x_{i}$, then $t^{A}$ is the projection on the $i$th coordinate.

  2. (2)

For products: $(MN)^{A}:A^{n}\to A:\overline{a}\mapsto
M^{A}(\overline{a})N^{A}(\overline{a})$.

  3. (3)

If the free variables of $M$ are among $x_{1},\dots,x_{n},x$, then

$(\lambda x.M)^{A}:\overline{a}\mapsto\lambda(a\mapsto M(\overline{a},a))$

######  Proposition 4.8.

If $M$ is a $\lambda$-term with free variables among $x_{1},\dots,x_{n}$ and
$a_{1}\preccurlyeq b_{1},\dots,a_{n}\preccurlyeq b_{n}$ in an arrow structure
$A$, then

$M^{A}(\overline{a})\preccurlyeq M^{A}(\overline{b})$

###### Proof.

Using Lemma 4.6 and Lemma 4.3 this is to be proven with induction on the
structure of $M$. ∎

We can now state this section’s main result.

######  Theorem 4.9.

Let $A$ be any arrow algebra with separator $S$. If $M$ is a $\lambda$-term
with free variables among $x_{1},\dots,x_{n}$ and $a_{1},\dots,a_{n}\in S$,
then

$M^{A}(a_{1},\dots,a_{n})\in S.$

###  4.2. The proof

To prove the main result, we are going to need some auxiliary lemmas. The idea
is that for each closed $\lambda$-term $M$, we give an associated ‘combinatory
term’ $M_{*}$ with $M_{*}^{A}\preccurlyeq M^{A}$ and $M_{*}^{A}\in S$. So the
combinatory term gives enough ‘evidence’ for the original term to be an
element of the separator.

We start with proving some properties of separators.

######  Lemma 4.10.

Separators are closed under application.

###### Proof.

Let $S$ be a separator and suppose $a,b\in S$. Because

$a\preccurlyeq\bigcurlywedge_{c\to d\in U_{a,b}}b\to c\to d$

we have $\bigcurlywedge_{c\to d\in U_{a,b}}b\to c\to d\in S$. Now
$\mathbf{a}\in S$ implies

$\displaystyle\big{(}\,\bigcurlywedge_{c\to d\in U_{a,b}}b\to c\to
d\,\big{)}\to b\to ab$ $\displaystyle=$
$\displaystyle\big{(}\,\bigcurlywedge_{c\to d\in U_{a,b}}b\to c\to
d\,\big{)}\to b\to\bigcurlywedge_{c\to d\in U_{a,b}}c\to d$ $\displaystyle\in
S.$

Using that separators are closed under modus ponens (twice), we obtain that
$ab\in S$. ∎

######  Lemma 4.11.

For any separator $S$,

$\eta:=\bigcurlywedge_{a\in A}a\to\bigcurlywedge_{b\in A}b\to ab\in S$

.

###### Proof.

By the definition of $U_{a,b}$ we have

$\displaystyle\mathbf{i}=\bigcurlywedge_{a\in A}a\to a$
$\displaystyle\preccurlyeq\bigcurlywedge_{a\in A}a\to\bigcurlywedge_{b\in
A}\bigcurlywedge_{c\to d\in U_{a,b}}b\to c\to d$
$\displaystyle\preccurlyeq\bigcurlywedge_{a,b\in A}a\to\bigcurlywedge_{c\to
d\in U_{a,b}}b\to c\to d\in S$

Here the first inequality follows from the definition of $U_{a,b}$, while the
second holds because $\to$ is monotone in the second argument (as in equation
(2)).

Similarly, as in the previous lemma, we have that

$\bigcurlywedge_{a,b\in A}\,\big{(}\,\bigcurlywedge_{c\to d\in U_{a,b}}b\to
c\to d\,\big{)}\to b\to ab\in S.$

Therefore it follows from Lemma 3.6 that

$\bigcurlywedge_{a,b\in A}a\to b\to ab\in S.$

Using $\mathbf{a}\in S$, again in combination with Lemma 3.6, we will get
$\eta\in S$. ∎

Next we define, in a way, the ‘ugly brothers’ of the combinators $\mathbf{i}$,
$\mathbf{k}$ and $\mathbf{s}$. These combinators will be the building blocks
of the combinatory terms that we will define later in Definition 4.13.

######  Lemma 4.12.

We define the following auxiliary combinators:

$\displaystyle\mathbf{i^{\prime}}$ $\displaystyle:=$
$\displaystyle\bigcurlywedge_{a\in A}a\to\partial a$
$\displaystyle\mathbf{k^{\prime}}$ $\displaystyle:=$
$\displaystyle\bigcurlywedge_{a\in A}a\to\bigcurlywedge_{b\in A}b\to\partial
a$ $\displaystyle\mathbf{s^{\prime}}$ $\displaystyle:=$
$\displaystyle\bigcurlywedge_{a\in A}a\to\bigcurlywedge_{b\in
A}b\to\bigcurlywedge\\{c\to\partial d\mid\exists e,f\in
A(ac\preccurlyeq\partial e,bc\preccurlyeq\partial f,ef\preccurlyeq d)\\}$

Then for any separator $S$ we have
$\mathbf{i^{\prime}},\mathbf{k^{\prime}},\mathbf{s^{\prime}}\in S$.

###### Proof.

The first two follow easily from Proposition 3.5, where $\mathbf{k^{\prime}}$
also needs the use of $\mathbf{a}\in S$.

As for $\mathbf{s}^{\prime}$, first of all define

$X:=\\{(a,b,c,d,e,f)\in A^{6}\mid ac\preccurlyeq\partial
e,bc\preccurlyeq\partial f,ef\preccurlyeq d\\}$

Then

$\mathbf{s}\preccurlyeq\bigcurlywedge_{(a,b,c,d,e,f)\in X}\big{(}c\to(\partial
f)\to\partial d\big{)}\to(c\to\partial f)\to(c\to\partial d)\in S$

together with

$\eta\preccurlyeq\bigcurlywedge_{(a,b,c,d,e,f)\in X}b\to c\to
bc\preccurlyeq\bigcurlywedge_{(a,b,c,d,e,f)\in X}b\to c\to\partial f\in S$

gives, with some intuitionistic reasoning,

(4) $\bigcurlywedge_{(a,b,c,d,e,f)\in X}\big{(}c\to(\partial f)\to\partial
d\big{)}\to b\to c\to\partial d\in S$

To be precise, we use here that $(A\to B\to C)\to(D\to B)\to(A\to D\to C)$ is
an intuitionistic tautology. So the claim follows from Proposition 3.5 in
combination with Lemma 3.6.

The proof of Lemma 4.11 together with the fact that $(A\to B\to C)\to(D\to
A)\to(D\to B)\to(D\to C)$ is an intuitionistic tautology, gives us that

$\bigcurlywedge_{(a,b,c,d,e,f)\in X}(\partial e)\to(\partial
f)\to\partial(ef)\preccurlyeq\bigcurlywedge_{(a,b,c,d,e,f)\in X}(\partial
e)\to(\partial f)\to\partial d\in S.$

Combined with

$\bigcurlywedge_{(a,b,c,d,e,f)\in X}a\to c\to
ac\preccurlyeq\bigcurlywedge_{(a,b,c,d,e,f)\in X}a\to c\to\partial e\in S$

we obtain

$\bigcurlywedge_{(a,b,c,d,e,f)\in X}a\to c\to(\partial f)\to\partial d\in S.$

If we further combine this with (4), we can conclude that

$\bigcurlywedge_{(a,b,c,d,e,f)\in X}a\to b\to(c\to\partial d)\in S.$

Fromthis $\mathbf{s^{\prime}}\in S$ follows by again using $\mathbf{a}\in S$
and Lemma 3.6 twice. ∎

######  Definition 4.13.

The _combinatory terms_ are the smallest collection of formal expressions
satisfying the following rules:

  1. (1)

Every variable is a combinatory term.

  2. (2)

The combinators $\mathbf{i^{\prime}},\mathbf{k^{\prime}},\mathbf{s^{\prime}}$
and $\eta$ are combinatory terms.

  3. (3)

If $M$ and $N$ are combinatory terms, then so is $MN$.

Like $\lambda$-terms, combinatory terms can be interpreted in any arrow
structure.

######  Definition 4.14.

Let $A$ be an arrow structure and $M$ be a combinatory term with free
variables among $\overline{x}=x_{1},\dots,x_{n}$. For
$\overline{a}=a_{1},\dots,a_{n}\in A^{n}$, we define the interpretation
$M^{A}[\overline{a}/\overline{x}]$ inductively as follows:

  1. (1)

$x^{A}_{i}[\overline{a}/\overline{x}]:=a_{i}$

  2. (2)

$\mathbf{i^{\prime}}^{A}[\overline{a}/\overline{x}]:=\mathbf{i^{\prime}}$

  3. (3)

$\mathbf{k^{\prime}}^{A}[\overline{a}/\overline{x}]:=\mathbf{k^{\prime}}$

  4. (4)

$\mathbf{s^{\prime}}^{A}[\overline{a}/\overline{x}]:=\mathbf{s^{\prime}}$

  5. (5)

$\eta^{A}[\overline{a}/\overline{x}]:=\eta$

  6. (6)

$(MN)^{A}[\overline{a}/\overline{x}]=M^{A}[\overline{a}/\overline{x}]N^{A}[\overline{a}/\overline{x}]$

######  Lemma 4.15.

Suppose $A$ is an arrow algebra with separator $S$. If $M$ a combinatory term
with variables among $\overline{x}$ and $\overline{a}\in S^{n}$, then
$M^{A}[\overline{a}/\overline{x}]\in S$.

###### Proof.

Proof by induction on the structure of $M$, using Lemma 4.10, Lemma 4.11 and
Lemma 4.12. ∎

Next, we introduce a form of abstraction for the combinatory terms as well.

######  Definition 4.16.

For a combinatory term $M$ and a variable $x$ we define the combinatory term
$\langle x\rangle M$ inductively as follows:

  1. (1)

$\langle x\rangle x:=\mathbf{i}^{\prime}$.

  2. (2)

$\langle x\rangle M:=\mathbf{k}^{\prime}M$ if $M$ is $\mathbf{i}^{\prime}$,
$\mathbf{k}^{\prime}$, $\mathbf{s}^{\prime}$, $\eta$ or a variable different
from $x$.

  3. (3)

$\langle x\rangle(MN):=\mathbf{s}^{\prime}(\langle x\rangle M)(\langle
x\rangle N)$.

With this definition we now proceed to prove $\langle x\rangle M$ indeed
behaves like an abstraction.

######  Lemma 4.17.

If $M$ is a combinatory term, $x$ a variable and the free variables of
$\langle x\rangle M$ are contained in $\overline{y}$, then:

  1. (1)

The free variables of $\langle x\rangle M$ are those of $M$ minus $x$.

  2. (2)

For all $a\in A$, $\overline{a}\in A^{n}$ we have

$(\langle x\rangle M)^{A}[\overline{a}/\overline{y}]a\preccurlyeq\partial
M^{A}[\overline{a}/\overline{y},a/x]$

###### Proof.

We prove the case of application. So suppose we have $M=M_{1}M_{2}$ and

$(\langle x\rangle M_{i})^{A}[\overline{a}/\overline{y}]a\preccurlyeq\partial
M_{i}^{A}[\overline{a}/\overline{y},a/y]$

Then

$\displaystyle(\langle x\rangle M_{1}M_{2})^{A}[\overline{a}/\overline{y}]a$
$\displaystyle\preccurlyeq$ $\displaystyle(\mathbf{s}^{\prime}(\langle
x\rangle M_{1})(\langle x\rangle M_{2}))^{A}[\overline{a}/\overline{y}]a$
$\displaystyle=$
$\displaystyle(\mathbf{s}^{\prime}((<x>M_{1})^{A}[\overline{a}/\overline{y}])((<x>M_{2})^{A}[\overline{a}/\overline{y}]))a$

If we take a look at the definition of $\mathbf{s}^{\prime}$ we see we would
like

$\displaystyle a\to\partial(M_{1}M_{2})^{A}[\overline{a}/\overline{y},a/x]\in$
$\displaystyle\big{\\{}c\to\partial d\mid\exists e,f\in
A\big{(}(<x>M_{1})^{A}[\overline{a}/\overline{y}]c\preccurlyeq\partial
e,(<x>M_{2})^{A}[\overline{a}/\overline{y}]c\preccurlyeq\partial
f,ef\preccurlyeq d\big{)}\big{\\}}$

But the induction hypothesis tells us we can use
$e=M_{1}^{A}[\overline{a}/\overline{y},a/x]$ and
$f=M_{2}^{A}[\overline{a}/\overline{y},a/x]$.

Now follows

$\displaystyle(\mathbf{s}^{\prime}((<x>M_{1})^{A}[\overline{a}/\overline{y}])((<x>M_{2})^{A}[\overline{a}/\overline{y}]))a$
$\displaystyle\preccurlyeq$
$\displaystyle(a\to\partial(M_{1}M_{2})^{A}[\overline{a}/\overline{y},a/x)a$
$\displaystyle\preccurlyeq$
$\displaystyle\partial(M_{1}M_{2})^{A}[\overline{a}/\overline{y},a/x]$

and this is what we wanted to show. ∎

######  Definition 4.18.

For each $\lambda$-term $M$ we define an associated combinatory term $M_{*}$
as follows:

  1. (1)

For a variable $x$, we put $x_{*}:=x$.

  2. (2)

$(MN)_{*}:=M_{*}N_{*}$.

  3. (3)

$(\lambda x.M)_{*}:=\eta(\langle x\rangle M_{*})$.

######  Lemma 4.19.

Suppose $M$ is a $\lambda$-term with free variables among
$\overline{y}=y_{1},\dots,y_{n}$. For any arrow structure $A$ and
$\overline{a}\in A^{n}$ we have

$M^{A}_{*}[\overline{a}/\overline{y}]\preccurlyeq M^{A}(\overline{a}).$

###### Proof.

Proof by induction on the structure of $t$. We will only show the abstraction
case $M=\lambda x.N$ as the other two cases are trivial.

$\displaystyle M_{*}^{A}[\overline{a}/\overline{y}]$ $\displaystyle=$
$\displaystyle\eta(\langle x\rangle N^{A}_{*})[\overline{a}/\overline{y}]$
$\displaystyle\preccurlyeq$ $\displaystyle\bigcurlywedge_{a\in A}a\to(\langle
x\rangle N_{*}^{A})[\overline{a}/\overline{y}]a$ $\displaystyle\preccurlyeq$
$\displaystyle\bigcurlywedge_{a\in
A}a\to\partial\big{(}N_{*}^{A}[\overline{a}/\overline{y},a/x]\big{)}$
$\displaystyle\preccurlyeq$ $\displaystyle\bigcurlywedge_{a\in A}a\to\partial
N^{A}(\overline{a},a)$ $\displaystyle=$ $\displaystyle(\lambda
x.N)^{A}(\overline{a})$ $\displaystyle=$ $\displaystyle M^{A}(\overline{a})$

where the second and third inequality follow from Lemma 4.17 and the induction
hypothesis respectively. ∎

This finishes the proof of Theorem 4.9, as it now follows from Lemma 4.19 and
Lemma 4.15.

###  4.3. Discussion

In the next chapter we will make extensive use of the fact that every closed
$\lambda$-term is an element of every separator. Miquel proves a similar
result for implicative algebras, using simpler definitions of both the
application and abstraction. Indeed, Miquel defines the application as

$ab:=\bigcurlywedge\\{c\in A\mid a\preccurlyeq b\to c\\}$

and abstraction for a function $f:A\to A$ as

$\lambda f:=\bigcurlywedge_{a\in A}a\to f(a).$

With these definitions in hand, Miquel can prove the “adjunction property”

(5) $ab\preccurlyeq c\Leftrightarrow a\preccurlyeq b\to c,$

and this is used in the proof of his version of Theorem 4.9. The problem for
us is that for arrow algebras we can no longer prove the direction for left to
right in (5), as it uses the inequality $a\preccurlyeq b\to ab$. To prove this
inequality, Miquel uses the axiom which says that

$\bigcurlywedge_{b\in B}a\to b\preccurlyeq a\to\bigcurlywedge_{b\in B}b$

for any $B\subseteq A$, which is precisely the axiom that we have dropped. One
place where Miquel uses the inequality $a\preccurlyeq b\to ab$ is in showing
that separators are closed under application. This is surely a property we
want; however, we do not know how to show this for arrow algebras using
Miquel’s definition of application.

For this reason we have modified Miquel’s definitions of both the application
and the abstraction. The price we pay is that we no longer have $(\lambda
f)a\preccurlyeq f(a)$, as with Miquel’s definitions, but only $(\lambda
f)a\preccurlyeq\partial f(a)$. This means that we only have $\beta$-reduction
up to an additional $\partial$.

It has to be admitted that this is a bit unpleasant. It is not really a
problem, however, because $\partial$ is a nucleus and we have the following
result, saying that $a$ and $\partial a$ are logically equivalent (isomorphic
in the logical ordering):

######  Lemma 4.20.

Let $A$ be an arrow algebra with separator $S$. Then

$\bigcurlywedge_{a\in A}a\to\partial a\in S\quad\mbox{ and
}\bigcurlywedge_{a\in A}(\partial a)\to a\in S.$

###### Proof.

The former follows from ${\bf k}\in S$. To prove the latter, we note that
$B\to(B\to A)\to A$ is intuitionistic tautology, so

$\bigcurlywedge_{a,b}b\to(b\to a)\to a\in S$

and

$\bigcurlywedge_{a}\top\to(\top\to a)\to a\in S.$

Since $\top\in S$, the result follows from Lemma 3.6. ∎

##  5\. Arrow triposes

We now turn to proving the main result about arrow algebras: that they give
rise to triposes. That is, we will generalise Proposition 2.17 and Theorem
2.19 to arrow algebras.

Let us start with the former.

######  Proposition 5.1.

Let $A=(A,\preccurlyeq,\to,S)$ be an arrow algebra. In that case we can define
a preorder $\vdash$ on $A$ as follows:

$a\vdash b\text{ iff }a\to b\in S$

Moreover, the preorder $(A,\vdash)$ is a preHeyting algebra, with $\to$ being
the Heyting implication.

###### Proof.

Preorder:

Reflexivity and transitivity follow from $\mathbf{i}\in S$ and $\mathbf{b}\in
S$ respectively.

Bounded:

This follows from the general fact that $\vdash$ contains $\preccurlyeq$,
which is true because $\mathbf{i}\in S$ and implication is monotone. In
particular, we have $a\vdash\top$ and $\bot\vdash a$, because
$a\preccurlyeq\top$ and $\bot\preccurlyeq a$.

Binary meets:

For elements $a,b\in A$ we define

$a\times b:=\big{(}\lambda z.z(\partial a)(\partial b)\big{)}^{A}.$

By considering the $\lambda$-term $\lambda z.zx$ and observing that
$\bigcurlywedge_{x}x\to\bigcurlywedge_{y\in A}y\to\partial x\in S$ by Lemma
4.12, we can deduce from Theorem 4.9 that

$\bigcurlywedge_{z}z\to\partial
z(\bigcurlywedge_{x}x\to\bigcurlywedge_{y}y\to\partial x)\in S.$

In addition, we have

$\displaystyle\bigcurlywedge_{z}z\to\partial
z(\bigcurlywedge_{x}x\to\bigcurlywedge_{y}y\to\partial x)$
$\displaystyle\preccurlyeq$ $\displaystyle\bigcurlywedge_{a,b}(a\times
b)\to\partial(\bigcurlywedge_{z}z\to\partial\big{(}z(\partial a)(\partial
b))\big{)}\big{(}\bigcurlywedge_{x}x\to\bigcurlywedge_{y}y\to\partial
x\big{)}$ $\displaystyle\preccurlyeq$
$\displaystyle\bigcurlywedge_{a,b}(a\times
b)\to\partial\partial\big{(}(\bigcurlywedge_{x}x\to\bigcurlywedge_{y}y\to\partial
x)(\partial a)(\partial b)\big{)}$ $\displaystyle\preccurlyeq$
$\displaystyle\bigcurlywedge_{a,b}(a\times
b)\to\partial\partial\partial\partial a\in S.$

Here the inequalities follow from variations of Lemma 4.3. Now repeated
application of Lemma 4.20 gives us $a\times b\vdash a$. The inequality
$a\times b\vdash b$ can be achieved in a similar manner with the
$\lambda$-term $\lambda z.zx$ and $\bigcurlywedge_{x\in
A}x\to\bigcurlywedge_{y\in A}y\to\partial y\in S$.

Now suppose $c\vdash a$ and $c\vdash b$. It follows from Lemma 4.20 that
$c\to\partial a$, $c\to\partial b\in S$. Now we also calculate

$\displaystyle(\lambda zw.w((c\to\partial a)z)((c\to\partial b)z))^{A}$
$\displaystyle=$
$\displaystyle\bigcurlywedge_{z}z\to\partial\bigcurlywedge_{w}w\to\partial
w\big{(}(c\to\partial a)z\big{)}\big{(}(c\to\partial b)z\big{)}$
$\displaystyle\preccurlyeq$ $\displaystyle
c\to\partial\bigcurlywedge_{w}w\to\partial w(\partial a)(\partial
b)=c\to\partial(a\times b)\in S$

So $c\to(a\times b)\in S$, which gives us $c\vdash a\times b$.

Heyting implication:

First, let us observe that

$\displaystyle(\lambda wz.zw)^{A}$ $\displaystyle=$
$\displaystyle\bigcurlywedge_{w}w\to\partial\bigcurlywedge_{z}z\to\partial zw$
$\displaystyle\preccurlyeq$ $\displaystyle\big{(}(\partial c)\to(\partial
a)\to\partial b\big{)}\to\partial(c\times a)\to$
$\displaystyle\partial(c\times a)\big{(}(\partial c)\to(\partial a)\to\partial
b\big{)}$ $\displaystyle\preccurlyeq$ $\displaystyle\big{(}(\partial
c)\to(\partial a)\to\partial b\big{)}\to\partial(c\times a)\to$
$\displaystyle\partial\big{(}\bigcurlywedge_{z}z\to\partial z(\partial
c)(\partial a)\big{)}\big{(}(\partial c)\to(\partial a)\to\partial b\big{)}$
$\displaystyle\preccurlyeq$ $\displaystyle\big{(}(\partial c)\to(\partial
a)\to\partial b\big{)}\to\partial(c\times a)\to\partial\partial\partial b\in
S$

Therefore $c\vdash a\to b$ implies $c\times a\vdash b$. For the converse, we
observe that

$\displaystyle(\lambda wxy.w(\lambda
z.z(\mathbf{i}^{\prime}x)(\mathbf{i}^{\prime}y)))^{A}$
$\displaystyle\preccurlyeq$
$\displaystyle\bigcurlywedge_{w}w\to\partial\bigcurlywedge_{x}x\to\partial\bigcurlywedge_{y}y\to\partial
w\big{(}\bigcurlywedge_{z}z\to\partial z(\partial x)(\partial y)\big{)}$
$\displaystyle\preccurlyeq$ $\displaystyle(c\times a\to\partial b)\to\partial
c\to\partial a\to\partial(c\times a\to\partial b)(c\times a)$
$\displaystyle\preccurlyeq$ $\displaystyle(c\times a\to\partial b)\to\partial
c\to\partial a\to\partial\partial b\in S$

And therefore $c\times a\vdash b$ implies $c\vdash a\to b$.

Binary join:

For elements $a,b\in A$ we define

$a+b:=\bigcurlywedge_{c}(a\to\partial c)\to(b\to\partial c)\to\partial c.$

To prove $a\vdash a+b$, we observe that

$\displaystyle(\lambda xzw.zx)^{A}$ $\displaystyle=$
$\displaystyle\bigcurlywedge_{x}x\to\partial\bigcurlywedge_{z}z\to\partial\bigcurlywedge_{w}w\to\partial
zx$ $\displaystyle\preccurlyeq$ $\displaystyle
a\to\partial\bigcurlywedge_{c}(a\to\partial c)\to\partial(b\to\partial
c)\to\partial(a\to\partial c)a$ $\displaystyle\preccurlyeq$ $\displaystyle
a\to\partial\bigcurlywedge_{c}(a\to\partial c)\to\partial(b\to\partial
c)\to\partial\partial c\in S.$

Similarly, $(\lambda xzw.wx)^{A}\in S$ will give that $b\vdash a+b$.

Now suppose $a\vdash c$ and $b\vdash c$. Then $a\to\partial c\in S$ and
$b\to\partial c\in S$ and therefore

$\displaystyle(\lambda z.z(a\to\partial c)(b\to\partial c))^{A}$
$\displaystyle=$ $\displaystyle\bigcurlywedge_{z}z\to\partial z(a\to\partial
c)(b\to\partial c)$ $\displaystyle\preccurlyeq$
$\displaystyle(a+b)\to\partial\partial c\in S.$

We conclude that $a+b\vdash c$.

∎

Similarly as for implicative algebras, we can note that if
$A=(A,\preccurlyeq,\to)$ is an arrow structure and $I$ is a set, then we can
give $A^{I}$, the set of functions from $I$ to $A$, an arrow structure by
choosing the pointwise ordering and implication. If $S$ is a separator on $A$,
then we can define two separators on $A^{I}$:

$\displaystyle\varphi:I\to A\in S_{I}$ $\displaystyle:\Leftrightarrow$
$\displaystyle(\forall i\in I)\,\varphi(i)\in S$ $\displaystyle\varphi:I\to
A\in S^{I}$ $\displaystyle:\Leftrightarrow$ $\displaystyle\bigcurlywedge_{i\in
I}\varphi(i)\in S$

Clearly, $S^{I}\subseteq S_{I}$, since separators are upwards closed. Again,
the second separator $S^{I}$ will be the relevant one as it used in the
following result:

######  Theorem 5.2.

(Arrow tripos) Let $A=(A,\preccurlyeq,\to,S)$ be an implicative algebra. If to
each set $I$ we assign the preHeyting algebra $PI=(A^{I},\vdash_{S^{I}})$,
while to each function $f:I\to J$ we assign the mapping $PJ\to PI$ sending a
function $\varphi:J\to A$ to the composition $\varphi\circ f:I\to A$, then $P$
is a functor $P:{\bf Set}^{\rm op}\to{\bf preHeyt}$. Indeed, $P$ is a tripos
whose generic element is the identity function $1_{A}:A\to A\in PA$.

###### Proof.

Because $f^{*}=Pf$ preserves the implication and infima for any $f:I\to J$, it
will preserve the interpretation of $\lambda$-terms and hence the preHeyting
algebra structure. The functoriality of $P$ is clear, so we do indeed obtain a
functor $P:{\bf Set}^{\rm op}\to{\bf preHeyt}$.

We move on to the left and right adjoints. Let $f:I\to J$ be a function and
define for $j\in J$:

$\displaystyle\forall_{f}(\alpha)(j)$ $\displaystyle:=$
$\displaystyle\bigcurlywedge_{f(i)=j}\partial\alpha(i)$
$\displaystyle\exists_{f}(\alpha)(j)$ $\displaystyle:=$
$\displaystyle\bigcurlywedge_{c}\big{(}\,\bigcurlywedge_{f(i)=j}\alpha(i)\to\partial
c\,\big{)}\to\partial\partial c$

Let $\alpha\in PI$ and $\beta\in PJ$, and let us abbreviate $\alpha(i)$ as
$\alpha_{i}$ to reduce the use of brackets. We start by proving

$f^{*}\beta\vdash_{J}\alpha\Longleftrightarrow\beta\vdash_{I}\forall_{f}\alpha$

by showing:

$\begin{array}[]{lclc}f^{*}\beta\to\alpha\in
S^{I}&\Longleftrightarrow&\bigcurlywedge_{i\in
I}\beta_{f(i)}\to\partial\alpha_{i}\in S&\Longleftrightarrow\\\ \\\
\bigcurlywedge_{j\in
J}\bigcurlywedge_{f(i)=j}\beta_{j}\to\partial\alpha_{i}\in
S&\Longleftrightarrow&\bigcurlywedge_{j\in
J}\beta_{j}\to\bigcurlywedge_{f(i)=j}\partial\alpha_{i}\in
S&\Longleftrightarrow\\\ \\\ \beta\to\forall_{f}\alpha\in S^{J}\end{array}$

Here the third equivalence follows from $\mathbf{a}\in S$.

Next, we would like to show

$\alpha\vdash_{I}f^{*}\beta\Longleftrightarrow\exists_{f}\alpha\vdash_{J}\beta.$

Let us first suppose $\alpha\vdash_{I}Pf\beta$, which gives
$\bigcurlywedge_{i\in I}\alpha_{i}\to\partial\beta_{f(i)}\in S$. We can now
calculate:

$\displaystyle(\lambda xy.yx)^{A}$ $\displaystyle=$
$\displaystyle\bigcurlywedge_{x}x\to\partial\bigcurlywedge_{y}y\to\partial yx$
$\displaystyle\preccurlyeq$ $\displaystyle\bigcurlywedge_{j\in
J}\big{(}\bigcurlywedge_{f(i)=j}\alpha_{i}\to\partial\beta_{j}\big{)}\to\partial(\exists_{f}\alpha_{j})\to\partial\big{(}\exists_{f}\alpha_{j}\big{)}\big{(}\bigcurlywedge_{f(i)=j}\alpha_{i}\to\partial\beta_{j}\big{)}$
$\displaystyle\preccurlyeq$ $\displaystyle\bigcurlywedge_{j\in
J}\big{(}\bigcurlywedge_{f(i)=j}\alpha_{i}\to\partial\beta_{j}\big{)}\to\partial(\exists_{f}\alpha_{j})\to\partial\partial\partial\beta_{j}\in
S.$

Therefore

$\bigcurlywedge_{j\in J}(\exists_{f}\alpha_{j}\to\partial\beta_{j})\in S$

and $\exists_{f}\alpha\vdash_{J}\beta$, as desired.

For the other direction, suppose $\exists_{f}\alpha\vdash_{J}\beta$, so
$s:=\bigcurlywedge_{j\in J}\exists_{f}\alpha_{j}\to\partial\beta_{j}\in S$.

Again we calculate:

$\displaystyle(\lambda x.s(\lambda y.yx))^{A}$ $\displaystyle=$
$\displaystyle\bigcurlywedge_{x}x\to\partial s(\bigcurlywedge_{y}y\to\partial
yx)$ $\displaystyle\preccurlyeq$ $\displaystyle\bigcurlywedge_{j\in
J}\bigcurlywedge_{f(i)=j}\alpha_{i}\to\partial
s\big{(}\bigcurlywedge_{c}\big{(}\bigcurlywedge_{f(i^{\prime})=j}\alpha_{i^{\prime}}\to\partial
c\big{)}\to\partial\big{(}\bigcurlywedge_{f(i^{\prime})=j}\alpha_{i^{\prime}}\to\partial
c\big{)}\alpha_{i}\big{)}$ $\displaystyle\preccurlyeq$
$\displaystyle\bigcurlywedge_{j\in
J}\bigcurlywedge_{f(i)=j}\alpha_{i}\to\partial
s\big{(}\bigcurlywedge_{c}\big{(}\bigcurlywedge_{f(i^{\prime})=j}\alpha_{i^{\prime}}\to\partial
c\big{)}\to\partial\partial c)$ $\displaystyle=$
$\displaystyle\bigcurlywedge_{j\in
J}\bigcurlywedge_{f(i)=j}\alpha_{i}\to\partial\big{(}\bigcurlywedge_{j\in
J}\exists_{f}\alpha_{j}\to\partial\beta_{j}\big{)}\exists_{f}\alpha_{j}$
$\displaystyle\preccurlyeq$ $\displaystyle\bigcurlywedge_{j\in
J}\bigcurlywedge_{f(i)=j}\alpha_{i}\to\partial\partial\beta_{j}$
$\displaystyle=$ $\displaystyle\bigcurlywedge_{i\in
I}\alpha_{i}\to\partial\partial\beta_{f(i)}\in S.$

Hence $\alpha\vdash_{I}f^{*}\beta$, as desired.

Now for the Beck-Chevalley condition: It suffices to only consider those
pullback squares in $\mathbf{Set}$

${I}$${{I_{1}}}$${{I_{2}}}$${J}$$\scriptstyle{f_{1}}$$\scriptstyle{f_{2}}$$\scriptstyle{g_{2}}$$\scriptstyle{g_{1}}$

for which

  * •

$I=\\{(a,b)\in I_{1}\times I_{2}\mid g_{1}(a)=g_{2}(b)\\}$

  * •

the $f_{i}$ are just the projections to the $i$th coordinate.

We need to check that the square

${PI}$${{PI_{1}}}$${{PI_{2}}}$${PJ}$$\scriptstyle{Pf_{2}}$$\scriptstyle{\forall_{f_{1}}}$$\scriptstyle{\forall_{g_{2}}}$$\scriptstyle{Pg_{1}}$

commutes. So let $\alpha\in PI_{2}$. Then

$\begin{array}[]{lclc}Pg_{1}\circ\forall_{g_{2}}(\alpha)&=&\big{(}(\forall_{g_{2}}\alpha)_{g_{1}(i_{1})}\big{)}_{i_{1}\in
I}&=\\\ \\\ \Big{(}\bigcurlywedge_{\stackrel{{\scriptstyle i_{2}\in
I}}{{g_{2}(i_{2})=g_{1}(i_{1})}}}\partial\alpha_{i_{2}}\Big{)}_{i_{1}\in
I_{1}}&=&\Big{(}\bigcurlywedge_{\stackrel{{\scriptstyle(i_{1},i_{2})\in
I}}{{f_{1}(i_{1},i_{2})=i_{1}^{\prime}}}}\partial\alpha_{i_{2}}\Big{)}_{i_{1}^{\prime}\in
I_{1}}&=\\\ \\\ \forall_{f_{1}}(\alpha_{i_{2}})_{(i_{1}.i_{2})\in
I}&=&\forall_{f_{1}}\circ P{f_{2}}(\alpha)\end{array}$

Finally, for the generic element we take $\Sigma:=A$ and $\sigma:=1_{A}\in
PA$. ∎

If the arrow algebra is compatible with joins, we can give a much simpler
description of the existential quantifier, as follows.

######  Lemma 5.3.

If the arrow algebra $A$ is compatible with joins we can define the left
adjoint by

$\exists_{f}(\alpha):=\big{(}\bigcurlyvee_{f(i)=j}\alpha_{i}\big{)}_{j\in J}.$

###### Proof.

This follows from the following straightforward calculation:

$\displaystyle\bigcurlywedge_{i\in I}\alpha_{i}\to(f^{*}\beta)_{i}$
$\displaystyle=$ $\displaystyle\bigcurlywedge_{i\in
I}\alpha_{i}\to\beta_{f(i)}$ $\displaystyle=$
$\displaystyle\bigcurlywedge_{j\in
J}\bigcurlywedge_{f(i)=j}(\alpha_{i}\to\beta_{j})$ $\displaystyle=$
$\displaystyle\bigcurlywedge_{j\in
J}(\bigcurlyvee_{f(i)=j}\alpha_{i})\to\beta_{j}$ $\displaystyle=$
$\displaystyle\bigcurlywedge_{j\in J}(\exists_{f}\alpha)_{j}\to\beta_{j}.$

∎

##  6\. Subtriposes from nuclei

We have seen in Proposition 3.14 that whenever $j$ is a nucleus on an arrow
algebra $A$, we obtain a new arrow algebra $A_{j}$. The result in the previous
section says that we obtain triposes from both $A_{j}$ and $A$. The natural
question is how these triposes are related. Locale theory suggests that the
tripos associated to $A_{j}$ should be a subtripos of the one associated to
$A$ and in this section we will show that that is indeed what happens.

So let us first define what we mean by a subtripos.

######  Definition 6.1.

(Geometric morphism) Let $P$ and $Q$ be triposes over $\mathbf{Set}$. A
_geometric morphism_ $Q\to P$ is a pair $\Phi=(\Phi_{+},\Phi^{+})$ consisting
of natural transformations $\Phi^{+}:P\to Q$ and $\Phi_{+}:Q\to P$. We require
that for any set $X$ the monotone map $\Phi^{+}_{X}:P(X)\to Q(X)$ is left
adjoint to $\Phi_{+}^{X}$ and preserves finite meets.

######  Definition 6.2.

(Inclusion of triposes) Let $P$ and $Q$ be triposes over $\mathbf{Set}$. A
geometric morphism $\Phi=(\Phi_{+},\Phi^{+}):Q\to P$ is called an _inclusion
of triposes_ if $\Phi_{+}^{X}$ is full and faithful for every set $X$. (This
translates to that it has to preserve and reflect the preorder.) In this case
we call $Q$ a _subtripos_ of $P$.

These definitions allow us to state the result we wish to prove.

######  Proposition 6.3.

(Subtripos induced by a nucleus) Let $A$ be an arrow algebra and $j$ a nucleus
on $A$. Let $P$ be the tripos induced by $A$ and $P_{j}$ the one induced by
$A_{j}$. Then $P_{j}$ is a subtripos of $P$.

To prove it, we need the following lemma, which is a continuation of Lemma
3.13.

######  Lemma 6.4.

Suppose $A$ is an arrow algebra with separator $S$. If $j$ is a nucleus on
$A$, then we have:

  1. (iv)

$\bigcurlywedge_{a,b\in A}j(a\times b)\rightarrow(ja\times jb)\in S$ and
$\bigcurlywedge_{a,b\in A}(ja\times jb)\to j(a\times b)\in S$.

  2. (v)

$j\big{(}\bigcurlywedge_{x\in X}x\big{)}\preccurlyeq\bigcurlywedge_{x\in X}jx$
for any $X\subseteq A$.

###### Proof.

  1. (iv)

This follows from $\bigcurlywedge_{a,b\in A}j(a\to b)\to(ja\to jb)\in S$
(point (iii) of Lemma 3.13) combined with the knowledge that $\times$ and
$\to$ act as the conjunction and implication.

Indeed, from $\bigcurlywedge_{a,b}a\times b\to a\in S$ and
$\bigcurlywedge_{a,b}a\times b\to b\in S$, we get
$\bigcurlywedge_{a,b}j(a\times b)\to ja\in S$ and
$\bigcurlywedge_{a,b}j(a\times b)\to jb\in S$. This gives the first claim.

For the other, we start by noting $\bigcurlywedge_{a,b}a\to(b\to a\times b)\in
S$, and thus by using point (iii) twice, we obtain
$\bigcurlywedge_{a,b}ja\to(jb\to j(a\times b))\in S$.

  2. (v)

For all $x\in X$ we have $\bigcurlywedge_{x\in X}x\preccurlyeq x$. By
monotonicity we have $j\big{(}\bigcurlywedge_{x\in X}x\big{)}\preccurlyeq jx$
for all $x\in X$, giving the desired result.

∎

###### Proof.

(Of Proposition 6.3.) Before we start, it should be noted that if $j$ is a
nucleus on $A$ with separator $S$, then $j^{X}=j\circ-$ is also a nucleus on
$A^{X}$ with separator $S^{X}$. This means that Lemma 3.13 and Lemma 6.4 can
be applied to $j^{X}$ as well.

Moreover, we have

$\alpha\vdash_{j}\beta\mbox{ in }P_{j}(X)\mbox{ if and only if }\alpha\to
j^{X}\beta\in S^{X}.$

In other words, we claim that

$j\big{(}\bigcurlywedge_{x\in X}\alpha(x)\to j\beta(x)\big{)}\in
S\Longleftrightarrow\bigcurlywedge_{x\in X}\alpha(x)\to j\beta(x)\in S.$

The right to left implication is trivial. For the left to right direction we
first use point (v) of Lemma 6.4 to see that $j\big{(}\bigcurlywedge_{x\in
X}\alpha(x)\to j\beta(x)\big{)}\in S$ implies $j^{X}(\alpha\to j^{X}\beta)\in
S^{X}$. From here we use Lemma 3.13 for $j^{X}$:

$\displaystyle j^{X}(\alpha\to j^{X}\beta)\in S^{X}$
$\displaystyle\Rightarrow$ $\displaystyle j^{X}\alpha\to j^{X}j^{X}\beta\in
S^{X}$ $\displaystyle\Rightarrow$ $\displaystyle j^{X}\alpha\to j^{X}\beta\in
S^{X}$ $\displaystyle\Rightarrow$ $\displaystyle\alpha\to j^{X}\beta\in S^{X}$

From this and the fact that $j^{X}$ is a nucleus it follows fairly easily that
$\Phi_{+}$ and $\Phi^{+}$ defined as:

$\displaystyle\Phi_{+}^{X}:P_{j}X\to PX:\alpha\mapsto j\circ\alpha$
$\displaystyle\Phi_{X}^{+}:PX\to P_{j}X:\alpha\mapsto\alpha$

are natural transformations, which are pointwise adjoints, in the sense that

$\Phi^{+}_{X}\alpha\vdash_{j}\beta\Longleftrightarrow\alpha\vdash\Phi^{X}_{+}\beta$

for any set $X$. In addition, it also follows easily from this that $\Phi_{+}$
at each point preserves and reflects the preorder, that is,
$\alpha\vdash_{j}\beta\Leftrightarrow j\alpha\vdash j\beta$.

What remains to be checked is that $\Phi^{+}$ preserves finite meets. However,
if $\gamma\vdash_{j}\alpha$ and $\gamma\vdash_{j}\beta$, then $\gamma\to
j^{X}\alpha\in S^{X}$ and $\gamma\to j^{X}\beta\in S^{X}$. Therefore
$\gamma\to j^{X}\alpha\times j^{X}\beta\in S^{X}$ and $\gamma\to
j^{X}(\alpha\times\beta)\in S^{X}$ by (iv) of Lemma 6.4. Hence
$\gamma\vdash_{j}\alpha\times\beta$, as desired. ∎

######  Remark 6.5.

Every subtripos of a localic tripos is equivalent to one induced by a nucleus.
We have not investigated whether the same applies for arrow triposes.

The tripos $P_{j}$ we have just constructed is equivalent to another tripos
which we will denote $P^{j}$. It turns out that the latter topos is often more
useful for doing calculations. Indeed, the main benefit of $P^{j}$ is that it
is, pointwise, a subpreorder of $P$. That is, the preorder is the same, it
only has fewer elements.

######  Proposition 6.6.

The tripos $P_{j}$ and functor

$P^{j}:I\mapsto\\{\alpha\in PI\mid j^{I}\alpha\vdash\alpha\\}$

are equivalent, making $P^{j}$ also a tripos.

###### Proof.

For this we use the geometric morphism as defined in the proof of Proposition
6.3. It is easy to see that $\Phi:P_{j}\to P^{j}$ is well-defined. What is
left is to show is that $\Phi^{+}\Phi_{+}$ and $\Phi_{+}\Phi^{+}$ are
equivalent to the identities.

For this let $I$ be a set and $\alpha\in P_{j}I$. Now
$\Phi^{+}_{I}\Phi_{+}^{I}\alpha=j^{I}\alpha$. From the proof of the previous
proposition it easily follows that we have $j^{I}\alpha\vdash_{j}\alpha$. From
here we can conclude that $j^{I}\alpha$ and $\alpha$ are equivalent because
$\alpha\vdash j^{I}\alpha$ and $\alpha\vdash_{j}j^{I}\alpha$ are true in
virtue of $j^{I}$ being a nucleus.

Now let $\alpha\in P^{j}I$. Then $\Phi_{+}^{I}\Phi_{I}^{+}\alpha=j^{I}\alpha$,
but this is equivalent to $\alpha$ by definition of $P^{j}$. ∎

The following corollary will prove useful in the next section:

######  Corollary 6.7.

Suppose $j$ is a nucleus on an arrow algebra $A$ with the property that
$j^{2}=j$ as maps $A\to A$. Then the tripos $P_{j}$ and functor

$P^{j}:I\mapsto\\{\alpha\in PI\mid j^{I}\alpha=\alpha\\}$

are equivalent, making $P^{j}$ also a tripos.

###### Proof.

If $j^{2}=j$ then this tripos is equivalent to the one from the previous
propsition. ∎

######  Remark 6.8.

For future reference, it will be worthwhile to make explicit how the tripos
structure in $P^{j}$ is calculated.

  1. (1)

Implication and meets are calculated as in $P$; this follows from items (iii)
and (iv) of Lemma 3.13 and Lemma 6.4 respectively.

  2. (2)

The joins of $P^{j}$ are those of $P$ with $j$ applied to them. To see this,
suppose $\alpha,\beta,\gamma\in P^{j}I$. Note that $\alpha\vdash\alpha+\beta$
implies $j\alpha\vdash j(\alpha+\beta)$, which in combination with $\alpha\in
P^{j}$ gives $\alpha\vdash j(\alpha+\beta)$. (Similarly for $\beta$.)

Now suppose $\alpha\vdash\gamma$ and $\beta\vdash\gamma$. Then
$\alpha+\beta\vdash\gamma$ implies $j(\alpha+\beta)\vdash j\gamma$, which in
combination with $\gamma\in P^{j}$ implies $j(\alpha+\beta)\vdash\gamma$.

  3. (3)

Now we claim the universal adjoint can stay the same and the existential will
be the old one with $j$ applied to it.

To see this we note that if $\alpha\in P^{j}$, then:

$\begin{array}[]{lclc}f^{*}\forall_{f}\alpha\vdash\alpha&\Rightarrow&jf^{*}\forall_{f}\alpha\vdash
j\alpha&\Rightarrow\\\ f^{*}j\forall_{f}\alpha\vdash
j\alpha&\Rightarrow&f^{*}j\forall_{f}\alpha\vdash\alpha&\Rightarrow\\\
j\forall_{f}\alpha\vdash\forall_{f}\alpha\end{array}$

In addition, we have

$j\exists_{f}\alpha\vdash\beta\Rightarrow\exists_{f}\alpha\vdash\beta\Rightarrow\alpha\vdash
f^{*}\beta$

and

$\alpha\vdash f^{*}\beta\Rightarrow\exists_{f}\alpha\vdash\beta\Rightarrow
j\exists_{f}\alpha\vdash j\beta\Rightarrow j\exists_{f}\alpha\vdash\beta,$

if $\alpha,\beta\in P^{j}$.

  4. (4)

As a generic element we can take $j:A\to A\in PA$.

######  Remark 6.9.

The two equivalent approaches to the subtriposes induced by a nucleus
correspond to the two different ways of approaching the negative translation
(see [1]). The first one, which is we denoted with $P_{j}$, is most closely
associated to the Kuroda negative translation. On this approach we keep the
usual predicates and change the notion of consequence. The second one, which
is the one we denoted with $P_{j}$, is to keep the usual notion of
consequence, but restrict the predicates: this is most closely associated to
the Gödel-Gentzen negative translation. The second view is often more pleasant
to work with because implication and universal quantification remain the same.

##  7\. Applications

In this section we wish to illustrate the flexibility of the framework we have
created by showing how various modified realizability toposes fit within it.
Indeed, the power is that we can construct triposes without too much effort
(and without going through the laborious task of checking that they define
triposes). We will not further investigate the resulting toposes – this is a
task that we hope to be able to take up in future work.

###  7.1. The modification of an arrow algebra

Let us start by showing that arrow algebras are closed under another
construction provided they are _binary implicative_.

######  Definition 7.1.

Let $A$ be an arrow structure. We will call $A$ _binary implicative_ if

$a\to(b\curlywedge b^{\prime})=(a\to b)\curlywedge(a\to b^{\prime})$

for all $a,b,b^{\prime}\in A$. An arrow algebra will be called binary
implicative if its underlying arrow structure is.

Clearly, (quasi-)implicative algebras are also binary implicative.

######  Proposition 7.2.

(Sierpiński construction) Let $A$ be an binary implicative arrow algebra.
Define

$A^{\to}:=\\{x=(x_{0},x_{1})\in A^{2}\mid x_{0}\preccurlyeq x_{1}\\}$

If we order $A^{\to}$ pointwise, and define implication as

$x\to y:=(x_{0}\to y_{0}\curlywedge x_{1}\to y_{1},x_{1}\to y_{1})$

then $A^{\to}$ carries an arrow structure. Moreover,

$S^{\to}:=\\{x\in A^{\to}\mid x_{0}\in S\\}$

defines a separator on this arrow structure.

###### Proof.

Since the proof is lengthy and tedious, we have relegated it to an appendix. ∎

The following lemma follows directly from intuitionistic logic.

######  Lemma 7.3.

Let $A$ be an arrow algebra and $a\in A$. Then

$j:A\to A:x\mapsto x+a$

defines a nucleus.

######  Definition 7.4.

Let $A$ be a binary implicative arrow algebra and $j$ be the nucleus on
$A^{\to}$ defined by $j(x)=x+(\bot,\top)$. Then we will refer to

$A^{m}:=A^{\to}_{j}$

as the _modification of the arrow algebra $A$_.

###  7.2. Modified realizability

In its original incarnation, modified realizability was a proof-theoretic
interpretation. It was invented by Kreisel in 1959, who used it to show the
independence of Markov’s Principle over intuitionistic arithmetic in finite
types [10]. Later, based on ideas by Hyland and Troelstra, Grayson gave a
semantic counterpart to Kreisel’s interpretation and defined the modified
realizability tripos [5]. (Other references for modified realisability toposes
include [7, 13, 2, 9].) His definition was as follows; here we use that
$\mathbb{N}$ carries the structure of an absolute and discrete pca ($K_{1}$,
see Example 2.12).

######  Definition 7.5.

(Grayson’s modified realizability tripos) Write

$\Sigma_{M}:=\\{(A_{0},A_{1})\mid A_{0}\subseteq A_{1}\subseteq\mathbb{N},0\in
A_{1}\\}.$

Then we can define a functor

$M:\mathbf{Set}^{op}\to\mathbf{Preorder}$

which sends a set $I$ to the set of functions $I\to\Sigma_{M}$ preordered as
follows:

$\displaystyle\alpha\leq_{MI}\beta$ if $\displaystyle\exists
r\in\mathbb{N}\,\forall i\in I\,\big{(}\,\forall
n\in\alpha_{1}(i)\,\,rn\downarrow\text{ and }rn\in\beta_{1}(i)\,\big{)}$
$\displaystyle\text{ and }\big{(}\,\forall
n\in\alpha_{0}(i)\,rn\in\beta_{0}(i)\,\,\big{)}$

In addition, the functor $M$ acts on morphisms by precomposition.

The following proposition explains how this indexed preorder is related to the
modification of an arrow algebra. Indeed, recall that any pca induces an arrow
algebra (as in Theorem 3.9), so that we have an arrow algebra $D(K_{1})$. (In
fact, this arrow algebra is binary implicative, even quasi-implicative.) The
tripos induced by its modification is equivalent to $M$.

######  Proposition 7.6.

As an indexed preorder, Grayson’s modified realizability tripos is equivalent
to the tripos induced by the modification of the arrow algebra ${\rm
Pow}(K_{1})$. Hence Grayson’s modified realizability tripos is indeed a
tripos.

###### Proof.

Let $A={\rm Pow}(K_{1})$ be the arrow algebra induced by $K_{1}$, while $P$ is
the tripos induced by $A^{\to}$ and $P^{j}$ the subtripos of $P$ induced by
$jx=x+(\bot,\top)$, as explained in Proposition 6.6.

There is an obvious natural transformation $F_{I}:MI\to PI$ induced by the
inclusion $\Sigma_{M}\to{\rm Pow}(K_{1})^{\to}$. Indeed, its pointwise full
and faithful, because

$\displaystyle\alpha\leq_{MI}\beta$ $\displaystyle\Leftrightarrow$
$\displaystyle\bigcurlywedge_{i\in I}\alpha(i)\to\beta(i)\in S^{\to}$
$\displaystyle\Leftrightarrow$ $\displaystyle\alpha\vdash_{PI}\beta$

So it remains to show that the essential image of $F$ is precisely $P^{j}$.

For that purpose let us determine what it means for an element $\alpha\in PI$
to belong to $P^{j}I$. In order for $\alpha\in P^{j}I$ to hold, we must have

$\bigcurlywedge_{i\in I}(\alpha(i)+(\emptyset,\mathbb{N}))\to\alpha(i)\in
S^{\to},$

which by intuitionistic reasoning is equivalent to

$\bigcurlywedge_{i\in I}(\emptyset,\mathbb{N})\to\alpha(i)\in S^{\to}.$

Using the definition of $S^{\to}$, this is equivalent to

$\bigcap_{i\in I}\big{(}(\emptyset,\mathbb{N})\to\alpha(i)\big{)}_{0}\mbox{ is
inhabited.}$

Because
$((\emptyset,\mathbb{N})\to\alpha(i))_{0}=\emptyset\to\alpha_{0}(i)\cap\mathbb{N}\to\alpha_{1}(i)=\mathbb{N}\to\alpha_{1}(i)$,
this is equivalent to

$\bigcap_{i\in I}\mathbb{N}\to\alpha_{1}(i)\mbox{ is inhabited,}$

which in turn is equivalent to

$\bigcap_{i\in I}\alpha_{1}(i)\mbox{ is inhabited.}$

Since $0\in\bigcap_{i\in I}\alpha_{1}(i)$ for any element $\alpha\in M$, every
element in $M$ lands in $P^{j}$ under $F$. Conversely, suppose $\alpha\in
P^{j}I$ and let $a\in\bigcap_{i\in I}\alpha_{1}(i)$. Now define

$f:\mathbb{N}\to\mathbb{N}:x\mapsto\begin{cases}0&x=a\\\ a&x=0\\\
x&\text{else}\end{cases}$

By postcomposition with $f$ (on both components) we get $f\circ\alpha\in MI$.
Because $f$ is a recursive bijection we can code it as a natural number $e$.
With this we get

$e\in\bigcurlywedge_{i\in I}\alpha(i)\to f\circ\alpha(i)$

which implies $\alpha\vdash_{PI}f\circ\alpha$. Using the code of the inverse
of $f$, we can prove $f\circ\alpha\vdash_{PI}\alpha$. We conclude that $F:M\to
P^{j}$ is pointwise essentially surjective. ∎

######  Remark 7.7.

Note that we have constructed a natural transformation $F:M\to P^{j}$ which is
pointwise fully faithful and essentially surjective. In a constructive
metatheory this seems to be the best possible: we do not see how to prove the
existence of a pseudo-inverse without using the Axiom of Choice.

######  Remark 7.8.

This analysis of modified realizability is a variation on the observation in
[13] that the modified realizability topos is a closed subtopos of the
effective topos over Sierpiński space.

###  7.3. Extensional modified realizability topos

The modification construction can also be applied to ${\rm PER}(\mathbb{N})$,
the arrow algebra of PERs on the natural numbers, which is the result of
applying the construction from Subsection 3.2.3 on the absolute and discrete
pca $K_{1}$. Again, this arrow algebra is binary implicative (even quasi-
implicative).

######  Definition 7.9.

Let

$\Sigma_{T}:=\\{(R,S)\in\text{PER}(\mathbb{N})\mid R\subseteq S,(0,0)\in
S\\}.$

Then we can define a functor

$T:{\bf Sets}^{\rm op}\to{\bf Preorder}$

by putting $TI=\Sigma_{T}^{I}$ and

$\displaystyle\alpha\leq_{TI}\beta$ if $\displaystyle\exists
r\in\mathbb{N}\,\forall i\in
I\,\big{(}\,r\in\alpha_{0}(i)\to\beta_{0}(i)\cap\alpha_{1}(i)\to\beta_{1}(i)\,\big{)}$

for any $\alpha,\beta\in\Sigma^{X}$. Moreover, $T$ acts on morphisms by
precomposition.

######  Proposition 7.10.

The indexed preorder $T$ and the tripos induced by the modification of ${\rm
PER}(\mathbb{N})$ are equivalent as indexed preorders. Hence $T$ is also a
tripos.

###### Proof.

The proof is similar to that of Proposition 7.6. Write $A={\rm
PER}(\mathbb{N})$ and denote the tripos induced by $A^{\to}$ by $P$ and its
subtripos induced by the nucleus $j(x)=x+(\bot,\top)$, computed as in
Proposition 6.6, by $P^{j}$. There is again an obvious natural transformation
$F:T\to P$ induced by the inclusion $\Sigma_{T}\to{\rm
PER}(\mathbb{N})^{\to}$, which is pointwise full and faithful. To show that
its essential image is $P^{j}$, first note that in this case
$(\bot,\top)=(\emptyset,\mathbb{N}\times\mathbb{N})$. Then an element
$\alpha\in PI$ belongs to $P^{j}I$ precisely when

$\bigcap_{i\in I}\mathbb{N}\times\mathbb{N}\to\alpha_{1}(i)\mbox{ is
inhabited.}$

This shows the image of $F$ is included in $P^{j}$. Conversely, if
$(a,b)\in\bigcap_{i\in I}\alpha_{1}(i)$, then also

$(a,a)\in\bigcap_{i\in I}\alpha_{1}(i),$

because $\alpha_{1}(i)$ is symmetric and transitive. This means that if $f$ is
the recursive bijection from Proposition 7.6, then for

$\tilde{f}:\mathbb{N}^{2}\to\mathbb{N}^{2}:(x,y)\mapsto(fx,fy)$

we have $\tilde{f}\circ\alpha\in TI$ as well as both
$\alpha\vdash\tilde{f}\circ\alpha$ and $\tilde{f}\circ\alpha\vdash\alpha$. ∎

In his MSc thesis [17] (supervised by the first author), Mees de Vries defines
a subtripos of $T$. One of his results is that in the internal logic of the
resulting topos both the Axiom of Choice for all finite types as well as the
Independence of Premise principle hold. This can be seen as an improvement
over Grayson’s topos: indeed, these are characteristic principles of modified
realizability, but the Axiom of Choice for finite types fails in Grayson’s
topos.

The tripos studied by De Vries is constructed as follows.

######  Definition 7.11.

Write

$\Sigma_{V}:=\\{(A_{0},A_{1},\sim)\mid A_{0}\subseteq
A_{1}\subseteq\mathbb{N},0\in A_{1},\sim\text{an equivalence relation on
}A_{1}\\}.$

Then we can define functor

$V:{\bf Sets}^{\rm op}\to{\bf Preorder}$

by putting $VI=\Sigma^{I}$ and

$\displaystyle\alpha\leq_{VI}\beta$ if $\displaystyle\exists
r\in\mathbb{N}\,\forall i\in I\big{(}\,\forall
n\in\alpha_{1}(i)\,rn\downarrow\text{ and }rn\in\beta_{1}(i)\,\big{)}$
$\displaystyle\text{and }\big{(}\,\forall n,m\in\alpha_{1}(i)\,n\sim m\text{
implies }rn\sim rm\,\big{)}$ $\displaystyle\text{ and }\big{(}\,\forall
n\in\alpha_{0}(i)\,rn\in\beta_{0}(x)\,\big{)}$

for any $I\in\mathbf{Set}$ and $\alpha,\beta\in\Sigma^{I}$. Moreover, on
morphisms $V$ acts by precomposition.

To see how the tripos defined defined by De Vries fits into our framework, we
need to make two simple observations.

######  Lemma 7.12.

  1. (i)

If $j$ and $k$ are nuclei on an arrow algebra $A$, then so is $j\times
k:x\mapsto j(x)\times k(x)$.

  2. (ii)

If we take $A:={\rm PER}(\mathbb{N})$, then

$k:A^{\to}\to A^{\to}:(R,S)\mapsto(S\upharpoonright{\rm dom}\,R,S)$

defines a nucleus. Here ${\rm dom}(R)=\\{x\,:\,(x,x)\in R\\}$ and
$S\upharpoonright X=\\{(x,y)\in S\,:x,y\in X\\}$.

###### Proof.

The statement in (i) is an exercise is intuitionistic logic, while the main
difficulty in (ii) is to show that $k$ satisfies the the third requirement for
being a nucleus as the first two are trivial.

In our case

$\bigcurlywedge_{a,b\in A}(a\to kb)\to(ka\to kb)\in S$

translates to there being an element $(a,a^{\prime})$ such that for any
$(R,S),(T,U)\in{\rm PER}(\mathbb{N})^{\to}$ and any $(x,x^{\prime})\in(\,(R\to
U\upharpoonright\text{dom}(T)\,)\cap S\to U,S\to U)$, we have
$(ax,a^{\prime}x^{\prime})\in(\,(\,S\upharpoonright\text{dom}(R)\to
U\upharpoonright\text{dom}(T)\,)\cap S\to U,S\to U)$. We claim this element is
just the identity. As you can see this clearly works for the second
coordinate, so we only have to worry about the first.

For this, take $(x,x^{\prime})\in(\,R\to U\upharpoonright\text{dom}(T)\,)\cap
S\to U$ and $(s,s^{\prime})\in S\upharpoonright\text{dom}(R)$. If we get
$(xs,x^{\prime}s^{\prime})\in U\upharpoonright\text{dom}(T)$, we are done.
First of all note that because $(x,x^{\prime})\in S\to U$, we have
$(xs,x^{\prime}s^{\prime})\in U$ and it remains to show that
$xs,x^{\prime}s^{\prime}\in{\rm dom}(T)$. Because
$s,s^{\prime}\in\text{dom}(R)$, we have that $(s,s),(s^{\prime},s^{\prime})\in
R$ and therefore $(xs,x^{\prime}s),(xs^{\prime},x^{\prime}s^{\prime})\in
U\upharpoonright\text{dom}(T)$. Hence $xs,x^{\prime}s^{\prime}\in{\rm dom}(T)$
and we are done. ∎

######  Proposition 7.13.

Let $B$ be the arrow algebra obtained from ${\rm PER}(\mathbb{N})^{\to}$ by
considering the nucleus $j\times k$, where $(x)=x+(\bot,\top)$ and $k$ is the
nucleus from the previous lemma. Then the indexed preorder $V$ is equivalent
to the tripos induced by $B$. In particular, $V$ is a tripos.

###### Proof.

Let us write $P$ for the tripos induced by ${\rm PER}(\mathbb{N})^{\to}$ and
$P^{j\times k}$ for the subtripos induced by $j\times k$, computed as in
Proposition 6.6. Note that there is a map $\Sigma_{V}\to{\rm
PER}(\mathbb{N})^{\to}$ sending $(A_{0},A_{1},\sim)$ to $(\sim\upharpoonright
A_{0},\sim)$, which induces a natural transformation $F:V\to P$ by
postcomposition with this map. We can again easily verify that this
transformation is pointwise full and faithful, so it remains to show that its
pointwise essential image is $P^{j\times k}$. Note that an element $\alpha\in
PI$ belongs to $P^{j\times k}(I)$ precisely when $j\alpha\vdash\alpha$ and
$k\alpha\vdash\alpha$. By an argument similar to that in Proposition 7.10 we
can verify that any $\alpha$ such that $j\alpha\vdash\alpha$ is equivalent to
one with $0\in\bigcap_{i\in I}\alpha_{1}(i)$. And then an argument similar to
one in Corollary 6.7 shows that any such with $k\alpha\vdash\alpha$ is
equivalent to one with $\alpha=k\alpha$, because $k^{2}=k$. This shows that
any element in $P^{j\times k}I$ is isomorphic to one in the image of $FI$. ∎

######  Remark 7.14.

We suspect that also in the internal logic of the topos associated to $T$ the
characteristic principles of modified realizability hold (Axiom of Choice for
all finite types and Independence of Premise). We hope to investigate this
further in future work.

##  8\. Conclusion

We have introduced the notion of an arrow algebra and shown it is flexible
tool for constructing triposes. This is due to the fact that there are many
naturally occurring examples, such as locales and those induced by pcas, and
that the notion of an arrow algebra is closed under various constructions, in
particular a notion of a subalgebra given by nuclei and a Sierpiński
construction. This is also our reason for preferring arrow algebras over some
of their alternatives; let us discuss these now.

###  8.1. Related work

In the literature one can find a few other attempts to isolate a basic
structure which is sufficient for constructing a tripos. Among those we have
focused mostly on Miquel’s implicative algebras [11], because our notion of an
arrow algebra is a modification of his. Evidenced frames, as introduced by
Cohen, Miquey and Tate in [3], are closely related to implicative algebras. It
can be shown that every arrow algebra gives rise to an evidenced frame in such
a way that the induced triposes are equivalent (see Appendix B).

Another line of research focuses on _basic combinatory objects_ (BCOs), as
introduced in [6] (see also [15]). We do not see how arrow algebra can be
fitted into this approach: indeed, we do not see how to obtain a BCO from an
arrow algebra. Part of the problem is that we do not see how arrow algebras
can be equipped with an application operation turning them into pcas (if that
is possible at all).

###  8.2. Directions for future research

There are many possible directions for future research. We mention a few of
them.

Application and abstraction:

One of the main technical properties of arrow algebras is that it is still
possible to define a notion of application and abstraction (Definition 4.2 and
Definition 4.4, respectively) so that one could partly mimick the properties
of the $\lambda$-calculus, that is, up to a couple of $\partial$s. For
instance, we only have $(\lambda f)a\preccurlyeq\partial a$, as in Lemma 4.6.
The reason this is sufficient is essentially given by Lemma 4.20, which says
that $a$ and $\partial a$ are logically equivalent.

Another way of saying this is as follows. Let us call an element $a$ in an
arrow algebra $A$ _regular_ if

$a=\bigcurlywedge\\{c\to d\,:\,a\preccurlyeq c\to d\\}.$

Then implications are regular and regular elements are closed under arbitrary
infima (hence applications are regular). We do not have $(a\to b)a\preccurlyeq
b$ in general, but it is true if $b$ is regular (this follows from Lemma 4.3).
The reason for all the $\partial$s is that $\partial a$ is a regular element
which is logically equivalent to $a$.

We are not sure if we have found the nicest way of implementing application
and abstraction. One could argue that we could have saved a few $\partial$s if
we had defined

$\lambda f=\bigcurlywedge_{a\in A}a\to\overline{f(a)},$

where $\overline{b}=b$ if $b$ is regular and $\partial b$ otherwise. However,
we are not sure this would have made the theory nicer; in any case, we have
tried to avoid non-constructive case distinctions as much as possible. But
perhaps something better could be done instead.

Modified realizabily toposes:

We have used our machinery to construct a number of toposes for modified
realizability, and we think it would not be too difficult to find a few more.
We hope to further investigate this matters in future work.

Morphisms of arrow algebras:

A natural question that we have not explored at all is the following: what
would be a good notion of morphism of arrow algebras? In the setting of locale
theory there is a well-known notion of morphism of locales which corresponds
to the notion of geometric morphism between the corresponding toposes; there
is also work on morphisms of pcas and how these result to the geometric
morphisms between the induced toposes (see [18] for an overview; see also
[4]). It would be worthwhile to see if this work could be further generalised
to arrow algebras.

In short, we hope the arrow algebras provide an interesting and fruitful
avenue for further developing topos theory and its relation to logic.

## References

  * [1] B. van den Berg.  A Kuroda-style $j$-translation.  Arch. Math. Logic, 58(5-6):627–634, 2019.
  * [2] L. Birkedal and J. van Oosten.  Relative and modified relative realizability.  Ann. Pure Appl. Logic, 118(1-2):115–132, 2002.
  * [3] L. Cohen, E. Miquey, and R. Tate.  Evidenced frames: A unifying framework broadening realizability models.  In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1–13. IEEE, 2021.
  * [4] W. Ferrer Santos and O. Malherbe.  The category of implicative algebras and realizability.  Mathematical Structures in Computer Science, 29(10):1575–1606, 2019.
  * [5] R.J. Grayson.  Modified realisability toposes.  Handwritten notes from Münster University, 1981.
  * [6] P.J. W. Hofstra.  All realizability is relative.  Math. Proc. Cambridge Philos. Soc., 141(2):239–264, 2006.
  * [7] J. M. E. Hyland and C.-H. L. Ong.  Modified realizability toposes and strong normalization proofs (extended abstract).  In Typed lambda calculi and applications (Utrecht, 1993), volume 664 of Lecture Notes in Comput. Sci., pages 179–194. Springer, Berlin, 1993.
  * [8] J.M.E. Hyland, P.T. Johnstone, and A.M. Pitts.  Tripos theory.  Math. Proc. Cambridge Philos. Soc., 88(2):205–231, 1980.
  * [9] P.T. Johnstone.  Functoriality of modified realizability.  Tbilisi Math. J., 10(3):209–222, 2017.
  * [10] G. Kreisel.  Interpretation of analysis by means of constructive functionals of finite types.  In Constructivity in mathematics: Proceedings of the colloquium held at Amsterdam, 1957 (edited by A. Heyting), Studies in Logic and the Foundations of Mathematics, pages pp 101–128. North-Holland Publishing Co., Amsterdam, 1959.
  * [11] A. Miquel.  Implicative algebras: a new foundation for realizability and forcing.  Math. Struct. Comput. Sci., 30(5):458–510, 2020.
  * [12] A. Miquel.  Implicative algebras ii: Completeness w.r.t. set-based triposes.  arXiv:2011.09085, 2020.
  * [13] J. van Oosten.  The modified realizability topos.  J. Pure Appl. Algebra, 116(1-3):273–289, 1997.  Special volume on the occasion of the 60th birthday of Professor Peter J. Freyd.
  * [14] J. van Oosten.  Realizability: an introduction to its categorical side, volume 152 of Studies in Logic and the Foundations of Mathematics.  Elsevier B. V., Amsterdam, 2008.
  * [15] J. van Oosten and T. Zou.  Classical and relative realizability.  Theory Appl. Categ., 31:Paper No. 22, 571–593, 2016.
  * [16] M.H. Sørensen and P. Urzyczyn.  Lectures on the Curry-Howard isomorphism.  Elsevier, Amsterdam; Oxford, 2006.
  * [17] M. de Vries.  An extensional modified realizability topos.  Master’s thesis, University of Amsterdam, 2017.  Available from https://msclogic.illc.uva.nl/theses/archive/.
  * [18] J. Zoethout.  Computability models and realizability toposes.  PhD thesis, Utrecht University, 2022.  Available from https://dspace.library.uu.nl/handle/1874/416798.

##  Appendix A Sierpiński construction

This appendix is devoted to a proof of the following result.

######  Proposition A.1.

Let $A$ be a binary implicative arrow algebra. Define

$A^{\to}:=\\{x=(x_{0},x_{1})\in A^{2}\mid x_{0}\preccurlyeq x_{1}\\}$

If we order $A^{\to}$ pointwise, and define implication as

$x\to y:=(x_{0}\to y_{0}\curlywedge x_{1}\to y_{1},x_{1}\to y_{1}),$

then $A^{\to}$ carries an arrow structure. Moreover,

$S^{\to}:=\\{x\in A^{\to}\mid x_{0}\in S\\}$

defines a separator on this arrow structure.

###### Proof.

It is easy to see $A^{\to}$ is an arrow structure and that $S^{\to}$ is
upwards closed and closed under modus ponens. The difficulty is showing that
$S^{\to}$ contains the combinators ${\bf k}^{\to},{\bf s}^{\to}$ and ${\bf
a}^{\to}$.

For $\mathbf{k}^{\to}\in S^{\to}$ note that

$\displaystyle\mathbf{k}_{0}$ $\displaystyle=$
$\displaystyle\bigcurlywedge_{a,b}(a_{0}\to(b_{0}\to a_{0}\curlywedge b_{1}\to
a_{1}))\curlywedge a_{1}\to b_{1}\to a_{1}$ $\displaystyle\succcurlyeq$
$\displaystyle\bigcurlywedge_{a,b}a_{0}\to(b_{0}\to a_{0}\curlywedge b_{1}\to
a_{0})\curlywedge a_{1}\to b_{1}\to a_{1}$ $\displaystyle=$
$\displaystyle\bigcurlywedge_{a,b}a_{0}\to b_{1}\to a_{0}\curlywedge a_{1}\to
b_{1}\to a_{1}$ $\displaystyle\succcurlyeq$ $\displaystyle\mathbf{k}\in S$

For $\mathbf{s}^{\to}\in S^{\to}$ we give only a part of the proof to give an
idea.

$\displaystyle\mathbf{s}_{0}$ $\displaystyle=$
$\displaystyle\bigcurlywedge_{a,b,c}((a_{0}\to(b_{0}\to c_{0}\curlywedge
b_{1}\to c_{1}))\curlywedge a_{1}\to b_{1}\to c_{1})\to$
$\displaystyle(((a_{0}\to b_{0}\curlywedge a_{1}\to b_{1})\to(a_{0}\to
c_{0}\curlywedge a_{1}\to c_{1}))\curlywedge(a_{1}\to b_{1})\to a_{1}\to
c_{1})$ $\displaystyle\curlywedge(a_{1}\to b_{1}\to c_{1})\to(a_{1}\to
b_{1})\to a_{1}\to c_{1}$

We would like this to be greater than $\mathbf{s}\in S$. Note that the second
part, on the third line, is already in a nice form. So we will give a lower
bound for the first part. To do this we use that $A$ is binary implicative.

$\begin{array}[]{cl}&((a_{0}\to(b_{0}\to c_{0}\curlywedge b_{1}\to
c_{1}))\curlywedge a_{1}\to b_{1}\to c_{1})\to\\\ &((a_{0}\to b_{0}\curlywedge
a_{1}\to b_{1})\to(a_{0}\to c_{0}\curlywedge a_{1}\to
c_{1}))\curlywedge((a_{1}\to b_{1})\to a_{1}\to c_{1})\\\
\succcurlyeq&((a_{0}\to(b_{0}\to c_{0}\curlywedge b_{1}\to c_{1}))\curlywedge
a_{1}\to b_{1}\to c_{1})\to\\\ &((a_{0}\to b_{0}\curlywedge a_{1}\to
b_{1})\to(a_{0}\to c_{0}\curlywedge a_{1}\to c_{1}))\curlywedge\\\
&((a_{0}\to(b_{0}\to c_{0}\curlywedge b_{1}\to c_{1}))\curlywedge a_{1}\to
b_{1}\to c_{1})\to\\\ &((a_{1}\to b_{1})\to a_{1}\to c_{1})\end{array}$

We would also find a nicer lower bound for this. We only give a lower bound
for the second part, the proof for the first part using that $A$ is binary
implicative and a similar idea.

$\displaystyle((a_{0}\to(b_{0}\to c_{0}\curlywedge b_{1}\to c_{1}))\curlywedge
a_{1}\to b_{1}\to c_{1})\to((a_{1}\to b_{1})\to a_{1}\to c_{1})$
$\displaystyle\succcurlyeq$ $\displaystyle(a_{1}\to b_{1}\to
c_{1})\to(a_{1}\to b_{1})\to a_{1}\to c_{1}$

This is again in a nice form and can be bounded from below by $\mathbf{s}\in
S$.

To prove $\mathbf{a}\in S^{\to}$, note that

$\displaystyle\mathbf{a}_{0}$ $\displaystyle=$
$\displaystyle\big{(}\bigcurlywedge_{x,I,y_{i},z_{i}}\big{(}\bigcurlywedge_{i}x\to
y_{i}\to z_{i}\big{)}_{0}\to\big{(}x\to\bigcurlywedge_{i}y_{i}\to
z_{i}\big{)}_{0}\big{)}\curlywedge\mathbf{a}_{1}$

As $\mathbf{a}_{1}\succcurlyeq\mathbf{a}\in S$, it suffices to show

$\mathbf{a}\preccurlyeq\big{(}\bigcurlywedge_{x,y_{i},z_{i}}\big{(}\bigcurlywedge_{i}x\to
y_{i}\to z_{i}\big{)}_{0}\to\big{(}x\to\bigcurlywedge_{i}y_{i}\to
z_{i}\big{)}_{0}\big{)}$

So we calculate

$\begin{array}[]{cl}&\big{(}\bigcurlywedge_{i}x\to y_{i}\to
z_{i}\big{)}_{0}\to\big{(}x\to\bigcurlywedge_{i}y_{i}\to z_{i}\big{)}_{0}\\\
\\\ =&\big{(}\big{(}\bigcurlywedge_{i}x_{0}\to(y_{i0}\to z_{i0}\curlywedge
y_{i1}\to z_{i1})\big{)}\curlywedge\big{(}\bigcurlywedge_{i}x_{1}\to y_{i1}\to
z_{i1}\big{)}\big{)}\to\\\ \\\
&\big{(}\big{(}x_{0}\to\bigcurlywedge_{i}y_{i0}\to z_{i0}\curlywedge y_{i1}\to
z_{i1}\big{)}\curlywedge\big{(}x_{1}\to\bigcurlywedge_{i}y_{i1}\to
z_{i1}\big{)}\big{)}\\\ \\\
=&\Big{(}\big{(}\big{(}\bigcurlywedge_{i}x_{0}\to(y_{i0}\to z_{i0}\curlywedge
y_{i1}\to z_{i1})\big{)}\curlywedge\big{(}\bigcurlywedge_{i}x_{1}\to y_{i1}\to
z_{i1}\big{)}\big{)}\to\\\ &\big{(}x_{0}\to\bigcurlywedge_{i}y_{i0}\to
z_{i0}\curlywedge y_{i1}\to z_{i1}\big{)}\Big{)}\curlywedge\\\
&\Big{(}\big{(}\big{(}\bigcurlywedge_{i}x_{0}\to(y_{i0}\to z_{i0}\curlywedge
y_{i1}\to z_{i1})\big{)}\curlywedge\big{(}\bigcurlywedge_{i}x_{1}\to y_{i1}\to
z_{i1}\big{)}\big{)}\to\\\ &\big{(}x_{1}\to\bigcurlywedge_{i}y_{i1}\to
z_{i1}\big{)}\big{)}\Big{)}\end{array}$

Here the final equality follows from compatibility with joins. The second part
we can be bound from below by

$\mathbf{a}\preccurlyeq\big{(}\bigcurlywedge_{i}x_{1}\to y_{i1}\to
z_{i1}\big{)}\to x_{1}\to\bigcurlywedge_{i}y_{i1}\to z_{i1}$

So we only have to bound the first part from below by $\mathbf{a}$.

Let us begin:

$\begin{array}[]{cl}&\big{(}\big{(}\bigcurlywedge_{i}x_{0}\to(y_{i0}\to
z_{i0}\curlywedge y_{i1}\to
z_{i1})\big{)}\curlywedge\big{(}\bigcurlywedge_{i}x_{1}\to y_{i1}\to
z_{i1}\big{)}\big{)}\to\\\ \\\ &\big{(}x_{0}\to\bigcurlywedge_{i}y_{i0}\to
z_{i0}\curlywedge y_{i1}\to z_{i1}\big{)}\\\ \\\
\succcurlyeq&\big{(}\bigcurlywedge_{i}x_{0}\to(y_{i0}\to z_{i0}\curlywedge
y_{i1}\to z_{i1})\big{)}\to\big{(}x_{0}\to\bigcurlywedge_{i}y_{i0}\to
z_{i0}\curlywedge y_{i1}\to z_{i1}\big{)}\\\ \\\
=&\big{(}\bigcurlywedge_{i}x_{0}\to(y_{i0}\to z_{i0}\curlywedge y_{i1}\to
z_{i1})\big{)}\to\big{(}x_{0}\to\bigcurlywedge_{i}y_{i0}\to
z_{i0}\big{)}\curlywedge\\\ \\\ &\big{(}\bigcurlywedge_{i}x_{0}\to(y_{i0}\to
z_{i0}\curlywedge y_{i1}\to
z_{i1})\big{)}\to\big{(}x_{0}\to\bigcurlywedge_{i}y_{i1}\to z_{i1}\big{)}\\\
\\\ =&\Big{(}\big{(}\big{(}\bigcurlywedge_{i}x_{0}\to y_{i0}\to
z_{i0}\big{)}\curlywedge\big{(}\bigcurlywedge_{i}x_{0}\to y_{i1}\to
z_{i1}\big{)}\big{)}\to\big{(}x_{0}\to\bigcurlywedge_{i}y_{i0}\to
z_{i0}\big{)}\Big{)}\curlywedge\\\ \\\
&\Big{(}\big{(}\big{(}\bigcurlywedge_{i}x_{0}\to y_{i0}\to
z_{i0}\big{)}\curlywedge\big{(}\bigcurlywedge_{i}x_{0}\to y_{i1}\to
z_{i1}\big{)}\big{)}\to\big{(}x_{0}\to\bigcurlywedge_{i}y_{i1}\to
z_{i1}\big{)}\Big{)}\\\ \\\
\succcurlyeq&\Big{(}\big{(}\bigcurlywedge_{i}x_{0}\to y_{i0}\to
z_{i0}\big{)}\to x_{0}\to\bigcurlywedge_{i}y_{i0}\to
z_{i0}\Big{)}\curlywedge\\\ \\\ &\Big{(}\big{(}\bigcurlywedge_{i}x_{0}\to
y_{i1}\to z_{i1}\big{)}\to x_{0}\to\bigcurlywedge_{i}y_{i1}\to
z_{i1}\Big{)}\\\ \succcurlyeq&\mathbf{a}\end{array}$

Hence $\mathbf{a}_{0}\succcurlyeq\mathbf{a}\in S$, which means
$\mathbf{a}^{\to}\in S^{\to}$ as desired. ∎

##  Appendix B Evidenced frames from arrow algebras

In [3] the authors develop another method for constructing triposes based on
what they call _evidenced frames_. In this appendix we will show that any any
arrow algebra gives rise to an evidenced frame.

Let us start by recalling the notion of an evidenced frame from [3].

######  Definition B.1.

An _evidenced frame_ is a triple $(\Phi,E,\to)$, where $\Phi$ is a set of
propositions, $E$ is a collection of evidence, and
$\phi_{1}\xrightarrow{e}\phi_{2}$ is a ternary evidence relation on
$\Phi\times E\times\Phi$. This triple of sets is required to satisfy the
following conditions:

Reflexivity:

There exists evidence $e_{{\mathsf{id}}}\in E$ such that

$\forall\phi.\phi\xrightarrow{e_{{\mathsf{id}}}}\phi.$

Transitivity:

There exists an operator $;\in E\times E\to E$ such that

$\forall\phi_{1},\phi_{2},\phi_{3},e,e^{\prime}.\mbox{ if
}\phi_{1}\xrightarrow{e}\phi_{2}\mbox{ and
}\phi_{2}\xrightarrow{e^{\prime}}\phi_{3}\mbox{, then
}\phi_{1}\xrightarrow{e;e^{\prime}}\phi_{3}.$

Top:

There is a proposition $\top\in\Phi$ for which there is evidence $e_{\top}\in
E$ such that

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

Conjunction:

There are operators $\land:\Phi\times\Phi\to\Phi$ and operator $<,>\in E\times
E\to E$ as well as evidence $e_{\mathsf{fst}},e_{\mathsf{snd}}\in E$ such
that:

$\begin{array}[]{l}\forall\phi_{1},\phi_{2}.\phi_{1}\land\phi_{2}\xrightarrow{e_{\mathsf{fst}}}\phi_{1},\\\
\forall\phi_{1},\phi_{2}.\phi_{1}\land\phi_{2}\xrightarrow{e_{\mathsf{snd}}}\phi_{2},\\\
\forall\phi,\phi_{1},\phi_{2},e_{1},e_{2}.\mbox{ if
}\phi\xrightarrow{e_{1}}\phi_{1}\mbox{ and
}\phi\xrightarrow{e_{2}}\phi_{2}\mbox{, then
}\phi\xrightarrow{<e_{1},e_{2}>}\phi_{1}\land\phi_{2}.\end{array}$

Universal implication:

There are operators $\supset\in\Phi\times{\mathcal{P}}(\Phi)\to\Phi$, and
operator $\lambda\in E\to E$ as well as evidence $e_{\mathsf{eval}}\in E$ such
that:

$\begin{array}[]{l}\forall\phi_{1},\phi_{2},\vec{\phi}.\big{(}\,\forall\phi\in\vec{\phi}.\phi_{1}\land\phi_{2}\xrightarrow{e}\phi)\mbox{
implies }\phi_{1}\xrightarrow{\lambda_{e}}\phi_{2}\supset\vec{\phi},\\\
\forall\phi_{1},\vec{\phi},\phi\in\vec{\phi}.(\phi_{1}\supset\vec{\phi})\land\phi_{1}\xrightarrow{e_{\mathsf{eval}}}\phi.\end{array}$

######  Proposition B.2.

Let $(A,\preccurlyeq,\to,S)$ be an arrow algebra. Then $(A,S,\to)$ is an
evidenced frame with $a\to^{s}b$ if $s\preccurlyeq a\to\partial b$.

###### Proof.

Reflexivity:

This follows from the fact that ${\bf k}^{\prime}\in S$ (see Lemma 4.12).

Transitivity:

From Proposition 3.5 it follows that

${\bf m}=\bigcurlywedge_{\phi_{1},\phi_{2}\phi_{3}\in
A}(\phi_{1}\to\partial\phi_{2})\to(\phi_{2}\to\partial\phi_{3})\to(\phi_{1}\to\partial\phi_{3})\in
S.$

Therefore $e;e^{\prime}={\bf m}ee^{\prime}$ is as desired (using Lemma 4.3 and
Lemma 4.10).

Top and conjunction:

This follows from the proof of the cases for top and conjunction in
Proposition 5.1 with $\phi_{1}\land\phi_{2}=\phi_{1}\times\phi_{2}$ and
$<e_{1},e_{2}>=e_{1}\times e_{2}$.

Universal implication:

The easiest is to put

$\phi\supset\vec{\psi}:=\phi\to\bigcurlywedge_{\psi\in\vec{\psi}}\partial\psi.$

That this has the required properties follows from the proof of the case of
the implication in Proposition 5.1.

∎

It follows from Lemma 4.20 that the tripos induced by the evidenced frame (as
in [3, Definition V.4]) is equivalent to the one induced by the arrow algebra.