# Moss’ logic for ordered coalgebras

Marta Bílková  Faculty of Arts, Charles University, Prague, Czech Republic
<EMAIL_ADDRESS>and  Matěj Dostál  Faculty of Electrical Engineering,
Czech Technical University in Prague, Czech Republic<EMAIL_ADDRESS>
###### Abstract.

We present a finitary coalgebraic logic for $T$-coalgebras, where $T$ is a
locally monotone endofunctor of the category of posets and monotone maps that
preserves exact squares and finite intersections. The logic uses a single
cover modality whose arity is given by the dual of the coalgebra functor $T$,
and the semantics of the modality is given by relation lifting. For the
finitary setting to work, we need to develop a notion of a base for subobjects
of $TX$. This in particular allows us to talk about a finite poset of
subformulas for a given formula, and of a finite poset of successors for a
given state in a coalgebra. The notion of a base is introduced generally for a
category equipped with a suitable factorisation system.

We prove that the resulting logic has the Hennessy-Milner property for the
notion of similarity based on the notion of relation lifting. We define a
sequent proof system for the logic and prove its completeness.

Marta Bílková acknowledges the support by the grant No. P202/11/P304 of the
Czech Science Foundation, and (for the revised version of the paper) by the
grant From Shared Evidence to Group Attitudes of Czech Science Foundation and
DFG, no. 16-07954J, and by Charles University research program Progres Q14
Rationality Crisis and Modern Thought. M. Dostál acknowledges the support of
the grant No. 19-0092S of the Czech Grant Agency.

##  1\. Introduction

Shortly after the theory of coalgebras emerged as a useful conceptual tool for
a uniform study of various kinds of dynamic systems, there has been an
interest in finding logics expressive enough to describe the behaviour of the
coalgebras up to bisimilarity.

For the case of coalgebras for endofunctors
$T:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$ preserving weak pullbacks,
this goal has been achieved by Moss in his pioneering paper [20], where he
introduces an expressive coalgebraic logic uniformly in the choice of the
coalgebra functor $T$. This logic has become a lively field of study. Its
finitary version has been explored by various authors, resulting in an almost
full picture, including (among others) the axiomatization and completeness
[16], a nice proof theory [4], applications to automata theory [17, 18, 15],
and applications to fixpoint logics [23, 24].

Much of the theory that has been built around Moss’ idea uses heavily that
endofunctors of ${\mathsf{Set}}$ are well understood. This is not the case for
the endofunctors on the categories of preorders and posets. One encounters
them naturally when interested in similarity rather then bisimilarity [12,
19]. For this reason (among others), poset extensions and liftings of set
functors were investigated in [2, 3]. Also a coalgebraic logic for poset
coalgebras, based on monotone predicate liftings, has been considered and
proved to be expressive in [12].

It therefore seems natural to investigate the possibilities of extending the
above mentioned results on Moss’ logic for set coalgebras beyond the category
of sets. This paper is a preliminary step in this direction, building on
results obtained in [5]. Namely, we use the existence of a functorial relation
lifting for functors preserving exact squares in the category ${\mathsf{Pos}}$
of posets and monotone maps. This provides us, as we show below, with the
technical background for the development of the Moss’ logic for poset
coalgebras. Since the results about relation lifting in [5] were further
generalised in [6] to the enriched case of ${\mathscr{V}}$-categories, where
${\mathscr{V}}$ is a commutative quantale, our ultimate future goal would be
to define Moss’ logic in this level of generality.

This paper is devoted to the ordered case. We present a finitary Moss’
coalgebraic language for coalgebras for a locally monotone functor
$T:{\mathsf{Pos}}\longrightarrow{\mathsf{Pos}}$ that preserves exact squares.
The logic is based on the language of logic of distributive lattices equipped
with a single cover modality $\nabla$ (and for the sake of proof theory later
also with its dual modality $\Delta$). The arity of both cover modalities is
the dual $T^{\partial}$ of the coalgebra functor, and the semantics of the
cover modalities uses relation lifting, proven to exist in [5].

For the finitary setting to work, one needs to develop a notion of a _base_.
In the “classical” case of a finitary coalgebraic functor
$T:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$, the base is a natural
transformation from $T$ to the powerset functor. We develop an appropriate
notion of base of a locally monotone finitary functor
$T:{\mathsf{Pos}}\longrightarrow{\mathsf{Pos}}$. Some additional assumptions
on the category ${\mathsf{Pos}}$ and the functor $T$ seem inevitable. First of
all, one has to choose a suitable factorisation system
$({\mathcal{E}},{\mathcal{M}})$ on the category ${\mathsf{Pos}}$ and the
functor $T$ should behave well with regard to the factorisation system.

We prove that if we equip ${\mathsf{Pos}}$ with the factorisation system
$({\mathcal{E}},{\mathcal{M}})$ of monotone surjections and order embeddings,
then a base can be computed for every finitary functor $T_{\omega}$ that
preserves order embeddings and their finite intersections. In particular,
bases can be used to produce, for each subobject of the poset $T_{\omega}X$, a
finite poset of its “generators”, e.g., a poset of subformulas of a formula of
arity $T_{\omega}$, or a poset of successors of a state in a coalgebra for
$T_{\omega}$.

The resulting finitary Moss’ logic has the Hennessy-Milner property — it is
expressive for a notion of simulation and similarity based on the relation
lifting. This notion of similarity coincides with the notion of similarity
given, e.g., in [25, 11, 2, 19]. The result matches the similar result for
Moss’ logic for coalgebras on the category of sets. It can also be seen as a
counterpart to the result proved in [12] for positive coalgebraic logics in
the category of posets, stating that the logic of all monotone predicate
liftings is expressive for any endofunctor of posets that satisfies our
conditions.

Instead of considering an axiomatization of the resulting logic, we define a
sound cut-free sequent proof calculus for the logic, and prove completeness.
To be able to do so, we essentially use the dual modality delta and its
relation to the nabla modality. This part of the paper closely follows
previous work [4] on proof theory of Moss’ logic in ${\mathsf{Set}}$.

### Organisation of the paper

  * •

We start by listing examples of poset endofunctors and examples of ordered
coalgebras in Section 2.

  * •

In Section 3 we study the notion of a base in a general category equipped with
a factorisation system. We describe the conditions under which an endofunctor
of a category ${\mathscr{K}}$ admits a base, and we show that a large class of
${\mathsf{Pos}}$-endofunctors admits a base.

  * •

Section 4 introduces monotone relations and the notion of relation lifting of
monotone relations. It states the main result of [5], that is, the
characterisation of locally monotone ${\mathsf{Pos}}$-endofunctors that admit
a relation lifting.

  * •

We define the syntax and semantics of Moss’ logic for ordered coalgebras in
Section 5. The syntax and semantics of this logic is parametric in the type of
coalgebras involved. We prove that the logic has Hennessy-Milner property for
the notion of a simulation of coalgebras defined by relation lifting.

  * •

In Section 6 we develop a sequent calculus for Moss’ logic that is again
parametric in the type of coalgebras involved. We give a proof of soundness
and completeness of the calculus.

  * •

Section 7 concludes with possible topics for future study.

### Acknowledgements

We would like to thank Jiří Velebil for his substantial help. His insights
were crucial in the development of the paper.

##  2\. Functors and coalgebras in ${\mathsf{Pos}}$

In this section we fix the basic notation and introduce the running examples
that are used throughout the paper. Firstly we introduce an important class of
endofunctors of posets, namely the locally monotone Kripke polynomial
functors. In the second part of this section we introduce the notion of a
coalgebra and show several examples of coalgebras for Kripke polynomial
functors.

###  2.A. Basic notions and Kripke polynomial functors

We denote by ${\mathsf{Pos}}$ the category of all posets and all monotone
maps. For every pair $X$ and $Y$ of posets the hom-set ${\mathsf{Pos}}(X,Y)$
of monotone maps from $X$ to $Y$ carries a natural partial order: given two
monotone maps $f$ and $g$ in ${\mathsf{Pos}}(X,Y)$, we define that $f\leq g$
holds if and only if $f(x)\leq g(x)$ holds for every $x\in X$ (i.e. we
introduce a pointwise order). The category ${\mathsf{Pos}}$ therefore can be
seen as enriched in posets. In cases where we need to emphasise this extra
structure of ${\mathsf{Pos}}$, we will speak of ${\mathsf{Pos}}$ as of a
2-category.

A functor $T:{\mathsf{Pos}}\longrightarrow{\mathsf{Pos}}$ is then called a
locally monotone functor (or a 2-functor), if it preserves the additional
structure present in ${\mathsf{Pos}}$: that is, if for any pair $f$, $g$ of
comparable morphisms in ${\mathsf{Pos}}$ the inequality $f\leq g$ implies that
the inequality $T(f)\leq T(g)$ holds.

The Kripke polynomial endofunctors of ${\mathsf{Pos}}$ are those defined by
the following grammar:

$T::=E\mid{\mathit{Id}}\mid T+T\mid T\times T\mid T^{E}\mid
T^{\partial}\mid{\mathbb{L}}T.$ (2.1)

We give an explanation of the building blocks of the grammar.

  1. (1)

Let $E$ be an arbitrary poset. Slightly abusing the notation, we denote by $E$
the constant-at-$E$ functor. The functor ${\mathit{Id}}$ is the identity
functor.

  2. (2)

Given two Kripke polynomial functors, their product and coproduct (in the
category of poset endofunctors) is again a Kripke polynomial functor.

  3. (3)

Given a poset $E$, we define that $T^{E}(X)=(TX)^{E}$ is the poset of all
monotone maps from $E$ to $TX$ with the pointwise ordering. The obvious action
on morphisms makes $T^{E}$ into a functor.

  4. (4)

Given a functor $T$, the functor $T^{\partial}$ is the dual of $T$, defined by
putting

$T^{\partial}X=(TX^{\mathit{op}})^{\mathit{op}}$

and again extending to the obvious action on morphisms.

  5. (5)

We denote by ${\mathbb{L}}$ the lowerset functor, with
${\mathbb{L}}X=[X^{\mathit{op}},{\mathbb{2}}]$ being the poset of all
lowersets on the poset $X$, and the order is given by inclusion. (By
${\mathbb{2}}$ we denote the two-element chain.) The lowerset functor
${\mathbb{L}}$ acts on morphisms as the direct image followed by closure:
given $f:X\longrightarrow Y$, a lowerset $l\in{\mathbb{L}}X$ is mapped by
${\mathbb{L}}f$ to ${\downarrow}f[l]$, i.e., to the lowerset generated by the
image $f[l]$ of $l$.

Observe that the dual of ${\mathbb{L}}$ is the upperset functor
${\mathbb{U}}$: for any poset $X$ we have that
${\mathbb{L}}^{\partial}X=[X,{\mathbb{2}}]^{\mathit{op}}$, and the latter is
the set of all uppersets on $X$, ordered by reversed inclusion. Therefore, the
upperset functor ${\mathbb{U}}$ is Kripke polynomial as well. For a monotone
map $f:X\longrightarrow Y$, the map
${\mathbb{U}}f:{\mathbb{U}}X\longrightarrow{\mathbb{U}}Y$ sends an upperset
$u\in{\mathbb{U}}X$ to the upperset ${\uparrow}f[u]$ generated by the image
$f[u]$ of $u$.

We will also use the _finitary_ lowerset functor ${\mathbb{L}}_{\omega}$. For
a poset $X$, the poset ${\mathbb{L}}_{\omega}X$ consists of finitely generated
lowersets on $X$. Analogously, the finitary upperset functor
${\mathbb{U}}_{\omega}$ assigns to a poset $X$ the poset of its finitely
generated uppersets, ordered by reversed inclusion. Categorically, both
functors are the finitary coreflections of the usual lowerset and upperset
functors. We will often use the notation $g(l)$ for the minimal finite set of
generators of the lowerset $l\in{\mathbb{L}}_{\omega}X$, and in the same way
$g(u)$ will denote the minimal finite set of generators for the upperset
$u\in{\mathbb{U}}_{\omega}X$.

###  2.B. Coalgebras for a functor

Given a (not necessarily locally monotone) functor
$T:{\mathsf{Pos}}\longrightarrow{\mathsf{Pos}}$, we define coalgebras and
their homomorphisms in the usual manner.

Explicitly, a coalgebra for $T$ is a monotone map $c:X\longrightarrow TX$, and
a monotone map $h:X\longrightarrow Y$ is a homomorphism from
$c:X\longrightarrow TX$ to $d:Y\longrightarrow TY$ if the following square

