# Coalgebraic Completeness-via-Canonicity

Fredrik Dahlqvist

► To cite this version:

Fredrik Dahlqvist. Coalgebraic Completeness-via-Canonicity. 13th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Apr 2016, Eindhoven, Netherlands. pp.174-194, 10.1007/978-3-319-40370-0_11. hal-01446026

HAL Id: hal-01446026

https://inria.hal.science/hal-01446026

Submitted on 25 Jan 2017

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Coalgebraic completeness-via-canonicity.

Fredrik Dahlqvist

University College London

**Abstract.** We present the technique of completeness-via-canonicity in a coalgebraic setting and apply it to both positive and boolean coalgebraic logics with relational semantics.

# 1 Introduction

Coalgebraic logic has been very successful at unifying the multitude of modal logics used to describe and specify state-based systems, both semantically and syntactically (see e.g. [CKP$^+$09,KP11]). One of the great insights of coalgebraic logics is that there exists a close correspondence between the coalgebraic semantics and *rank 1 axiomatizations*, i.e. axioms with nesting depth of modal operators uniformly equal to 1. For a *Set*-endofunctor $T$ the class of all $T$-coalgebras can be characterised logically in rank 1 (see [Sch06]). Conversely, given a modal logic axiomatized in rank 1, there exist a *Set*-endofunctor $T$ such that the logic is strongly complete with respect to the class of all $T$-coalgebras (see [SP10]). However, one is often interested in providing a sound and complete semantics to modal logics which are known to include axioms of rank greater than one. Most temporal logics for example (see [Gol92]) contain such axioms. Alternatively, one may have a rank 1 axiomatization of the class of $T$-coalgebras for a functor $T$ of particular interest, and be interested in logically carving out important proper sub-classes of $T$-coalgebras, which may very well require axioms with nested modalities, for example the axiomatization of transitive Kripke frames by the axiom $\Diamond\Diamond p \rightarrow \Diamond p$.

Very little is known about the question of completeness for coalgebraic logics with axioms of arbitrary rank. To our knowledge, the only results in this direction are the work of Pattinson and Schröder in [PS08] as well as our previous work in [DP13] which dealt with the $\nabla$ formalism of coalgebraic logic and [DP15a] which focused on a coalgebraic account of distributive substructural logics. In what follows we will present the general principles of *coalgebraic completeness-via-canonicity*, a method for proving strong completeness of coalgebraic logics with axioms of arbitrary rank, in as much abstraction and generality as possible. To this end we will use the abstract presentation of coalgebraic logic (see e.g. [KKP04, KKP05, JS10, KP11]) which can be summarized by the following *fundamental diagram*:

<figure><img src="image_2.png" /></figure>
where $\mathcal{C}$ is the category in which 'modal formulas' are built from the functor $L$
and interpreted in $T$-coalgebras over 'carriers' in $\mathcal{D}$. We must however be careful:
in this abstract formulation coalgebraic logic is extremely general indeed, and
the notion of *canonical extension* (and thus of *canonicity*) does not in general
make sense in the base category $\mathcal{C}$ on which the logic is defined. We therefore
need to restrict our attention to base categories whose objects have a notion
of canonical extension. This presents us with a conceptual restriction which
in practice is harmless since all examples of coalgebraic logics are based on
a category with a good notion of canonical extension, viz. the categories **BA**
of boolean algebras, **DL** or distributive lattice, or **MSL** of meet semilattices
(see [JS10] for an example of meet semilattice-based coalgebraic logic, and see
[GP14] for a discussion of canonical extensions in **MSL**). A second restriction
comes from the fact that canonicity must spontaneously appear from the diagram
above, in the sense that for any $\mathcal{C}$-object $A$, the canonical extension of $A$ must be
representable as $GFA$. This condition is more restrictive. In the case of boolean
logics, this poses no problem: if we take $\mathcal{D} = \mathbf{Set}$ and the usual adjunction $F =$
$Uf \dashv P = G$ between the ultrafilter and powerset functors then $\mathcal{P}UfA$ is indeed
the canonical extension of $A$. However, in the case of positive coalgebraic logics
this requirement precludes the use of **Set**-based models for positive coalgebraic
logics, and we have to take $F = \mathbf{Pf} : \mathbf{DL} \to \mathbf{Pos}^{\mathrm{OP}}$ the prime filter functor and
$G = \mathcal{U} : \mathbf{Pos}^{\mathrm{OP}} \to \mathbf{DL}$ the upsets functor to represent the canonical extension of a
distributive lattice $A$ as $\mathcal{U}\mathbf{Pf}A$. The situation for **MSL**-based logics is much more
involved. The canonical extension of general semilattices is described in [GP14],
however no adjunction $F \dashv G$ between **MSL** and a category $\mathcal{D}^{\mathrm{OP}}$ emerges as a
'natural' way of building it. A duality theory for *distributive meet-semilattices*
is given in [BJ11]. It consists in building a distributive lattice $D(A)$ from a
distributive semilattice $A$ and then applying the usual functor $\mathbf{Pf}$. It follows
from the construction of [BJ11] that $F = \mathbf{Pf} \circ D \dashv U \circ \mathcal{U} = G$ (where $U$ is
the obvious forgetful functor), but we have not investigated if $GFA$ is then the
canonical extension of $A$ as described in [GP14]. We will therefore restrict our
attention to logics based on the category **DL** of which boolean logics (based on
**BA**) are a special case.

Having established the scope of logics which coalgebraic completeness-via-cano-
nicity can hope to tackle a priori, we must make the following remark about what
can be achieved in practice. Questions of canonicity are very hard; in general it
is undecidable whether a given formula is canonical, and establishing that a par-
ticular class of formulas is canonical is almost always highly non-trivial. What
we will present in this paper is a general coalgebraic template which avoids
these hard questions altogether, a conceptual roadmap of how the technique of
completeness-via-canonicity works in coalgebraic logic. To actually prove com-
pleteness of a particular coalgebraic logic with a particular coalgebraic semantic
means implementing the technique, at which point the hard work begins.

So why choose the technique of completeness-via-canonicity to prove complete-
ness if implementing it is so difficult? First of all, much of the implementation
has been done for many well-known logics and as we will show, we now have
a complete theory for all positive or boolean logics with a relational seman-
tics. Secondly, because of all the methods for proving completeness in modal
logic, it is probably the best suited to being generalized to coalgebraic logic
since it has a very clean and abstract algebraic formulation which connects in a
very generic fashion to the coalgebraic semantics via the well-established coalge-
braic Jónsson-Tarski theorem (see [KKP05,SP09,KR12]). Moreover, we believe
that generalising completeness-via-canonicity to coalgebraic logics also greatly
clarifies the technique itself. The connection between the syntactic/algebraic
part of the method on one side, viz. canonical extensions and canonical equa-
tions, and the semantics/coalgebraic part of the method on the other side, viz.
the construction of ‘canonical models’, is greatly clarified by the abstracting
power of coalgebraic logics and its semantics. Another advantage of coalgebraic
completeness-via-canonicity is that it applies equally well to positive coalgebraic
logics (see [KKV12]). In fact, since the traditional boolean setting is a special case
of the more general setting of positive coalgebraic logics, we will formulate most
results in terms positive coalgebraic logics. A final advantage of the technique
its *modularity*: we can combine strongly complete logics to create new strongly
complete logics in a completely mechanical way (in the spirit of [CP07,DP11]).
This work is in many ways a continuation and generalisation of the author’s
previous work with his PhD supervisor Dirk Pattinson ([DP13]). The paper will
be structured as follows. We start by presenting coalgebraic logics in its ‘abstract’
flavour. In Section 3 we describe the semantics/coalgebraic side of completeness-
via-canonicity, whilst Section 4 will deal with the syntactic/algebraic side of
the technique. Section 5 will show how and when the algebraic and coalgebraic
halves of the method can be combined, and strong completeness proved. We will
use the example of (positive) modal logic to illustrate every important concept,
and conclude with an application to ‘positive separation logics’.

2 Preliminaries

**Coalgebraic logics** require seven mathematical entities, six of which we intro-
duced in the *fundamental diagram* (1). These six entities are:

(1) a ‘*minimal reasoning structure*’ in the form of a category $\mathcal{C}$ whose objects are endowed with the fundamental logical operations we wish to take for granted. Due to the algebraic nature of $\mathcal{C}$-objects, we will assume throughout that there exist a free-forgetful adjunction $F \dashv U$ between **Set** and $\mathcal{C}$ (note the sans-serif font for the free functor). We will take $\mathcal{C}$ to be **DL**, **BDL** or **BA**, the categories of distributive lattices, bounded distributive lattices or boolean algebras with the obvious morphisms.

(2) a ‘minimal modelling structure’ in the form of a category $\mathcal{D}$ whose objects have the structure we wish the carriers of models to have. In our examples we will take $\mathcal{D}$ to be either **Pos** or **Set**, the category of posets and monotone functions or sets and functions.

(3)-(4) two functors $F : \mathcal{C} \to \mathcal{D}^{\text{op}}$ and $G : \mathcal{D}^{\text{op}} \to \mathcal{C}$ forming a dual adjunction $F \dashv G$ relating the world of syntax to the world of semantics. In the examples
we will take $F = \text{Pf} : \mathbf{DL} \to \mathbf{Pos}^{\text{op}}$ the functor sending a distributive lattice to the poset of its prime filters and $\mathbf{DL}$-morphisms to their inverse images, and $G = \mathcal{U} : \mathbf{Pos}^{\text{op}} \to \mathbf{DL}$ the functor sending a poset to the distributive lattice of its upsets and monotone maps to their inverse images. An important special case of the adjunction $\text{Pf} \dashv \mathcal{U}$ is its restriction $\text{Uf} \dashv \mathcal{P}$ to boolean algebras and sets: since prime filters are maximal in boolean algebras – i.e. ultrafilters (hence the ultrafilter functor $\text{Uf}$), their posets are trivial and thus simply form sets; upsets of trivial posets are simply subsets (hence the powerset functor $\mathcal{P}$).

