# Free constructions and coproducts of d-frames

Tomáš Jakl  Achim Jung

(April 7, 2017)

###### Abstract

A general theory of presentations for d-frames does not yet exist. We review
the difficulties and give sufficient conditions for when they can be overcome.
As an application we prove that the category of d-frames is closed under
coproducts.

##  1 Introduction

In his celebrated _Domain Theory in Logical Form_ [1], Abramsky describes a
flexible framework for connecting the denotational semantics of a programming
language with an algebraic presentation of a program logics. The denotational
spaces are spectral spaces and the algebras are distributive lattices; they
are connected via Stone duality [7].

The attempt to expand the scope of Abramsky’s work to cover probabilistic and
real-number computation led to the study of stably compact spaces and their
Stone duality. Later, it was shown that stably compact spaces have a very
natural bitopological description; they are exactly the compact regular
bitopological spaces (or _bispaces_ for short) [8, 11]. Moreover, the Stone-
type duality between bispaces and _d-frames_ given in [8] has a finitistic
description in the compact regular case, and so we can try to extend
Abramsky’s work to this setting.

Free constructions of distributive lattices are an essential tool of Domain
Theory in Logical Form and therefore a general theory of free constructions of
d-frames is highly desirable. Unfortunately, no such theory exists as of yet.
The difficulty lies in the mixed algebraic-relational nature of d-frames and
particularly in the axiom ($\mathsf{con}$-$\mathsf{tot}$). In the absence of a
general theory one can look at special instances of the problem where the
difficulties with ($\mathsf{con}$-$\mathsf{tot}$) can be controlled. This is
our approach in this paper.

The carrier of a d-frame is two-sorted, consisting of two standard frames
$L_{+}$ and $L_{-}$. We use the usual generator and relations machinery to
present them separately. The remaining parts of the structure, the consistency
and totality relations $\mathsf{con},\mathsf{tot}\subseteq
L_{+}\mathord{\times}L_{-}$ can be specified by generating relations
$\mathsf{con}_{1}$ and $\mathsf{tot}_{1}$, but it is not clear how to make
sure that ($\mathsf{con}$-$\mathsf{tot}$), the only axiom that bonds both
relations, will hold in the generated structure. Rather than solve this
general problem, we provide sufficient conditions which can be checked in an
early stage of the generating process (Section 4).

As an application, we prove that the category of d-frames is closed under
coproducts (Section 5). In forthcoming work, [5], we show that the same
techniques allow us to define the d-frame that corresponds to the _Vietoris
power space_ over a bispace. Together, this lays the foundation for the
extension of Abramsky’s program as explained above as well as four-valued
coalgebraic logic (inspired by [9, 10, 4]). We believe that our results are
interesting from a model-theoretic perspective as well, as they provide an
example of a free construction for a two-sorted algebraic-relational
structure. Although not completely general, our techniques hold promise for
extending many other frame-theoretic constructions to d-frames (for examples
see [6, 12, 13]).

##  2 Preliminaries

Frames are algebraic structures which capture the order-theoretic properties
of the lattice of open sets of a topological space. We say that a complete
lattice $(L;\,\bigvee,\wedge,0,1)$ is a _frame_ if it satisfies the following
infinitary distributivity law

  1. (Frm)

$b\wedge(\bigvee_{i}\,a_{i})=\bigvee_{i}\,(b\wedge a_{i})$.

The counterparts to continuous maps are the _frame homomorphisms_ which are
maps distributing over _all_ joins and _all finite_ meets.

A topological space $(X;\,\tau)$ gives rise to a frame: the lattice of its
open sets ordered by set inclusion
$\Omega(X)=(\tau;\,\bigcup,\cap;\,\emptyset,X)$ is a frame. Also, any
continuous map $f\colon X\to Y$ gives rise to a frame homomorphism
$\Omega(f)\colon\Omega(Y)\to\Omega(X)$ as $U\in\tau^{Y}\mapsto
f^{-1}[U]\in\tau^{X}$.

Following the example of frames we have d-frames as the algebraic counterparts
to bitopological spaces (or _bispaces_ , for short)111Bispaces are the
structures $(X;\,\tau_{+},\tau_{-})$ where $(X;\,\tau_{+})$ and $(X;\tau_{-})$
are topological spaces. A map between two bispaces $f\colon X\to Y$ is
_bicontinuous_ if both $f_{+}\colon(X;\,\tau_{+}^{X})\to(Y;\,\tau_{+}^{Y})$
and $f_{-}\colon(X;\,\tau_{-}^{X})\to(Y;\,\tau_{-}^{Y})$ (which are acting on
the underlying set $X$ the same way as $f$ does) are continuous.. Because
bispaces have two topologies, we expect to have two frames, $L_{+}$ and
$L_{-}$, as part of the structure of d-frames.

This alone has some consequences. We can recognise two orders in the product
$L_{+}\mathord{\times}L_{-}$; the first is the _information order_
$\sqsubseteq$ where, for $\alpha=(\alpha_{+},\alpha_{-})$ and
$\beta=(\beta_{+},\beta_{-})\in L_{+}\mathord{\times}L_{-}$,
$\alpha\sqsubseteq\beta$ iff $\alpha_{+}\leq\beta_{+}$ and
$\alpha_{-}\leq\beta_{-}$. The second is the _logical order_ $\leq$ where
$\alpha\leq\beta$ iff $\alpha_{+}\leq\beta_{+}$ and $\alpha_{-}\geq\beta_{-}$.
Both $(L_{+}\mathord{\times}L_{-};\sqsubseteq)$ and
$(L_{+}\mathord{\times}L_{-};\leq)$ are bounded distributive lattices with
meets and joins computed as follows

$\displaystyle\alpha\vee\beta=(\alpha_{+}\vee\beta_{+},\alpha_{-}\wedge\beta_{-}),$
$\displaystyle\qquad\alpha\sqcup\beta=(\alpha_{+}\vee\beta_{+},\alpha_{-}\vee\beta_{-}),$
$\displaystyle\alpha\wedge\beta=(\alpha_{+}\wedge\beta_{+},\alpha_{-}\vee\beta_{-}),$
$\displaystyle\qquad\alpha\sqcap\beta=(\alpha_{+}\wedge\beta_{+},\alpha_{-}\wedge\beta_{-}).$

The smallest and largest elements in the information order are $\bot=(0,0)$
and $\top=(1,1)$, and in the logical order $\text{\emph{ff}}=(0,1)$ and
$\text{\emph{t}}\mkern-3.0mu\text{\emph{t}}=(1,0)$, respectively.

With just two frames we would not be able to express many bitopological
properties. One can require $L_{+}$ and $L_{-}$ to be subframes of a bigger
frame representing the join of the two topologies as proposed by Banashewski
[3]. Or, following the second author and Moshier [8], we can require two
binary relations $\mathsf{con}$ and $\mathsf{tot}$ between the two frame
components where $(a,b)\in\mathsf{con}$ corresponds to $a$ being disjoint from
$b$, and $(a,b)\in\mathsf{tot}$ if $a$ and $b$ cover the whole space. Our work
takes the second approach.

Formally, then, a _d-frame_ is a structure
$\mathcal{L}=(L_{+},L_{-};\,\mathsf{con},\mathsf{tot})$ such that $L_{+}$ and
$L_{-}$ are frames and the binary _consistency_ $\mathsf{con}\subseteq
L_{+}\mathord{\times}L_{-}$ and _totality_ $\mathsf{tot}\subseteq
L_{+}\mathord{\times}L_{-}$ relations satisfy the following axioms, for all
$\alpha,\beta\in L_{+}\mathord{\times}L_{-}$:

  1. ($\mathsf{con}$–$\mathord{\downarrow}\mkern 1.0mu$)

$\alpha\in\mathsf{con}$ and
$\beta\sqsubseteq\alpha\implies\beta\in\mathsf{con}$,

  2. ($\mathsf{tot}$–$\mathord{\uparrow}\mkern 1.0mu$)

$\alpha\in\mathsf{tot}$ and
$\beta\sqsupseteq\alpha\implies\beta\in\mathsf{tot}$,

  3. ($\mathsf{con}$,$\mathsf{tot}$–$\text{\emph{t}}\mkern-3.0mu\text{\emph{t}},\text{\emph{ff}}$)

$\text{\emph{t}}\mkern-3.0mu\text{\emph{t}}\in\mathsf{con}$ and
$\text{\emph{t}}\mkern-3.0mu\text{\emph{t}}\in\mathsf{tot}$,
$\text{\emph{ff}}\in\mathsf{con}$ and $\text{\emph{ff}}\in\mathsf{tot}$,

  4. ($\mathsf{con}$–$\wedge,\vee$)

$\alpha,\beta\in\mathsf{con}\implies\alpha\vee\beta\in\mathsf{con}$ and
$\alpha\wedge\beta\in\mathsf{con}$,

  5. ($\mathsf{tot}$–$\wedge,\vee$)

$\alpha,\beta\in\mathsf{tot}\implies\alpha\vee\beta\in\mathsf{tot}$ and
$\alpha\wedge\beta\in\mathsf{tot}$,

  6. ($\mathsf{con}$–$\bigsqcup\\!{}^{\mathord{\uparrow}\mkern 1.0mu}$)

$A\subseteq\mathsf{con}$ and $A$ is $\sqsubseteq$-directed
$\implies\\!\mathop{\,\ThisStyle{\ensurestackMath{\bigsqcup\stackengine{-0pt}{\,}{\SavedStyle\\!^{\mathord{\uparrow}}}{O}{l}{F}{T}{S}}}\\!}A\in\mathsf{con}$,

  7. ($\mathsf{con}$–$\mathsf{tot}$)

$\alpha\in\mathsf{con},\beta\in\mathsf{tot}$ and $(\alpha_{+}=\beta_{+}$ or
$\alpha_{-}=\beta_{-})\implies\alpha\sqsubseteq\beta$.

Algebraically speaking, the 3rd–6th axioms say that
$(\mathsf{con};\wedge,\vee,\text{\emph{t}}\mkern-3.0mu\text{\emph{t}},\text{\emph{ff}})$
and
$(\mathsf{tot};\wedge,\vee,\text{\emph{t}}\mkern-3.0mu\text{\emph{t}},\text{\emph{ff}})$
are (bounded) distributive lattices and that $(\mathsf{con};\sqsubseteq)$ is a
DCPO. Directed suprema are computed pointwise, i.e. for a
$\sqsubseteq$-directed $A\subseteq\mathsf{con}$,
$\\!\mathop{\,\ThisStyle{\ensurestackMath{\bigsqcup\stackengine{-0pt}{\,}{\SavedStyle\\!^{\mathord{\uparrow}}}{O}{l}{F}{T}{S}}}\\!}A=(\\!\mathop{\,\ThisStyle{\ensurestackMath{\bigvee\stackengine{-0pt}{\,}{\SavedStyle\\!^{\mathord{\uparrow}}}{O}{l}{F}{T}{S}}}\\!}\
\\{\alpha_{+}:\alpha\in A\\},\
\\!\mathop{\,\ThisStyle{\ensurestackMath{\bigvee\stackengine{-0pt}{\,}{\SavedStyle\\!^{\mathord{\uparrow}}}{O}{l}{F}{T}{S}}}\\!}\
\\{\alpha_{-}:\alpha\in A\\})$.

A pair of frame homomorphisms $h=(h_{+}\colon L_{+}\to M_{+},h_{-}\colon
L_{-}\to M_{-})$ is a _d-frame homomorphism_
$h\colon\mathcal{L}\to\mathcal{M}$ if, for all
$\alpha\in\mathsf{con}^{\mathcal{L}}$,
$h(\alpha)=(h_{+}(\alpha_{+}),h_{-}(\alpha_{-}))\in\mathsf{con}^{\mathcal{M}}$
and, for all $\alpha\in\mathsf{tot}^{\mathcal{L}}$,
$h(\alpha)\in\mathsf{tot}^{\mathcal{M}}$.

Every bispace $X=(X;\,\tau_{+},\tau_{-})$ gives rise to a d-frame
$\Omega^{d}(X)=(\tau_{+},\tau_{-};\mathsf{con}^{X},\mathsf{tot}^{X})$ where
$(U_{+},U_{-})\in\mathsf{con}^{X}$ iff $U_{+}\cap U_{-}=\emptyset$ and
$(U_{+},U_{-})\in\mathsf{tot}^{X}$ iff $U_{+}\cup U_{-}=X$. Similarly, every
bicontinuous map $f\colon X\to Y$ gives rise to a d-frame homomorphism
$\Omega^{d}(f)=(\Omega(f_{+}),\Omega(f_{-}))\colon\Omega^{d}(Y)\to\Omega^{d}(X)$.

The ($\mathsf{con}$-$\mathsf{tot}$) axiom, while essential in the theory of
d-frames, is harder to guarantee in constructions. We therefore introduce the
auxiliary notion of a _pre-d-frame_ where all but the
($\mathsf{con}$-$\mathsf{tot}$) axiom of d-frames are required to hold.

######  Remark.

Often, when we quantify over elements or sets that appear in both plus and
minus forms we will use the symbol “$\pm$” to mean both of them. For example,
“$A_{\pm}$ has property X” means “$A_{+}$ and $A_{-}$ have property X”, or
“there exist elements $x_{\pm}\in L_{\pm}$” means “there exist elements
$x_{+}\in L_{+}$ and $x_{-}\in L_{-}$”.

Also, because of the symmetrical nature of d-frames, many proofs consist of
two identical arguments, one for the plus and and one for the minus side.
Instead, we give only one of the variants without even mentioning the other.

##  3 Presentations

###  3.1 Presentation of frames

Frames, like other algebraic structures, may be presented in terms of
generators and relations $\left<G|R\right>$. The resulting frame
$\mathbb{F}r\\!\left<G|R\right>$ is obtained as the quotient
$\mathbb{F}r\\!\left<G\right>\\!/_{\sim_{R}}$. Here,
$\mathbb{F}r\\!\left<G\right>$ represents the term algebra generated by the
set of generators $G$ which, because of the frame distributivity law, consists
of terms of the form: $\bigvee_{i}(\wedge_{j=1}^{n_{i}}\ g_{i,j})$. The
congruence $\sim_{R}$ is generated from a relation
$R\subseteq\mathbb{F}r\\!\left<G\right>\mathord{\times}\mathbb{F}r\\!\left<G\right>$
where each element of $R$ is thought of as an equation:

$\displaystyle\bigvee_{i}(\wedge_{j=1}^{n_{i}}\
g_{i,j})=\bigvee_{i^{\prime}}(\wedge_{j^{\prime}=1}^{n^{\prime}_{i^{\prime}}}\
g^{\prime}_{i^{\prime},j^{\prime}}).$ (1)

