* This is a revised and extended version of a paper which appeared in the proceedings of CSL 2020 [KR20]. Part of this research was carried out during the second author’s stay at University College London, funded by the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 795119.

# Expressive Logics for Coinductive Predicates

Clemens Kupke  Department of Computer & Information Sciences, Strathclyde
University, United Kingdom<EMAIL_ADDRESS>and  Jurriaan Rot
Institute for Computing and Information Sciences (iCIS), Radboud University,
The Netherlands<EMAIL_ADDRESS>
###### Abstract.

The classical Hennessy-Milner theorem says that two states of an image-finite
transition system are bisimilar if and only if they satisfy the same formulas
in a certain modal logic. In this paper we study this type of result in a
general context, moving from transition systems to coalgebras and from
bisimilarity to coinductive predicates. We formulate when a logic fully
characterises a coinductive predicate on coalgebras, by providing suitable
notions of adequacy and expressiveness, and give sufficient conditions on the
semantics. The approach is illustrated with logics characterising similarity,
divergence and a behavioural metric on automata.

###### Key words and phrases:

Coalgebra, Fibration, Modal Logic

##  1\. Introduction

The deep connection between bisimilarity and modal logic manifests itself in
the _Hennessy-Milner theorem_ : two states of an image-finite labelled
transition system (LTS) are behaviourally equivalent iff they satisfy the same
formulas in a certain modal logic [HM85]. From left to right, this equivalence
is sometimes referred to as _adequacy_ of the logic w.r.t. bisimilarity, and
from right to left as _expressiveness_. By stating both adequacy and
expressiveness, the Hennessy-Milner theorem thus gives a logical
characterisation of behavioural equivalence.

There are numerous variants and generalisations of this kind of result. For
instance, a state $x$ of an LTS _simulates_ a state $y$ if every formula
satisfied by $x$ is also satisfied by $y$, where the logic only has
conjunction and diamond modalities; see [vG90] for this and many other related
results. Another class of examples is logical characterisations of
quantitative notions of equivalence, such as probabilistic bisimilarity and
behavioural distances (e.g., [LS91, DGJP99, DEP02, vBW05, JS09, KM18, WSPK18,
CFKP19]). In many such cases, including bisimilarity, the comparison between
states is _coinductive_ , and the problem is thus to characterise a
coinductively defined relation (or distance) with a suitable modal logic.

Both coinduction and modal logic can be naturally and generally studied within
the theory of _coalgebra_ , which provides an abstract, uniform study of
state-based systems [Rut00, Jac16]. Indeed, in the area of _coalgebraic modal
logic_ [KP11] there is a rich literature on deriving expressive logics for
behavioural equivalence between state-based systems, thus going well beyond
labelled transition systems [Pat04, Sch08, Kli07]. However, such results focus
almost exclusively on behavioural equivalence or bisimilarity—a coalgebraic
theory of logics for characterising coinductive predicates other than
bisimilarity is still missing. The aim of this paper is to accommodate the
study of logical characterisation of coinductive predicates in a general
manner, and provide tools to prove adequacy and expressiveness.

Our approach is based on universal coalgebra, to achieve results that apply
generally to state-based systems. Central to the approach are the following
two ingredients.

  1. (1)

_Coinductive predicates in a fibration._ To characterise coinductive
predicates, we make use of fibrations—this approach originates from the
seminal work of Hermida and Jacobs [HJ98]. The fibration is used to speak
about predicates and relations on states. In this context, liftings of the
type functor of coalgebras uniformly determine coinductive predicates and
relations on such coalgebras. An important feature of this approach, advocated
in [HKC18], is that it covers not only bisimilarity, but also other
coinductive predicates including, e.g., similarity of labelled transition
systems and other coalgebras [HJ04], behavioural metrics [BBKK18, BKP18,
SKDH18], unary predicates such as divergence [BPPR17, HKC18], and many more.

  2. (2)

_Coalgebraic modal logic via dual adjunctions._ We use an abstract formulation
of coalgebraic logic, which originated in [PMW06, Kli07], building on a
tradition of logics via duality (e.g., [KKP04, BK05b]). This framework is
formulated in terms of a contravariant adjunction, which captures the basic
connection between states and theories, and a distributive law, which captures
the one-step semantics of the logic. It covers classical modal logics of
course, but also easily accommodates multi-valued logics, and, e.g., logics
without propositional connectives, where formulas can be thought of as basic
tests on state-based systems. This makes the framework suitable for an
abstract formulation of Hennessy-Milner type theorems, where formulas play the
role of tests on state-based systems.

To formulate adequacy and expressiveness with respect to general coinductive
predicates, we need to know how to compare collections of formulas. For
instance, if the coinductive predicate is similarity of LTSs, then the
associated logical theories of one state should be _included_ in the other,
not necessarily equal. This amounts to stipulating a _relation_ on truth
values, that extends to a relation between theories. In the quantitative case,
we need a _logical distance_ between collections of formulas; this typically
arises from a distance between truth values (which, in this case, will
typically be an interval in the real numbers). The fibrational setting
provides a convenient means for defining such an object for comparing
theories.

With this in hand, we arrive at the main contributions of this paper: the
formulation of adequacy and expressiveness of a coalgebraic modal logic with
respect to a coinductive predicate in a fibration, and sufficient conditions
on the semantics of the logic that guarantee adequacy and expressiveness. We
exemplify the approach through a range of examples, including logical
characterisations of a simple behavioural distance on deterministic automata,
similarity of labelled transition systems, and a logical characterisation of a
unary predicate: divergence, the set of states of an LTS which have an
infinite path of outgoing $\tau$-steps. The latter is characterised, on image-
finite LTSs, by a quantitative logic with only diamond formulas, i.e., the set
of formulas is simply the set of words.

### Related work

As mentioned above, there are numerous specific results on Hennessy-Milner
theorems, which—e.g., in the probabilistic setting as in [CFKP19]—can be
highly non-trivial. A comprehensive historical treatment is beyond the scope
of this paper, which is, instead, broad: it aims at studying these kinds of
results in a general, coalgebraic setting.

The case of capturing bisimilarity and behavioural equivalence of coalgebras
by modal logics has been very well studied, see [KP11] for an overview.
Expressiveness w.r.t. similarity has been studied in [KKV12], which is close
in spirit to our approach, but focuses on the poset case. On a detailed level,
the logic for similarity is based on distributive lattices, hence it uses
disjunction; this differs from our example, which only uses conjunction and
diamond modalities. Another study of expressiveness of logics w.r.t. various
forms of similarity is in [Wil13]. Expressiveness of multi-valued coalgebraic
logics w.r.t. behavioural equivalence is studied in [BD16]. In [BH17], notions
of equivalence are extracted from a logic through a variant of
$\Lambda$-bisimulation [GS13]. To the best of our knowledge, the current work
is the first in the area that connects general coinductive predicates in a
fibration to coalgebraic logics.

In the recent [DMS19], the authors prove Hennessy-Milner type theorems for
coalgebras including, but going significantly beyond bisimilarity. The logics
are related to a semantics obtained from graded monads. The scope differs
substantially from the current paper: the graded monad approach is inductive
and focuses on semantic equivalence of different types, whereas our framework
aims at characterising coinductive predicates, and in our approach it is
essential to be able to relate theories in different ways than equivalence (to
cover, e.g., similarity, divergence or logical distance). On the one hand, it
appears that none of our examples can be covered immediately in _loc. cit._ ;
on the other hand, trace equivalence of various kinds can be covered in
[DMS19] but not (directly) in the current paper.

In [WSPK18] a characterisation theorem is shown for fuzzy modal logic, and in
[KM18] for a wide class of behavioural metrics. These papers are not aimed at
other kinds of coinductive predicates, and they do not cover the examples in
Section 4 (including the behavioural metric for deterministic automata, as we
use a much simpler logic than in [KM18]). Conversely, the question whether the
logical characterisation results of [KM18] can be covered in the current
framework is left open. These papers also treat game-based characterisations
of bisimilarity, which are studied in a general setting in the recent
[KKH+19]. That paper, however, does not yet feature modal logic explicitly; in
fact, the connection is posed there as future work.

An earlier version of this paper appeared in the proceedings of CSL 2020
[KR20]. The current paper extends this with a more detailed treatment of the
basic setup of logics in a contravariant adjunction in Section 2.3, a
treatment of expressiveness of logics w.r.t. behavioural equivalence rather
than bisimilarity making use of so-called lax liftings, in Section 3.2, and a
new section on finite-depth expressiveness via initial and final sequences
(Section 5).

### Outline

The paper starts in Section 2 with preliminaries on coalgebra, fibrations and
coinductive predicates, and coalgebraic modal logic. Section 3 contains the
abstract framework for expressiveness and adequacy, together with sufficient
conditions for establishing these. Section 4 contains three detailed examples
of this setup. A different route to expressiveness, via initial and final
sequences, is explored in Section 5. The paper concludes in Section 6 with
directions for future work.

### Acknowledgments

We would like to thank Fredrik Nordvall Forsberg, Ichiro Hasuo, Bart Jacobs,
Shin-ya Katsumata and Yuichi Komorida for helpful discussions, comments and
suggestions.

##  2\. Preliminaries

The category of sets and functions is denoted by $\mathsf{Set}$. The powerset
functor is denoted by $\mathcal{P}\colon\mathsf{Set}\rightarrow\mathsf{Set}$,
and the finite powerset functor by $\mathcal{P}_{\omega}$. The diagonal
relation on a set $X$ is denoted by $\Delta_{X}=\\{(x,x)\mid x\in X\\}$.

Let $\mathcal{C}$ be a category, and
$B\colon\mathcal{C}\rightarrow\mathcal{C}$ a functor. A _$(B)$ -coalgebra_ is
a pair $(X,\gamma)$ where $X$ is an object in $\mathcal{C}$ and $\gamma\colon
X\rightarrow BX$ a morphism. A homomorphism from a coalgebra $(X,\gamma)$ to a
coalgebra $(Y,\theta)$ is a morphism $h\colon X\rightarrow Y$ such that
$\theta\circ h=Bh\circ\gamma$. An _algebra_ for a functor
$L\colon\mathcal{D}\rightarrow\mathcal{D}$ on a category $\mathcal{D}$ is a
pair $(A,\alpha)$ of an object $A$ in $\mathcal{D}$ and an arrow $\alpha\colon
LA\rightarrow A$.

######  Example .

A _labelled transition system (LTS)_ over a set of labels $A$ is a coalgebra
$(X,\gamma)$ for the functor $B\colon\mathsf{Set}\rightarrow\mathsf{Set}$,
$BX=(\mathcal{P}X)^{A}$. For states $x,x^{\prime}\in X$ and a label $a\in A$,
we sometimes write $x\xrightarrow{a}x^{\prime}$ for
$x^{\prime}\in\gamma(x)(a)$. Image-finite labelled transition systems are
coalgebras for the functor $BX=(\mathcal{P}_{\omega}X)^{A}$. A _deterministic
automaton_ over an alphabet $A$ is a coalgebra for the functor
$B\colon\mathsf{Set}\rightarrow\mathsf{Set}$, $BX=2\times X^{A}$. For many
other examples of state-based systems modelled as coalgebras, see, e.g.,
[Jac16, Rut00].

###  2.1. Coinductive Predicates in a Fibration

We recall the general approach to coinductive predicates in a fibration,
starting by briefly presenting how bisimilarity of $\mathsf{Set}$ coalgebras
arises in this setting (see [HKC18, HJ98, Jac16] for details). Let
$\mathrm{Rel}$ be the category where an object is a pair $(X,R)$ consisting of
a set $X$ and a relation $R\subseteq X\times X$ on it, and a morphism from
$(X,R)$ to $(Y,S)$ is a map $f\colon X\rightarrow Y$ such that $x\mathrel{R}y$
implies $f(x)\mathrel{R}f(y)$, for all $x,y\in X$. Below, we sometimes refer
to an object $(X,R)$ only by the relation $R\subseteq X\times X$. Any set
functor $B\colon\mathsf{Set}\rightarrow\mathsf{Set}$ gives rise to a functor
$\mathrm{Rel}(B)\colon\mathrm{Rel}\rightarrow\mathrm{Rel}$, defined by
_relation lifting_ :

$\mathrm{Rel}(B)(R\subseteq X\times X)=\\{((B\pi_{1})(z),(B\pi_{2})(z))\in
BX\times BX\mid z\in BR\\}\,.$ (1)

Given a $B$-coalgebra $(X,\gamma)$, a _bisimulation_ is a relation $R\subseteq
X\times X$ such that
$R\subseteq(\gamma\times\gamma)^{-1}(\mathrm{Rel}(B)(R))$, i.e., if
$x\mathrel{R}y$ then $\gamma(x)\mathrel{\mathrm{Rel}(B)(R)}\gamma(y)$.
_Bisimilarity_ is the greatest such relation, and equivalently, the greatest
fixed point of the monotone map
$R\mapsto(\gamma\times\gamma)^{-1}(\mathrm{Rel}(B)(R))$ on the complete
lattice of relations on $X$, ordered by inclusion.

The functor $\mathrm{Rel}(B)$ is a _lifting_ of $B$: it maps a relation on $X$
to a relation on $BX$. A first step towards generalisation beyond bisimilarity
is obtained by replacing $\mathrm{Rel}(B)$ by an arbitrary lifting
$\overline{B}\colon\mathrm{Rel}\rightarrow\mathrm{Rel}$ of $B$. For instance,
for $BX=(\mathcal{P}_{\omega}X)^{A}$ one may take

$\overline{B}(R)=\\{(t_{1},t_{2})\mid\forall a\in A.\,\forall x\in
t_{1}(a).\,\exists y\in t_{2}(a).(x,y)\in R\\}\,.$ (2)

Then, for an LTS $\gamma\colon X\rightarrow(\mathcal{P}_{\omega}X)^{A}$, the
greatest fixed point of the monotone map
$R\mapsto(\gamma\times\gamma)^{-1}\circ\overline{B}(R)$ is _similarity_. In
the same way, by varying the lifting $\overline{B}$, one can define many
different coinductive relations on $\mathsf{Set}$ coalgebras.

Yet a further generalisation is obtained by replacing $\mathsf{Set}$ by a
general category $\mathcal{C}$, and $\mathrm{Rel}$ by a category of
‘predicates’ on $\mathcal{C}$. A suitable categorical infrastructure for such
predicates on $\mathcal{C}$ is given by the notion of _fibration_. This allows
us, for instance, to move beyond (Boolean, binary) relations to quantitative
relations (e.g., behavioural metrics) or unary predicates. Such examples
follow in Section 4; also see, e.g., [HKC18, BPPR17].

To define fibrations, it will be useful to fix some associated terminology
first. Let $p\colon\mathcal{E}\rightarrow\mathcal{C}$ be a functor. If
$p(R)=X$, then we say $R$ is _above_ $X$, and similarly for morphisms. The
collection of all objects $R$ above a given object $X$ and arrows above the
identity $\mathsf{id}_{X}$ form a category, called the _fibre above $X$_ and
denoted by $\mathcal{E}_{X}$.

######  Definition .

A functor $p\colon\mathcal{E}\rightarrow\mathcal{C}$ is a _(poset) fibration_
if

  * •

each fibre $\mathcal{E}_{X}$ is a poset category (that is, at most one arrow
between every two objects); the corresponding order on objects is denoted by
$\leq$;

  * •

for every $f\colon X\rightarrow Y$ in $\mathcal{C}$ and object $S$ above $Y$
there is a _Cartesian morphism_ $\widetilde{f}_{S}\colon f^{*}(S)\rightarrow
S$ above $f$, with the property that for every arrow $g\colon Z\rightarrow X$,
every object $R$ above $Z$ and arrow $h\colon R\rightarrow S$ above $f\circ
g$, there is a unique arrow $k\colon R\rightarrow f^{*}(S)$ above $g$ such
that $\widetilde{f}_{S}\circ k=h$.