$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{c}$$\scriptstyle{h}$$\textstyle{TX\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Th}$$\textstyle{Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{d}$$\textstyle{TY}$

commutes.

There are various interesting structures from computer science and logic that
can be modelled as coalgebras for a suitable Kripke polynomial functor. We
show some of the examples below.

Examples of ordered coalgebraic structures.

  1. (1)

Let us consider the functor $T=A\times{\mathit{Id}}$ for some fixed poset $A$.
Coalgebras for the functor $T$ are the monotone maps
$c=\langle{\mathit{out}},{\mathit{next}}\rangle:X\longrightarrow A\times X$
that can be seen as a particularly trivial kind of automata with the set of
states $X$ and an (ordered) output alphabet $A$. Hence the monotone map
$\mathit{out}:X\longrightarrow A$ produces an output in $A$ for every state in
$X$ and the monotone map $\mathit{next}:X\longrightarrow X$ produces the next
state of the automaton.

  2. (2)

A _complete deterministic ordered automaton_ (see Chapter 2 of [21]) can be
seen as a coalgebra of the form $c:X\longrightarrow X^{A}\times{\mathbb{2}}$
where $X$ is a partial order of states, $A$ the (discrete) input alphabet, the
left-hand component of the monotone map $c$ is a monotone transition map
$x\mapsto(a\mapsto x.a)$ and its right-hand component is a monotone map from
$X$ to the two-element chain ${\mathbb{2}}$, determining the accepting states.
(In our approach there is no problem in considering the more general case of
ordered automata with an _ordered_ input alphabet; we however stick to the
definition already used in literature.)

  3. (3)

Consider the functor $T={\mathbb{L}}_{\omega}^{A}\times{\mathbb{2}}$ (with $A$
being discrete). A coalgebra
$c:X\longrightarrow({\mathbb{L}}_{\omega}X)^{A}\times{\mathbb{2}}$ is a
nondeterministic automaton consisting of an upperset $F\subseteq X$ of
accepting states, and a set $C$ of transitions of the form $(x,a,y)$ with
$x,y\in X$ and $a\in A$, satisfying two confluence properties:

    1. (a)

Whenever $(x,a,y)\in C$ and $x\leq x^{\prime}$ in $X$, it follows that
$(x^{\prime},a,y)\in C$.

    2. (b)

Whenever $(x,a,y)\in C$ and $y\leq y^{\prime}$ in $X$, it follows that
$(x,a,y^{\prime})\in C$.

Let moreover
$d:Z\longrightarrow{\mathbb{2}}\times({\mathbb{L}}_{\omega}Z)^{A}$ be an
automaton with an upperset $G\subseteq Z$ of accepting states and a set $D$ of
transitions. A monotone map $h:X\longrightarrow Z$ is a homomorphism between
$c$ and $d$ if the following three conditions are satisfied:

    1. (a)

$h[C]=D$ and $h[X\setminus C]\cap D=\emptyset$ ($h$ preserves the set of
accepting states).

    2. (b)

For every transition $(x,a,y)\in C$ there is a transition $(h(x),a,h(y))\in
D$.

    3. (c)

For every transition $(h(x),a,z)\in D$ there is a transition $(x,a,y)\in C$
with $z\leq h(y)$.

We will call coalgebras for the functor
${\mathbb{L}}_{\omega}^{A}\times{\mathbb{2}}$ _lowerset automata_.

  4. (4)

_Frames for distributive substructural logics_ [22] are frames consisting of a
poset $X$ of states, together with a ternary relation on $X$, satisfying the
following monotonicity condition:

$R(x,y,z)\mbox{ and }x^{\prime}\leq x\mbox{ and }y^{\prime}\leq y\mbox{ and
}z\leq z^{\prime}\mbox{ implies }R(x^{\prime},y^{\prime},z^{\prime}).$

In the notation of monotone relations of Section 4 below, $R$ is a monotone
relation of the form
$\textstyle{R:X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X\times
X}$.

Given a set ${\mathsf{At}}$ of atomic formulas and a monotone valuation
$X\times{\mathsf{At}}\longrightarrow{\mathbb{2}}$ of the atomic formulas, we
can interpret the fusion and implication connectives as follows:

$\displaystyle x\Vdash a_{0}\otimes a_{1}$ iff $\displaystyle\ (\exists
x_{0})(\exists x_{1})(R(x_{0},x_{1},x)\mbox{ and }x_{0}\Vdash a_{0}\mbox{ and
}x_{1}\Vdash a_{1})$ $\displaystyle x\Vdash a\rightarrow b$ iff
$\displaystyle\ (\forall y)(\forall z)\ ((R(x,y,z)\mbox{ and }y\Vdash a)\mbox{
implies }z\Vdash b)$

It has been shown in [7] that such frames can be treated as coalgebras in a
natural way so that the coalgebraic morphisms coincide with the frame
morphisms. In particular, $R$ generates a natural coalgebraic structure
$c_{\otimes}:X\longrightarrow{\mathbb{L}}(X\times X)$ for a locally monotone
functor ${\mathbb{L}}({\mathit{Id}}\times{\mathit{Id}})$, when we understand
$R$ as interpreting the fusion connective. We call $R$ finitary when the
generated coalgebraic structure is in fact of the form
$c_{\otimes}:X\longrightarrow{\mathbb{L}}_{\omega}(X\times X)$, i.e. when we
can use the finitary lowerset functor.

  5. (5)

Consider a poset $X$ equipped with a monotone relation
$\textstyle{R:X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}$.
This is a frame for positive modal logic with adjoint modalities. More in
detail, such frames with a monotone valuation enable one to interpret
conjunction, disjunction, and two monotone modalities: a forward-looking
$\Box$ and a backward-looking $\blacklozenge$. We put

$\displaystyle x\Vdash\Box a$ iff $\displaystyle\ (\forall y)\ (R(x,y)\mbox{
implies }y\Vdash a)$ $\displaystyle x\Vdash\blacklozenge a$ iff
$\displaystyle\ (\exists y)\ (R(y,x)\mbox{ and }y\Vdash a)$

The modalities $\Box$ and $\blacklozenge$ are adjoint in a sense that will be
explained in Remark 11. The relation $R$ generates two coalgebras

$c:X\longrightarrow{\mathbb{U}}X\ \ \mbox{and}\ \
d:X\longrightarrow{\mathbb{L}}X$

defined by $c(x)=\\{y\ |\ R(x,y)\\}$ and $d(x)=\\{y\ |\ R(y,x)\\}$. We say
that the frame $(X,R)$ is _finitary_ if $R$ in fact generates coalgebras

$c:X\longrightarrow{\mathbb{U}}_{\omega}X\ \ \mbox{and}\ \
d:X\longrightarrow{\mathbb{L}}_{\omega}X$

for the finitary functors ${\mathbb{U}}_{\omega}$ and ${\mathbb{L}}_{\omega}$.

We shall use some of the above coalgebras as running examples to illuminate
concretely the general theory.

##  3\. Base in a category ${\mathscr{K}}$ with a factorisation system

When studying finitary coalgebraic logics for finitary endofunctors of
${\mathsf{Set}}$, the notion of a base is of central importance. On the level
of models, the base allows us to produce a finite set of successors of a state
of the model. On the level of the logical syntax, the base yields a finite set
of subformulas of a given formula.

Technically, given a functor $T:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$,
a base is a natural transformation
${\mathsf{base}}^{T}_{X}:TX\longrightarrow{\mathbb{P}}_{\omega}X$, assigning
to each element $\alpha$ of $TX$ a finite subset of $X$, called the base of
$\alpha$. The idea is to define ${\mathsf{base}}^{T}_{X}(\alpha)$ as the
smallest finite $Z\subseteq X$ such that $\alpha\in TZ$ holds. For this idea
to work, $T$ has to satify additional conditions: it has been shown in [10]
that when $T$ preserves intersections and weakly preserves inverse images,
then the base exists and it is natural. For various properties of bases for
endofunctors of ${\mathsf{Set}}$ we refer to, e.g., [16].

In this section we explain how to define and compute a base for an endofunctor
$T:{\mathscr{K}}\longrightarrow{\mathscr{K}}$ of an arbitrary category
${\mathscr{K}}$ that is equipped with a factorisation system
$({\mathcal{E}},{\mathcal{M}})$ for morphisms. The factorisation system is
used in order to be able to imitate the powerset: the set of all subsets is
going to be replaced by the poset of ${\mathcal{M}}$-subobjects.

By applying our definition of a base to the epi-mono factorisation system on
the category of sets and mappings, we then obtain the above notion of a base,
see Example 3.B. By applying our definition of a base to the category of all
posets and all monotone maps, equipped with a suitable factorisation system,
we will be able to speak of bases in the ordered case as well. See Examples
3.A and 3.B below.

###  3.A. Factorisation systems

For more details on the general theory of factorisation systems we refer to
the book [1].

Suppose ${\mathscr{K}}$ is a category and let ${\mathcal{E}}$ and
${\mathcal{M}}$ be classes of morphisms in ${\mathscr{K}}$. We say that
$({\mathcal{E}},{\mathcal{M}})$ is a factorisation system on ${\mathscr{K}}$
(and that ${\mathscr{K}}$ is an $({\mathcal{E}},{\mathcal{M}})$-category),
provided the following conditions are satisfied:

  1. (1)

The classes ${\mathcal{E}}$ and ${\mathcal{M}}$ are closed under composition
with isomorphisms.

  2. (2)

Every morphism in ${\mathscr{K}}$ can be factorised as a morphism in
${\mathcal{E}}$ followed by a morphism in ${\mathcal{M}}$.

  3. (3)

${\mathscr{K}}$ has the $({\mathcal{E}},{\mathcal{M}})$-diagonalisation
property, i.e., for every commutative square

$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{e}$$\scriptstyle{u}$$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{v}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m}$$\textstyle{Y}$

where $e$ is in ${\mathcal{E}}$ and $m$ is in ${\mathcal{M}}$, there exists a
unique diagonal $d:B\longrightarrow X$, making both triangles in the diagram

$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{e}$$\scriptstyle{u}$$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{v}$$\scriptstyle{d}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m}$$\textstyle{Y}$

commutative.

A factorisation system $({\mathcal{E}},{\mathcal{M}})$ is called proper if
members of ${\mathcal{E}}$ are (some) epimorphisms and members of
${\mathcal{M}}$ are (some) monomorphisms.

######  Remark 1.

Any factorisation system $({\mathcal{E}},{\mathcal{M}})$ on any category
${\mathscr{K}}$ satisfies the following (see Proposition 14.6 of [1]):

  1. (1)

The classes ${\mathcal{E}}$ and ${\mathcal{M}}$ are closed under composition.

  2. (2)

The intersection ${\mathcal{E}}\cap{\mathcal{M}}$ is the class of all
isomorphisms in ${\mathscr{K}}$.

The following are examples of $({\mathcal{E}},{\mathcal{M}})$-categories
${\mathscr{K}}$:

  1. (1)

${\mathscr{K}}$ is the category ${\mathsf{Set}}$ of all sets and mappings,
${\mathcal{E}}$ is the class of all epis (=surjections) and ${\mathcal{M}}$ is
the class of all monos (=injections).

  2. (2)

${\mathscr{K}}$ is the category ${\mathsf{Pos}}$ of all posets and monotone
mappings, ${\mathcal{E}}$ is the class of all monotone surjections and
${\mathcal{M}}$ is the class of all monotone maps that reflect the order.

  3. (3)

If ${\mathscr{K}}$ is the category ${\mathsf{Pre}}$ of all preorders and
monotone mappings, one can choose from at least one of the following three
prominent factorisation systems:

    1. (a)

${\mathcal{E}}$ is the class of all monotone maps that are bijective on the
level of elements and ${\mathcal{M}}$ is the class of all monotone maps that
reflect the order.

    2. (b)

${\mathcal{E}}$ is the class of all monotone surjections and ${\mathcal{M}}$
is the class of all monotone injections that reflect the order.

    3. (c)

${\mathcal{M}}$ is the class of monotone injections. The class ${\mathcal{M}}$
is the class of all monomorphisms, hence the corresponding ${\mathcal{E}}$
necessarily coincides with the class of all strong epimorphisms, see [1].

All of the above cases, except for (3a), are proper factorisation systems.

  1. (4)

If ${\mathscr{K}}$ is an $({\mathcal{E}},{\mathcal{M}})$-category, then
${\mathscr{K}}^{\mathit{op}}$ is an $({\mathcal{M}},{\mathcal{E}})$-category.
If the factorisation system $({\mathcal{E}},{\mathcal{M}})$ on ${\mathscr{K}}$
is proper, so is the factorisation system $({\mathcal{M}},{\mathcal{E}})$ on
${\mathscr{K}}^{\mathit{op}}$.

For a factorisation system $({\mathcal{E}},{\mathcal{M}})$ on ${\mathscr{K}}$,
the morphisms in ${\mathcal{M}}$ will serve as “subobjects”. It is however
more useful to define subobjects as equivalence classes. More precisely: we
fix an object $X$ and we denote a morphism in ${\mathcal{M}}$ into $X$ by
$\textstyle{m:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}$.
We define a preorder on such morphisms by putting $m\subseteq m^{\prime}$ if
there is a factorisation

$\textstyle{Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m}$$\textstyle{Z^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m^{\prime}}$$\textstyle{X}$

The preorder defines an equivalence $m\sim m^{\prime}$ iff $m\subseteq
m^{\prime}$ and $m^{\prime}\subseteq m$. We denote the equivalence classes by
$[m]$. If the category ${\mathscr{K}}$ has a final object ${\mathbb{1}}$, we
denote the situation

$\textstyle{{\mathbb{1}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{x}$$\textstyle{Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m}$$\textstyle{X}$

by writing that $x\in m$ holds.

The equivalence class $[m]$ of
$\textstyle{m:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}$
is called an ${\mathcal{M}}$-subobject of $X$.

The class of all subobjects of $X$ is denoted by

${\mathsf{Sub}}_{\mathcal{M}}(X)$

and we consider it ordered by $[m]\subseteq[m^{\prime}]$ if $m\subseteq
m^{\prime}$.

We say that an $({\mathcal{E}},{\mathcal{M}})$-category ${\mathscr{K}}$ is
${\mathcal{M}}$-wellpowered, if every ${\mathsf{Sub}}_{\mathcal{M}}(X)$ has a
set of elements. And ${\mathscr{K}}$ is ${\mathcal{E}}$-cowellpowered, if
${\mathscr{K}}^{\mathit{op}}$ (equipped with the factorisation system
$({\mathcal{M}},{\mathcal{E}})$, see Example 3.A) is
${\mathcal{E}}$-wellpowered.

######  Remark 2.

  1. (1)

We will abuse the notation and write $m$ instead of $[m]$, and $m\subseteq
m^{\prime}$ instead of $[m]\subseteq[m^{\prime}]$.

  2. (2)

An $({\mathcal{E}},{\mathcal{M}})$-category need not be
${\mathcal{M}}$-wellpowered, even for a proper factorisation system
$({\mathcal{E}},{\mathcal{M}})$. Indeed, suppose ${\mathscr{K}}$ is the class
of all ordinals with the reversed order (so that the ordinal $0$ becomes the
top element) and consider ${\mathscr{K}}$ as a category. Put ${\mathcal{E}}$
to be the class of identity morphisms, ${\mathcal{M}}$ to be the class of all
morphisms. The factorisation system $({\mathcal{E}},{\mathcal{M}})$ on
${\mathscr{K}}$ is proper, since every morphism in ${\mathscr{K}}$ is both a
monomorphism and an epimorphism. Then it follows that
${\mathsf{Sub}}_{\mathcal{M}}(0)$ is a proper class.

  3. (3)

If ${\mathsf{Sub}}_{\mathcal{M}}(X)$ has a set of elements, then it is a
complete lattice whenever ${\mathscr{K}}$ has enough limits. In fact, it
suffices to establish the existence of infima in
${\mathsf{Sub}}_{\mathcal{M}}(X)$. The infima can be computed as limits of
diagrams of the form

$\textstyle{\vdots}$$\textstyle{Z_{i}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m_{i}}$$\textstyle{\vdots}$$\textstyle{X}$$\textstyle{(i,j\in
I)}$$\textstyle{Z_{j}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m_{j}}$$\textstyle{\vdots}$

that are called wide pullbacks of ${\mathcal{M}}$-morphisms (or, intersections
of ${\mathcal{M}}$-subobjects).

We denote by
$\textstyle{p_{i}:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{Z_{i}}$
the limit cone. Every $p_{i}$ belongs to ${\mathcal{M}}$ by the general
properties of (proper) factorisation systems, see [1], Proposition 14.15. The
composite $\textstyle{m_{i}\cdot
p_{i}:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}$
represents the ${\mathcal{M}}$-subobject that is the intersection of
$m_{i}$’s. We denote the intersection by

$\textstyle{\bigcap_{i\in
I}m_{i}:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}$

The existence of suprema in ${\mathsf{Sub}}_{\mathcal{M}}(X)$ then follows
from the existence of infima by the usual argument.

  4. (4)

When, moreover, coproducts exist in ${\mathscr{K}}$, suprema in
${\mathsf{Sub}}_{\mathcal{M}}(X)$ can be computed by an explicit formula.
Namely, the supremum $\bigcup_{i\in I}m_{i}$ (called the union of $m_{i}$’s)
can be computed as the ${\mathcal{M}}$-part

$\textstyle{\bigcup_{i\in
I}m_{i}:C\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}$

of the $({\mathcal{E}},{\mathcal{M}})$-factorisation of the unique cotupling
morphism $m:\coprod_{i\in I}Z_{i}\longrightarrow X$ as follows:

---
$\textstyle{\vdots}$$\textstyle{Z_{i}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{\sf{inj}}\,_{i}}$$\scriptstyle{m_{i}}$$\textstyle{\vdots}$$\textstyle{\coprod\limits_{i\in
I}Z_{i}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{C\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\bigcup_{i\in
I}m_{i}}$$\textstyle{X}$$\textstyle{Z_{j}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{\sf{inj}}\,_{j}}$$\scriptstyle{m_{j}}$$\textstyle{\vdots}$

###  3.B. General bases

For the rest of this section we assume the following three conditions:

  1. (1)

${\mathscr{K}}$ is an $({\mathcal{E}},{\mathcal{M}})$-category for a proper
factorisation system $({\mathcal{E}},{\mathcal{M}})$.

  2. (2)

${\mathscr{K}}$ is ${\mathcal{M}}$-wellpowered (i.e., we assume that every
${\mathsf{Sub}}_{\mathcal{M}}(X)$ has a set of elements).

  3. (3)

$T:{\mathscr{K}}\longrightarrow{\mathscr{K}}$ is a functor which preserves
${\mathcal{M}}$-morphisms.

An ${\mathcal{M}}$-subobject
$\textstyle{{\mathsf{base}}_{X}(\alpha):\widetilde{Z}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}$
is called a base of an ${\mathcal{M}}$-subobject
$\textstyle{\alpha:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{TX}$
provided that the following holds for every
$\textstyle{m:Z^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}$

${\mathsf{base}}_{X}(\alpha)\subseteq m$ holds in
${\mathsf{Sub}}_{\mathcal{M}}(X)$

iff

$\alpha\subseteq Tm$ holds in ${\mathsf{Sub}}_{\mathcal{M}}(TX)$.

######  Remark 3.

Since ${\mathsf{Sub}}_{\mathcal{M}}(X)$ is a poset, the base
${\mathsf{base}}_{X}(\alpha)$ is determined uniquely, whenever it exists. The
base satisfies the _unit_ property

$\alpha\subseteq T{\mathsf{base}}_{X}(\alpha)$

for every $\alpha$ in ${\mathsf{Sub}}_{\mathcal{M}}(TX)$, and satisfies the
_counit_ property

${\mathsf{base}}_{X}(Tm)\subseteq m$

for every $m$ in ${\mathsf{Sub}}_{\mathcal{M}}(X)$. These properties are
immediate consequences of the definition of base.

We shall characterise functors admitting a base in Proposition 4. Before we
state the result, let us show that some functors do not admit a base.

Consider the category ${\mathsf{Pre}}$ equipped with the factorisation system
of Example 3.A (2), and the lowerset functor
${\mathbb{L}}:{\mathsf{Pos}}\longrightarrow{\mathsf{Pos}}$. We claim that

$\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
9.47626pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 1.0pt\raise
0.0pt\hbox{$\textstyle{\alpha:{\mathbb{1}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
7.97627pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\hbox{{}{\hbox{\kern 3.0pt\hbox{\ignorespaces\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}}}}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
25.0763pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
25.0763pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
1.0pt\raise
0.0pt\hbox{$\textstyle{{\mathbb{L}}\mathbb{Z}}$}}}}}}}\ignorespaces}}}}\ignorespaces,\quad*\mapsto\mathbb{Z},$