However, the structure of $\mathbb{F}r\\!\left<G\right>\\!/_{\sim_{R}}$ is not
transparent at all. Its elements are equivalence classes of infinitary terms
quotiented by $R$, which itself consists of “infinitary” equations. This is
addressed in the $\mathcal{C}$-ideal presentation of frames. We assume that
our generators form a meet-semilattice222We always assume that meet-
semilattices are closed under _all_ finite meets, i.e. they also contain the
top element. $B$ representing the terms $\wedge_{j=1}^{n}\ g_{j}$. Moreover,
we can restrict to equations in which the right-hand side consists of a single
finite meet of generators, i.e. an element of $B$. In the terminology of
$\mathcal{C}$-ideals, we have a set of cover relations $\mathcal{C}$ where a
_cover relation_ is any pair $U\dashv a$ such that $a\in B$ and
$U\subseteq\mathord{\downarrow}\mkern 1.0mua$ (to represent the equation
$\bigvee U=a$). If, moreover, $\mathcal{C}$ satisfies the stability condition

$U\dashv a\in\mathcal{C},\ b\leq a\implies\\{u\wedge b:u\in U\\}\dashv
b\in\mathcal{C}$

then we call $(B,\mathcal{C})$ a _frame presentation_.

The frame presented by $(B,\mathcal{C})$ has an explicit description as the
frame of all $\mathcal{C}$-ideals, denoted by
$\mathcal{C}\text{-}\mathtt{Idl}\\!\left(B\right)$, where $I\subseteq B$ is a
_$\mathcal{C}$ -ideal_ if it is a downset and

$U\dashv a\in\mathcal{C},\ U\subseteq I\implies a\in I$

Computing with $\mathcal{C}$-ideals is straightforward. The join of a set
$\\{I_{i}\\}_{i}$ of $\mathcal{C}$-ideal is computed as
$\mathcal{C}\text{-}\mathtt{Idl}\\!\left<\bigcup_{i}I_{i}\right>$ where, for
an $M\subseteq B$, $\mathcal{C}\text{-}\mathtt{Idl}\\!\left<M\right>$ is the
smallest $\mathcal{C}$-ideal containing $M$. The meets of $\mathcal{C}$-ideals
are just intersections: $\bigwedge_{i}I_{i}=\bigcap_{i}I_{i}$, [6, Proposition
II.2.11].

There is a map translating syntactic terms to their semantic interpretation as
$\mathcal{C}$-ideals with the following universal property:

######  Lemma 1 (Universality).

Let $(B,\mathcal{C})$ be a presentation of a frame. Then the map
$\llbracket-\rrbracket\colon
B\to\mathcal{C}\text{-}\mathtt{Idl}\\!\left(B\right)$ defined as
$b\mapsto\mathcal{C}\text{-}\mathtt{Idl}\\!\left<\\{b\\}\right>$ is a meet-
semilattice homomorphism that transforms covers into joins, i.e.
$\bigvee\\{\llbracket u\rrbracket:u\in U\\}=\llbracket a\rrbracket$ for every
$U\dashv a\in\mathcal{C}$.

Moreover, $\llbracket-\rrbracket$ is universal among all such maps. That is,
if $f\colon B\to L$ is a meet-semilattice homomorphisms that transform covers
in $\mathcal{C}$ into joins, where $L$ is a frame, then there exists a unique
frame homomorphism
$\overline{f}\colon\mathcal{C}\text{-}\mathtt{Idl}\\!\left(B\right)\to L$ such
that $f=\overline{f}\circ\llbracket-\rrbracket$.

######  Remark.

There are numerous ways of presenting frames, e.g. [13], [6], [2] or [12]. We
picked this one because it suits us better later on for the coproduct of
d-frames. For the actual definition of presentation of d-frames it should not
really matter as long as we have a universality property similar to the one in
Lemma 1.

###  3.2 Presentations of pre-d-frames

In this section we show that we can extend the classical theory to also
present a (pre-)d-frame $(L_{+},L_{-};\,\mathsf{con},\mathsf{tot})$. Let us
assume that
$L_{\pm}=\mathcal{C}_{\pm}\text{-}\mathtt{Idl}\\!\left(B_{\pm}\right)$, for
some frame presentations $(B_{\pm},\mathcal{C}_{\pm})$, as in the previous
section. We also have the translations $\llbracket-\rrbracket_{\pm}\colon
B_{\pm}\to L_{\pm}$ from syntax to semantics according to Lemma 1.

Any consistency relation $\mathsf{con}$ on $L_{+}\mathord{\times}L_{-}$ can be
specified via the generators: Let $\alpha\in\mathsf{con}$. Since the sets
$\llbracket B_{\pm}\rrbracket_{\pm}=\\{\llbracket b\rrbracket_{\pm}:b\in
B_{\pm}\\}$ generate the frames $L_{\pm}$,

$\alpha=(\bigvee_{i\in I_{+}}b^{i}_{+},\ \bigvee_{i\in
I_{-}}b^{i}_{-})\quad\text{for some }\\{b^{i}_{+}\\}_{i}\subseteq\llbracket
B_{+}\rrbracket_{+}\text{ and }\\{b^{i}_{-}\\}_{i}\subseteq\llbracket
B_{-}\rrbracket_{-}$

and, because $\mathsf{con}$ is downwards closed in the information order,
$\mathsf{con}$ must contain all the pairs $(b^{i}_{+},\ b^{i^{\prime}}_{-})$,
for $(i,i^{\prime})\in I_{+}\mathord{\times}I_{-}$. Moreover, the converse is
also true:

######  Lemma 2.

$(\bigvee_{i\in I_{+}}b^{i}_{+},\ \bigvee_{i\in
I_{-}}b^{i}_{-})\in\mathsf{con}\quad\text{iff}\quad(b^{i}_{+},\
b^{i^{\prime}}_{-})\in\mathsf{con}$, for all $(i,i^{\prime})\in
I_{+}\mathord{\times}I_{-}$

###### Proof.

Only the right-to-left implication remains to be proved. Assume that
$(b^{i}_{+},\ b^{i^{\prime}}_{-})\in\mathsf{con}$, for all $(i,i^{\prime})\in
I_{+}\mathord{\times}I_{-}$. Since $\mathsf{con}$ is $\wedge$-closed, for an
$i\in I_{+}$ and a finite $F_{-}\mathbin{\subseteq\\!^{\text{fin}}}I_{-}$,
$(b^{i}_{+},\,\bigvee_{i\in F_{-}}b^{i}_{-})\in\mathsf{con}$. Similarly, since
$\mathsf{con}$ is $\vee$-closed, for finite
$F_{-}\mathbin{\subseteq\\!^{\text{fin}}}I_{-}$ and
$F_{+}\mathbin{\subseteq\\!^{\text{fin}}}I_{+}$, $(\bigvee_{i\in
F_{+}}b^{i}_{+},\,\bigvee_{i\in F_{-}}b^{i}_{-})\in\mathsf{con}$. Notice that
the set $M=\\{(\bigvee_{i\in F_{+}}b^{i}_{+},\,\bigvee_{i\in
F_{-}}b^{i}_{-}):F_{+}\mathbin{\subseteq\\!^{\text{fin}}}I_{+}\text{ and
}F_{-}\mathbin{\subseteq\\!^{\text{fin}}}I_{-}\\}$ is directed and
$\\!\mathop{\,\ThisStyle{\ensurestackMath{\bigsqcup\stackengine{-0pt}{\,}{\SavedStyle\\!^{\mathord{\uparrow}}}{O}{l}{F}{T}{S}}}\\!}M=(\bigvee_{i\in
I_{+}}b^{i}_{+},\ \bigvee_{i^{\prime}\in I_{-}}b^{i^{\prime}}_{-})$. Moreover,
because $M\subseteq\mathsf{con}$ and $\mathsf{con}$ is closed under directed
suprema,
$\\!\mathop{\,\ThisStyle{\ensurestackMath{\bigsqcup\stackengine{-0pt}{\,}{\SavedStyle\\!^{\mathord{\uparrow}}}{O}{l}{F}{T}{S}}}\\!}M\in\mathsf{con}$.
∎

This means that we can specify $\mathsf{con}$ by a subset
$\mathsf{con}_{1}\subseteq B_{+}\mathord{\times}B_{-}$ such that
$\mathsf{con}=\mathtt{CON}\langle\llbracket\mathsf{con}_{1}\rrbracket\rangle$
where $\mathtt{CON}\langle\llbracket\mathsf{con}_{1}\rrbracket\rangle$ is _the
smallest consistency relation_ containing
$\llbracket\mathsf{con}_{1}\rrbracket=\\{(\llbracket\alpha_{+}\rrbracket_{+},\llbracket\alpha_{-}\rrbracket_{-}):\alpha\in\mathsf{con}_{1}\\}$.333Formally,
for an $R\subseteq L_{+}\mathord{\times}L_{-}$,  $\mathtt{CON}\langle
R\rangle=\bigcap\\{R^{\prime}\subseteq
L_{+}\mathord{\times}L_{-}~{}|~{}R\subseteq R^{\prime},R^{\prime}\text{ is
$\mathord{\downarrow}\mkern 1.0mu$-closed, closed under
$\wedge,\vee,\\!\mathop{\,\ThisStyle{\ensurestackMath{\bigsqcup\stackengine{-0pt}{\,}{\SavedStyle\\!^{\mathord{\uparrow}}}{O}{l}{F}{T}{S}}}\\!}$,
and $\text{\emph{ff}},\text{\emph{t}}\mkern-3.0mu\text{\emph{t}}\in
R^{\prime}$}\\}.$

In general, we cannot hope to do the same for $\mathsf{tot}$, i.e. find a
$\mathsf{tot}_{1}\subseteq B_{+}\mathord{\times}B_{-}$ such that
$\mathsf{tot}=\mathtt{TOT}\langle\llbracket\mathsf{tot}_{1}\rrbracket\rangle$
where $\mathtt{TOT}\langle\llbracket\mathsf{tot}_{1}\rrbracket\rangle$ is _the
smallest totality relation_ containing $\llbracket\mathsf{tot}_{1}\rrbracket$.
We would have to specify $\mathsf{tot}$ by a subset of
$\mathcal{P}(B_{+})\mathord{\times}\mathcal{P}(B_{-})$. However, the special
kind of presentations, when $\mathsf{tot}_{1}\subseteq
B_{+}\mathord{\times}B_{-}$, turns out to be sufficient for our purposes.

######  Definition.

A tuple
$(B_{+},B_{-};\,\mathcal{C}_{+},\mathcal{C}_{-};\,\mathsf{con}_{1},\mathsf{tot}_{1})$
is a _presentation of a pre-d-frame_ if

  1. (d-Pres-1)

$(B_{+},\mathcal{C}_{+})$ and $(B_{-},\mathcal{C}_{-})$ are presentations of
frames,

  2. (d-Pres-2)

$\mathsf{con}_{1}\subseteq B_{+}\mathord{\times}B_{-}$ and
$\mathsf{tot}_{1}\subseteq B_{+}\mathord{\times}B_{-}$.

The resulting pre-d-frame is obtained in two steps. First, we generate the
frames of $\mathcal{C}$-ideals
$\mathcal{C}_{\pm}\text{-}\mathtt{Idl}\\!\left(B_{\pm}\right)$ and then we
generate the consistency and totality relations from the embedded relations
$\llbracket\mathsf{con}_{1}\rrbracket,\llbracket\mathsf{tot}_{1}\rrbracket\subseteq\mathcal{C}_{+}\text{-}\mathtt{Idl}\\!\left(B_{+}\right)\\!\mathord{\times}\mathcal{C}_{-}\text{-}\mathtt{Idl}\\!\left(B_{-}\right)$.
We obtain the following pre-d-frame:

$(\mathcal{C}_{+}\text{-}\mathtt{Idl}\\!\left(B_{+}\right),\mathcal{C}_{-}\text{-}\mathtt{Idl}\\!\left(B_{-}\right);\
\mathtt{CON}\langle\llbracket\mathsf{con}_{1}\rrbracket\rangle,\mathtt{TOT}\langle\llbracket\mathsf{tot}_{1}\rrbracket\rangle)$

Similarly to its frame counterpart,
$\llbracket-\rrbracket\\!=\\!(\llbracket-\rrbracket_{+},\llbracket-\rrbracket_{-})$
has the following universal property.

######  Lemma 3 (Universality).

Let
$(B_{+},B_{-};\,\mathcal{C}_{+},\mathcal{C}_{-};\,\mathsf{con}_{1},\mathsf{tot}_{1})$
be a presentation of a pre-d-frame. Then,

$\llbracket-\rrbracket\colon(B_{+},B_{-};\,\mathsf{con}_{1},\mathsf{tot}_{1})\to(\mathcal{C}_{+}\text{-}\mathtt{Idl}\\!\left(B_{+}\right),\,\mathcal{C}_{-}\text{-}\mathtt{Idl}\\!\left(B_{-}\right);\;\mathtt{CON}\langle\llbracket\mathsf{con}_{1}\rrbracket\rangle,\mathtt{TOT}\langle\llbracket\mathsf{tot}_{1}\rrbracket\rangle),$

is presentation preserving, i.e. its components are meet-semilattice
homomorphisms that transform covers from $\mathcal{C}_{\pm}$ into joins and
together they preserve $\mathsf{con}_{1}$ and $\mathsf{tot}_{1}$.

Also, if $\mathcal{M}$ is a pre-d-frame and
$f=(f_{+},f_{-})\colon(B_{+},B_{-};\,\mathsf{con}_{1},\mathsf{tot}_{1})\to\mathcal{M}$
is a presentation-preserving pair of maps, then there is a unique d-frame
homomorphism

$\overline{f}\colon(\mathcal{C}_{+}\text{-}\mathtt{Idl}\\!\left(B_{+}\right),\,\mathcal{C}_{-}\text{-}\mathtt{Idl}\\!\left(B_{-}\right);\;\mathtt{CON}\langle\llbracket\mathsf{con}_{1}\rrbracket\rangle,\mathtt{TOT}\langle\llbracket\mathsf{tot}_{1}\rrbracket\rangle)\to\mathcal{M}$

such that $f=\overline{f}\circ\llbracket-\rrbracket$. Moreover, the components
of $\overline{f}$ are the unique frame homomorphisms that are guaranteed to
exist by Lemma 1.

##  4 Generating d-frames

So far we made no attempt in making sure that the axiom
($\mathsf{con}$-$\mathsf{tot}$) is satisfied in the generated pre-d-frame. Let
us fix a presentation
$(B_{+},B_{-};\,\mathcal{C}_{+},\mathcal{C}_{-};\,\mathsf{con}_{1},\mathsf{tot}_{1})$
for the rest of this section and, because both frame components stay intact
after we generate them, let us denote them by $L_{\pm}\overset{\text{\tiny
def}}{\equiv}\mathcal{C}_{\pm}\text{-}\mathtt{Idl}\\!\left(B_{\pm}\right)$.
Also, for brevity, we will identify $B_{\pm}$ with $\llbracket
B_{\pm}\rrbracket_{\pm}\subseteq L_{\pm}$ and, also, $\mathsf{con}_{1}$ and
$\mathsf{tot}_{1}$ with $\llbracket\mathsf{con}_{1}\rrbracket$ and
$\llbracket\mathsf{tot}_{1}\rrbracket\subseteq L_{+}\mathord{\times}L_{-}$,
respectively.