$\textstyle{R\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{k}$$\scriptstyle{h}$$\textstyle{f^{*}(S)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\widetilde{f}_{S}}$$\textstyle{S}$$\textstyle{Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g}$$\scriptstyle{f\circ
g}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\textstyle{Y}$

######  Remark .

In this paper we only consider poset fibrations, and refer to them simply as
fibrations. The usual definition of fibration is more general (e.g., [Jac99]):
normally, fibres are not assumed to be posets. Poset fibrations have several
good properties, mentioned below. In the application to coinductive
predicates, it is customary to work with poset fibrations.

For a morphism $f\colon X\rightarrow Y$, the assignment $R\mapsto f^{*}(R)$
gives rise to a functor$f^{*}\colon\mathcal{E}_{Y}\rightarrow\mathcal{E}_{X}$,
called _reindexing along $f$_. (Note that functors between poset categories
are just monotone maps.) We use a strengthening of poset fibrations, following
[SKDH18, KKH+19].

######  Definition .

A poset fibration $p\colon\mathcal{E}\rightarrow\mathcal{C}$ is called a
$\mathsf{CLat}_{\wedge}$-fibration if $(\mathcal{E}_{X},\leq)$ is a complete
lattice for every $X$, and reindexing preserves arbitary meets.

Any poset fibration $p$ is split: we have $(g\circ f)^{*}=f^{*}\circ g^{*}$
for any morphisms $f,g$ that compose. Further, $p$ is faithful. This captures
the intuition that morphisms in $\mathcal{E}$ are morphisms in $\mathcal{C}$
with a certain property; e.g., relation-preserving, or non-expansive (Examples
2.1, 2.1). We note that $\mathsf{CLat}_{\wedge}$-fibrations are instances of
topological functors [Her74]. We use the former, in line with existing related
work [HKC18, KKH+19]. This also has the advantage of keeping our results
amenable to possible future extensions to a wider class of examples.

######  Example .

Consider the _relation fibration_
$p\colon\mathrm{Rel}\rightarrow\mathsf{Set}$, where $p(R\subseteq X\times
X)=X$. Reindexing is given by inverse image: for a map $f\colon X\rightarrow
Y$ and a relation $S\subseteq Y\times Y$, we have $f^{*}(S)=(f\times
f)^{-1}(S)$. The functor $p$ is a $\mathsf{CLat}_{\wedge}$-fibration.

Closely related is the _predicate fibration_
$p\colon\mathrm{Pred}\rightarrow\mathsf{Set}$. An object of $\mathrm{Pred}$ is
a pair $(X,\Gamma)$ consisting of a set $X$ and a subset $\Gamma\subseteq X$,
and an arrow from $(X,\Gamma)$ to $(Y,\Theta)$ is a map $f\colon X\rightarrow
Y$ such that $x\in\Gamma$ implies $f(x)\in\Theta$. The functor $p$ is given by
$p(X,\Gamma)=X$, reindexing is given by inverse image, and $p$ is a
$\mathsf{CLat}_{\wedge}$-fibration as well.

In the relation fibration, we sometimes refer to an object $(X,R\subseteq
X^{2})$ simply by $R$, and similarly in the predicate fibration.

######  Example .

Let $\mathcal{V}$ be a complete lattice. Define the category
$\mathrm{Rel}_{\mathcal{V}}$ as follows: an object is a pair $(X,d)$ where $X$
is a set and a function $d\colon X\times X\rightarrow\mathcal{V}$, and a
morphism from $(X,d)$ to $(Y,e)$ is a map $f\colon X\rightarrow Y$ such that
$d(x,y)\leq e(f(x),f(y))$. The forgetful functor
$p\colon\mathrm{Rel}_{\mathcal{V}}\rightarrow\mathsf{Set}$ is a
$\mathsf{CLat}_{\wedge}$-fibration, where reindexing along $f\colon
X\rightarrow Y$ is given by $f^{*}(Y,e)=(X,e\circ f\times f)$.

For $\mathcal{V}=2=\\{0,1\\}$ with the usual order $0\leq 1$,
$\mathrm{Rel}_{\mathcal{V}}$ coincides with $\mathrm{Rel}$. Another example is
given by the closed interval $\mathcal{V}=[0,1]$, with the _reverse_ order.
Then, a morphism from $(X,d)$ to $(Y,e)$ is a _non-expansive map_ $f\colon
X\rightarrow Y$, that is, s.t. $e(f(x),f(y))\leq d(x,y)$ (with $\leq$ the
usual order, i.e., where $0$ is the smallest). This instance will be denoted
by $\mathrm{Rel}_{[0,1]}$.

#### Liftings and Coinductive Predicates

Let $p\colon\mathcal{E}\rightarrow\mathcal{C}$ be a fibration, and
$B\colon\mathcal{C}\rightarrow\mathcal{C}$ a functor. A functor
$\overline{B}\colon\mathcal{E}\rightarrow\mathcal{E}$ is called a _lifting_ of
$B$ if $p\circ\overline{B}=B\circ p$. In that case, $\overline{B}$ restricts
to a functor
$\overline{B}_{X}\colon\mathcal{E}_{X}\rightarrow\mathcal{E}_{BX}$, for any
$X$ in $\mathcal{C}$.

A lifting $\overline{B}$ of $B$ gives rise to an abstract notion of
coinductive predicate, as follows. For any $B$-coalgebra $(X,\gamma)$ there is
the functor, i.e., monotone function defined by
$\gamma^{*}\circ\overline{B}_{X}\colon\mathcal{E}_{X}\rightarrow\mathcal{E}_{X}$.
We think of post-fixed points of $\gamma^{*}\circ\overline{B}_{X}$ as
_invariants_ , generalising _bisimulations_. If $p$ is a
$\mathsf{CLat}_{\wedge}$-fibration, then $\gamma^{*}\circ\overline{B}_{X}$ has
a greatest fixed point $\nu(\gamma^{*}\circ\overline{B}_{X})$, which is also
the greatest post-fixed point. It is referred to as the _coinductive
predicate_ defined by $\overline{B}$ on $\gamma$.

######  Example .

First, for a $\mathsf{Set}$ functor
$B\colon\mathsf{Set}\rightarrow\mathsf{Set}$, recall the lifting
$\mathrm{Rel}(B)$ of $B$ defined in the beginning of this section. We refer to
$\mathrm{Rel}(B)$ as the _canonical relation lifting_ of $B$. For a coalgebra
$(X,\gamma)$, a post-fixed point of the operator
$\gamma^{*}\circ\mathrm{Rel}(B)_{X}$ is a bisimulation, as explained above.
The coinductive predicate $\nu(\gamma^{*}\circ\mathrm{Rel}(B)_{X})$ defined by
$\mathrm{Rel}(B)$ is bisimilarity. Another example is given by the lifting
$\overline{B}$ for similarity defined in the beginning of this section, which
we further study in Section 4. In that section we also define a unary
predicate, divergence, making use of the predicate fibration. Coinductive
predicates in the fibration $\mathrm{Rel}_{[0,1]}$ can be thought of as
_behavioural distances_ , providing a quantitative analogue of bisimulations,
measuring the distances between states. A simple example on deterministic
automata is studied in Section 4.1.

######  Remark .

In the quantitative examples, such as $\mathrm{Rel}_{[0,1]}$, one can replace
the latter with a category with more structure, such as the category of
pseudometrics and non-expansive maps. Similarly, one can replace
$\mathrm{Rel}$ with the category of equivalence relations. Defining liftings
then requires slightly more work, and since we use fibrations to define
coinductive predicates, this is not needed. Therefore, we do not use such
categories in our examples.

We sometimes need the notion of _fibration map_ : if $\overline{B}$ is a
lifting of $B$, the pair $(\overline{B},B)$ is called a fibration map if
$(Bf)^{*}\circ\overline{B}_{Y}=\overline{B}_{X}\circ f^{*}$ for any arrow
$f\colon X\rightarrow Y$ in $\mathcal{C}$. If $B$ preserves weak pullbacks,
then $(\mathrm{Rel}(B),B)$ is a fibration map [Jac16] in the relation
fibration (Example 2.1).

###  2.2. Coalgebraic Modal Logic

We recall a general duality-based approach to coalgebraic modal logic where we
work in the context of a contravariant adjunction [PMW06, Kli07, JS09] in
contrast to earlier work [KKP04, BK05a] that assumed a dual equivalence.

We assume the following setting, involving an adjunction $P\dashv Q$ and a
natural transformation $\delta\colon BQ\Rightarrow QL$:

$\textstyle{\mathcal{C}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{P}$$\scriptstyle{B}$$\textstyle{\bot}$$\textstyle{\mathcal{D}^{\mathsf{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Q}$$\scriptstyle{L}$
with$\textstyle{BQ\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\delta}$$\textstyle{QL}$
(3)

In this context, a _logic_ for $B$-coalgebras is a pair $(L,\delta)$ as above.
The functor $L\colon\mathcal{D}\rightarrow\mathcal{D}$ represents the syntax
of the modalities. It is assumed to have an initial algebra $\alpha\colon
L\Phi\stackrel{{\scriptstyle\cong}}{{\rightarrow}}\Phi$, which represents the
set (or other structure) of formulas of the logic. The natural transformation
$\delta$ gives the one-step semantics. It can equivalently be presented in
terms of its _mate_ $\widehat{\delta}\colon LP\Rightarrow PB$, which is
perhaps more common in the literature. However, we will formulate adequacy and
expressiveness in terms of the current presentation of $\delta$.

Let $(X,\gamma)$ be a $B$-coalgebra. The semantics $\llbracket\\_\rrbracket$
of a logic $(L,\delta)$ arises by initiality of $\alpha$, making use of the
mate $\widehat{\delta}$, as the unique map making the diagram on the left
below commute.

$\textstyle{L\Phi\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{L\llbracket\\_\rrbracket}$$\scriptstyle{\alpha}$$\textstyle{LPX\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\widehat{\delta}}$$\textstyle{PBX\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{P\gamma}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathit{th}}$$\scriptstyle{\gamma}$$\textstyle{Q\Phi\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Q\alpha}$$\textstyle{\Phi\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\exists!\llbracket\\_\rrbracket}$$\textstyle{PX}$$\textstyle{BX\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{B\mathit{th}}$$\textstyle{BQ\Phi\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\delta}$$\textstyle{QL\Phi}$

The _theory map_ $\mathit{th}\colon X\rightarrow Q\Phi$ is defined as the
transpose of $\llbracket\\_\rrbracket$, i.e.,
$\mathit{th}=Q\llbracket\\_\rrbracket\circ\eta_{X}$ where
$\eta\colon\mathsf{Id}\rightarrow QP$ is the unit of the adjunction $P\dashv
Q$. It is the unique map making the diagram on the right above commute.

######  Example .

Let $\mathcal{C}=\mathcal{D}=\mathsf{Set}$, $P=Q=2^{-}$ the contravariant
powerset functor, and $BX=2\times X^{A}$. We define a simple logic for
$B$-coalgebras, where formulas are just words over $A$. To this end, let
$LX=A\times X+1$. The initial algebra of $L$ is the set $A^{*}$ of words.
Define $\delta\colon BQ\Rightarrow QL$ on a component $X$ as follows:

$\delta_{X}\colon 2\times(2^{X})^{A}\rightarrow 2^{A\times
X+1}\qquad\delta_{X}(o,t)(u)=\begin{cases}o&\text{ if }u=\ast\in 1\\\
t(a)(x)&\text{ if }u=(a,x)\in A\times X\end{cases}$

For a coalgebra $\langle o,t\rangle\colon X\rightarrow 2\times X^{A}$, the
associated theory map $\mathit{th}\colon X\rightarrow 2^{A^{*}}$ is given by
$\mathit{th}(x)(\varepsilon)=o(x)$ and
$\mathit{th}(x)(aw)=\mathit{th}(t(x)(a))(w)$ for all $x\in X$, $a\in A$, $w\in
A^{*}$. This is, of course, the usual semantics of deterministic automata.

In the above example, the logic does not contain propositional connectives;
this is reflected by the choice $\mathcal{D}=\mathsf{Set}$. Although it is
possible to include propositional connectives into the functor $L$ (cf. e.g.
[Kli07]), one usually adds those connectives by choosing $\mathcal{D}$ to be a
category of algebras. For instance, Boolean algebras are a standard choice for
propositional logic, and in Section 4 we use the category of semilattices to
represent conjunction. In fact, if one is only interested in defining the
semantics of the logic, one can simply work with algebras for a signature;
this is supported by the adjunctions presented in the next subsection. We
outline in the next subsection how this can be used to represent the
propositional part of a real-valued modal logic.

###  2.3. Contravariant Adjunctions

In this subsection we discuss several adjunctions that we use for presenting
coalgebraic logic as above, and will allow us in Section 4 to demonstrate that
a large variety of concrete examples is covered by our framework. In all
cases, the adjunctions that we use for the logic are generated by an object
$\Omega$ of ‘truth values’. In fact, we believe all of the dual adjunctions
listed in this section are instances of the so-called concrete dualities from
[PT91] where $\Omega$ is the dualising object inducing the adjunction.

For a simple but useful class of such adjunctions, let $\mathcal{D}$ be a
category with products, and $\Omega$ an object in $\mathcal{D}$. Then there is
an adjunction

$P\dashv
Q\colon\mathsf{Set}\leftrightarrows\mathcal{D}^{\mathsf{op}}\qquad\text{ where
}PX=\Omega^{X}\text{ and }QX=\mathrm{Hom}(X,\Omega)\,,$ (4)

where $\Omega^{X}$ is the $X$-fold product of $\Omega$.

This adjunction is instrumental for representing the semantics of a
coalgebraic modal logic for $B$-coalgebras based on predicate liftings (cf.
e.g. [KP11]) within the dual adjunction framework by defining a suitable
category of $L$-algebras. In general, describing the category of $L$-algebras
that precisely represents a given logic (i.e., where the initial algebra
corresponds to the set of formulas modulo equivalence) is nontrivial. For
studying expressiveness, however, it is sufficient to consider formulas and
their semantics. This can be done as follows: We start by considering a set
$\mathcal{O}$ of propositional operators, each $o\in\mathcal{O}$ associated
with a certain finite arity $\mathrm{ar}(o)\in\mathbb{N}$ and define the
(propositional) signature functor

$\Sigma_{\mathcal{O}}\colon\mathsf{Set}\to\mathsf{Set}\qquad\mbox{by
putting}\qquad\Sigma_{\mathcal{O}}X\mathrel{:=}\coprod_{o\in\mathcal{O}}X^{\mathrm{ar}(o)}.$
(5)

The category $\mathrm{Alg}(\Sigma_{\mathcal{O}})$ of algebras for the functor
$\Sigma_{\mathcal{O}}$ will play the role of the category $\mathcal{D}$ in
(4). We assume that we are given a set of truth values $\Omega$ together with
a $\Sigma_{\mathcal{O}}$-algebra structure
$a_{\Omega}\colon\Sigma_{\mathcal{O}}\Omega\to\Omega$, which gives an
interpretation of the propositional operators. As $\Omega$ is a
$\Sigma_{\mathcal{O}}$-algebra we obtain functors
$P\colon\mathsf{Set}\to\mathrm{Alg}(\Sigma_{\mathcal{O}})^{\mathsf{op}}$ and
$Q\colon\mathrm{Alg}(\Sigma_{\mathcal{O}})^{\mathsf{op}}\to\mathsf{Set}$ as
described in (4). An $\Omega$-valued coalgebraic modal logic
$\mathcal{L}(\Lambda)$ for a functor $B\colon\mathsf{Set}\to\mathsf{Set}$ is
now given as a set $\Lambda$ of modal operators where each $\lambda\in\Lambda$
is an $\Omega$-valued predicate lifting $\lambda\colon P^{n}\Rightarrow PB$
with $\mathrm{ar}(\lambda)=n$ the arity of $\lambda$. Given
$\mathcal{L}(\Lambda)$ we define
$L_{\Lambda}\colon\mathrm{Alg}(\Sigma_{\mathcal{O}})\to\mathrm{Alg}(\Sigma_{\mathcal{O}})$
by putting

$L_{\Lambda}A\mathrel{:=}T_{\Sigma_{\mathcal{O}}}\left(\\{[\lambda](a_{1},\dots,a_{n})\mid\lambda\in\Lambda,n=\mathrm{ar}(\lambda),a_{j}\in
A\mbox{ for }1\leq j\leq n\\}\right)$

where $[\lambda](a_{1},\dots,a_{n})$ should be understood as name of a
generator and where $T_{\Sigma_{\mathcal{O}}}$ denotes the free (term) monad
over $\Sigma_{\mathcal{O}}$. The action of $L_{\mathcal{L}}$ on a given
morphism $f\colon A\to B$ is defined to be the unique
$\mathrm{Alg}(\Sigma_{\mathcal{O}})$-morphism extending the map
$[\lambda_{i}](a_{1},\ldots,a_{n})\mapsto[\lambda_{i}](f(a_{1}),\ldots,f(a_{n}))$.
It is now easy to see that the predicate liftings in $\Lambda$ give rise to a
natural transformation $\widehat{\delta}\colon L_{\Lambda}P\Rightarrow PB$
where, for an arbitrary set $X$, the $X$ component $\widehat{\delta}_{X}\colon
L_{\Lambda}PX\to PBX$ is the unique extension of the map

$[\lambda](u_{1},\ldots,u_{n})\mapsto\lambda(u_{1},\ldots,u_{n})$

for $\lambda\in\Lambda$, $n=\mathrm{ar}(\lambda)$ and $u_{j}\in\Omega^{X}$ for
$1\leq j\leq n$. In other words, $(L_{\Lambda},\delta)$ with $\delta$ being
the mate of $\widehat{\delta}$ is a logic for $B$-coalgebras in the sense of
(3). We arrive at the following picture:

$\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
35.72488pt\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 3.0pt\raise
0.0pt\hbox{$\textstyle{\mathsf{Set}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}\ignorespaces\ignorespaces{\hbox{\kern
28.7363pt\raise 12.15373pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.82222pt\hbox{$\scriptstyle{P=\Omega^{-}}$}}}\kern
3.0pt}}}}}}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern
71.73296pt\raise 4.77687pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{}{}{{}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{}{{}{{}{{}{{}{{}{{}}{}{{}{{}}{}{{}}{}{{}}{}{{}{{}{{}}}}}}}}}}{}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{}{{}}{{}{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{}{{}{{}}}\ignorespaces\ignorespaces{\hbox{\kern-35.72488pt\raise
0.0pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern 0.0pt\raise-2.39166pt\hbox{$\scriptstyle{B}$}}}\kern
3.0pt}}}}}}\ignorespaces{}{}{}{}{{}{{}}{}{{}}{}{{}}{}{{}{{}}{}{{}}{}{{}}{}{{}{{}{{}{{}{{}}}}}}}}{\hbox{\kern-9.94829pt\raise
4.27873pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{}{}{{}}{{}{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}{}}{}}}}\ignorespaces{}{\hbox{\kern
33.94446pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise 0.0pt\hbox{$\textstyle{\bot}$}}}}}}}{\hbox{\kern 71.72226pt\raise
0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\mathrm{Alg}(\Sigma_{\mathcal{O}})^{\mathsf{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}\ignorespaces\ignorespaces{\hbox{\kern
18.57426pt\raise-15.01973pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{Q=\mathrm{Hom}(-,\Omega)}$}}}\kern
3.0pt}}}}}}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern
9.16089pt\raise-3.00137pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{}{}{{}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{}{{}{{}{{}{{}{{}}{}{{}{{}{{}{{}{{}}{}{{}{{}}{}{{}}}}}}}}}}}{}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{}{{}}{{}{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{}{{}{{}}}\ignorespaces\ignorespaces{\hbox{\kern
132.7043pt\raise 0.0pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.70833pt\hbox{$\scriptstyle{L_{\Lambda}}$}}}\kern
3.0pt}}}}}}\ignorespaces{}{}{}{}{{}{{}}{}{{}}{}{{}}{}{{}{{}}{}{{}}{}{{}}{}{{}}{}{{}{{}}{}{{}{{}}}}}}{\hbox{\kern
118.26602pt\raise-4.04694pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{}{}{{}}{{}{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{}{{}}{{}{}{}{}}{}}}}\ignorespaces{}\ignorespaces}}}}\ignorespaces\hskip
42.67912pt\delta\colon BQ\Rightarrow QL_{\Lambda}$ (6)