where $\mathbb{Z}$ is the poset of integers with the usual order, does not
admit a base.

Indeed, for any
$\textstyle{m:Z^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathbb{Z}}$,
the inequality $\alpha\subseteq{\mathbb{L}}m$ states that (the image of)
$Z^{\prime}$ is a cofinal subset of $\mathbb{Z}$. Had
$\textstyle{{\mathsf{base}}(\alpha):\widetilde{{\mathbb{1}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathbb{Z}}$
existed, its image would yield the least cofinal subset of $\mathbb{Z}$ — a
contradiction.

Recall that meet-preserving maps between complete lattices have left adjoints.
The proof of the following characterisation is a simple application of this
fact.

######  Proposition 4.

Suppose ${\mathscr{K}}$ has intersections of ${\mathcal{M}}$-subobjects. For
$T:{\mathscr{K}}\longrightarrow{\mathscr{K}}$, the following are equivalent:

  1. (1)

For every $X$ and every
$\textstyle{\alpha:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{TX}$,
the base
$\textstyle{{\mathsf{base}}_{X}(\alpha):\widetilde{Z}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}$
exists.

  2. (2)

$T$ preserves intersections of ${\mathcal{M}}$-subobjects.

Moreover, under any of the above conditions, ${\mathsf{base}}_{X}(\alpha)$ can
be computed as the intersection

$\bigcap_{\alpha\subseteq Tm}m$

of all ${\mathcal{M}}$-subobjects
$\textstyle{m:Z^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}$
such that $\alpha\subseteq Tm$ holds in ${\mathsf{Sub}}_{\mathcal{M}}(TX)$.

######  Proof 3.1.

Observe that the assignment $f\mapsto Tf$ induces a monotone map

$T_{X}:{\mathsf{Sub}}_{\mathcal{M}}(X)\longrightarrow{\mathsf{Sub}}_{\mathcal{M}}(TX)$

since $T$ is assumed to preserve ${\mathcal{M}}$-morphisms. The assignment
$\alpha\mapsto{\mathsf{base}}_{X}(\alpha)$ is then simply the value of a left
adjoint

${\mathsf{base}}_{X}:{\mathsf{Sub}}_{\mathcal{M}}(X)\longrightarrow{\mathsf{Sub}}_{\mathcal{M}}(TX)$

to $T_{X}$ at a point $\alpha$. Moreover, ${\mathsf{Sub}}_{\mathcal{M}}(X)$
and ${\mathsf{Sub}}_{\mathcal{M}}(TX)$ are complete lattices, since
${\mathscr{K}}$ is assumed to have intersections of
${\mathcal{M}}$-subobjects.

Then (1) is equivalent to (2), since (1) asserts that
${\mathsf{base}}_{X}\dashv T_{X}$ holds for any $X$ and (2) asserts that
$T_{X}$ preserves infima for any $X$.

The final assertion is true since the value of the left adjoint
${\mathsf{base}}_{X}$ can be computed by the formula

${\mathsf{base}}_{X}(\alpha)=\bigcap_{\alpha\subseteq Tm}m.$

In practical applications it may be the case that one is interested in the
existence of ${\mathsf{base}}_{X}(\alpha)$ only for particular $\alpha$’s. For
example, in [24] the base is computed only for finite subsets of $TX$ for
functors $T:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$.

We imitate this approach here. Namely, besides our standing assumptions, we
assume further that a full subcategory ${\mathscr{K}}_{\lambda}$ of
${\mathscr{K}}$ is given, where $\lambda$ is a regular cardinal. We want to
think of the objects of ${\mathscr{K}}_{\lambda}$ as being “smaller than
$\lambda$”. Our goal is to construct the value of a left adjoint
$\textstyle{{\mathsf{base}}_{X}(\alpha):\widetilde{Z}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}$
only for those ${\mathcal{M}}$-subobjects
$\textstyle{\alpha:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{TX}$
with $Z$ in ${\mathscr{K}}_{\lambda}$, and such that $\widetilde{Z}$ is in
${\mathscr{K}}_{\lambda}$ as well.

For every $X$, denote by

$I_{X}:{\mathsf{Sub}}_{{\mathcal{M}},\lambda}(X)\longrightarrow{\mathsf{Sub}}_{{\mathcal{M}}}(X)$

the inclusion of the subposet spanned by ${\mathcal{M}}$-subobjects having a
domain in ${\mathscr{K}}_{\lambda}$.

One can refine the existence of the base by applying the ideas of Freyd’s
Adjoint Functor Theorem [8]. In the formulation we use the terminology
$\lambda$-small to abbreviate “of cardinality less than $\lambda$”. For
example, a $\lambda$-small set is one of less than $\lambda$ elements, a
$\lambda$-small intersection is one indexed by a $\lambda$-small set, etc.

######  Proposition 5.

Suppose that for every $X$, the poset ${\mathsf{Sub}}_{\mathcal{M}}(X)$ has
$\lambda$-small infima, and suppose that
${\mathsf{Sub}}_{{\mathcal{M}},\lambda}(X)$ is a subset in
${\mathsf{Sub}}_{\mathcal{M}}(X)$ that is closed under $\lambda$-small infima.

Suppose further that the following two conditions are satisfied:

  1. (1)

$T$ preserves $\lambda$-small intersections.

  2. (2)

For any
$\textstyle{\alpha:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{TX}$
with $Z$ in ${\mathscr{K}}_{\lambda}$ there exists a $\lambda$-small set

$F=\\{f_{i}\mid i\in I,\;\alpha\subseteq
Tf_{i}\\}\subseteq{\mathsf{Sub}}_{{\mathcal{M}},\lambda}(X)$

such that for every $m$ in ${\mathsf{Sub}}_{{\mathcal{M}}}(X)$ with
$\alpha\subseteq Tm$ there exists $f\in F$ with $Tf\subseteq Tm$.

Then ${\mathsf{base}}_{X}(\alpha)$ exists for every
$\textstyle{\alpha:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{TX}$
with $Z$ in ${\mathscr{K}}_{\lambda}$, it is an element of
${\mathsf{Sub}}_{{\mathcal{M}},\lambda}(X)$, and it is computed by the formula

${\mathsf{base}}_{X}(\alpha)=\bigcap F.$

######  Proof 3.2.

By hypothesis, ${\mathsf{Sub}}_{{\mathcal{M}},\lambda}(X)$ has $\lambda$-small
infima, and the map $T_{X}$ preserves them by condition (1). Condition (2) now
ensures that

$\bigcap_{\alpha\subseteq Tm}m=\bigcap F$

holds. The latter infimum is $\lambda$-small and $T_{X}$ is assumed to
preserve such infima. The result now follows.

We show how Proposition 5 is applied in the classical case when
${\mathscr{K}}={\mathsf{Set}}$. Recall that a category ${\mathscr{D}}$ is
$\lambda$-filtered if every $\lambda$-small diagram in ${\mathscr{D}}$ has a
cocone in ${\mathscr{D}}$. A colimit is $\lambda$-filtered if its scheme is a
$\lambda$-filtered category.

Let ${\mathscr{K}}$ be the category ${\mathsf{Set}}$ of all sets and mappings
with the factorisation system of surjections and injections. Let
$T:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$ be a finitary functor that
preserves injections and finite intersections. Then, for every
$\textstyle{\alpha:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{TX}$
with the set $Z$ finite,
$\textstyle{{\mathsf{base}}_{X}(\alpha):\widetilde{Z}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}$
exists and the set $\widetilde{Z}$ is finite.

It suffices to verify conditions (1) and (2) of Proposition 5 (where
$\lambda=\aleph_{0}$ and ${\mathsf{Set}}_{\aleph_{0}}$ are the finite sets).
Condition (1) is well-known to hold for ${\mathsf{Set}}$. Condition (2) is
verified as follows. Given
$\textstyle{\alpha:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{TX}$
with $Z$ a finite set, express $X$ as a filtered colimit
$\mathop{{\mathrm{colim}}}\nolimits_{i\in I}X_{i}$ of subobjects
$\textstyle{m_{i}:X_{i}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}$
with all $X_{i}$ finite. Since $T$ is finitary and is assumed to preserve
injections, $TX$ is a filtered colimit
$\mathop{{\mathrm{colim}}}\nolimits_{i\in I}TX_{i}$ of injections. Since $Z$
is finite, there exists $i_{0}$ such that the triangle

$\textstyle{Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\alpha}$$\textstyle{TX}$$\textstyle{TX_{i_{0}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Tm_{i_{0}}}$

commutes. Denote by $F$ the set

$\\{f\mid f\subseteq m_{i_{0}}\mbox{ and }\alpha\subseteq Tf\\}$

of elements of ${\mathsf{Sub}}_{\mathcal{M}}(X)$.

Observe first that $F$ is nonempty and finite. Secondly, if $\alpha\subseteq
Tm$, then

$\alpha\subseteq Tm_{i_{0}}\cap Tm=T(m_{i_{0}}\cap m)$

since $T$ preserves finite intersections. Since the subobject $m_{i_{0}}\cap
m$ is in $F$, condition (2) has been verified.

More generally, Proposition 5 and the technique of Example 3.B can be applied
to the case when ${\mathscr{K}}$ is a locally $\lambda$-bounded category for
some regular cardinal $\lambda$ and a proper factorisation system
$({\mathcal{E}},{\mathcal{M}})$, see [13]. In particular, we will use the
results for ${\mathscr{K}}={\mathsf{Pos}}$ equipped with the factorisation
system of monotone surjections and order-embeddings, see Example 3.B.

A category ${\mathscr{K}}$ is locally $\lambda$-bounded w.r.t. a proper
factorisation system $({\mathcal{E}},{\mathcal{M}})$, if the following two
conditions hold:

  1. (1)

There is an essentially small full subcategory ${\mathscr{K}}_{\lambda}$ of
${\mathscr{K}}$ such that:

    1. (a)

Every object $Z$ in ${\mathscr{K}}_{\lambda}$ is $\lambda$-bounded, i.e., the
functor ${\mathscr{K}}(Z,{-})$ preserves colimits of $\lambda$-filtered
diagrams of ${\mathcal{M}}$-subobjects.

    2. (b)

A morphism
$\textstyle{m:X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{Y}$
is an isomorphism iff the map
${\mathscr{K}}(Z,m):{\mathscr{K}}(Z,X)\longrightarrow{\mathscr{K}}(Z,Y)$ is a
bijection for every $\lambda$-bounded $Z$. (I.e., ${\mathscr{K}}_{\lambda}$ is
an _$({\mathcal{M}},{\mathcal{E}})$ -generator_ of ${\mathscr{K}}$.)

  2. (2)

The category ${\mathscr{K}}$ is cocomplete and has all
${\mathcal{E}}$-cointersections. This means that the opposite category
${\mathscr{K}}^{\mathit{op}}$ (that is equipped with
$({\mathcal{M}},{\mathcal{E}})$ as a factorisation system) has all
intersections of ${\mathcal{E}}$-subobjects.

A category ${\mathscr{K}}$ is called $\lambda$-ranked, if it is locally
$\lambda$-bounded and ${\mathcal{E}}$-cowellpowered.

Examples of locally $\lambda$-bounded categories w.r.t. a factorisation system
$({\mathcal{E}},{\mathcal{M}})$ include the following:

  1. (1)

All locally $\lambda$-presentable categories when we take ${\mathcal{E}}$ to
be strong epimorphisms and ${\mathcal{M}}$ to be monomorphisms, see [13].

In particular, the categories ${\mathsf{Pos}}$ and ${\mathsf{Pre}}$ are
locally $\aleph_{0}$-bounded, if we take ${\mathcal{M}}$ to consist of all
monotone injections (not necessarily reflecting order). A preorder or a poset
$X$ is $\aleph_{0}$-bounded iff it is finite.

  2. (2)

The category ${\mathsf{Pos}}$ of posets and monotone maps is locally
$\aleph_{0}$-bounded for ${\mathcal{E}}$ consisting of surjective monotone
maps and ${\mathcal{M}}$ of monotone maps reflecting the order. A poset is
$\aleph_{0}$-bounded iff it is finite.

  3. (3)

The category ${\mathsf{Pre}}$ of preorders and monotone maps can be equipped
with a variety of factorisation systems, see Example 3.A. The category
${\mathsf{Pre}}$ is locally $\aleph_{0}$-bounded w.r.r. the factorisation
system where ${\mathcal{E}}$ consists of all monotone surjections and
${\mathcal{M}}$ consists of all monotone injections that reflect the order,
see Theorem 5.6 of [14]. A preorder $X$ is $\aleph_{0}$-bounded iff it is
finite.

Let ${\mathscr{K}}$ be a $\lambda$-bounded category w.r.t. a factorisation
system $({\mathcal{E}},{\mathcal{M}})$. We say that
$T:{\mathscr{K}}\longrightarrow{\mathscr{K}}$ admits $\lambda$-bounded bases,
provided that
$\textstyle{{\mathsf{base}}^{T}_{X}:\widetilde{Z}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}$
exists for any
$\textstyle{\alpha:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{TX}$
with $Z$ in ${\mathscr{K}}_{\lambda}$ and, moreover, $\widetilde{Z}$ is in
${\mathscr{K}}_{\lambda}$.

######  Proposition 6.

Suppose that ${\mathscr{K}}$ is locally $\lambda$-bounded w.r.t. a
factorisation system $({\mathcal{E}},{\mathcal{M}})$. Then
$T:{\mathscr{K}}\longrightarrow{\mathscr{K}}$ admits $\lambda$-bounded bases,
whenever the following four conditions are satisfied:

  1. (1)

Every subposet ${\mathsf{Sub}}_{{\mathcal{M}},\lambda}(X)$ in
${\mathsf{Sub}}_{\mathcal{M}}(X)$ is closed under $\lambda$-small infima.

  2. (2)

The principal lowersets in every poset
${\mathsf{Sub}}_{{\mathcal{M}},\lambda}(X)$ are $\lambda$-small.

  3. (3)

$T$ preserves colimits of $\lambda$-filtered diagrams of
${\mathcal{M}}$-subobjects.

  4. (4)

$T$ preserves $\lambda$-small intersections of ${\mathcal{M}}$-subobjects.

######  Proof 3.3.

It is proved in [14] that every locally $\lambda$-bounded category is
necessarily complete. Hence every ${\mathsf{Sub}}_{\mathcal{M}}(X)$ is a
complete lattice. Every object $X$ of ${\mathscr{K}}$ can be represented as a
filtered colimit of its $\lambda$-subobjects; consider the canonical filtered
diagram $D:{\mathscr{D}}\longrightarrow{\mathscr{K}}$ of $X$ and its colimit
$Y$, which yields a unique comparison $Y\longrightarrow X$ that is an
isomorphism since ${\mathscr{K}}_{\lambda}$ is an
$({\mathcal{M}},{\mathcal{E}})$-generator. Using the argument of Example 3.B
yields the result.

###  3.C. Bases in posets

We will apply the general theory of Subsection 3.B to the particular case of
the category ${\mathsf{Pos}}$. In more detail, we consider ${\mathsf{Pos}}$ as
an $({\mathcal{E}},{\mathcal{M}})$-category for ${\mathcal{E}}$ = monotone
surjections and ${\mathcal{M}}$ = order-embeddings. Then the following
conditions hold:

  1. (1)

$({\mathcal{E}},{\mathcal{M}})$ is a proper factorisation system, see Example
3.A.

  2. (2)

${\mathsf{Pos}}$ is ${\mathcal{M}}$-wellpowered.

  3. (3)

${\mathsf{Pos}}$ is locally $\aleph_{0}$-bounded, see Example 3.B. The
category ${\mathsf{Pos}}_{\aleph_{0}}$ consists of finite posets.

Hence, by Proposition 6, a functor
$T:{\mathsf{Pos}}\longrightarrow{\mathsf{Pos}}$ admits $\aleph_{0}$-bounded
(=finite) bases, whenever $T$ preserves order-embeddings and their finite
intersections.

From now on, all bases will be considered finite.

Not all locally monotone endofunctors
$T:{\mathsf{Pos}}\longrightarrow{\mathsf{Pos}}$ preserve order-embeddings. See
e.g. Example 6.1 of [6].

Moreover, a locally monotone endofunctor of ${\mathsf{Pos}}$ that preserves
order-embeddings does not necessarily preserve finite intersections. Suppose
$T:{\mathsf{Pos}}\longrightarrow{\mathsf{Pos}}$ assigns the two-element chain
${\mathbb{2}}$ to every nonempty poset and it assigns the one-element poset
${\mathbb{1}}$ to the empty poset. On morphisms $T$ sends the unique morphism
$!_{X}:\emptyset\longrightarrow X$ to $\ulcorner
1\urcorner:{\mathbb{1}}\longrightarrow{\mathbb{2}}$, all other morphisms are
mapped to the identity morphism. The intersection

$\textstyle{\emptyset\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{!_{\mathbb{1}}}$$\scriptstyle{!_{\mathbb{1}}}$$\textstyle{{\mathbb{1}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\ulcorner
1\urcorner}$$\textstyle{{\mathbb{1}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\ulcorner
0\urcorner}$$\textstyle{\mathbb{2}}$

is clearly not preserved by $T$.

We list examples of endofunctors of the category ${\mathsf{Pos}}$ that admit
finite bases. We start with the preservation of order-embeddings.

All Kripke-polynomial endofunctors (2.1) of the category ${\mathsf{Pos}}$
preserve order-embeddings. This is essentially proved in [6], Examples 5.3 and
6.3, for the case of Kripke polynomial endofunctors of ${\mathsf{Pre}}$. One
only needs to notice that order-embeddings in ${\mathsf{Pos}}$ are precisely
the order-reflecting monotone injective maps of the underlying preorders.

In fact, the class of endofunctors of ${\mathsf{Pos}}$ that preserve order-
embeddings is quite large. It includes all functors that preserve certain lax
diagrams called _exact squares_ , see [9] or [5].

A lax square

$\textstyle{P\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p_{1}}$$\scriptstyle{p_{0}}$$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\scriptstyle{\nearrow}$$\textstyle{C}$

in ${\mathsf{Pos}}$ is called exact, if $fa\leq_{C}gb$ entails the existence
of $w$ in $P$ such that both $a\leq_{A}p_{0}w$ and $p_{1}w\leq_{B}b$ hold.

A functor $T$ which preserves exact squares will be also called a functor
satisfying the Beck-Chevalley Condition, or BCC for short.

All endofunctors of ${\mathsf{Pos}}$ satisfying BCC preserve order-embeddings.
In particular, all Kripke-polynomial endofunctors of ${\mathsf{Pos}}$ satisfy
BCC. See [5].

The following series of results deals with preservation of finite
intersections. As the next example shows, not all Kripke polynomial functors
preserve finite intersections.

The lowerset functor ${\mathbb{L}}$ does not preserve intersections of order-
embeddings. Consider the poset ${\mathbb{Z}}$ of integers and its subposets
$\textstyle{m:E\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathbb{Z}}$
and
$\textstyle{n:O\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathbb{Z}}$
of even and odd integers, respectively. The intersection of $m$ and $n$ is
_empty_ , as it is shown in the diagram on the left below:

$\textstyle{\emptyset\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{O\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{n}$$\textstyle{E\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m}$$\textstyle{\mathbb{Z}}$
$\textstyle{{\mathbb{L}}\emptyset\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\mathbb{L}}O\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{\mathbb{L}}n}$$\textstyle{{\mathbb{L}}E\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{\mathbb{L}}m}$$\textstyle{{\mathbb{L}}{\mathbb{Z}}}$

Then the one-element poset ${\mathbb{L}}\emptyset$ in the diagram on the right
above is not the intersection of ${\mathbb{L}}m$ and ${\mathbb{L}}n$. Namely,
the intersection of ${\mathbb{L}}m$ and ${\mathbb{L}}n$ contains at least two
elements, since ${\mathbb{L}}m(\emptyset)=\emptyset={\mathbb{L}}n(\emptyset)$
and ${\mathbb{L}}m(E)={\mathbb{Z}}={\mathbb{L}}n(O)$.

The functor ${\mathbb{L}}$ does not, in general, preserve _non-empty_
intersections of order-embeddings as well. Consider again the above example,
and take as $m:E\longrightarrow{\mathbb{Z}}$ the poset of even integers and
$n:O\longrightarrow{\mathbb{Z}}$ of odd integers and zero. Then $m\cap n$ is
the one-element set $\\{0\\}$ and ${\mathbb{L}}\\{0\\}$ has two elements,
while ${\mathbb{L}}m\cap{\mathbb{L}}n$ contains $\emptyset$, ${\downarrow}0$,
and ${\mathbb{Z}}$.

######  Proposition 7.

All finitary Kripke-polynomial endofunctors of ${\mathsf{Pos}}$ preserve
finite intersections of order-embeddings.

######  Proof 3.4.

The proof is trivial for all the formation steps (2.1) except for $T^{E}$ and
${\mathbb{L}}_{\omega}T$. For the induction hypothesis, suppose $T$ preserves
finite intersections of order-embeddings.

  1. (1)

Since $T^{E}X=(TX)^{E}$, it suffices to observe that the diagram

$\textstyle{(TL)^{E}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{(Ti)^{E}}$$\scriptstyle{(Tj)^{E}}$$\textstyle{(TB)^{E}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{(Tn)^{E}}$$\textstyle{(TA)^{E}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{(Tm)^{E}}$$\textstyle{(TX)^{E}}$

is a pullback whenever the following diagram is:

$\textstyle{TL\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Ti}$$\scriptstyle{Tj}$$\textstyle{TB\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Tn}$$\textstyle{TA\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Tm}$$\textstyle{TX.}$

This is true because the functor
$(-)^{E}:{\mathsf{Pos}}\longrightarrow{\mathsf{Pos}}$ preserves all limits: it
is a right adjoint by cartesian closedness of ${\mathsf{Pos}}$.

  2. (2)

It suffices to prove that ${\mathbb{L}}_{\omega}$ preserves finite
intersections of order-embeddings.

$\textstyle{L\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{n}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m}$$\textstyle{X}$
$\textstyle{{\mathbb{L}}_{\omega}L\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\mathbb{L}}_{\omega}B\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{\mathbb{L}}_{\omega}n}$$\textstyle{{\mathbb{L}}_{\omega}A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{\mathbb{L}}_{\omega}m}$$\textstyle{{\mathbb{L}}_{\omega}X}$
$\textstyle{\lambda\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\beta\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{\mathbb{L}}_{\omega}n}$$\textstyle{\alpha\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{\mathbb{L}}_{\omega}m}$$\textstyle{\chi}$

Given an intersection in the diagram on the left above, we show that the
diagram in the center above is again an intersection of the morphisms
${\mathbb{L}}_{\omega}m$ and ${\mathbb{L}}_{\omega}n$. For any two lowersets
$\alpha$ in ${\mathbb{L}}_{\omega}A$ and $\beta$ in ${\mathbb{L}}_{\omega}B$
satisfying ${\mathbb{L}}_{\omega}m(\alpha)=\chi={\mathbb{L}}_{\omega}n(\beta)$
it is enough to find a lowerset $\lambda$ in ${\mathbb{L}}_{\omega}L$ as shown
in the diagram above on the right. All of the depicted lowersets are
determined by their minimal sets of generators. Recall that the minimal set of
generators of the lowerset $\alpha$ is denoted by $g(\alpha)$. Since $m$ and
$n$ are inclusions, we see that $g(\alpha)=g(\chi)=g(\beta)$. The equality of
sets of generators implies that $g(\chi)\subseteq L$. Defining $\lambda$ in
${\mathbb{L}}_{\omega}L$ to be the lowerset generated by $g(\chi)$ yields the
unique witness in ${\mathbb{L}}_{\omega}L$.

Observe that the preceding argument works even in the case of $g(\chi)$ being
empty.

By the above, all finitary Kripke-polynomial functors $T$ admit finite bases.

We will show how the bases for Kripke-polynomial functors can be computed.

  1. (1)

Constant functor $E$: For an arbitrary subobject
$\textstyle{\alpha:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{E}$,
we have that its base is of the form
$\textstyle{{\mathsf{base}}(\alpha):\emptyset\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}$,
with ${\mathsf{base}}(\alpha)$ being the empty mapping.

  2. (2)

Identity functor ${\mathit{Id}}:$ Given a subobject
$\textstyle{\alpha:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}$,
its base
$\textstyle{{\mathsf{base}}(\alpha):\widetilde{Z}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}$
is the mapping $\alpha$ itself.

  3. (3)

Sum and product of functors: Fix two functors $T_{1}$ and $T_{2}$. Given a
subobject
$\textstyle{\alpha:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{T_{1}X+T_{2}X}$,
it is equally well a subobject
$\textstyle{\alpha_{1}+\alpha_{2}:Z_{1}+Z_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{T_{1}X+T_{2}X}$
for some choice of posets $Z_{1}$ and $Z_{2}$. Then
${\mathsf{base}}(\alpha)={\mathsf{base}}(\alpha_{1})\cup{\mathsf{base}}(\alpha_{2})$.
For the case of the product of functors, given a subobject
$\textstyle{\alpha:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{T_{1}X\times
T_{2}X}$, denote by $p_{i}:T_{1}X\times T_{2}X\longrightarrow T_{i}X$ the
$i$-th projection from the product ($i\in\\{1,2\\}$). Then
${\mathsf{base}}(\alpha)={\mathsf{base}}(p_{1}\cdot\alpha)\cup{\mathsf{base}}(p_{2}\cdot\alpha)$.

  4. (4)

Power of a functor: Given a functor $T^{E}$ and a subobject
$\textstyle{\alpha:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{(TX)^{E}}$,
we denote by $p_{e}:TX^{E}\longrightarrow TX$ the obvious projection (with
$e\in E$). Then ${\mathsf{base}}(\alpha)=\bigcup_{e\in
E}{\mathsf{base}}(p_{e}\cdot\alpha)$.

  5. (5)

The dual of a functor: A straightforward computation yields that the base of
$\textstyle{\alpha:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{T^{\partial}X}$
is $({\mathsf{base}}(\alpha^{\mathit{op}}))^{\mathit{op}}$.

  6. (6)

The lowerset functor: Given a lowerset
$\textstyle{\alpha:{\mathbb{1}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\mathbb{L}}_{\omega}X}$,
the base
$\textstyle{{\mathsf{base}}(\alpha):\widetilde{{\mathbb{1}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}$
is the (discrete) finite poset of generators of $\alpha$. More generally, the
base of
$\textstyle{\alpha:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\mathbb{L}}_{\omega}X}$
is $\bigcup_{z\in Z}{\mathsf{base}}(\alpha\cdot z)$.

##  4\. Monotone relations and their lifting

In the current section, we summarise the notation and the necessary facts that
concern monotone relations between posets. We will use these facts and the
facts about liftings of monotone relations in Section 5 to introduce the
semantics of a coalgebraic logic over posets. For a more detailed treatment of
the theory of relation liftings in the categories ${\mathsf{Pre}}$ and
${\mathsf{Pos}}$ we refer to [5].

The category ${\mathsf{Rel}}$ of monotone relations over ${\mathsf{Pos}}$ has
the same objects as the category ${\mathsf{Pos}}$, and has _monotone
relations_ as arrows. A monotone relation $R$ from $X$ to $Y$ will be denoted
by
$\textstyle{R:X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{Y}$
and it will be identified with a monotone map $R:Y^{\mathit{op}}\times
X\longrightarrow{\mathbb{2}}$. We shall often write $R(y,x)$ or
$y\mathrel{R}x$ to denote that $R$ relates $x$ to $y$. Using this notation, a
relation $R$ is monotone if it satisfies the following monotonicity condition:

$R(y,x)\mbox{ and }y^{\prime}\leq_{Y}y\mbox{ and }x\leq_{X}x^{\prime}\mbox{
implies }R(y^{\prime},x^{\prime}).$

The composition in ${\mathsf{Rel}}$ is computed in the usual manner: $(S\cdot
R)(z,x)$ holds if and only if $S(z,y)$ and $R(y,x)$ hold for some $y$. The
identity morphism on a poset $X$ is the order $\leq_{X}$ of $X$, considered as
the monotone map ${\leq_{X}}:X^{\mathit{op}}\times
X\longrightarrow{\mathbb{2}}$. For any two posets $X$ and $Y$, the hom-set
${\mathsf{Rel}}(X,Y)$ of all monotone relations from $X$ to $Y$ carries a
poset structure given by the inclusion of relations.

We shall often use two special kinds of relations: graph relations and
membership relations.

  1. (1)

Graph relations. For a monotone map $f:X\longrightarrow Y$ we define two graph
relations

$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f_{\diamond}}$$\textstyle{Y}$$\textstyle{Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f^{\diamond}}$$\textstyle{X}$

by putting

$f_{\diamond}(y,x)\textrm{ iff }y\leq fx,\quad f^{\diamond}(x,y)\textrm{ iff
}fx\leq y.$

The assignment

$f\mapsto f_{\diamond}$

can be extended to a locally monotone functor

$({-})_{\diamond}:{\mathsf{Pos}}\longrightarrow{\mathsf{Rel}}.$

  2. (2)

Membership relations. For a poset $X$, we use the following two membership
relations:

$\textstyle{\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}_{X}:{\mathbb{L}}X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}$$\textstyle{\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}_{X}:X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\mathbb{U}}X}$

defined by
$\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}_{X}(x,l)=1$
iff $x$ is in $l$ and
$\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}_{X}(u,x)=1$
iff $x$ is in $u$.

As in the case of ordinary relations, there are various operations that we can
perform on monotone relations.

[Operations on relations] Suppose
$\textstyle{R:X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{Y}$
is a monotone relation.

  1. (1)

The converse
$\textstyle{R^{{\mathit{con}}}:Y^{\mathit{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X^{\mathit{op}}}$
of $S$ is defined by putting $R^{\mathit{con}}(x,y)$ iff $R(y,x)$.

  2. (2)

The negation $\textstyle{\neg
R:X^{\mathit{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{Y^{\mathit{op}}}$
is defined by putting $\neg R(y,x)$ iff not $R(y,x)$.

  3. (3)

Given monotone maps $f:A\longrightarrow X$, $g:B\longrightarrow Y$, the
composite

$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f_{\diamond}}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{R}$$\textstyle{Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g^{\diamond}}$$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{R(g-,f-)}$

is called a restriction of $R$ along $f$ and $g$.

######  Remark 8.

Observe that
$\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}_{X}$ is
the converse of
$\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}_{X^{\mathit{op}}}$.
We omit the subscript $X$ whenever it is clear from the context. We also often
use the notation

$\textstyle{\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}_{X}:({\mathbb{L}}X)^{\mathit{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X^{\mathit{op}}}$$\textstyle{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}_{X}:X^{\mathit{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{({\mathbb{U}}X)^{\mathit{op}}}$

instead of the notation
$\neg{\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}}$
and
$\neg{\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}}$
for the negation of the respective membership relations. Whenever it is
possible, we use the infix notation for the membership relations.

Any locally monotone functor $T:{\mathsf{Pos}}\longrightarrow{\mathsf{Pos}}$
that satisfies BCC (see Definition 3.C) can be lifted to a locally monotone
functor $\overline{T}:{\mathsf{Rel}}\longrightarrow{\mathsf{Rel}}$. In fact,
BCC is equivalent to the existence of such a lifting. The following theorem
was proved in [5] for the category ${\mathsf{Pre}}$, but the proof goes
through verbatim for the case of ${\mathsf{Pos}}$.

######  Theorem 9 ([5]).

For a locally monotone functor $T:{\mathsf{Pos}}\longrightarrow{\mathsf{Pos}}$
the following are equivalent:

  1. (1)

The functor $T$ has a locally monotone functorial relation lifting
$\overline{T}$, i.e., there is a 2-functor
$\overline{T}:{\mathsf{Rel}}\longrightarrow{\mathsf{Rel}}$ such that the
square

$\textstyle{{\mathsf{Rel}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{T}}$$\textstyle{\mathsf{Rel}}$$\textstyle{{\mathsf{Pos}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{T}$$\scriptstyle{({-})_{\diamond}}$$\textstyle{{\mathsf{Pos}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{({-})_{\diamond}}$
(4.2)

commutes.

  2. (2)

The functor $T$ satisfies the Beck-Chevalley Condition. (i.e., it preserves
exact squares).

A relation lifting $\overline{T}$ of a locally a locally monotone functor $T$
satisfying the BCC is computed in the following way. A relation
$\textstyle{R:X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{Y}$
can be represented by a certain span

$\textstyle{Y}$$\textstyle{E\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p_{1}}$$\scriptstyle{p_{0}}$$\textstyle{X,}$

of monotone maps such that the equality
$R=(p_{1})_{\diamond}\cdot(p_{0})^{\diamond}$ holds (see [5] or [6] for
details). Then the lifting $\overline{T}$ is computed by the following
composition of graph relations:

$\textstyle{\overline{T}R:TX\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{(Tp_{1})^{\diamond}}$$\textstyle{TE\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{(Tp_{0})_{\diamond}}$$\textstyle{TY}$

In elementary terms, we can check if the elements $\alpha\in TX$ and $\beta\in
TY$ are related by the lifted relation $\overline{T}R$ as follows:

$\overline{T}R(\beta,\alpha)\ \mbox{ iff }\ (\exists w\in
TR)(\beta\leq_{TY}Tp_{0}(w)\mbox{ and }Tp_{1}(w)\leq_{TX}\alpha).$ (4.3)

Relation lifting behaves well with respect to graph relations, converse
relations and restrictions of relations. The easy proofs of these properties
follow immediately from the formula (4.3). We also give explicit explicit
instances of relation liftings for Kripke-polynomial functors.

Suppose $T:{\mathsf{Pos}}\longrightarrow{\mathsf{Pos}}$ is a locally monotone
functor satisfying BCC, and
$\textstyle{R:X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{Y}$
is a given relation.

  1. (1)

The relation lifting commutes with graph relations, i.e., the equalities
$\overline{T}f_{\diamond}=(Tf)_{\diamond}$ and
$\overline{T}f^{\diamond}=(Tf)^{\diamond}$ hold.

  2. (2)

Relation lifting commutes with converses, i.e., the equality
$\overline{T}R^{\mathit{con}}=(\overline{T^{\partial}}R)^{\mathit{con}}$ (or,
equivalently,
$\overline{T^{\partial}}R=(\overline{T}R^{\mathit{con}})^{\mathit{con}}$)
holds for every monotone relation $R$.

  3. (3)

Relation lifting commutes with taking restrictions. Given a restriction

$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f_{\diamond}}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{R}$$\textstyle{Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g^{\diamond}}$$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{R(g-,f-)}$

of
$\textstyle{R:X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{Y}$
along $f:A\longrightarrow X$ and $g:B\longrightarrow Y$, we can apply
$\overline{T}$ to obtain

$\textstyle{TA\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{(Tf)_{\diamond}}$$\textstyle{TX\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{T}R}$$\textstyle{TY\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{(Tg)^{\diamond}}$$\textstyle{TB\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{T}R(Tg-,Tf-)}$

since $\overline{T}$ commutes with taking the graphs by (1) above.

  4. (4)

Relation lifting for Kripke-polynomial functors can be computed inductively:

$\displaystyle\overline{const_{X}}R\ $ $\displaystyle={\leq_{X}},$
$\displaystyle\overline{T_{0}\times
T_{1}}R((\alpha_{0},\alpha_{1})(\beta_{0},\beta_{1}))$ $\displaystyle\mbox{
iff }\overline{T_{0}}R(\alpha_{0},\beta_{0})\mbox{ and
}\overline{T_{1}}R(\alpha_{1},\beta_{1}),$
$\displaystyle\overline{T_{0}+T_{1}}R(\alpha,\beta)=1$ $\displaystyle\mbox{
iff }\begin{cases}\alpha\in T_{0}Y,\;\beta\in T_{0}X,\text{ and
}\overline{T_{0}}R(\alpha,\beta),\\\ \alpha\in T_{1}Y,\;\beta\in T_{1}X,\text{
and }\overline{T_{1}}R(\alpha,\beta).\end{cases}$
$\displaystyle\overline{{\mathbb{L}}}R(o,l)$ $\displaystyle\mbox{ iff
}(\forall
y)(y\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}o\mbox{
implies }(\exists
x)(x\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}l\mbox{
and }R(y,x))),$ $\displaystyle\overline{{\mathbb{U}}}R(v,u)$
$\displaystyle\mbox{ iff }(\forall
x)(u\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}x\mbox{
implies }(\exists
y)(v\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}y\mbox{
and }R(y,x))).$

The above calculus of relation liftings allows us to explicitly describe the
relation liftings for functors introduced in Section 2.

Recall the various ordered coalgebraic structures from Example 2.B.

  1. (1)

The lifting of the functor $T=A\times{\mathit{Id}}$ is particularly easy.
Given a relation
$\textstyle{R:X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{Y}$,
let us denote the lifted relation

$\textstyle{\overline{(A\times{\mathit{Id}})}R:A\times
X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{A\times
Y}$

by $\overline{R}$. Then the relation $\overline{R}((b,y),(a,x))$ holds if and
only if $b\leq a$ and $R(y,x)$ holds.

  2. (2)

The coalgebras for the functor $T={\mathit{Id}}^{A}\times{\mathbb{2}}$ model
deterministic ordered automata. Given a monotone relation
$\textstyle{R:X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{Y}$
the elements $\alpha=(f,i)\in X^{A}\times{\mathbb{2}}$ and $\beta=(g,j)\in
Y^{A}\times{\mathbb{2}}$ are related by the lifted relation
$\textstyle{\overline{T}R:TX\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{TY}$
if and only if $j\leq i$ and $R(g(a),f(a))$ for every $a\in A$.

  3. (3)

Given the functor $T=({\mathbb{L}}_{\omega})^{A}\times{\mathbb{2}}$ (with $A$
discrete) for lowerset automata and a relation
$\textstyle{R:X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{Y}$,
its lifted relation
$\textstyle{\overline{T}R:TX\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{TY}$
is defined as follows: For an element $\alpha=(l,i)$ in
$({\mathbb{L}}_{\omega}X)^{A}\times{\mathbb{2}}$ and $\beta=(o,j)$ in
$({\mathbb{L}}_{\omega}Y)^{A}\times{\mathbb{2}}$ we have that
$\overline{T}R(\beta,\alpha)$ holds if and only if

$j\leq i\mbox{ and }(\forall a\in
A)\mathrel{\overline{{\mathbb{L}}_{\omega}}R}(o(a),l(a))$

holds, with the latter condition meaning that for every $y$ such that
$y\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}o(a)$
there is an element $x$ with
$x\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}l(a)$
such that $R(y,x)$ holds. Due to the monotonicity of the relation $R$, the
condition can be weakened further using the sets of minimal generators of the
lowersets $l$ and $o$. For every $y\in g(o(a))$ there has to be some $x\in
g(l(a))$ such that $R(y,x)$ holds. The computation of the lifting stays the
same even for an ordered set $A$ of “inputs”.

##  5\. Moss’ logic for ordered coalgebras

In this section we introduce a logic for ordered coalgebras parametric in the
coalgebra functor $T$. The syntax of the logic will be finitary, the
propositional part will be given by the conjunction and disjunction
connectives, and the modal part will consist of a single modality $\nabla$ of
arity $T^{\partial}$. The semantics of the logic will be given by monotone
valuations over $T$-coalgebras, with the semantics of the modality $\nabla$
given by relation lifting. We will show that this logic has the Hennessy-
Milner property.

From this section on, we fix a finitary locally monotone functor
$T:{\mathsf{Pos}}\longrightarrow{\mathsf{Pos}}$ and assume it preserves exact
squares and finite intersections.

It is easy to see that if $T$ satisfies the above assumptions, so does its
dual $T^{\partial}$.

###  5.A. The syntax of the coalgebraic language

The syntax of Moss’ logic for ordered coalgebras will be based on finitary
conjunction and disjunction, and a single finitary modality. It will be
convenient to regard the arities of both the connectives and the modality as
finitary functors. A similar approach has been already used in [16] for the
Moss’ logic in sets. When passing from sets to posets one has to be more
careful about the precise shape of the arities. Namely:

  1. (1)

In ${\mathsf{Set}}$, the arity of the finitary conjunction and disjunction is
given by the finitary powerset functor
$P_{\omega}:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$. This means that,
e.g., the conjunction is a map
$\bigwedge:P_{\omega}{\mathcal{L}}\longrightarrow{\mathcal{L}}$ where
${\mathcal{L}}$ denotes the set of all formulas. In ${\mathsf{Pos}}$, the
natural choice for the arity of the conjunction is ${\mathbb{U}}_{\omega}$,
whereas for the disjunction it is ${\mathbb{L}}_{\omega}$.

  2. (2)

In ${\mathsf{Set}}$, the cover modality $\nabla$ has the coalgebraic functor
$T$ as its arity. In ${\mathsf{Pos}}$, one needs to use the dual
$T^{\partial}$ of $T$ for type-checking reasons, as will become clear in
Subsection 5.B below.

Therefore the formulas of the coalgebraic language should have the following
intuitive description in BNF:

$a::=p\mid\bigwedge\varphi\mid\bigvee\psi\mid\nabla\alpha$ (5.4)

where $p$ is an atom, $\varphi={\uparrow}\\{a_{1},\dots,a_{k}\\}$ is a
finitely generated upperset of formulas,
$\psi={\downarrow}\\{a_{1},\dots,a_{k}\\}$ is a finitely generated lowerset of
formulas, and $\alpha$ is a “$T^{\partial}$-tuple” of formulas. There is a
slight technicality however: since we work in posets we expect to obtain a
poset of formulas. The precise definition of formulas is achieved by the free
algebra construction in the category ${\mathsf{Pos}}$.

[Formulas] Fix a poset ${\mathsf{At}}$ of propositional atoms. The language
${\mathcal{L}}$ is given as an algebra for
${\mathbb{U}}_{\omega}+{\mathbb{L}}_{\omega}+T^{\partial}$, free on
${\mathsf{At}}$. The components of the algebraic structure
$a:{\mathbb{U}}_{\omega}{\mathcal{L}}+{\mathbb{L}}_{\omega}{\mathcal{L}}+T^{\partial}{\mathcal{L}}\longrightarrow{\mathcal{L}}$
will be denoted by

$\bigwedge:{\mathbb{U}}_{\omega}{\mathcal{L}}\longrightarrow{\mathcal{L}},\quad\bigvee:{\mathbb{L}}_{\omega}{\mathcal{L}}\longrightarrow{\mathcal{L}},\quad\nabla_{T^{\partial}}:T^{\partial}{\mathcal{L}}\longrightarrow{\mathcal{L}}$

######  Remark 10.

  1. (1)

The language ${\mathcal{L}}$ is a poset by its construction. Moreover, an
algebra for $F={\mathbb{U}}_{\omega}+{\mathbb{L}}_{\omega}+T^{\partial}$ free
on ${\mathsf{At}}$ can be defined by a colimit of a transfinite chain

$w_{i,i+1}:W_{i}\longrightarrow W_{i+1}$

where $W_{0}={\mathsf{At}}$, $W_{i+1}=F(W_{i})+{\mathsf{At}}$ and the
connecting morphisms are defined in the obvious way:
$w_{0,1}:{\mathsf{At}}\longrightarrow F({\mathsf{At}})+{\mathsf{At}}$ is the
coproduct injection and $w_{i+1,i+2}=F(w_{i,i+1})+{\mathsf{At}}$.

The above chain $w_{i,i+1}$ has ${\mathcal{L}}$ as its colimit; we denote the
colimit injections by $w_{i}:W_{i}\longrightarrow{\mathcal{L}}$.

  2. (2)

The transfinite construction of ${\mathcal{L}}$ also shows that the “intuitive
BNF” of (5.4) works. More in detail, one can show that each formula $a$ in
${\mathcal{L}}$ has a unique finite depth.

Indeed, for every
$\textstyle{a:{\mathbb{1}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{L}}$
there is a least $i$ such that $a\in w_{i}$. There are two cases for a fixed
$a$ in ${\mathcal{L}}$:

    1. (a)

$i=0$ means that $a$ is an atom.

    2. (b)

$i$ is positive, i.e., $i=k+1$. Then $a\in w_{k+1}$ holds. The formula $a$ is
not an atom by the definition of $i$; hence $a$ is either a conjunction, a
disjunction or a nabla of an object in $W_{k}$.

The finite poset of direct subformulas of $a$ can be obtained as the subobject
${\mathsf{base}}^{F}_{F(W_{k})}(w_{k+1}(a))$.

  3. (3)

We defined the arity of a conjunction to be a finitely generated upperset of
formulas, which itself may not be finite. We abuse the notation in writing the
formulas, and list only the finite set of generators of the upperset to keep
the notation finite. For example, by $\bigwedge\\{a,b\\}$ we implicitly mean
the conjunction applied to the upperset ${\uparrow\\{a,b\\}}$ generated by $a$
and $b$.

Notice that, for finite sets $A$ and $B$ of formulas such that
${\uparrow}A={\uparrow}B$ holds, the equality $\bigwedge A=\bigwedge B$ is
built into the relaxed notation. Similarly for disjunctions, the equality
${\downarrow}A={\downarrow}B$ implies the syntactic equality $\bigvee
A=\bigvee B$. In both conjunction and disjunction, the commutativity,
associativity and idempotence properties are built into the notation as well.

For a given formula $a$, the above remark allows us to define its finite poset
of subformulas and its modal depth inductively.

[Subformulas and modal depth] Given a formula $a$ in ${\mathcal{L}}$, the
(finite) subobject ${\mathsf{Sf}}(a)$ of ${\mathcal{L}}$ is called the
subobject of _subformulas_ of $a$, and is defined inductively as follows.
Simultaneously we define the _modal depth_ $d(a)$.

  1. (1)

For $a$ in ${\mathsf{At}}$, put ${\mathsf{Sf}}(a)=\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
8.9207pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 1.0pt\raise
0.0pt\hbox{$\textstyle{a:{\mathbb{1}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
7.4207pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\hbox{{}{\hbox{\kern 3.0pt\hbox{\ignorespaces\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}}}}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
24.52074pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
24.52074pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
1.0pt\raise
0.0pt\hbox{$\textstyle{\mathcal{L}}$}}}}}}}\ignorespaces}}}}\ignorespaces$ and
$d(a)=0$.

  2. (2)

For $a$ of the form $\bigwedge\varphi$, put

$\displaystyle{\mathsf{Sf}}(a)$ $\displaystyle=$
$\displaystyle\bigcup\limits_{z\in{\mathsf{base}}(\varphi)}{\mathsf{Sf}}(z)\cup
a$ $\displaystyle d(a)$ $\displaystyle=$
$\displaystyle{\mathsf{max}}\\{d(b)\mid\varphi\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}b\\}$

  3. (3)

For $a$ of the form $\bigvee\psi$, put

$\displaystyle{\mathsf{Sf}}(a)$ $\displaystyle=$
$\displaystyle\bigcup\limits_{z\in{\mathsf{base}}(\psi)}{\mathsf{Sf}}(z)\cup
a$ $\displaystyle d(a)$ $\displaystyle=$
$\displaystyle{\mathsf{max}}\\{d(b)\mid
b\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}\psi\\}$

  4. (4)

For $a$ of the form $\nabla\alpha$, put

$\displaystyle{\mathsf{Sf}}(a)$ $\displaystyle=$
$\displaystyle\bigcup\limits_{w\in{\mathsf{base}}(\alpha)}{\mathsf{Sf}}(w)\cup
a$ $\displaystyle d(a)$ $\displaystyle=$
$\displaystyle{\mathsf{max}}\\{d(w)\mid w\in{\mathsf{base}}(\alpha)\\}+1$

Above, all the unions are taken in the lattice of subobjects, see Remark 2.

Let us describe the syntax of the logic for the functor
$T=A\times{\mathit{Id}}$, where as $A$ we take the poset
${\mathbb{2}}=\\{0<1\\}$. If we are given a poset ${\mathsf{At}}$ of atomic
propositions, the syntax is defined inductively as follows:

$a::=p\mid\bigwedge\varphi\mid\bigvee\psi\mid\nabla_{T^{\partial}}(n,a).$

In the above, $p$ is any atomic proposition,
$\varphi={\uparrow}\\{a_{1},\dots,a_{k}\\}$ is a finitely generated upperset
and $\psi={\downarrow}\\{a_{1},\dots,a_{k}\\}$ is a finitely generated
lowerset of formulas, and the $n$ in $\nabla_{T^{\partial}}(n,a)$ is an
element of ${\mathbb{2}}$. Observe that $\nabla$ is monotone with respect to
the first argument.

Hence the more relaxed description of the syntax can be given by

$a::=p\mid\bigwedge\\{a_{1},\dots,a_{k}\\}\mid\bigvee\\{a_{1},\dots,a_{k}\\}\mid\nabla_{T^{\partial}}(n,a).$

###  5.B. The semantics of the coalgebraic language

The above language ${\mathcal{L}}$ will be interpreted in coalgebras for $T$.
More precisely, given a coalgebra $c:X\longrightarrow TX$, the semantics will
be given by a monotone relation
$\textstyle{\Vdash_{0}:{\mathsf{At}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X^{\mathit{op}}}$
called a valuation of propositional atoms. We extend $\Vdash_{0}$ to obtain
the semantics
$\textstyle{\Vdash:{\mathcal{L}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X^{\mathit{op}}}$
of an arbitrary formula $a$ by induction on $a$ as follows:

$\displaystyle x\Vdash\bigwedge\varphi\ $ iff $\displaystyle\ (\forall
a)(\varphi\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}a\mbox{
implies }x\Vdash a)$ $\displaystyle x\Vdash\bigvee\psi\ $ iff $\displaystyle\
(\exists
a)(a\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}\psi\mbox{
and }x\Vdash a)$ $\displaystyle x\Vdash\nabla_{T^{\partial}}\alpha\ $ iff
$\displaystyle\ c(x)\mathrel{\overline{T^{\partial}}{\Vdash}}\alpha$

The semantics for the modality $\nabla$ is indeed well defined: in the
inductive process of defining the relation $\Vdash$ we use that relation
lifting commutes with restrictions (see Definition 4 and Example 4). In
particular, to compute the lifted relation it is enough to have $\Vdash$
restricted to bases of $\alpha$ and $c(x)$ defined previously.

######  Remark 11.

Recall from Remark 10 that ${\mathcal{L}}$ is a poset. The above semantics
allows us to define a monotone relation
$\textstyle{\sqsubseteq:{\mathcal{L}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{L}}$
by putting:

$a\sqsubseteq b\ $ iff for all $c,x$ and all valuations: $x\Vdash a$ implies
$x\Vdash b$. (5.9)

The relation $\sqsubseteq$ is reflexive (i.e., the relation
${\leq_{\mathcal{L}}}$ is smaller than ${\sqsubseteq}$) and transitive (i.e.,
the composite relation ${\sqsubseteq}\cdot{\sqsubseteq}$ is smaller than
${\sqsubseteq}$). Therefore $\sqsubseteq$ allows us to define an order-
quotient ${\mathcal{Q}}={\mathcal{L}}/{\sqsubseteq}$ of ${\mathcal{L}}$. The
elements of the poset $\mathcal{Q}$ are equivalence classes $[a]_{\equiv}$
where

$a\equiv b\ \mbox{iff}\ a\sqsubseteq b\mbox{ and }b\sqsubseteq a$

and $\leq_{\mathcal{Q}}$ is the least order such that $a\sqsubseteq b$ entails
$[a]_{\equiv}\leq_{\mathcal{Q}}[b]_{\equiv}$.

The quotient $\mathcal{Q}$ carries an algebra structure for
${\mathbb{U}}_{\omega}+{\mathbb{L}}_{\omega}+T^{\partial}$ that is derived
from the algebra structure on ${\mathcal{L}}$.

  1. (1)

Nabla for the functor $T=A\times{\mathit{Id}}$. Observe that the functor dual
to $T$ is:

$T^{\partial}X=(A\times X^{\mathit{op}})^{\mathit{op}}=A^{\mathit{op}}\times
X.$

If we fix a coalgebra $c=\langle out,next\rangle:X\longrightarrow A\times X$,
then it holds that

$x\Vdash\nabla_{T^{\partial}}(a,b)\quad\mbox{iff}\quad
out(x)\geq_{A}a\;\mbox{and}\;next(x)\Vdash b,$

since the lifting of the semantics relation
$\textstyle{\Vdash:{\mathcal{L}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X^{\mathit{op}}}$
is the relation

$\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
37.95279pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 1.0pt\raise
0.0pt\hbox{$\textstyle{(\leq_{A^{\mathit{op}}}\times\Vdash):A^{\mathit{op}}\times{\mathcal{L}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
49.95279pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{$\scriptstyle{\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\ignorespaces\lx@xy@stopper}}}}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
61.95279pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
61.95279pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
1.0pt\raise 0.0pt\hbox{$\textstyle{A^{\mathit{op}}\times
X^{\mathit{op}}}$}}}}}}}\ignorespaces}}}}\ignorespaces.$

The monotonicity of $\Vdash$ says that

    1. (a)

If $x\leq_{X}x^{\prime}$ and $x\Vdash\nabla_{T^{\partial}}(a,b)$, then
$x^{\prime}\Vdash\nabla_{T^{\partial}}(a,b)$, and

    2. (b)

if $a\geq_{A}a^{\prime}$ and $b\leq_{\mathcal{L}}b^{\prime}$, then
$x\Vdash\nabla_{T^{\partial}}(a,b)$ implies that
$x\Vdash\nabla_{T^{\partial}}(a^{\prime},b^{\prime})$.

  2. (2)

Nabla for the functor $T=({\mathbb{L}}_{\omega})^{A}\times{\mathbb{2}}$.
Observe that the functor dual to $T$ is:

$T^{\partial}X=({\mathbb{U}}_{\omega}X)^{A}\times{\mathbb{2}}.$

By definition, $x\Vdash\nabla_{T^{\partial}}\alpha$ holds if and only if
$c(x)\mathrel{\overline{T^{\partial}}{\Vdash}}\alpha$ holds. Suppose $c(x)$ is
a tuple $(l,i)$ and $\alpha$ is a tuple $(o,j)$. Then
$c(x)\mathrel{\overline{T^{\partial}}{\Vdash}}\alpha$ holds if and only if

$i\geq j\mbox{ and }(\forall a\in A)(\forall
x)(x\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}l(a)\mbox{
implies
}(\exists\varphi)(o(a)\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}\varphi\mbox{
and }x\Vdash\varphi)).$

We can again use the monotonicity of the semantics relation $\Vdash$ to weaken
the above condition: $c(x)\mathrel{\overline{T^{\partial}}{\Vdash}}\alpha$
holds if and only if

$i\geq j\mbox{ and }(\forall a\in A)(\forall x\in g(l(a)))(\exists\varphi\in
g(o(a)))\ x\Vdash\varphi.$

Here $g(l(a))$ and $g(o(a))$ are, again, the generators for the lowerset
$l(a)$ in $X$ and _upperset_ $o(a)$ in ${\mathcal{L}}$, respectively.

  3. (3)

Recall from Example 2.B that a finitary frame for positive modal logic is a
poset $X$ equipped with a monotone relation
$\textstyle{R:X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}$
that gives rise to two coalgebras

$c:X\longrightarrow{\mathbb{U}}_{\omega}X\ \ \mbox{and}\ \
d:X\longrightarrow{\mathbb{L}}_{\omega}X$

defined by $c(x)=\\{y\ |\ R(x,y)\\}$ and $d(x)=\\{y\ |\ R(y,x)\\}$. The
modalities $\Box$ and $\blacklozenge$ defined by the equivalences

$\displaystyle x\Vdash\Box a$ iff $\displaystyle\ (\forall y)\ (R(x,y)\mbox{
implies }y\Vdash a)$ $\displaystyle x\Vdash\blacklozenge a$ iff
$\displaystyle\ (\exists y)\ (R(y,x)\mbox{ and }y\Vdash a)$

are adjoint in the sense that $a\sqsubseteq\Box b$ holds if and only if
$\blacklozenge a\sqsubseteq b$ holds, where $\sqsubseteq$ is the semantic
preorder as defined in (5.9).

Now, using the definition of the modalities $\nabla_{{\mathbb{L}}_{\omega}}$
and $\nabla_{{\mathbb{U}}_{\omega}}$ and the corresponding liftings of the
semantics $\Vdash$, we see that

$\displaystyle x\Vdash\nabla_{{\mathbb{L}}_{\omega}}\alpha$ iff $\displaystyle
c(x)\mathrel{\overline{{\mathbb{L}}_{\omega}}{\Vdash}}\alpha$ iff
$\displaystyle(\forall
y)(y\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}c(x)\mbox{
implies }(\exists a)\
(a\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}\alpha\mbox{
and }y\Vdash a)),$ $\displaystyle x\Vdash\nabla_{{\mathbb{U}}_{\omega}}\beta$
iff $\displaystyle
d(x)\mathrel{\overline{{\mathbb{U}}_{\omega}}{\Vdash}}\beta$ iff
$\displaystyle(\forall
b)(\beta\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}b\mbox{
implies }(\exists y)\
(d(x)\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}y\mbox{
and }y\Vdash b)).$

Therefore

$\displaystyle\nabla_{{\mathbb{L}}_{\omega}}\alpha$ $\displaystyle\mbox{ can
be expressed as }\Box\bigvee\alpha,$
$\displaystyle\nabla_{{\mathbb{U}}_{\omega}}\beta$ $\displaystyle\mbox{ can be
expressed as }\bigwedge\blacklozenge\beta,$

and also conversely

$\displaystyle\Box a$ $\displaystyle\mbox{ can be expressed as
}\nabla_{{\mathbb{L}}_{\omega}}\\{a\\},$ $\displaystyle\blacklozenge b$
$\displaystyle\mbox{ can be expressed as
}\nabla_{{\mathbb{U}}_{\omega}}\\{b\\}.$

  4. (4)

Recall frames for distributive substructural logics from Example 2.B. We
restrict ourselves to finitary ternary relations $R$ that generate coalgebras
of the form $c_{\otimes}:X\longrightarrow{\mathbb{L}}_{\omega}(X\times X)$.

The polynomial coalgebra functor
$T={\mathbb{L}}_{\omega}({\mathit{Id}}\times{\mathit{Id}})$ is locally
monotone and satisfies BCC. Its relation lifting is easy to compute, using the
properties listed in Example 4. The semantics of the nabla modality for (the
dual of) this functor, which is
$T^{\partial}={\mathbb{U}}_{\omega}({\mathit{Id}}\times{\mathit{Id}})$, works
as follows:

$x\Vdash\nabla_{T^{\partial}}\alpha\mbox{ iff
}(\forall(a_{0},a_{1})\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}\alpha)(\exists(x_{0},x_{1})\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}c(x))\
(x_{0}\Vdash a_{0}\ \&\ x_{1}\Vdash a_{1}).$

Therefore

$\nabla_{T^{\partial}}\alpha\mbox{ can be expressed as
}\bigwedge\limits_{\alpha\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}(a_{0},a_{1})}(a_{0}\otimes
a_{1}),$

and conversely

$(a_{0}\otimes a_{1})\mbox{ can be expressed as
}\nabla_{T^{\partial}}\\{(a_{0},a_{1})\\}.$

###  5.C. Hennessy-Milner property

We now turn to proving that the finitary language defined in Subsection 5.A
has the Hennessy-Milner property — it is adequate and expressive for the
following notion of _similarity_ , which is defined in terms of relation
lifting.

We fix two pointed models $(c,\Vdash_{c},x_{0})$ and $(d,\Vdash_{d},y_{0})$,
i.e., we fix coalgebras $c:X\longrightarrow TX$ and $d:Y\longrightarrow TY$,
valuations $\Vdash_{c}$ and $\Vdash_{d}$, and $x_{0}\in X$ and $y_{0}\in Y$.

  1. (1)

A relation
$\textstyle{S:Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}$
is called a $T$-_simulation_ (from $(d,\Vdash_{d},y_{0})$ to
$(c,\Vdash_{c},x_{0})$), if the following three conditions are satisfied:

    1. (a)

$S(x_{0},y_{0})$ holds.

    2. (b)

For any $x\in X$ and $y\in Y$, $S(x,y)$ implies $\overline{T}S(c(x),d(y))$.

    3. (c)

If $S(x,y)$ holds, then $x\Vdash_{c}p$ implies $y\Vdash_{d}p$, for each atom
$p$ in ${\mathsf{At}}$.

And we say that $(d,\Vdash_{d},y_{0})$ simulates $(c,\Vdash_{c},x_{0})$, if
there is a simulation
$\textstyle{S:Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}$
from $(d,\Vdash_{d},y_{0})$ to $(c,\Vdash_{c},x_{0})$.

  2. (2)

We say that $(d,\Vdash_{d},y_{0})$ is modally stronger than
$(c,\Vdash_{c},x_{0})$, if $x_{0}\Vdash_{c}a$ implies $y_{0}\Vdash_{d}a$, for
each formula $a$.

######  Remark 12.

The notion of simulation given by the monotone relation lifting coincides with
the one given by Worrell in [25] in the enriched setting of
${\mathscr{V}}$-categories (of which preorders, hence also posets, are a
special case for ${\mathscr{V}}={\mathbb{2}}$). It is also shown in [25] that
similarity coincides with the preorder on the final coalgebra, whenever the
final coalgebra exists.

Fix the empty poset ${\mathsf{At}}$ of atomic propositions. Taking two
coalgebras $c:X\longrightarrow A\times X$ and $d:Y\longrightarrow A\times Y$
with two distinguished states $x_{0}\in X$ and $y_{0}\in Y$, the notion of
simulation yields that $(d,\Vdash,y_{0})$ simulates $(c,\Vdash,x_{0})$ if the
infinite stream $\gamma$ obtained as the behaviour of $x_{0}$ is pointwise
smaller than the infinite stream $\delta$ obtained as the behaviour of
$y_{0}$.

######  Proposition 13.

The language ${\mathcal{L}}$ is

  1. (1)

Adequate: if $(d,\Vdash_{d},y_{0})$ simulates $(c,\Vdash_{c},x_{0})$, then
$(d,\Vdash_{d},y_{0})$ is modally stronger than $(c,\Vdash_{c},x_{0})$.

and

  1. (2)

Expressive: if $(d,\Vdash_{d},y_{0})$ is modally stronger than
$(c,\Vdash_{c},x_{0})$, then $(d,\Vdash_{d},y_{0})$ simulates
$(c,\Vdash_{c},x_{0})$. Moreover, the relation “being modally stronger” is a
$T$-simulation.

######  Proof 5.1.

(1) Let us assume that $(d,\Vdash_{d},y_{0})$ simulates $(c,\Vdash_{c},x_{0})$
via a simulation
$\textstyle{S:Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}$.
We need to prove that $x_{0}\Vdash_{c}a$ implies $y_{0}\Vdash_{y}a$ for every
formula $a$. The adequacy is proved by induction on the complexity of a given
formula $a$.

The case when $a$ is an atom is immediate from $S$ being a simulation, the
cases of conjunction and disjunction are easy. For the induction step for
$a=\nabla\alpha$, let us assume that $x_{0}\Vdash_{c}\nabla\alpha$ holds. The
induction hypothesis states that for every $x\in X$, $y\in Y$ and
$z\in{\mathsf{base}}(\alpha)$ the following implication holds:

$\mbox{If }x\Vdash_{c}z\mbox{ and }S(x,y),\mbox{ then }y\Vdash_{d}z.$

The induction hypothesis can equivalently be described as a lax triangle

$\textstyle{Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\Vdash_{d}(-,{\mathsf{base}}(\alpha)-)}$$\scriptstyle{\Vdash_{c}(-,{\mathsf{base}}(\alpha)-)\phantom{MM}}$$\textstyle{Y^{\mathit{op}}}$$\textstyle{X^{\mathit{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{S^{\mathit{con}}}$$\scriptstyle{\uparrow}$
(5.12)

denoting the base of $\alpha$ by
$\textstyle{{\mathsf{base}}(\alpha):Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{L}}$.

We shall prove that for any $x$ in $X$, $y$ in $Y$, and $w\in
T^{\partial}{\mathsf{base}}(\alpha)$, the following implication holds:

$\overline{T}S(c(x),d(y))\mbox{ and
}c(x)\mathrel{\overline{T^{\partial}}{\Vdash_{c}}}w\;\mbox{ implies
}\;d(y)\mathrel{\overline{T^{\partial}}{\Vdash_{d}}}w$ (5.13)

The relation $\overline{T}S(c(x_{0}),d(y_{0}))$ holds since $S$ is a
simulation. Moreover,
$c(x_{0})\mathrel{\overline{T^{\partial}}{\Vdash_{c}}}\alpha$ holds since
$x_{0}\Vdash_{c}\nabla\alpha$ holds. Since $\alpha\in
T^{\partial}{\mathsf{base}}(\alpha)$, we could instantiate the implication to
get that $d(y_{0})\mathrel{\overline{T^{\partial}}{\Vdash_{d}}}\alpha$ holds,
and this would yield $y_{0}\Vdash_{d}\nabla\alpha$ as we wanted.

However, the implication (5.13) can be expressed as the lax triangle

$\textstyle{T^{\partial}\widetilde{{\mathbb{1}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{T^{\partial}}{\Vdash_{d}}(-,T^{\partial}{\mathsf{base}}(\alpha)-)}$$\scriptstyle{\overline{T^{\partial}}{\Vdash_{c}}(-,T^{\partial}{\mathsf{base}}(\alpha)-)\phantom{MM}}$$\textstyle{(TY)^{\mathit{op}}}$$\textstyle{(TX)^{\mathit{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{(\overline{T}S)^{\mathit{con}}}$$\scriptstyle{\uparrow}$

that is, the image under $\overline{T^{\partial}}$ of (5.12). This finishes
the proof.

(2) Expressivity boils down to proving that “being modally stronger” is a
$T$-simulation. For the purpose of the proof, write

$S(x,y)$

to denote that $(d,\Vdash_{d},y)$ is modally stronger than $(c,\Vdash_{c},x)$.

Hence the following implication holds for any formula $a$:

$\mbox{If }S(x,y)\mbox{ and }x\Vdash_{c}a\mbox{, then }y\Vdash_{d}a.$ (5.14)

It is clear that $S$ verifies the properties (a) and (c) of $T$-simulations
from Definition 5.C. It remains to be proved that $S$ satisfies the property
(b):

$\mbox{If }S(x,y)\mbox{, then }\overline{T}S(c(x),d(y)).$ (5.15)

Assume therefore that $S(x,y)$ holds and denote the corresponding bases of
$c(x)$ and $d(y)$ by

$\textstyle{{\mathsf{base}}(c(x)):U\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}$and$\textstyle{{\mathsf{base}}(d(y)):W\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{Y.}$

We first construct a monotone map
$f:X^{\mathit{op}}\longrightarrow{\mathcal{L}}$ such that for any
$x^{\prime}\in X$ and $w\in{\mathsf{base}}(d(y))$ the following two
requirements hold:

$\displaystyle x^{\prime}\Vdash_{c}f(x^{\prime})$ (5.16) $\displaystyle
w\Vdash_{d}f(x^{\prime})\mbox{ implies }S^{\mathit{con}}(w,x^{\prime})$ (5.17)

Fix $x^{\prime}$ in $X$, and for each $w\in{\mathsf{base}}(d(y))$ such that

$\neg S(x^{\prime},w)$

pick a formula $b_{(x^{\prime},w)}$ for which
$x^{\prime}\Vdash_{c}b_{(x^{\prime},w)}$ but
$w\not\Vdash_{d}b_{(x^{\prime},w)}$, which is possible by $\neg
S(x^{\prime},w)$ and (5.14). Define

$f(x^{\prime})=\bigwedge\limits_{w\in{\mathsf{base}}(d(y)):\neg
S(x^{\prime},w)}b_{(x^{\prime},w)}.$

The above conjunction is finitary since $W$ is a finite poset. In case the
conjunction is empty, we set $f(x^{\prime})=\top$. Moreover, $f$ is a monotone
map (with $x^{\prime\prime}\geq x^{\prime}$ the number of conjuncts in the
definition of $f(x^{\prime\prime})$ decreases), and the properties (5.16) and
(5.17) hold. In particular, given any $u\in{\mathsf{base}}(c(x))$, the
implication

$w\Vdash_{d}f(u)\mbox{ implies }S^{\mathit{con}}(w,u)$

holds.

The latter implication can be expressed as a 2-cell

$\textstyle{U^{\mathit{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\uparrow}$$\textstyle{W^{\mathit{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{S^{\mathit{con}}({\mathsf{base}}(d(y)^{\mathit{op}})-,{\mathsf{base}}(c(x)^{\mathit{op}})-)}$$\scriptstyle{\Vdash_{d}({\mathsf{base}}(d(y))-,f{\mathsf{base}}(c(x))-)}$

in ${\mathsf{Rel}}$. We apply the functor $\overline{T^{\partial}}$ to it and
use the properties of relation lifting to obtain a 2-cell

$\textstyle{(TU)^{\mathit{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\uparrow}$$\textstyle{(TW)^{\mathit{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{(\overline{T}S)^{\mathit{con}}((T{\mathsf{base}}(d(y))^{\mathit{op}}-,(T{\mathsf{base}}(c(x))^{\mathit{op}}-)}$$\scriptstyle{\overline{T^{\partial}}{\Vdash_{d}}(T{\mathsf{base}}(d(y))-,T^{\partial}f\cdot
T{\mathsf{base}}(c(x))-)}$ (5.18)

By the unit property of ${\mathsf{base}}$, we know that

$c(x)\in T{\mathsf{base}}(c(x))\mbox{ and }d(y)\in T{\mathsf{base}}(d(y))$

holds. Therefore we can use (5.18) and the definition of the converse of a
relation to observe that $\overline{T}S(c(x),d(y))$ holds whenever
$d(y)\mathrel{\overline{T^{\partial}}{\Vdash_{d}}}(T^{\partial}f)c(x)$ holds.

The relation
$d(y)\mathrel{\overline{T^{\partial}}{\Vdash_{d}}}(T^{\partial}f)c(x)$ holds
iff $y\Vdash_{d}\nabla((T^{\partial}f)c(x))$ holds. Since we assume that
$S(x,y)$ holds, it is enough to prove that
$x\Vdash_{c}\nabla((T^{\partial}f)c(x))$ holds, and
$y\Vdash_{d}\nabla((T^{\partial}f)c(x))$ will follow.

By (5.16) we know that $x^{\prime}\Vdash_{c}f(x^{\prime})$ holds for every
$x^{\prime}$. Thus we get the inequality
${\mathit{id}}_{X}\leq{\Vdash_{c}}(-,f-)$, and by applying the functor
$\overline{T^{\partial}}$ to it, we obtain the inequality
${\mathit{id}}_{T^{\partial}X}\leq\overline{T^{\partial}}{\Vdash_{c}}(-,T^{\partial}f-)$.
Hence $c(x)\mathrel{\overline{T^{\partial}}{\Vdash_{c}}}(T^{\partial}f)c(x)$
holds, and therefore $x\Vdash_{c}\nabla((T^{\partial}f)c(x))$ holds as
required.

###  5.D. A dual modality $\Delta$

In the preceding paragraphs we proved that the coalgebraic language
${\mathcal{L}}$ is expressive. Nevertheless, we introduce a new modality
$\Delta$ in this subsection. The semantics of this new modality will show that
$\Delta$ is, in a sense, dual to $\nabla$. Why would we want to extend the
language with a new modality, knowing that the language with nabla as the only
modality is already expressive? It will turn out that the dual modality is
crucial in designing a _cut-free_ sequent calculus which is sound and complete
for the logic.

The definition of semantics of $\Delta$ below is a straightforward adaptation
of a similar modality studied in the case of ${\mathsf{Set}}$ and classical
Moss’ logic in [15], where $\Delta$ is the _boolean_ dual of $\nabla$. For the
classical Moss’ logic in ${\mathsf{Set}}$, the dual modality $\Delta$, and its
interdefinability with the modality $\nabla$, played a crucial role in the
formulation of a cut-free _two-sided_ sequent calculus as shown in [4].
Without a negation, a one-sided sequent calculus is not available in our case
already for the propositional part of the language ${\mathcal{L}}$. For that
reason we aim at a two-sided calculus, and therefore it seems convenient to
have a modality dual to nabla in the language.

We extend the language ${\mathcal{L}}$ with a monotone modality

$\Delta_{T^{\partial}}:T^{\partial}{\mathcal{L}}\longrightarrow{\mathcal{L}}.$

Given a coalgebra $c:X\longrightarrow TX$ and a monotone valuation
$\textstyle{\Vdash:{\mathcal{L}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X^{\mathit{op}}}$,
the semantics of $\Delta_{T^{\partial}}$ is given by the relation lifting of
the negated relation
$\textstyle{\nVdash:{\mathcal{L}}^{\mathit{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}$
as follows:

$x\nVdash\Delta\alpha\ \mbox{ iff }\
c(x)\mathrel{\overline{T}{\nVdash}}\alpha.$

Before we discuss the mutual relation of the two modalities $\nabla$ and
$\Delta$, we illustrate the semantics of $\Delta$ on the running examples:

  1. (1)

Delta for the functor $T=A\times{\mathit{Id}}$. Let us fix a coalgebra
$c=\langle out,next\rangle:X\longrightarrow A\times X$. The semantics of the
modality $\Delta$ is then given as follows:

$x\Vdash\Delta(a,b)\quad\mbox{iff}\quad
out(x)\nleq_{A}a\;\mbox{or}\;next(x)\Vdash b.$

  2. (2)

Delta for the functor $T=({\mathit{Id}})^{A}\times{\mathbb{2}}$. Fix a
coalgebra $c:X\longrightarrow X^{A}\times{\mathbb{2}}$. If for some state
$x\in X$ we denote by $c(x)=(f,i)$ the successors and output of $x$, the
semantics of the modality $\Delta$ in the state $x$ is given as follows:

$x\Vdash\Delta(\Phi,j)\quad\mbox{iff}\quad j\nleq i\;\mbox{or}\;(\exists
a)f(a)\Vdash\Phi(a)$

  3. (3)

Delta for the functor $T=({\mathbb{L}}_{\omega})^{A}\times{\mathbb{2}}$. For a
coalgebra $c:X\longrightarrow({\mathbb{L}}_{\omega}X)^{A}\times{\mathbb{2}}$
and for its state $x$ with $c(x)=(l,i)$, we have that $x\Vdash\Delta(p,j)$
holds if and only if

$j\nleq i\mbox{ or }(\exists a\in A)(\exists
y\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}l(a))(\forall\varphi\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}p(a))\
y\Vdash\varphi.$

  4. (4)

Consider again finitary frames for positive modal logic with adjoint
modalities (see Example 2.B). We view the frames as coalgebras of the form
$c:X\longrightarrow{\mathbb{U}}_{\omega}X$. The semantics of
$\Delta_{{\mathbb{L}}_{\omega}}$ works as follows:

$\displaystyle x\nVdash\Delta_{{\mathbb{L}}_{\omega}}\beta$
$\displaystyle\equiv$
$\displaystyle(c(x)\mathrel{\overline{{\mathbb{U}}_{\omega}}{\nVdash}}\beta)$
$\displaystyle\equiv$ $\displaystyle((\forall
b)(\beta\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}b\mbox{
implies }(\exists
x^{\prime})(c(x)\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}x^{\prime}\mbox{
and }x^{\prime}\nVdash b))$ $\displaystyle\equiv$ $\displaystyle\neg(\exists
b)(\beta\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}b\mbox{
and }(\forall
x^{\prime})(c(x)\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}x^{\prime}\mbox{
implies }x^{\prime}\Vdash b))$

Therefore

$\Delta_{{\mathbb{L}}_{\omega}}\beta\equiv\bigvee\Box\beta.$

Recall from Example 5.B that

$\Box b\equiv\nabla_{{\mathbb{L}}_{\omega}}\\{b\\}.$

We see that in this particular example $\Delta$ is definable by $\nabla$ as
follows:

$\Delta_{{\mathbb{L}}_{\omega}}\beta\equiv\bigvee\limits_{b\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}\beta}\nabla_{{\mathbb{L}}_{\omega}}\\{b\\}.$

Since the arity functor ${\mathbb{L}}_{\omega}$ is finitary, the above
expression is a well-formed formula.

The above example suggests that the modality $\Delta$ is expressible by a
certain disjunction of $\nabla$ formulas. This is indeed (almost) true in
general. However, for some coalgebra functors the disjunction of the $\nabla$
formulas might be infinite and thus $\Delta$ may not be definable by a well-
formed formula of the finitary language.

To understand the relationship between the modalities $\nabla$ and $\Delta$,
we will first need to understand the relations
$\neg\overline{T}{\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}}$
and
$\neg\overline{T}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}}$.
We will therefore give an inductive definition of these relations for the case
of $T$ being a Kripke-polynomial functor.

We state explicit formulas for the relation
$\textstyle{\neg\overline{T}{\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}}:T^{\partial}{\mathbb{L}}_{\omega}X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{T^{\partial}X}$
when $T$ is a Kripke-polynomial functor.

  1. (1)

$T={\mathit{const}}_{E}$: The relation
$\textstyle{\neg\overline{E}{\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}}:E^{\mathit{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{E^{\mathit{op}}}$
is the relation
$\textstyle{\not\leq_{E}:E^{\mathit{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{E^{\mathit{op}}}$.

  2. (2)

$T={\mathit{Id}}$: The relation
$\textstyle{\neg\overline{{\mathit{Id}}}{\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}}:{\mathbb{L}}_{\omega}X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}$
is the relation
$\textstyle{\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}:{\mathbb{L}}_{\omega}X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}$.

  3. (3)

$T=T_{1}+T_{2}$: Let $\alpha$ be in $T_{i}^{\partial}X$ and $\Phi$ be in
$T_{j}^{\partial}{\mathbb{L}}_{\omega}X$ for some $i,j$ in $\\{1,2\\}$. The
relation
$\alpha\mathrel{\neg(\overline{T_{1}+T_{2}}{\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}})}\Phi$
holds iff $i\neq j$ or
$\alpha\mathrel{\neg\overline{T_{i}}{\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}}}\Phi$
with $i=j$.

  4. (4)

$T=T_{1}\times T_{2}$: The relation
$(\alpha_{1},\alpha_{2})\mathrel{\neg(\overline{T_{1}\times
T_{2}}{\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}})}(\Phi_{1},\Phi_{2})$
holds iff
$\alpha_{1}\mathrel{\neg\overline{T_{1}}{\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}}}\Phi_{1}$
or
$\alpha_{2}\mathrel{\neg\overline{T_{2}}{\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}}}\Phi_{2}$
holds.

  5. (5)

$T=T_{1}^{E}$: Generalising the case (4), the relation
$\alpha\mathrel{\neg\overline{T_{1}^{E}}{\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}}}\Phi$
holds iff there is some $e$ from $E$ such that
$\alpha(e)\mathrel{\neg\overline{T_{1}}{\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}}}\Phi(e)$
holds.

  6. (6)

$T={\mathbb{L}}_{\omega}T_{1}$: The relation
$v\mathrel{\neg\overline{{\mathbb{L}}_{\omega}T_{1}}{\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}}}u$
holds iff the following condition is satisfied:

$(\exists\alpha\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}v)(\forall\Phi\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}u)\;\alpha\mathrel{\neg\overline{T_{1}}{\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}}}\Phi.$

The formulas for the relation
$\textstyle{\neg\overline{T}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}}:T^{\partial}{\mathbb{L}}_{\omega}X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{T^{\partial}X}$
are easy to obtain by dual reasoning. For example, the relation
$u\mathrel{\neg\overline{{\mathbb{L}}_{\omega}T_{1}}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}}}v$
holds if and only if the following condition is satisfied:

$(\exists\Phi\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}u)(\forall\alpha\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}v)\;\Phi\mathrel{\neg\overline{T_{1}}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}}}\alpha.$

Let us fix elements $\alpha\in T^{\partial}{\mathcal{L}}$ and $\beta\in
T^{\partial}{\mathcal{L}}$.

We define the collections $R_{\alpha}$ and $L_{\beta}$ as follows:

  1. (1)

$R_{\alpha}$ is the collection of all elements $\Psi\in
T^{\partial}{\mathbb{L}}_{\omega}{\mathsf{base}}(\alpha)$ with

$\alpha\mathrel{\neg\overline{T}{\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}}}\Psi.$

  2. (2)

$L_{\beta}$ is the collection of all elements $\Phi\in
T^{\partial}{\mathbb{U}}_{\omega}{\mathsf{base}}(\beta)$ with

$\Phi\mathrel{\neg\overline{T}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}}}\beta.$

To illustrate the above definition we give two simple examples:

  1. (1)

Consider $T^{\partial}={\mathbb{L}}_{\omega}$, thus $T={\mathbb{U}}_{\omega}$.
Note that
$\alpha\neg\overline{{\mathbb{U}}_{\omega}}\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}\Psi$
holds iff

$\exists\psi(\Psi\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}\psi\mbox{
and }\forall
a(\alpha\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}a\mbox{
implies
}a\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}\psi)).$

For $\alpha=\\{\bot\\}$, the collection $R_{\\{\bot\\}}$ consists of those
elements $\Psi$ of ${\mathbb{L}}_{\omega}{\mathbb{L}}_{\omega}\\{\bot\\}$,
where some
$\psi\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}\Psi$
contains $\bot$. The only such lowerset $\Psi$ is
$\\{\emptyset,\\{\bot\\}\\}$. Thus $R_{\\{\bot\\}}$ equals
$\\{\\{\emptyset,\\{\bot\\}\\}\\}$.

  2. (2)

Consider $T^{\partial}=\mathbb{N}^{\mathit{op}}\times{\mathit{Id}}$ where
$\mathbb{N}$ is the poset of natural numbers with their natural order, and
$T=\mathbb{N}\times{\mathit{Id}}$. For $\alpha=(5,b\wedge c)$, the collection
$R_{(5,b\wedge c)}$ consists of elements $(n,\psi)$ of
$N^{\mathit{op}}\times{\mathbb{L}}_{\omega}{\mathsf{base}}(5,b\wedge c)$ where
$5\nleq n$ or $b\wedge
c\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}\psi$.
Note that ${\mathbb{L}}_{\omega}{\mathsf{base}}(5,b\wedge
c)=\\{\emptyset,\\{b\wedge c\\}\\}$. Therefore $R_{(5,b\wedge
c)}=\\{(n,\emptyset)\ |\ 5\nleq n\\}\cup\\{(n,\\{b\wedge c\\})\ |\ n\in N\\}$.

It is shown in [15] that the two modalities $\nabla$ and $\Delta$ are mutually
definable already in the positive fragment of the classical Moss’ logic. Their
mutual definability is used in [4] in designing a two-sided sequent proof
system for the logic. We will state a similar fact in our setting in the
following two propositions. They will become useful in the next section, when
we define a sequent proof system.

######  Proposition 14.

For each coalgebra $c:X\longrightarrow TX$ and every semantics relation
$\Vdash_{c}$, the relations

$\textstyle{T^{\partial}{\mathcal{L}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{\Vdash_{c}}(-,\Delta-)}$$\textstyle{X^{\mathit{op}}}$

and

$\textstyle{T^{\partial}{\mathcal{L}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\neg(\overline{T}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}})}$$\textstyle{T^{\partial}{\mathbb{U}}_{\omega}{\mathcal{L}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{\Vdash_{c}}(-,\nabla
T^{\partial}\bigwedge-)}$$\textstyle{X^{\mathit{op}}}$

are equal.

In other words, for each $x$ in $X$, and each $\beta$ in
$T^{\partial}{\mathcal{L}}$, we have that $x\Vdash_{c}\Delta\beta$ holds if
and only if there is a $\Phi$ in
$T^{\partial}{\mathbb{U}}_{\omega}{\mathcal{L}}$ such that

$\Phi\mathrel{\neg{\overline{T}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}}}}\beta\mbox{
and }\ x\Vdash_{c}\nabla(T^{\partial}\bigwedge)\Phi.$