The question for this section is: Under which conditions for
$(B_{+},B_{-};\,\mathcal{C}_{+},\mathcal{C}_{-};\,\mathsf{con}_{1},\mathsf{tot}_{1})$
is the generated pre-d-frame

$(L_{+},L_{-};\,\mathtt{CON}\langle\mathsf{con}_{1}\rangle,\mathtt{TOT}\langle\mathsf{tot}_{1}\rangle)$

a d-frame? We solve this problem (partially) by showing that the following
conditions are sufficient (though not necessarily minimal):

  1. 1.

($\mathord{\downarrow}\mkern 1.0mu\mathsf{con}_{\wedge,\vee}$-ind±), from
Section 4.2, which will ensure that the structure of
$\mathtt{CON}\langle\mathsf{con}_{1}\rangle$ is “sufficiently simple”, and

  2. 2.

($\lambda^{4}_{\pm}$-$\mathsf{con}$-$\mathsf{tot}$), from Section 4.3, which
is just a simple instance of ($\mathsf{con}$-$\mathsf{tot}$).

###  4.1 The structure of $\mathtt{CON}\langle\mathsf{con}_{1}\rangle$ and
$\mathtt{TOT}\langle\mathsf{tot}_{1}\rangle$

Before we get to the two conditions, we show that the relations
$\mathtt{CON}\langle\mathsf{con}_{1}\rangle$ and
$\mathtt{TOT}\langle\mathsf{tot}_{1}\rangle$ can be generated more explicitly.
As in the HSP theorem from universal algebra, we can close $\mathsf{con}_{1}$
and $\mathsf{tot}_{1}$ under the operations they should be closed under (e.g.
$\wedge$, $\vee$, etc.) and, if we proceed in a certain order, we do not have
to repeat any of the steps.

Let $R\subseteq L_{+}\mathord{\times}L_{-}$ be a any relation. We say that $R$
is $\wedge$-closed (resp. $\vee$-closed), if for every $\alpha,\beta\in R$,
$\alpha\wedge\beta\in R$ (resp. $\alpha\vee\beta\in R$). By
$\mathord{\downarrow}\mkern 1.0muR$ denote the downwards closure of $R$ in the
$\sqsubseteq$-ordering, i.e. the relation $\\{\alpha\in
L_{+}\mathord{\times}L_{-}~{}|~{}\exists\beta\in R.\
\alpha\sqsubseteq\beta\\}$ and define $\mathord{\uparrow}\mkern 1.0muR$
similarly.

Finally, define $\mathcal{D}(R)\overset{\text{\tiny
def}}{\equiv}\\{\,\\!\mathop{\,\ThisStyle{\ensurestackMath{\bigsqcup\stackengine{-0pt}{\,}{\SavedStyle\\!^{\mathord{\uparrow}}}{O}{l}{F}{T}{S}}}\\!}A~{}|~{}A\mathbin{\subseteq\\!\\!{}^{\mathord{\uparrow}\mkern
1.0mu}}R\\}$.444$A\mathbin{\subseteq\\!\\!{}^{\mathord{\uparrow}\mkern
1.0mu}}R$ means that $A$ is a directed subset of $R$ in the
$\sqsubseteq$-order. Note that $\mathcal{D}(R)$ is only a _“one-step”_ closure
under joins of directed subsets in $\sqsubseteq$-order. $\mathcal{D}(R)$ might
still contain directed subsets which do not have suprema in $\mathcal{D}(R)$.
To close $R$ under all directed suprema, one would have to iterate this
process. However, as we will see later, there are natural conditions under
which only one application is enough.

######  Lemma 4.

Let $L_{+},L_{-}$ be two frames and let $R\subseteq
L_{+}\mathord{\times}L_{-}$ be a relation. Then:

  1. 1.

If $R$ is $(\wedge,\vee)$-closed then $\mathord{\downarrow}\mkern 1.0muR$ and
$\mathord{\uparrow}\mkern 1.0muR$ in $L_{+}\mathord{\times}L_{-}$ are also
$(\wedge,\vee)$-closed.

  2. 2.

If $R$ is $(\wedge,\vee)$-closed then the relation $\mathcal{D}(R)$ is still
$(\wedge,\vee)$-closed.

  3. 3.

If $R$ is downwards closed then the relation $\mathcal{D}(R)$ is still
downwards closed.

###### Proof.

For 1., let $\alpha,\beta\in\mathord{\downarrow}\mkern 1.0muR$. This means
that there are $\alpha^{\prime},\beta^{\prime}\in R$ such that
$\alpha\sqsubseteq\alpha^{\prime}$ and $\beta\sqsubseteq\beta^{\prime}$.
Observe that
$(\alpha\wedge\beta)_{+}=\alpha_{+}\wedge\beta_{+}\leq\alpha^{\prime}_{+}\wedge\beta^{\prime}_{+}=(\alpha^{\prime}\wedge\beta^{\prime})_{+}$
and similarly
$(\alpha\wedge\beta)_{-}\leq(\alpha^{\prime}\wedge\beta^{\prime})_{-}$.
Therefore, $\alpha\wedge\beta\sqsubseteq\alpha^{\prime}\wedge\beta^{\prime}\in
R$ and $\alpha\wedge\beta\in\mathord{\downarrow}\mkern 1.0muR$. Proving
closedness $\mathord{\downarrow}\mkern 1.0muR$ under $\vee$ is the same and
the same reasoning also applies to $\mathord{\uparrow}\mkern 1.0muR$. For 2.,
let $\alpha,\beta\in\mathcal{D}(R)$. From the definition
$\alpha=\bigsqcup\\!{}^{\mathord{\uparrow}\mkern 1.0mu}_{i}\alpha^{i}$ and
$\beta=\bigsqcup\\!{}^{\mathord{\uparrow}\mkern 1.0mu}_{j}\beta^{j}$ for some
$\alpha^{i}$’s and $\beta^{j}$’s from $R$. Let us calculate,

$\displaystyle\alpha\wedge\beta$
$\displaystyle=(\bigvee\\!{}^{\mathord{\uparrow}\mkern
1.0mu}_{i}\alpha^{i}_{+}\wedge\bigvee\\!{}^{\mathord{\uparrow}\mkern
1.0mu}_{j}\beta^{j}_{+},\bigvee\\!{}^{\mathord{\uparrow}\mkern
1.0mu}_{i}\alpha^{i}_{-}\vee\bigvee\\!{}^{\mathord{\uparrow}\mkern
1.0mu}_{j}\beta^{j}_{-})$
$\displaystyle=(\bigvee\\!{}^{\mathord{\uparrow}\mkern
1.0mu}_{i}\bigvee\\!{}^{\mathord{\uparrow}\mkern
1.0mu}_{j}(\alpha^{i}_{+}\wedge\beta^{j}_{+}),\bigvee\\!{}^{\mathord{\uparrow}\mkern
1.0mu}_{i}\bigvee\\!{}^{\mathord{\uparrow}\mkern
1.0mu}_{j}(\alpha^{i}_{-}\vee\beta^{j}_{-}))$
$\displaystyle=(\bigvee\\!{}^{\mathord{\uparrow}\mkern
1.0mu}_{i,j}(\alpha^{i}_{+}\wedge\beta^{j}_{+}),\bigvee\\!{}^{\mathord{\uparrow}\mkern
1.0mu}_{i,j}(\alpha^{i}_{-}\vee\beta^{j}_{-}))$

Notice that the set $\\{\alpha^{i}\wedge\beta^{j}:i\in I,j\in J\\}$ is
directed since $\\{\alpha^{i}\\}_{i}$ and $\\{\beta^{j}\\}_{j}$ are and,
moreover, $\alpha^{i}\wedge\beta^{j}\in R$ for all $i,j$ since $R$ is closed
under logical meets.

For 3., let $\beta\sqsubseteq\bigsqcup\\!{}^{\mathord{\uparrow}\mkern
1.0mu}_{i}\alpha_{i}$ where $\alpha_{i}$’s are from $R$. Then,
$\beta=\bigsqcup\\!{}^{\mathord{\uparrow}\mkern
1.0mu}_{i}(\beta\sqcap\alpha_{i})\in\mathcal{D}(R)$ because the set
$\\{\beta\sqcap\alpha_{i}\\}_{i}$ is a directed subset of $R$. ∎

Lemma 4 shows the order in which one can generate
$\mathtt{CON}\langle\mathsf{con}_{1}\rangle$ and
$\mathtt{TOT}\langle\mathsf{tot}_{1}\rangle$. Set $\mathsf{con}_{\wedge,\vee}$
to be the algebraic closure of $\mathsf{con}_{1}$ under all _finite_ logical
joins and meets in $L_{+}\mathord{\times}L_{-}$, and define
$\mathsf{tot}_{\wedge,\vee}$ correspondingly. Then we have:

######  Corollary 5.

$\mathtt{CON}\langle\mathsf{con}_{1}\rangle=\bigcup_{\iota\in\text{Ord}}\mathcal{D}^{\iota}(\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee})\quad\text{and}\quad\mathtt{TOT}\langle\mathsf{tot}_{1}\rangle=\mathord{\uparrow}\mkern
1.0mu\mathsf{tot}_{\wedge,\vee}$

where, for an ordinal $\iota$ and a limit ordinal $\lambda$,

$\mathcal{\mathcal{missing}}D^{0}(R)\overset{\text{\tiny def}}{\equiv}R,\quad
D^{\iota+1}(R)\overset{\text{\tiny
def}}{\equiv}\mathcal{D}(\mathcal{D}^{\iota}(R))\quad\text{and}\quad\mathcal{D}^{\lambda}(R)\overset{\text{\tiny
def}}{\equiv}\bigcup_{\iota<\lambda}\mathcal{D}^{\iota}(R)\;.$

###  4.2 When is one step enough?

Proving ($\mathsf{con}$-$\mathsf{tot}$) for
$\mathtt{CON}\langle\mathsf{con}_{1}\rangle$ and
$\mathtt{TOT}\langle\mathsf{tot}_{1}\rangle$ as it is, turned out to be too
hard and, unless the authors have missed something obvious, we need to assume
additional properties about the presentation. One of the reasons for the
difficulty is the fact that $\mathtt{CON}\langle\mathsf{con}_{1}\rangle$ is
computed as an iteration of $\mathcal{D}(-)$. In this subsection, we focus on
the question whether there are natural properties, for a relation $R\subseteq
L_{+}\mathord{\times}L_{-}$, which guarantee
$\mathcal{D}(\mathcal{D}(R))=\mathcal{D}(R)$.

At the moment, $R$ can be any relation on the frames but for the application
to presentations we would like to instantiate $R$ with
$\mathord{\downarrow}\mkern 1.0mu\mathsf{con}_{\wedge,\vee}$. Because of that
we will assume that $R$ is downwards closed in $\sqsubseteq$-order and that it
is closed under $\wedge$ and $\vee$.

We start with an important definition. Two sets $A_{+}\subseteq L_{+}$ and
$A_{-}\subseteq L_{-}$ are said to be _$R$ -independent_ if $\forall a_{+}\in
A_{+}$ and $\forall a_{-}\in A_{-}$, $(a_{+},a_{-})\in R$.

######  Observation 6.

For every $\alpha\in R$, the sets $\mathcal{B}_{+}(\alpha_{+})$ and
$\mathcal{B}_{-}(\alpha_{-})$ are $R$-independent where
$\mathcal{B}_{\pm}(\alpha_{\pm})\,\overset{\text{\tiny
def}}{\equiv}\,\mathord{\downarrow}\mkern 1.0mu\alpha_{\pm}\cap B_{\pm}$.

It turns out that $\mathcal{D}(R)$ can reformulated by using $R$-independent
sets. Let $\alpha\in\mathcal{D}(R)$. From the definition, there is some
directed $A\mathbin{\subseteq\\!\\!{}^{\mathord{\uparrow}\mkern 1.0mu}}R$ such
that
$\alpha=\\!\mathop{\,\ThisStyle{\ensurestackMath{\bigsqcup\stackengine{-0pt}{\,}{\SavedStyle\\!^{\mathord{\uparrow}}}{O}{l}{F}{T}{S}}}\\!}A$.
Because $\mathcal{B}_{\pm}(-)$ are monotone and $A$ is directed, the sets
$\\{\mathcal{B}_{+}(\alpha_{+}):\alpha\in A\\}$ and
$\\{\mathcal{B}_{-}(\alpha_{-}):\alpha\in A\\}$ are both also directed (in the
subset order) and so we have:

$\displaystyle\forall A\mathbin{\subseteq\\!\\!{}^{\mathord{\uparrow}\mkern
1.0mu}}R\implies\bigcup_{\alpha\in A}\mathcal{B}_{+}(\alpha_{+})\text{ and
}\bigcup_{\alpha\in A}\mathcal{B}_{-}(\alpha_{-})\text{ are $R$-independent}$
($\star$)

Moreover, because $L_{\pm}$ is generated by $B_{\pm}$ and every $x\in L_{\pm}$
is equal to $\bigvee\mathcal{B}_{\pm}(x)$, we obtain that
$\alpha=(\\!\mathop{\,\ThisStyle{\ensurestackMath{\bigvee\stackengine{-0pt}{\,}{\SavedStyle\\!^{\mathord{\uparrow}}}{O}{l}{F}{T}{S}}}\\!}_{\alpha\in
A}\alpha_{+},\\!\mathop{\,\ThisStyle{\ensurestackMath{\bigvee\stackengine{-0pt}{\,}{\SavedStyle\\!^{\mathord{\uparrow}}}{O}{l}{F}{T}{S}}}\\!}_{\alpha\in
A}\alpha_{-})=(\bigvee\mathcal{A}_{+},\bigvee\mathcal{A}_{-})$ where
$\mathcal{A}_{\pm}=\bigcup_{\alpha\in A}\mathcal{B}_{\pm}(\alpha_{\pm})$.

It might seem that $\mathcal{D}(-)$ is just a special case of a more general
construction:

$\mathcal{D}^{\text{ind}}(R)=\\{(\bigvee A_{+},\,\bigvee
A_{-})~{}|~{}A_{+}\subseteq B_{+},\,A_{-}\subseteq B_{-}\text{ s.t.\
}A_{+}\text{ and }A_{-}\text{ are $R$-independent}\\}$

What we have proved in the previous paragraphs is that
$\mathcal{D}(R)\subseteq\mathcal{D}^{\text{ind}}(R)$. In fact, both closures
are equivalent:

######  Lemma 7.

$\mathcal{D}(R)=\mathcal{D}^{\text{ind}}(R)$

###### Proof.