(5) a syntax building functor $L : \mathcal{C} \to \mathcal{C}$ which specifies how to build ‘modal algebras’, and in particular how to build modal formulas.

(6) a model building functor $T : \mathcal{D} \to \mathcal{D}$ which specifies the kind of transition structure we want our models to have.

**Languages, logics and free algebras.** As will be illustrated in the examples, $L$ can specify much more than a grammar, it can also enforce axioms. What is included in $L$ is a matter of convenience, but as we shall see, including some axioms – specifically *distribution laws* – is a good idea. The distinction between *language* and *logic* therefore becomes blurred, and indeed may not be terribly useful in this presentation of coalgebraic logics. The relevant notion is that of a *free L-algebra*. For our purpose it will be enough to say that the free $L$-algebra over a $\mathcal{C}$-object $A$, written as $F_L A$, is the initial $L(-) + A$ algebra. We will assume throughout that these algebras exist, i.e. that $L$ is a *varietor*, and focus on a particular choice of objects in $\mathcal{C}$, namely those which are themselves free objects (recall that we assume a free-forgetful adjunction between **Set** and $\mathcal{C}$). For example, if $\mathcal{C} = \mathbf{DL}$ and $V$ is a set of propositional variables, we will consider the free $L$-algebra over the free distributive lattice over $V$, i.e. we will consider $L$-algebras of the type $F_L FV$. These are the entities which play the role of *language* since their carriers contain terms freely built from propositional variables, modulo the axioms of $\mathcal{C}$ and those encoded in $L$. In particular, it is the elements of these algebras which we will want to *interpret*.

**Coalgebraic semantics.** Terms in a free $L$-algebra are interpreted as ‘predicates’ on the carriers of $T$-coalgebras. The exact meaning of the word ‘predicate’ is specified by the functor $G$ which maps the carrier of a $T$-coalgebra to a $\mathcal{C}$-structure whose elements are by definition the predicates. An interpretation is thus a map from terms over $V$, viz. elements $F_L FV$, to predicates on $X$, viz. elements of $GX$. We produce such an map by equipping $GX$ with an $L(-) + FV$-algebra structure and using the *initiality* of $F_L FV$ amongst $L(-) + FV$-algebras. By definition of the coproduct, to define a morphism $LGX + FV \to GX$ we need:

1. a morphism of the type $FV \to GX$, and

2. a morphism of the type $LGX \to GX$

By adjunction any morphism of the type $FV \to GX$ is equivalent to a map $V \to UGX$ interpreting each propositional variable as a predicate, i.e. a *valuation* $v: V \to UGX$. The second morphism deals with modal terms whose interpretation should depend on the transition structure $\gamma: X \to TX$. To encode this
dependency we make the second morphism factor through $G\gamma : GTX \to GX$. What we therefore need is a morphism $\delta_X : LGX \to GTX$ for any $\mathcal{D}$-object $X$. Moreover, if $\beta : Y \to TY$ is another $T$-coalgebra and $f : Y \to X$ is a $T$-coalgebra morphism, it is not hard to check that the unicity of catamorphisms enforces $G\beta \circ GTf \circ \delta_X = G\beta \circ \delta_Y \circ LGf$. In fact we assume the somewhat stronger condition that the maps $\delta_X$ in fact define a natural transformation $\delta : LG \to GT$. This natural transformation will be called the semantic transformation and is the final necessary ingredient of coalgebraic logics. Given a semantics transformation and a valuation we define the interpretation of 'formulas' of $F_LFV$ in $\gamma : X \to TX$ as the catamorphism $\llbracket - \rrbracket_{(\gamma, v)}$ given by:

<figure><img src="image_3.png" /></figure>

**Modularity.** Coalgebraic logics defined on a common minimal reasoning structure can be freely combined to form new logics combining the modalities of their constituents in a process called the *fusion* of modal logics (see [CP07,DP11]). Formally, if $L_1, L_2 : \mathcal{C} \to \mathcal{C}$ are two syntax constructors, then the *fusion* of $F_{L_1}FV$ and $F_{L_2}FV$ is the language defined by the (point-wise) coproduct of these functors, i.e. $F_{L_1+L_2}FV$. Assuming that free $L_i$-algebras are interpreted in $T_i$-coalgebras via a semantics transformation $\delta_i$ for $i = 1, 2$, we can combine the semantics in a dual way to the syntax by interpreting free $L_1 + L_2$-algebras in $T_1 \times T_2$-coalgebras via the semantics transformation $G\pi_1 \circ \delta_1 + G\pi_2 \circ \delta_2$ where $\pi_1, \pi_2$ are the usual projections from a product.

*Example 1* ((Positive) Modal Logic). Standard Modal Logic, henceforth ML, is boolean and we therefore choose **BA** as our minimal reasoning structure. The syntax building functor is $L^{\text{ML}} : \mathbf{BA} \to \mathbf{BA}$ defined by:

$$L^{\text{ML}}A = F\{\diamond a \mid a \in UA\} / \{\diamond(a \lor b) = \diamond a \lor \diamond b, \diamond \perp = \perp\}$$

i.e. $L^{\text{ML}}$ builds the free boolean algebra over the formal expressions $\diamond a$ with $a \in A$, and then quotients this object by the fully invariant equivalence relation (in **BA**!) generated by the distribution laws above. We will show how $L^{\text{ML}}A$ can be defined categorically in Section 4. An $L^{\text{ML}}$-algebra is a boolean algebra with operator, i.e. a boolean algebra together with a unary operation which distributes over joins. Given a set $V$ of propositional variables, the object representing the language of ML will be $F_{L^{\text{ML}}}FV$, the colimit of the diagram

$$2 \xrightarrow{c_0} L^{\text{ML}}2 + FV \xrightarrow{c_1=L^{\text{ML}}(c_0)+\text{Id}_{FV}} L^{\text{ML}}(L^{\text{ML}}2 + FV) + FV \dots$$

where $2 = \{\perp, \top\}$ is the initial object in **BA**. The $L^{\text{ML}}$-algebra $F_{L^{\text{ML}}}FV$ thus contains all terms which can be built from elements of $V, \top, \perp, \neg, \lor, \land$ and $\diamond$
modulo the axioms of **BA** and the distribution laws encoded in $L^{\text{ML}}$. For the semantics we take $T = \mathbf{P}$, the *covariant* powerset functor on **Set**, and the transformation $\delta: LP \to PP$ given at any set $X$ and generator $\diamond U \in L^{\text{ML}}PX$ by:

$$ \delta_X^{\text{ML}}(\diamond U) = \{V \subseteq X \mid U \cap V \neq \emptyset\} $$

It is clear that $\delta_X(\diamond(U_1 \cup U_2)) = \delta_X(\diamond U_1 \cup \diamond U_2)$ and $\delta_X(\diamond\emptyset) = \delta_X(\emptyset)$, and $\delta_X$ is thus well-defined. $\mathbf{P}$ and $\delta$ give the standard Kripke semantics of ML, the only difference being that here we interpret equivalence classes of formulas.

*Mutantis mutandis* we can perform the exact same construction for positive ML. The minimal reasoning structure becomes either **DL** or **BDL** depending on whether we want $\top$ and $\bot$ or not, and due to the lack of negation one needs to introduce the dual operator $\Box$ explicitly. The functor becomes $L^{\text{ML}}: \mathbf{DL} \to \mathbf{DL}$

$$ L^{\text{ML}}A = F\{\diamond a, \Box a \mid a \in UA\} / \{\diamond(a \lor b) = \diamond a \lor \diamond b, \Box(a \land b) = \Box a \land \Box b\} $$

In the case of **BDL** one also adds $\diamond \bot = \bot$ and $\Box \top = \top$ to the equations defining the quotient. The construction of the language $F_{L^{\text{ML}}FV}$ is exactly the same as in the boolean case, with the caveat that the initial object in **DL** is the empty distributive lattice $\emptyset$. On the semantics side we need to find an equivalent of the covariant powerset for **Pos**. This is not entirely straightforward, but as was persuasively argued in Example 5.3 of [VK11] and in [BKV13], the **Pos** equivalent of $\mathbf{P}$ is the *convex powerset functor* $P_c: \mathbf{Pos} \to \mathbf{Pos}$ sending a poset to the set of its convex subsets ordered by the Egli-Milner order. Since we are not yet enforcing any relation between $\diamond$ and $\Box$, we interpret positive ML in $T^{\text{ML}}$-coalgebras for the functor $T^{\text{ML}} = P_c \times P_c$ (one copy of $P_c$ per modality). The semantics transformation $\delta^{\text{ML}}: L^{\text{ML}}\mathcal{U} \to \mathcal{U}(P_c \times P_c)$ is then defined as:

$$ \delta_X^{\text{ML}}(\diamond U) = \{(V_1, V_2) \mid U \cap V_1 \neq \emptyset\} $$

$$ \delta_X^{\text{ML}}(\Box U) = \{(V_1, V_2) \mid V_2 \subseteq U\} $$

and it is not hard to check that $\delta_X$ is well-defined, although interestingly this relies heavily on the definition of the Egli-Milner order, confirming the choice of $P_c$ as the 'correct' generalization of $\mathbf{P}$.

## 3 Strong completeness and Jónsson-Tarski Extensions