Whenever $L_{\beta}$ is finite, we have the following semantic equivalence:

$\Delta\beta\equiv\bigvee\limits_{\Phi\in
L_{\beta}}\nabla(T^{\partial}\bigwedge)\Phi.$

######  Proof 5.2.

We divide the proof into several parts:

  1. (1)

The inequality ${\Vdash_{c}}(-,\Delta-)\leq{\Vdash_{c}}(-,\nabla
T^{\partial}\bigwedge-)\cdot\neg(\overline{T}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}})$.

Suppose that $x\Vdash\Delta\beta$ holds. We will construct an element
$\Phi_{x}$ in $(T^{\partial}{\mathbb{U}}_{\omega}{\mathcal{L}})^{\mathit{op}}$
such that

$\Phi\mathrel{\neg{\overline{T}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}}}}\beta\
\mbox{ and }\ x\Vdash_{c}\nabla(T^{\partial}\bigwedge)\Phi_{x}.$

To that end, consider the monotone map

$f^{\sharp}:X\longrightarrow({\mathbb{U}}_{\omega}{\mathcal{L}})^{\mathit{op}},\quad
x\mapsto{\uparrow}\\{w\in{\mathsf{base}}(\beta)\ |\ x\Vdash_{c}w\\}.$

Using the base of $\beta$, denoted by
${\mathsf{base}}(\beta):W\longrightarrow{\mathcal{L}}$, we can factorise
$f^{\sharp}$ as follows:

$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\scriptstyle{f^{\sharp}}$$\textstyle{({\mathbb{U}}_{\omega}W)^{\mathit{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{({\mathbb{U}}_{\omega}{\mathsf{base}}(\beta))^{\mathit{op}}}$$\textstyle{({\mathbb{U}}_{\omega}{\mathcal{L}})^{\mathit{op}}}$

The mapping $f$ is then defined as

$f:X\longrightarrow({\mathbb{U}}_{\omega}W)^{\mathit{op}},\quad
x\mapsto\\{w\in W\ |\ x\Vdash_{c}{\mathsf{base}}(\beta)(w)\\}.$

Define the element $\Phi_{x}$ in
$(T^{\partial}{\mathbb{U}}_{\omega}{\mathcal{L}})^{\mathit{op}}$ to be

$\Phi_{x}=(Tf^{\sharp})c(x).$

    1. (a)

To prove that
$\Phi\mathrel{\neg{\overline{T}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}}}}\beta$
holds, it suffices to prove that

$c(x)\mathrel{\neg\overline{T}{\nVdash}}\beta\ \ \mbox{implies}\ \
\Phi_{x}\mathrel{\neg\overline{T}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}}}\beta.$

We reason by contraposition and we assume that
$\Phi_{x}\mathrel{\overline{T}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}}}\beta$
to show that then $c(x)\mathrel{\overline{T}{\nVdash}}\beta$, contradicting
the assumption $x\Vdash\Delta\beta$.