######  Example .

To illustrate the outlined approach, consider the real-valued coalgebraic
modal logics from [KM18]. The set $\Phi$ of formulas of these logics is given
by the following definition that is indexed by a set $\Lambda$ of unary modal
operators:

$\Phi::=\top\mid[\lambda]\varphi,\lambda\in\Lambda\mid\min(\varphi_{1},\varphi_{2})\mid\neg\varphi\mid\varphi\ominus
q,q\in\mathbb{Q}\cap[0,\top]$

where $[0,\top]$ is a closed interval of real numbers with $\top$ denoting an
arbitrary positive real number, $\ominus$ is interpreted as truncated
subtraction on $[0,\top]$ given by $p\ominus q\mathrel{:=}\max(p-q,0)$, $\min$
is interpreted as minimum and negation on $[0,\top]$ is defined as $\neg
q\mathrel{:=}\top-q$. Following the construction of $L_{\Lambda}$ as described
above, we obtain the following dual adjunction:

$\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
35.72488pt\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 3.0pt\raise
0.0pt\hbox{$\textstyle{\mathsf{Set}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}\ignorespaces\ignorespaces{\hbox{\kern
23.57874pt\raise 13.19594pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.18056pt\hbox{$\scriptstyle{P=[0,\top]^{-}}$}}}\kern
3.0pt}}}}}}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern
71.73201pt\raise 5.1323pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{}{}{{}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{}{{}{{}{{}{{}{{}{{}}{}{{}{{}}{}{{}}{}{{}}{}{{}{{}{{}}}}}}}}}}{}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{}{{}}{{}{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{}{{}{{}}}\ignorespaces\ignorespaces{\hbox{\kern-35.72488pt\raise
0.0pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern 0.0pt\raise-2.39166pt\hbox{$\scriptstyle{B}$}}}\kern
3.0pt}}}}}}\ignorespaces{}{}{}{}{{}{{}}{}{{}}{}{{}}{}{{}{{}}{}{{}}{}{{}}{}{{}{{}{{}{{}{{}}}}}}}}{\hbox{\kern-9.94829pt\raise
4.27873pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{}{}{{}}{{}{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}{}}{}}}}\ignorespaces{}{\hbox{\kern
33.94446pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise 0.0pt\hbox{$\textstyle{\bot}$}}}}}}}{\hbox{\kern 71.72226pt\raise
0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\mathrm{Alg}(\Sigma_{[0,\top]})^{\mathsf{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}\ignorespaces\ignorespaces{\hbox{\kern
12.09914pt\raise-14.90155pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{Q=\mathrm{Hom}(-,[0,\top])}$}}}\kern
3.0pt}}}}}}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern
9.52094pt\raise-3.00137pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{}{}{{}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{}{{}{{}{{}{{}{{}}{}{{}{{}{{}}{}{{}}{}{{}}{}{{}{{}}}}}}}}}{}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{}{{}}{{}{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{}{{}{{}}}\ignorespaces\ignorespaces{\hbox{\kern
139.42432pt\raise 0.0pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.70833pt\hbox{$\scriptstyle{L_{\Lambda}}$}}}\kern
3.0pt}}}}}}\ignorespaces{}{}{}{}{{}{{}}{}{{}}{}{{}}{}{{}{{}}{}{{}}{}{{}{{}{{}{{}}{}{{}}{}{{}{{}}}}}}}}{\hbox{\kern
125.73013pt\raise-4.57147pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{}{}{{}}{{}{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{}{{}}{{}{}{}{}}{}}}}\ignorespaces{}\ignorespaces}}}}\ignorespaces.$

Here the operations on $[0,\top]$ are $\top$, $\min$, $\neg$ and $-\ominus q$
for $q\in\mathbb{Q}\cap[0,\top]$, thus

$\Sigma_{[0,\top]}X=1+X^{2}+X+X\times(\mathbb{Q}\cap[0,\top])\quad\mbox{ and
}\quad L_{\Lambda}(A)=T_{\Sigma_{[0,\top]}}(\\{[\lambda]a\mid a\in
A,\lambda\in\Lambda\\}).$

To study expressiveness relative to a coinductive predicate in a fibration
$p\colon\mathcal{E}\to\mathcal{C}$ we rely on a given dual adjunction $P\dashv
Q$ between $\mathcal{C}$ and $\mathcal{D}$ together with its lifted version
$\overline{P}\dashv\overline{Q}$ between $\mathcal{E}$ and $\mathcal{D}$. In a
large class of examples the fibration under consideration will be of type
$p\colon\mathrm{Rel}_{\mathcal{V}}\to\mathsf{Set}$ with $P\dashv Q$ being the
dual adjunction between $\mathsf{Set}$ and $\mathrm{Alg}(\Sigma)$ described
above. We will now provide a proposition that yields the required dual
adjunction $\overline{P}\dashv\overline{Q}$ between
$\mathrm{Rel}_{\mathcal{V}}$ and $\mathrm{Alg}(\Sigma)$. To obtain this dual
adjunction we need a number of assumptions. First we make some assumptions on
the truth and distance values $\Omega$ and $\mathcal{V}$:

  * •

$\mathcal{V}$ is a complete lattice of distance values,

  * •

$\Omega$ is a bounded poset of truth values,

  * •

$(\Omega,R_{\Omega}\colon\Omega\times\Omega\to\mathcal{V})\in\mathrm{Rel}_{\mathcal{V}}$.

Furthermore we let
$\Delta\colon\mathsf{Set}\rightarrow\mathrm{Rel}_{\mathcal{V}}$ be the
diagonal functor given by $\Delta X=\Delta_{X}$ where

$\displaystyle\Delta_{X}(x_{1},x_{2})$ $\displaystyle\mathrel{:=}$
$\displaystyle\left\\{\begin{array}[]{ll}\top&\mbox{ if }x_{1}=x_{2}\\\
\perp&\mbox{ otherwise.}\end{array}\right.$

######  Proposition .

Let $\Omega$ and $\mathcal{V}$ be sets of truth and distance values that
satisfy the above assumptions and let
$\Sigma\colon\mathsf{Set}\to\mathsf{Set}$ be a functor. Suppose furthermore
that $\Sigma$ has a lifting
$\overline{\Sigma}\colon\mathrm{Rel}_{\mathcal{V}}\to\mathrm{Rel}_{\mathcal{V}}$
such that (i) $\Delta\circ\Sigma\leq\overline{\Sigma}\circ\Delta$ and (ii) for
any $(X,R),(Y,S)\in\mathrm{Rel}_{\mathcal{V}}$ there is a morphism
$\overline{\mathrm{st}}_{R,S}\colon
R\times\overline{\Sigma}S\to\overline{\Sigma}(R\times S)$ above the strength
map $\mathrm{st}_{X,Y}\colon X\times\Sigma Y\to\Sigma(X\times Y)$ (the latter
exists for any set functor $\Sigma$). If $\overline{\Sigma}R_{\Omega}\leq
a_{\Omega}^{*}(R_{\Omega})$, then there is a dual adjunction

$\textstyle{\mathrm{Rel}_{\mathcal{V}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathrm{Hom}(\\_,R_{\Omega})}$$\textstyle{\bot}$$\textstyle{\mathrm{Alg}(\Sigma)^{\mathsf{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathrm{Hom}(\\_,a_{\Omega})}$
(8)

###### Proof.

We first have to show that the functors that form the adjunction are well-
defined. In the following we write $\alpha$ as abbreviation for an algebra
$(A,\alpha)$. Throughout this proof we denote the least and the largest
element of $\mathcal{V}$ by $\perp$ and $\top$, respectively. Recall that the
condition for a function $f$ to be a $\mathrm{Rel}_{\mathcal{V}}$-morphism is
$R_{1}(x_{1},x_{2})\leq R_{2}(fx_{1},fx_{2})$.

To see that the functors are well-defined on objects, first note that for each
$\Sigma$-algebra $(A,\alpha)$, the set $\mathrm{Hom}(\alpha,a_{\Omega})$ can
be turned into a $\mathrm{Rel}_{\mathcal{V}}$-object by defining

$\displaystyle
R_{\mathrm{Hom}(\alpha,a_{\Omega})}\colon\mathrm{Hom}(\alpha,a_{\Omega})\times\mathrm{Hom}(\alpha,a_{\Omega})$
$\displaystyle\to$ $\displaystyle\mathcal{V}$ $\displaystyle(h_{1},h_{2})$
$\displaystyle\mapsto$ $\displaystyle\bigwedge_{a\in
A}R_{\Omega}(h_{1}(a),h_{2}(a)).$

Likewise, for each $\mathrm{Rel}_{\mathcal{V}}$-object $(X,R)$, the set
$\mathrm{Hom}(R,R_{\Omega})$ carries a $\Sigma$-algebra structure
$a_{R}\colon\Sigma\mathrm{Hom}(R,R_{\Omega})\to\mathrm{Hom}(R,R_{\Omega})$
given by the function that maps $t\colon 1\to\Sigma\mathrm{Hom}(R,R_{\Omega})$
to the following composition of arrows:

$\textstyle{R\cong R\times
1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{id}\times
t}$$\textstyle{R\times\Delta\Sigma
D\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\leq}$$\textstyle{R\times\overline{\Sigma}\Delta
D\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{\mathrm{st}}_{R,\Delta
D}}$$\textstyle{\overline{\Sigma}(R\times\Delta
D)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{\Sigma}\mathrm{ev}}$$\textstyle{\overline{\Sigma}R_{\Omega}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{a_{\Omega}}}$$\textstyle{R_{\Omega}}$

where $D=\mathrm{Hom}(R,R_{\Omega})$ and where $\mathrm{ev}(x,f)=f(x)$ is the
evaluation function. To see that the above is a well-defined
$\mathrm{Rel}_{V}$-morphism we only have to check that
$\mathrm{ev}\in\mathrm{Rel}_{\mathcal{V}}$ as the other arrows are morphisms
by our assumption that $\Sigma$ has a lifting
$\overline{\Sigma}\colon\mathrm{Rel}_{\mathcal{V}}\to\mathrm{Rel}_{\mathcal{V}}$
such that $\mathrm{st}$ and $a_{\Omega}$ become morphisms in
$\mathrm{Rel}_{\mathcal{V}}$. We now show that $\mathrm{ev}$ satisfies the
$\mathrm{Rel}_{\mathcal{V}}$ morphism condition. Consider two pairs
$(x_{1},f_{1}),(x_{2},f_{2})\in X\times\mathrm{Hom}(R,R_{\Omega})$. We
distinguish cases:

Case:

$f_{1}=f_{2}=f$ In this case we have

$\displaystyle R\times\Delta D((x_{1},f),(x_{2},f))$ $\displaystyle=$
$\displaystyle R(x_{1},x_{2})\wedge\top=R(x_{1},x_{2})$ $\displaystyle\leq$
$\displaystyle
R_{\Omega}(f(x_{1}),f(x_{2}))=R_{\Omega}(\mathrm{ev}(x_{1},f),\mathrm{ev}(x_{2},f)).$

Case:

$f_{1}\not=f_{2}$. Then

$R\times\Delta
D((x_{1},f_{1}),(x_{2},f_{2}))=R(x_{1},x_{2})\wedge\perp\;=\;\perp\;\leq\;R_{\Omega}(\mathrm{ev}(x_{1},f_{1}),\mathrm{ev}(x_{2},f_{2})).$

Too see that the $\mathrm{Hom}$-functors are well-defined on morphisms we
first check that $\mathrm{Hom}(\\_,a_{\Omega})$ maps algebra morphisms to
morphisms in $\mathrm{Rel}_{\mathcal{V}}$. To this aim consider an algebra
morphism $h\colon(A_{1},\alpha_{1})\to(A_{2},\alpha_{2})$ and
$g_{1},g_{2}\in\mathrm{Hom}(\alpha_{2},a_{\Omega})$. We calculate:

$\displaystyle R_{\mathrm{Hom}(\alpha_{2},a_{\Omega})}(g_{1},g_{2})$
$\displaystyle=$ $\displaystyle\bigwedge_{a\in
A_{2}}R_{\Omega}(g_{1}(a),g_{2}(a))\leq\bigwedge_{a^{\prime}\in
A_{1}}R_{\Omega}(g_{1}(h(a^{\prime})),g_{2}(h(a^{\prime})))$ $\displaystyle=$
$\displaystyle
R_{\mathrm{Hom}(\alpha_{1},a_{\Omega})}\left(\mathrm{Hom}(h,a_{\Omega})(g_{1}),\mathrm{Hom}(h,a_{\Omega})(g_{2})\right)$

We now check that the functor $\mathrm{Hom}(\\_,R_{\Omega})$ is well-defined
on morphisms as well. Let
$h\colon(X_{1},R_{1})\to(X_{2},R_{2})\in\mathrm{Rel}_{\mathcal{V}}$. We have
to show that
$\mathrm{Hom}(h,R_{\Omega})\colon\mathrm{Hom}(R_{2},R_{\Omega})\to\mathrm{Hom}(R_{1},R_{\Omega})$
is a $\Sigma$-algebra morphism.

We calculate:

$\displaystyle\mathrm{Hom}(h,R_{\Omega})(a_{\mathrm{Hom}(R_{2},R_{\Omega})}(t))$
$\displaystyle=$ $\displaystyle\mathrm{Hom}(h,R_{\Omega})(\lambda
x.a_{\Omega}\circ\Sigma\mathrm{ev}\circ\mathrm{st}(x,t))$ $\displaystyle=$
$\displaystyle\lambda
y.a_{\Omega}\circ\Sigma\mathrm{ev}\circ\mathrm{st}(h(y),t)$
$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny nat. of
$\mathrm{st}$}}}{{=}}$ $\displaystyle\lambda
y.a_{\Omega}\circ\Sigma\mathrm{ev}\circ\Sigma(h\times\mathsf{id})\circ\mathrm{st}(y,t)$
$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny(*)}}}{{=}}$
$\displaystyle\lambda
y.a_{\Omega}\circ\Sigma\mathrm{ev}\circ\Sigma(\mathsf{id}\times\mathrm{Hom}(h,R_{\Omega}))\circ\mathrm{st}(y,t)$
$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny nat. of
$\mathrm{st}$}}}{{=}}$ $\displaystyle\lambda
y.a_{\Omega}\circ\Sigma\mathrm{ev}\circ\mathrm{st}(y,\Sigma\mathrm{Hom}(h,R_{\Omega})(t))$
$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny Def.~{}of
$a_{\mathrm{Hom}(\dots)}$}}}{{=}}$ $\displaystyle
a_{\mathrm{Hom}(R_{1},R_{\Omega})}(\Sigma\mathrm{Hom}(h,R_{\Omega})(t))$

where (*) holds as the following diagram can be easily seen to commute in
$\mathsf{Set}$:

$\textstyle{X_{1}\times\mathrm{Hom}(X_{2},\Omega)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{h\times\mathsf{id}}$$\scriptstyle{\mathsf{id}\times\mathrm{Hom}(h,\Omega)}$$\textstyle{X_{1}\times\mathrm{Hom}(X_{1},\Omega)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathrm{ev}}$$\textstyle{X_{2}\times\mathrm{Hom}(X_{2},\Omega)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathrm{ev}}$$\textstyle{\Omega}$

This finishes the argument that the functors are well-defined. We will now
argue that they form an adjunction. We prove this by defining the unit and
counit of the adjunction satisfying the triangle identities.

For $(X,R)\in\mathrm{Rel}_{\mathcal{V}}$ we define the unit map
$\eta_{R}\colon R\to\mathrm{Hom}(\mathrm{Hom}(R,R_{\Omega}),a_{\Omega})$ by
putting $\eta_{R}(x)\mathrel{:=}\lambda f.f(x)$. Naturality of $\eta$ can be
easily checked (left to the reader), but well-definedness is not obvious. For
the latter we have to show that $\eta_{R}$ is a
$\mathrm{Rel}_{\mathcal{V}}$-morphism and that $\eta_{R}(x)$ is a
$\mathrm{Alg}(\Sigma)$-morphism for all $(X,R)\in\mathrm{Rel}_{\mathcal{V}}$
and all $x\in X$.

To see that $\eta_{R}$ is a $\mathrm{Rel}_{\mathcal{V}}$-morphism, consider
$x_{1},x_{2}\in X$.

$\displaystyle R(x_{1},x_{2})$ $\displaystyle\leq$
$\displaystyle\bigwedge_{f\in\mathrm{Hom}(R,R_{\Omega})}R_{\Omega}(f(x_{1}),f(x_{2}))=\bigwedge_{f\in\mathrm{Hom}(R,R_{\Omega})}R_{\Omega}(\eta_{R}(x_{1})(f),\eta_{R}(x_{2})(f))$
$\displaystyle=$ $\displaystyle
R_{\mathrm{Hom}(\mathrm{Hom}(R,R_{\Omega}),a_{\Omega})}(\eta_{R}(x_{1}),\eta_{R}(x_{2}))$

To check that $\eta_{R}(x)$ is a $\Sigma$-algebra morphism, we calculate

$\displaystyle(a_{\Omega}\circ\Sigma\eta_{R}(x))(t)$ $\displaystyle=$
$\displaystyle(a_{\Omega}\circ\Sigma(\lambda
f.f(x))(t)=(a_{\Omega}\circ\Sigma(\mathrm{ev}(x,\\_)))(t)$ $\displaystyle=$
$\displaystyle(a_{\Omega}\circ\Sigma(\mathrm{ev}\circ\mathrm{st}))(x,t)$
$\displaystyle=$ $\displaystyle\eta_{R}(x)\left(\lambda
x.(a_{\Omega}\circ\Sigma(\mathrm{ev}\circ\mathrm{st}))(x,t)\right)=\eta_{R}(x)\left(a_{\mathrm{Hom}(R,R_{\Omega})}(t)\right)$

For the counit of the (dual) adjunction we define
$\epsilon_{\alpha}\colon(A,\alpha)\to\mathrm{Hom}(\mathrm{Hom}(\alpha,a_{\Omega}),R_{\Omega})$
by putting $\epsilon_{\alpha}(a)\mathrel{:=}\lambda g.g(a)$ for all
$(A,\alpha)\in\mathrm{Alg}(\Sigma)$ and all $a\in A$. Again we leave it to the
reader to convince themselves that $\epsilon$ is natural. We have to check
well-definedness, i.e, we need to check that $\epsilon_{\alpha}(a)$ is a
$\mathrm{Rel}_{\mathcal{V}}$-morphism and that $\epsilon_{\alpha}$ is an
$\mathrm{Alg}(\Sigma)$-morphism.

To see that $\epsilon_{\alpha}(a)$ is a $\mathrm{Rel}_{\mathcal{V}}$-morphism
we consider $g_{1},g_{2}\in\mathrm{Hom}(\alpha,a_{\Omega})$:

$\displaystyle R_{\mathrm{Hom}(\alpha,a_{\Omega})}(g_{1},g_{2})$
$\displaystyle=$ $\displaystyle\bigwedge_{a^{\prime}\in
A}R_{\Omega}(g_{1}(a^{\prime}),g_{2}(a^{\prime}))\leq
R_{\Omega}(g_{1}(a),g_{2}(a))$ $\displaystyle=$ $\displaystyle
R_{\Omega}(\epsilon_{\alpha}(a)(g_{1}),\epsilon_{\alpha}(a)(g_{2}))$

To check that $\epsilon_{\alpha}$ is an $\mathrm{Alg}(\Sigma)$-morphism we
calculate:

$\displaystyle
a_{\mathrm{Hom}(\mathrm{Hom}(\alpha,a_{\Omega}),R_{\Omega})}\circ\Sigma\epsilon_{\alpha}(t)$
$\displaystyle=$ $\displaystyle(\lambda
g.(a_{\Omega}\circ\Sigma\mathrm{ev}\circ\mathrm{st})(g,\Sigma\epsilon_{\alpha}(t))$
$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny Def. of
$\mathrm{st}$}}}{{=}}$ $\displaystyle(\lambda
g.(a_{\Omega}\circ\Sigma\mathrm{ev}(g,\\_)))(\Sigma\epsilon_{\alpha}(t))$
$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny(+)}}}{{=}}$
$\displaystyle(\lambda g.(a_{\Omega}\circ\Sigma g))(t)$
$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny$g$ alg.~{}mor.}}}{{=}}$
$\displaystyle\lambda g.g(\alpha(t))=\epsilon_{\alpha}(\alpha(t))$

where (+) is an easy consequence of
$(\mathrm{ev}(g,\\_)\circ\epsilon_{\alpha})(a)=g(a)$ for all $a\in A$.

This finishes the definition of unit and counit of the adjunction - checking
the triangle equalities is a straightforward exercise. ∎

The following remark is obvious, but at the same time useful for concrete
examples.

######  Remark .

Let $\mathcal{C}$ be a full subcategory of $\mathrm{Rel}_{\mathcal{V}}$ and
$\mathcal{D}$ a full subcategory of $\mathrm{Alg}(\Sigma)$ such that
$\mathrm{Hom}(-,a_{\Omega})$ and $\mathrm{Hom}(-,R_{\Omega})$ restrict to
functors of type $\mathcal{D}\to\mathcal{C}$ and of type
$\mathcal{C}\to\mathcal{D}$, respectively. Then the dual adjunction from Prop.
2.3 restricts to a dual adjunction between $\mathcal{C}$ and $\mathcal{D}$.

The assumptions in Proposition 2.3 concerning existence of a suitable lifting
of $\Sigma$ are in particular met when the algebraic signature $\Sigma$ is
given by a polynomial functor.

######  Corollary .

Let $\Omega$ and $\mathcal{V}$ be sets of truth and distance values that
satisfy the assumptions from Prop. 2.3, let $\Sigma$ be a signature functor.
Then $\Sigma$ lifts to $\mathrm{Rel}_{\mathcal{V}}$ such that (i)
$\Delta\circ\Sigma\leq\overline{\Sigma}\circ\Delta$ and (ii) there is a
strength map $\overline{\mathrm{st}}_{R,S}$ above $\mathrm{st}_{X,Y}$.
Consequently, the dual adjunction
$\mathrm{Hom}(\\_,R_{\Omega})\dashv\mathrm{Hom}(\\_,a_{\Omega})$ from (8)
$\mathrm{Hom}(\\_,R_{\Omega})\dashv\mathrm{Hom}(a_{\Omega},\\_)$ exists if
$\overline{\Sigma}R_{\Omega}\leq a_{\Omega}^{*}(R_{\Omega})$.

###### Proof.

It is clear that the existence of the dual adjunction follows from Prop 2.3
once we establish that any polynomial functor $\Sigma$ has a lifting to
$\mathrm{Rel}_{\mathcal{V}}$ such that (i)
$\Delta\circ\Sigma\leq\overline{\Sigma}\circ\Delta$ and such that (ii) there
is a strength map $\overline{\mathrm{st}}_{R,S}$ above $\mathrm{st}_{X,Y}$ for
all
$R\in{(\mathrm{Rel}_{\mathcal{V}})}_{X},S\in{(\mathrm{Rel}_{\mathcal{V}})}_{Y}$.
In the following we prove this claim not only for signature functors but for
the collection of functors $\mathcal{F}$ generated by the following grammar:

$\mathcal{F}\mathrel{::=}A\in\mathsf{Set}\mid\mathsf{Id}\mid\prod_{j\in
J}\Sigma_{j}\mid\coprod_{j\in J}\Sigma_{j}$

where $J$ are arbitrary sets of indexes, $A$ denotes the constant functor and
$\mathsf{Id}\colon\mathsf{Set}\to\mathsf{Set}$ denotes the identity functor.
For a functor $\Sigma\in\mathcal{F}$ we will now inductively define the action
of its lifting
$\overline{\Sigma}\colon\mathrm{Rel}_{\mathcal{V}}\to\mathrm{Rel}_{\mathcal{V}}$
on objects while at the same time proving that for arbitrary
$R\in{(\mathrm{Rel}_{\mathcal{V}})}_{X},S\in{(\mathrm{Rel}_{\mathcal{V}})}_{Y}$
we have that there is a morphism $\overline{\mathrm{st}}_{R,S}\colon
R\times\overline{\Sigma}S\to\overline{\Sigma}(R\times S)$ above the strength
map $\mathrm{st}_{X,Y}$.

Case:

$\Sigma=A$ (constant functor). Then we put

$(\overline{A}R)(a_{1},a_{2})\mathrel{:=}\left\\{\begin{array}[]{l}\top\qquad\mbox{if
}a_{1}=a_{2}\\\ \perp\qquad\mbox{otherwise.}\end{array}\right.$

The conditions on $\Delta$ and $\mathrm{st}$ are easy to check as in this case
$\Delta AX=\Delta_{A}=\overline{A}\Delta X$ and as $\mathrm{st}_{X,Y}(x,a)=a$
which clearly lifts to a suitable $\overline{\mathrm{st}}_{R,S}$.

Case:

$\Sigma=\mathsf{Id}$. Then $\overline{\Sigma}(R)=R$,
$\Delta\circ\Sigma=\Delta=\overline{\Sigma}\circ\Delta$ and the strength map
is simply the identity.

Case:

$\Sigma=\prod_{j\in J}\Sigma_{j}$. Then

$\overline{\Sigma}(R)(x_{1},x_{2})=\bigwedge_{j\in
J}\overline{\Sigma}_{j}(R)(\pi_{j}(x_{1}),\pi_{j}(x_{2}))$

where $\pi_{j}$ is the projection onto the $j$-th component of the product.
For proving property (i) we consider an arbitrary set $X$,
$x_{1},x_{2}\in\Sigma X$ and we calculate:

$\displaystyle\Delta\Sigma X(x_{1},x_{2})$ $\displaystyle=$
$\displaystyle\Delta\prod_{j\in
J}\Sigma_{j}X(x_{1},x_{2})\stackrel{{\scriptstyle\mbox{\tiny(*)}}}{{=}}\bigwedge_{j\in
J}\Delta(\Sigma_{j}X)(\pi_{j}(x_{1}),\pi_{j}(x_{2}))\stackrel{{\scriptstyle\mbox{\tiny
I.H.}}}{{\leq}}\bigwedge_{j\in J}\overline{\Sigma}_{j}(\Delta
X)(\pi_{j}(x_{1}),\pi_{j}(x_{2}))$ $\displaystyle=$
$\displaystyle\overline{\Sigma}(\Delta X)(x_{1},x_{2})$

To check that $\mathrm{st}\colon X\times\Sigma Y\to\Sigma(X\times Y)$
satisfies condition (ii) let $\mathrm{st}_{j}\colon
X\times\Sigma_{j}Y\to\Sigma_{j}(X\times Y)$ and consider two arbitrary pairs
$(x_{1},z_{1}),(x_{2},z_{2})\in X\times\Sigma Y$. We calculate:

$\displaystyle(R\times\overline{\Sigma}S)((x_{1},z_{1}),(x_{2},z_{2}))$
$\displaystyle=$ $\displaystyle R(x_{1},x_{2})\wedge\overline{S}(z_{1},z_{2})$
$\displaystyle=$
$\displaystyle\bigwedge\\{R(x_{1},x_{2})\\}\cup\\{\overline{\Sigma}_{j}S(\pi_{j}(z_{1}),\pi_{j}(z_{2}))\mid
j\in J\\}$ $\displaystyle=$ $\displaystyle\bigwedge_{j\in
J}\left\\{(R\times\overline{\Sigma}_{j}S)((x_{1},\pi_{j}(z_{1})),(x_{2},\pi_{j}(z_{2})))\right\\}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny I.H.}}}{{\leq}}$
$\displaystyle\bigwedge_{j\in J}\left\\{\overline{\Sigma}_{j}(R\times
S)(\mathrm{st}_{j}(x_{1},\pi_{j}(z_{1})),\mathrm{st}_{j}(x_{2},\pi_{j}(z_{2})))\right\\}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny(+)}}}{{=}}$
$\displaystyle\bigwedge_{j\in J}\left\\{\overline{\Sigma}_{j}(R\times
S)(\pi_{j}(\mathrm{st}(x_{1},z_{1})),\pi_{j}(\mathrm{st}(x_{2},z_{2})))\right\\}$
$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny Def.}}}{{=}}$
$\displaystyle\overline{\Sigma}(R\times
S)(\mathrm{st}(x_{1},z_{1}),\mathrm{st}(x_{2},z_{2}))$

where for (+) we used that
$\pi_{j}\circ\mathrm{st}=\mathrm{st}_{j}\circ(\mathsf{id}\times\pi_{j})$ as
can be easily checked.

Case:

$\Sigma=\coprod_{j\in J}\Sigma_{j}$. Then

$\overline{\Sigma}(R)(\kappa_{m}(x_{1}),\kappa_{n}(x_{2}))=\left\\{\begin{array}[]{l}\overline{\Sigma}_{n}(R)(x_{1},x_{2})\mbox{
if }n=m\\\ \perp\mbox{ otherwise.}\end{array}\right.$

where the $\kappa_{n}$ denotes the $n$-th inclusion into the coproduct. As in
the previous case we first verify (i): let $X$ be a set and consider
$x_{1},x_{2}\in\Sigma X$. W.l.o.g. we assume there are $j\in J$ and
$x_{1}^{\prime},x_{2}^{\prime}\in\Sigma_{j}X$ with
$x_{i}=\kappa_{j}(x_{i}^{\prime})$ for $i=1,2$ \- otherwise property (i) is
trivially satisfied. Spelling out the definitions we get

$\displaystyle\Delta(\Sigma X)(x_{1},x_{2})$ $\displaystyle=$
$\displaystyle\Delta(\Sigma_{j}X)(x_{1}^{\prime},x_{2}^{\prime})\stackrel{{\scriptstyle\mbox{\tiny
I.H.}}}{{\leq}}\overline{\Sigma}_{j}(\Delta
X)(x_{1}^{\prime},x_{2}^{\prime})=\overline{\Sigma}(\Delta X)(x_{1},x_{2})$

Let $\mathrm{st}_{j}\colon X\times\Sigma_{j}Y\to\Sigma_{j}(X\times Y)$ be the
strength maps of the components of $\Sigma$. Consider pairs
$(x_{1},\kappa_{j}(y_{1})),(x_{2},\kappa_{j}(y_{2}))\in X\times\Sigma Y$ where
we assumed that the $y_{i}$’s are from the same $j$-th component of $\Sigma Y$
\- otherwise the strength condition is trivially true. We calculate:

$\displaystyle(R\times\overline{\Sigma}S)((x_{1},\kappa_{j}(y_{1})),(x_{2},\kappa_{j}(y_{2})))$
$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny Def of
$\overline{\Sigma}$}}}{{=}}$
$\displaystyle(R\times\overline{\Sigma}_{j}S)((x_{1},y_{1}),(x_{2},y_{2}))$
$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny I.H.}}}{{\leq}}$
$\displaystyle\overline{\Sigma}_{j}(\mathrm{st}_{j}(x_{1},y_{1}),\mathrm{st}_{j}(x_{2},y_{2}))$
$\displaystyle=$ $\displaystyle\overline{\Sigma}(R\times
S)(\kappa_{j}(\mathrm{st}_{j}(x_{1},y_{1})),\kappa_{j}(\mathrm{st}_{j}(x_{2},y_{2})))$
$\displaystyle=$ $\displaystyle\overline{\Sigma}(R\times
S)(\mathrm{st}(x_{1},\kappa_{j}(y_{1})),\mathrm{st}(x_{2},\kappa_{j}(y_{2})))$

where the last equality follows from the easily verifiable fact that
$\kappa_{j}\circ\mathrm{st}_{j}=\mathrm{st}\circ(\mathsf{id}\times\kappa_{j})$.

This finishes both the definition of $\overline{\Sigma}$ on objects - it is
now a routine exercise to extend $\overline{\Sigma}$ to a functor. Furthermore
we proved that for polynomial functors $\Sigma$, the map $\mathrm{st}$ lifts
to $\mathrm{Rel}_{\mathcal{V}}$ as required. ∎

Let $\mathcal{L}(\Lambda)$ be a coalgebraic modal logic for some functor $B$
and its representation via a dual adjunction from $\mathsf{Set}$ to
$\mathrm{Alg}(\Sigma_{\mathcal{O}})$ for some polynomial functor
$\Sigma_{\mathcal{O}}$ together with a functor
$L_{\Lambda}\colon\mathrm{Alg}(\Sigma_{\mathcal{O}})\to\mathrm{Alg}(\Sigma_{\mathcal{O}})$
as in (6). Furthermore let
$a_{\Omega}\colon\Sigma_{\mathcal{O}}\Omega\to\Omega$ the algebra structure
induced by the propositional operators $\mathcal{O}$ of $\mathcal{L}(\Lambda)$
such that for all operations $o\in O$ and all
$v_{1},\dots,v_{n},v_{1}^{\prime},\dots,v_{n}^{\prime}\in\Omega$ we have

$\bigwedge_{1\leq i\leq n}R_{\Omega}(v_{i},v_{i}^{\prime})\leq
R_{\Omega}\left(o(v_{1},\dots,v_{n}),o(v_{1}^{\prime},\dots,v_{n}^{\prime})\right).$

Then the results of this section can be summarised in the following diagram:

$\textstyle{\mathrm{Rel}_{\mathcal{V}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{B}}$$\scriptstyle{p}$$\scriptstyle{\overline{P}}$$\textstyle{\mathsf{Set}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{P}$$\scriptstyle{B}$$\textstyle{\bot}$$\textstyle{\mathrm{Alg}(\Sigma_{\Omega})^{\mathsf{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Q}$$\scriptstyle{\overline{Q}}$$\scriptstyle{L_{\Lambda}}$
with$\textstyle{BQ\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\delta}$$\textstyle{QL_{\Lambda}}$

In the next section we will see that adequacy of the logic
$\mathcal{L}(\Lambda)$ follows if $\delta$ lifts to
$\overline{\delta}\colon\overline{B}\overline{Q}\Rightarrow\overline{Q}L_{\Lambda}$,
while expressiveness is implied by an additional property of
$\overline{\delta}$.

##  3\. Abstract Framework: Adequacy & Expressiveness

In this section, we define when a logic is adequate and expressive with
respect to a coinductive predicate, and provide sufficient conditions on the
logic. Coinductive predicates are expressed abstractly via fibrations and
functor lifting, and logic via a contravariant adjunction. Therefore, we make
the following assumptions.

######  Assumption .

Throughout this section, we assume:

  1. (1)

_(Type of coalgebra)_ An endofunctor
$B\colon\mathcal{C}\rightarrow\mathcal{C}$ on a category $\mathcal{C}$;

  2. (2)

_(Coinductive predicate)_ A $\mathsf{CLat}_{\wedge}$-fibration
$p\colon\mathcal{E}\rightarrow\mathcal{C}$ and a lifting
$\overline{B}\colon\mathcal{E}\rightarrow\mathcal{E}$ of $B$;

  3. (3)

_(Coalgebraic logic)_ An adjunction $P\dashv
Q\colon\mathcal{C}\leftrightarrows\mathcal{D}^{\mathsf{op}}$, a functor
$L\colon\mathcal{D}\rightarrow\mathcal{D}$ with an initial algebra
$\alpha\colon L(\Phi)\stackrel{{\scriptstyle\cong}}{{\rightarrow}}\Phi$, and a
natural transformation $\delta\colon BQ\Rightarrow QL$.

As explained in the introduction, to formulate adequacy and expressiveness, we
need one more crucial ingredient: an object that stipulates how collections of
formulas should be compared. In the abstract fibrational setting, we assume an
object above $Q\Phi$; more systematically, a functor $\overline{Q}$ above $Q$.

######  Definition  (Adequacy and Expressiveness).

Let $\overline{Q}\colon\mathcal{D}^{\mathsf{op}}\rightarrow\mathcal{E}$ be a
functor such that $p\circ\overline{Q}=Q$. We say the logic $(L,\delta)$ is

  * •

_adequate_ if
$\nu(\gamma^{*}\circ\overline{B}_{X})\leq\mathit{th}^{*}(\overline{Q}\Phi)$
for every $B$-coalgebra $(X,\gamma)$;

  * •

_expressive_ if
$\nu(\gamma^{*}\circ\overline{B}_{X})\geq\mathit{th}^{*}(\overline{Q}\Phi)$
for every $B$-coalgebra $(X,\gamma)$.

When we need to refer to the functors $\overline{Q}$ or $\overline{B}$
explicitly, we speak about adequacy and expressiveness _via $\overline{Q}$_
_w.r.t. $\overline{B}$_. Examples follow in Section 3.2, where classical
expressiveness and adequacy w.r.t. bisimilarity is recovered, and Section 4,
where other instances are treated.

######  Remark .

Definition 3 can be generalised to arbitrary poset fibrations, not necessarily
assuming complete lattice structure on the fibres, as follows. Adequacy means
that for any $B$-coalgebra $(X,\gamma)$, if
$R\leq\gamma^{*}\circ\overline{B}_{X}(R)$ then
$R\leq\mathit{th}^{*}(\overline{Q}\Phi)$. Expressiveness means that for any
$B$-coalgebra $(X,\gamma)$, we have $\mathit{th}^{*}(\overline{Q}\Phi)\leq R$
for some $R$ with $R\leq\gamma^{*}\circ\overline{B}_{X}(R)$. In fact, with
these definitions, if $(L,\delta)$ is both adequate and expressive then
$\gamma^{*}\circ\overline{B}_{X}$ has a greatest fixed point, given by
$\mathit{th}^{*}(\overline{Q}\Phi)$. We prefer to work with
$\mathsf{CLat}_{\wedge}$-fibrations, since the definition is slightly simpler,
and it covers all our examples.

###  3.1. Sufficient conditions for expressiveness and adequacy

The results below give conditions on $\overline{B}$, $\overline{Q}$ and
primarily the one-step semantics $\delta$ that guarantee expressiveness
(Theorem 3.1) and adequacy (Theorem 3.1). For simplicity we fix the functor
$\overline{Q}$.

######  Assumption .

In the remainder of this section we assume a functor
$\overline{Q}\colon\mathcal{D}^{\mathsf{op}}\rightarrow\mathcal{E}$ such that
$p\circ\overline{Q}=Q$.

For adequacy, the main idea is to require sufficient conditions to lift
$\delta$ to a logic for $\overline{B}$.

######  Theorem .

Suppose that

  1. (1)

$\overline{B}\,\overline{Q}X\leq\delta_{X}^{*}(\overline{Q}LX)$ for every
object $X$ in $\mathcal{D}$, and

  2. (2)

the functor $\overline{Q}$ has a left adjoint.

Then $(L,\delta)$ is adequate.

###### Proof.

The first assumption yields a natural transformation
$\overline{\delta}\colon\overline{B}\,\overline{Q}\Rightarrow\overline{Q}L$,
defined on a component $X$ by

$\overline{\delta}_{X}=\left(\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
13.36804pt\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 3.0pt\raise
0.0pt\hbox{$\textstyle{\overline{B}\,\overline{Q}X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
37.36804pt\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
37.36804pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\delta_{X}^{*}(\overline{Q}LX)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
87.7664pt\raise 6.61111pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-3.61111pt\hbox{$\scriptstyle{\widetilde{\delta}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 105.54419pt\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
105.54419pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\overline{Q}LX}$}}}}}}}\ignorespaces}}}}\ignorespaces\right)$

where the left arrow is the inclusion
$\overline{B}\,\overline{Q}X\leq\delta_{X}^{*}(\overline{Q}LX)$, and the right
arrow $\widetilde{\delta}$ is the Cartesian morphism to $\overline{Q}LX$ above
$\delta_{X}$. It follows that $\overline{\delta}_{X}$ is above $\delta_{X}$.
Further, naturality follows from $p$ being faithful (as it is a poset
fibration, see Section 2.1) and naturality of $\delta$. Observe that we have
thus established $(L,\overline{\delta})$ as a logic for
$\overline{B}$-coalgebras, via the adjunction
$\overline{P}\dashv\overline{Q}$.

Now let $(X,\gamma)$ be a $B$-coalgebra, and
$R=\nu(\gamma^{*}\circ\overline{B}_{X})$. Then, in particular,
$R\leq\gamma^{*}\circ\overline{B}_{X}(R)$, which is equivalent to a coalgebra
$\overline{\gamma}\colon R\rightarrow\overline{B}R$ above $\gamma\colon
X\rightarrow BX$. The logic $(L,\overline{\delta})$ gives us a theory map
$\overline{\mathit{th}}$ of $(R,\overline{\gamma})$ as the unique map making
the following diagram commute.

$\textstyle{R\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{\mathit{th}}}$$\scriptstyle{\overline{\gamma}}$$\textstyle{\overline{Q}\Phi\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{Q}\alpha}$$\textstyle{\overline{B}R\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{B}\,\overline{\mathit{th}}}$$\textstyle{\overline{B}\,\overline{Q}\Phi\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{\delta}}$$\textstyle{\overline{Q}L\Phi}$

Since $p\circ\overline{Q}=Q$ and $p(\overline{\delta}_{\Phi})=\delta_{\Phi}$,
it follows that $p(\overline{\mathit{th}})$ equals the theory map
$\mathit{th}$ of $(X,\gamma)$. Hence $R\leq\mathit{th}^{*}(\overline{Q}\Phi)$
as required. ∎

Expressiveness requires the converse inequality of the one in Theorem 3.1, but
only on one component: the carrier $\Phi$ of the initial algebra. Further, the
conditions include that $(\overline{B},B)$ is a fibration map. In particular,
for the canonical relation lifting $\mathrm{Rel}(B)$ this means that $B$
should preserve weak pullbacks; this case is explained in more detail in
Section 3.2.

######  Lemma .

Let $\iota\colon X\stackrel{{\scriptstyle\cong}}{{\rightarrow}}Y$ be an
isomorphism in $\mathcal{D}$. Then
$Q(\iota^{-1})^{*}(\overline{Q}Y)=\overline{Q}X$.

###### Proof.

Since $p\circ\overline{Q}=Q$, we have that
$\overline{Q}(\iota^{-1})\colon\overline{Q}X\rightarrow\overline{Q}Y$ is above
$Q(\iota^{-1})$, and hence $\overline{Q}X\leq
Q(\iota^{-1})^{*}(\overline{Q}Y)$ by the latter’s universal property. For the
converse, consider the following composition, where the left-hand side is the
Cartesian morphism:

$\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
26.74748pt\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 3.0pt\raise
0.0pt\hbox{$\textstyle{Q(\iota^{-1})^{*}(\overline{Q}Y)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
38.7037pt\raise 7.74667pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.47557pt\hbox{$\scriptstyle{\widetilde{Q\iota^{-1}}_{\overline{Q}Y}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 69.4266pt\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
69.4266pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\overline{Q}Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
103.31558pt\raise 5.83888pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.83888pt\hbox{$\scriptstyle{\overline{Q}\iota}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 131.13353pt\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
131.13353pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\overline{Q}X}$}}}}}}}\ignorespaces}}}}\ignorespaces\,.$

This sits above the identity on $QY$:
$p(\overline{Q}(\iota)\circ\widetilde{Q\iota^{-1}}_{\overline{Q}Y}=p(\overline{Q}(\iota))\circ
p(\widetilde{Q\iota^{-1}}_{\overline{Q}Y})=Q(\iota)\circ
Q(\iota^{-1})=\mathsf{id}$. Hence we get
$Q(\iota^{-1})^{*}(\overline{Q}Y)\leq\overline{Q}X$ as needed. ∎

######  Theorem .

Suppose $(\overline{B},B)$ is a fibration map. If
$\delta_{\Phi}^{*}(\overline{Q}L\Phi)\leq\overline{B}\,\overline{Q}\Phi$, then
$(L,\delta)$ is expressive.

###### Proof.

Let $(X,\gamma)$ be a $B$-coalgebra, with $\mathit{th}$ the associated theory
map. We show that $\mathit{th}^{*}(\overline{Q}\Phi)$ is a post-fixed point of
$\gamma^{*}\circ\overline{B}_{X}$:

$\displaystyle\mathit{th}^{*}(\overline{Q}\Phi)$
$\displaystyle=(Q(\alpha^{-1})\circ\delta_{\Phi}\circ
B\mathit{th}\circ\gamma)^{*}(\overline{Q}\Phi)$
$\displaystyle=\gamma^{*}\circ(B\mathit{th})^{*}\circ\delta_{\Phi}^{*}\circ
Q(\alpha^{-1})^{*}(\overline{Q}\Phi)$
$\displaystyle=\gamma^{*}\circ(B\mathit{th})^{*}\circ\delta_{\Phi}^{*}(\overline{Q}L\Phi)$
(Lemma 3.1)
$\displaystyle\leq\gamma^{*}\circ(B\mathit{th})^{*}(\overline{B}\,\overline{Q}\Phi)$
(assumption)
$\displaystyle=\gamma^{*}\circ\overline{B}_{X}\circ\mathit{th}^{*}(\overline{Q}\Phi)$
($(\overline{B},B)$ fibration map)

Expressiveness follows since $\nu(\gamma^{*}\circ\overline{B}_{X})$ is the
greatest post-fixed point. ∎

Note that in the above theorem the reference to the initial algebra $\Phi$
could be avoided by requiring that the inequality in the assumption holds for
arbitrary objects in $\mathcal{D}$. We opted for the above formulation
reflecting the fact that, whenever one is applying the theorem to concrete
instances, it is useful that one is able to focus on the initial $L$-algebra
only.

###  3.2. Adequacy and Expressiveness w.r.t. Behavioural Equivalence

In the setting of coalgebraic modal logic recalled in Section 2.2, Klin
[Kli07] proved that

  1. (1)

the theory map $\mathit{th}$ of a coalgebra $(X,\gamma)$ factors through
coalgebra morphisms from $(X,\gamma)$;

  2. (2)

if $\delta$ has monic components, then $\mathit{th}$ factors as a coalgebra
morphism followed by a mono.

The first item can be seen as adequacy w.r.t. behavioural equivalence (i.e.,
identification by a coalgebra morphism), and the second as expressiveness.
111For weak pullback preserving functors, behavioural equivalence coincides
with bisimilarity but for arbitrary set functors the latter can be a strictly
smaller relation.

In the current section we revisit this result for $\mathsf{Set}$ functors, as
a sanity check of Definition 3. To obtain the appropriate notion of adequacy
and expressiveness, we need to compare collections of formulas for equality.
Therefore, the functor $\overline{Q}$ in Definition 3 will be instantiated
with $\overline{Q}X=(QX,\Delta_{QX})$ where $\Delta_{QX}$ denotes the
diagonal. Then, for a coalgebra $(X,\gamma)$,
$\mathit{th}^{*}(\overline{Q}\Phi)$ is the set of all pairs of states $(x,y)$
such that $\mathit{th}(x)=\mathit{th}(y)$. Adequacy then means that for every
coalgebra $(X,\gamma)$, behavioural equivalence is contained in
$\mathit{th}^{*}(\overline{Q}\Phi)$, i.e., if $x$ is behaviourally equivalent
to $y$ then $\mathit{th}(x)=\mathit{th}(y)$. Expressiveness is the converse
implication.

We start with an abstract result, where the functor $\overline{Q}$ assigns the
equality relation (diagonal); thus this is specifically about capturing
(behavioural) equivalence logically. To state and prove it, let
$\Delta\colon\mathsf{Set}\rightarrow\mathrm{Rel}$ be the functor given by
$\Delta(X)=\Delta_{X}$. This functor has a left adjoint
$\mathsf{Quot}\colon\mathrm{Rel}\rightarrow\mathsf{Set}$, which maps a
relation $R\subseteq X\times X$ to the quotient of $X$ by the least
equivalence relation containing $R$ (cf. [HJ98]). This can be generalised to
the notion of fibration with quotients, see [Jac99], but we stick to
$\mathsf{Set}$ here.

######  Proposition .

Consider the relation fibration $p\colon\mathrm{Rel}\rightarrow\mathsf{Set}$,
let $B\colon\mathsf{Set}\rightarrow\mathsf{Set}$ be a functor with a lifting
$\overline{B}\colon\mathrm{Rel}\rightarrow\mathrm{Rel}$ which preserves
diagonals, that is, $\overline{B}\circ\Delta=\Delta\circ B$, and such that
$(\overline{B},B)$ is a fibration map.

Let $P\dashv Q\colon\mathsf{Set}\leftrightarrows\mathcal{D}^{\mathsf{op}}$ for
some category $\mathcal{D}$, $L\colon\mathcal{D}\rightarrow\mathcal{D}$ a
functor with an initial algebra and $\delta\colon BQ\Rightarrow QL$. Then

  1. (1)

$(L,\delta)$ is adequate w.r.t. $\overline{B}$;

  2. (2)

if $\delta$ is componentwise injective, then $(L,\delta)$ is expressive w.r.t.
$\overline{B}$,

via $\overline{Q}=\Delta\circ Q$.

###### Proof.

For adequacy, we use Theorem 3.1. By composition of adjoints,
$P\circ\mathsf{Quot}$ is a left adjoint to $\Delta\circ Q$. It will be useful
to simplify $\overline{B}\circ\Delta\circ QX$ and $\delta_{X}^{*}(\Delta\circ
Q\circ LX)$:

$\displaystyle\overline{B}\circ\Delta\circ QX$ $\displaystyle=\Delta_{BQX}\,,$
(9) $\displaystyle\delta_{X}^{*}(\Delta\circ Q\circ LX)$
$\displaystyle=(\delta_{X}\times\delta_{X})^{-1}(\Delta_{QLX})\,,$ (10)

using that $\overline{B}$ preserves diagonals in the first equality. The
remaining hypothesis of Theorem 3.1 is that $\overline{B}\circ\Delta\circ
QX\leq\delta_{X}^{*}(\Delta\circ Q\circ LX)$ for all $X$, i.e.,
$\Delta_{BQX}\subseteq(\delta_{X}\times\delta_{X})^{-1}(\Delta_{QLX})$, which
is trivial.

For expressiveness, we use Theorem 3.1. By assumption, $(\overline{B},B)$ is a
fibration map. We need to prove that $\delta_{\Phi}^{*}(\Delta\circ Q\circ
L\Phi)\leq\overline{B}\circ\Delta\circ Q\Phi$, which amounts to the inclusion

$(\delta_{\Phi}\times\delta_{\Phi})^{-1}(\Delta_{QL\Phi})\subseteq\Delta_{BQ\Phi}$

But this is equivalent to injectivity of $\delta_{\Phi}$. ∎

The canonical lifting $\mathrm{Rel}(B)$ of a $\mathsf{Set}$ functor $B$ always
preserves diagonals, and if $B$ preserves weak pullbacks, then it is a
fibration map. Thus, we obtain expressiveness w.r.t. bisimilarity for weak
pullback preserving functors, if $\delta$ has injective components.

In order to be able to cover a larger class of functors, and move to
behavioural equivalence, we use the notion of _lax extension_ preserving
diagonals.

######  Definition  ([MV15]).

Let $B\colon\mathsf{Set}\to\mathsf{Set}$ be a functor. An operation
$\widehat{B}$ associating with each relation $R\subseteq X\times Y$ a relation
$\widehat{B}\subseteq BX\times BY$ is called a lax extension of $B$ preserving
diagonals if for all relations $R$, $S$, all functions $f$ an all sets $X$ we
have

  1. (1)

$\widehat{B}(R^{\bullet})=(\widehat{B}R)^{\bullet}$ where $(\\_)^{\bullet}$
denotes the converse relation,

  2. (2)

$R\subseteq S$ implies $\widehat{B}R\subseteq\widehat{B}S$ (monotonicity),

  3. (3)

$\widehat{B}R;\widehat{B}S\subseteq\widehat{B}(R;S)$ (lax preservation of
relational composition),

  4. (4)

$\widehat{B}\mathrm{Gr}(f)=\mathrm{Gr}(Bf)$ and, in particular,
$\widehat{B}\Delta_{X}=\Delta_{BX}$ (preservation of diagonals).

Here for a function $f\colon X\to Y$ we we denote by $\mathrm{Gr}(f)$ its
graph relation:

$\mathrm{Gr}(f)=\\{(x,f(x))\mid x\in X\\}\subseteq X\times Y$

The following key fact is an immediate consequence of the results in [MV15].

######  Fact 1.

Let $B$ be a set functor and let $\widehat{B}$ be a lax extension of $B$
preserving diagonals. Then on any coalgebra $(X,\gamma)$ we have that
behavioural equivalence is equal to $\nu(\gamma^{*}\circ\widehat{B}_{X})$.

######  Proof 3.1 (Proof (Sketch)).

Monotonicity of $\widehat{B}$ implies that $\gamma^{*}\circ\widehat{B}_{X}$ is
a monotone operator. The result now follows from $\mathrm{Rel}_{X}$ being a
complete lattice and behavioural equivalence being the greatest post-fixpoint
of $\gamma^{*}\circ\widehat{B}_{X}$. The latter is a consequence of [MV15,
Prop. 9].

In particular, for a weak pullback preserving functor $B$, the canonical
lifting $\mathrm{Rel}(B)$ is a lax extension preserving diagonals. But the
results in [MV15] also show that non-weak pullback preserving set functors
have such lax extensions. In fact, any finitary functor for which an
expressive logic with “monotone” modalities exist, has a suitable lifting.
Examples include the so-called $(\\_)^{3}_{2}$-functor , the functor
$\mathcal{P}_{n}$ that maps a set $X$ to the collection $\mathcal{P}_{n}X$ of
subsets of $X$ with less than $n$ elements and the so-called monotone
neighbourhood functor (cf. Example 7 in [MV15]). The following proposition
establishes that the lax lifting $\widehat{B}$ fits into the fibrational
framework of our paper, and that Proposition 3.2 applies.

######  Proposition 3.2.

Let $B\colon\mathsf{Set}\to\mathsf{Set}$ be a functor and let $\widehat{B}$ be
a lax lifting of $B$ that preserves diagonals. Then
$\widehat{B}\colon\mathrm{Rel}\to\mathrm{Rel}$ is a lifting of $B$ along the
relation fibration $p\colon\mathrm{Rel}\to\mathsf{Set}$. In addition to that,
$(\widehat{B},B)$ is a fibration map.

######  Proof 3.3.

In order to turn $\widehat{B}$ into a functor $\mathrm{Rel}\to\mathrm{Rel}$ we
define $\widehat{B}(f)\mathrel{:=}Bf$ \- we will verify later in the proof
that the functor is well-defined. Now note that for all relations $R\subseteq
X\times X$ and functions $f\colon Y\to X$ we have

$\widehat{B}_{Y}(f^{*}(R)))=\widehat{B}_{Y}((f\times
f)^{-1}(R))\stackrel{{\scriptstyle\mbox{\tiny(*)}}}{{=}}(Bf\times
Bf)^{-1}(\widehat{B}_{X}(R))=(Bf)^{*}(\widehat{B}_{X}(R))$