We have seen how important the 'predicate' functor $G: \mathcal{P}^{\text{OP}} \to \mathcal{C}$ is to define the coalgebraic semantics but have so far ignored its left-adjoint $F: \mathcal{C} \to \mathcal{P}^{\text{OP}}$. The intuition behind $F$ is that it sends a reasoning structure to 'states' on this structure, where a 'state' is a collection of elements structured in such a way that it may be understood as a consistent set of logical terms which can simultaneously hold at some point in a model. A coarse description of the semantic half of completeness-via-canonicity, which we present in this section, is that it consists in equipping a (po)set of such states with the target coalgebraic structure, i.e. in building models on collections of algebraic terms. Formally, starting from a $\mathcal{C}$-object $A$ with an $L$-algebra structure, we want to place a $T$-coalgebra structure
adjoint semantic transformation also requires the PIT or the AC, which makes these models deeply non-canonical. It follows from the unicity of catamorphisms that if $\hat{\delta}_{F_L FV}$ has a right-inverse $\zeta_{F_L FV}$ then the interpretation map in

$$Pf_F L FV \to Pf_L F_L FV \xrightarrow{\zeta_{F_L FV}} TPf_F L FV$$

is given by Diagram (2), in other words $[[\cdot]]_{Pf_F L FV} = \eta_{F_L FV}$. Modal logicians refer to this as the truth lemma: a formula $a$ holds at a prime filter $w$ in a ‘canonical model’ iff $a \in w$, by definition of $\eta$.

**The case of boolean coalgebraic logics.** In practice, when $\mathcal{C} = \mathbf{DL}$, right-inverses to adjoint semantic transformations must be built explicitly, and in fact this is also done in the construction of the standard ‘canonical’ model of ML. However, when the minimal reasoning structure is **BA** the criterion for the existence of Jónsson-Tarski extensions can be simplified somewhat, at the cost of being even less constructive. Assuming the axiom of choice all epimorphisms in **Set** are split, i.e. all surjections have a right inverse. For boolean coalgebraic logics, it is therefore sufficient to require that $\hat{\delta}$ be a pointwise epimorphism, and useful criteria for this to happen have been developed in [SP09,KR12,Dah15].

**Strong completeness.** The main application of Jónsson-Tarski extensions is to prove strong completeness. Let us first define precisely what we mean by strong completeness. Let $\mathcal{C}$ be $\mathbf{DL}$, $\mathbf{BDL}$ or **BA**, let $V$ be a set of propositional variables, let $q : F_L FV \to \mathcal{L}$ be a regular epi, and let $\Phi, \Psi \subseteq \mathcal{L}$ be two families of ‘formulas’ such that $\Phi \upharpoonright \Psi$, i.e. such that no finite set $\Phi_0$ of elements of $\Phi$ and no finite set $\Psi_0$ of elements of $\Psi$ can be found such that $\bigwedge \Phi_0 \leq \bigvee \Psi_0$. The statement that $\mathcal{L}$ is strongly complete w.r.t. to a class $\mathfrak{T}$ of T-coalgebras means that for any such choice of $\Phi, \Psi$ there exists a T-coalgebra $\gamma : X \to TX$ in $\mathfrak{T}$, a valuation $v : FV \to GX$, and a point $x \in X$ such that $x \in [[a]]_{(\gamma,v)}$ for all $a \in \Phi$ and $x \notin [[b]]_{(\gamma,v)}$ for all $b \in \Psi$.

**Theorem 2 (Strong completeness).** If the adjoint semantic transformation $\hat{\delta}$ has a right-inverse $\zeta_{F_L FV}$ at $F_L FV$, then $F_L FV$ is strongly complete w.r.t. to the class $\mathbf{Coalg}_{\mathcal{D}}(T)$ of T-coalgebras.

*Proof.* Let $\Phi, \Psi \subseteq F_L FV$ and $\Phi \upharpoonright \Psi$. Then the filter $\langle\Phi\rangle^\uparrow$ generated by $\Phi$ and the ideal $\langle\Psi\rangle^\downarrow$ generated by $\Psi$ obey $\langle\Phi\rangle^\uparrow \cap \langle\Psi\rangle^\downarrow = \emptyset$. By the PIT there exists a prime filter $w_\Phi$ extending $\langle\Phi\rangle^\uparrow$ such that $w_\Phi \cap \langle\Psi\rangle^\downarrow = \emptyset$. By Theorem 1, the $L$-algebra $F_L FV$ has a Jónsson-Tarski extension which provides an interpretation of $F_L FV$ in the $T$-coalgebra $Pf_F L FV \to Pf_L F_L FV \xrightarrow{\zeta_{F_L FV}} TPf_F L FV$, which coincides with $\eta_{F_L FV}$. In this interpretation $w_\Phi \in [[a]]$ for all $a \in \Phi$ and $w_\Phi \notin [[b]]$ for all $b \in \Psi$.

Jónsson-Tarski extensions, and thus strong completeness, are modular:

**Theorem 3 ([DP15b]).** Let $L_i : \mathcal{C} \to \mathcal{C}, T_i : \mathcal{D} \to \mathcal{D}, \delta^i : L_i G \to GT_i, i = 1, 2$. For any $\mathbf{Alg}_\mathcal{C}(L_1 + L_2)$-object $(A, \alpha)$, if $\hat{\delta}_A^i$ has a right-inverse $\zeta_A^i, i = 1, 2$, then $\eta_A : A \to GFA$ lifts to an $L_1 + L_2$-algebra morphism.

In a nutshell, the purpose of coalgebraic completeness-via-canonicity is to determine how and when Theorem 2 resists to quotienting $F_L FV$.
*Example 2.* The PIT-based technique of [DP15a] becomes particularly simple for unary operators and shows that the adjoint transformation $\delta^{\text{ML}}: T^{\text{ML}}\text{Pf} \to \text{PfL}^{\text{ML}}$ of the semantic transformation defined in Example 1 has right-inverses $\zeta_A^{\text{ML}}: \text{PfL}^{\text{ML}}A \to T^{\text{ML}}\text{PfA}$ at every $A$ in **DL** given by:

$$ \zeta_A^{\text{ML}}(F) = (\{F_1 \mid a \in F_1 \Rightarrow \diamond a \in F\}, \{F_2 \mid \Box a \in F \Rightarrow a \in F_2\}) $$

The (positive) language for ML defined by the functor $L^{\text{ML}}$ is thus strongly complete w.r.t. $P_c \times P_c$-coalgebras. We will show later that quotienting this language by the axioms relating $\diamond$ and $\Box$ defines a variety closed under Jónsson-Tarski extension. Strong completeness with respect to $P_c$-coalgebras interpreting both modalities by the same relation will then follow (modulo two lemmas).

# 4 Canonical equations and canonical extensions of L-algebras

In the previous section we have shown how to construct coalgebraic models whose carriers are the ‘states’ $FA$ of an $L$-algebra $A$ in a way that provides an $L$-algebra embedding of $A$ into $GFA$. When $\mathcal{C} = \text{DL}$ (or $\text{BDL}$ or $\text{BA}$) and $F \vdash G$ is the adjunction $\text{Pf} \vdash \mathcal{U}$, objects of the form $GFA$ are very well-known to algebraists studying boolean algebras and distributive lattices, and are known as *canonical extensions* and denoted $A^\sigma$. Motivated by the algebraic semantics of modal logic, this notion was extended to boolean algebra with operators (BAOs) [JT51] and distributive lattice expansions (DLEs) [GJ94,GJ04]. One of the key areas of research in this domain is to find conditions under which the validity of an equation in an BAO or a DLE can be transferred to its canonical extension, i.e. conditions under which $A \models s = t$ implies $A^\sigma \models s = t$. Such equations are called *canonical*. In this section we will review the basic facts about canonical equations and about a topological technique for establishing the canonicity of equations. As a by-product of this theory we will give a theoretically partial but practically complete answer to the following question:

*For which functors $L: \text{DL} \to \text{DL}$ does the canonical extension construction in $\text{DL}$ lift to $\text{Alg}_{\text{DL}}(L)$?*

**Canonical extensions of DLs.** For any $A$ in $\text{DL}$, $\mathcal{U}\text{PfA}$ is known as the *canonical extension* of $A$ and denoted $A^\sigma$. It can be characterised uniquely up to isomorphism through purely algebraic properties, namely that $A$ is *dense* and *compact* in $A^\sigma$. In this sense the adjective ‘canonical’ is fully justified, in contrast with its usage in the expression ‘canonical model’. For our purpose however, *defining* the canonical extension of $A$ as $\mathcal{U}\text{PfA}$ will be sufficient. The canonical extension $A^\sigma$ of a distributive lattice $A$ is always *completely distributive* (see [GJ04]). The following terminology will be important: $A^\sigma$ is a completion of $A$ and all joins of elements of $A$ therefore exist in $A^\sigma$, such elements are called *open* and their set is denoted by $O(A)$. Dually, meets in $A^\sigma$ of elements of $A$ will be called *closed* and their set denoted $K(A)$. Elements of $A = K(A) \cap O(A)$ are therefore called *clopens*.
**Canonical extension of DLEs.** It was shown in [JT51] that if A is a BA with a map $f: UA \to UA$ preserving joins then $A^\sigma = \mathcal{P}UfA$ can be equipped with a map $f^\sigma: UA^\sigma \to UA^\sigma$ which extends $f$ and preserves all non-empty joins. This construction was later extended to DLs with n-ary maps and no particular preservation properties in [GJ94,GJ04]. Formally, given a signature $\Sigma$ with arity map $\text{ar}: \Sigma \to \mathbb{N}$, define the syntax building functor $L_\Sigma: \mathbf{DL} \to \mathbf{DL}$ by:

$$L_\Sigma A = F\left(\prod_{s \in \Sigma} UA^{\text{ar}(s)}\right) \qquad (3)$$

An $L_\Sigma$-algebra is a distributive lattice with n-ary maps defined by the signature, i.e. a Distributive Lattice Expansion, or DLE for short. We now sketch the theory of their canonical extensions. Each map $f: UA^n \to UA$ can be extended to a map $(UA^\sigma)^n \to UA^\sigma$ in two canonical ways:

$$f^\sigma(x) = \bigvee \{\bigwedge f[d, u] \mid K(A)^n \ni d \le x \le u \in O(A)^n\}$$

$$f^\pi(x) = \bigwedge \{\bigvee f[d, u] \mid K(A)^n \ni d \le x \le u \in O(A)^n\}$$

where $f[d, u] = \{f(a) \mid a \in A^n, d \le a \le u\}$. In many important cases, the two extensions (viz. $f^\sigma$ and $f^\pi$) agree, in which case $f$ is said to be smooth. We define the canonical extension of an $L_\Sigma$-algebra A as the $L_\Sigma$-algebra $A^\sigma$ defined by $(A^\sigma, (f_s^\sigma : (UA^\sigma)^{\text{ar}(s)} \to UA^\sigma)_{s \in \Sigma})$. This gives us a first class of functors $L$ which answers the question above: for any finitary signature $\Sigma$, the DL-endofunctor $L_\Sigma$ defined by Eq. (3) lifts canonical extensions from DL to Alg$_{DL}$(L_Σ).

**Topological methods** where introduced in [GJ04,Ven06] to study the canonical extension of maps. These methods are useful because they (a) uniquely characterize canonical extensions, (b) reflect interesting algebraic properties of maps (e.g. the preservation of meets) and, crucially (c) provide a very effective way of studying the composition of canonical extensions which is essential to establishing canonicity. We need six topologies on $A^\sigma$. First, we define $\sigma^\uparrow, \sigma^\downarrow$ and $\sigma$ as the topologies defined by the bases $\{\uparrow p \mid p \in K\}, \{\downarrow u \mid u \in O\}$ and $\{\uparrow p \cap \downarrow u, K \ni p, u \in O\}$. The next set of topologies is well-known to domain theorists: a Scott open in $A^\sigma$ is a subset $U \subseteq A^\sigma$ such that (1) $U$ is an upset and (2) for any up-directed set $D$ such that $\bigvee D \in U, D \cap U \neq \emptyset$. The collection of Scott opens forms a topology called the Scott topology, which we denote $\gamma^\uparrow$. The dual topology will be denoted by $\gamma^\downarrow$, and their join by $\gamma$. Since for every $x \in A^\sigma$, $x = \bigvee \downarrow x \cap K = \bigwedge \uparrow x \cap O$, it is easy to see that $\gamma^\uparrow \subseteq \sigma^\uparrow, \gamma^\downarrow \subseteq \sigma^\downarrow$, and $\gamma \subseteq \sigma$. We denote the product of topologies by $\times$, and the n-fold product by $(-)^n$.

**Proposition 1 ([GJ04]).** For any DL A and map $f: UA^n \to UA$,

1. $f^\sigma$ is the largest $(\sigma^n, \gamma^\uparrow)$-continuous extension of $f$,

2. $f^\pi$ is the smallest $(\sigma^n, \gamma^\downarrow)$-continuous extension of $f$

3. $f$ is smooth iff it has a unique $(\sigma^n, \gamma)$-continuous extension.

The following result which relates algebraic and topological properties, is a straightforward generalization of results from [GJ94,GH01,GJ04,Ven06].
**Proposition 2.** Let $A$ be a distributive lattice, and let $f : UA^n \to UA$ be a map. For any $(n-1)$-tuple $a = (a_i)_{1\le i\le n-1}$, we denote by $f_a^k : UA \to UA$ the map defined by $x \mapsto f(a_1, \dots, a_{k-1}, x, a_k, \dots, a_{n-1})$.

1. If $f_a^k$ preserves binary joins, $(f^\sigma)_a^k$ preserves all non-empty joins.

2. If $f_a^k$ preserves binary meets, $(f^\sigma)_a^k$ preserves all non-empty meets.

3. If $f_a^k$ anti-preserves binary joins, $(f^\sigma)_a^k$ anti-preserves all non-empty joins.

4. If $f_a^k$ anti-preserves binary meets, $(f^\sigma)_a^k$ anti-preserves all non-empty meets.

5. If $(f^\sigma)_a^k$ preserves all non-empty joins, it is $(\sigma^\downarrow, \sigma^\downarrow)$-continuous.

6. If $(f^\sigma)_a^k$ preserves all non-empty meets, it is $(\sigma^\uparrow, \sigma^\uparrow)$-continuous.

7. If $(f^\sigma)_a^k$ anti-preserves all non-empty joins, it is $(\sigma^\downarrow, \sigma^\uparrow)$-continuous.

8. If $(f^\sigma)_a^k$ anti-preserves all non-empty meets, it is $(\sigma^\uparrow, \sigma^\downarrow)$-continuous.

9. In each case $f_a^k$ is smooth.

Function composition and canonical extension interact in a non-trivial way, but the following consequence of Proposition 1 greatly clarifies their interaction. This result is our main tool for proving canonicity.

**Theorem 4 (Principle of Matching Topologies, [GH01,Ven06]).** Let $A$ be a DL, and $f : UA^n \to UA$ and $g_i : UA^{m_i} \to UA$, $1 \le i \le n$ be arbitrary maps. Assume that there exist topologies $\tau_i$ on $A$, $1 \le i \le n$ such that each $g_i^\sigma$ is $(\sigma^{m_i}, \tau_i)$-continuous. If $f^\sigma$ is

1. $(\tau_1 \times \dots \times \tau_n, \gamma^\uparrow)$-continuous, then $f^\sigma(g_1^\sigma, \dots, g_n^\sigma) \le (f(g_1, \dots, g_n))^\sigma,$

2. $(\tau_1 \times \dots \times \tau_n, \gamma^\downarrow)$-continuous, then $f^\sigma(g_1^\sigma, \dots, g_n^\sigma) \ge (f(g_1, \dots, g_n))^\sigma,$

3. $(\tau_1 \times \dots \times \tau_n, \gamma)$-continuous, then $f^\sigma(g_1^\sigma, \dots, g_n^\sigma) = (f(g_1, \dots, g_n))^\sigma.$

Monotone (i.e. isotone or antitone) maps have a nice property which complements the Principle of Matching Topologies very effectively. The proof of this property can already be found for isotone maps in [Rib52], and generalizes tediously but straightforwardly to monotone maps (i.e. either isotone or antitone).

**Proposition 3.** Let $g_i : (UA)^{n_i} \to UA$, $1 \le i \le m$ and $f : (UA)^m \to UA$ be monotone maps, then $(f(g_1, \dots, g_m))^\sigma \le f^\sigma(g_1^\sigma, \dots, g_m^\sigma)$.

**Canonicity.** Before we consider the canonical extension of more general L-algebras, we need to talk about canonicity. Let us fix a signature $\Sigma$. Recall that an equation $s = t$ in the language of $L_\Sigma$-algebras (i.e. DLEs with signature $\Sigma$) is *canonical* if it has the property that $A^\sigma \models s = t$ whenever $A \models s = t$. To say anything about the canonicity of equations, we therefore need to compare interpretations in $A$ with those in $A^\sigma$. It is natural to try to use the extension $(\cdot)^\sigma$ to mediate between these interpretations, but $(\cdot)^\sigma$ is defined on maps, not on terms. Moreover, not every valuation on $A^\sigma$ originates from valuation on $A$. We therefore want to recast the problem in such a way that (1) terms are viewed as maps, and (2) we do not need to worry about valuations. The solution is to adopt the language of *term functions* (as first suggested in [Jón94]). Let $\Sigma$ be a signature and $t$ be a term in the language $F_{L_\Sigma}FV$, there exist a finite set $V_0 = \{p_1, \dots, p_n\} \subseteq V$ containing the propositional variables of $t$. For any $L_\Sigma$-algebra $A$, we can put an $L_\Sigma(-) + FV_0$-algebra structure on the distributive lattice $A_n$ of $n$-ary maps on $A$ (with pointwise meets and joins) as follows:
- Define $v: V_0 \to UA_n, p_i \mapsto \pi_i$, the ith projection $(UA)^n \to UA$.

- For each $f \in \Sigma$, we overload and define $f : (UA_n)^{\mathrm{ar}(f)} \to UA_n$ by $(g_1, \dots, g_{\mathrm{ar}(f)}) \mapsto f \circ \langle g_1, \dots, g_{\mathrm{ar}(f)} \rangle$, where $\langle \cdot \rangle$ denotes the product.

By taking the adjoint transpose of these maps (i.e. freely extending) we equip $\mathcal{A}_n$ with the desired algebraic structure. We can now interpret a term $t$ as the term function $t^A : UA^n \to UA$ given by the catamorphism $\langle \cdot \rangle^A$:

$$ L_{\Sigma} F_{L_{\Sigma}} FV_0 + FV_0 \xrightarrow{L_{\Sigma}(\cdot)^A + \mathrm{Id}_{FV_0}} L_{\Sigma} \mathcal{A}_n + FV_0 \\ \downarrow \\ F_{L_{\Sigma}} FV_0 \xrightarrow{\langle \cdot \rangle^A} \mathcal{A}_n $$

For any two terms $s, t \in F_{L_{\Sigma}} FV$ we can take $V_0$ to be the set of propositional variables required to build both $s$ and $t$ and thus get a common catamorphism $\langle \cdot \rangle^A$ interpreting both terms as maps $(UA)^n \to UA$. It is then well-known and easy to check that $A \models s = t$ iff $s^A = t^A$. Following [Jón94], we say that $t \in F_{L_{\Sigma}} FV$ is stable if $(t^A)^\sigma = t^A$, that $t$ is expanding if $(t^A)^\sigma \le t^A$, and that $t$ is contracting if $(t^A)^\sigma \ge t^A$, for any $A$. The inequality between maps is taken pointwise. The following proposition illustrates the usefulness of these notions:

**Proposition 4 ([Jón94]).** If $s, t \in F_{L_{\Sigma}} FV$ are stable then $s = t$ is canonical. If $s$ is contracting and $t$ is expanding, then $s \le t$ is canonical.