By the definition of $f^{\sharp}$, observe that for any
$w\in{\mathsf{base}}(\beta)$ we have an implication

$x\Vdash_{c}w\mbox{ implies
}fx\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}w.$

By contraposition,
$fx\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}w$
implies $x\not\Vdash_{c}w$. Write this implication as a 2-cell

$\textstyle{W^{\mathit{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\uparrow}$$\textstyle{X.\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{\not\Vdash_{c}}(-,{\mathsf{base}}(\beta)^{\mathit{op}}-)}$$\scriptstyle{{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}}(f-,-)}$

The image under $\overline{T}$ of the above 2-cell yields

$\textstyle{(T^{\partial}W)^{\mathit{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\uparrow}$$\textstyle{TX\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{T}{\not\Vdash_{c}}(-,(T^{\partial}{\mathsf{base}}(\beta))^{\mathit{op}}-)}$$\scriptstyle{\overline{T}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}}(Tf-,-)}$

The unit property of base says that $\beta\in
T^{\partial}{\mathsf{base}}(\beta)$ holds. By assumption
$\Phi_{x}\mathrel{\overline{T}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}}}\beta$
holds; since $\Phi_{x}=(Tf^{\sharp})c(x)$, we deduce that
$(Tf^{\sharp})(c(x))\mathrel{\overline{T}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}}}\beta$
holds, and therefore
$(Tf)(c(x))\mathrel{\overline{T}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}}}\beta$
holds. Hence we have $c(x)\mathrel{\overline{T}{\nVdash}}\beta$ by using the
above 2-cell. This is a contradiction with $x\Vdash_{c}\Delta\beta$.

    2. (b)