Only the right-to-left inclusion remains to be proved. Let $A_{+}\subseteq
B_{+}$ and $A_{-}\subseteq B_{-}$ be $R$-independent. Observe that for two
finite sets $F_{+}\mathbin{\subseteq\\!^{\text{fin}}}A_{+}$ and
$F_{-}\mathbin{\subseteq\\!^{\text{fin}}}A_{-}$, $(\bigvee F_{+},\bigvee
F_{-})\in R$. This is because R is $\vee$-closed and so $(\bigvee
F_{+},f_{-})\in R$ for every $f_{-}\in F_{-}$ and, because R is
$\wedge$-closed, $(\bigvee F_{+},\bigvee F_{-})\in R$. Clearly, the set
$\mathcal{A}=\\{(\bigvee F_{+},\bigvee
F_{-}):F_{+}\mathbin{\subseteq\\!^{\text{fin}}}A_{+}\text{ and
}F_{-}\mathbin{\subseteq\\!^{\text{fin}}}A_{-}\\}$ is a directed subset of $R$
and $(\bigvee A_{+},\bigvee
A_{-})=\\!\mathop{\,\ThisStyle{\ensurestackMath{\bigsqcup\stackengine{-0pt}{\,}{\SavedStyle\\!^{\mathord{\uparrow}}}{O}{l}{F}{T}{S}}}\\!}\mathcal{A}\in\mathcal{D}(R)$.
∎

Because $\mathcal{D}(R)$ is also downwards closed and closed under $\wedge$
and $\vee$ (Lemma 4),
$\mathcal{D}(\mathcal{D}(R))=\mathcal{D}^{\text{ind}}(\mathcal{D}^{\text{ind}}(R))$
and it might seem that this is already equal to $\mathcal{D}^{\text{ind}}(R)$.
But, this is not true in general. Take, for example,
$\mathcal{A}_{+}=\\{a_{+}\\}$ and $\mathcal{A}_{-}=\\{a^{1}_{-},a^{2}_{-}\\}$
which are $\mathcal{D}^{\text{ind}}(R)$-independent. Each of
$(a_{+},a^{1}_{-})$ and $(a_{+},a^{2}_{-})\in\mathcal{D}^{\text{ind}}(R)$ is
witnessed by a pair of $R$-independent sets $A^{1}_{+}$ and $A^{1}_{-}$, and
$A^{2}_{+}$ and $A^{2}_{-}$, respectively, such that $a_{+}=\bigvee
A^{1}_{+}=\bigvee A^{2}_{+}$ and $a^{1}_{-}=\bigvee A^{1}_{-}$ and
$a^{2}_{-}=\bigvee A^{2}_{-}$. However, because there is no reason to believe
that $A^{1}_{+}$ and $A^{2}_{+}$ are equal, there are no obvious candidates
for $R$-independent sets which would have $(a_{+},a^{1}_{-}\vee a^{2}_{-})$ as
their supremum. To overcome this problem, we assume the following condition:

  1. ($R$-ind)

For all $\forall\alpha\in\mathcal{D}^{\text{ind}}(R)$,
$\mathcal{B}_{+}(\alpha_{+})$ and $\mathcal{B}_{-}(\alpha_{-})$ are
$R$-independent.

This guarantees, for every $\alpha\in\mathcal{D}^{\text{ind}}(R)$, a canonical
choice of $R$-independent sets, namely
$A_{\pm}=\mathcal{B}_{\pm}(\alpha_{\pm})$.

######  Lemma 8.

$\mathcal{D}(\mathcal{D}^{\text{ind}}(R))\subseteq\mathcal{D}^{\text{ind}}(R)$

###### Proof.

Let $A\mathbin{\subseteq\\!\\!{}^{\mathord{\uparrow}\mkern
1.0mu}}\mathcal{D}^{\text{ind}}(R)$. By ($R$-ind), for every $\alpha\in A$,
$\mathcal{B}_{+}(\alpha_{+})$ and $\mathcal{B}_{-}(\alpha_{-})$ are
$R$-independent. As in ($\star$ ‣ 4.2), because $A$ is directed, the sets
$\mathcal{A}_{+}\overset{\text{\tiny
def}}{\equiv}\\!\mathop{\,\ThisStyle{\ensurestackMath{\bigcup\stackengine{-0pt}{\,}{\SavedStyle\\!^{\mathord{\uparrow}}}{O}{l}{F}{T}{S}}}\\!}_{\alpha\in
A}\mathcal{B}_{+}(\alpha_{+})$ and $\mathcal{A}_{-}\overset{\text{\tiny
def}}{\equiv}\\!\mathop{\,\ThisStyle{\ensurestackMath{\bigcup\stackengine{-0pt}{\,}{\SavedStyle\\!^{\mathord{\uparrow}}}{O}{l}{F}{T}{S}}}\\!}_{\alpha\in
A}\mathcal{B}_{+}(\alpha_{+})$ are $R$-independent and
$\\!\mathop{\,\ThisStyle{\ensurestackMath{\bigsqcup\stackengine{-0pt}{\,}{\SavedStyle\\!^{\mathord{\uparrow}}}{O}{l}{F}{T}{S}}}\\!}A=(\bigvee\mathcal{A}_{+},\bigvee\mathcal{A}_{-})$.
Hence,
$\\!\mathop{\,\ThisStyle{\ensurestackMath{\bigsqcup\stackengine{-0pt}{\,}{\SavedStyle\\!^{\mathord{\uparrow}}}{O}{l}{F}{T}{S}}}\\!}A\in\mathcal{D}^{\text{ind}}(R)$.
∎

A combination of the preceding lemmas yields the desired result:

######  Theorem 9.

Let $R\subseteq L_{+}\mathord{\times}L_{-}$ be downwards closed, closed under
logical meets and joins. If ($R$-ind) is true for $R$, then
$\mathcal{D}(\mathcal{D}(R))=\mathcal{D}(R).$

###### Proof.

$\mathcal{D}(\mathcal{D}(R))\overset{(Lemma~{}\ref{l:d-equals-
db})}{=}\mathcal{D}(\mathcal{D}^{\text{ind}}(R))\overset{(Lemma~{}\ref{l:reduce-
dirjoin})}{\subseteq}\mathcal{D}^{\text{ind}}(R)\overset{(Lemma~{}\ref{l:d-equals-
db})}{=}\mathcal{D}(R)\ \subseteq\ \mathcal{D}(\mathcal{D}(R))\qed$

######  Remark.

Because $\mathcal{D}(R)=\mathcal{D}^{\text{ind}}(R)$ is downwards closed, for
every $\alpha\in\mathcal{D}(R)$ and every
$(b_{+},b_{-})\in\mathcal{B}_{+}(\alpha_{+})\mathord{\times}\mathcal{B}_{-}(\alpha_{-})$,
also $(b_{+},b_{-})\in\mathcal{D}(R)$. Therefore, ($R$-ind) can be
reformulated in the following more compact way:

  1. ($R$-ind)

$(B_{+}\mathord{\times}B_{-})\cap\mathcal{D}(R)\subseteq R$

###  4.3 Chasing down ($\mathsf{con}$-$\mathsf{tot}$)

Finally, we can focus on the original ($\mathsf{con}$-$\mathsf{tot}$) axiom
for
$(L_{+},L_{-};\,\mathtt{CON}\langle\mathsf{con}_{1}\rangle,\mathtt{TOT}\langle\mathsf{tot}_{1}\rangle)$.
We split it into two parts:

  1. ($\lambda^{0}_{+}$-$\mathsf{con}$-$\mathsf{tot}$)

$\alpha\in\mathtt{CON}\langle\mathsf{con}_{1}\rangle$,
$\beta\in\mathtt{TOT}\langle\mathsf{tot}_{1}\rangle$ and
$\alpha_{+}=\beta_{+}\implies\alpha_{-}\leq\beta_{-}$

  2. ($\lambda^{0}_{-}$-$\mathsf{con}$-$\mathsf{tot}$)

$\alpha\in\mathtt{CON}\langle\mathsf{con}_{1}\rangle$,
$\beta\in\mathtt{TOT}\langle\mathsf{tot}_{1}\rangle$ and
$\alpha_{-}=\beta_{-}\implies\alpha_{+}\leq\beta_{+}$

If we assume ($R$-ind) about $\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee}$, then the conditions of Theorem 9 hold for
$R=\mathord{\downarrow}\mkern 1.0mu\mathsf{con}_{\wedge,\vee}$ and we can
rewrite ($\lambda^{0}_{\pm}$-$\mathsf{con}$-$\mathsf{tot}$) into the following
more explicit form

  1. ($\lambda^{0}_{+}$-$\mathsf{con}$-$\mathsf{tot}$)

$\alpha\in\mathcal{D}(\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee})$, $\beta\in\mathord{\uparrow}\mkern
1.0mu\mathsf{tot}_{\wedge,\vee}$ and
$\alpha_{+}=\beta_{+}\implies\alpha_{-}\leq\beta_{-}$

  2. ($\lambda^{0}_{-}$-$\mathsf{con}$-$\mathsf{tot}$)

$\alpha\in\mathcal{D}(\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee})$, $\beta\in\mathord{\uparrow}\mkern
1.0mu\mathsf{tot}_{\wedge,\vee}$ and
$\alpha_{-}=\beta_{-}\implies\alpha_{+}\leq\beta_{+}$

Our aim now is to restrict $\alpha$ and $\beta$ to smaller and smaller sets.
First, we restate the axioms such that the $\beta$’s come from
$\mathsf{tot}_{\wedge,\vee}$ and then from $\mathsf{tot}_{\wedge}$ (resp.
$\mathsf{tot}_{\vee}$). Then, we do the same with $\alpha$ until we obtain a
version of the ($\mathsf{con}$-$\mathsf{tot}$) axiom stated purely in terms of
formulas involving only elements from $\mathsf{con}_{\wedge,\bigvee}$ (resp.
$\mathsf{con}_{\vee,\bigwedge}$) and $\mathsf{tot}_{\wedge}$ (resp.
$\mathsf{tot}_{\vee}$). The individual stages are depicted in the diagram
below (the $\lambda$ superscripts in the axiom name correspond to the stages
as shown in the diagram):

${\mathcal{D}(\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee})}$${\mathord{\uparrow}\mkern
1.0mu\mathsf{tot}_{\wedge,\vee}}$${\mathsf{con}_{\wedge,\vee,\bigvee}/\mathsf{con}_{\wedge,\vee,\bigwedge}}$${\mathsf{tot}_{\wedge,\vee}}$${\mathsf{con}_{\wedge,\bigvee}/\mathsf{con}_{\vee,\bigwedge}}$${\mathsf{tot}_{\wedge}/\mathsf{tot}_{\vee}}$$\scriptstyle{0th}$$\scriptstyle{1st}$$\scriptstyle{2nd}$$\scriptstyle{3rd}$$\scriptstyle{4th}$

In every stage we introduce a pair of axioms (named
($\lambda^{i}_{\pm}$-$\mathsf{con}$-$\mathsf{tot}$), for $i=1,\dots,4$) and
show that they imply the previous axioms. Because the axioms
($\lambda^{i}_{+}$-$\mathsf{con}$-$\mathsf{tot}$) and
($\lambda^{i}_{-}$-$\mathsf{con}$-$\mathsf{tot}$) are dual to each other, we
will always only prove that, say,
($\lambda^{i}_{+}$-$\mathsf{con}$-$\mathsf{tot}$) implies
($\lambda^{i-1}_{+}$-$\mathsf{con}$-$\mathsf{tot}$) and leave out that
($\lambda^{i}_{-}$-$\mathsf{con}$-$\mathsf{tot}$) implies
($\lambda^{i-1}_{-}$-$\mathsf{con}$-$\mathsf{tot}$) as it is proved dually.

######  Remark.

Above we use a notation similar to the one introduced earlier. The relation
$\mathsf{con}_{\vee}$ is the algebraic closure of $\mathsf{con}_{1}$ under all
_finite_ logical joins ($\vee$) in $L_{+}\mathord{\times}L_{-}$, and
$\mathsf{con}_{\wedge}$, $\mathsf{tot}_{\vee}$, $\mathsf{tot}_{\wedge}$,
$\mathsf{tot}_{\wedge,\vee}$ and $\mathsf{con}_{\wedge,\vee}$ are defined
correspondingly. Likewise, $\mathsf{con}_{\wedge,\bigvee}$ is the closure of
$\mathsf{con}_{1}$ under finite meets followed by the closure under all joins,
both in logical order555This makes sense because, in any d-frame
$(L_{+},L_{-};\,\mathsf{con},\mathsf{tot})$, $\\{(\bigvee_{i}\alpha^{i}_{+},\
\bigwedge_{i}\alpha^{i}_{-}):\\{\alpha^{i}\\}_{i}\subseteq\mathsf{con}\\}\subseteq\mathsf{con}$.
Indeed, from ($\mathsf{con}$–$\mathord{\downarrow}\mkern 1.0mu$), all
$(\alpha^{i}_{+},\ \bigwedge_{i}\alpha^{i}_{-})\in\mathsf{con}$ and, by $\vee$
and
$\\!\mathop{\,\ThisStyle{\ensurestackMath{\bigsqcup\stackengine{-0pt}{\,}{\SavedStyle\\!^{\mathord{\uparrow}}}{O}{l}{F}{T}{S}}}\\!}$-closedness,
$(\bigvee_{i}\alpha^{i}_{+},\ \bigwedge_{i}\alpha^{i}_{-})\in\mathsf{con}$. ,
i.e.

$\mathsf{con}_{\wedge,\bigvee}=\\{(\bigvee_{i}\alpha^{i}_{+},\
\bigwedge_{i}\alpha^{i}_{-}):\\{\alpha^{i}\\}_{i}\subseteq\mathsf{con}_{\wedge}\\}.$

The other versions, such as $\mathsf{con}_{\vee,\bigwedge}$,
$\mathsf{con}_{\wedge,\vee,\bigvee}$ and
$\mathsf{con}_{\wedge,\vee,\bigwedge}$, are defined correspondingly.

#### 1st stage.

We intend to simplify the elements in the $\mathsf{tot}$ relation. Consider
the following axioms:

  1. ($\lambda^{1}_{+}$-$\mathsf{con}$-$\mathsf{tot}$)

$\alpha\in\mathcal{D}(\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee}),\
{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\dbox{\normalcolor$\beta\in\mathsf{tot}_{\wedge,\vee}$}},\
\beta_{+}\leq\alpha_{+}\implies\alpha_{-}\leq\beta_{-}$

  2. ($\lambda^{1}_{-}$-$\mathsf{con}$-$\mathsf{tot}$)

$\alpha\in\mathcal{D}(\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee}),\
{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\dbox{\normalcolor$\beta\in\mathsf{tot}_{\wedge,\vee}$}},\
\beta_{-}\leq\alpha_{-}\implies\alpha_{+}\leq\beta_{+}$

Now, let $\alpha\in\mathcal{D}(\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee})$ and let
$\beta\in\mathtt{TOT}\langle\mathsf{tot}_{1}\rangle$ with
$\alpha_{+}=\beta_{+}$. That means that there is some
$\beta^{\prime}\in\mathsf{tot}_{\wedge,\vee}$ such that
$\beta^{\prime}\sqsubseteq\beta$. We have that
$\beta^{\prime}_{+}\leq\alpha_{+}$ and so we can now apply
($\lambda^{1}_{+}$-$\mathsf{con}$-$\mathsf{tot}$) and get that
$\alpha_{-}\leq\beta^{\prime}_{-}$ and so
$\alpha_{-}\leq\beta^{\prime}_{-}\leq\beta_{-}$. To sum up, we have proved the
first part of:

######  Lemma 10.

($\lambda^{1}_{\pm}$-$\mathsf{con}$-$\mathsf{tot}$) implies
($\lambda^{0}_{\pm}$-$\mathsf{con}$-$\mathsf{tot}$), and vice versa.

For the converse assume $\beta_{+}\leq\alpha_{+}$. Then the pair
$(\alpha_{+},\beta_{-})$ belongs to $\mathord{\uparrow}\mkern
1.0mu\mathsf{tot}_{\wedge,\vee}$ and by
($\lambda^{0}_{\pm}$-$\mathsf{con}$-$\mathsf{tot}$) we can conclude
$\alpha_{-}\leq\beta_{-}$.

#### 2nd stage.

We can simplify the elements in $\mathsf{tot}$ even further. Take the axioms:

  1. ($\lambda^{2}_{+}$-$\mathsf{con}$-$\mathsf{tot}$)

$\alpha\in\mathcal{D}(\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee}),\
{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\dbox{\normalcolor$\beta\in\mathsf{tot}_{\wedge}$}},\
\beta_{+}\leq\alpha_{+}\implies\alpha_{-}\leq\beta_{-}$

  2. ($\lambda^{2}_{-}$-$\mathsf{con}$-$\mathsf{tot}$)

$\alpha\in\mathcal{D}(\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee}),\
{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\dbox{\normalcolor$\beta\in\mathsf{tot}_{\vee}$}},\
\beta_{-}\leq\alpha_{-}\implies\alpha_{+}\leq\beta_{+}$

Let $\alpha\in\mathcal{D}(\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee})$ and let $\beta\in\mathsf{tot}_{\wedge,\vee}$
with $\alpha_{+}\leq\beta_{+}$. We can decompose $\beta$ such that
$\beta=\bigvee_{k=1}^{n}\beta^{k}$ where $\beta^{k}\in\mathsf{tot}_{\wedge}$,
for every $k=1,\dots,n$. Then, for every $k$, we have that
$\beta^{k}_{+}\leq\beta_{+}\leq\alpha$ and so $\alpha_{-}\leq\beta^{k}_{-}$.
Because $\alpha_{-}\leq\beta^{k}_{-}$ for every $k$, also
$\alpha_{-}\leq\beta_{-}=\bigwedge_{k=1}^{n}\beta^{k}_{-}$.

######  Lemma 11.

($\lambda^{2}_{\pm}$-$\mathsf{con}$-$\mathsf{tot}$) implies
($\lambda^{1}_{\pm}$-$\mathsf{con}$-$\mathsf{tot}$), and vice versa.

Here the converse direction is trivial.

#### 3rd stage.

Now we focus on the complexity of elements $\alpha$ from $\mathsf{con}$. To
eliminate $\mathcal{D}(-)$ consider the following auxiliary axioms:

  1. ($\alpha_{+}$-$\mathsf{con}$-$\mathsf{tot}$)

${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\dbox{\normalcolor$\\{(x^{k},y)\\}_{k}\subseteq\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee}$}},\ \beta\in\mathsf{tot}_{\wedge},\
\beta_{+}\leq\bigvee_{k}x^{k}\implies y\leq\beta_{-}$

  2. ($\alpha_{-}$-$\mathsf{con}$-$\mathsf{tot}$)

${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\dbox{\normalcolor$\\{(x,y^{k})\\}_{k}\subseteq\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee}$}},\ \beta\in\mathsf{tot}_{\vee},\
\beta_{-}\leq\bigvee_{k}y^{k}\implies x\leq\beta_{+}$

Let $\alpha\in\mathcal{D}(\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee})$. By Lemma 7, this means that there exist
$A_{\pm}\subseteq B_{\pm}$ which are ($\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee}$)-independent and such that $\alpha=(\bigvee
A_{+},\bigvee A_{-})$. Let us fix a $b_{-}\in A_{-}$. The
($\mathord{\downarrow}\mkern 1.0mu\mathsf{con}_{\wedge,\vee}$)-independence of
$A_{+}$ and $A_{-}$ means that
$A_{+}\mathord{\times}\\{b\\}\subseteq\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee}$. Because also
$\beta_{+}\leq\alpha_{+}=\bigvee A_{+}$, we can apply
($\alpha_{+}$-$\mathsf{con}$-$\mathsf{tot}$) and obtain that
$b_{-}\leq\beta_{-}$. Since $b_{-}\in A_{-}$ was chosen arbitrarily,
$\alpha_{-}=\bigvee A_{-}\leq\beta_{-}$. We have proved that
($\alpha_{+}$-$\mathsf{con}$-$\mathsf{tot}$) implies
($\lambda^{2}_{+}$-$\mathsf{con}$-$\mathsf{tot}$).

Finally, we can get rid of the downwards closure of
$\mathsf{con}_{\wedge,\vee}$. Consider the following axioms:

  1. ($\lambda^{3}_{+}$-$\mathsf{con}$-$\mathsf{tot}$)

${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\dbox{\normalcolor$\alpha\in\mathsf{con}_{\wedge,\vee,\bigvee}$}},\
\beta\in\mathsf{tot}_{\wedge}$,
$\beta_{+}\leq\alpha_{+}\implies\alpha_{-}\leq\beta_{-}$

  2. ($\lambda^{3}_{-}$-$\mathsf{con}$-$\mathsf{tot}$)

${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\dbox{\normalcolor$\alpha\in\mathsf{con}_{\wedge,\vee,\bigwedge}$}},\
\beta\in\mathsf{tot}_{\vee}$,
$\beta_{-}\leq\alpha_{-}\implies\alpha_{+}\leq\beta_{+}$

Let $\\{(x^{k},y)\\}_{k}\subseteq\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee}$ be such that $\beta_{+}\leq\bigvee_{k}x^{k}$.
For every $k$, there exists an $\alpha^{k}\in\mathsf{con}_{\wedge,\vee}$ such
that $(x^{k},y)\sqsubseteq\alpha^{k}$. Clearly,
$\beta_{+}\leq\bigvee_{k}x^{k}\leq\bigvee_{k}\alpha^{k}_{+}$, and
$\alpha=(\bigvee_{k}\alpha^{k}_{+},\bigwedge_{k}\alpha^{k}_{-})\in\mathsf{con}_{\wedge,\vee,\bigvee}$.
We can apply ($\lambda^{3}_{+}$-$\mathsf{con}$-$\mathsf{tot}$) and obtain that
$y\leq\alpha_{-}\leq\beta_{-}$. Together with the previous result we have
that:

######  Lemma 12.

($\lambda^{3}_{\pm}$-$\mathsf{con}$-$\mathsf{tot}$) implies
($\lambda^{2}_{\pm}$-$\mathsf{con}$-$\mathsf{tot}$).

#### 4th stage.

The final simplification is similar to the 2nd stage but this time acts on the
$\mathsf{con}$ side:

  1. ($\lambda^{4}_{+}$-$\mathsf{con}$-$\mathsf{tot}$)

${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\dbox{\normalcolor$\alpha\in\mathsf{con}_{\wedge,\bigvee}$}},\
\beta\in\mathsf{tot}_{\wedge}$,
$\beta_{+}\leq\alpha_{+}\implies\alpha_{-}\leq\beta_{-}$

  2. ($\lambda^{4}_{-}$-$\mathsf{con}$-$\mathsf{tot}$)

${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\dbox{\normalcolor$\alpha\in\mathsf{con}_{\vee,\bigwedge}$}},\
\beta\in\mathsf{tot}_{\vee}$,
$\beta_{-}\leq\alpha_{-}\implies\alpha_{+}\leq\beta_{+}$

Distributivity of $\wedge$ and $\vee$ gives us that

$\displaystyle\mathsf{con}_{\wedge,\vee,\bigvee}=\mathsf{con}_{\wedge,\bigvee}\quad\text{and}\quad\mathsf{con}_{\wedge,\vee,\bigwedge}=\mathsf{con}_{\vee,\bigwedge}$

from which we can conclude:

######  Lemma 13.

($\lambda^{4}_{\pm}$-$\mathsf{con}$-$\mathsf{tot}$) implies
($\lambda^{3}_{\pm}$-$\mathsf{con}$-$\mathsf{tot}$), and vice versa.

Furthermore, ($\lambda^{4}_{\pm}$-$\mathsf{con}$-$\mathsf{tot}$) and
($\lambda^{1}_{\pm}$-$\mathsf{con}$-$\mathsf{tot}$) are equivalent because

$\displaystyle\mathsf{con}_{\wedge,\bigvee}\subseteq\mathcal{D}(\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee})\quad\text{and}\quad\mathsf{con}_{\vee,\bigwedge}\subseteq\mathcal{D}(\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee}).$ (2)

To prove these inclusions, let
$\alpha=(\bigvee_{k}\alpha^{k}_{+},\bigwedge_{k}\alpha^{k}_{-})$ where
$\\{\alpha^{k}\\}_{k\in K}\subseteq\mathsf{con}_{\wedge}$. Then, for every
$k\in K$, $(\alpha^{k}_{+},\alpha_{-})\sqsubseteq\alpha^{k}$ and so
$(\alpha^{k}_{+},\alpha_{-})\in\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge}\subseteq\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee}$. Because $\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee}$ is $\vee$-closed, $\\{(\bigvee_{k\in
F}\,\alpha^{k}_{+},\alpha_{-}):F\mathbin{\subseteq\\!^{\text{fin}}}K\\}$ is
directed in $\mathord{\downarrow}\mkern 1.0mu\mathsf{con}_{\wedge,\vee}$ and
so $\alpha\in\mathcal{D}(\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee})$.

We can apply similar techniques to simplify ($R$-ind):

######  Lemma 14.

($\mathord{\downarrow}\mkern 1.0mu\mathsf{con}_{\wedge,\vee}$-ind) is
equivalent to having the following two conditions

  1. ($\mathord{\downarrow}\mkern 1.0mu\mathsf{con}_{\wedge,\vee}$-ind+)

$(B_{+}\mathord{\times}B_{-})\cap\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\bigvee}\subseteq\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee}$

  2. ($\mathord{\downarrow}\mkern 1.0mu\mathsf{con}_{\wedge,\vee}$-ind-)

$(B_{+}\mathord{\times}B_{-})\cap\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\vee,\bigwedge}\subseteq\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee}$

We sum up all the previous results into this theorem:

######  Theorem 15.

If ($\lambda^{4}_{\pm}$-$\mathsf{con}$-$\mathsf{tot}$) and
($\mathord{\downarrow}\mkern 1.0mu\mathsf{con}_{\wedge,\vee}$-ind±) hold for a
pre-d-frame presentation, then the generated pre-d-frame satisfies
($\mathsf{con}$-$\mathsf{tot}$).

######  Remark.

It is not possible to check if ($\mathsf{con}$-$\mathsf{tot}$) holds in the
generated pre-d-frame just by looking at its syntactic presentation. However,
our sufficient conditions are much simpler than the formulas involving
infinitary applications of $\mathcal{D}(-)$. Nevertheless we still need to
understand the structure of the generated frame components.

###  4.4 A special case

In our applications even stronger and simpler conditions hold for the
presentations. Namely, consider the following _“micro version”_ of
($\mathsf{con}$-$\mathsf{tot}$):

  1. ($\mu_{+}$-$\mathsf{con}$-$\mathsf{tot}$)

$\alpha\in\mathsf{con}_{\vee}$, $\beta\in\mathsf{tot}_{\wedge}$.
$\beta_{+}\leq\alpha_{+}\implies\alpha_{-}\leq\beta_{-}$

  2. ($\mu_{-}$-$\mathsf{con}$-$\mathsf{tot}$)

$\alpha\in\mathsf{con}_{\wedge}$, $\beta\in\mathsf{tot}_{\vee}$.
$\beta_{-}\leq\alpha_{-}\implies\alpha_{+}\leq\beta_{+}$

and the following (more powerful) version of conditions
($\mathord{\downarrow}\mkern 1.0mu\mathsf{con}_{\wedge,\vee}$-ind±):

  1. (Indep+)

$(L_{+}\mathord{\times}B_{-})\cap\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\bigvee}\subseteq\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\vee}$

  2. (Indep-)

$(B_{+}\mathord{\times}L_{-})\cap\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\vee,\bigwedge}\subseteq\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge}$

######  Proposition 16.

If ($\mu_{\pm}$-$\mathsf{con}$-$\mathsf{tot}$) and (Indep±) hold for a pre-d-
frame presentation, then the generated pre-d-frame satisfies
($\mathsf{con}$-$\mathsf{tot}$).

##  5 Application: Coproducts

###  5.1 Coproducts of frames

For a nice presentation of the coproducts of frames, we refer the reader to
the book _“Frames and Locales”_ [12]. Here we only outline basic facts about
the construction. Let $\\{L^{i}\\}_{i\in\mathcal{I}}$ be a family of frames.
The coproduct of $\\{L^{i}\\}_{i}$ in the category of meet-semilattices is
$\prod^{\prime}_{i}L^{i}$ which is the subset of $\prod_{i}L^{i}$ consisting
of those elements with all but finitely many coordinates equal to 1. Then, the
coproduct of $\\{L^{i}\\}_{i}$ in the category of frames $\bigoplus_{i}L^{i}$
can be presented as the frame of $\mathcal{C}$-ideals of
$(\prod^{\prime}_{i}L^{i},\mathcal{C})$ with the set of coverings
$\mathcal{C}$ of the form:

$\\{a^{k}*_{j}u:k\in K\\}\dashv(\bigvee_{k\in K}a^{k})*_{j}u$

where, for an $a\in L^{j}$ and $u\in\prod^{\prime}_{i}L^{i}$, $a*_{j}u$ is the
element of $\prod^{\prime}_{i}L^{i}$ such that $(a*_{j}u)_{j}=a$ and
$(a*_{j}u)_{i}=u_{i}$ for $i\not=j$. Recall also that the smallest element of
$\bigoplus_{i}L^{i}$ is the $\mathcal{C}$-ideal
$\mathbf{n}=\\{u\in\prod^{\prime}_{i}L^{i}~{}|~{}u_{i}=0\text{ for some
}i\\}$.

The inclusion maps are the frame homomorphisms $\iota^{j}\colon
L^{j}\to\bigoplus_{i}L^{i}$, $x\mapsto\mathord{\downarrow}\mkern
1.0mu(x*_{j}\overline{1})\cup\mathbf{n}$, where $(\overline{1})_{i}=1$ for all
$i\in\mathcal{I}$. We can factor $\iota^{j}$ into a composition of two meet-
semilattice homomorphisms $\llbracket-\rrbracket\circ\kappa^{j}$ where