In practice, we use the Principle of Matching Topologies (Theorem 4) to determine when a term is stable, expanding or contracting, and thus when equations or inequations are canonical.

**Canonical extension of L-algebras.** We now show that $L^{\mathrm{ML}}$ defined in Example 1 belongs to a general class of functors of the form $L_{\Sigma}/\{E\}$ for which the canonical extension construction always lifts to $\mathbf{Alg}_{\mathrm{DL}}(L)$. To categorically formalize functors of the type $L_{\Sigma}/\{E\}$ for a set $E$ of equations, we need to capture the notion of fully invariant equivalence relation generated by a set of equations. We will only sketch the construction which can be performed in great generality in any well-powered cocomplete regular category (see [Dah15], Chapter 1). Consider a set $E$ of equations in $F_{L_{\Sigma}} FV$ (e.g. $E = \{\diamond(a \lor b) = \diamond a \lor \diamond b, \diamond \perp = \perp\}$), it is equivalent to a pair of jointly monic functions $e_1, e_2 : E \twoheadrightarrow \mathcal{U}\mathcal{L}$ where $\mathcal{L}$ is the distributive lattice underlying the $L_{\Sigma}$-algebra $F_{L_{\Sigma}} FV$. By adjunction we can re-write this as a pair of morphisms $\hat{e}_1, \hat{e}_2 : \mathcal{F}\mathcal{E} \twoheadrightarrow \mathcal{L}$ where $\mathcal{F}\mathcal{E}$ is the ‘free DL of equations’. Consider the coequalizer $\mathcal{F}\mathcal{E} \twoheadrightarrow \mathcal{L} \xrightarrow{q} \mathcal{Q}$ of $\hat{e}_1, \hat{e}_2$ and all the terms $s, t \in \mathcal{L}$ such that $q(s) = q(t)$. They form an equivalence relation in DL (the kernel pair of $q$) containing $E$, but not a fully invariant one (e.g. $\diamond(c \lor d) = \diamond c \lor \diamond d$ for $c \ne a, d \ne b$ does not in general belong to this relation). To capture substitution instances we must consider a ‘bigger’ coequalizer, namely

$$ \coprod_{f \in \hom(\mathcal{L}, \mathcal{L})} L_{\Sigma} f \circ \phi^{-1} \circ \hat{e}_1 \xrightarrow{q_{\mathcal{L}}} L_{\Sigma} \mathcal{L} \xrightarrow{\mathcal{L}} L_{\Sigma} := L_{\Sigma}/\{E\}(\mathcal{L}) \quad (4) $$
where $\phi : L_{\Sigma}\mathcal{L} \to \mathcal{L}$ is the iso structure map of the free $L_{\Sigma}$-algebra. The pairs of terms $s, t$ such that $q(s) = q(t)$ now form a fully invariant equivalence relation in $\mathbf{DL}$. We nearly have a rigorous definition of functors of the shape $L_{\Sigma}/\{E\}$, the final step is to notice that (4) can to some extent be made parametric in the choice of the middle object. We define for any $A$ the coequalizer $q_A$:

$$ \coprod_{f \in \operatorname{hom}(\mathcal{L}, A)} \mathcal{L}_{\Sigma} f \circ \phi^{-1} \circ \hat{e}_1 \xrightarrow{q_A} \mathcal{L}_{\Sigma} A \xrightarrow{\coprod_{f \in \operatorname{hom}(\mathcal{L}, A)} \mathcal{L}_{\Sigma} f \circ \phi^{-1} \circ \hat{e}_2} \mathcal{L}_{\Sigma} A \quad (5) $$

It is easy to see that (5) defines a functor: for any $f : A \to B$, amongst the morphisms $\mathcal{L} \to L_{\Sigma}B$ are all the ones which factor through $L_{\Sigma}A$ via $L_{\Sigma}f$, and thus $LB$ is a co-cone for the diagram defining $LA$ and so there must exist a unique $Lf : LA \to LB$. For the same reason $LL$ is initial amongst all objects of the form $LA$ with $A$ in $\mathbf{DL}$. Any $L$-algebra $\alpha : LA \to A$ defines an $L_{\Sigma}$-algebra, i.e. a $\Sigma$-DLE, $\alpha \circ q_A : L_{\Sigma}A \to LA \to A$ which will call the associated $\Sigma$-DLE.

**Theorem 5 (Canonical extension lifting).** Let $\Sigma$ be a finitary signature, let $E$ be a set of equations between terms in $F_{L_{\Sigma}}FV$ of modal depth at most one and let $L : \mathbf{DL} \to \mathbf{DL}$ be defined by $LA = L_{\Sigma}/\{E\}(A)$ as in (5). If for any $L$-algebra $\alpha : LA \to A$, the $n$-ary maps of the associated $\Sigma$-DLE are monotone, then the canonical extension construction lifts from $\mathbf{DL}$ to $\mathbf{Alg}_{\mathbf{DL}}(L)$.