We prove that $x\Vdash_{c}\nabla(T^{\partial}\bigwedge)\Phi_{x}$ holds by
proving
$c(x)\mathrel{\overline{T^{\partial}}{\Vdash}}(T^{\partial}\bigwedge)\Phi_{x}$.

See that by the definition of $f^{\sharp}$ we have that $x\Vdash_{c}\bigwedge
f^{\sharp}(x)$ holds. The monotonicity of $\Vdash_{c}$ together with the
definition of conjunction says that for any other
$\varphi\in{\mathbb{U}}_{\omega}{\mathcal{L}}$ with $f^{\sharp}(x)\leq\varphi$
we can deduce $x\Vdash_{c}\bigwedge\varphi$. This observation yields a 2-cell
in ${\mathsf{Rel}}$ of the form

$\textstyle{{\mathbb{U}}_{\omega}{\mathcal{L}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\uparrow}$$\textstyle{X^{\mathit{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{\Vdash_{c}}(-,\bigwedge-)}$$\scriptstyle{\leq_{{\mathbb{U}}_{\omega}{\mathcal{L}}}((f^{\sharp})^{\mathit{op}}-,-)}$

By applying $\overline{T^{\partial}}$ to the above 2-cell we obtain

$\textstyle{T^{\partial}{\mathbb{U}}_{\omega}{\mathcal{L}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\uparrow}$$\textstyle{(TX)^{\mathit{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{T^{\partial}}{\Vdash_{c}}(-,T^{\partial}\bigwedge-)}$$\scriptstyle{\leq_{T^{\partial}{\mathbb{U}}_{\omega}{\mathcal{L}}}(Tf^{\sharp})^{\mathit{op}}-,-)}$

Since $(Tf^{\sharp})^{\mathit{op}}c(x)=(Tf^{\sharp})c(x)=\Phi_{x}$, we have in
particular the inequality $(Tf^{\sharp})^{\mathit{op}}c(x)\leq\Phi_{x}$ in
$T^{\partial}{\mathbb{U}}_{\omega}{\mathcal{L}}$. By the above 2-cell, the
relation
$c(x)\mathrel{\overline{T^{\partial}}{\Vdash_{c}}}(T^{\partial}\bigwedge)\Phi_{x}$
follows.

  2. (2)

The inequality ${\Vdash_{c}}(-,\nabla
T^{\partial}\bigwedge-)\cdot\neg(\overline{T}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}})\leq{\Vdash_{c}}(-,\Delta-)$.

Consider $x$, $\Phi$ and $\beta$ of the appropriate type such that

$\Phi\mathrel{\neg{\overline{T}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}}}}\beta\
\mbox{ and }\ x\Vdash_{c}\nabla(T^{\partial}\bigwedge)\Phi.$

We need to show that $x\Vdash_{c}\Delta\beta$ holds, so by the definition of
the semantics of $\Delta$ we need to prove that
$c(x)\mathrel{\neg\overline{T}{\nVdash}}\beta$ holds. Reasoning by
contraposition, we show that

$c(x)\mathrel{\overline{T}{\nVdash}}\beta\ \ \mbox{entails}\ \
\Phi\mathrel{\overline{T}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}}}\beta,$

