# The positivication of coalgebraic logics111This work was supported by the
ERC grant ERC-2015-STG, ProFoundNet

Fredrik Dahlqvist
University College London
<EMAIL_ADDRESS>Alexander Kurz
University of Leicester
<EMAIL_ADDRESS>
###### Abstract

We present positive coalgebraic logic in full generality, and show how to
obtain a positive coalgebraic logic from a boolean one. On the model side this
involves canonically computing a endofunctor
$T^{\prime}:\mathbf{Pos}\to\mathbf{Pos}$ from an endofunctor
$T:\mathbf{Set}\to\mathbf{Set}$, in a procedure previously defined by the
second author et alii called _posetification_. On the syntax side, it involves
canonically computing a syntax-building functor
$L^{\prime}:\mathbf{DL}\to\mathbf{DL}$ from a syntax-building functor
$L:\mathbf{BA}\to\mathbf{BA}$, in a dual procedure which we call
_positivication_. These operations are interesting in their own right and we
explicitly compute posetifications and positivications in the case of several
modal logics. We show how the semantics of a boolean coalgebraic logic can be
canonically lifted to define a semantics for its positive fragment, and that
weak completeness transfers from the boolean case to the positive case.

##  1 Introduction

Partially ordered structures are ubiquitous in theoretical computer science.
From knowledge representation to abstract interpretation in static analysis,
from resource modelling to protocol or access rights formalization in formal
security, the list of applications is enormous. Being able to formally reason
about transition systems over posets therefore seems important, but has not
been systematically developed. The natural formalism to reason about
transition systems is undoubtedly the class of _modal_ logics. However, most
are tailored to transition structures over _sets_. This is a direct
consequence of the fact that most modal logics are _boolean_. _Positive modal
logic_ is the exception, and is most naturally interpreted in partially
ordered Kripke structures (see for example [6, 9]).

Arguably, the most natural and powerful framework to study boolean modal
logics in a uniform and systematic way, is the theory of _Boolean Coalgebraic
Logics_ (henceforth BCL, see e.g. [7]). In its ‘abstract’ ([19]) presentation,
it is parametrised by an endofunctor $L:\mathbf{BA}\to\mathbf{BA}$ which
builds modal algebras of modal terms over a boolean structure, an endofunctor
$T:\mathbf{Set}\to\mathbf{Set}$ which builds the transition structures over
which the modal terms are to be interpreted, and a natural transformation
$\delta:L\mathsf{P}\to\mathsf{P}T^{\mathrm{op}}$ (where
$\mathsf{P}:\mathbf{Set}^{\mathrm{op}}\to\mathbf{BA}$ is the powerset functor)
which implements the interpretation by associating sets of acceptable
successors states to each modal term over a predicate (see [17, 18, 12, 21]).
This data, and the dual adjunction between $\mathbf{Set}$ and $\mathbf{BA}$,
is traditionally summarized in the following diagram