*Proof.* For any $\alpha : LA \to A$, the map $\phi = \alpha \circ q_A : L_{\Sigma}A \to LA \to A$ defines an $L_{\Sigma}$-algebra, and we know how to build the canonical extension of $L_{\Sigma}$-algebras. Let $\phi^{\sigma} : L_{\Sigma}A^{\sigma} \to A^{\sigma}$ be this canonical extension and let us define $\alpha^{\sigma} : LA^{\sigma} \to A^{\sigma}$ by $\alpha^{\sigma}(x) = \phi^{\sigma}(y)$ for $y \in q_{A^{\sigma}}^{-1}(x)$. We need to show that $\alpha^{\sigma}$ is well-defined, i.e. that if $q_{A^{\sigma}}(y) = q_{A^{\sigma}}(y') = x$ then $\phi^{\sigma}(y) = \phi^{\sigma}(y')$. Note that if it is the case, then it is immediate to check that $\alpha^{\sigma}$ is a $\mathbf{DL}$-morphism. If $q_{A^{\sigma}}(y) = q_{A^{\sigma}}(y')$ then there must exist a $z \in FE$ and $f \in \operatorname{hom}(\mathcal{L}, L_{\Sigma}A^{\sigma})$ such that $y = f \circ \hat{e}_1(z)$, $y' = f \circ \hat{e}_1(z)$. But we know that $\phi(g \circ \hat{e}_1(z)) = \phi(g \circ \hat{e}_2(z))$ for any $g \in \operatorname{hom}(\mathcal{L}, L_{\Sigma}A)$ by definition of $\phi$. This means that $(A, \phi) \models \hat{e}_1(z) = \hat{e}_1(z)$, and therefore if the equation is canonical we are done, for then $(A^{\sigma}, \phi^{\sigma}) \models \hat{e}_1(z) = \hat{e}_2(z)$, i.e. $\phi^{\sigma}(g \circ \hat{e}_1(z)) = \phi^{\sigma}(g \circ \hat{e}_2(z))$ for any $g \in \operatorname{hom}(\mathcal{L}, L_{\Sigma}A^{\sigma})$, and thus for $g = f$. The result thus amounts to showing that equations involving terms of modal depth at most one are canonical, and this will follow immediately from Proposition 4 if we can show that terms of modal depth at most one are stable. Let $A$ be in $\mathbf{DL}$ and $t \in F_{L_{\Sigma}}FV$ be a term of modal depth 0 built from propositional variables in $V_0 = \{p_1, \dots, p_n\}$. By distributivity, we can assume $t = \bigvee_{i=1}^{l} \bigwedge_{j=1}^{m_i} p_{k(i,j)}$ where $k$ picks for each $(i, j)$ the index of a variable in $V$. By definition

$$ t^A = \bigvee^A \circ \langle \wedge^A \circ \langle \pi_{k(1,1)}, \dots, \pi_{k(1,m_1)} \rangle, \dots, \wedge^A \circ \langle \pi_{k(l,1)}, \dots, \pi_{k(l,m_l)} \rangle \rangle $$

where $\bigvee^A : (UA)^l \to UA$ is the $l$-ary join in $A$, and similarly for every $\wedge^A$. Each $\pi_i^{\sigma} : (UA^{\sigma})^n \to UA^{\sigma}$ is $(\sigma^n, \sigma)$-continuous by definition of $\sigma^n$. Moreover, $\bigvee^{A^{\sigma}}$ and $\wedge^{A^{\sigma}}$ preserve meets and joins in every argument by distributivity, and are
thus $(\sigma^l, \sigma)$- and $(\sigma^{m_i}, \sigma)$-continuous respectively by Proposition 2. It follows that $t^{A^\sigma} = (t^A)^\sigma$ by the Principle of Matching Topologies. Assume now that $t$ is of modal depth 1, i.e. $t = \bigvee_{i=1}^n \bigwedge_{j=1}^{m_i} f_{ij}(a_{ij1}, \dots, a_{ijar(f_{ij})})$, where each $a_{ijk}$ is of modal depth 0. Since every extension $f_{ij}$ is assumed to be monotone, Proposition 3 implies that $(t^A)^\sigma \le t^{A^\sigma}$. So we need only show the reverse inequality. We have established above that each $a_{ijk}^{A^\sigma}$ is $(\sigma^n, \sigma)$-continuous, and by Proposition 1 $f_{ij}^{A^\sigma}$ is $(\sigma^{\mathrm{ar}(f_{ij})}, \gamma^\uparrow)$-continuous. Finally since $\vee^{A^\sigma}$ and $\wedge^{A^\sigma}$ preserve all joins they preserve up-directed ones and are thus $((\gamma^\uparrow)^k, \gamma^\uparrow)$-continuous. The result then follows from the Principle of Matching Topologies. A completely analogous proof can be shown to hold in boolean algebras by using the de Morgan laws and the antitone preservation properties of Proposition 2.

**Remark.** Not all sets $E$ of equations satisfying the conditions of Theorem 5 make sense, take for example $\Sigma = \{\diamond\}$ and $E = \{a = b, \diamond(c \vee d) = \diamond c \vee \diamond d\}$ with $a, b, c, d \in V$ all distinct. The equation $a = b$ is canonical: choose $V_0 = \{a, b, c, d\}$, then $a^A$ is simply the projection $\pi_1^A : A^4 \to A$ and $b^A$ is simply $\pi_2^A : A^4 \to A$ for any $L_\Sigma$-algebra $A$. It is easy to check from the definition that $(\pi_1^A)^\sigma = (\pi_1)^{A^\sigma}$, and similarly for $\pi_2^A$, so the terms are stable, and the equation canonical. But it is vacuously canonical: $\pi_1^A$ and $\pi_2^A$ are not equal.

**Remark.** As was mentioned earlier, [Sch06] shows that for a Set-endofunctor $T$, the class of all $T$-coalgebras can be characterized by axioms of modal depth one. From the point of view of coalgebraic logic, the only restrictive requirement of Theorem 5 is therefore that the expansions defined by such an axiomatization should be monotone. This however covers most coalgebraic logics, for example graded modal logic, probability logic, conditional logic, etc.

*Example 3.* It is clear from the definition of $L^{\mathrm{ML}}$ in Example 1 that $L^{\mathrm{ML}}$ satisfies the conditions of Theorem 5, i.e. canonical extensions lift to $\mathrm{Alg}_{\mathrm{DL}}(L^{\mathrm{ML}})$. In order to axiomatize the duality between $\diamond$ and $\Box$ in positive ML, one must enforce Dunn's *Interaction Axioms* on $L^{\mathrm{ML}}$-algebras ([Dun95]):

$$ \diamond a \wedge \Box b \le \diamond (a \wedge b), \quad \Box (a \vee b) \le \Box a \vee \diamond b $$

It follows from the proof of Theorem 5 that these inequations are also canonical.

# 5 Jónsson-Tarski vs canonical extensions.

Combining the results of Sections 2 and 3, we know that for logics defined by an endofunctor $L: \mathscr{C} \to \mathscr{C}$ satisfying the conditions of Theorem 5 and a semantic transformation $\delta: LG \to GT$ satisfying the conditions of Theorem 1, any $L$-algebra $\alpha: LA \to A$ has two extensions with a common carrier: the Jónsson-Tarski extension $\alpha^\zeta$ and the canonical extension $\alpha^\sigma$. There is no reason *a priori* for them to be isomorphic $L$-algebras, but it turns out that this is frequently the case in practice. It is in these instances that coalgebraic completeness-via-canonicity applies. For now though the situation is the following:
$$
\begin{tikzcd}[column sep=2.8em, row sep=2.8em]
    & LGFA \arrow[r, "\delta_{FA}", "\alpha^{\zeta}", "\eta_A"] \arrow[d, "\alpha"] & LA \arrow[r, "\eta_A", "\alpha"] \arrow[d, "\alpha"] & LA^{\sigma} \arrow[d, "\alpha^{\sigma}", "\eta_A"] \\
    LGFA \arrow[r, "\delta_{FA}", "\alpha^{\zeta}", "\eta_A"] & GTFA \arrow[d, "G\zeta_A"] & GFLA \arrow[d, "GF\alpha"] & GFA \arrow[r, "\delta_{FA}", "\alpha^{\zeta}", "\eta_A"]
\end{tikzcd}
\qquad (6)
$$

The left-hand side of Diagram (6) deals with the model-building part of coalgebraic completeness-via-canonicity, whilst the right-hand side of Diagram (6) deals with the algebraic part of the method.

**Theorem 6 (Coalgebraic Completeness-via-Canonicity).** Let $L : \mathbf{DL} \to \mathbf{DL}$ satisfy the conditions of Theorem 5 and $\delta : \mathcal{LU} \to \mathcal{UT}$ the conditions of Theorem 1. If $q : F_L FV \to \mathcal{L}$ is the quotient in $\mathbf{Alg}_{\mathbf{DL}}(L)$ of a fully invariant equivalence relation defining a variety closed under canonical extensions, and if the Jónsson-Tarski and canonical extensions coincide, then $\mathcal{L}$ is strongly complete w.r.t. the class of T-coalgebras validating all equations $s = t$ s.th. $q(s) = q(t)$.

*Proof.* For any $\Phi, \Psi \subseteq \mathcal{L}$ such that $\Phi \upharpoonright \Psi$ we can find a point in the coalgebra $\gamma : \mathbf{Pf}\mathcal{L} \to \mathbf{TPf}\mathcal{A}$ satisfying every formula in $\Phi$ and none of $\Psi$ exactly as in Theorem 2, but we must also check that this T-coalgebra validates all the equations $s = t$ where $s, t \in F_L FV$ and $q(s) = q(t)$. If $q(s) = q(t)$, then $(\mathcal{L}, \alpha) \models s = t$ by construction of $\mathcal{L}$. Since $\mathcal{L}$ belongs to the variety it defines (in fact it is its initial object), and since this variety is assumed to be closed under canonical extensions, it follows that $(\mathcal{L}^{\sigma}, \alpha^{\sigma}) \models s = t$. Finally, since the Jónsson-Tarski and canonical extensions coincide we have $(\mathcal{UPf}\mathcal{L}, \alpha^{\zeta}) \models s = t$ which means that $\llbracket s \rrbracket_{(\gamma,v)} = \llbracket t \rrbracket_{(\gamma,v)}$ for any valuation $v : FV \to \mathcal{UPf}\mathcal{L}$.

**Remark.** If $E$ is a set of equations between terms of $F_L FV$, then the quotient $q : F_L FV \to \mathcal{L}$ defined from $E$ in the fashion of Diagram (4) is usually called the *Lindenbaum-Tarski algebra of the logic defined by $L$ and $E$*.

**Remark.** We choose to require that a variety defined by a regular quotient of the free $L$-algebra should be canonical, i.e. closed under canonical extensions. This is strictly more general than requiring that a variety be defined by canonical equations (in which case it is also canonical). Indeed, as was shown in [HV05], there exist canonical varieties of BAOs with no canonical axiomatization.

**Remark.** In fact we could require less than a full isomorphism of $L$-algebras, what is really needed is the implication $(A^{\sigma}, \alpha^{\sigma}) \models s = t \Rightarrow (\mathcal{UPf}A, \alpha^{\zeta}) \models s = t$.

We now give a useful criterion for the Jónsson-Tarski and canonical extensions to be equal. Consider for a finitary signature $\Sigma$ a set $E$ of equations of the shape

$$
\left\{
\begin{array}{@{}l@{}}
  \{f(a_1, \dots, a_{i-1}, \bigwedge^{f,i} X, a_{i+1}, \dots, a_n) = \bigwedge_{b \in X}^{f,i} f(a_1, \dots, a_{i-1}, b, a_{i+1}, \dots, a_n) \mid \\
  \phantom{\{f(a_1, \dots, a_{i-1}, \bigwedge^{f,i} X, a_{i+1}, \dots, a_n) = \bigwedge_{b \in X}^{f,i} } f \in \Sigma, 1 \le i \le \mathrm{ar}(f), \bigwedge^{f,i}, \bigvee^{f,i} \in \{\bigwedge, \bigvee\}, X \in \mathcal{P}_f(F_{L_{\Sigma}} FV)\}
\end{array}
\right\}
\qquad (7)
$$
and let $L: \mathbf{DL} \to \mathbf{DL}$ be defined as $LA = L_{\Sigma}/\{E\}(A)$ as in Eq. (5). It is easy to see that for any $\alpha: LA \to A$, the associated $\Sigma$-DLE has $n$-ary expansions which (anti)-preserve meets or joins in each argument.

**Theorem 7.** Let $E$ be as in Eq. (7) and $LA = L_{\Sigma}/\{E\}(A)$. Let $E^{\infty}$ denote the set equations defined as (7) but with $\mathcal{P}_f(\mathbb{F}_{L_{\Sigma}}\mathbb{F}V)$ replaced by $\mathcal{P}(\mathbb{F}_{L_{\Sigma}}\mathbb{F}V)$. If at every $A$ in $\mathbf{DL}$ the adjoint transformation $\hat{\delta}$ of $\delta: LU \to UT$ has a right-inverse $\zeta_A$ and $\delta_{\mathbb{P}_fA} \circ q_A$ coequalizes the pair of morphisms defined by plugging $E^{\infty}$ in (5), then the Jónsson-Tarski and canonical extensions coincide.

*Proof.* Let $(A, \alpha)$ be an $L$-algebra. Note first that $L$ is of the shape required by Theorem 5: $E$ is a set of equations of modal depth at most one, and if the $n$-ary expansions of the $\Sigma$-DLE associated with $(A, \alpha)$ (anti)-preserve meets or joins in each argument, they are in particular monotone in each argument.

The structure map of the Jónsson-Tarski extension of $(A, \alpha)$ is denoted by $\alpha^{\zeta}$ and that of the canonical extension by $\alpha^{\sigma}$. The situation can be summarised in the following diagram whose innermost and outermost triangles commute:

<figure><img src="image_4.png" /></figure>

We need to show $\alpha^{\zeta} = \alpha^{\sigma}$. It follows from the definition of $E$ and Proposition 2 that the $n$-ary expansions of the $\Sigma$-DLE associated with $(A, \alpha)$ are smooth, and therefore have unique $(\sigma^n, \gamma)$-continuous extensions given by $(\alpha \circ q_A)^{\sigma}$, moreover $\alpha^{\sigma}$ is defined in such a way that $\alpha^{\sigma} \circ q_{A^{\sigma}} = (\alpha \circ q_A)^{\sigma}$ (see Theorem 5).

By definition $\alpha^{\zeta} = \mathcal{U}\mathbb{P}_f\alpha \circ \mathcal{U}\zeta_A \circ \delta_{\mathbb{P}_fA}$. Since $\delta_{\mathbb{P}_fA} \circ q_{A^{\sigma}}$ is assumed to coequalize the maps defined by $E^{\infty}$ in the way of Diagram (5), so does $\alpha^{\zeta} \circ q_{A^{\sigma}}$, and it follows that the $n$-ary expansions of the $\Sigma$-DLE associated with $\alpha^{\zeta}$ satisfy one of the conditions 5,6,7,8 of Proposition 2, and are in particular $(\sigma^n, \gamma)$-continuous. They therefore define the same $L_{\Sigma}$-algebra structure on $A^{\sigma}$ as $(\alpha \circ q_A)^{\sigma}$. It follows that $\alpha^{\zeta} \circ q_{A^{\sigma}} = \alpha^{\sigma} \circ q_{A^{\sigma}}$, i.e. that $\alpha^{\zeta} = \alpha^{\sigma}$ since $q_{A^{\sigma}}$ is (regular) epi.

**Example 4.** As was shown in Example 2, $L^{\text{ML}}$-algebras have Jónsson-Tarski extensions. Moreover, it is not difficult to see directly from the definition of $\delta^{\text{ML}}$ that for any $A$ in $\mathbf{DL}$ its composition with the quotient $q_A: L_{\{\diamond, \Box\}}A \to L^{\text{ML}}A$ determines two unary maps on $A$ preserving respectively all non-empty joins and all non-empty meets, i.e. $\delta^{\text{ML}}$ meets the criterion of Theorem 7.

Moreover as was shown in Example 3, $L^{\text{ML}}$-algebras also have canonical extensions, and it is clear from the definition that the equations defining $L^{\text{ML}}$ are of the general shape of (7). It follows that $L^{\text{ML}}$ satisfies the conditions of Theorems 7 and coalgebraic completeness-via-canonicity, i.e. Theorem 6, can therefore be used. Consider for example Dunn's Interaction axioms:

$$I = \{\diamond a \wedge \Box b \leq \diamond (a \wedge b), \Box (a \vee b) \leq \Box a \vee \diamond b\}$$
Since they are canonical (see Example 3), it follows from Theorem 6 that the quotient of $F_{LMLFV}$ under the fully invariant equivalence relation in DL defined by $l$, is strongly complete w.r.t. to $P_c \times P_c$-coalgebras validating $l$. We will denote this logic $K_+$. These axioms do not collapse the relations interpreting $\diamond$ and $\square$ as might be expected and as is the case in standard Kripke frames (see [Dun95] and 6.1 of [GNV05] for a discussion on models with one or two relations). However, we can always find such a model if we accept to have a relation closed upward and downward. The following lemma is very useful in practice and greatly clarifies correspondence theory for positive ML (see [CJ97]). We denote by $\downarrow \gamma$ (resp. $\uparrow \gamma$) the pointwise downward (resp. upward) closure of a map $\gamma : W \to P_c W$.

**Lemma 1.** Let $\gamma_{\diamond} \times \gamma_{\square} : W \to P_c(W) \times P_c(W)$, $w \in W$ and $a \in F_{LMLFV}$. then $(w, \gamma_{\diamond} \times \gamma_{\square}, v) \models a \text{ iff } (w, \downarrow \gamma_{\diamond} \times \uparrow \gamma_{\square}, v) \models a \text{ for any valuation } v$.

*Proof.* Immediate from the fact that denotations are upsets.

**Lemma 2.** Let $\gamma_{\diamond} \times \gamma_{\square} : W \to P_c(W) \times P_c(W)$ be a coalgebra validating the Interaction axioms, and let $w \in W$ and $a \in F_{LMLFV}$, then $(w, \gamma_{\diamond} \times \gamma_{\square}, v) \models a \text{ iff } (w, (\gamma_{\diamond} \cap \gamma_{\square}) \times (\gamma_{\diamond} \cap \gamma_{\square}), v) \models a \text{ for any valuation } v$.

*Proof.* By induction on $a$, the interesting cases being $a = \diamond b$ and $a = \square b$. We show the $\diamond b$ case, the other is dual. From Lemma 1, we can assume w.l.o.g. that $\gamma_{\square}$ is upward-closed. We fix a valuation $v : V \to \mathcal{U}(W)$ and show the non-trivial direction: assume $(w, \gamma_{\diamond} \times \gamma_{\square}, v) \models \diamond b$. Since $\diamond c \wedge \square d \le \diamond (c \wedge d)$ is valid, it must hold at $w$ for any valuation. Consider for instance the following valuation: let $q$ be a free variable, i.e. not occurring in $b$, and let us define $v'(p) = v(p)$ on $V \setminus \{q\}$ and $v'(q) = \gamma_{\square}(w)$, which is an upset. The denotations of $b$ under $v$ and $v'$ are equal. By construction we have $(w, \gamma_{\diamond} \times \gamma_{\square}, v') \models \diamond b \wedge \square q$, and thus $(w, \gamma_{\diamond} \times \gamma_{\square}, v') \models \diamond (b \wedge q)$, and therefore there exist $x \in \gamma_{\diamond}(w) \cap \gamma_{\square}(w) \cap [[b]]_{v'}$ but since $[[b]]_{v'} = [[b]]_v$ this means that there exists $x \in \gamma_{\diamond}(w) \cap \gamma_{\square}(w) \cap [[b]]_v$, i.e. $(w, (\gamma_{\diamond} \cap \gamma_{\square}) \times (\gamma_{\diamond} \cap \gamma_{\square}), v) \models \diamond b$ as desired.

The choice of which type of model to consider, viz. models with one or two relations, will in fine depend on what the models represent. In the next example we will present models where states are memory resources and accessibility relations correspond to the action of programs. A single relation then interprets each pair of existential and universal modalities, and $l$ is then trivially satisfied.

*Example 5 (Modal separation logics).* We conclude with a more elaborate family of examples. In [DP15a] we introduced the functor $L^{SL} : DL \to DL$ defined by

$$ 
\begin{align*}
L^{SL} A &= \mathcal{F}\{I, a * b, a \dashv b, a \dashv \neg b \mid a, b \in UA\} \\
&\quad \cup \\
&\quad \{(a \vee b) * c = (a * c) \vee (b * c), a * (b \vee c) = (a * b) \vee (a * c) \\
&\quad a \dashv (b \wedge c) = (a \dashv b) \wedge (a \dashv c), (a \vee b) \dashv c = (a \dashv c) \wedge (b \dashv c) \\
&\quad (a \wedge b) \dashv \neg c = (a \dashv \neg c) \wedge (a \dashv \neg c), a \dashv (b \vee c) = (a \dashv \neg b) \wedge (a \dashv \neg c)\}
\end{align*}
$$

We interpret $L^{SL}$-formulas in $T^{SL}$-coalgebras for $T^{SL} : \mathbf{Pos} \to \mathbf{Pos}$ defined by:

$$ T^{SL} W = \mathbb{2} \times P_c(W \times W) \times P_c(W^{op} \times W) \times P_c(W \times W^{op}) $$
via the semantic transformation $\delta^{\text{SL}} : L^{\text{SL}}U \to UT^{\text{SL}}$ defined on generators at each poset $W$ by $\delta_W^{\text{SL}}(I) = \{t \in T^{\text{SL}}W \mid \pi_1(t) = 0\}$ and

$$
\begin{align*}
\delta_W^{\text{SL}}(U * V) &= \{t \in T^{\text{SL}}W \mid \exists(x, y) \in \pi_2(t), x \in U, y \in V\} \\
\delta_W^{\text{SL}}(U *_V V) &= \{t \in T^{\text{SL}}W \mid \forall(x, y) \in \pi_3(t), x \in U \Rightarrow y \in V\} \\
\delta^{\text{SL}}W(U *_- V) &= \{t \in T^{\text{SL}}W \mid \forall(x, y) \in \pi_4(t), y \in V \Rightarrow x \in U\}
\end{align*}
$$

The intended interpretation of this language is that worlds represent resources which can be split and $w \models p * q$ means that the resource $w$ can be split into two resource $s, t$ such that $s \models p$ and $t \models q$. The operations $*$ and $*$ are left and right residuals to $*$, and $I$ acts as a unit. This is encoded by the (in)equations:

$$
\begin{align*}
\text{FC1} \quad & a * 1 = a, 1 * a = a & \text{FC4} \quad & (c * -b) * a \leq c * -(a * b) \\
\text{FC2} \quad & 1 \leq a * -a, 1 \leq a * -a & \text{FC5} \quad & (a * -b) * b \leq a \\
\text{FC3} \quad & a * (b * -c) \leq (a * b) * -c & \text{FC6} \quad & b * (b * -a) \leq a
\end{align*}
$$

The logic defined by $L^{\text{SL}}$ and these (in)equalities is known as separation logic or the logic of bunched implication or the distributive Lambek calculus depending on the context, and we shall denote it as **SL**. These (in)equations are canonical (residuated maps and their residuals are very well-behaved under canonical extension, even in posets see [Mor14]). As was shown in [DP15a], the adjoint transformation $\delta^{\text{SL}}$ has right-inverses at every $A$ in **DL**, and $L^{\text{SL}}$-algebras therefore have Jónsson-Tarski extensions. Moreover, as can be seen from the definition of $\delta^{\text{SL}}$ the criterion of (anti)-preservation of arbitrary joins or meets of Theorem 7 is also satisfied. Finally, the equations defining $L^{\text{SL}}$ satisfy the conditions of Theorem 5 and canonical extensions thus lift to $\mathbf{Alg}_{\mathbf{DL}}(L^{\text{SL}})$. All the conditions of Theorem 7 are thus satisfied, and we can use Theorem 6 on the regular quotient defined by FC1-FC6. The logic **SL** is thus strongly complete w.r.t. the $T^{\text{SL}}$-coalgebras validating these axioms, viz. $T^{\text{SL}}$-coalgebras such that

$$ (x, y) \in \gamma_*(w) \quad \text{iff} \quad (x, w) \in \gamma_*(y) \quad \text{iff} \quad (w, y) \in \gamma_*(x) \qquad (8) $$

and for every $w \in W$ there exists $(w, x)$, $(y, w) \in \gamma_*(w)$ with $x, y \models I$. A typical example of such coalgebra is given by memory states represented by the set $H$ of heaps, i.e. partial maps $f : \mathbb{N}_+ \to \mathbb{N}$ with finite domain. These are ordered by $f \leq g$ if $g \upharpoonright \text{dom} f = f$, the empty heap is the unit and $\gamma_* : H \to \mathbf{P}_c(H \times H)$, $f \mapsto \{(g, h) \mid \text{dom} g \cap \text{dom} h = \emptyset, g, h \leq f\}$ interprets the separation conjunction $*$ and its residuals via (8). In this context, it is reasonable to combine modal logics for program specification with separation logic to describe heaps evolving under the action of programs. Various fragments of PDL (see [Gol92]) are good candidates. For example, consider the simple program syntax $\alpha ::= \pi \mid \alpha$; $\alpha$ with $\pi \in \Pi$ a set of atomic programs. By Theorem 3, the results for **SL** and $\mathbf{K}_+$, and Lemma 2, it follows that the fusion $\bigoplus_{\Pi^*} \mathbf{K}_+ \oplus \mathbf{SL}$ is strongly complete w.r.t. to $\prod_{\Pi^*} \mathbf{P}_c(-) \times 2 \times \mathbf{P}_c((-) \times (-))$-coalgebras. If we want to encode the sequential composition of the grammar in the interpretation we need the axioms

$$ \mathbf{Comp} = \{\langle \alpha_1; \alpha_2 \rangle a = \langle \alpha_1 \rangle \langle \alpha_2 \rangle a, [\alpha_1; \alpha_2] a = [\alpha_1][\alpha_2] a \mid \alpha_1, \alpha_2 \in \Pi^*\} $$
It is easy to check from Theorem 4 that these axioms are canonical. They are valid in a model with a single relation $R_\alpha$ interpreting each pair $\langle\alpha\rangle$, $[\alpha]$ if $R_{\alpha_1}^\perp \circ R_{\alpha_2}^\perp = R_{\alpha_1;\alpha_2}^\perp$ and $R_{\alpha_1}^\uparrow \circ R_{\alpha_2}^\uparrow = R_{\alpha_1;\alpha_2}^\uparrow$, where $R_\alpha^\perp$ and $R_\alpha^\uparrow$ are the downward and upward closure of $R_\alpha$ respectively. Theorem 6 gives us strong completeness of $\bigoplus_{\Pi^*} K_+ / \{\text{Comp}\}$ with respect to such coalgebras, and modularity then gives us strong completeness of $\bigoplus_{\Pi^*} K_+ / \{\text{Comp}\} \oplus \text{SL}$. Note how the use of positive logics allows us to talk about existential access to all resources smaller than certain upper bounds, and universal access to resources larger than certain lower bounds. More interestingly perhaps, we could consider $\alpha ::= \pi | \alpha; \alpha | \alpha || \alpha$ with a parallel composition operation and interaction axioms of the shape

$$ \langle \alpha_1 || \alpha_2 \rangle a = \langle \alpha_1 \rangle a * \langle \alpha_2 \rangle a $$

This time, strong completeness will not simply transfer by modularity since we are making the languages interact, however since such equations are canonical, we can still apply completeness-via-canonicity, only this time to the entire logic.

# 6 Conclusion

We have described the key steps of the coalgebraic version of completeness-via-canonicity, and in particular the key role played by the Jónsson-Tarski and canonical extensions. We have sketched an implementation of the method for all positive or boolean logics with modalities satisfying a set of equations in the shape of (7) and a relational semantics. Much work remains to be done. We have a complete implementation for boolean graded logics, but not yet in the positive case, and no implementation at all for probability logic. For this we would like to explore whether the method can be applied to MSL-based logics, since an expressive logics for Markov chains can be formulated over MSL ([JS10]).

# References

[BJ11] G. Bezhanishvili and R. Jansana, Priestley style duality for distributive meet-semilattices, Studia Logica 98 (2011), no. 1-2, 83-122.

[BKV13] A. Balan, A. Kurz, and J. Velebil, Positive fragments of coalgebraic logics, Algebra and Coalgebra in Computer Science, Springer, 2013, pp. 51-65.

[CJ97] S. Celani and R. Jansana, A new semantics for positive modal logic, Notre Dame Journal of Formal Logic 38 (1997), no. 1, 1-18.

[CKP+09] C. Cirstea, A. Kurz, D. Pattinson, L. Schröder, and Y. Venema, Modal logics are coalgebraic, The Computer Journal (2009).

[CP07] C. Cirstea and D. Pattinson, Modular construction of complete coalgebraic logics, Theor. Comput. Sci. 388 (2007), no. 1-3, 83-108.

[Dah15] F. Dahlqvist, Completeness-via-canonicity for coalgebraic logics, Ph.D. thesis, Imperial College London, 2015.

[DP11] F. Dahlqvist and D. Pattinson, On the fusion of coalgebraic logics, CALCO, 2011, pp. 161-175.

[DP13] ——, Some Sahlqvist completeness results for coalgebraic logics, FoSSaCS, 2013, pp. 193-208.
[DP15a] F. Dahlqvist and D. Pym, *Completeness-via-canonicity for distributive sub-structural logics, a coalgebraic perspective*, RAMICS, 2015.

[DP15b] ——, *Completeness-via-canonicity for distributive substructural logics, a coalgebraic perspective*, Tech. Report RN/15/04, UCL, 2015.

[Dun95] J. M. Dunn, *Positive modal logic*, Studia Logica **55** (1995), no. 2, 301–317.

[GH01] M. Gehrke and J. Harding, *Bounded lattice expansions*, Journal of Algebra **238** (2001), no. 1, 345–371.

[GJ94] M. Gehrke and B. Jónsson, *Bounded distributive lattices with operators*, Math. Japon. **40**, No. 2 (1994), 207–215.

[GJ04] ——, *Bounded distributive lattice expansions*, Math. Scand. **94** (2004), 13–45.

[GNV05] M. Gehrke, H. Nagahashi, and Y. Venema, *A Sahlqvist theorem for distributive modal logic*, Ann. Pure Appl. Logic **131** (2005), no. 1-3, 65–102.

[Gol92] R. Goldblatt, *Logics of time and computation*, CSLI Lecture Notes, Center for the Study of Language and Information, Stanford, CA, 1992.

[GP14] MJ Gouveia and HA Priestley, *Canonical extensions and profinite completions of semilattices and lattices*, Order **31** (2014), no. 2, 189–216.

[HV05] I. Hodkinson and Y. Venema, *Canonical varieties with no canonical axiomatisation*, Transactions of the AMS **357** (2005), no. 11, 4579–4605.

[Jón94] B. Jónsson, *On the canonicity of Sahlqvist identities*, Studia Logica **53** (1994), no. 4, 473–492.

[JS10] B. Jacobs and A. Sokolova, *Exemplaric expressivity of modal logics*, J. Log. and Comput. **20** (2010), 1041–1068.

[JT51] B. Jónsson and A. Tarski, *Boolean algebras with operators. part 1.*, Amer. J. Math. **33** (1951), 891–937.

[KKP04] C. Kupke, A. Kurz, and D. Pattinson, *Algebraic semantics for coalgebraic logics*, CMCS, Electr. Notes in Th. Comp. Sc., vol. 106, 2004, pp. 219–241.

[KKP05] ——, *Ultrafilter Extensions for Coalgebras*, CALCO, Springer, 2005, pp. 263–277.

[KKV12] K. Kapulkin, A. Kurz, and J. Velebil, *Expressiveness of positive coalgebraic logic*, AiML 9, 2012, pp. 368–385.

[KP11] C. Kupke and D. Pattinson, *Coalgebra semantics of modal logics: an overview*, Th. Comp. Sc. **412** (2011), no. 38, 5070–5094, CMCS 2010.

[KR12] A. Kurz and J. Rosický, *Strongly complete logics for coalgebras*, Logical Methods in Computer Science **8** (2012), no. 3, 1–32.

[Mor14] W. Morton, *Canonical extensions of posets*, Algebra universalis **72** (2014), no. 2, 167–200.

[PS08] D. Pattinson and L. Schröder, *Beyond rank 1: Algebraic semantics and finite models for coalgebraic logics*, FoSSaCS, LNCS, no. 4962, 2008, pp. 66–80.

[Rib52] H. Ribeiro, *A remark on boolean algebras with operators*, Amer. J. Math. **74** (1952), 162–167.

[Sch06] L. Schröder, *A finite model construction for coalgebraic modal logic*, FoSSaCS, LNCS, vol. 3921, Springer, 2006, pp. 157–171.

[SP09] L. Schröder and D. Pattinson, *Strong completeness of coalgebraic modal logics*, STACS, Dagstuhl Seminar Proc., vol. 09001, 2009, pp. 673–684.

[SP10] L. Schröder and D. Pattinson, *Rank-1 logics are coalgebraic*, J. of Log. and Comput. **20** (2010), no. 5, 1113–1147.

[Ven06] Yde Venema, *Algebras and coalgebras*, Handbook of Modal Logic (J. van Benthem, P. Blackburn, and F. Wolter, eds.), Elsevier, 2006.

[VK11] J. Velebil and A. Kurz, *Equational presentations of functors and monads*, Math. Struct. in Comp. Sc. **21** (2011), no. 2, 363–381.