where (*) is a well-known property of lax extensions (cf. e.g. Remark 4 in
[MV15]) and the other equalities follow from the definition of reindexing.
This implies that $(\widehat{B},B)$ is a fibration map once we establish that
$\widehat{B}$ is a lifting of $B$ along $p\colon\mathrm{Rel}\to\mathsf{Set}$.
For the latter we only need to verify that $\widehat{B}$ is a functor on
$\mathrm{Rel}$. To avoid confusion, please note that [MV15] uses a different
category $\mathrm{Rel}$ where the relations are morphisms whereas in our case
the relations are objects. In order to see that $\widehat{B}$ is well-defined
on $\mathrm{Rel}$-morphisms, consider relations $R\subseteq X\times X$,
$S\subseteq Y\times Y$ and a function $f\colon R\to S\in\mathrm{Rel}$. We need
to show that $\widehat{B}(f)\colon\widehat{B}(R)\to\widehat{B}(S)$. As
$\widehat{B}(f)=Bf$, we need to prove that $Bf$ is a $\mathrm{Rel}$-morphism
from $\widehat{B}(R)$ to $\widehat{B}(S)$. Consider an arbitrary pair
$(t_{1},t_{2})\in\widehat{B}(R)$. We have

$\widehat{B}(R)\subseteq\widehat{B}((f\times f)^{-1}(S))=(Bf\times
Bf)^{-1}(\widehat{B}(S))$

where the inclusion is a consequence of $f$ being a $\mathrm{Rel}$-morphism
and monotonicity of $\widehat{B}$, and the equality is an instance of (*).
Therefore $(t_{1},t_{2})\in\widehat{B}(R)$ implies $(t_{1},t_{2})\in(Bf\times
Bf)^{-1}[\widehat{B}(S)]$ which is in turn equivalent to
$(Bf(t_{1}),Bf(t_{2}))\in\widehat{B}(S)$. This shows that
$\widehat{B}f\colon\widehat{B}(R)\to\widehat{B}(S)$ as required. Functoriality
now follows easily from the fact that $\widehat{B}f=Bf$ for all functions $f$.

##  4\. Examples

In this section we instantiate the abstract framework to three concrete
examples: a behavioural metric on deterministic automata (Section 4.1),
captured by $[0,1]$-valued tests; a unary predicate on transition systems
(Section 4.2); and similarity of transition systems, captured by a logic with
conjunction and diamond modalities (Section 4.3).

###  4.1. Shortest distinguishing word distance

We study a simple behavioural distance on deterministic automata: for two
states $x,y$ and a fixed constant $c$ with $0<c<1$, the distance is given by
$c^{n}$, where $n$ is the length of the smallest word accepted from one state
but not the other. Following [BKP18], we refer to this distance as the
_shortest distinguishing word distance_ , and, for an automaton with state
space $X$, denote it by $d_{\mathit{sdw}}\colon X\times X\rightarrow[0,1]$.

Formally, fix a finite alphabet $A$, and consider the functor
$B\colon\mathsf{Set}\rightarrow\mathsf{Set}$, $BX=2\times X^{A}$ of
deterministic automata. We make use of the fibration
$p\colon\mathrm{Rel}_{[0,1]}\rightarrow\mathsf{Set}$, and define the lifting
$\overline{B}\colon\mathrm{Rel}_{[0,1]}\rightarrow\mathrm{Rel}_{[0,1]}$ by

$\overline{B}(X,d)=\left(BX,((o_{1},t_{1}),(o_{2},t_{2}))\mapsto\begin{cases}1&\text{
if }o_{1}\neq o_{2}\\\ c\cdot\max_{a\in A}\\{d(t_{1}(a),t_{2}(a))\\}&\text{
otherwise}\end{cases}\right)$

The shortest distinguishing word distance $d_{\mathit{sdw}}$ on a
deterministic automaton $\gamma\colon X\rightarrow 2\times X^{A}$ is the
greatest fixed point $\nu(\gamma^{*}\circ\overline{B}_{X})$ (recall that in
$\mathrm{Rel}_{[0,1]}$ we use the reverse order on $[0,1]$, see Example 2.1).

For an associated logic, we simply use words over $A$ as formulas, and define
a satisfaction relation which is weighted in $[0,1]$. Consider the following
setting.

$\textstyle{\mathsf{Set}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{P={[0,1]}^{-}}$$\scriptstyle{B=2\times\mathsf{Id}^{A}}$$\textstyle{\bot}$$\textstyle{\mathsf{Set}^{\mathsf{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Q=[0,1]^{-}}$$\scriptstyle{L=A\times\mathsf{Id}+1}$
with$\textstyle{B([0,1]^{-})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\delta}$$\textstyle{[0,1]^{L-}}$

The initial algebra of $L$ is the set of words $A^{*}$. The natural
transformation $\delta$ is given by $\delta_{X}\colon
2\times([0,1]^{X})^{A}\rightarrow[0,1]^{A\times X+1}$,

$\delta_{X}(o,t)(u)=\begin{cases}o&\text{ if }u=\ast\in 1\\\ c\cdot
t(a)(x)&\text{ if }u=(a,x)\in A\times X\end{cases}$

which is a quantitative, discounted version of the Boolean-valued logic in
Example 2.2. The logic $(L,\delta)$ defines, for any deterministic automaton
$\langle o,t\rangle\colon X\rightarrow 2\times X^{A}$, a theory map
$\mathit{th}\colon X\rightarrow[0,1]^{A^{*}}$, given by

$\displaystyle\mathit{th}(x)(\varepsilon)$ $\displaystyle=o(x)\qquad\text{ and
}\qquad\mathit{th}(x)(aw)=c\cdot\mathit{th}(t(x)(a))(w)\,,$

for all $x\in X$, $a\in A$, $w\in A^{*}$.

We characterise the shortest distinguishing word distance with the above
logic, by instantiating and proving adequacy and expressiveness. Define

$\overline{Q}\colon\mathsf{Set}^{\mathsf{op}}\rightarrow\mathrm{Rel}_{[0,1]}\,,\qquad\overline{Q}(X)=\left([0,1]^{X},(\phi_{1},\phi_{2})\mapsto\sup_{x\in
X}|\phi_{1}(x)-\phi_{2}(x)|\right)\,.$

Technically, this functor is given by mapping a set $X$ to the $X$-fold
product of the object $\overline{[0,1]}=([0,1],(r,s)\mapsto|r-s|)$. It follows
immediately that $\overline{Q}$ has a left adjoint, mapping $(X,d)$ to
$\mathrm{Hom}((X,d),\overline{[0,1]})$, see Equation 4. This will be useful
for proving adequacy below.

The functor $\overline{Q}$ yields a ‘logical distance’ between states $x,y\in
X$, given by $\mathit{th}^{*}(\overline{Q}\Phi)$. We abbreviate it by
$d_{\mathit{log}}\colon X\times X\rightarrow[0,1]$. Explicitly, we have

$d_{\mathit{log}}(x,y)=\sup_{w\in
A^{*}}|\mathit{th}(x)(w)-\mathit{th}(y)(w)|\,.$ (11)

Instantiating Definition 3, the logic $(L,\delta)$ is

  * •

_adequate_ if $d_{\mathit{sdw}}\geq d_{\mathit{log}}$, and

  * •

_expressive_ if $d_{\mathit{sdw}}\leq d_{\mathit{log}}$.

Here $\leq$ is the usual order on $[0,1]$, with $0$ the least element (the
order in $\mathrm{Rel}_{[0,1]}$ is reversed).

To prove adequacy and expressiveness, we use Theorem 3.1 and Theorem 3.1. The
functor $\overline{Q}$ has a left adjoint, as explained above. Further,
$(\overline{B},B)$ is a fibration map [BKP18]. We prove the remaining
hypotheses of both propositions by showing the equality
$\overline{B}\,\overline{Q}X=\delta_{X}^{*}(\overline{Q}LX)$ for every object
$X$ in $\mathcal{D}$. To this end, we compute (suppressing the carrier set
$BQX$):

$\begin{array}[]{rcl}&&\delta_{X}^{*}(\overline{Q}LX)\\\
&=&\left(((o_{1},t_{1}),(o_{2},t_{2}))\mapsto\sup_{u\in A\times
X+1}|\delta_{X}(o_{1},t_{1})(u)-\delta_{X}(o_{2},t_{2})(u)|\right)\\\
&=&\left((o_{1},t_{1}),(o_{2},t_{2}))\mapsto\begin{cases}1&\text{ if
}o_{1}\neq o_{2}\\\ \sup_{u\in A\times
X}|\delta_{X}(o_{1},t_{1})(u)-\delta_{X}(o_{2},t_{2})(u)|)&\text{
otherwise}\end{cases}\right)\\\
&=&\left((o_{1},t_{1}),(o_{2},t_{2}))\mapsto\begin{cases}1&\text{ if
}o_{1}\neq o_{2}\\\ \sup_{(a,x)\in A\times X}|c\cdot t_{1}(a)(x)-c\cdot
t_{2}(a)(x)|)&\text{ otherwise}\end{cases}\right)\\\
&=&\left((o_{1},t_{1}),(o_{2},t_{2}))\mapsto\begin{cases}1&\text{ if
}o_{1}\neq o_{2}\\\ c\cdot\max_{a\in A}\sup_{x\in
X}|t_{1}(a)(x)-t_{2}(a)(x)|)&\text{ otherwise}\end{cases}\right)\\\
&=&\overline{B}\,\overline{Q}X\\\ \end{array}$

Hence, the logic $(L,\delta)$ is adequate and expressive w.r.t. the shortest
distinguishing word distance, i.e., $d_{\mathit{sdw}}$ coincides with the
logical distance $d_{\mathit{log}}$ given in Equation 11.

###  4.2. Divergence of processes

A state of an LTS is said to be _diverging_ if there exists an infinite path
of $\tau$-transitions starting at that state. To model this predicate, let
$B\colon\mathsf{Set}\rightarrow\mathsf{Set}$,
$BX=(\mathcal{P}_{\omega}X)^{A}$, where $A$ is a set of labels containing the
symbol $\tau\in A$. Consider the predicate fibration
$p\colon\mathrm{Pred}\rightarrow\mathsf{Set}$, and define the lifting
$\overline{B}\colon\mathrm{Pred}\rightarrow\mathrm{Pred}$ by

$\overline{B}(X,\Gamma)=((\mathcal{P}_{\omega}X)^{A},\\{t\mid\exists
x\in\Gamma.\,x\in t(\tau)\\})\,.$

The coinductive predicate defined by $\overline{B}$ on a $B$-coalgebra
$(X,\gamma)$ is the set of diverging states:

$\nu(\gamma^{*}\circ\overline{B}_{X})=(X,\\{x\mid x\text{ is
diverging}\\})\,.$

Now, we want to prove in our framework of adequacy and expressiveness that $x$
is diverging iff for every $n\in\mathbb{N}$ there is a finite path of
$\tau$-steps starting in $x$, i.e.,
$x\models\left\langle\tau\right\rangle^{n}\top$ for every $n$. The proof
relies on two main observations:

  * •

if $x$ satisfies infinitely many formulas of
$\left\langle\tau\right\rangle^{n}\top$, then one of its $\tau$-successors
does, too;

  * •

if a state $x$ satisfies $\left\langle\tau\right\rangle^{n}\top$ for some $n$,
then $x$ satisfies $\left\langle\tau\right\rangle^{m}\top$ for all $0\leq
m\leq n$.

Combined, one can then give a coinductive proof, showing that if the current
state satisfies all formulas of the form
$\left\langle\tau\right\rangle^{n}\top$, then one of its $\tau$-successors
also satisfies all these formulas.

We make this argument precise by casting it into the abstract framework.
First, for the logic, we have the following setting:

$\textstyle{\mathsf{Set}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{P=2^{-}}$$\scriptstyle{B=(\mathcal{P}_{\omega}-)^{A}}$$\textstyle{\bot}$$\textstyle{\mathsf{Pos}^{\mathsf{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Q=\mathrm{Hom}(-,2)}$$\scriptstyle{L=\mathsf{Id}_{\top}}$
with$\textstyle{B\mathrm{Hom}(-,2)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\delta}$$\textstyle{\mathrm{Hom}(L-,2)}$

Here $\mathsf{Pos}$ is the category of posets and monotone maps, and
$2=\\{0,1\\}$ is the poset given by the order $0\leq 1$. For a poset $S$,
$\mathrm{Hom}(S,2)$ is then the set of _upwards closed_ subsets of $S$.

The functor $LS=S_{\top}$ is defined on a poset $S$ by adjoining a new top
element $\top$, i.e., the carrier is $S+\\{\top\\}$ and $\top$ is strictly
above all elements of $S$. The initial algebra $\Phi$ of $L$ is the set of
natural numbers, representing the formulas of the form
$\left\langle\tau\right\rangle^{n}\top$, linearly ordered, with $0$ the top
element. The choice of $\mathsf{Pos}$ means that the set
$\mathrm{Hom}(\Phi,2)$ used to represent the theory of a state $x\in X$
consists of upwards closed sets (so closed under lower natural numbers in the
usual ordering), corresponding to the second observation above concerning the
set of formulas satisfied by $x$.

The natural transformation $\delta$ is given by
$\delta_{S}\colon(\mathcal{P}_{\omega}\mathrm{Hom}(S,2))^{A}\rightarrow\mathrm{Hom}(S_{\top},2)$,

$\delta_{S}(t)(x)=\begin{cases}1&\text{ if }x=\top\\\ \bigvee_{\phi\in
t(\tau)}\phi(x)&\text{ otherwise}\end{cases}\,.$

To show that this is well-defined, suppose $x,y\in S_{\top}$ with $x\leq y$,
and suppose $\delta_{S}(t)(x)=1$. If $x=\top$, then $y=\top$, so
$\delta_{S}(t)(y)=1$. Otherwise, there is $\phi\in\mathrm{Hom}(S,2)$ such that
$\phi\in t(\tau)$ and $\phi(x)=1$. Since $\phi$ is upwards closed, $\phi(y)=1$
and consequently $\delta_{S}(t)(y)=1$ as needed.

Now, the theory map $\mathit{th}\colon X\rightarrow\mathrm{Hom}(\Phi,2)$ is
given by $\mathit{th}(x)(n)=1$ iff there exists a path of $\tau$-steps of
length $n$ from $x$. We define

$\overline{Q}\colon\mathsf{Pos}^{\mathsf{op}}\rightarrow\mathrm{Pred}\,,\quad\overline{Q}(S)=(\mathrm{Hom}(S,2),\\{\phi\mid\forall
x\in S.\,\phi(x)=1\\})\,.$

Instantiating Definition 3, _adequacy_ means that if $x$ is diverging, then
$x\models\left\langle\tau\right\rangle^{n}\top$ for all $n$; and
expressiveness is the converse.

We start with proving adequacy, using Theorem 3.1. The left adjoint
$\overline{P}$ is given by
$\overline{P}(X,\Gamma)=(\mathrm{Hom}((X,\Gamma),(2,\\{1\\})),\\{(\phi_{1},\phi_{2})\mid\forall
x\in X.\,\phi_{1}(x)\leq\phi_{2}(x)\\})$. It remains to prove that
$\overline{B}\,\overline{Q}(S)\leq\delta_{S}^{*}(\overline{Q}LS)$ for all $S$.
To this end, we observe $BQS=(\mathcal{P}_{\omega}(\mathrm{Hom}(S,2)))^{A}$
and compute:

$\displaystyle\delta_{S}^{*}(\overline{Q}LS)$
$\displaystyle=\\{t\mid\delta_{S}(t)\in\overline{Q}LS\\}$
$\displaystyle=\\{t\mid\forall x\in S_{\top}.\,\delta_{S}(t)(x)=1\\}$
$\displaystyle=\\{t\mid\forall x\in S.\,\delta_{S}(t)(x)=1\\}$
$\displaystyle=\\{t\mid\forall x\in S.\,\bigvee_{\phi\in t(\tau)}\phi(x)=1\\}$

and $\overline{B}\,\overline{Q}(S)=\\{t\mid(\lambda x.1)\in t(\tau)\\}$. The
needed inclusion is now trivial.

For expressiveness we have to prove the reverse inclusion with $S=\Phi$, i.e.,

$\\{t\in(\mathcal{P}_{\omega}(\mathrm{Hom}(\Phi,2)))^{A}\mid\forall
x\in\Phi.\bigvee_{\phi\in
t(\tau)}\phi(x)=1\\}\subseteq\\{t\in(\mathcal{P}_{\omega}(\mathrm{Hom}(\Phi,2)))^{A}\mid(\lambda
x.1)\in t(\tau)\\}.$

To this end, let $t$ be an element of the left-hand side, and suppose towards
a contradiction that for all $\phi$ with $\phi\in t(\tau)$, there is an
element $x_{\phi}\in\Phi$ with $\phi(x_{\phi})=0$. Choosing an assignment
$\phi\mapsto x_{\phi}$ of such elements, we get a _finite_ set
$\\{x_{\phi}\mid\phi\in t(\tau)\\}$. Let $x_{\phi}$ be the smallest element of
that set (w.r.t. the order of $\Phi$, i.e., the largest natural number), and
let $\psi\in\mathrm{Hom}(\Phi,2)$ be such that $\psi(x_{\phi})=1$; such a
$\psi$ exists by assumption on $t$. However, since $x_{\phi}\leq x_{\psi}$ and
$\psi$ is upwards closed we have $\psi(x_{\psi})=1$, which gives a
contradiction. Hence, the inclusion holds as required. The lifting
$(\overline{B},B)$ is a fibration map. We thus conclude from Theorem 3.1 that
the logic is expressive.

###  4.3. Simulation of processes

Let $B\colon\mathsf{Set}\rightarrow\mathsf{Set}$,
$BX=(\mathcal{P}_{\omega}X)^{A}$, and let $\gamma\colon
X\rightarrow(\mathcal{P}_{\omega}X)^{A}$ be $B$-coalgebra, i.e., a labelled
transition system. Denote _similarity_ by ${\precsim}\subseteq X\times X$,
defined more precisely below. Consider the logic with the following syntax:

$\varphi,\psi\mathrel{::=}\left\langle
a\right\rangle\varphi\mid\varphi\wedge\psi\mid\top$ (12)

where $a$ ranges over $A$, with the usual interpretation $x\models\varphi$ for
states $x\in X$. A classical Hennessy-Milner theorem for similarity is:

$x\precsim y\text{ iff }\forall\varphi.\,x\models\varphi\rightarrow
y\models\varphi\,.$ (13)

We show how to formulate and prove this result within our abstract framework.

First, recall from Equation 2 in Section 2.1 the appropriate lifting
$\overline{B}\colon\mathrm{Rel}\rightarrow\mathrm{Rel}$ in the relation
fibration $p\colon\mathrm{Rel}\rightarrow\mathsf{Set}$. A simulation on a
$B$-coalgebra $(X,\gamma)$ is a relation $R$ such that
$R\leq\gamma^{*}\circ\overline{B}_{X}(R)$, and similarity $\precsim$ is the
greatest fixed point of $\gamma^{*}\circ\overline{B}_{X}$.

For the logic, to incorporate finite conjunction, we instantiate $\mathcal{D}$
with the category $\mathsf{SL}$ of bounded (meet)-semilattices, i.e., sets
equipped with an associative, commutative and idempotent binary operator
$\wedge$ and a top element $\top$.

To add the modalities $\left\langle a\right\rangle$ for each $a\in A$, we
proceed as follows. Let $U\colon\mathsf{SL}\rightarrow\mathsf{Set}$ be the
forgetful functor. It has a left adjoint
$\mathcal{F}\colon\mathsf{Set}\rightarrow\mathsf{SL}$, mapping a set $X$ to
the meet-semilattice $\mathcal{P}_{\omega}(X)$ with the top element given by
$\emptyset$ and the meet by union. The functor
$L\colon\mathsf{SL}\rightarrow\mathsf{SL}$ is given by $LX=\mathcal{F}(A\times
UX)$; its initial algebra $\Phi$ consists precisely of the language presented
in Equation 12, quotiented by the semilattice equations222To simplify the
presentation we do not quotient with monotonicity axioms for the modal
operators, i.e., we do not ensure that $\varphi_{1}\leq\varphi_{2}$ implies
$\left\langle a\right\rangle\varphi_{1}\leq\left\langle
a\right\rangle\varphi_{2}$. . For the adjunction, we use:

$\textstyle{\mathsf{Set}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{P=2^{-}}$$\scriptstyle{B=(\mathcal{P}_{\omega}-)^{A}}$$\textstyle{\bot}$$\textstyle{\mathsf{SL}^{\mathsf{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Q=\mathrm{Hom}(-,2)}$$\scriptstyle{L=\mathcal{F}(A\times
U-)}$$\textstyle{\mbox{\qquad\qquad with}\quad
B\mathrm{Hom}(-,2)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\delta}$$\textstyle{\mathrm{Hom}(L-,2)}$

which is an instance of Equation 4. Here $2=\\{0,1\\}$ is the meet-semilattice
given by the order $0\leq 1$. For a semilattice $S$, the set
$\mathrm{Hom}(S,2)$ of semi-lattice morphisms is isomorphic to the set of
_filters_ on $S$: subsets $X\subseteq S$ such that $\top\in X$, and $x,y\in X$
iff $x\wedge y\in X$.

To define the natural transformation
$\delta_{S}\colon(\mathcal{P}_{\omega}(\mathrm{Hom}(S,2)))^{A}\rightarrow\mathrm{Hom}(\mathcal{F}(A\times
US),2)$ on a semilattice $S$, we use that for every map $f\colon A\times
US\rightarrow 2$ there is a unique semilattice homomorphism
$f^{\sharp}\colon\mathcal{F}(A\times US)\rightarrow 2$:

$\delta_{S}(t)=((a,x)\mapsto\bigvee_{\phi\in
t(a)}\phi(x))^{\sharp}=\left(W\mapsto\bigwedge_{(a,x)\in W}\bigvee_{\phi\in
t(a)}\phi(x)\right)\,.$

For an LTS $(X,\gamma)$, the associated theory map $\mathit{th}\colon
X\rightarrow\mathrm{Hom}(\Phi,2)$ maps a state to the formulas in (12) that it
accepts, with the usual semantics.

To recover (13), we need to relate logical theories appropriately. Define

$\overline{Q}\colon\mathsf{SL}^{\mathsf{op}}\rightarrow\mathrm{Rel}\,,\qquad\overline{Q}S=(\mathrm{Hom}(S,2),\\{(\phi_{1},\phi_{2})\mid\forall
x\in S.\,\phi_{1}(x)\leq\phi_{2}(x)\\})\,.$

Then
$\mathit{th}^{*}(\overline{Q}\Phi)=\\{(x,y)\mid\forall\varphi\in\Phi.\,\mathit{th}(x)(\varphi)\leq\mathit{th}(y)(\varphi)\\}$,
i.e., it relates all $(x,y)$ such that the set of formulas satisfied at $x$ is
included in the set of formulas satisfied at $y$. Thus, instantiating
Definition 3, adequacy
${\precsim}=\nu(\gamma^{*}\circ\overline{B}_{X})\leq\mathit{th}^{*}(\overline{Q}\Phi)$
is the implication from left to right in Equation 13, and expressiveness is
the converse.

We prove adequacy and expressiveness. The functor $\overline{Q}$ has a left
adjoint, given by $\overline{P}(X,R)=\mathrm{Hom}((X,R),\overline{2})$, where
$\overline{2}=(2,\\{(x,y)\mid x\leq y\\})$. This follows by Corollary 2.3 with
Remark 2.3, with $\mathsf{SL}$ as a full subcategory of the category of all
algebras for the corresponding signature.

Given a semilattice $S$, we compute
$\delta_{S}^{*}(\overline{Q}LS)\subseteq(BQS)^{2}=((\mathcal{P}_{\omega}(\mathrm{Hom}(S,2)))^{A})^{2}$:

$\displaystyle\delta_{S}^{*}(\overline{Q}LS)$
$\displaystyle=\delta_{S}^{*}(\\{(\phi_{1},\phi_{2})\mid\forall
W\in\mathcal{F}(A\times US).\,\phi_{1}(W)\leq\phi_{2}(W)\\})$
$\displaystyle=\\{(t_{1},t_{2})\mid\forall W\in\mathcal{F}(A\times
US).\,\bigwedge_{(a,x)\in W}\bigvee_{\phi\in
t_{1}(a)}\phi(x)\leq\bigwedge_{(a,x)\in W}\bigvee_{\phi\in
t_{2}(a)}\phi(x)\\}\,.$

Further, $\overline{B}\,\overline{Q}S=\\{(t_{1},t_{2})\mid\forall a\in
A.\,\forall\phi_{1}\in t_{1}(a).\,\exists\phi_{2}\in t_{2}(a).\,\forall x\in
S.\,\phi_{1}(x)\leq\phi_{2}(x)\\}$. For adequacy, we need to prove
$\overline{B}\,\overline{Q}S\leq\delta_{S}^{*}(\overline{Q}LS)$; but this is
trivial, given the above computations. For expressiveness, let
$(t_{1},t_{2})\in\delta_{S}^{*}(\overline{Q}LS)$. We need to show that
$(t_{1},t_{2})\in\overline{B}\,\overline{Q}S$. Suppose, towards a
contradication, that $(t_{1},t_{2})\not\in\overline{B}\,\overline{Q}S$, i.e.,
there exist $a\in A$ and $\phi_{1}\in t_{1}(a)$ such that for all $\phi_{2}\in
t_{2}(a)$, there is $x\in S$ with $\phi_{1}(x)=1$ and $\phi_{2}(x)=0$. We
choose such an element $x_{\phi_{2}}$ for every $\phi_{2}\in t_{2}(a)$. Note
that the collection $\\{x_{\phi_{2}}\mid\phi_{2}\in t_{2}(a)\\}$ is _finite_
—here we make use of the image-finiteness captured by the functor $B$. Now,
consider the conjunction $\psi=\bigwedge_{\phi_{2}\in t_{2}(a)}x_{\phi_{2}}\in
S$. Using that $\phi_{1}$ is a homomorphism, we have
$\phi_{1}(\psi)=\phi_{1}(\bigwedge_{\phi_{2}\in
t_{2}(a)}x_{\phi_{2}})=\bigwedge_{\phi_{2}\in
t_{2}(a)}\phi_{1}(x_{\phi_{2}})=1$, and consequently $\bigvee_{\phi\in
t_{1}(a)}\phi(\psi)=1$. We also have $\bigvee_{\phi\in
t_{2}(a)}\phi(\psi)=\bigvee_{\phi\in t_{2}(a)}\bigwedge_{\phi_{2}\in
t_{2}(a)}\phi(x_{\phi_{2}})=0$ since $\phi_{2}(x_{\phi_{2}})=0$ for every
$\phi_{2}\in t_{2}(a)$. Finally, to arrive at a contradiction, let
$W=\\{(a,\psi)\\}$. Since $(t_{1},t_{2})\in\delta_{S}^{*}(\overline{Q}LS)$
this implies $\bigvee_{\phi\in t_{1}(a)}\phi(\psi)\leq\bigvee_{\phi\in
t_{2}(a)}\phi(\psi)$, which is in contradiction with the above. It is easy to
check that $(\overline{B},B)$ is a fibration map (cf. [HJ04]). Hence, we
conclude expressiveness from Theorem 3.1.

######  Remark 4.1.

In fact, the expressiveness argument also goes through if we replace
$\mathsf{SL}$ in the above argument with the category of algebras for the
bounded semilattice signature. As pointed out in Sec. 2.3 this can be useful
in cases where an axiomatisation of the class of algebras involved is not
known. In the concrete case above we opted to work with the well-known
category $\mathsf{SL}$ instead.

##  5\. Finite-depth expressiveness and the Kleene fixed point theorem

In Section 3 we formulated expressiveness as an inequality
$\nu(\gamma^{*}\circ\overline{B}_{X})\geq\mathit{th}^{*}(\overline{Q}\Phi)$
for all $B$-coalgebras $(X,\gamma)$. The sufficient conditions formulated in
Theorem 3.1 ensure that $\mathit{th}^{*}(\overline{Q}\Phi)$ is a post-fixed
point of $\gamma^{*}\circ\overline{B}_{X}$, so that the desired inequality
follows. Thereby, that approach relies on the Knaster-Tarski fixed point
theorem, constructing the greatest fixed point as the largest post-fixed
point.

In the current section we explore a different abstract technique for proving
expressiveness, which instead relies on a technique for constructing greatest
fixed points which is often referred to as Kleene’s fixed point theorem. Given
a monotone function $\varphi\colon L\rightarrow L$ on a complete lattice $L$,
we construct the chain

$\top\geq\varphi(\top)\geq\varphi(\varphi(\top))\geq\ldots$

and take its limit

$\bigwedge_{i\in\omega}\varphi^{i}(\top)$

If $\varphi$ preserves limits of $\omega$-cochains (decreasing sequences
indexed by the natural numbers), also referred to as cocontinuity, then this
is the greatest fixed point of $\varphi$.

This suggests a different route to expressiveness: we will formulate
sufficient conditions to ensure that

$(\gamma^{*}\circ\overline{B}_{X})^{i}(\top)\geq(\mathit{th}_{i})^{*}(\overline{Q}\Phi_{i})$

for all $i\in\omega$; here $\Phi_{i}$ refers to formulas of depth $i$, made
more precise below using the _initial_ sequence of the functor $L$, and
$\mathit{th}_{i}\colon X\rightarrow Q\Phi_{i}$ is the associated theory map.
The above family of inequalities (indexed by $i$) can be thought of as
_finite-depth expressiveness_ : it states that the formulas of depth at most
$i$ are expressive with respect to the $i$-th approximation of the coinductive
predicate defined by $\overline{B}$. For instance, that logical equivalence
w.r.t. formulas of depth $i$ in Hennessy-Milner logic imply $i$-step
bisimilarity.

These conditions are sufficient to ensure finite-depth expressiveness—if we
then make the additional assumption that $\gamma^{*}\circ\overline{B}_{X}$ is
cocontinuous, we obtain proper expressiveness. In the ‘Knaster-Tarski’
approach to expressiveness of Theorem 3.1, instead, no such assumption is
explicitly formulated. So in that approach, cocontinuity is not explicitly
assumed. This explains why in some of the examples—for instance similarity of
labelled transition systems—part of the argument resembles a proof of
cocontinuity.

A remark is in order here. The cocontinuity of
$\gamma^{*}\circ\overline{B}_{X}$, which is a functor on a fibre (hence, a
monotone map between posets), is of course different from preservation of
limits of chains by $\overline{B}$ or $B$. We refer to [HKC18] for a proper
study of the relation between these different sequences. The current section
is primarily about another the relation between these various sequences and
the initial sequence of $L$.

Throughout this section we work again under Assumptions 3 and 3.1 concerning
our overall categorical setting. We start by recalling the notion of initial
and final sequence.

######  Definition 5.1 (Initial and final sequence).

Suppose $\mathcal{D}$ has an initial object $0$. The _initial sequence_ of $L$
is the chain $(L^{i}0)_{i\in\omega}$, with connecting morphisms $l_{i,j}\colon
L^{i}0\rightarrow L^{j}0$ for all $i\leq j$ defined by $l_{0,j}={!_{L^{j}0}}$
for all $j$ and $l_{i+1,j+1}=Ll_{i,j}$. Further, given an algebra
$\alpha\colon LA\rightarrow A$, we inductively define a cocone
$\alpha_{i}\colon L^{i}0\rightarrow A$ by $\alpha_{0}={!_{A}}$ and
$\alpha_{i+1}=\alpha\circ L\alpha_{i}$.

If $\mathcal{C}$ has an initial object $1$, the final sequence of $B$ is
defined dually as $(B^{i}1)_{i\in\omega}$, with the associated connecting
morphisms $b_{j,i}\colon B^{j}1\rightarrow B^{i}1$ for $i\leq j$. Any
coalgebra $\gamma\colon X\rightarrow BX$ defines a cone $\gamma_{i}\colon
X\rightarrow B^{i}1$ by $\gamma_{0}={!_{X}}$ and
$\gamma_{i+1}=B\gamma_{i}\circ\gamma$.

If $L$ preserves colimits of $\omega$-chains, of which the initial sequence is
an instance, then the colimit $\mathrm{colim}_{i\in\omega}L^{i}0$ carries an
initial algebra [Adá74]. Dually if $B$ preserves limits of $\omega$-co-chains,
$\lim_{i\in\omega}B^{i}1$ is a final coalgebra. In both cases, the elements of
the respective sequences can be thought of as approximations of the initial
algebra and final coalgebra, respectively.

For a coalgebra $(X,\gamma)$, we define the cone

$\llbracket\\_\rrbracket_{i}=(P\gamma\circ\widehat{\delta}_{A})_{i}\colon
L^{i}0\rightarrow PX\,,$

as above, and let

$\mathit{th}_{i}\colon X\rightarrow QL^{i}0$

be the transpose of $\llbracket\\_\rrbracket_{i}$. The elements of $L^{i}0$
are thought of as modal formulas of rank at most $i$, and $\mathit{th}_{i}$ is
the theory map of a coalgebra restricted to those formulas. It is easy to show
that the $\mathit{th}_{i}$ maps satisfy the following properties:

######  Lemma 5.2.

For all $i$, the two triangles in the following diagram commute.

$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathit{th}_{i}}$$\scriptstyle{\gamma}$$\scriptstyle{\mathit{th}_{i+1}}$$\textstyle{QL^{i}0}$$\textstyle{BX\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{B\mathit{th}_{i}}$$\textstyle{BQL^{i}0\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\delta_{L^{i}0}}$$\textstyle{QL^{i+1}0\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Ql_{i,i+1}}$

Furthermore we define a sequence $(\delta_{i}\colon B^{i}1\rightarrow
QL^{i}0)_{i\in\omega}$, which iterates $\delta$ on the final sequence of $B$,
as follows:

$\delta_{0}=\mathsf{id}\colon 1\rightarrow
Q0\qquad\delta_{i+1}=\left(\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
14.55145pt\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 3.0pt\raise
0.0pt\hbox{$\textstyle{BB^{i}1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
18.4765pt\raise 6.09007pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.77103pt\hbox{$\scriptstyle{B\delta_{i}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 38.55145pt\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
38.55145pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{BQL^{i}0\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
78.81078pt\raise 6.3777pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.48341pt\hbox{$\scriptstyle{\delta_{L^{i}0}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 98.27866pt\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
98.27866pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{QL^{i+1}0}$}}}}}}}\ignorespaces}}}}\ignorespaces\right).$

We use here that $Q0=1$ is a final object, as $0$ is initial and $Q$ a right
adjoint. This enables us to relate $\mathit{th}_{i}$ and $\gamma_{i}$.

######  Lemma 5.3.

Let $(X,\gamma)$ be a coalgebra. For all $i$,
$\mathit{th}_{i}=\delta_{i}\circ\gamma_{i}$.

######  Proof 5.4.

By induction on $i$. The base case is trivial:
$\mathit{th}_{0}={!_{X}}=\delta_{0}\circ\gamma_{0}$. Suppose it holds for some
$i$. Then: $\mathit{th}_{i+1}=\delta_{L^{i}0}\circ
B\mathit{th}_{i}\circ\gamma=\delta_{L^{i}0}\circ B\delta_{i}\circ
B\gamma_{i}\circ\gamma=\delta_{i+1}\circ\gamma_{i+1}$, where the first
equality holds by Lemma 5.2.

The following lemma shows that, for a coalgebra $(X,\gamma)$, the elements of
the final sequence of $\gamma^{*}\circ\overline{B}_{X}$ (in the fibre
$\mathcal{E}_{X}$) can be retrieved from the final sequence of $\overline{B}$
(in the total category $\mathcal{E}$) by reindexing along the maps
$\gamma_{i}\colon X\rightarrow B^{i}1$.

######  Lemma 5.5.

Suppose $(B,\overline{B})$ is a fibration map, and let $(X,\gamma)$ be a
$B$-coalgebra. Then for all $i$,
$(\gamma_{i})^{*}(\overline{B}^{i}1)=(\gamma^{*}\circ\overline{B}_{X})^{i}(\top)$.

######  Proof 5.6.

By induction on $i$. The base case is easy, since reindexing in
$\mathsf{CLat}_{\wedge}$-fibrations preserves top elements. For the inductive
case, suppose it holds for some $i$. We compute:

$\displaystyle(\gamma_{i+1})^{*}(\overline{B}^{i+1}1)$
$\displaystyle=(B\gamma_{i}\circ\gamma)^{*}(\overline{B}\,\overline{B}^{i}1)$
$\displaystyle=\gamma^{*}\circ(B\gamma_{i})^{*}(\overline{B}\,\overline{B}^{i}1)$
$\displaystyle=\gamma^{*}\circ\overline{B}_{X}\circ(\gamma_{i})^{*}(\overline{B}^{i}1)$
($(\overline{B},B)$ fibration map)
$\displaystyle=\gamma^{*}\circ\overline{B}_{X}\circ(\gamma\circ\overline{B}_{X})^{i}(\top)$
(induction hypothesis)
$\displaystyle=(\gamma\circ\overline{B}_{X})^{i+1}(\top)\,.$

The following result now establishes a sufficient condition on $\delta$ for
finite-depth expressiveness, formulated in terms of the final sequence of
$\overline{B}$ and initial sequnece of $L$.

######  Proposition 5.7 (Finite-depth expressiveness).

Suppose $(\overline{B},B)$ is a fibration map. Then for all $i$: if
$\delta_{i}^{*}(\overline{Q}L^{i}0)\leq\overline{B}^{i}1$ then for any
$B$-coalgebra $(X,\gamma)$, we have
$(\mathit{th}_{i})^{*}(\overline{Q}L^{i}0)\leq(\gamma^{*}\circ\overline{B}_{X})^{i}(\top)$.

######  Proof 5.8.

If $\delta_{i}^{*}(\overline{Q}L^{i}0)\leq\overline{B}^{i}1$, then:

$\displaystyle(\mathit{th}_{i})^{*}(\overline{Q}L^{i}0)$
$\displaystyle=(\gamma_{i})^{*}\circ(\delta_{i})^{*}(\overline{Q}L^{i}0)$
(Lemma 5.3) $\displaystyle\leq(\gamma_{i})^{*}(\overline{B}^{i}1)$
(assumption) $\displaystyle=(\gamma\circ\overline{B}_{X})^{i}(\top)\,.$ (Lemma
5.5)

A natural way to move from the above result on finite-depth expressiveness to
full expressiveness is to assume that the functors $\overline{B}_{X}$ on the
fibre preserve limits of $\omega$-chains. Note that these are functors on
fibres (that is, monotone functions), and there is no assumption on $B$ or
$\overline{B}$ preserving anything.

######  Theorem 5.8 (Expressiveness via Kleene fixed point theorem).

Suppose $(\overline{B},B)$ is a fibration map, and for all $i$:
$\delta_{i}^{*}(\overline{Q}L^{i}0)\leq\overline{B}^{i}\overline{Q}0$. Then
for all $i$:
$\mathit{th}^{*}(\overline{Q}\Phi)\leq(\gamma^{*}\circ\overline{B}_{X})^{i}(\top)$.
In particular, if $\overline{B}_{X}$ preserves limits of $\omega$-cochains,
then the logic $(L,\delta)$ is expressive.

######  Proof 5.9.

Let $(X,\gamma)$ be a coalgebra; we need to prove that
$\mathit{th}^{*}(\overline{Q}\Phi)\leq\nu(\gamma^{*}\circ\overline{B}_{X})$.
For the initial algebra $(\Phi,\alpha)$, we have the sequence
$\alpha_{i}\colon L^{i}0\rightarrow\Phi$ (Definition 5.1) and since
$\llbracket\\_\rrbracket\colon\Phi\rightarrow PX$ is an algebra morphism, it
follows that
$\llbracket\\_\rrbracket\circ\alpha_{i}=\llbracket\\_\rrbracket_{i}$ for all
$i$. Hence, $\mathit{th}_{i}=Q\alpha_{i}\circ\mathit{th}\colon X\rightarrow
QL^{i}0$. Now, since there is the composite morphism

$\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
19.12225pt\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 3.0pt\raise
0.0pt\hbox{$\textstyle{\mathit{th}^{*}(\overline{Q}\Phi)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
28.39436pt\raise 7.74667pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.47557pt\hbox{$\scriptstyle{\widetilde{\mathit{th}}_{\overline{Q}\Phi}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 56.11092pt\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
56.11092pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\overline{Q}\Phi\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
84.3995pt\raise 6.49841pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.17937pt\hbox{$\scriptstyle{\overline{Q}\alpha_{i}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 111.32181pt\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
111.32181pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\overline{Q}L^{i}0}$}}}}}}}\ignorespaces}}}}\ignorespaces\,,$