$\textstyle{\mathbf{BA}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{S}}$$\scriptstyle{L}$$\textstyle{\perp}$$\textstyle{\mathbf{Set}^{\mathrm{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{P}}$$\scriptstyle{T^{\mathrm{op}}}$$\textstyle{\delta:L\mathsf{P}\Rightarrow\mathsf{P}T^{\mathrm{op}}}$
(1)

where $\mathsf{S}$ is the functor sending a boolean algebra to the set of its
ultrafilters.

To develop an equally powerful framework for reasoning about transition
structures over posets, it seems natural to study _Positive Coalgebraic
Logics_ (henceforth PCL). In fact, work in this direction has already started,
see for example [14, 3]. We pursue this work further and present PCL in full
generality, i.e. at the same level of generality as its boolean counterpart.
Moreover, given the close kinship between the two theories, we will show that
the wheel needn’t be re-invented every time, and that many BCLs have a
canonical positive fragment which inherits useful properties from its boolean
parent. The data defining a PCL will be

$\textstyle{\mathbf{DL}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{S^{\prime}}}$$\scriptstyle{L^{\prime}}$$\textstyle{\perp}$$\textstyle{\mathbf{Pos}^{\mathrm{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{P}^{\prime}}$$\scriptstyle{(T^{\prime})^{\mathrm{op}}}$$\textstyle{\delta^{\prime}:L^{\prime}\mathsf{P}^{\prime}\Rightarrow\mathsf{P}^{\prime}(T^{\prime})^{\mathrm{op}}}$
(2)

where $\mathsf{S^{\prime}}$ is the functor sending a distributive lattice to
the poset of its prime filters, and $\mathsf{P}^{\prime}$ is the functor
sending a poset to the distributive lattice of its upsets. The following
observation will be of fundamental importance in what follows: the adjunction
$\mathsf{S^{\prime}}\dashv\mathsf{P}^{\prime}:\mathbf{Pos}^{\mathrm{op}}\to\mathbf{DL}$
which is the backbone of diagram (2) is in fact _$\mathbf{Pos}$ -enriched_;
that is to say $\mathbf{DL}$ and $\mathbf{Pos}$ are $\mathbf{Pos}$-enriched
categories and $\mathsf{S^{\prime}},\mathsf{P}^{\prime}$ are
$\mathbf{Pos}$-enriched functors ([16]). Clearly, it would be a shame not to
use this extra structure which comes for free. But more seriously, this
enriched structure is not simply a mathematical quirk, it suggests that ‘doing
logic’ positively is quite different from ‘doing logic’ in a boolean setting,
in particular it is more than simply dropping negations. In fact _inequations_
become the standard relation between terms on the syntax side, just as it is
between elements on the model side. This is borne out by the existing
axiomatization of positive modal logic originally proposed in [8] which is
entirely given by inequations. For these reasons, and following [14, 3], this
paper will present positive coalgebraic logic as a $\mathbf{Pos}$-enriched
coalgebraic logic. In a slogan: “ _in positive coalgebraic logic we remove
negations but we add order_ ”.

Working in a $\mathbf{Pos}$-enriched setting means that the syntax-building
functor $L^{\prime}:\mathbf{DL}\to\mathbf{DL}$ and the coalgebra-building
functor $T^{\prime}:\mathbf{Pos}\to\mathbf{Pos}$ will also need to be
$\mathbf{Pos}$-enriched. The first main contributions of this paper is to show
how well-known ordinary functors from BCL can be turned into
$\mathbf{Pos}$-enriched functors performing analogous roles in PCL. On the
semantics side this means turning an ordinary functor
$T:\mathbf{Set}\to\mathbf{Set}$ into a $\mathbf{Pos}$-enriched functor
$T^{\prime}:\mathbf{Pos}\to\mathbf{Pos}$ by a process called _posetification_
first developed in [3], for which we develop a practical understanding in
Section 3 by computing the posetification of several well-known functors from
modal logic: the neighbourhood, monotone neighbourhood, powerset and multiset
functors. On the syntax side this means turning an ordinary functor
$L:\mathbf{BA}\to\mathbf{BA}$ into a $\mathbf{Pos}$-enriched functor
$L^{\prime}:\mathbf{DL}\to\mathbf{DL}$, a process which we call
_positivication_ and which is detailed in Section 4. We show how
positivication can be applied to the functor defining normal modal logic, but
also to functors which define non-monotone modal logics. In this case, the
positivication procedure may not yield a logic at all, at least not in the
usual meaning of the word. The second main contribution of this paper is to
show how a semantic natural transformation $\delta:L\mathsf{P}\to\mathsf{P}T$
can also be lifted to define a $\mathbf{Pos}$-enriched semantic natural
transformation
$\delta^{\prime}:L^{\prime}\mathsf{P}^{\prime}\to\mathsf{P}^{\prime}T^{\prime}$,
where $T^{\prime}$ is the posetification of $T$, and $L^{\prime}$ is the
positivication of $L$. This is done in Section 5, where we also prove that by
construction of $\delta^{\prime}$, if $\delta$ defines a weakly complete
logic, then so does $\delta^{\prime}$.

Related work. As mentioned above several aspects of positive coalgebraic
logics have been studied in [14, 3], the concept of posetification and the
idea of working in an enriched setting in particular. The key contribution of
this work is to dissociate the syntax from the semantics. This reflects the
practise of modal logics, where the syntax-building functor $L$ is usually not
defined directly from the semantics-building functor, but rather from a
grammar which is convenient to express certain properties. Graded modal logic
for example relies on a syntax which is not obviously related to its
semantics. This justifies going beyond the techniques of [3]. As a
consequence, one must also be able to define a semantic natural transformation
$L^{\prime}\mathsf{P}^{\prime}\to\mathsf{P}^{\prime}T^{\prime}$, which we do
be adapting the boolean semantics. We are also indebted to work on monotone
modal logic for the monotone neighbourhood functor, see eg [11, 23], and on
non-monotone modal logic for the (unrestricted) neighbourhood functor as these
two cases highlight many of the peculiar features of our approach.

##  2 A maths toolkit

###  2.1 Ordinary vs $\mathbf{Pos}$-enriched category theory

The central tool of this paper is to work in categories enriched over
$\mathbf{Pos}$. For a general reference to enriched categories we refer to
[16]. But the special case of $\mathbf{Pos}$-categories is much simpler than
the general case and we believe that most of this paper can be read without
special knowledge in enriched category theory. The purpose of this section is
to review what will be required.

A $\mathbf{Pos}$-category is a category in which homsets are posets and
composition is monotone in each argument. A $\mathbf{Pos}$-functor is a
functor that is _locally monotone_ , that is, it preserves the order on
homsets. $\mathbf{Pos}$-natural transformations are just natural
transformations.

Monotonicity permeates all aspects of $\mathbf{Pos}$-enriched categories. For
example, $\mathbf{Pos}$-enriched algebra, or _ordered algebra_ , is
characterised by all operations of an ordered algebra being monotone. This is
important for our application of ordered algebra to positive coalgebraic
logic, that is, to coalgebraic logic with monotone operations.

The basic features of ordered universal algebra can be developed in much the
same way as ordinary universal algebra [5]. Following the
$\mathbf{Pos}$-enriched approach of [22], the most important change to make is
to replace coequalisers by so-called coinserters.

One of the most important features of the $\mathbf{Pos}$-enriched setting is
that with the so-called weighted limits and colimits additional universal
constructions become available. For example,

$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g}$$\scriptstyle{f}$$\scriptstyle{\uparrow}$$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{c}$$\textstyle{C}$

is a _coinserter_ if $c\circ f\leq c\circ g$ and for all $h$ with $h\circ
f\leq h\circ g$ there is a unique $k$ such that $k\circ c=h$. This is almost
like a coequaliser, but $C$ is a quotient of $B$ w.r.t. inequations. For
example, in $\mathbf{Pos}$, the coinserter $C$ is obtained by adding to $B$
the inequations $\\{fa\leq ga\mid a\in A\\}$ and then quotienting by anti-
symmetry. We will encounter two special kinds of coinserters (we sometimes
drop now the $\uparrow$ notation in the interest of typesetting):

$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\pi_{1}}$$\scriptstyle{\pi_{0}}$$\scriptstyle{s}$$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{i}$

A pair of arrows, and also its coinserter, is called _reflexive_ if there is
$i:B\to A$ such that $\pi_{0}\circ i=\pi_{1}\circ i=\mathrm{id}$ and it is
called _symmetric_ if there is $s:A\to A$ such that $\pi_{0}\circ s=\pi_{1}$
and $\pi_{1}\circ s=\pi_{0}$. Note that an arrow is a coinserter of a
symmetric pair, or a symmetric coinserter for short, iff it is a coequaliser
of the same pair.

The dual notion is that of an _inserter_

$\textstyle{E\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{e}$$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g}$$\scriptstyle{f}$$\scriptstyle{\uparrow}$$\textstyle{A.}$

In $\mathbf{Pos}$, as well as in categories of ordered algebras, the inserter
$E$ is $\\{b\in B\mid fa\leq gb\\}$.

Another important limit not available in ordinary categories is the _power_ or
_cotensor_ with a poset. For example, in $\mathbf{Pos}$ we have
$X^{\mathbbm{2}}=\\{(x,x^{\prime})\mid x\leq x^{\prime}\\}$ where
$\mathbbm{2}$ is $\\{0<1\\}$. We will also encounter the dual notion, the
_tensor_ or _copower_ $X\bullet A$. Here we say that a category $\cal A$ has
tensors if for all $A\in\cal A$ and all posets $X$, there is an object
$X\bullet A$ such that

${\cal A}(X\bullet A,A^{\prime})\cong[X,{\cal A}(A,A^{\prime})]$

where $[X,Y]$ denotes exponentiation (aka internal hom) in $\mathbf{Pos}$. The
tensor $\mathbbm{2}\bullet A$ can be understood as an ordered coproduct of $A$
with itself in which “each $a$ on the left is smaller than the $a$ on the
right”.

In order to treat ordinary categories and $\mathbf{Pos}$-enriched categories
in the same framework, we consider an ordinary category as a
$\mathbf{Pos}$-category with discrete homsets. For each
$\mathbf{Pos}$-category $\cal A$ there is a corresponding ordinary category
${\cal A}_{o}$. For example, we have $\mathbf{Set}=\mathbf{Set}_{o}$ and
$\mathbf{BA}=\mathbf{BA}_{o}$, but $\mathbf{Pos}$ and $\mathbf{Pos}_{o}$ are
different. In particular, there is no (enriched) forgetful functor
$\mathbf{Pos}\to\mathbf{Set}$, only an (ordinary) forgetful functor
$\mathbf{Pos}_{o}\to\mathbf{Set}_{o}$. Note that using “o” allows us to drop
the qualifications enriched and ordinary without creating ambiguity. For
example, the inclusion $\mathsf{D}:\mathbf{Set}\to\mathbf{Pos}$ has a left
adjoint $\mathsf{C}:\mathbf{Pos}\to\mathbf{Set}$ mapping a poset to its
connected components and the inclusion
$\mathsf{D}_{o}:\mathbf{Set}_{o}\to\mathbf{Pos}_{o}$ has as a right adjoint
the forgetful functor $\mathsf{V}:\mathbf{Pos}_{o}\to\mathbf{Set}_{o}$, but
$\mathsf{D}:\mathbf{Set}\to\mathbf{Pos}$ does not have a right
adjoint.222$L:\cal A\to\cal B$ is a $\mathbf{Pos}$-enriched left-adjoint of
$R:\cal B\to\cal A$ if there is a natural isomorphism _of posets_ ${\cal
B}(LA,B)\cong{\cal A}(A,RB)$. We have
$\mathbf{Pos}_{o}(DA,B)\cong\mathbf{Set}_{o}(A,\mathsf{V}B)$ but not
$\mathbf{Pos}(DA,B)\cong\mathbf{Set}(A,\mathsf{V}B)$.

$\hfill\mathsf{C}\dashv\mathsf{D}:\mathbf{Set}\to\mathbf{Pos}\quad\quad\quad\quad\mathsf{D}_{o}\dashv\mathsf{V}:\mathbf{Pos}_{o}\to\mathbf{Set}_{o}\hfill$
(3)

Accordingly, $\mathsf{D}$ preserves all (weighted) limits and $\mathsf{D}_{o}$
preserves all (ordinary) colimits. But $\mathsf{D}$ does not preserve all
($\mathbf{Pos}$-enriched) colimits and indeed we will see later that
$\mathsf{D}$ does not preserve all coinserters.

We will also need the corresponding results on the algebraic side. The
inclusion $\mathsf{W}:\mathbf{BA}\to\mathbf{DL}$ has a right adjoint
$\mathsf{K}$ (mapping a $\mathbf{DL}$ to the largest Boolean subalgebra it
contains) and $\mathsf{W}_{o}:\mathbf{BA}_{o}\to\mathbf{DL}_{o}$ has a left-
adjoint $G:\mathbf{DL}_{o}\to\mathbf{BA}_{o}$ (mapping a distributive lattice
to the free $\mathbf{BA}$ over it).

$\hfill\mathsf{K}\vdash\mathsf{W}:\mathbf{BA}\to\mathbf{DL}\quad\quad\quad\quad\mathsf{W}_{o}\vdash\mathsf{G}:\mathbf{DL}_{o}\to\mathbf{BA}_{o}\hfill$
(4)

Note that (3) and (4) are dually equivalent when restricted to finite
structures.

###  2.2 The ordered variety of Boolean algebras

The category $\mathbf{BA}$ of Boolean algebras has discrete homsets, giving
rise to a forgetful functor $\mathbf{BA}\to\mathbf{Set}$. This functor is a
$\mathbf{Pos}$-enriched, or ordered, variety [22]. At the heart of this
observation is the fact that reflexive coinserters in $\mathbf{BA}$ are
symmetric, a fact that we prove in detail as it will be important later.

######  Proposition 1.

Every reflexive pair
$\textstyle{A_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\pi_{1}}$$\scriptstyle{\pi_{0}}$$\textstyle{A_{0}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{i}$
in $\mathbf{BA}$ is symmetric.

###### Proof.

Let $(a,b)\in A_{1}$. Here, $(a,b)$ is a shorthand for an element in $A_{1}$
such that $\pi_{0}((a,b))=a$ and $\pi_{1}((a,b))=b$. We write $(a,a)$ for
$i(a)$. Consider the Boolean algebra morphism $\phi:A_{1}\to A_{1}$ defined by

$\displaystyle\phi(a,b)=\Big{(}(a,b)\wedge(b,b)\to(a,a)\Big{)}\wedge\Big{(}(a,b)\wedge(a,a)\to(b,b)\Big{)}\wedge\Big{(}(a,a)\vee(a,b)\vee(b,b)\Big{)}$

Since the projections are $\mathbf{BA}$-morphisms, we obtain
$\pi_{0}(\phi(a,b))=(a\to b)\wedge(a\vee b)=b$ and $\pi_{1}(\phi(a,b))=(b\to
a)\wedge(a\vee b)=a$, showing $(b,a)\in A_{1}$. ∎

(The argument also works for Heyting algebras.) Note that we can equip
$\mathbf{BA}$ with a forgetful functor
$\mathbf{BA}\stackrel{{\scriptstyle\mathsf{W}}}{{\longrightarrow}}\mathbf{DL}\to\mathbf{Pos}$
mapping each BA to its carrier in its natural order, but this functor is not
an ordered variety since $\mathbf{BA}$ is not closed under weighted limits in
$\mathbf{DL}$.

###  2.3 Density and Kan extensions

Much of our technical work revolves around the result that
$\mathsf{D}:\mathbf{Set}\to\mathbf{Pos}$ is dense, see [3], and that
$\mathsf{W}:\mathbf{BA}\to\mathbf{DL}$ is codense, see Theorem 10. This in
turn allows us to extend functors on $\mathbf{Set}$ to functors on
$\mathbf{Pos}$ via left Kan extension and to extend functors on $\mathbf{BA}$
to functors on $\mathbf{DL}$ via right Kan extensions, as we will review now.

A functor $K:\cal A\to\cal C$ is _dense_ if colimit preserving functors $\cal
C\to\cal B$ are determined by their restriction along $K$, or, more formally,
if the functor $[K,\mathsf{Id}_{\cal B}]:[\cal C,\cal B]\to[\cal A,\cal B]$
restricting along $K$ is fully faithful [16, Thm 5.1]. If, moreover, $K$
itself is fully faithful, then a colimit preserving functor $\cal C\to\cal B$
is the left Kan extension of its restriction along $K$ [16, Thm 5.29].
Furthermore, we may be able to compute left Kan extensions explicitely with
the help of a so-called density presentation [16, Thm 5.19]. For example, we
know (see [3]) that $\mathsf{D}:\mathbf{Set}\to\mathbf{Pos}$ is dense and has
a density presentation given by reflexive coinserters of ‘nerves of posets’.
Explicitly, every poset $X$ is the reflexive coinserter 333The coinserter of
$\textstyle{VX^{\mathbbm{2}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{VX}$
in $\mathbf{Set}$ provides an example of weighted colimit that is not
preserved by $\mathsf{D}$, showing that $\mathsf{D}$ cannot have an (enriched)
right adjoint.

$\textstyle{\mathsf{D}\mathsf{V}X^{\mathbbm{2}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{D}\pi_{1}}$$\scriptstyle{\mathsf{D}\pi_{0}}$$\textstyle{\mathsf{D}\mathsf{V}X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{i}$$\textstyle{X}$
(5)

where $\mathsf{V}X^{\mathbbm{2}}=\\{(x,x^{\prime})\mid
x\leq_{X}x^{\prime}\\}$. That the coinserter is reflexive means that
$\mathsf{D}\pi_{0}\circ i=\mathsf{D}\pi_{1}\circ i=\mathrm{id}$, which is true
for $i(x)=(x,x)$. The fact that these coinserters provide a density
presentation means that the left Kan extension of a functor
$F:\mathbf{Set}\to\mathbf{Pos}$ along $\mathsf{D}$ can be computed as the
coinserter

$\textstyle{F\mathsf{V}X^{\mathbbm{2}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{F\pi_{1}}$$\scriptstyle{F\pi_{0}}$$\textstyle{F\mathsf{V}X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{(\mathrm{Lan}_{\mathsf{D}}F)X}$
(6)

and we will see examples of this in the next section. If one happens to extend
along an adjoint functor $K$, Kan-extensions are easier:

$\hfill K\dashv V\ \Longrightarrow\ \mathrm{Lan}_{K}F=FV\hfill G\dashv K\
\Longrightarrow\ \mathrm{Ran}_{K}F=FG\hfill$ (7)

This implies that to compute (ordinary) Kan extensions along $\mathsf{D}_{o}$
or $\mathsf{W}_{o}$ we can use (3) or (4), and (7). To better understand the
difference with extending along $\mathsf{D}$ or $\mathsf{W}$, we can see the
computation of the Kan extensions in two steps:

$\textstyle{{\cal
C}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{H^{\prime}}$$\textstyle{{\cal
C}}$$\textstyle{{\cal
C}_{o}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\tilde{H}}$$\textstyle{{\cal
C}_{o}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\cal
A}_{o}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{J_{o}}}$$\scriptstyle{J}$$\scriptstyle{H}$$\textstyle{{\cal
A}_{o}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{J_{o}}}$$\scriptstyle{J}$
$\textstyle{\mathbf{Pos}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{H^{\prime}}$$\textstyle{\mathbf{Pos}}$$\textstyle{\mathbf{Pos}_{o}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\tilde{H}}$$\textstyle{\mathbf{Pos}_{o}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathbf{Set}_{o}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{D}_{o}}$$\scriptstyle{\;\dashv}$$\scriptstyle{\mathsf{V}}$$\scriptstyle{H}$$\scriptstyle{\mathsf{D}}$$\textstyle{\mathbf{Set}_{o}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{D}_{o}}$$\scriptstyle{\mathsf{D}}$
$\textstyle{\mathbf{DL}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{H^{\prime}}$$\textstyle{\mathbf{DL}}$$\textstyle{\mathbf{DL}_{o}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\tilde{H}}$$\textstyle{\mathbf{DL}_{o}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathbf{BA}_{o}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{W_{o}}$$\scriptstyle{\
\vdash}$$\scriptstyle{\mathsf{G}}$$\scriptstyle{H}$$\scriptstyle{\mathsf{W}}$$\textstyle{\mathbf{BA}_{o}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{W_{o}}$$\scriptstyle{\mathsf{W}}$
(8)

(i) Since ${\cal C}_{o}\to{\cal C}$ preserves all ordinary (co)limits we can
use [16, Thm 4.47] to break down the extension of $JH$ along $J$ into first
extending $J_{o}H$ along $J_{o}$ to $\tilde{H}$ and then extending $\tilde{H}$
to $H^{\prime}$. (ii) If a functor ${\cal C}_{o}\to{\cal C}_{o}$ is locally
monotone then this functor is its own extension (both left and right) to
${\cal C}\to{\cal C}$. This means that for locally monotone functors
$\tilde{H}$ the upper square is trivial. (iii) To compute $\tilde{H}$ we can
use (3) or (4), and (7). — While this is sometimes a good approach, the
downside is that $\tilde{H}$ is typically not locally monotone (so we cannot
use (i)) and the inclusion ${\cal C}_{o}\to{\cal C}$ is not fully faithful (so
we loose the good properties of Kan extensions along fully faithful functors).
To summarise, to compute Kan extensions along $\mathsf{D}$ we use (6) and for
$\mathsf{W}$ we will develop a similar presentation in Theorem 10.

##  3 Posetification

We define the _posetification $T^{\prime}$ of a $\mathbf{Set}$-functor $T$_ as
$\mathrm{Lan}_{\mathsf{D}}\mathsf{D}T$, the left Kan-extension of
$\mathsf{D}T$ along $\mathsf{D}$, together with a natural isomorphism
$\alpha:\mathsf{D}T\Rightarrow T^{\prime}\mathsf{D}$. In concrete examples we
will typically define $T^{\prime}$ so that $\alpha$ is the identity. In
particular, $T^{\prime}$ is the universal locally monotone extension of $T$,
that is, for all $S:\mathbf{Pos}\to\mathbf{Pos}$ and
$\beta:\mathsf{D}T\Rightarrow S\mathsf{D}$, there is a unique
$\gamma:T^{\prime}\to S$ such that $\gamma\circ\alpha=\beta$. The coinserter
(6) now becomes

$\textstyle{\mathsf{D}T\mathsf{V}X^{\mathbbm{2}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{D}T\pi_{1}}$$\scriptstyle{\mathsf{D}T\pi_{0}}$$\textstyle{\mathsf{D}T\mathsf{V}X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{e_{X}}$$\textstyle{T^{\prime}X.}$
(9)

It is computed for any poset $X$ in the following way:

  1. (i)

consider the (reflexive) relation $R_{T}\subseteq T\mathsf{V}X\times
T\mathsf{V}X$ given by

$(a,b)\in R_{T}\Leftrightarrow\exists c\in T\mathsf{V}X^{\mathbbm{2}}.\hskip
4.30554ptT\pi_{0}(c)=a\hskip 4.30554pt\&\hskip 4.30554ptT\pi_{1}(c)=b$

  2. (ii)

compute its transitive closure $\leq_{T}$

  3. (iii)

quotient $T\mathsf{V}X$ by the equivalence relation $\equiv_{T}\hskip
3.0pt=\hskip 3.0pt\leq_{T}\hskip 2.0pt\cap\hskip 2.0pt\geq_{T}$,

  4. (iv)

the coinserter is given by $(T\mathsf{V}X/\equiv_{T},\leq_{T})$.

Note that by definition,
$\mathsf{V}X^{\mathbbm{2}}\subseteq\mathsf{V}X\times\mathsf{V}X$ is precisely
the graph of the partial order on $X$. It follows that $R_{T}$ is simply the
_lifting of the partial order on $X$ by the functor $T$_ (see [3, Remark
4.8]), often denoted $\overline{T}\leq$. In the rest of this section we will
see examples where $R_{T}$ is transitive, where $R_{T}$ is transitive and
antisymmetric, and where $R_{T}$ is not even transitive.

###  3.1 Posetification of the covariant powerset functor $\mathcal{P}$.

We recall this case here from [3] because it illustrates the steps (ii)-(iv)
of the posetification procedure very clearly. We start by defining the
relation
$R_{\mathcal{P}}\subseteq\mathcal{P}\mathsf{V}X\times\mathcal{P}\mathsf{V}X$
by

$\hfill(a,b)\in R_{\mathcal{P}}\Leftrightarrow\exists
c\in\mathcal{P}\mathsf{V}X^{\mathbbm{2}}.\,\pi_{0}[c]=a\ \&\
\pi_{1}[c]=b\hfill$

which means that

$\hfill(a,b)\in R_{\mathcal{P}}\ \Longleftrightarrow\ (\forall x\in a)(\exists
y\in b)\hskip 2.0pt.\hskip 2.0ptx\leq y\text{ and }(\forall y\in b)(\exists
x\in a)\hskip 2.0pt.\hskip 2.0ptx\leq y\hfill$

It is well-known that $\mathcal{P}$ preserves weak-pullbacks, and that this
guarantees the transitivity of $R_{\mathcal{P}}$. We can thus skip step (i) of
the posetification procedure since $R_{\mathcal{P}}=\hskip
2.0pt\leq_{\mathcal{P}}$. The relation
$R_{\mathcal{P}}=\overline{\mathcal{P}}\leq$ is known as the Egli-Milner
(pre-)order associated with $\leq$. It is not hard to check that
$a\equiv_{\mathcal{P}}b$, i.e. $a\leq_{\mathcal{P}}b$ and
$b\leq_{\mathcal{P}}a$, iff $\mathrm{Conv}(a)=\mathrm{Conv}(b)$ where
$\mathrm{Conv}(a)$ is the convex closure of $a$, i.e. the set $\\{x\in
X\mid\exists y_{1},y_{2}\in a,y_{1}\leq x\leq y_{2}\\}$, and that
$a\equiv_{\mathcal{P}}\mathrm{Conv}(a)$. It follows that
$\mathcal{P}^{\prime}X=(\mathcal{P}\mathsf{V}X/\equiv_{\mathcal{P}},R_{\mathcal{P}})=(\\{\mathrm{Conv}(a)\mid
a\subseteq X\\},R_{\mathcal{P}})$.

###  3.2 Posetification of analytic functors

Consider first a polynomial functor
$\mathsf{H}_{\Sigma}:\mathbf{Set}\to\mathbf{Set}$ given by a signature
$\mathrm{ar}:\Sigma\to\mathbb{N}$ and a collection of set
$(A_{\sigma})_{\sigma\in\Sigma}$

$\begin{cases}\mathsf{H}_{\Sigma}X=\coprod_{\sigma\in\Sigma}A_{\sigma}\times
X^{\mathrm{ar}(\sigma)}\\\
\mathsf{H}_{\Sigma}f=\coprod_{\sigma\in\Sigma}\mathrm{id}_{A_{\sigma}}\times
f^{\mathrm{ar}(\sigma)}\end{cases}$

By definition of $\mathsf{H}_{\Sigma}$ on morphisms, the relation
$R_{\mathsf{H}}\subseteq\mathsf{H}_{\Sigma}\mathsf{V}X\times\mathsf{H}_{\Sigma}\mathsf{V}X$
is given by

$\big{(}(a,x_{1},\ldots,x_{\mathrm{ar}(\sigma)}),(b,y_{1},\ldots,y_{\mathrm{ar}(\sigma^{\prime})})\big{)}\in
R_{\mathsf{H}}\Leftrightarrow a=b,\sigma=\sigma^{\prime},x_{i}\leq y_{i},1\leq
i\leq\mathrm{ar}(\sigma)$

Since polynomial functors preserve weak-pullbacks we have
$R_{\mathsf{H}}=\overline{\mathsf{H}_{\Sigma}}\leq\hskip 2.0pt=\hskip
2.0pt\leq_{\mathsf{H}}$. Moreover, it is easy to see from the definition above
that $\leq_{\mathsf{H}}$ is anti-symmetric (since $\leq$ is). It follows that
$\mathsf{H}_{\Sigma}^{\prime}X$ is simply given by
$(\mathsf{H}_{\Sigma}\mathsf{V}X,R_{\mathsf{H}})$.

We can now compute the posetification of _analytic functors_ ([13]), i.e.
functors of the shape

$\mathsf{G}_{\Sigma}X=\coprod_{\sigma\in\Sigma}A_{\sigma}\times(X^{\mathrm{ar}(\sigma)}/G_{\sigma})$

where each quotient $X^{\mathrm{ar}(\sigma)}/G_{\sigma}$ is taken with respect
to the obvious action of a subgroup of the permutation group
$G_{\sigma}\subseteq\mathrm{Perm}(\mathrm{ar}(\sigma))$ on the tuples of
$X^{\mathrm{ar}(\sigma)}$. The most well-known example is the ‘bag’ or
‘multiset’ functor which is given by the choice $\Sigma=\mathbb{N}$,
$\mathrm{ar}=\mathrm{id}_{\mathbb{N}}$ and
$G_{n}=\mathrm{Perm}(n),n\in\mathbb{N}$. Analytical functors preserve weak-
pullbacks (in fact wide pullbacks, see [1]), and thus
$R_{\mathsf{G}}=\leq_{\mathsf{G}}$.

######  Proposition 2.

The posetification of an analytic functor
$\mathsf{G}_{\Sigma}:\mathbf{Set}\to\mathbf{Set}$ is given by
$\mathsf{G}_{\Sigma}^{\prime}X=(\mathsf{G}_{\Sigma}\mathsf{V}X,\overline{\mathsf{G}_{\Sigma}}\leq)$.

###### Proof.

To simplify the notation we assume that each $A_{\sigma}=1$, fix an element
$\sigma$ with arity $\mathrm{ar}(\sigma)=n$, and denote by
$[(x_{1},\ldots,x_{n})]$ the equivalence class of the tuple
$(x_{1},\ldots,x_{n})$ under the action of $G_{\sigma}$. Note that by
definition of $\mathsf{G}_{\Sigma}$, two elements of
$\mathsf{G}_{\Sigma}\mathsf{V}X$ can only be related by $\leq_{\mathsf{G}}$ if
they belong to the same $\sigma$-component of the coproduct. Moreover, if
$[(x_{1},\ldots,x_{n})]\leq_{\mathsf{G}}[(y_{1},\ldots,y_{n})]$, then by
definition there exists a permutation $\pi\in G_{\sigma}$ such that
$(x_{1},\ldots,x_{n})\leq(y_{\pi(1)},\ldots,y_{\pi(n)})$ (where $\leq$ here is
component-pointwise). Similarly, if
$[(y_{1},\ldots,y_{n})]\leq_{\mathsf{G}}[(x_{1},\ldots,x_{n})]$, there exists
a permutation $\rho\in G_{\sigma}$ such that
$(y_{1},\ldots,y_{n})\leq(x_{\rho(1)},\ldots,x_{\rho(n)})$. It follows that
$(x_{1},\ldots,x_{n})\leq(x_{\pi(\rho(1))},\ldots,x_{\pi(\rho(n))})$, and
since $\pi\rho$ is of finite order we easily get by iterating at most $n$
times that $(x_{1},\ldots,x_{n})=(x_{\pi(\rho(1))},\ldots,x_{\pi(\rho(n))})$.
This in turn implies that
$(y_{\pi(1)},\ldots,y_{\pi(n)})\leq(x_{1},\ldots,x_{n})$, from which we can
conclude that $[(x_{1},\ldots,x_{n})]=[(y_{1},\ldots,y_{n})]$. Thus
$\leq_{\mathsf{G}}=\overline{\mathsf{G}_{\Sigma}}\leq$ is anti-symmetric.

∎

In particular the posetification of the bag functor $\mathsf{B}$ is given by
$\mathsf{B}^{\prime}(X,\leq)=(\mathsf{B}\mathsf{V}X,\overline{\mathsf{B}}\leq)$.

###  3.3 Posetification of the monotone neighbourhood functor $\mathsf{M}$

Recall that the _monotone neighbourhood functor_
$\mathsf{M}:\mathbf{Set}\to\mathbf{Set}$ if defined on sets by

$\hfill\mathsf{M}X=\\{A\subseteq\mathcal{P}X\mid U\in A,U\subseteq
V\Rightarrow V\in A\\}\hfill$

and on functions $f:X\to Y$ by taking the double inverse image
$(f^{-1})^{-1}:\mathsf{M}X\to\mathsf{M}Y$. It is not hard to check that
$\mathsf{M}f$ can be described more simply as $\mathsf{M}f(A)=\hskip
1.0pt\uparrow f[A]$, where $\hskip 1.0pt\uparrow f[A]$ is the upward closure
(under inclusion) of the direct image of $A$ by $f$. With this in place we can
compute the coinserter (9)

$\textstyle{\mathsf{D}\mathsf{M}\mathsf{V}X^{\mathbbm{2}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\uparrow\pi_{1}[-]}$$\scriptstyle{\uparrow\pi_{0}[-]}$$\textstyle{\mathsf{D}\mathsf{M}\mathsf{V}X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{e_{X}}$$\textstyle{\mathsf{M}^{\prime}X.}$

This time we need to consider the relation
$R_{\mathsf{M}}\subseteq\mathsf{M}\mathsf{V}X\times\mathsf{M}\mathsf{V}X$
defined by

$\hfill(A,B)\in R_{\mathsf{M}}\Leftrightarrow\exists
C\in\mathsf{M}\mathsf{V}X^{\mathbbm{2}}.\hskip 1.0pt\uparrow\pi_{0}[C]=A\hskip
4.0pt\&\hskip 1.0pt\hskip 1.0pt\uparrow\pi_{1}[C]=B\hfill$

It is known (see [11]) that $\mathsf{M}$ does _not_ preserve weak pullbacks,
and in particular we cannot assume that the relation $R_{M}$ is transitive.
The proof of the following result can essentially be found in Theorem 8.25 of
[10]444We thank Clemens Kupke for pointing out this reference.

######  Proposition 3.

$(A,B)\in{\leq_{\mathsf{M}}}$ iff $\forall a\in A.\exists b\in B.\hskip
1.0pt\uparrow b\subseteq\hskip 1.0pt\uparrow a$ and $\forall b\in B.\exists
a\in A.\hskip 1.0pt\downarrow a\subseteq\hskip 1.0pt\downarrow b$.

For any $A\in\mathsf{M}\mathsf{V}X$ and $a\in A$, we write $\hskip
1.0pt\uparrow a$ for the upward closure of $a$ under the order of $X$, and
$\hskip 1.0pt\downarrow(\hskip 1.0pt\uparrow(A))$ for the set $\hskip
1.0pt\downarrow\\{\hskip 1.0pt\uparrow a\mid a\in A\\}$, where the downward
closure is taken with respect to the inclusion. The following corollaries are
then easy to check.

######  Corollary 4.

$A\equiv_{\mathsf{M}}B$ iff $\hskip 1.0pt\downarrow(\hskip
1.0pt\uparrow(A))=\hskip 1.0pt\downarrow(\hskip 1.0pt\uparrow(B))$, and
moreover $A\equiv_{\mathsf{M}}\hskip 1.0pt\downarrow(\hskip
1.0pt\uparrow(A))$.

######  Corollary 5.

The posetification $\mathsf{M}$ is given by
$\mathsf{M}^{\prime}X=(\mathsf{Down}(\mathsf{Up}(X)),\leq_{\mathsf{M}})$.

###  3.4 Posetification of the neighbourhood functor $\mathsf{N}$.

Consider the adjunctions
$\mathsf{F}_{\mathsf{BA}}\dashv\mathsf{U_{BA}}:\mathbf{BA}\to\mathbf{Set}$ and
$\mathsf{F_{CABA}}\dashv\mathsf{U_{CABA}}:\mathbf{CABA}\to\mathbf{Set}$. The
monad $\mathsf{U_{BA}}\mathsf{F}_{\mathsf{BA}}$ is naturally isomorphic to the
finitary version $\mathsf{N}_{f}$ of the neighbourhood functor $\mathsf{N}$. A
natural isomorphism is given by the natural transformation
$\alpha:\mathsf{N}_{f}\to\mathsf{U}_{\mathbf{BA}}\mathsf{F}_{\mathbf{BA}}$
given at each $X$ by

$\hfill\alpha_{X}(A)=\bigvee\\{\bigwedge a\wedge\bigwedge(a)^{c}\mid a\in
A\\}\hfill$

which is indeed a boolean term since $A$ and each $a\in A$ are finite. The
inverse of $\alpha$ is built as follows: given a boolean term over $X$ in
conjunctive normal form, check for each clause $\bigwedge_{p\in
a_{1}}p\wedge\bigwedge_{q\in a_{2}}\neg q$ if $a_{1}\cup a_{2}=X$, if not
rewrite the clause as the equivalent CNF expression

$\hfill\bigvee\\{\bigwedge_{p\in a_{1}\cup a_{3}}p\hskip
4.30554pt\wedge\bigwedge_{q\in a_{2}\cup(a_{3})^{c}}\neg q\mid a_{3}\subseteq
X\setminus(a_{1}\cup a_{2})\\}\hfill$

This yields a finite disjunction $\bigvee\\{\bigwedge_{p\in
a_{i}}p\wedge\bigwedge_{q\notin a_{i}}\neg q\mid i\in I\\}$, which we
associate with $\\{a_{i}\\}_{i\in I}\in\mathsf{N}_{f}X$. Similarly, the monad
$\mathsf{U_{CABA}}\mathsf{F_{CABA}}$ is naturally isomorphic to the full
neighbourhood functor $\mathsf{N}$. We can use the special properties of the
adjunctions above to compute the posetification of $\mathsf{N}_{f}$ and
$\mathsf{N}$ indirectly, but relatively straightforwardly.

######  Proposition 6.

Let $X$ be a poset presented by the coinserter
$\mathsf{D}\mathsf{V}X^{\mathbbm{2}}\rightrightarrows\mathsf{D}\mathsf{V}X\stackrel{{\scriptstyle
c^{\prime}}}{{\longrightarrow}}X$ and let $\mathsf{F}\dashv\mathsf{U}$ denote
either of the adjunctions $\mathsf{F}_{\mathsf{BA}}\dashv\mathsf{U_{BA}}$ or
$\mathsf{F_{CABA}}\dashv\mathsf{U_{CABA}}$, then the coinserter of
$\mathsf{F}\mathsf{V}X^{\mathbbm{2}}\rightrightarrows\mathsf{F}\mathsf{V}X$ is
$\mathsf{F}c:\mathsf{F}\mathsf{V}X\to\mathsf{F}\mathsf{C}X$, where
$c:\mathsf{V}X\to\mathsf{C}X$ is the adjoint of $c^{\prime}$.

###### Proof.

Note first that $c$ coequalizes
$\pi_{0},\pi_{1}:\mathsf{V}X^{\mathbbm{2}}\rightrightarrows\mathsf{V}X$;
indeed two elements $x,y$ lie in the same connected component precisely when
$x\leq y$ or $y\leq x$. It follows that $Fc$ coequalizes
$\mathsf{F}\mathsf{V}X^{\mathbbm{2}}\rightrightarrows\mathsf{F}\mathsf{V}X$,
and in particular $Fc\circ\pi_{0}\leq Fc\circ\pi_{1}$. We need to show that it
is in fact a coinserter for which, due to Prop.1, it is enough to show that it
is a coequaliser. Let $d:\mathsf{F}\mathsf{V}X\to Y$ with
$d\circ\mathsf{F}\pi_{0}=d\circ\mathsf{F}\pi_{1}$. Let
$d^{\prime}:\mathsf{V}X\to\mathsf{U}Y$ be the adjoint transpose of $d$. We
have that $d^{\prime}$ factors through $c$. Writing
$\eta:\mathsf{Id}\to\mathsf{U}\mathsf{F}$ for the unit of the adjunction, it
follows that there is a unique $f:\mathsf{F}\mathsf{C}X\to Y$ such that
$\mathsf{U}f\circ\eta_{CX}\circ c=d^{\prime}$, or, equivalently, that
$f\circ\mathsf{F}c=d$. We have shown that $\mathsf{F}c$ is the coequaliser
(and coinserter) of
$\mathsf{F}\mathsf{V}X^{\mathbbm{2}}\rightrightarrows\mathsf{F}\mathsf{V}X$. ∎

######  Lemma 7.

$\mathsf{U_{BA}}$ and $\mathsf{U_{CABA}}$ preserve reflexive coequalisers.

###### Proof.

Being a variety of finitary algebras, $\mathsf{U_{BA}}$ preserves sifted
colimits and, in particular, reflexive coequalisers [2]. In the case of
$\mathsf{U_{CABA}}$ we use that $\mathbf{CABA}$ is equivalent to
$\mathbf{Set}^{\mathrm{op}}$ and that
$[-,2]:\mathbf{Set}^{\mathrm{op}}\to\mathbf{Set}$ preserves reflexive
coequalisers, see [4, 5.1.5 Lemma]. ∎

######  Theorem 8.

The posetification of $\mathsf{N}_{f}$ is $\mathsf{D}\mathsf{N}_{f}\mathsf{C}$
and the posetification of $\mathsf{N}$ is $\mathsf{D}\mathsf{N}\mathsf{C}$.

###### Proof.

We use the notation of Proposition 6. It follows from (3) that $\mathsf{D}$
preserves all ordinary colimits and, in particular, reflexive coequalizers.
Due to the lemma $\mathsf{U}$ preserves reflexive coequalizers. Like all
functors, $\mathsf{D}$ and $\mathsf{U}$ preserve the symmetry of coinserters.
It follows from Proposition 6 that

$\textstyle{\mathsf{D}\mathsf{U}\mathsf{F}\mathsf{V}X^{\mathbbm{2}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{D}\mathsf{U}\mathsf{F}\pi_{0}}$$\scriptstyle{\mathsf{D}\mathsf{U}\mathsf{F}\pi_{1}}$$\textstyle{\mathsf{D}\mathsf{U}\mathsf{F}\mathsf{V}X^{\mathbbm{2}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{D}\mathsf{U}\mathsf{F}\mathsf{C}X}$

is a coequalizer and coinserter. Thus
$\mathsf{D}\mathsf{U}\mathsf{F}\mathsf{C}$ is the posetification of
$\mathsf{U}\mathsf{F}$. ∎

######  Remark 1.

This result is curious at first sight. Due to (3) and (7),
$\mathsf{D}\mathsf{N}_{f}\mathsf{C}$ and $\mathsf{D}\mathsf{N}\mathsf{C}$ are
also the _right_ Kan-extensions of $\mathsf{N}_{f}$ and $\mathsf{N}$,
respectively. To better understand the situation let us recall that we need
the posetification to be locally monotone, which means that it must be an
_enriched_ left Kan extension. Now, working in the ordered setting (ie
$\mathbf{Pos}$-enriched), Prop.1 enforces that Boolean algebras cannot be
quotiented by a partial order in $\mathbf{BA}$ without quotienting by its
symmetric closure.

For example, let $X=\\{p<q\\}$, so that $\mathsf{V}X=\\{p,q\\}$ and
$\mathsf{V}X^{\mathbbm{2}}=\\{(p,p),(p,q),(q,q)\\}$. Then dividing
$\mathsf{F}\mathsf{V}X$ by $p\leq q$ ‘equationally’ gives the Boolean algebra
$2^{3}$ whereas the coinserter gives $\mathsf{F}1=2^{2}$. In more detail:
Dividing $\mathsf{F}\mathsf{V}X$ by $p\leq q$ (or $p\wedge q=p$ or
$p\wedge\neg q=0$) gives the Boolean algebra $2^{3}$ because
$\mathsf{F}\mathsf{V}X=2^{4}$ and $p\leq q$ kills one of the 4 atoms, namely
$p\wedge\neg q$. On the other hand, the coinserter divides
$\mathsf{F}\mathsf{V}X$ by a larger theory, namely by one in which negation is
monotone. (Recall that in the $\mathbf{Pos}$-enriched setting all operations
are monotone. Of course, one can still have algebras with “non-monotone”
operations like negation in $\mathbf{BA}$, but then the
$\mathbf{Pos}$-enriched order must be discrete. Which does not prevent us from
recovering the natural order of $\mathbf{BA}$s by considering $\mathbf{BA}$ as
a subcategory of $\mathbf{DL}$.)

##  4 Positivication

As mentioned in the introduction, a boolean coalgebraic logic is given by an
endofunctor $T:\mathbf{Set}\to\mathbf{Set}$ determining the type of
coalgebraic semantics, and an endofunctor $L:\mathbf{BA}\to\mathbf{BA}$
constructing general ‘modal algebras’. We have just seen how to extend a
functor $T:\mathbf{Set}\to\mathbf{Set}$ to a functor
$T^{\prime}:\mathbf{Pos}\to\mathbf{Pos}$ to extend a type of coalgebraic
semantics to posets. Now we want to extend a boolean syntax-building functor
to a positive syntax-building functor $L^{\prime}:\mathbf{DL}\to\mathbf{DL}$.

An obvious idea is to work dually to the posetification procedure and define
the _positivication_ of $L:\mathbf{BA}\to\mathbf{BA}$ as the right Kan
extension $L^{\prime}=\mathrm{Ran}_{\mathsf{W}}(\mathsf{W}L)$, where
$\mathsf{W}$ is the inclusion $\mathbf{BA}\to\mathbf{DL}$.555$\mathsf{W}$ is
fully faithful. Moreover, whereas $B\in\mathbf{BA}$ is discrete (see Section
2.2), $\mathsf{W}B\in\mathbf{DL}$ is equipped with its natural order. So while
$\mathsf{W}$ ‘forgets negation’ it also ‘adds the order’. Note that this gives
us what we would expect: (i) an isomorphism
$\beta:L^{\prime}\mathsf{W}\cong\mathsf{W}L$, saying that $L^{\prime}$ is the
same as $L$ on boolean algebras and (ii) for all $H:\mathbf{DL}\to\mathbf{DL}$
and all $\alpha:H\mathsf{W}\to\mathsf{W}L$ there is a unique $\gamma:H\to
L^{\prime}$ such that $\beta\circ\gamma=\alpha$, saying that $L^{\prime}$ is
the optimal (or co-universal) extension with (i).

It is also worth emphasising that $\beta:L^{\prime}\mathsf{W}\cong\mathsf{W}L$
will be doing some real work once the abstract framework is instantiated with
concrete examples. In particular, $\beta^{-1}$ will translate a boolean
formula $\phi$ in $LB$ into a positive formula $\beta_{B}^{-1}(\phi)$ where
negation is eliminated from the modal part and pushed “onto the atoms in $B$”.

In order to capture this process of eliminating negation in the abstract
categorical framework, we need to understand, once again, the Kan extension in
the $\mathbf{Pos}$-enriched way. To compute these right Kan extensions we use
a presentation of distributive lattices which will play the same role in the
computation of positivications as (6) played in the case of posetifications.

######  Proposition 9.

Every $A\in\mathbf{DL}$ is the inserter of a diagram of boolean algebras
(where $in_{1},in_{2}$ are the canonical embeddings and $e$ is the unit at $A$
of the adjunction $\mathsf{G}\dashv\mathsf{W}_{o}$):

$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{e}$$\textstyle{\mathsf{W}\mathsf{G}A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{W}\mathsf{G}in_{2}}$$\scriptstyle{\mathsf{W}\mathsf{G}in_{1}}$$\scriptstyle{\uparrow}$$\textstyle{\mathsf{W}\mathsf{G}(\mathbbm{2}\bullet
A)}$ (10)

######  Remark 2.

  1. 1.

The tensor $\mathbbm{2}\bullet A$ is isomorphic to $A+A$ modulo inequations
$in_{1}a\leq in_{2}a$. If $a\in A$ has a complement then $in_{1}a=in_{2}a$. If
all elements of $A$ are complemented, that is, if the distributive lattice $A$
happens to be a boolean algebra, then $\mathbbm{2}\bullet A\cong A$.

  2. 2.

Equivalently, $\mathbbm{2}\bullet A$ can be represented as the distributive
lattice generated by $\\{\Box_{1}a\mid a\in A\\}$ and $\\{\Box_{2}a\mid a\in
A\\}$ modulo equations specifying that $\Box_{1},\Box_{2}$ preserve all
$\mathbf{DL}$-operations and modulo inequations $\Box_{1}a\leq\Box_{2}a$.

  3. 3.

Let $A^{\partial}$ be the Priestley space dual to $A\in\mathbf{DL}$, that is,
the space of prime filters on $A$. Then $2\bullet A$ is dual to
$(A^{\partial})^{\mathbbm{2}}$. 666Cotensors in Priestley spaces are computed
as cotensors in $\mathbf{Pos}$, since the forgetful functor from Priestely
spaces to posets preserves and creates all $\mathbf{Pos}$-enriched limits.

  4. 4.

The inserters (10) are reflexive. This follows easily from the definition of
tensor with $\mathbbm{2}$ as ${\cal A}(\mathbbm{2}\bullet
A,A^{\prime})\cong[\mathbbm{2},{\cal A}(A,A^{\prime})]$ giving us a half-
inverse $\mathbbm{2}\bullet A\to A$ of both
$in_{1},in_{2}:A\to\mathbbm{2}\bullet A$ as the transpose of the map
$\mathbbm{2}\to{\cal A}(A,A)$ which maps both truth values to
$\mathrm{id}_{A}$.

###### Proof of Prop.9.

Let $(-)^{\partial}$ be the functor that dualises $\mathbf{DL}$s to Priestley
spaces. Its composition with the forgetful functor to posets we denote by
$\mathsf{S^{\prime}}:\mathbf{DL}\to\mathbf{Pos}$. Applying it to (10) yields a
reflexive coinserter in $\mathbf{Pos}$

$\textstyle{\mathsf{S^{\prime}}A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{D}\mathsf{V}(\mathsf{S^{\prime}}A)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\uparrow}$$\textstyle{\mathsf{D}\mathsf{V}(\mathsf{S^{\prime}}A)^{\mathbbm{2}}}$
(11)

as in (5). Now it only remains to check that it is also a coinserter in
Priestley spaces, from which the result follows by duality. ∎

The following theorem requires some knowledge of enriched category theory.
Even though the theorem is one of the main contributions, we encourage the
reader so inclined to skip directly ahead to its corollary, which is all that
is needed to follow the rest of the paper.

######  Theorem 10.

$\mathsf{W}:\mathbf{BA}\to\mathbf{DL}$ is co-dense and the inserters (10) form
a co-density presentation in the sense of [16, Thm 5.19].

Together with [16, Thm 5.30] we obtain

######  Corollary 11.

Every $\mathbf{BA}$-endofunctor $L$ has a positivication $L^{\prime}$ which
can be computed explicitly at any distributive lattice $A$ as the inserter

$\textstyle{L^{\prime}A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{W}L\mathsf{G}A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{W}L\mathsf{G}in_{2}}$$\scriptstyle{\mathsf{W}L\mathsf{G}in_{1}}$$\scriptstyle{\uparrow}$$\textstyle{\mathsf{W}L\mathsf{G}(\mathbbm{2}\bullet
A)}$ (12)

Moreover, a functor is a positivication iff it preserves Boolean algebras and
the inserters (10).

######  Proposition 12.

If $L:\mathbf{BA}\to\mathbf{BA}$ is finitary, then so is its positivication
$L^{\prime}:\mathbf{DL}\to\mathbf{DL}$.

###### Proof.

All operations involved in (12), that is, $\mathsf{W}$, $L$, $\mathsf{G}$,
$\mathbbm{2}\bullet-$, preserve filtered colimits. And filtered colimits
commute with finite weighted limits, see [15, Prop.4.9].777We are grateful to
John Power for pointing out this reference. ∎

###  4.1 Positivication of normal modal logic

Of course, the positivication of Kripke’s normal modal logic with one meet-
preserving $\Box$ should turn out to be Dunn’s positive modal logic [8]. We
show this in a roundabout way which has the advantage of making precise the
relationship of our notion of positivication with the procedure employed in
[3].

To summarise, going back to Diagrams (1) and (2), [3] starts with $T$ and
then, on the one hand define $L$ via $LB=\mathsf{P}T\mathsf{S}B$ on finite
$\mathbf{BA}$s and, on the other hand, define $L^{\prime}$ via
$L^{\prime}A=\mathsf{P}^{\prime}T^{\prime}\mathsf{S^{\prime}}A$ on finite
$\mathbf{DL}$s with $T^{\prime}$ the posetification of $T$.

######  Theorem 13.

Let $T:\mathbf{Set}\to\mathbf{Set}$ preserve finite sets and let $L$ be given
on finite $B\in\mathbf{BA}$ by $LB=\mathsf{P}T\mathsf{S}B$. Let $T^{\prime}$
be the posetification of $T$ and let $L^{\prime}$ be given on finite
$A\in\mathbf{DL}$ by
$L^{\prime}A=\mathsf{P}^{\prime}T^{\prime}\mathsf{S^{\prime}}A$. Then
$L^{\prime}$ is the positivication of $L$.

###### Proof.

We have to show that $L^{\prime}=\mathrm{Ran}_{W}WL$. By duality and
definition of $T^{\prime}$ as $\mathrm{Lan}_{D}DT$, we know that $L^{\prime}$
and $\mathrm{Ran}_{W}WL$ agree on finite $\mathbf{DL}$s. Now the claim follows
from Prop.12. ∎

######  Remark 3.

  1. 1.

The conditions of the theorem are not strong enough to guarantee that
$L^{\prime}$ is strongly finitary and thus has a presentation by operations
and equations. As shown in [3, Thm 6.20], this is the case if $T$ preserves
weak pullbacks.

  2. 2.

In the case of graded modal logic, $L$ is different from
$\mathsf{P}T\mathsf{S}$ even on finite $\mathbf{BA}$s. Therefore, the approach
of [3] cannot be applied. We leave a description of the positivication of
graded modal logic for a sequel.

Now, if, in the notation of the theorem, we start with $T$ as the powerset
functor, it is well known that $L$ is Kripke’s normal modal logic and [3]
shows that $L^{\prime}$ is Dunn’s positive modal logic. It follows from
Theorem 13, that the latter is indeed the positivication of the former.

###  4.2 Positivication of non-monotone modal logics

The basic idea of positivication is the following. Given a modal logic with
monotone modalities, add the duals and find the axioms so that boolean
negation can be pushed to the atoms. But our abstract definition of
positivication is powerful enough to also apply to logics which have
modalities that are not monotone.

We will study what happens in such a situation through the example of the
modal logic with one $\Box$ that does not obey any equations, not even
monotonicity. In our functorial setting, this logic is given by
$L=\mathsf{F}_{\mathsf{BA}}\mathsf{U_{BA}}:\mathbf{BA}\to\mathbf{BA}$. Recall
the functors $\mathsf{W},\mathsf{K},\mathsf{G}$ from (4).

######  Theorem 14.

The positivication of
$\mathsf{F}_{\mathsf{BA}}\mathsf{U_{BA}}:\mathbf{BA}\to\mathbf{BA}$ is
$\mathsf{W}\mathsf{F}_{\mathsf{BA}}\mathsf{U_{BA}}\mathsf{K}:\mathbf{DL}\to\mathbf{DL}$.

###### Proof.

We know from Theorem 8 that
$\mathrm{Lan}_{\mathsf{D}}\mathsf{D}\mathsf{U_{BA}}\mathsf{F}_{\mathsf{BA}}=\mathsf{D}\mathsf{U_{BA}}\mathsf{F}_{\mathsf{BA}}\mathsf{C}$.
By duality, on finite $\mathbf{DL}$s,
$\mathrm{Ran}_{\mathsf{W}}\mathsf{W}\mathsf{F}_{\mathsf{BA}}\mathsf{U_{BA}}=\mathsf{W}\mathsf{F}_{\mathsf{BA}}\mathsf{U_{BA}}\mathsf{K}$.
Now the result follows from Prop.12 since all of
$\mathsf{W},\mathsf{F}_{\mathsf{BA}},\mathsf{U_{BA}},\mathsf{K}$ are finitary.
∎

######  Remark 15.

From a logical point of view, the appearance of
$\mathsf{K}:\mathbf{DL}\to\mathbf{BA}$ in Thm 14 tells us that, given
$A\in\mathbf{DL}$, we are only allowed to build a formula $\Box a$, $a\in A$,
_if $a$ lies in a boolean subalgebra_ (ie $a$ has a complement). This side
condition takes us out of the realm of equational logic and, hence, of modal
logics given by axioms. This is related to the fact that $\mathsf{K}$ is _not_
strongly finitary [3, Example 6.6] and, therefore, functors involving
$\mathsf{K}$ cannot be expected to have a presentation by operations and
equations.

To give another example of an extension by non-monotone modalities, the logic
$\mathsf{W}_{o}\mathsf{G}:\mathbf{DL}_{o}\to\mathbf{DL}_{o}$ is a modal logic
over distributive lattices with one unary modality obeying the axioms of
negation. In other words, $\mathsf{W}_{o}\mathsf{G}$-algebras over
$\mathbf{DL}_{o}$ are just boolean algebras. Clearly,
$\mathsf{W}_{o}\mathsf{G}$ is not locally monotone and negation, considered as
a unary modality, cannot be ‘positivised’. Nevertheless, writing $I$ for the
inclusion $\mathbf{DL}_{o}\to\mathbf{DL}$, the right Kan extension
$\mathrm{Ran}_{I}I\mathsf{W}_{o}\mathsf{G}$ does exist and is the identity.

######  Proposition 16.

$\mathrm{Ran}_{I}I\mathsf{W}_{o}\mathsf{G}=\mathsf{Id}$.

###### Proof.

Going back to (8), we have $\tilde{H}=\mathsf{W}_{o}\mathsf{G}$, which means
that we can take $H=\mathsf{Id}$. But then, by Thm 10 and [16, Thm 5.1], we
have $H^{\prime}=\mathsf{Id}$. ∎

To summarise, we have seen two examples of positivication of modal extensions
by non-monotone modalities. In the first case, the non-monotone modality was
made monotone by adding a side-condition restricting its use. In the second
case, the non-monotone modality was eliminated.

##  5 Positive coalgebraic logic

###  5.1 Semantics

Recall from the introduction that we wish to move from an ordinary BCL given
by the diagram (1) to a $\mathbf{Pos}$-enriched PCL given by diagram (2). In
Sections 3 and 4 we have shown how to build $T^{\prime}$ from $T$ and
$L^{\prime}$ from $L$ respectively. The missing element is the construction of
$\delta^{\prime}$ from $\delta$. Let us first remind the reader of how
$\delta$ defines the interpretation, this will also be the occasion to fix
some notation.

######  Theorem 17 ([21]).

An endofunctor $L$ on a variety $\mathcal{A}$ has a finitary presentation by
operations and equations iff it preserves sifted colimits, in which case
$\mathrm{Alg}(L)$ is a variety.

For $L$ strongly finitary on either $\mathbf{BA}$ or $\mathbf{DL}$ and $A$ an
object of the corresponding category, let $\mathsf{F}_{L}(A)$ denote the free
$L$-algebra over $A$. In particular, if $V$ denotes a countable set of
propositional variables and $\mathsf{F}V$ is the freely generated object over
$V$ in $\mathbf{BA}$ or $\mathbf{DL}$, then the free $L$-algebra
$\mathsf{F}_{L}(\mathsf{F}V)$ is the algebra of $L$-modal formulas for the
syntax defined by $L$, which we denote more succinctly by $\mathcal{L}$. Now,
let $\gamma:X\to TX$ be a $T$-coalgebra and assume that it comes equipped with
a _valuation_ $v:\mathsf{F}V\to\mathsf{P}X$, the interpretation map
$\llbracket-\rrbracket_{(\gamma,v)}$ is the unique map given by initiality of
$\mathcal{L}$ amongst $L(-)+\mathsf{F}V$-algebras.

$\textstyle{L\mathcal{L}+\mathsf{F}V\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\simeq}$$\scriptstyle{L\llbracket-\rrbracket_{(\gamma,v)}+\mathrm{id}_{\mathsf{F}V}}$$\textstyle{\mathcal{L}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\llbracket-\rrbracket_{(\gamma,v)}}$$\textstyle{L\mathsf{P}X+\mathsf{F}V\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\delta_{X}+\mathrm{id}_{\mathsf{F}V}}$$\textstyle{\mathsf{P}TX+\mathsf{F}V\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{P}\gamma+v}$$\textstyle{\mathsf{P}X}$

We can now turn to defining $\delta^{\prime}$ from $\delta$. To avoid
unsightly $(-)^{\mathrm{op}}$ symbols appearing everywhere we simply consider
$\mathsf{P},\mathsf{P}^{\prime},\mathsf{S},\mathsf{S^{\prime}}$ to be
_contravariant functors_ throughout (as opposed to covariant functors from/to
an $(-)^{\mathrm{op}}$ category). The following definition was given in [3].

######  Definition 4.

A logic $(L^{\prime},\delta^{\prime})$ for $T^{\prime}$ is _a positive
fragment_ of the logic $(L,\delta)$ for $T$, if there exist natural
transformations $\alpha:T^{\prime}\mathsf{D}\to\mathsf{D}T$ and
$\beta:L^{\prime}\mathsf{W}\to\mathsf{W}L$ such that
$\mathsf{W}\delta\circ\beta\mathsf{S}=\mathsf{S^{\prime}}\alpha\circ\delta^{\prime}\mathsf{D}$.

Clearly, we have natural transformations
$\alpha:T^{\prime}\mathsf{D}\to\mathsf{D}T$ and
$\beta:L^{\prime}\mathsf{W}\to\mathsf{W}L$ by construction of the
posetification $T^{\prime}$ and of the positivication $L^{\prime}$. We can
construct a natural transformation $\delta^{\prime}$ as follows. First, it is
not hard to check that
$\mathsf{W}\circ\mathsf{P}=\mathsf{P}^{\prime}\circ\mathsf{D}$. Thus, given a
natural transformation $\delta:L\mathsf{P}\to\mathsf{P}T$ we get a natural
transformation

$L^{\prime}\mathsf{P}^{\prime}\mathsf{D}=L^{\prime}\mathsf{W}\mathsf{P}\stackrel{{\scriptstyle\beta_{\mathsf{P}}}}{{\Longrightarrow}}\mathsf{W}L\mathsf{P}\stackrel{{\scriptstyle
W\delta}}{{\Longrightarrow}}W\mathsf{P}T=\mathsf{P}^{\prime}\mathsf{D}T$

######  Lemma 18.

For any poset $X$, the following diagram is an inserter:

$\textstyle{\mathsf{P}^{\prime}T^{\prime}X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{P}^{\prime}\mathsf{D}T\mathsf{V}X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{P}^{\prime}\mathsf{D}T\pi_{1}}$$\scriptstyle{\mathsf{P}^{\prime}\mathsf{D}T\pi_{0}}$$\textstyle{\mathsf{P}^{\prime}\mathsf{D}T\mathsf{V}X^{\mathbbm{2}}}$

###### Proof.

$\mathsf{D}TX_{0}\rightrightarrows\mathsf{D}TX_{1}\to T^{\prime}X$ is a
coinserter and since $\mathsf{P}^{\prime}$ is the enriched hom functor
$\hom(-,\mathbbm{2})$ it turns coinserters into inserters. ∎

By naturality of $\beta$ and $\delta$, the two right-hand side squares of the
following diagram commute, and this defines a $\mathbf{Pos}$-enriched natural
transformation
$\delta^{\prime}:L^{\prime}\mathsf{P}^{\prime}\to\mathsf{P}^{\prime}(T^{\prime})$.

$\textstyle{L^{\prime}\mathsf{P}^{\prime}X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\delta^{\prime}_{X}}$$\textstyle{L^{\prime}\mathsf{P}^{\prime}\mathsf{D}\mathsf{V}X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{L^{\prime}\mathsf{P}^{\prime}\mathsf{D}\pi_{1}}$$\scriptstyle{L^{\prime}\mathsf{P}^{\prime}\mathsf{D}\pi_{0}}$$\scriptstyle{\mathsf{W}\delta_{\mathsf{V}X}\circ\beta_{\mathsf{P}\mathsf{V}X}}$$\textstyle{L^{\prime}\mathsf{P}^{\prime}\mathsf{D}\mathsf{V}X^{\mathbbm{2}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{W}\delta_{\mathsf{V}X^{\mathbbm{2}}}\circ\beta_{\mathsf{P}\mathsf{V}X^{\mathbbm{2}}}}$$\textstyle{\mathsf{P}^{\prime}T^{\prime}X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{P}^{\prime}\mathsf{D}T\mathsf{V}X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{P}^{\prime}\mathsf{D}T\pi_{1}}$$\scriptstyle{\mathsf{P}^{\prime}\mathsf{D}T\pi_{0}}$$\textstyle{\mathsf{P}^{\prime}\mathsf{D}T\mathsf{V}X^{\mathbbm{2}}}$
(13)

######  Theorem 19.

With $\delta^{\prime}$ defined as above, the logic
$(L^{\prime},\delta^{\prime})$ for $T^{\prime}$ is a positive fragment of the
logic $(L,\delta)$ for $L^{\prime}$.

###### Proof.

We need to check that
$\mathsf{W}\delta\circ\beta\mathsf{S}=\mathsf{S^{\prime}}\alpha\circ\delta^{\prime}\mathsf{D}$.
Given a set $X$, the poset $\mathsf{D}X$ has a completely trivial coinserter
presentation given by $\mathsf{D}X\rightrightarrows\mathsf{D}X\to\mathsf{D}X$,
and in particular $T^{\prime}\mathsf{D}X=\mathsf{D}TX$, i.e.
$\alpha_{X}=\mathrm{id}_{X}$, and the result follows from the diagram (13). ∎

###  5.2 Completeness

We say that a BCL or a PCL $(L,\delta)$ is _weakly complete_ for
$T$-coalgebras if for any formulas $\phi,\psi\in\mathcal{L}$ such that
$\phi\nleq\psi$, there exists a $T$-coalgebra $\gamma:X\to TX$ and a valuation
$v:\mathsf{F}_{\mathsf{BA}}V\to\mathsf{P}X$
($v:\mathsf{F}_{\mathsf{DL}}V\to\mathsf{P}^{\prime}X$ for posets) and an
element $x\in X$ such that $x\in\llbracket\phi\rrbracket_{(\gamma,v)}$ but
$x\notin\llbracket\psi\rrbracket_{(\gamma,v)}$. The following theorem gives a
sufficient condition for weak completeness.

######  Theorem 20 ([17]).

A BCL or a PCL $(L,\delta)$ for a functor $T$ is weakly complete if $\delta$
is component-wise injective.

Weak completeness transfers from a boolean logic to its positive fragment.

######  Theorem 21.

For a BCL $(L,\delta)$ defined by a strongly finitary functor
$L:\mathbf{BA}\to\mathbf{BA}$, if $\delta$ is component-wise injective, then
so is $\delta^{\prime}$. In particular $(L^{\prime},\delta^{\prime})$ is then
weakly complete.

###### Proof.

Recall first that finitary (and thus strongly finitary) functors
$L:\mathbf{BA}\to\mathbf{BA}$ preserve injective maps ([20, Lemma 6.14]).
Since the natural transformation $\beta:L^{\prime}\mathsf{W}\to\mathsf{W}L$ is
an isomorphism, it follows that the vertical legs of (13) are injective. Since
$\mathsf{P}^{\prime}=(-,\mathbbm{2})$ turns coinserters into inserters and
$L^{\prime}$ preserves inserters by construction, the top row of (13) is an
inserter as well, and hence injective. It follows that $\delta^{\prime}_{X}$
must be injective. ∎

The case of normal modal logic. Let $L:\mathbf{BA}\to\mathbf{BA}$ be the
syntax-building functor for normal modal logic:

$LA=(\mathsf{F}_{\mathsf{BA}}\mathsf{U_{BA}}A)/\\{\Diamond(a\vee b)=\Diamond
a\vee\Diamond b,\Diamond\bot=\bot\\}$

and let $\delta:L\mathsf{P}\to\mathsf{P}\mathcal{P}$ be the semantic
transformation for normal modal logic, i.e.

$\delta_{X}(\Diamond U)=\\{V\subseteq X\mid V\cap U\neq\emptyset\\}$

We have computed the posetification $\mathsf{P}^{\prime}$ or $\mathsf{P}$ in
Section 3 and shown that the positivication $L^{\prime}$ of $L$ is given by
Dunn’s syntax ([8]) in Section 4. The following result is well-known, and can
be shown directly.

######  Theorem 22.

The natural transformation $\delta:L\mathsf{P}\to\mathsf{P}\mathcal{P}$ is
component-wise injective.

######  Corollary 23.

If $L^{\prime}$ is the positivication of the syntax functor for normal modal
logic, $\mathcal{P}^{\prime}$ the posetification of the powerset functor, and
$\delta^{\prime}:L^{\prime}\mathsf{P}^{\prime}\to\mathsf{P}^{\prime}\mathcal{P}^{\prime}$
the semantics generated from $\delta:L\mathsf{P}\to\mathsf{P}\mathcal{P}$ by
diagram (13), then the PCL $(L^{\prime},\delta^{\prime})$ is weakly complete
for $\mathcal{P}^{\prime}$-coalgebras.

##  6 Conclusion and future work

We have presented positive coalgebraic logic at the same level of generality
as boolean coalgebraic logic, and developed a method by which boolean
coalgebraic logics can systematically be turned into positive coalgebraic
logics. We have also shown that completeness follows automatically from the
boolean case in this setup. More broadly, we have also presented a practical
application of enriched category theory in logic by showing that positive
modal logic amounts to a type of $\mathbf{Pos}$-enriched coalgebraic logic. We
believe that this perspective offers a deep insight into the fundamental
difference between boolean and positive logics.

Much remains to be investigated. First, we do not yet have much practical
experience and tools to compute positivications. As Section 4 illustrates, our
calculations are all indirect. In particular we would like to compute the
positivication of graded modal logic. On the logic side, we have good reasons
to believe that strong completeness transfers from the boolean to the positive
case for a large class of functors. On the other hand, we believe that
expressivity does not transfer in general. All this will be investigated in a
future companion publication to this work.

## References

  * [1] J. Adámek, H. P. Gumm, and V. Trnková.  Presentation of set functors: a coalgebraic perspective.  Journal of Logic and Computation, 20(5):991–1015, 2010.
  * [2] J. Adámek, J. Rosickỳ, and E. M. Vitale.  Algebraic theories: a categorical introduction to general algebra, volume 184.  Cambridge University Press, 2010.
  * [3] A. Balan, A. Kurz, and J. Velebil.  Positive fragments of coalgebraic logics.  In International Conference on Algebra and Coalgebra in Computer Science, pages 51–65. Springer, 2013.
  * [4] M. Barr and C. Wells.  Toposes, triples and theories, volume 278.  Springer-Verlag, 1985.
  * [5] S. L. Bloom and J. B. Wright.  P-varieties-a signature independent characterization of varieties of ordered algebras.  Journal of Pure and Applied Algebra, 29(1):13–58, 1983.
  * [6] S. Celani and R. Jansana.  A new semantics for positive modal logic.  Notre Dame Journal of Formal Logic, 38(1), 1997.
  * [7] C. Cirstea, A. Kurz, D. Pattinson, L. Schröder, and Y. Venema.  Modal logics are coalgebraic.  The Computer Journal, 54(1):31–41, 2009.
  * [8] J. M. Dunn.  Positive modal logic.  Studia Logica, 55(2):301–317, 1995.
  * [9] M. Gehrke, H. Nagahashi, and Y. Venema.  A Sahlqvist theorem for distributive modal logic.  Annals of pure and applied logic, 131(1):65–102, 2005.
  * [10] H. H. Hansen.  Monotonic modal logics.  Technical Report PP-2003-24, ILLC, University of Amsterdam, 2003.
  * [11] H. H. Hansen and C. Kupke.  A coalgebraic perspective on monotone modal logic.  Electronic Notes in Theoretical Computer Science, 106:121–143, 2004\.
  * [12] B. Jacobs and A. Sokolova.  Exemplaric expressivity of modal logics.  J. Log. and Comput., 20:1041–1068, October 2010.
  * [13] André Joyal.  Foncteurs analytiques et especes de structures.  Combinatoire énumérative, pages 126–159, 1986.
  * [14] K. Kapulkin, A. Kurz, and J. Velebil.  Expressiveness of positive coalgebraic logic.  Advances in Modal Logic, 9:368–385, 2012.
  * [15] G. M. Kelly.  Structures defined by finite limits in the enriched context, i.  Cahiers de topologie et géométrie différentielle catégoriques, 23(1):3–42, 1982.
  * [16] M. Kelly.  Basic concepts of enriched category theory, volume 64.  CUP Archive, 1982.
  * [17] C. Kupke, A. Kurz, and D. Pattinson.  Algebraic semantics for coalgebraic logics.  In CMCS 2004, volume 106 of ENTCS, pages 219–241, 2004\.
  * [18] C. Kupke, A. Kurz, and D. Pattinson.  Ultrafilter Extensions for Coalgebras.  In CALCO 2005, volume 3629, pages 263–277. Springer, 2005.
  * [19] C. Kupke and D. Pattinson.  Coalgebraic semantics of modal logics: an overview.  TCS, 412(38):5070–5094, 2011.  Special issue CMCS 2010.
  * [20] A. Kurz and D. Petrişan.  Presenting functors on many-sorted varieties and applications.  Information and Computation, 208(12):1421–1446, 2010.
  * [21] A. Kurz and J. Rosický.  Strongly complete logics for coalgebras.  Logical Methods in Computer Science, 8, 2012.
  * [22] A. Kurz and J. Velebil.  Quasivarieties and varieties of ordered algebras: regularity and exactness.  Mathematical Structures in Computer Science, 2016.
  * [23] L. Santocanale, Y. Venema, et al.  Uniform interpolation for monotone modal logic.  Advances in Modal Logic, 8:350–370, 2010.