$\displaystyle\kappa^{j}\colon L^{j}$
$\displaystyle\to\prod\nolimits_{i}^{\prime}L^{i}$ and
$\displaystyle\llbracket-\rrbracket\colon\prod\nolimits^{\prime}_{i}L^{i}$
$\displaystyle\to\bigoplus_{i}L^{i}$ $\displaystyle x$ $\displaystyle\mapsto
x*_{j}\overline{1}$ $\displaystyle u$
$\displaystyle\mapsto\mathord{\downarrow}\mkern 1.0muu\cup\mathbf{n}$

Here $\kappa^{j}$ is the universal map for the semilattice coproduct
$\prod\nolimits_{i}^{\prime}L^{i}$ and $\llbracket-\rrbracket$ is the
inclusion $B\to\mathcal{C}\text{-}\mathtt{Idl}\\!\left(B\right)$ as in Lemma
1, $B=\prod^{\prime}_{i}L^{i}$, and $\mathord{\downarrow}\mkern
1.0muu\cup\mathbf{n}$ is the smallest $\mathcal{C}$-ideal containing $u$.

###  5.2 Coproducts of d-frames

Let
$\\{\mathcal{L}^{i}=(L_{+}^{i},L_{-}^{i};\mathsf{con}^{i},\mathsf{tot}^{i})\\}_{i\in\mathcal{I}}$
be a family of d-frames. We will define the coproduct of
$\\{\mathcal{L}^{i}\\}_{i}$ by a free d-frame construction. First, we compute
the frame components of the coproduct of $\\{\mathcal{L}^{i}\\}_{i}$ as the
coproducts of the frame components of the d-frames
$\\{\mathcal{L}^{i}\\}_{i}$. Set $B_{+}=\prod^{\prime}_{i}L_{+}^{i}$ and
$B_{-}=\prod^{\prime}_{i}L_{-}^{i}$ and $\mathcal{C}_{+}$ and
$\mathcal{C}_{-}$ independently as in Subsection 5.1 (for $B_{+}$ and $B_{-}$,
respectively). Namely, for every $j\in\mathcal{I}$, we have a frame
homomorphism

${\iota^{j}_{\pm}\colon
L^{j}_{\pm}}$${\prod^{\prime}_{i}L^{i}_{\pm}}$${\bigoplus_{i}L^{i}_{\pm}}$$\scriptstyle{\kappa^{j}_{\pm}}$$\scriptstyle{\llbracket-\rrbracket_{\pm}}$

In order for $\iota^{j}=(\iota^{j}_{+},\iota^{j}_{-})$ to be a _d-frame_
embedding into a coproduct, for every $(a,b)\in\mathsf{con}^{j}$ (resp.
$\mathsf{tot}^{j}$), it has to be the case that
$(\iota^{j}_{+}(a),\,\iota^{j}_{-}(b))\in\mathtt{CON}\langle\mathsf{con}_{1}\rangle$
(resp. $\mathtt{TOT}\langle\mathsf{tot}_{1}\rangle$). Also, the universal
property of coproducts guarantees that for any d-frame cone
$\\{\mathcal{L}^{i}\to\mathcal{M}\\}_{i}$ there is a mediating d-frame
homomorphism $\bigoplus_{i}\mathcal{L}^{i}\to\mathcal{M}$. This means that the
relations we generate $\mathtt{CON}\langle\mathsf{con}_{1}\rangle$ and
$\mathtt{TOT}\langle\mathsf{tot}_{1}\rangle$ from should not contain anything
more. Therefore, define $\mathsf{con}_{1},\mathsf{tot}_{1}\subseteq
B_{+}\mathord{\times}B_{-}$ by

$\displaystyle(a*_{j}\overline{1},\,b*_{j}\overline{1})\in\mathsf{con}_{1}$
$\displaystyle\quad\text{iff}\quad(a,b)\in\mathsf{con}^{j}$
$\displaystyle(a*_{j}\overline{1},\,b*_{j}\overline{1})\in\mathsf{tot}_{1}$
$\displaystyle\quad\text{iff}\quad(a,b)\in\mathsf{tot}^{j}$

and by $\bigoplus_{i}\mathcal{L}^{i}$ denote the resulting pre-d-frame
$(\bigoplus_{i}L_{+}^{i}\mathord{\times}\bigoplus_{i}L_{-}^{i};\,\mathtt{CON}\langle\mathsf{con}_{1}\rangle,\mathtt{TOT}\langle\mathsf{tot}_{1}\rangle)$.

######  Notation.

For every $a\in L^{i}$ and $u\in B$, denote $a\oplus_{i}u=\llbracket
a*_{i}u\rrbracket_{\pm}=\mathord{\downarrow}\mkern
1.0mu(a*_{i}u)\cup\mathbf{n}_{\pm}$. In particular,
$a\oplus_{i}\overline{1}=\mathord{\downarrow}\mkern
1.0mu(a*_{i}\overline{1})\cup\mathbf{n}_{\pm}$. As before, we identify
$B_{\pm}$ with $\llbracket
B_{\pm}\rrbracket_{\pm}\subseteq\bigoplus_{i}L^{i}_{\pm}$, $\mathsf{con}_{1}$
with
$\llbracket\mathsf{con}_{1}\rrbracket\subseteq\bigoplus_{i}L_{+}^{i}\mathord{\times}\bigoplus_{i}L_{-}^{i}$,
and $\mathsf{tot}_{1}$ with $\llbracket\mathsf{tot}_{1}\rrbracket$.

To simplify our work by making sure that we can deal with indexes coherently,
we prove the following lemma about normal forms of elements from
$\mathsf{con}_{\vee}$, $\mathsf{con}_{\wedge}$, $\mathsf{tot}_{\vee}$ and
$\mathsf{tot}_{\wedge}$:

######  Lemma 17.

Let $\alpha\in\mathsf{con}_{\wedge}/\mathsf{tot}_{\wedge}$. Then, it is of the
form $(\bigwedge_{i}\alpha^{i}_{+},\bigvee_{i}\alpha^{i}_{-})$ such that

  1. 1.

for every $i\in\mathcal{I}$:
$\alpha^{i}=(a_{+}\oplus_{i}\overline{1},a_{-}\oplus_{i}\overline{1})$ for
some $(a_{+},a_{-})\in\mathsf{con}^{i}$ (resp. $\mathsf{tot}^{i}$), and

  2. 2.

there exists a _finite_
$I(\alpha)\mathbin{\subseteq\\!^{\text{fin}}}\mathcal{I}$ s.t. $i\in
I(\alpha)$ iff $\alpha^{i}\not=\text{\emph{t}}\mkern-3.0mu\text{\emph{t}}$

Similarly, every $\alpha\in\mathsf{con}_{\vee}$ (resp.
$\mathsf{tot}_{\wedge}$) is of the form
$(\bigvee_{i}\alpha^{i}_{+},\bigwedge_{i}\alpha^{i}_{-})$ where
$\alpha^{i}\in\mathsf{con}_{1}$ (resp. $\mathsf{tot}_{1}$) and $I(\alpha)$
denotes the finite set of indexes for which $\alpha^{i}\not=\text{\emph{ff}}$.

Notice that 1. and 2. make sense together. Anytime
$\alpha^{i}=\text{\emph{t}}\mkern-3.0mu\text{\emph{t}}$ we have that
$\text{\emph{t}}\mkern-3.0mu\text{\emph{t}}=(\mathord{\downarrow}\mkern
1.0mu\overline{1}\cup\mathbf{n_{+}},\mathbf{n_{-}})=(1\oplus_{i}\overline{1},0\oplus_{i}\overline{1})$
and $(1,0)\in\mathsf{con}^{i}/\mathsf{tot}^{i}$. The case for
$\alpha^{i}=\text{\emph{ff}}$ is similar.

###  5.3 Strips, rectangles and crosses

Before we get into proving that $\bigoplus_{i}\mathcal{L}^{i}$ satisfies
($\mathsf{con}$-$\mathsf{tot}$) we look into the structure of
$\mathsf{con}_{\vee}$, $\mathsf{con}_{\wedge}$, $\mathsf{tot}_{\vee}$ and
$\mathsf{tot}_{\wedge}$. It turns out that there is a nice geometrical
intuition that we can employ.

First, for an $a\in L^{i}_{\pm}$, we call $a\oplus_{i}\overline{1}$ _an
$i$-strip_666We sometimes omit the index and call $i$-strips just strips
whenever it does not lead to a confusion.. Then, anytime
$(a,b)\in\mathsf{con}^{i}$, we can think of the corresponding pair
$(a\oplus_{i}\overline{1},\,b\oplus_{i}\overline{1})\in\mathsf{con}_{1}$ as of
a pair of _“disjoint”_ $i$-strips and, similarly, $(c,d)\in\mathsf{tot}^{i}$
gives a pair of strips that are _“covering the whole space”_ , i.e.
$(c\oplus_{i}\overline{1},\,d\oplus_{i}\overline{1})\in\mathsf{tot}_{1}$. This
terminology is motivated by the case when $\mathcal{I}=\\{1,2\\}$. Both cases
are displayed in the picture below for $\mathcal{L}^{1}\oplus\mathcal{L}^{2}$:

$a\oplus_{1}\overline{1}$$a\oplus_{1}\overline{1}$ab$\mathcal{L}^{1}$$\mathcal{L}^{2}$$c\oplus_{1}\overline{1}$$d\oplus_{1}\overline{1}$cd$\mathcal{L}^{1}$$\mathcal{L}^{2}$

Therefore, all elements of $\mathsf{con}_{1}$ and $\mathsf{tot}_{1}$ are pairs
of strips. It is rather a technical lemma that the set of $i$-strips in the
coproduct has exactly the same structure as the d-frame $\mathcal{L}^{i}$:

######  Lemma 18.

Let $S^{i}_{\pm}$ be the set of all $i$-strips in $\bigoplus_{i}L^{i}_{\pm}$.
If all $L^{i}_{\pm}$’s are nontrivial777A frame is _trivial_ if it is
isomorphic to the trivial frame $\mathbf{1}=\\{0=1\\}$. then

$(S^{i}_{+},S^{i}_{-};\,\mathsf{con}_{1}\cap(S^{i}_{+}\mathord{\times}S^{i}_{-}),\,\mathsf{tot}_{1}\cap(S^{i}_{+}\mathord{\times}S^{i}_{-}))\cong\mathcal{L}^{i}.$

Moreover, finite $\wedge$-combinations of pairs of strips is something that we
can imagine as a pair consisting of a rectangle and a cross. For example, let
$\alpha\in\mathsf{con}_{1}$ be a pair of $1$-strips and
$\alpha^{\prime}\in\mathsf{con}_{1}$ a pair of $2$-strips. Then, as the
picture below suggests, the plus coordinate of $\alpha\wedge\alpha^{\prime}$
in $\mathcal{L}^{1}\oplus\mathcal{L}^{2}$ is a rectangle and the minus
coordinate is a cross. Notice also that the cross and rectangle are disjoint.

$\alpha_{+}$$\alpha_{-}$$\mathcal{L}^{1}$$\mathcal{L}^{2}$$\wedge$$\alpha^{\prime}_{+}$$\alpha^{\prime}_{-}$$\mathcal{L}^{1}$$\mathcal{L}^{2}$$=$$\alpha_{-}\vee\alpha^{\prime}_{-}$$\alpha_{+}\wedge\alpha^{\prime}_{+}$$\mathcal{L}^{1}$$\mathcal{L}^{2}$

The picture for two pairs of strips $\beta,\beta^{\prime}\in\mathsf{tot}_{1}$
is similar but this time the cross and rectangle of
$\beta\wedge\beta^{\prime}$ cover the whole space.

This geometrical intuition builds up well for these formal definitions:
$\gamma=\bigwedge_{i}\gamma^{i}$, where
$\gamma^{i}=c^{i}\oplus_{i}\overline{1}$ ($\forall i\in\mathcal{I}$), is a
_rectangle_ if there exists a finite
$I(\gamma)\mathbin{\subseteq\\!^{\text{fin}}}\mathcal{I}$ such that
$c^{i}\not=1$ iff $i\in I(\gamma)$. Similarly, $\delta=\bigvee_{i}\delta^{i}$,
where $\delta^{i}=d^{i}\oplus_{i}\overline{1}$, is a _cross_ if for some
finite $I(\delta)\mathbin{\subseteq\\!^{\text{fin}}}\mathcal{I}$,
$d^{i}\not=0$ iff $i\in I(\delta)$.

Notice that, by Lemma 17, every element of $\mathsf{con}_{\wedge}$ (resp.
$\mathsf{tot}_{\wedge}$) is of the form
$(\bigwedge_{i}\alpha^{i}_{+},\bigvee_{i}\alpha^{i}_{-})$ with only finitely
many nontrivial $\alpha^{i}$’s. In the present terminology, $\alpha$ is a pair
rectangle–cross and this exactly matches the geometrical intuition we just
discussed.

######  Observation 19.

Rectangles are exactly the elements of $B_{\pm}$.

###### Proof.

Every $\gamma\in B_{\pm}$ is of the form $\llbracket u\rrbracket_{\pm}$ for
some $u\in\prod^{\prime}_{i}L^{i}_{\pm}$. Because $u$ has only finitely many
indexes different from 1, $\llbracket
u\rrbracket_{\pm}=\llbracket(a^{1}*_{i(1)}\overline{1})\wedge\dots\wedge(a^{n}*_{i(n)}\overline{1})\rrbracket_{\pm}=\llbracket
a^{1}*_{i(1)}\overline{1}\rrbracket_{\pm}\wedge\dots\wedge\llbracket
a^{n}*_{i(n)}\overline{1}\rrbracket_{\pm}=(a^{1}\oplus_{i(1)}\overline{1})\wedge\dots\wedge(a^{n}\oplus_{i(n)}\overline{1})$.
The reverse direction is similar. ∎

There is a nice interplay between rectangles and crosses:

######  Lemma 20.

Let $\gamma=\bigwedge_{i}\gamma^{i}$ be a rectangle and let
$\delta=\bigvee_{i}\delta^{i}$ be a cross such that $\gamma\leq\delta$. Then,
there exists an $i\in I(\gamma)$ such that $\gamma^{i}\leq\delta^{i}$.

###### Proof.

Let $\gamma^{i}=c^{i}\oplus_{i}\overline{1}$ and
$\delta^{i}=d^{i}\oplus_{i}\overline{1}$, for every $i\in\mathcal{I}$. By
Observation 19, $\gamma=\llbracket u\rrbracket_{\pm}$ for some
$u\in\prod^{\prime}_{i}L^{i}_{\pm}$ such that, for every $i\in\mathcal{I}$,
$(u)_{i}=c^{i}$. This means that $(u)_{i}\not=1$ iff $i\in I(\gamma)$. Also,
by Lemma 27, $\delta$ has a form of a finite union $\bigcup_{i\in
I(\delta)}\delta^{i}$. If $c^{i}=0$ for some $i\in I(\gamma)$, then $c^{i}\leq
d^{i}$. Otherwise, $c^{i}\not=0$ for all $i\in I(\gamma)$ and, since
$\gamma\leq\delta$ iff $u\in\delta$, there must exist an $i\in I(\delta)$ such
that $u\in\delta^{i}$ and then, by Lemma 25.1, $(u)_{i}=c^{i}\leq d^{i}$.
Finally, because $i\in I(\delta)$, $d^{i}\not=1$ and so also $c^{i}\not=1$ and
$i\in I(\gamma)$. ∎