which sits above $Q\alpha_{i}\circ\mathit{th}=\mathit{th}_{i}$, we have
$\mathit{th}^{*}(\overline{Q}\Phi)\leq\mathit{th}_{i}^{*}(\overline{Q}L^{i}0)$.
Combined with Proposition 5.7, we get

$\mathit{th}^{*}(\overline{Q}\Phi)\leq(\gamma^{*}\circ\overline{B}_{X})^{i}(\top)$

for all $i$.

Finally, if $\overline{B}_{X}$ preserves limits of $\omega$-cochains, then so
does $\gamma^{*}\circ\overline{B}_{X}$ (reindexing $\gamma^{*}$ preserves all
meets, by the definition of $\mathsf{CLat}_{\wedge}$-fibration). Hence
$\bigwedge_{i\in\omega}\nu(\gamma^{*}\circ\overline{B}_{X})(\top)=\nu(\gamma^{*}\circ\overline{B}_{X})$.
And thus
$\mathit{th}^{*}(\overline{Q}\Phi)\leq\nu(\gamma^{*}\circ\overline{B}_{X})$.

######  Example 5.10.

We show (finite-depth) expressiveness via the above approach for the example
of similarity of labelled transition systems (Section 4.3). The relevant
endofunctors $B=\mathcal{P}_{\omega}(-)^{A},\overline{B},L$, adjunctions
$P\dashv Q$ and $\overline{P}\dashv\overline{Q}$, and $\delta$ are all as
defined there. Contrary to the treatment in Section 4.3, with the current
approach it matters quite a bit whether $A$ is finite or not.333This was
pointed out to us by Yuichi Komorida. For the moment, we will assume that $A$
is finite, which significantly simplifies the matter. In Example 5.11 below we
discuss the infinite case.

The final sequence of $\overline{B}$ is concretely described as a sequence of
relations on $B^{i}1$, by just instantiating $\overline{B}$ for the inductive
case:

$\overline{B}B^{i}1=\\{(t_{1},t_{2})\mid\forall a\in A.\,\forall x\in
t_{1}(a).\,\exists y\in t_{2}(a).(x,y)\in B^{i}1\\}\,.$

and $\overline{B}^{0}1=\\{(\ast,\ast)\\}$. Thus,
$(t_{1},t_{2})\in\overline{B}^{i}1$ iff $t_{1}$ “$i$-step simulates” $t_{2}$,
where both $t_{1}$ and $t_{2}$ are viewed as trees of height at most $i$.

The initial sequence of $L\colon\mathsf{SL}\rightarrow\mathsf{SL}$ is
characterised, once again by spelling out the definition, by
$L^{0}0=\\{\top\\}$ (the one-element semilattice) and
$LL^{i}0=\mathcal{P}_{\omega}(A\times L^{i}0)$. Concretely, elements of
$L^{i}0$ can be identified with formulas in the logic of Section 4.3 (diamond
modalities and conjunction), quotiented by the semilattice equations. By the
assumption that $A$ is finite, each set $L^{i}0$ is finite.

We continue to prove the main hypothesis of Proposition 5.7 and Theorem 2:
that

$\delta_{i}^{*}(\overline{Q}L^{i}0)\leq\overline{B}^{i}1$ (14)

for all $i$. Before doing so, we spell out
$\delta_{i}^{*}(\overline{Q}L^{i}0)$ in some more detail. First, we
characterise $\delta_{i+1}\colon BB^{i}1\rightarrow QLL^{i}0$:

$\displaystyle\delta_{i+1}(t)(W)$
$\displaystyle=\delta_{L^{i}0}(B\delta_{i}(t))(W)$
$\displaystyle=\bigwedge_{(a,\psi)\in
W}\bigvee_{\phi\in(B\delta_{i}(t))(a)}\phi(\psi)$
$\displaystyle=\bigwedge_{(a,\psi)\in W}\bigvee_{x\in
t(a)}\delta_{i}(x)(\psi)$

The map $\delta_{i}$ assigns to an element $t\in B^{i}1$ the formulas of modal
depth at most $i$ that hold for $t$, viewed as a tree.

We now prove (14) by induction on $i$. The base case is trivial. For the
inductive case, assume (14) holds for some $i$. We have to prove that, for all
$(t_{1},t_{2})\in\delta^{*}_{i+1}(\overline{Q}L^{i+1}0)$, $a\in A$ and $x\in
t_{1}(a)$, there exists $y\in t_{2}(a)$ such that $(x,y)\in B^{i}1$. We first
spell out $\delta_{i+1}^{*}(\overline{Q}L^{i+1}0)$:

$\displaystyle\delta_{i+1}^{*}(\overline{Q}L^{i+1}0)$
$\displaystyle=\\{(t_{1},t_{2})\in\overline{B}^{i+1}\mid\forall\phi\in
L^{i+1}0.\,\delta^{*}_{i+1}(t_{1})(\phi)\leq\delta^{*}_{i+1}(t_{2})(\phi)\\}$
$\displaystyle=\\{(t_{1},t_{2})\mid\forall W\in
L^{i+1}0.\,\bigwedge_{(a,\psi)\in W}\bigvee_{x\in
t_{1}(a)}\delta_{i}(x)(\psi)\leq\bigwedge_{(a,\psi)\in W}\bigvee_{x\in
t_{2}(a)}\delta_{i}(x)(\psi)\\}\,.$

Now, let $(t_{1},t_{2})\in\delta^{*}_{i+1}(\overline{Q}L^{i+1}0)$, $a\in A$
and $x\in t_{1}(a)$. Define $\Psi=\\{\psi\in
L^{i}0\mid\delta_{i}(x)(\psi)=1\\}$ (this represents the formula
$\bigwedge_{\delta_{i}(x)(\psi)=1}\psi$). Note that $\Psi$ is finite, as
$L^{i}0$ is. Since $\delta_{i}(x)$ is a filter, we get
$\delta_{i}(x)(\bigwedge_{\psi\in\Psi}\psi)=\bigwedge_{\psi\in\Psi}\delta_{i}(x)(\psi)=1$,
where the second equality holds by definition of $\Psi$. Since
$(t_{1},t_{2})\in\delta_{i+1}(\overline{Q}L^{i+1}0)$, taking
$W=\\{(a,\Psi)\\}$ (this represents $\left\langle
a\right\rangle\bigwedge_{\delta_{i}(x)(\psi)=1}\psi$) we get that there exists
$y\in t_{2}(a)$ such that $\delta_{i}(y)(\bigwedge_{\psi\in\Psi}\psi)=1$.
Hence, since $\delta_{i}(y)$ is a filter, we get $\delta_{i}(y)(\psi)=1$ for
all $\psi\in\Psi$. Thus $(x,y)\in\delta_{i}^{*}(\overline{Q}L^{i}0)$, and by
the induction hypothesis we obtain $(x,y)\in\overline{B}^{i}1$ as needed.

The above proof relies on the set of labels $A$ to be finite. In the following
example we show a way to adapt the proof to the case where this assumption is
dropped.

######  Example 5.11.

If $A$ is not assumed to be infinite, the above proof doesn’t work, as the
meet $\bigwedge\Psi$ may be infinite, which is not defined as we are working
with semilattices. To remedy this, with $\Psi$ defined as above, let
$\Psi_{0}\subseteq\Psi_{1}\subseteq\Psi_{2}\subseteq\ldots$ be an increasing
sequence of finite subsets of $\Psi$ such that
$\bigcup_{i\in\mathbb{N}}\Psi_{i}=\Psi$. First note that, for each $i$, we
have $\delta_{i}(x)(\bigwedge_{\psi\in\Psi_{i}}\psi)=1$ using again the filter
property. Now, take

$W=\\{(a,\Psi_{i})\mid i\in\mathbb{N}\\}\,.$

Following the earlier reasoning, we get for each $i$ an element $y\in
t_{2}(a)$ such that $\delta_{i}(y)(\bigwedge_{\psi\in\Psi_{i}}\psi)=1$. In
fact, since $t_{2}(a)$ is finite, there exists an $y$ such that
$\delta_{i}(y)(\bigwedge_{\psi\in\Psi_{i}}\psi)=1$ for infinitely many $i$
(and as a consequence for all $i$). Since $\delta_{i}(y)$ is a filter this
means $\bigwedge_{\psi\in\Psi_{i}}\delta_{i}(y)(\psi)=1$ for infinitely many
$i$. Finally, since every $\psi\in\Psi$ is contained in some $\Psi_{i}$ we
obtain the desired result that $\delta(y)(\psi)=1$ for all $\psi\in\Psi$. The
proof then concludes as above.

##  6\. Future work

We proposed suitable notions of expressiveness and adequacy, connecting
coinductive predicates in a fibration to coalgebraic modal logic in a
contravariant adjunction. Further, we gave sufficient conditions on the one-
step semantics that guarantee expressiveness and adequacy, and showed how to
put these methods to work in concrete examples.

There are several avenues for future work. First, an intriguing question is
whether the characterisation of behavioural metrics in [KM18, WSPK18] can be
covered in the setting of this paper, as well as logics for other distances
such as the (abstract, coalgebraic) Wasserstein distance. Those behavioural
metrics are already framed in a fibrational setting [BKP18, SKDH18, BBKK18,
KKH+19]. While all our examples are for coalgebras in $\mathsf{Set}$, the
fibrational framework allows different base categories, which might be useful
to treat, e.g., behavioural metrics for continuous probabilistic systems
[vBW05].

A further natural question is whether we can automatically _derive_ logics for
a given predicate. As mentioned in the introduction, there are various tools
to find expressive logics for behavioural equivalence. But extending this to
the current general setting is non-trivial. Conversely, given a logic, one
would like to associate a lifting to it, perhaps based on techniques related
to $\Lambda$-bisimulations [GS13, BH17, Enq13].

## References

  * [Adá74] Jiří Adámek.  Free algebras and automata realizations in the language of categories.  Commentationes Mathematicae Universitatis Carolinae, 15(4):589–602, 1974.
  * [BBKK18] Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König.  Coalgebraic behavioral metrics.  Logical Methods in Computer Science, 14(3), 2018.