contradicting the assumption.

First let us observe that whenever there is an $x_{0}\in X$ such that
$x_{0}\not\Vdash_{c}w$ for some $w\in{\mathsf{base}}(\beta)$, and
$x_{0}\Vdash_{c}\bigwedge u$ for an upperset
$u\in{\mathbb{U}}_{\omega}{\mathsf{base}}(\beta)$, then
$u\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}w$
follows. This is precisely the information contained in the 2-cell in
${\mathsf{Rel}}$ of the form

$\textstyle{{\mathbb{U}}_{\omega}W\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}}^{\mathit{con}}({\mathsf{base}}(\beta)-,{\mathbb{U}}_{\omega}{\mathsf{base}}(\beta)-)}$$\scriptstyle{{\Vdash_{c}}(-,\bigwedge\cdot{\mathbb{U}}_{\omega}{\mathsf{base}}(\beta)-)\phantom{MMM}}$$\textstyle{W}$$\textstyle{X^{\mathit{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\uparrow}$$\scriptstyle{\phantom{MMM}{\not\Vdash_{c}}^{\mathit{con}}({\mathsf{base}}(\beta)^{\mathit{op}}-,-)}$

Apply $\overline{T^{\partial}}$ to the above lax triangle to obtain

$\textstyle{T^{\partial}{\mathbb{U}}_{\omega}W\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{(\overline{T}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}})^{\mathit{con}}(T^{\partial}{\mathsf{base}}(\beta)-,T^{\partial}{\mathbb{U}}_{\omega}{\mathsf{base}}(\beta)-)}$$\scriptstyle{\overline{T^{\partial}}{\Vdash_{c}}(-,T^{\partial}\bigwedge\cdot
T^{\partial}{\mathbb{U}}_{\omega}{\mathsf{base}}(\beta)-)\phantom{MMMM}}$$\textstyle{T^{\partial}W}$$\textstyle{(TX)^{\mathit{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\uparrow}$$\scriptstyle{\phantom{MMM}(\overline{T}{\not\Vdash_{c}})^{\mathit{con}}(\overline{T}{\mathsf{base}}(\beta)^{\mathit{op}}-,-)}$

Use the unit properties $\beta\in T^{\partial}{\mathsf{base}}(\beta)$ and
$\Phi\in T^{\partial}{\mathbb{U}}_{\omega}{\mathsf{base}}(\beta)$ together
with the assumptions
$c(x)\mathrel{\overline{T^{\partial}}{\Vdash}}(T^{\partial}\bigwedge)\Phi$ and
$c(x)\mathrel{\overline{T}{\nVdash}}\beta$ to conclude that
$\Phi\mathrel{\overline{T}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{$\sqsupset$\cr$-$\cr}}}}}\beta$
holds.

We proved the desired equality of the two relations. The last assertion of the
proposition is trivial.

The previous proposition states that under certain conditions, the modality
$\Delta$ is semantically equivalent to a disjunction of $\nabla$ formulas. The
following proposition deals with the dual statement: the modality $\nabla$ is
semantically equivalent to a conjunction of $\Delta$ formulas.

######  Proposition 15.

For each coalgebra $c:X\longrightarrow TX$ and every semantics relation
$\Vdash_{c}$, the relations

$\textstyle{T^{\partial}{\mathcal{L}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{\Vdash_{c}}(-,\nabla-)}$$\textstyle{X^{\mathit{op}}}$

and

$\textstyle{T^{\partial}{\mathcal{L}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\neg\overline{T}{\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}}}$$\textstyle{T^{\partial}{\mathbb{L}}_{\omega}{\mathcal{L}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{\Vdash_{c}}(-,\Delta
T^{\partial}\bigvee-)}$$\textstyle{X^{\mathit{op}}}$

are equal.

In other words, for each $x$ in $X$, and each $\alpha$ in
$T^{\partial}{\mathcal{L}}$, $x\Vdash_{c}\nabla\beta$ holds iff there is a
$\Psi$ in $T^{\partial}{\mathbb{L}}_{\omega}{\mathcal{L}}$ such that

$\alpha\mathrel{\neg{\overline{T}{\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{$\sqsubset$\cr$-$\cr}}}}}}\Psi\
\mbox{ and }\ x\Vdash_{c}\Delta(T^{\partial}\bigvee)\Psi.$

Whenever $R_{\alpha}$ is finite, we have the following semantic equivalence:

$\nabla\alpha\equiv\bigwedge\limits_{\Psi\in
R_{\alpha}}\Delta(T^{\partial}\bigvee)\Psi.$

######  Proof 5.3.

The proof is completely analogous to that of Proposition 14.

##  6\. Proof system and completeness

In this section we define a sequent calculus ${\mathbf{G}}_{\nabla\Delta}$ for
the coalgebraic language ${\mathcal{L}}$ defined in Section 5. We prove that
the calculus is complete with respect to the semantics of ${\mathcal{L}}$
given therein. The definition of the calculus as well as the completeness
proof is general and parametric in the coalgebra functor $T$.

The calculus we are going to define can be seen as an appropriate
generalisation of the two-sided sequent calculus for Moss’ coalgebraic logic
of coalgebras in ${\mathsf{Set}}$ as presented in [4].

###  6.A. The proof system ${\mathbf{G}}_{\nabla\Delta}$

The calculus ${\mathbf{G}}_{\nabla\Delta}$ will manipulate sequents. A
_sequent_ is a syntactic object of the form $\varphi\Rightarrow\psi$ where
$\varphi$ is a finitely generated upperset of formulas, i.e. $\varphi$ is in
${\mathbb{U}}_{\omega}{\mathcal{L}}$, and $\psi$ is a finitely generated
lowerset of formulas, i.e., $\psi$ is in ${\mathbb{L}}_{\omega}{\mathcal{L}}$.
When writing down a sequent we often list only the generators of the
corresponding lowersets and uppersets to keep the notation finite. If
$\varphi$ is an upperset of formulas (or a finite list of its generators), by
writing $\varphi,a$ we mean the upperset generated by $\varphi\cup\\{a\\}$,
and similarly for lowersets.

Given a coalgebra $c:X\longrightarrow TX$ equipped with a monotone valuation
$\Vdash_{c}$ and a state $x_{0}$, we say that sequent $\varphi\Rightarrow\psi$
is _refuted_ in $x_{0}$ if $x_{0}\Vdash_{c}\bigwedge\varphi$ while