###  5.4 Proof of ($\mathsf{con}$-$\mathsf{tot}$)

In this section we prove that $\bigoplus_{i}\mathcal{L}^{i}$ is a d-frame. To
simplify our proofs, we can assume that all $\mathcal{L}^{i}$’s are nontrivial
thanks to the following lemma.

######  Lemma 21.

If $L^{i}_{+}=\mathbf{1}$ or $L^{i}_{-}=\mathbf{1}$ for some
$i\in\mathcal{I}$, then $\bigoplus_{i}\mathcal{L}^{i}$ satisfies
($\mathsf{con}$-$\mathsf{tot}$).

###### Proof.

Observe that, by ($\mathsf{con}$-$\mathsf{tot}$) for $\mathcal{L}^{i}$, if
$L^{i}_{+}=\mathbf{1}$ then automatically also $L^{i}_{-}=\mathbf{1}$, and
vice versa. Therefore, $\bigoplus_{i}L^{i}_{\pm}=\\{\mathbf{n_{\pm}}\\}$ and
so $\bigoplus_{i}\mathcal{L}^{i}$ is trivial and satisfies
($\mathsf{con}$-$\mathsf{tot}$). ∎

To show that ($\mathsf{con}$-$\mathsf{tot}$) holds for
$\bigoplus_{i}\mathcal{L}^{i}$ we will use Proposition 16. In order to be able
to do that we need to prove that ($\mu_{\pm}$-$\mathsf{con}$-$\mathsf{tot}$)
and (Indep±) hold:

######  Lemma 22.

($\mu_{\pm}$-$\mathsf{con}$-$\mathsf{tot}$) holds for
$\bigoplus_{i}\mathcal{L}^{i}$:

###### Proof.

Let $\alpha=\bigvee_{i}\alpha^{i}\in\mathsf{con}_{\vee}$ and
$\beta=\bigwedge_{i}\beta^{i}\in\mathsf{tot}_{\wedge}$ be in canonical forms,
and assume that $\beta_{+}\leq\alpha_{+}$. From canonicity of $\alpha$ and
$\beta$, know that $\alpha_{+}$ is a cross and $\beta_{+}$ is a rectangle. By
Lemma 20, there is an $i\in I(\beta)$ such that
$\beta^{i}_{+}\leq\alpha^{i}_{+}$. From ($\mathsf{con}$-$\mathsf{tot}$) for
$\mathcal{L}^{i}$, $\alpha^{i}_{-}\leq\beta^{i}_{-}$ and so
$\alpha_{-}=\bigwedge_{i}\alpha^{i}_{-}\,\leq\,\alpha^{i}_{-}\,\leq\,\beta^{i}_{-}\,\leq\,\bigvee_{i}\beta^{i}_{-}=\beta_{-}.$
∎

######  Lemma 23.

(Indep±) holds for $\bigoplus_{i}\mathcal{L}^{i}$.

###### Proof.

Let $(x,b_{-})\in(L_{+}\mathord{\times}B_{-})\cap\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\bigvee}$. Denote its upper bound
$(\bigvee_{k}\alpha^{k}_{+},\bigwedge_{k}\alpha^{k}_{-})$ where, for each $k$,
$\alpha^{k}=(\bigwedge_{i}\alpha^{k,i}_{+},\bigvee_{i}\alpha^{k,i}_{-})$ is a
pair rectangle–cross from $\mathsf{con}_{\wedge}$. Because $b_{-}\in B_{-}$,
it is a rectangle of the form $b_{-}=\bigwedge_{i}\gamma^{i}$ (Observation
19). Because, for every $k$, $b_{-}\leq\alpha^{k}_{-}$, by Lemma 20, there
exists an $i(k)\in I(b_{-})$ such that $\gamma^{i(k)}\leq\alpha^{k,i(k)}_{-}$.
Fix an $i\in I(b_{-})$ and set $K(i)=\\{k~{}|~{}i(k)=i\\}$. By Lemma 21, we
can assume that all $L^{i}_{\pm}$’s are nontrivial and because
$\\{\alpha^{k,i}:k\in K(i)\\}$ are all pairs of $i$-strips and $\gamma^{i}$ is
an $i$-strip, by Lemma 18, we can carry the reasoning in the rest of this
paragraph in the d-frame $\mathcal{L}^{i}$. Since $\mathsf{con}^{i(k)}$ is
downwards closed and $\gamma^{i}\leq\alpha^{k,i}$ ($\forall k\in K(i)$), also
$(\alpha^{k,i(k)}_{+},\gamma^{i(k)})\in\mathsf{con}_{1}$ and, therefore, by
$\\!\mathop{\,\ThisStyle{\ensurestackMath{\bigsqcup\stackengine{-0pt}{\,}{\SavedStyle\\!^{\mathord{\uparrow}}}{O}{l}{F}{T}{S}}}\\!}$
and $\vee$-closeness of $\mathsf{con}^{i(k)}$, $(\bigvee_{k\in
K(i)}\alpha^{k,i}_{+},\gamma^{i})\in\mathsf{con}_{1}$.

Finally, because $I(b_{-})$ is finite

$\bigvee_{i\in I(b_{-})}(\bigvee_{k\in
K(i)}\alpha^{k,i}_{+},\gamma^{i})=(\bigvee_{i\in I(b_{-})}(\bigvee_{k\in
K(i)}\alpha^{k,i}_{+}),\bigwedge_{i\in
I(b_{-})}\gamma^{i})=(\bigvee_{k}\alpha^{k,i(k)}_{+},b_{-})\in\mathsf{con}_{\vee}.$

Because $\alpha^{k}_{+}=\bigwedge_{i}\alpha^{k,i}_{+}\leq\alpha^{k,i(k)}_{+}\
(\forall k)$,
$x\leq\bigvee_{k}\alpha^{k}_{+}\leq\bigvee_{k}\alpha^{k,i(k)}_{+}$ and so
$(x,b_{-})\in\mathord{\downarrow}\mkern 1.0mu\mathsf{con}_{\vee}$. ∎

By Proposition 16, we know that $\bigoplus_{i}\mathcal{L}^{i}$ is a d-frame
and, moreover, by the same reasoning as for frames, we can prove that it has
the universal property of a coproduct:

######  Theorem 24.

$\bigoplus_{i}\mathcal{L}^{i}$ is the coproduct in the category of d-frames.

## Acknowledgement

Discussions with Aleš Pultr helped greatly in the simplifications of Section
4.

## References

  * [1] S. Abramsky.  Domain theory in logical form.  In Symposium on Logic In Computer Science, pages 47–53. IEEE Computer Society Press, 1987.
  * [2] Richard N. Ball and Aleš Pultr.  Extending semilattices to frames using sites and coverages.  Mathematica Slovaca, 64(3):527–544, 2014.
  * [3] B Banaschewski, GCL Brümmer, and KA Hardie.  Biframes and bispaces.  Quaestiones Mathematicae, 6(1-3):13–25, 1983.
  * [4] Bart Jacobs.  Many-sorted coalgebraic modal logic: a model-theoretic study.  RAIRO-Theoretical Informatics and Applications, 35(1):31–59, 2001\.
  * [5] T. Jakl and A. Jung.  Vietoris construction for bispaces and d-frames.  In preparation.
  * [6] P. T. Johnstone.  Stone Spaces, volume 3 of Cambridge Studies in Advanced Mathematics.  Cambridge University Press, 1982.
  * [7] A. Jung.  Continuous domain theory in logical form.  In B. Coecke, L. Ong, and P. Panangaden, editors, Computation, Logic, Games, and Quantum Foundations. The Many Facets of Samson Abramsky, volume 7860 of Lecture Notes in Computer Science, pages 166–177. Springer Verlag, 2013.  doi:10.1007/978-3-642-38164-5_12.
  * [8] A. Jung and M. A. Moshier.  On the bitopological nature of Stone duality.  Technical Report CSR-06-13, School of Computer Science, The University of Birmingham, 2006.  110 pages.  URL: ftp://ftp.cs.bham.ac.uk/pub/tech-reports/2006/CSR-06-13.pdf.
  * [9] Bartek Klin.  Coalgebraic modal logic beyond sets.  Electronic Notes in Theoretical Computer Science, 173:177–201, 2007\.
  * [10] Clemens Kupke, Alexander Kurz, and Yde Venema.  Stone coalgebras.  Theoretical Computer Science, 327(1-2):109–134, 2004.
  * [11] Jimmie Lawson.  Stably compact spaces.  Mathematical Structures in Computer Science, 21(01):125–169, 2011\.
  * [12] Jorge Picado and Aleš Pultr.  Frames and Locales: Topology without points.  Springer-Birkhauser Basel, 2011.
  * [13] S. J. Vickers.  Topology Via Logic, volume 5 of Cambridge Tracts in Theoretical Computer Science.  Cambridge University Press, 1989.

##  Appendix A Missing proofs in Section 3 and 4

###### Proof of Lemma 3 (Universality).

By Lemma 1, $\llbracket-\rrbracket$ is a pointwise meet-semilattice
homomorphism which transforms $\mathcal{C}_{\pm}$ covers into joins and, by
the definition, also
$\llbracket\mathsf{con}_{1}\rrbracket\subseteq\mathsf{con}_{*}$ and
$\llbracket\mathsf{tot}_{1}\rrbracket\subseteq\mathsf{tot}_{*}$. To show
universality, let
$f\colon(B_{+},B_{-};\,\mathsf{con}_{1},\mathsf{tot}_{1})\to\mathcal{M}$ be a
presentation preserving map. Because the individual components of $f$, i.e.
$f_{\pm}\colon B_{\pm}\to M_{\pm}$, are meet-preserving and transform covers
into joins, by Lemma 1, there exist unique frame homomorphisms
$\overline{f}_{\pm}\colon L_{\pm}\to M_{\pm}$ such that
$f_{\pm}=\overline{f}_{\pm}\circ\llbracket-\rrbracket_{\pm}$.

We need to prove that $\overline{f}=(\overline{f}_{+},\overline{f}_{-})$ is a
d-frame homomorphism. Since $f$ preserves $\mathsf{con}_{1}$ and
$\mathsf{tot}_{1}$, we have that
$\overline{f}[\llbracket\mathsf{con}_{1}\rrbracket]=f[\mathsf{con}_{1}]\subseteq\mathsf{con}_{\mathcal{M}}$
which is equivalent to
$\llbracket\mathsf{con}_{1}\rrbracket\subseteq\overline{f}^{-1}[\mathsf{con}_{\mathcal{M}}]$.
Because $\overline{f}$ is a pair of frame homomorphisms,
$\overline{f}^{-1}[\mathsf{con}_{\mathcal{M}}]$ is $\mathord{\downarrow}\mkern
1.0mu$-closed, closed under
$\wedge,\vee,\\!\mathop{\,\ThisStyle{\ensurestackMath{\bigsqcup\stackengine{-0pt}{\,}{\SavedStyle\\!^{\mathord{\uparrow}}}{O}{l}{F}{T}{S}}}\\!}$
and contains tt and ff. However,
$\mathtt{CON}\langle\llbracket\mathsf{con}_{1}\rrbracket\rangle$ is the
smallest such relation which contains $\llbracket\mathsf{con}_{1}\rrbracket$
and so
$\mathtt{CON}\langle\llbracket\mathsf{con}_{1}\rrbracket\rangle\subseteq\overline{f}^{-1}[\mathsf{con}_{\mathcal{M}}]$.
Finally, as before, this is equivalent to
$\overline{f}[\mathtt{CON}\langle\llbracket\mathsf{con}_{1}\rrbracket\rangle]\subseteq\mathsf{con}_{\mathcal{M}}$.
The case for
$\overline{f}[\llbracket\mathsf{tot}_{1}\rrbracket]\subseteq\mathsf{tot}_{\mathcal{M}}$
is similar. ∎

###### Proof of Lemma 14.

The left-to-right implication holds immediately from (2) on page 2 and the
fact that $\mathcal{D}(\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee})$ is downwards closed. For the other
implication, let
$(b_{+},b_{-})\in(B_{+}\mathord{\times}B_{-})\cap\mathcal{D}(\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee})$. By Lemma 7, there exist $A_{\pm}\subseteq
B_{\pm}$ such that $b_{\pm}=\bigvee A_{\pm}$ and
$A_{+}\mathord{\times}A_{-}\subseteq\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee}$. Fix an $a_{-}\in A_{-}$. Because
$A_{+}\mathord{\times}\\{a_{-}\\}\subseteq\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee}$, for every $a^{k}_{+}\in A_{+}$, there exists
an $\alpha^{k}\in\mathsf{con}_{\wedge,\vee}$ such that
$(a^{k}_{+},a_{-})\sqsubseteq\alpha^{k}$. Then,

$(b_{+},a_{-})=(\bigvee
A_{+},a_{-})\sqsubseteq(\bigvee_{k}\alpha^{k}_{+},\bigwedge_{k}\alpha^{k}_{-})\in\mathsf{con}_{\wedge,\vee,\bigvee}=\mathsf{con}_{\wedge,\bigvee}$

and because $(b_{+},a_{-})\in B_{+}\mathord{\times}B_{-}$ we can use
($\mathord{\downarrow}\mkern 1.0mu\mathsf{con}_{\wedge,\vee}$-ind+) and obtain
that $(b_{+},a_{-})\in\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee}$.

Since $a_{-}\in A_{-}$ was chosen arbitrarily,
$\\{b_{+}\\}\mathord{\times}A_{-}\subseteq\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee}$. Similarly to the above, for every
$a^{k}_{-}\in A_{-}$ there is an $\alpha^{k}\in\mathsf{con}_{\wedge,\vee}$
such that $(b_{+},a^{k}_{-})\sqsubseteq\alpha^{k}$, and
$(b_{+},b_{-})\sqsubseteq(\bigwedge_{k}\alpha^{k}_{+},\bigvee_{k}\alpha^{k}_{-})\in\mathsf{con}_{\vee,\bigwedge}$.
Finally, by ($\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\vee}$-ind-),
$(b_{+},b_{-})\in\mathord{\downarrow}\mkern 1.0mu\mathsf{con}_{\wedge,\vee}$.
∎

###### Proof of Proposition 16.

We use Theorem 15. Clearly, (Indep±) is a strengthening of
($\mathord{\downarrow}\mkern 1.0mu\mathsf{con}_{\wedge,\vee}$-ind+). To prove
($\lambda^{4}_{\pm}$-$\mathsf{con}$-$\mathsf{tot}$), let
$\alpha\in\mathsf{con}_{\wedge,\bigvee}$ and $\beta\in\mathsf{tot}_{\wedge}$
be such that $\beta_{+}\leq\alpha_{+}$. Moreover, fix a $b_{-}\in B_{-}$ such
that $b_{-}\leq\alpha_{-}$. Then,
$(\alpha_{+},b_{-})\in\mathord{\downarrow}\mkern
1.0mu\mathsf{con}_{\wedge,\bigvee}$. By, (Indep+),
$(\alpha_{+},b_{-})\in\mathord{\downarrow}\mkern 1.0mu\mathsf{con}_{\vee}$ and
so there must be some $\gamma\in\mathsf{con}_{\vee}$ such that
$(\alpha_{+},b_{-})\sqsubseteq\gamma$. Because
$\beta_{+}\leq\alpha_{+}\leq\gamma_{+}$, by
($\mu_{+}$-$\mathsf{con}$-$\mathsf{tot}$), $b_{-}\leq\gamma_{-}\leq\beta_{-}$.
Finally, because $b_{-}\in\mathord{\downarrow}\mkern 1.0mu\alpha_{-}\cap
B_{-}$ was chosen arbitrarily, then also
$\alpha_{-}=\bigvee(\mathord{\downarrow}\mkern 1.0mu\alpha_{-}\cap
B_{-})\leq\beta_{-}$. ∎

##  Appendix B Missing proofs in Section 5

First, we prove general lemmas about a coproduct of frames
$\bigoplus_{i}L^{i}$.

######  Lemma 25.

Let $a,b\in L^{j},\,\\{a^{k}\\}_{k}\subseteq L^{j}$ and $u,v\in B$. Then,

  1. 1.

If $u\notin\mathbf{n}$, $\llbracket u\rrbracket\leq\llbracket v\rrbracket$ iff
$u\leq v$.

  2. 2.

$\llbracket-\rrbracket$ is injective on $B\setminus\mathbf{n}$.

  3. 3.

$(a\oplus_{j}u)\wedge(b\oplus_{j}u)=(a\wedge b)\oplus_{j}u$

  4. 4.

$\bigvee_{k}(a^{k}\oplus_{j}u)=(\bigvee_{k}a^{k})\oplus_{j}u$

###### Proof.

(1) is exactly Proposition IV.5.2.4 in [12]. (2) follows from (1). For (3),
recall that $\llbracket-\rrbracket$ is a meet-semilattice homomorphism, so
$(a\oplus_{j}u)\wedge(b\oplus_{j}u)=\llbracket
a*_{j}u\rrbracket\wedge\llbracket
b*_{j}u\rrbracket=\llbracket(a*_{j}u)\wedge(b*_{j}u)\rrbracket=\llbracket(a\wedge
b)*_{j}u\rrbracket=(a\wedge b)\oplus_{j}u$. Finally, for (4), by Proposition
IV.5.2.3 in [12], we know that in a coproduct of two frames we have

$\bigvee_{k}(a^{k}\oplus_{1}(1,b))=(\bigvee_{k}a^{k})\oplus_{1}(1,b)$

and we can view $\bigoplus_{i}L^{i}$ as a coproduct of two frames
$L^{j}\oplus(\bigoplus_{i\in\mathcal{I}\setminus\\{j\\}}L^{i})$. ∎

######  Lemma 26 (finite meets).

Let $\alpha^{j}=a^{j}\oplus_{i(j)}\overline{1}$, for $j=1,\dots,n$. Then,

$\bigwedge_{j=1}^{n}\alpha^{j}=\bigwedge_{i\in
I}(b^{i}\oplus_{i}\overline{1})=\bigcap_{i\in I}(b^{i}\oplus_{i}\overline{1})$

where $I=\\{i(j):j=1,\dots,n\\}$, $b^{i}=\bigwedge\\{a^{j}~{}|~{}i(j)=i\\})$.

Moreover, $\bigwedge_{j=1}^{n}\alpha^{j}=\llbracket
u\rrbracket=\mathord{\downarrow}\mkern 1.0muu\cup\mathbf{n}$ where
$u\in\prod^{\prime}_{i}L^{i}$ such that $(u)_{i}=b^{i}$ for every $i\in I$ and
$(u)_{i}=1$ otherwise.

###### Proof.

By Lemma 25, $\bigwedge_{j=1}^{n}\alpha^{j}=\bigwedge_{i\in
I}(b^{i}\oplus_{i}\overline{1})$ and, because meets of $\mathcal{C}$-ideals
are computed as their intersection (see Section 3.1),
$\bigwedge_{j=1}^{n}\alpha^{j}=\bigcap_{i\in I}(b^{i}\oplus_{i}\overline{1})$.
The ‘Moreover’ part follows from this representation. ∎

######  Lemma 27 (finite joins).

Let $\alpha^{j}=a^{j}\oplus_{i(j)}\overline{1}$, for $j=1,\dots,n$. Then,

$\bigvee_{j=1}^{n}\alpha^{j}=\bigvee_{i\in
I}(b^{i}\oplus_{i}\overline{1})=\bigcup_{i\in I}(b^{i}\oplus_{i}\overline{1})$

where $I=\\{i(j):j=1,\dots,n\\}$ and $b^{i}=\bigvee\\{a^{j}~{}|~{}i(j)=i\\}$.

###### Proof.

Let $\beta^{i}\overset{\text{\tiny def}}{\equiv}b^{i}\oplus_{i}\overline{1}$,
for every $i\in I$. First, we will show that $\bigcup_{i\in I}\beta^{i}$ is a
$\mathcal{C}$-ideal. Let $X=\\{x^{k}*_{l}u\\}_{k\in K}\subseteq\bigcup_{i\in
I}\beta^{i}$. Without loss of generality, assume that
$X\cap\mathbf{n}=\emptyset$, i.e. $u_{i}\not=0$, for all $i\not=l$, and that
$x^{k}\not=0$, for all $k\in K$. If $X\subseteq\beta^{i}$, for some $i$, then
also $\bigvee_{k\in K}x^{k}*_{l}u\in\beta^{i}$ because $\beta^{i}$ is a
$\mathcal{C}$-ideal. Otherwise, there must exist an $m\in K$ which is
different from $l$ such that $x^{m}*_{l}u\in\beta^{m}$. This means that
$(x^{m}*_{l}u)_{m}=u_{m}\leq b^{m}$. From this we have that, for all $k\in K$,
$(x^{k}*_{l}u)_{m}=u_{m}\leq b^{m}$ and, therefore, $x^{k}*_{l}u\in\beta^{k}$.
Again, because $\beta^{k}$ is a $\mathcal{C}$-ideal, $(\bigvee_{k\in
K}x^{k})*_{l}u\in\beta^{k}$.

Next, $\alpha^{j}\subseteq\beta^{i(j)}$, for all $j=1,\dots,n$, and so
$\bigcup_{j}\alpha^{j}\subseteq\bigcup_{i\in I}\beta^{i}$. Because
$\bigvee_{j=1}^{n}\alpha^{j}$ is the smallest $\mathcal{C}$-ideal containing
$\bigcup_{j}\alpha^{j}$ and $\bigcup_{i\in I}\beta^{i}$ is also a
$\mathcal{C}$-ideal, we get that
$\bigvee_{j=1}^{n}\alpha^{j}\subseteq\bigcup_{i\in I}\beta^{j}$. Finally,
every
$\beta^{i}\subseteq\bigvee\\{\alpha^{j}~{}|~{}i(j)=i\\}\subseteq\bigvee_{j=1}^{n}\alpha^{j}$
and so $\bigcup_{i\in I}\beta^{j}\subseteq\bigvee_{j=1}^{n}\alpha^{j}$. ∎

Now, let us look at the missing proofs from Section 5:

###### Proof of Lemma 17.

We prove that, for every $\alpha\in\mathsf{con}_{\vee}$, $\alpha=\bigvee_{i\in
I}\alpha^{i}$ for some $I\mathbin{\subseteq\\!^{\text{fin}}}\mathcal{I}$ and
$\alpha^{i}=(b_{+}^{i}\oplus_{i}\overline{1},\,b_{-}^{i}\oplus_{i}\overline{1})\in\mathsf{con}_{1}$
(or $\mathsf{tot}_{1}$) and from this the lemma follows.

Let $\bigvee_{j=1}^{n}\alpha^{j}\in\mathsf{con}_{\vee}$ where
$\alpha^{j}=(a_{+}^{j}\oplus_{i(j)}\overline{1},\,a_{-}^{j}\oplus_{i(j)}\overline{1})\in\mathsf{con}_{1}$,
for all $j=1,\dots,n$. From Lemma 26 and Lemma 27, we have that

$\bigvee_{j=1}^{n}\alpha^{j}=(\bigvee_{i\in
I}(b_{+}^{i}\oplus_{i}\overline{1}),\,\bigwedge_{i\in
I}(b_{-}^{i}\oplus_{i}\overline{1}))$

where $I=\\{i(j):j=1,\dots,n\\}$ and
$b^{i}_{+}=\bigvee\\{a^{j}~{}|~{}i(j)=i\\}$ and
$b^{i}_{-}=\bigwedge\\{a^{j}~{}|~{}i(j)=i\\}$. For every $i\in I$, because
($\mathsf{con}$-$\vee$) holds for $\mathcal{L}^{i}$,
$(b^{i}_{+},b^{i}_{-})\in\mathsf{con}^{i}$ and, therefore, also
$(b_{+}^{i}\oplus_{i}\overline{1},\,b_{-}^{i}\oplus_{i}\overline{1})\in\mathsf{con}_{1}$.
∎

###### Proof of Lemma 18.

Recall that, for every $i\in\mathcal{I}$, $\iota^{i}_{\pm}\colon
L^{i}_{\pm}\to\bigoplus_{i}L^{i}_{\pm}$, $a\mapsto a\oplus_{i}\overline{1}$,
is a frame homomorphism obtained as a composition
$\iota^{i}_{\pm}=\llbracket-\rrbracket_{\pm}\circ\kappa^{i}_{\pm}$ (see
Section 5.1). Here, $\kappa^{i}_{\pm}$ is always one-one and, because all
$L^{i}_{\pm}$’s are nontrivial,
$\kappa^{i}_{\pm}[L^{i}_{\pm}\setminus\\{0\\}]\cap\mathbf{n_{\pm}}=\emptyset$
and so, by Lemma 25, $\llbracket-\rrbracket_{\pm}$ is one-one when restricted
to image of $\kappa^{i}_{\pm}$. Therefore, $\iota^{i}$ is also one-one as it
is a composition of those two maps. Moreover, $\iota^{i}$ is also onto
$S^{i}_{\pm}$ and, because of Lemma 25,

$(a\oplus_{i}\overline{1})\wedge(b\oplus_{i}\overline{1})=(a\wedge
b)\oplus_{i}\overline{1}\quad\text{and}\quad\bigvee_{k}(a^{k}\oplus_{i}\overline{1})=(\bigvee_{k}a^{k})\oplus_{i}\overline{1}$

and so the associated inverse image map $(\iota^{i}_{\pm})^{-1}\colon
S^{i}_{\pm}\to L^{i}_{\pm}$ is also a frame homomorphism. Finally, from the
definitions

$\displaystyle(a,b)\in\mathsf{con}^{i}$
$\displaystyle\quad\text{iff}\quad(a\oplus_{i}\overline{1},\,b\oplus_{i}\overline{1})\in\mathsf{con}_{1}$
$\displaystyle(a,b)\in\mathsf{tot}^{i}$
$\displaystyle\quad\text{iff}\quad(a\oplus_{i}\overline{1},\,b\oplus_{i}\overline{1})\in\mathsf{tot}_{1}$

which makes $\iota^{i}$ restricted to the image, i.e. to
$S^{i}_{+}\mathord{\times}S^{i}_{-}$, an isomorphism of both structures. ∎

###### Proof of Theorem 24.

The last thing we need to check is universality of the construction. Let
$\mathcal{M}$ be a d-frame such that for every $j\in\mathcal{I}$ there is a
d-frame homomorphism $\lambda^{j}\colon\mathcal{L}^{j}\to\mathcal{M}$. We have
the following situation:

${\mathcal{L}^{j}}$${(\prod^{\prime}_{i}L^{i}_{+},\prod^{\prime}_{i}L^{i}_{-},\mathsf{con}_{1},\mathsf{tot}_{1})}$${\bigoplus_{i}\mathcal{L}^{i}}$${\mathcal{M}}$$\scriptstyle{\kappa^{j}}$$\scriptstyle{\lambda^{j}}$$\scriptstyle{\llbracket-\rrbracket}$$\scriptstyle{\lambda}$$\scriptstyle{\overline{\lambda}}$

We obtain $\lambda=(\lambda_{+},\lambda_{-})$ from the universal property of
the coproduct $\prod^{\prime}_{i}L^{i}_{\pm}$: because all
$\lambda^{j}_{\pm}$’s are meet-semilattice homomorphisms, $\lambda_{\pm}$ is
the unique meet-semilattice homomorphism such that
$\lambda^{j}_{\pm}=\lambda_{\pm}\circ\kappa^{j}_{\pm}$. Since all
$\lambda^{j}$ are d-frame homomorphisms, also $\lambda$ preserves
$\mathsf{con}_{1}$ and $\mathsf{tot}_{1}$ (follows immediately from the
definition). It also preserves the cover relations in the presentation of
d-frame coproducts (similarly to Proposition 4.3.2 in [12]):

$\displaystyle\bigvee_{k}\lambda_{\pm}(a^{k}*_{j}u)$
$\displaystyle=\bigvee_{k}\lambda_{\pm}((a^{k}*_{j}\overline{1})\wedge(1*_{j}u))\overset{(1)}{=}\bigvee_{k}(\lambda_{\pm}(a^{k}*_{j}\overline{1})\wedge\lambda_{\pm}(1*_{j}u))$
$\displaystyle=(\bigvee_{k}\lambda_{\pm}(a^{k}*_{j}\overline{1}))\wedge\lambda_{\pm}(1*_{j}u)$
$\displaystyle\overset{(2)}{=}\lambda_{\pm}((\bigvee_{k}a^{k})*_{j}\overline{1})\wedge\lambda_{\pm}(1*_{j}u)\overset{(1)}{=}\lambda_{\pm}((\bigvee_{k}a^{k})*_{j}u)$

Where (1)’s hold because $\lambda_{\pm}$ is a meet-semilattice homomorphism
and (2) holds because $\lambda^{j}_{\pm}$ is a frame homomorphism and so
$\bigvee_{k}\lambda_{\pm}(a^{k}*_{j}\overline{1})=\bigvee_{k}\lambda_{\pm}(\kappa^{j}_{\pm}(a^{k}))=\bigvee_{k}\lambda^{j}_{\pm}(a^{k})=\lambda^{j}_{\pm}(\bigvee_{k}a^{k})=\lambda_{\pm}(\kappa^{j}_{\pm}(\bigvee_{k}a^{k}))=\lambda^{j}_{\pm}((\bigvee_{k}a^{k})*_{j}\overline{1})$.
Therefore, $\lambda$ preserves $\bigoplus_{i}\mathcal{L}^{i}$ presentation
and, by Lemma 3, it can be uniquely extended to a d-frame homomorphisms
$\overline{\lambda}$. ∎