# Internal Models for Coalgebraic Modal Logics

Toby Wilkinson

► To cite this version:

Toby Wilkinson. Internal Models for Coalgebraic Modal Logics. 11th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Mar 2012, Tallinn, Estonia. pp.238-258, 10.1007/978-3-642-32784-1_13. hal-01539883

HAL Id: hal-01539883

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

Submitted on 15 Jun 2017

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
Internal Models for Coalgebraic Modal Logics

Toby Wilkinson *

University of Southampton, UK
stw08r@ecs.soton.ac.uk

**Abstract.** We present ongoing work into the systematic study of the use of dual adjunctions in coalgebraic modal logic. We introduce a category of internal models for a modal logic. These are constructed from syntax, and yield a generalised notion of canonical model. Further, expressivity of a modal logic is shown to be characterised by factorisation of its models via internal models and the existence of cospans of internal models.

**Keywords:** Coalgebra; Modal Logic; Dual Adjunction; Expressivity

# 1 Introduction

The now standard approach to coalgebraic modal logic is through a so called logical connection - a dual adjunction between two base categories X and A. The category X represents state spaces, or sets of processes, and the category A base logics, typically presented as algebras. The standard example is that of the categories **Set** and **BA**, where the latter is taken to represent classical propositional logics.

To these are added transition structures and modal operators. The modal operators, added to the base logics, aim to capture the dynamics of the transition structures. In choosing the modalities there is often a conflict between fully capturing the dynamics, and choosing modalities with an intuitive meaning, as logics with modalities that are hard to understand are unlikely to be adopted.

The transition structures are defined as coalgebras for an endofunctor $T$ on $X$, and the modal logics as algebras for an endofunctor $L$ on A. The semantics are then given by means of a natural transformation. Clearly this is a very general framework. Our work aims to explore the rich structure of this framework through the use of categorical techniques.

The first step is to make precise when a $T$-coalgebra is a model for an $L$-algebra, and this requires the notion of a valuation of an $L$-algebra in a $T$-coalgebra. A model then becomes a coalgebra, valuation pair. The models for an $L$-algebra form a category, and the structure of this category determines many of the properties of the modal logic that the $L$-algebra represents.

The main contribution of this paper is the observation that for each $L$-algebra, there is a full subcategory of its category of models that in many cases determines the logical properties of that $L$-algebra. These models we call the

<footnote>* Research supported by an EPSRC Doctoral Training Account.</footnote>
internal models, and as will be seen, they generalise the concept of canoni-
cal models found in Kripke semantics [2]. Like canonical models, they can be
thought of as being constructed from the syntax of the modal logic.

The most important property that an *L*-algebra can have, is that every model
factors via an internal model. If an *L*-algebra has this property, then the infor-
mation content of the category of models is contained entirely within the sub-
category of internal models, and the other models need not be considered. This
turns out to be very useful, since if X is wellpowered and certain morphisms are
monomorphisms, then because the category of internal models is thin, its objects
can be partitioned into a collection of equivalence classes that is a set (actually
a poset). Moreover, under similar conditions, and if X has an appropriate fac-
torisation system, the forgetful functor from the category of internal models to
X detects colimits. So if X is cocomplete, wellpowered, and has an appropriate
factorisation system, then the category of internal models is cocomplete, and a
final internal model exists as the coproduct of a representative from each of the
equivalence classes of internal models. This forms the basis of an adjoint functor
theorem between the categories *Alg*(*L*) and *CoAlg*(*T*).

The factorisation of models via internal models is shown to follow from the
existence of a factorisation system (E, M) in X, and a condition that essentially
amounts to T preserving M, and a particular natural transformation being com-
ponentwise in M. This is a restatement of [8, Theorem 4.2] and [6, Theorem 4].

In [8,6] this result is used to prove expressivity results for coalgebraic modal
logics. We go beyond this, and show that under certain mild assumptions on the
category X and if T preserves M, then an L-algebra is expressive for its category
of models, if and only if, every model factors via an internal model, and for every
pair of internal models there exists a cospan. This result is a purely categorical
characterisation of expressivity, and provides strong support to the school of
thought that the correct way to formulate expressivity is via cospans, and not
by bisimulation relations represented as spans. This is particularly important
for labelled Markov processes, for which in [3], the authors point out that the
failure of T to preserve weak pullbacks, which is the case for the Giry monad
on measurable spaces, poses a severe difficulty to the construction of such a
bisimulation. In [6] the expressivity result of [3] is recast in our dual adjunction
framework, and we examine it in Example 24 (3) and Example 36 (3).

A general outline of this paper is as follows. In section 2 we recall the category theoretic notion of a factorisation system. Then in section 3 we explain the dual adjunction framework in which we work. In section 4 we define what we mean by a model for a modal logic, and introduce the concept of an internal model. Then in section 5 we show when colimits of models and internal models exist. The proofs of these results are relatively straightforward, but long and tedious, so we restrict our presentation to an outline of the proofs. In section 6 an adjoint functor theorem is proved as a simple example of the utility of internal models. Then in section 7 internal models are used to characterise expressivity.
## 2 Preliminaries

In what follows we will need to be able to factorise morphisms. The standard approach to this is via a factorisation system [1].

**Definition 1.** In a category $\mathcal{C}$, a pair $(E, M)$ of classes of morphisms is called a factorisation system for $\mathcal{C}$, if the following hold:

1. If $e \in E$, and $h$ an isomorphism in $\mathcal{C}$, then if $h \circ e$ exists, $h \circ e \in E$.

2. If $m \in M$, and $h$ an isomorphism in $\mathcal{C}$, then if $m \circ h$ exists, $m \circ h \in M$.

3. $\mathcal{C}$ has $(E, M)$-factorisations; i.e. every morphism $f$ in $\mathcal{C}$ factors as $f = m \circ e$, with $m \in M$ and $e \in E$.

4. $\mathcal{C}$ has the unique $(E, M)$-diagonalisation property; i.e. every commuting square in $\mathcal{C}$ with $e \in E$ and $m \in M$, has a unique diagonal $d$ such that the following commutes

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

**Definition 2.** In a category $\mathcal{C}$ a factorisation system $(E, M)$ is called proper, if $E$ is a subclass of the epimorphisms of $\mathcal{C}$, and if $M$ is a subclass of the monomorphisms of $\mathcal{C}$.

*Example 3.*

1. In the category **Set** the obvious factorisation system $(E, M)$, is to take $E$ to be all the epimorphisms (surjective functions), and $M$ all the monomorphisms (injective functions).

2. In the category **Top** of topological spaces, (Epi, Mono) is not a factorisation system, however (RegEpi, Mono) and (Epi, RegMono) are. Here, RegEpi is the class of regular epimorphisms (quotients), and RegMono is the class of regular monomorphisms (embeddings).

We shall also make use of the following proposition which is a statement of parts of [1, Propositions 14.6, 14.9].

**Proposition 4.** Let $\mathcal{C}$ be a category with a factorisation system $(E, M)$.

1. Each of $E$ and $M$ is closed under composition.

2. If $f \circ g \in M$ and $f \in M$, then $g \in M$.

3. If $f \circ g \in E$ and $g \in E$, then $f \in E$.

A class of monomorphisms defines a notion of subobject in a category, and it is often important that for every object in a category its collection of subobjects is a set. The following definitions are standard [1].
**Definition 5.** Given a class M of monomorphisms in a category $\mathcal{C}$ we define the following:

1. An M-subobject of an object A in $\mathcal{C}$ is a pair $(S, m)$, where $m: S \to A$ is in M.

2. Two M-subobjects $(S, m)$ and $(S', m')$ of A are isomorphic if there exists an isomorphism $h: S \to S'$ such that $m = m' \circ h$.

3. $\mathcal{C}$ is M-wellpowered if no object in $\mathcal{C}$ has a proper class of pairwise non-isomorphic M-subobjects. Here by pairwise non-isomorphic we mean that any pair of distinct subobjects are non-isomorphic.

Dually, for a class E of epimorphisms we can define an E-quotient object of an object A as a pair $(e, Q)$, where $e: A \to Q$ is in E. The obvious dual notion to $\mathcal{C}$ being M-wellpowered is that $\mathcal{C}$ is E-cowellpowered.

**Definition 6.** A category $\mathcal{C}$ is thin if each homset has at most one element.

**Proposition 7.** Given a class M of monomorphisms in a category $\mathcal{C}$, the M-subobjects of an object A form a thin category $\mathrm{Sub}_M(A)$, the objects of which can be partitioned by isomorphisms into a collection of equivalence classes that carries a partial order, and if $\mathcal{C}$ is M-wellpowered this collection is a set.

## 3 Dual-Adjunction Framework

Increasingly, the standard approach to coalgebraic modal logic is to formulate it in a dual-adjunction framework [10,8,6].

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

Briefly this consists of two categories $\mathcal{A}$ and $\mathcal{X}$, and two contravariant functors $P$ and $S$ that form a dual adjunction i.e. there exists a natural isomorphism

$$ \Phi: \mathcal{A}(-1, P(-2)) \Rightarrow \mathcal{X}(-2, S(-1)) $$

Such a dual-adjunction is often referred to as a **logical connection** [12], and we denote the unit and counit by

$$ \rho: \mathrm{id}_{\mathcal{A}} \Rightarrow \mathrm{PS} $$

$$ \sigma: \mathrm{id}_{\mathcal{X}} \Rightarrow \mathrm{SP} $$

The category $\mathcal{X}$ represents a collection of state spaces, and a collection of generalised transition systems is defined on these state spaces as coalgebras for an endofunctor $T$. Similarly, the category $\mathcal{A}$ represents a collection of base logics to which modal operators are to be added. These are introduced via an endofunctor $L$, and the corresponding modal logics are the $L$-algebras. The semantics of these
modal logics is given in two stages. First the dual adjunction gives a semantics for the base logics in terms of the state spaces, and then secondly, a natural transformation

$$ \delta: LP \Rightarrow PT $$

gives the semantics of the modal operators in terms of the transition structures introduced by T [9,11].

*Example 8.* Many examples of logical connections have appeared in the literature. A small sample includes:

1. The logical connection arising from the contravariant powerset functor on **Set**, and the ultrafilter construction on the objects of **BA** [6].

2. Stone's Representation Theorem arising from taking the clopen sets of the objects of **Stone**, and an ultrafilter construction on the objects of **BA** [10].

3. The logical connection arising from the contravariant powerset functor on **Set**, and the filter construction on the objects of **MSL** (meet semilattices with top) [6].

4. The logical connection arising from taking the $\sigma$-algebra of the objects of **Meas** (measurable spaces), and a filter construction on the objects of **MSL** [6].

# 4 Models and Internal Models

The Kripke semantics for modal logic [2] introduces the concepts of frame, valuation, and model, where a model is a pair consisting of a frame and a valuation. There are obvious generalisations of these notions to coalgebraic modal logic.

**Definition 9.** Given an $L$-algebra $(A, \alpha)$ and a $T$-coalgebra $(X, \gamma)$, if there exists a morphism $f$ (not necessarily unique) such that the diagram below commutes, then $(X, \gamma)$ is called a **frame** for $(A, \alpha)$, and $f$ is called a **valuation of** $(A, \alpha)$ in $(X, \gamma)$, and the pair is called a **model** for $(A, \alpha)$.

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

Clearly, if $(A, \alpha)$ is the initial $L$-algebra then every $T$-coalgebra is a frame, but in general this is not the case.
*Remark 10.* If we were following the conventions of Kripke semantics for modal logic [2] we would call every *T-coalgebra* a frame irrespective of the choice of *L-algebra*. We do not do this as we already have a name for such entities - they are *T-coalgebras*. Therefore we reserve the name frame for only those *T-coalgebras* for which valuations exists, and this necessarily makes the concept of a frame one that is relative to a choice of *L-algebra*.

Now, as observed in [12], the logical connection allows every model diagram
in A to be redrawn in X as

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

where $f^b$ is the adjunct of $f$, and $\delta^*: TS \Rightarrow SL$ is defined following [8] as

$$
\delta^* = SL\rho \circ \delta^b S
$$

where $\rho$ is the unit of the logical connection. Such an $f^b$ we will call a theory map.

**Definition 11 (Models).** For an *L-algebra* $(A, \alpha)$ we define **Mod**$(A, \alpha)$, the category of **models** for $(A, \alpha)$, with objects given by *pairs*

$$
((X, \gamma), f : X \to S(A))
$$

where $(X, \gamma)$ is a *T-coalgebra*, and $f$ is a **theory map** (as above), and **morphisms**

$$
g: ((X_1, \gamma_1), f_1) \to ((X_2, \gamma_2), f_2)
$$

given by a *T-coalgebra morphism* $g: (X_1, \gamma_1) \to (X_2, \gamma_2)$ such that $f_1 = f_2 \circ g$.

In the above definition, the requirement on model morphisms that $f_1 = f_2 \circ g$
arises from the fact that theory maps need not be unique. In simple terms, we
have to ensure that any propositional variables are given interpretations in the
two models that are compatible with the *T*-coalgebra morphism.

In [4] a similar definition of a category of models for an *L-algebra* is made,
however this is done in terms of diagrams in *A* i.e. pairs of *T-coalgebras* and
valuations. In what follows next we prefer to work in *X*, but as already noted
above, and first observed in [12], the logical connection allows us to move freely
backwards and forwards between the two definitions. We can make this precise
with the following proposition.
**Proposition 12.** The natural transformation $\delta: LP \Rightarrow PT$ defines a functor $\tilde{P}: \mathbf{CoAlg}(T) \to \mathbf{Alg}(L)$ given by

$$ \tilde{P}(X, \gamma) = (P(X), P(\gamma) \circ \delta_X) \\ \tilde{P}(f) = P(f): \tilde{P}(Z, \xi) \to \tilde{P}(X, \gamma) $$

where $f: (X, \gamma) \to (Z, \xi)$, and for each $L$-algebra $(A, \alpha)$, $\mathbf{Mod}(A, \alpha)$ is dually isomorphic to the comma category $((A, \alpha) \downarrow \tilde{P})$.

We are now ready to introduce our key idea. Recall from Kripke semantics the notion of a canonical model [2]. This is a model of a modal logic constructed from the syntax itself. The idea is that when trying to prove completeness, by the way the canonical model is constructed from the syntax, for every formula that is not derivable, one can find a state that witnesses that the formula is not valid.

In such a canonical model the possible worlds are the theories of the logic. In our setup, $S(A)$ is the collection of all possible theories of $(A, \alpha)$, so an obvious question is when can we construct a model from $S(A)$ i.e. when can we put a $T$-coalgebra structure on $S(A)$ such that it becomes a model for $(A, \alpha)$?

In general this cannot be done, but in [14] conditions are given in the case of the standard logical connection between **BA** and **Set** (Example 8 (1)) for the existence of a, not necessarily unique, model for the initial $L$-algebra with carrier set $S(A)$. From this they derive a strong completeness result.

To illustrate our approach consider a toy example, where the logical connection consists of functors $P$ and $S$ given by the contravariant powerset functor on **Set**, the functors $L$ and $T$ both map every object to the two element set **2**, and $\delta_X(i) = \{i\}$ for $i \in \mathbf{2}$. Then the initial $L$-algebra is $(\mathbf{2}, \mathrm{id}_2)$, and a final $T$-coalgebra is given by $((\{0\}, \{1\}), \gamma)$, where $\gamma(\{i\}) = i$. Here it should be observed that the carrier set of the final coalgebra is clearly a proper subset of $S(\mathbf{2})$, so our approach is to consider not just models constructed from the whole of $S(A)$, but to consider models built from subobjects of $S(A)$. In other words, models where the theory map is a monomorphism.

**Definition 13 (Internal Models).** Given a class $M$ of monomorphisms in $\mathcal{X}$, we define the category $\mathbf{IntMod}_M(A, \alpha)$ to be the full subcategory of $\mathbf{Mod}(A, \alpha)$ where the theory maps are in $M$, and write

$$ G: \mathbf{IntMod}_M(A, \alpha) \to \mathbf{Mod}(A, \alpha) $$

for the corresponding inclusion functor.

We parameterise by the class $M$, as sometimes we require the morphisms of $M$ to have additional properties, for example, that the members of $M$ are preserved by $T$. In Example 24 (3) the Giry functor does not preserve all monomorphisms, but does preserve a particular subclass of them.

**Proposition 14.** The category $\mathbf{IntMod}_M(A, \alpha)$ is thin, and if for all $m \in M$ $\delta_A^* \circ T(m)$ is a monomorphism, then the forgetful functor from $\mathbf{IntMod}_M(A, \alpha)$ to $\mathbf{Sub}_M(S(A))$ is full.
*Proof.* Since the theory maps of internal models are monomorphisms the category **IntMod**<sub>*M*</sub>(A, α) is thin. For the second part, consider a pair of internal models I<sub>1</sub> and I<sub>2</sub>, and a morphism *g* in **Sub**<sub>*M*</sub>(S(A)) between the theory maps of I<sub>1</sub> and I<sub>2</sub>. We have to show that *g* is an internal model morphism, but this can be seen to easily follow if δ<sup>*</sup><sub>A</sub> ◦ T(m<sub>2</sub>) is a monomorphism, where m<sub>2</sub> is the theory map of I<sub>2</sub>. □

At this point we should provide some intuition for the condition on $\delta_A^* \circ T(m)$.
Indeed, in the rest of the paper we shall frequently see the slightly strengthened
condition $m \in M \Rightarrow \delta_A^* \circ T(m) \in M$. The reason for this particular formulation
of the condition is a technical one relating to use of the unique diagonalisation
property of a factorisation system, but we can motivate this choice as follows.

If we consider the logical connection of Example 8 (1) between **BA** and **Set**, and consider the finite powerset functor on **Set**, then as we shall see in Example 24 (1), we can choose *L* to add a finite meet preserving operator □ to each Boolean algebra (A, α), say the Lindenbaum-Tarski algebra of the logic **S4** (for some set of propositional variables), every state of an internal model for (A, α) has a distinct theory consisting of the set of formulae that are satisfied in that state. Informally, <fnref n="1" /> the function *S*(α) can then be thought of as taking each such theory *s*, and generating the set of formulae *a*, such that □*a* ∈ *s*. Since this set is an element in *SL*(A) it is also an ultrafilter. The function δ<sub>A</sub><sup>*</sup> ◦ T(*m*) therefore sends the set *U* of successors of a state *x*, to the set of formulae satisfied by all *x'* ∈ *U*, and these are precisely those in the theory of *x* that are prefixed with the □ operator. In this example, the condition that *m* ∈ *M* ⇒ δ<sub>A</sub><sup>*</sup> ◦ T(*m*) ∈ *M* means that in models where each state has a distinct theory, that for each finite set of possible successors, the set of formulae that are satisfied by all members of that set is also distinct.

The utility of internal models arises from the observation that in many cases
it is possible to take a model and "quotient by behavioural equivalence" i.e.
produce a smaller model by identifying states that are behaviourally equivalent.
Such a quotiented model will be an internal model, and we say the model factors
via the internal model.

The above is not very precise as we have not said what we mean by quotient
and behavioural equivalence. This will become clear in Section 7, but first we
make the following definition.

**Definition 15.** We say a model *X* in Mod(*A*, α) *factors via the internal model I* in IntMod*M*(*A*, α) *if there exists a morphism g: X → G(I) in Mod(*A*, α).*

It is possible to give very general conditions under which models factor via
internal models. The following proposition is essentially a restatement of [8,
Theorem 4.2] and [6, Theorem 4].

<footnote n="1">¹ The elements of *L*(A) are actually equivalence classes of elements of A arising from a free Boolean algebra construction over the underlying meet semilattice of A [10, Proposition 3.12].</footnote>
**Proposition 16.** If the category $\mathcal{X}$ has a factorisation system $(E, M)$ and

$$m \in M \Rightarrow \delta_A^* \circ T(m) \in M$$

then every model in $\mathbf{Mod}(A, \alpha)$ factors via an internal model in $\mathbf{IntMod}_M(A, \alpha)$.

*Proof.* Consider a model $((X, \gamma), f)$ in $\mathbf{Mod}(A, \alpha)$. Then by the factorisation system there exists $e \in E$ and $m \in M$ such that $f = m \circ e$, and by the definition of a model, the perimeter of the following diagram commutes

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

and by assumption $\delta_A^* \circ T(m) \in M$, and so by the diagonalisation property of the factorisation system, there exists a unique $\zeta: I \to T(I)$ making the diagram commute.

Thus $((I, \zeta), m)$ is an internal model in $\mathbf{IntMod}_M(A, \alpha)$, and $e$ is the morphism by which $((X, \gamma), f)$ factors via $((I, \zeta), m)$. $\square$

If the category $\mathcal{X}$ has a proper factorisation system $(E, M)$, factoring a model via an internal model, can be viewed as putting a $T$-coalgebra structure map on an $E$-quotient object of the state space of the model. As we will see in Section 7, this corresponds to quotienting with respect to behavioural equivalence.

We can also note that the construction of models is functorial. To see this, observe that since $\delta^*$ is a natural transformation, and $(g \circ f)^b = S(f) \circ g^b$, that we have the following proposition.

**Proposition 17.** For every $L$-algebra morphism $f: (A, \alpha) \to (A', \alpha')$ there exists a functor

$$\mathbf{Mod}(f): \mathbf{Mod}(A', \alpha') \to \mathbf{Mod}(A, \alpha) \\ ((X, \gamma), g^b) \mapsto ((X, \gamma), (g \circ f)^b) \\ h \mapsto h$$

where $h: ((X, \gamma), g^b) \to ((X', \gamma'), g'^b)$.

Can we construct a similar functor between the categories $\mathbf{IntMod}_M(A', \alpha')$ and $\mathbf{IntMod}_M(A, \alpha)$ for such an $L$-algebra morphism? The answer is yes whenever all models in $\mathbf{Mod}(A, \alpha)$ factor via an internal model in $\mathbf{IntMod}_M(A, \alpha)$.

**Theorem 18.** If the category $\mathcal{X}$ has a factorisation system $(E, M)$ and

$$m \in M \Rightarrow \delta_A^* \circ T(m) \in M$$
then for all L-algebra morphisms $f: (A, \alpha) \to (A', \alpha')$ there exists a functor

$$ \mathbf{IntMod}_M(f): \mathbf{IntMod}_M(A', \alpha') \to \mathbf{IntMod}_M(A, \alpha) \\ ((X, \gamma), g^b) \mapsto ((I, \zeta), m) \\ h \mapsto \mu $$

where $h: ((X, \gamma), g^b) \to ((X', \gamma'), g'^b)$, $(g \circ f)^b = m \circ e$, $(g' \circ f)^b = m' \circ e'$, and $\mu$ is the unique morphism in $\mathbf{IntMod}_M(A, \alpha)$ such that

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

*Proof.* By Proposition 16 $((X, \gamma), (g \circ f)^b)$ factors via $((I, \zeta), m)$ with $(g \circ f)^b = m \circ e$, and $((X', \gamma'), (g' \circ f)^b)$ factors via $((I', \zeta'), m')$ with $(g' \circ f)^b = m' \circ e'$. Then by the diagonalisation property of the factorisation system, there is a unique $\mu$ such that the above diagram commutes, and it is not hard to see that $\delta_A^* \circ T(m') \in M$ means that $\mu$ is a morphism in $\mathbf{IntMod}_M(A, \alpha)$. $\square$

# 5 Colimits in Mod($A$, $\alpha$) and IntMod$_M$($A$, $\alpha$)

As we shall see in future sections, one of the most important aspects of the structure of the categories $\mathbf{Mod}(A, \alpha)$ and $\mathbf{IntMod}_M(A, \alpha)$ is the presence, or otherwise, of colimits. In this section we shall see that in the case of the category $\mathbf{Mod}(A, \alpha)$, the forgetful functor from $\mathbf{Mod}(A, \alpha)$ to $\mathcal{X}$ creates small colimits, but that for the category $\mathbf{IntMod}_M(A, \alpha)$, the corresponding forgetful functor does not. However, under certain additional conditions it does detect small colimits, but does not necessarily preserve them.

We define the following forgetful functors

$$ \begin{align*} U: \mathbf{CoAlg}(T) &\to \mathcal{X} \\ V: \mathbf{Mod}(A, \alpha) &\to \mathcal{X} \\ V^*: \mathbf{Mod}(A, \alpha) &\to \mathbf{CoAlg}(T) \\ W: \mathbf{IntMod}_M(A, \alpha) &\to \mathcal{X} \end{align*} $$

where $V = UV^*$ and $W = VG$.

To start we state without proof the well known result (see for example [13] for the case in **Set**) that the forgetful functor $U: \mathbf{CoAlg}(T) \to \mathcal{X}$ creates small colimits.

**Theorem 19.** The forgetful functor $U: \mathbf{CoAlg}(T) \to \mathcal{X}$ creates small colimits.

The case for the forgetful functor $V: \mathbf{Mod}(A, \alpha) \to \mathcal{X}$ follows in a similar fashion, with the additional detail that a theory map must be constructed for the colimit.
**Theorem 20.** The forgetful functor $V: \mathbf{Mod}(A, \alpha) \to \mathbb{X}$ creates small colimits.

*Proof.* Consider a small category $\mathcal{J}$ and a functor $D: \mathcal{J} \to \mathbf{Mod}(A, \alpha)$, and suppose that $\mathbb{X}$ has colimits of shape $\mathcal{J}$. Then we have that $VD$ has a colimit $(C, \phi_j : VD(j) \to C)_{j \in \mathcal{J}}$. We now proceed as follows (sketch):

1. Use the functor $V^*$ and Theorem 19 to construct a colimiting $T$-coalgebra $(C, \chi)$.

2. Use the theory maps and the universal property of $C$ to construct a morphism $g$ from $C$ to $S(A)$.

3. Use the universal property of $C$ to show that there is a unique morphism from $C$ to $SL(A)$ and that this makes $g$ into a theory map, $((C, \chi), g)$ a model, and the $\phi_j$ model morphisms.

4. For another cocone of $D$ use the functor $V^*$ and the universal property of $(C, \chi)$ to construct a unique mediating morphism to the underlying $T$-coalgebra.

5. Use the uniqueness of $g$ to show that the mediating morphism is a model morphism, and thus $((C, \chi), g)$ is the colimit of $D$.

It is clear that $(((C, \chi), g), \phi_j : D(j) \to ((C, \chi), g))_{j \in \mathcal{J}}$ is the unique cocone for $D$ that is mapped by $V$ to the colimit $(C, \phi)$ of $VD$. Thus we can conclude that $V$ creates colimits of shape $\mathcal{J}$. $\square$

For the category $\mathbf{IntMod}_M(A, \alpha)$ the details are more complicated. The approach we take is that the colimit is constructed in $\mathbf{Mod}(A, \alpha)$, and then the resulting colimiting model is factored via an internal model using Proposition 16.

**Theorem 21.** Given an $L$-algebra $(A, \alpha)$, if the following hold:

1. the category $\mathbb{X}$ has a factorisation system $(E, M)$,

2. $m \in M \Rightarrow \delta_A^* \circ T(m) \in M,$

then the forgetful functor $W: \mathbf{IntMod}_M(A, \alpha) \to \mathbb{X}$ detects small colimits.

*Proof.* Consider a small category $\mathcal{J}$ and a functor $D: \mathcal{J} \to \mathbf{IntMod}_M(A, \alpha)$, and suppose that $\mathbb{X}$ has colimits of shape $\mathcal{J}$. Then by Theorem 20, the functor $GD$ has the colimit $(((C, \chi), g), \tau_j : GD(j) \to ((C, \chi), g))_{j \in \mathcal{J}}$ in $\mathbf{Mod}(A, \alpha)$. We now proceed as follows (sketch):

1. Use Proposition 16 to factor $((C, \chi), g)$ via an internal model $((I, \zeta), m)$ by $e: ((C, \chi), g) \to ((I, \zeta), m)$.

2. For another cocone $(((Z, \xi), h), \psi_j : D(j) \to ((Z, \xi), h))_{j \in \mathcal{J}}$ of $D$ there is a unique mediating morphism $\mu: ((C, \chi), g) \to ((Z, \xi), h)$ in $\mathbf{Mod}(A, \alpha)$.

3. The uniqueness of $g$ means $g = h \circ V(\mu)$, then use the diagonalisation property of the factorisation system to construct a unique $\eta: I \to Z$.

4. Use $\delta_A^* \circ T(h) \in M$ and thus a monomorphism to show that $\eta$ is an internal model morphism, and $(((I, \zeta), m), e \circ \tau_j : D(j) \to ((I, \zeta), m))_{j \in \mathcal{J}}$ is the colimit of $D$. $\square$
# 6 An Adjoint Functor Theorem

As a simple example to show the utility of the categories $\mathbf{IntMod}_M(A, \alpha)$ we prove an adjoint functor theorem.

To find a functor $\tilde{S}: \mathbf{Alg}(L) \to \mathbf{CoAlg}(T)$ that together with $\tilde{P}$ forms a dual adjunction between $\mathbf{Alg}(L)$ and $\mathbf{CoAlg}(T)$ we must show that for every $L$-algebra there is a universal morphism to $\tilde{P}$. But this is the same as requiring that each comma category $((A, \alpha) \downarrow \tilde{P})$ has an initial object.

**Theorem 22.** If for all $L$-algebras $(A, \alpha)$ the following hold:

1. every model in $\mathbf{Mod}(A, \alpha)$ factors via some model in $\mathbf{IntMod}_M(A, \alpha)$,

2. $\mathbf{IntMod}_M(A, \alpha)$ has a final object,

then there exists a dual adjunction between $\mathbf{Alg}(L)$ and $\mathbf{CoAlg}(T)$.

*Proof.* We are required to show that for any $L$-algebra $(A, \alpha)$ that $((A, \alpha) \downarrow \tilde{P})$ has an initial object. But by Proposition 12 this is the same as requiring that each $\mathbf{Mod}(A, \alpha)$ has a final object.

Consider such a $\mathbf{Mod}(A, \alpha)$. By the two premises above, every model in $\mathbf{Mod}(A, \alpha)$ factors via the final object in $\mathbf{IntMod}_M(A, \alpha)$, and since the theory map of the final internal model is a monomorphism, the morphism from a model in $\mathbf{Mod}(A, \alpha)$ to the final internal model is unique. Thus the final object in $\mathbf{IntMod}_M(A, \alpha)$ is the final object in $\mathbf{Mod}(A, \alpha)$. $\square$

In the above proof, no explicit use was made of the class $M$, only that $\mathbf{IntMod}_M(A, \alpha)$ is a special subcategory of $\mathbf{Mod}(A, \alpha)$ - it has a final object, and for all objects in $\mathbf{Mod}(A, \alpha)$ there exists a unique morphism to an object in $\mathbf{IntMod}_M(A, \alpha)$. Therefore for each $L$-algebra a different class $M$ of monomorphisms could in principle be chosen, but typically the same class would be used for all $L$-algebras. Indeed, the choice of $M$ is likely to be driven by the properties of the base category $\mathcal{X}$ and the functor $T$, as in the following corollary.

**Corollary 23.** If the following hold:

1. $\mathcal{X}$ has a factorisation system $(E, M)$, is $M$-wellpowered, and has small co-products,

2. for all $L$-algebras $(A, \alpha)$ we have $m \in M \Rightarrow \delta_A^* \circ T(m) \in M$,

then there is a dual adjunction between $\mathbf{Alg}(L)$ and $\mathbf{CoAlg}(T)$.

*Proof.* By Proposition 16, for every $L$-algebra, every model in $\mathbf{Mod}(A, \alpha)$ factors via an internal model in $\mathbf{IntMod}_M(A, \alpha)$.

Now since $\mathcal{X}$ is $M$-wellpowered, by Proposition 7, the objects of $\mathbf{Sub}_M(A)$ can be partitioned into a set of equivalence classes. Also by Proposition 14, the forgetful functor from $\mathbf{IntMod}_M(A, \alpha)$ to $\mathbf{Sub}_M(A)$ is full and $\mathbf{IntMod}_M(A, \alpha)$ is thin. Therefore the objects of $\mathbf{IntMod}_M(A, \alpha)$ can also be partitioned into a set of equivalence classes, and since $\mathcal{X}$ has small coproducts, by Theorem 21, the coproduct of a representative from each equivalence class exists. Further,
since $\mathbf{IntMod}_M(A, \alpha)$ is thin, and between each pair of representatives of an
equivalence class there exists an isomorphism, the injections into the coproduct
yield a unique morphism from each object of $\mathbf{IntMod}_M(A, \alpha)$ to the coproduct.
Thus the coproduct is the final object in $\mathbf{IntMod}_M(A, \alpha)$.

Finally by Theorem 22 we have the result. □

In most cases, for a particular choice of $\mathcal{X}$, the existence of a factorisation
system, wellpoweredness, and the existence of small coproducts, is well known.
Further, it is often straightforward to show that $T$ preserves $M$, thus by Proposi-
tion 4, what is left to show is that $\delta^*$ is componentwise in $M$, and this is typically
where the bulk of the work lies.

Example 24.

1. Example 8 (1): **Set** clearly satisfies the premises of Corollary 23 with the usual factorisation system given by surjective and injective functions. Then if we take $T$ to be the finite powerset functor $\mathcal{P}_f$, and $L$ to be the functor that adds a finite meet preserving operator $\square$ to a Boolean algebra, it is shown in [6, Theorem 9] that for a natural choice of $\delta$, that $\delta^*$ is componentwise injective. From this, and that $\mathcal{P}_f$ preserves injections, Corollary 23 yields a dual adjunction between **Alg**($L$) and **CoAlg**($\mathcal{P}_f$).

2. Example 8 (3): Again take **Set** with the usual factorisation system. This time take $T$ to be the valuation functor $\mathcal{V}_O$ of [6, Section 3.1]. This is a generalisation of the finite powerset, finitely supported discrete subdistribution, and finitely supported multiset functors. $O$ is a downward-closed subset of a partially ordered commutative cancellative monoid $M$, and $M$ also has the property $x \leq x + y$ for all $x, y \in M$. Then the valuation functor sends a set to the set of its valuations in $O$

$$ \mathcal{V}_O(X) = \{\phi: X \to O \mid \text{supp}(\phi) \text{ is finite and } \sum_{x \in X} \phi(x) \in O\} $$

The analogous generalisation of $L$ in the previous example is $K_{\hat{O}}$, where $\hat{O}$ is a dense subset of $O$, and this functor adds to a meet semilattice an order preserving modality $\square_o$ for each $o \in \hat{O}$. It is shown in [6, Theorem 13] that for a natural choice of $\delta$, that the resulting $\delta^*$ is componentwise injective. From this, and that $\mathcal{V}_O$ preserves injections, Corollary 23 yields a dual adjunction between $\mathbf{Alg}(K_{\hat{O}})$ and $\mathbf{CoAlg}(\mathcal{V}_O)$.

3. Example 8 (4): Since $\sigma$-algebras are closed under intersection, **Meas** is topological over **Set**, and since **Meas** is fibre-small, by [1, Theorem 21.16], **Meas** is wellpowered and cocomplete. Also in [6, Section 3.1] it is observed that morphisms with surjective underlying functions, and morphisms with injective underlying functions and surjective inverse image functions, form a factorisation system $(E, M)$. Moreover, the Giry functor (or monad) $G$ is observed to preserve $M$. For $L$ take $K$, an instance of $K_{\hat{O}}$ above, for $\hat{O} = \mathbb{Q} \cap [0, 1]$. Then for a natural choice of $\delta$, it is shown in [6, Theorem 17] that $\delta^*$ is componentwise in $M$. From this, Corollary 23 yields a dual adjunction between $\mathbf{Alg}(K)$ and $\mathbf{CoAlg}(G)$.
# 7 Expressivity

The notion of expressivity for a coalgebraic modal logic states that two states are logically equivalent if and only if they are behaviourally equivalent. Here logically equivalent means "have the same theory", and behaviourally equivalent means "can be identified in a model", where the identification is by means of coalgebra homomorphisms.

To investigate expressivity we need to access individual states of objects in $X$, so we make the additional assumption:

**Assumption 1.** The category $X$ is a concrete category [1] i.e. the objects are sets with some additional structure, and the morphisms have underlying functions. Technically this means we assume there is a faithful forgetful functor from $X$ to the category Set.

**Definition 25.** Given two models $X_1, X_2$ in Mod($A, \alpha$), and states $x_1 \in X_1$, $x_2 \in X_2$, we say $x_1$ and $x_2$ are logically equivalent if

$$f_1(x_1) = f_2(x_2)$$

where $f_1$ and $f_2$ are the theory maps of $X_1$ and $X_2$ respectively.

**Definition 26.** Given two models $X_1, X_2$ in Mod($A, \alpha$), and states $x_1 \in X_1$, $x_2 \in X_2$, we say $x_1$ and $x_2$ are behaviourally equivalent if there exists in Mod($A, \alpha$) a cospan

$$X_1 \xrightarrow{g_1} X_3 \leftarrow \xrightarrow{g_2} X_2$$

such that $g_1(x_1) = g_2(x_2)$.

Our definition extends the standard definition of behavioural equivalence. The forgetful functor from Mod($A, \alpha$) to CoAlg($T$) yields the usual definition of behavioural equivalence as a cospan in CoAlg($T$) [9], but in addition, the forgetful functor to $X$ yields a condition that the theory maps are compatible. This is because we are working with arbitrary $L$-algebras, and not just the initial $L$-algebra, and is similar to the definition of bisimulation in [2].

We have the following obvious result and definition.

**Proposition 27.** Given two models $X_1, X_2$ in Mod($A, \alpha$), and states $x_1 \in X_1$, $x_2 \in X_2$, if $x_1$ and $x_2$ are behaviourally equivalent then $x_1$ and $x_2$ are logically equivalent.

**Definition 28.** An $L$-algebra $(A, \alpha)$ is *expressive* for Mod($A, \alpha$) if for all models in Mod($A, \alpha$), states are logically equivalent if and only if they are behaviourally equivalent.

To use internal models to investigate the phenomena of expressivity we must choose the class $M$ to be a subclass of the class of monomorphisms that have injective underlying functions. See Example 36 (3) for a case where $M$ is chosen to be a strict subclass.
**Theorem 29.** Given an L-algebra $(A, \alpha)$, and if $M$ is a subclass of the class of monomorphisms in $\mathcal{X}$ that have injective underlying functions, then if the following hold:

1. every model in $\mathbf{Mod}(A, \alpha)$ factors via some model in $\mathbf{IntMod}_M(A, \alpha)$,

2. for every pair $I_1, I_2$ in $\mathbf{IntMod}_M(A, \alpha)$ there is a cospan $I_1 \to I_3 \leftarrow I_2$ in $\mathbf{IntMod}_M(A, \alpha)$,

then $(A, \alpha)$ is expressive for $\mathbf{Mod}(A, \alpha)$.

*Proof.* Take any pair of models $X_1$ and $X_2$ in $\mathbf{Mod}(A, \alpha)$. Then these factor via the internal models $I_1$ and $I_2$ respectively, and by assumption there exists an internal model $I_3$ such that there exists a cospan $I_1 \to I_3 \leftarrow I_2$ in $\mathbf{IntMod}_M(A, \alpha)$. Thus both $X_1$ and $X_2$ factor via $I_3$.

Spelling this out, the models $((X_1, \gamma_1), f_1)$ and $((X_2, \gamma_2), f_2)$ factor via the internal model $((I_3, \zeta_3), m_3)$ via T-coalgebra morphisms $g_1: (X_1, \gamma_1) \to (I_3, \zeta_3)$ and $g_2: (X_2, \gamma_2) \to (I_3, \zeta_3)$ such that $f_1 = m_3 \circ g_1$ and $f_2 = m_3 \circ g_2$.

Now suppose two states $x_1 \in X_1$ and $x_2 \in X_2$ are logically equivalent for $(A, \alpha)$. Then $f_1(x_1) = f_2(x_2)$, which means $m_3 \circ g_1(x_1) = m_3 \circ g_2(x_2)$, and since $m_3$ is injective, $g_1(x_1) = g_2(x_2)$, and $x_1$ and $x_2$ are behaviourally equivalent.

The converse direction is given by Proposition 27. □

In addition to Assumption 1, for several of the results that follow we will also need to make assumptions about the category $\mathbf{Mod}(A, \alpha)$. Whenever we require these additional assumptions this will be indicated in the premises of the relevant proposition, lemma, or theorem.

**Assumption 2.** Given an L-algebra $(A, \alpha)$ the category $\mathbf{Mod}(A, \alpha)$ has small pushouts, a factorisation system $(E_{\mathbf{Mod}(A,\alpha)}, M_{\mathbf{Mod}(A,\alpha)})$, and is $E_{\mathbf{Mod}(A,\alpha)}$-cowellpowered, where $M_{\mathbf{Mod}(A,\alpha)}$ is a subclass of those morphisms in $\mathbf{Mod}(A, \alpha)$ with injective underlying functions, and $E_{\mathbf{Mod}(A,\alpha)}$ is a subclass of those morphisms in $\mathbf{Mod}(A, \alpha)$ with surjective underlying functions.

Note that there is a forgetful functor from $\mathbf{Mod}(A, \alpha)$ to Set since $\mathcal{X}$ is a concrete category, and further, since faithful functors reflect monomorphisms and epimorphisms [1, Propositions 7.37 and 7.44], we have

$$M_{\mathbf{Mod}(A,\alpha)} \subseteq \mathrm{Inject}_{\mathbf{Mod}(A,\alpha)} \subseteq \mathrm{monos in} \ \mathbf{Mod}(A, \alpha)$$

$$E_{\mathbf{Mod}(A,\alpha)} \subseteq \mathrm{Surject}_{\mathbf{Mod}(A,\alpha)} \subseteq \mathrm{epis in} \ \mathbf{Mod}(A, \alpha)$$

where $\mathrm{Inject}_{\mathbf{Mod}(A,\alpha)}$ is the class of morphisms in $\mathbf{Mod}(A, \alpha)$ with injective underlying functions, and $\mathrm{Surject}_{\mathbf{Mod}(A,\alpha)}$ those with surjective underlying functions.

Using Assumption 2 we can prove a converse to Theorem 29. The most difficult part is the proof that expressivity of $(A, \alpha)$ for $\mathbf{Mod}(A, \alpha)$ implies that all models factor via internal models. The reason for this is that, whilst it is intuitively obvious that since we think of a theory map as having an underlying function it ought to factor via its image, the construction of a T-coalgebra
structure map on this image need not be straightforward. We therefore need
to ensure that any operations we might perform on a model always result in
another model.

**Theorem 30.** Given an L-algebra $(A, \alpha)$, and with the following assumptions:

1. the conditions of Assumption 2 hold,

2. the class $M$ of monomorphisms used to define $\text{IntMod}_M(A, \alpha)$ is precisely the class of morphisms with injective underlying functions,

if $(A, \alpha)$ is expressive for $\text{Mod}(A, \alpha)$ then every model in $\text{Mod}(A, \alpha)$ factors via an internal model in $\text{IntMod}_M(A, \alpha)$.

*Proof.* We proceed as follows:

1. All model morphisms have an $(E_{\text{Mod}(A,\alpha)}, M_{\text{Mod}(A,\alpha)})$-factorisation:
Any model morphism $g: ((X, \gamma), f) \to ((X', \gamma'), f')$ factors via a model $((I, \zeta), f' \circ m)$, where $g = m \circ e$, and $e: ((X, \gamma), f) \to ((I, \zeta), f' \circ m)$ is in $E_{\text{Mod}(A,\alpha)}$ and $m: ((I, \zeta), f' \circ m) \to ((X', \gamma'), f')$ is in $M_{\text{Mod}(A,\alpha)}$.

2. Take the pushout of the $E_{\text{Mod}(A,\alpha)}$-quotient objects of $((X, \gamma), f)$:
Given a model $((X, \gamma), f)$, since $\text{Mod}(A, \alpha)$ is $E_{\text{Mod}(A,\alpha)}$-cowellpowered, the collection of equivalence classes of $E_{\text{Mod}(A,\alpha)}$-quotient objects is indexed by a set $J$, and we can therefore take the pushout of a representative from each equivalence class $\coprod_{<e_j>} ((I_j, \zeta_j), f_j)$, which by Theorem 20 we can write as $((\coprod_{<e_j>} I_j, \zeta), f^\dagger)$ for some $\zeta$ and $f^\dagger$. This gives the following diagram

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

where any $g: ((X, \gamma), f) \to ((X', \gamma'), f')$ factors via a representative of one of the equivalence classes.

3. Construct a model epimorphism $h: ((X, \gamma), f) \to ((\coprod_{<e_j>} I_j, \zeta), f^\dagger)$:
By the definition of a pushout there is a morphism $h = p_j \circ e_j$ for all $j \in J$ in $\text{Mod}(A, \alpha)$. To show that this is an epimorphism we use the fact that the forgetful functor $V: \text{Mod}(A, \alpha) \to \mathcal{X}$ reflects epimorphisms. Given any parallel pair of morphisms $u$ and $v$ in $\text{Mod}(A, \alpha)$ where $V(u), V(v): \coprod_{<e_j>} I_j \to Y$, if $u \circ h = v \circ h$, then $u \circ p_j \circ e_j = v \circ p_j \circ e_j$, but since $e_j$ is an epimorphism,
we must have $u \circ p_j = v \circ p_j = q_j$ as in the following diagram

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

Clearly the $q_j$ form a cocone for the pushout, so by the universal property of the pushout $u = v$, and thus $h$ is an epimorphism.

4. Show $h, p_j \in E_{\mathbf{Mod}(A,\alpha)}$ for all $j \in J$:
If we take the $(E_{\mathbf{Mod}(A,\alpha)}, M_{\mathbf{Mod}(A,\alpha)})$-factorisation of $h$ in $\mathbf{Mod}(A, \alpha)$ given by $e$ and $m$, then by the diagonalisation property of the factorisation system, there exists a unique $\mathbf{Mod}(A, \alpha)$ morphism $\mu_j$ for each $j \in J$ such that the following diagram commutes

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

Once again the $\mu_j$ form a cocone for the pushout, so there exists a unique $\mathbf{Mod}(A, \alpha)$ morphism $\eta: \coprod_{<e_j>} I_j \to I$ such that $\mu_j = \eta \circ p_j$. Now trivially $\mathrm{id}_I \circ e = e$, and also $\eta \circ m \circ e = \eta \circ m \circ \mu_j \circ e_j = \eta \circ p_j \circ e_j = \mu_j \circ e_j = e$ so since $e$ is an epimorphism we must have $\eta \circ m = \mathrm{id}_I$. Similarly, we have $\mathrm{id}_{\coprod_{<e_j>} I_j} \circ h = h$, and $m \circ \eta \circ h = m \circ \eta \circ p_j \circ e_j = m \circ \mu_j \circ e_j = p_j \circ e_j = h$ and since $h$ is also an epimorphism, we must have $m \circ \eta = \mathrm{id}_{\coprod_{<e_j>} I_j}$. From this we deduce that $m$ is an isomorphism, and therefore $h \in E_{\mathbf{Mod}(A,\alpha)}$, and so by Proposition 4, $p_j \in E_{\mathbf{Mod}(A,\alpha)}$ for all $j \in J$.

5. Show that $f^\dagger$ has an underlying injective function:
Since $\coprod_{<e_j>} I_j$ has an underlying set we can pick a pair of states $w_1, w_2 \in \coprod_{<e_j>} I_j$. Now since $h \in E_{\mathbf{Mod}(A,\alpha)}$ is a surjective function, there exists states $x_1, x_2 \in X$ such that $w_1 = h(x_1)$ and $w_2 = h(x_2)$. Thus if $f^\dagger(w_1) = f^\dagger(w_2)$ then $f(x_1) = f(x_2)$, and by expressivity there must exist a $g: ((X, \gamma), f) \to ((X', \gamma'), f')$ such that $g(x_1) = g(x_2)$, and therefore a $j \in J$ such that $m_j \circ e_j(x_1) = m_j \circ e_j(x_2)$. However, since $m_j \in M_{\mathbf{Mod}(A,\alpha)}$, we have that $m_j$ is injective, therefore $e_j(x_1) = e_j(x_2)$. Thus $p_j \circ e_j(x_1) = p_j \circ e_j(x_2)$, which implies $h(x_1) = h(x_2)$, and therefore $w_1 = w_2$. Therefore $f^\dagger$ has an injective underlying function.

6. Observe that this makes $((\coprod_{<e_j>} I_j, \zeta), f^\dagger)$ an internal model:
Since $\mathrm{IntMod}_M(A, \alpha)$ is defined in terms of precisely those morphisms with underlying injective functions, the model $((\coprod_{<e_j>} I_j, \zeta), f^\dagger)$ is an object in $\mathrm{IntMod}_M(A, \alpha)$. $\square$
*Remark 31.* It should be noted that the statement of Theorem 30 requires that the category of internal models that we consider include all models with an injective theory map. If we had instead tried to consider only models with theory maps that are, say, embeddings, Theorem 30 would fail to hold, as expressivity is not in general a strong enough condition to ensure $f^\dagger$ is an embedding (consider topological spaces where injective continuous functions need not be embeddings).

**Corollary 32.** Given an L-algebra $(A, \alpha)$, and with the following assumptions:

1. the conditions of Assumption 2 hold,

2. $\mathbf{Mod}(A, \alpha)$ has binary coproducts,

3. the class $M$ of monomorphisms used to define $\mathbf{IntMod}_M(A, \alpha)$ is precisely the class of morphisms with injective underlying functions,

if $(A, \alpha)$ is expressive for $\mathbf{Mod}(A, \alpha)$ then for every pair $I_1, I_2$ in $\mathbf{IntMod}_M(A, \alpha)$ there is a cospan $I_1 \to I_3 \leftarrow I_2$ in $\mathbf{IntMod}_M(A, \alpha)$.

*Proof.* Given two internal models $I_1$ and $I_2$, since they are also models their coproduct exists, and by Theorem 30 the coproduct factors via an internal model, say $I_3$, and this induces an obvious cospan between $I_1$ and $I_2$. □

From Theorems 29, 30, and Corollary 32 we obtain our main expressivity result - an abstract, category theoretic, characterisation of expressivity.

**Theorem 33.** Given an L-algebra $(A, \alpha)$, and with the following assumptions:

1. the conditions of Assumption 2 hold,

2. $\mathbf{Mod}(A, \alpha)$ has binary coproducts,

3. the class $M$ of monomorphisms used to define $\mathbf{IntMod}_M(A, \alpha)$ is precisely the class of morphisms with injective underlying functions,

$(A, \alpha)$ is expressive for $\mathbf{Mod}(A, \alpha)$ if and only if

1. every model in $\mathbf{Mod}(A, \alpha)$ factors via an internal model in $\mathbf{IntMod}_M(A, \alpha)$,

2. for every pair $I_1, I_2$ in $\mathbf{IntMod}_M(A, \alpha)$ there is a cospan $I_1 \to I_3 \leftarrow I_2$ in $\mathbf{IntMod}_M(A, \alpha)$.

The conditions of Assumption 2 follow from appropriate conditions on the category $\mathcal{X}$ and the functor $T$. Indeed, such conditions on $\mathcal{X}$ essentially summarise the category theoretic properties of **Set** that underpin the intuitive understanding that models with injective theory maps fully capture the notion of expressivity. This is made precise in the following corollary.

**Corollary 34.** Given an L-algebra $(A, \alpha)$, and with the following assumptions:

1. $\mathcal{X}$ is a concrete category (over **Set**) that is cocomplete, has a factorisation system $(E_\mathcal{X}, M_\mathcal{X})$, and is $E_\mathcal{X}$-cowellpowered, where $M_\mathcal{X}$ is chosen to be a subclass of those morphisms in $\mathcal{X}$ with injective underlying functions, and $E_\mathcal{X}$ is chosen to be a subclass of those morphisms in $\mathcal{X}$ with surjective underlying functions,
2. $T$ preserves $M_X$ i.e. $m \in M_X \Rightarrow T(m) \in M_X$,

3. the class $M$ of monomorphisms used to define $\text{IntMod}_M(A, \alpha)$ is precisely the class of morphisms with injective underlying functions i.e. $M_X \subseteq M$,

$(A, \alpha)$ is expressive for $\text{Mod}(A, \alpha)$ if and only if

1. every model in $\text{Mod}(A, \alpha)$ factors via an internal model in $\text{IntMod}_M(A, \alpha)$,

2. for every pair $I_1, I_2$ in $\text{IntMod}_M(A, \alpha)$ there is a cospan $I_1 \to I_3 \leftarrow I_2$ in $\text{IntMod}_M(A, \alpha)$.

*Proof.* We have to show that the premises of Theorem 33 hold. Firstly we observe that by Theorem 20 $\text{Mod}(A, \alpha)$ is cocomplete.

To show that the factorisation system of $\mathcal{X}$ lifts to $\text{Mod}(A, \alpha)$ we note that in [6] it is observed that if $T$ preserves $M_X$, and the members of $M_X$ are monomorphisms, then the factorisation system of $\mathcal{X}$ lifts to $\text{CoAlg}(T)$, and it is easy to see that this extends to $\text{Mod}(A, \alpha)$.

Finally, $\text{Mod}(A, \alpha)$ is $E_X$-cowellpowered since the morphisms in $E_X$ are epimorphisms, and this ensures that given a span in $\text{Mod}(A, \alpha)$ where the underlying morphisms are in $E_X$, there is an isomorphism between the two so defined $E_X$-quotient objects in $\text{Mod}(A, \alpha)$, if and only if, there is an isomorphism between the underlying $E_X$-quotient objects in $\mathcal{X}$. $\square$

The above characterisation of expressivity, whilst providing a neat, element free definition of expressivity, is not very useful for proving a given $L$-algebra is expressive for its category of models. For this we have a direct corollary of Theorem 29 that generalises [8, Theorem 4.2] and [6, Theorem 4] (they only consider the initial $L$-algebra and pairs of states in the same $T$-coalgebra).

**Corollary 35.** If given an $L$-algebra $(A, \alpha)$ the following hold:

1. $\mathcal{X}$ is a concrete category (over **Set**) with binary coproducts, and a factorisation system $(E, M)$, where $M$ is a subclass of the class of monomorphisms in $\mathcal{X}$ that have injective underlying functions,

2. $m \in M \Rightarrow \delta_A^* \circ T(m) \in M$,

then $(A, \alpha)$ is expressive for $\text{Mod}(A, \alpha)$.

*Proof.* By Proposition 16 every model in $\text{Mod}(A, \alpha)$ factors via an internal model in $\text{IntMod}_M(A, \alpha)$. Also since $\mathcal{X}$ has binary coproducts, by Theorem 21 the coproduct of every pair of objects in $\text{IntMod}_M(A, \alpha)$ exists. So by Theorem 29 we have the result. $\square$

An examination of corollaries 23 and 35 reveals that with the exception of the exact choice of the class $M$, the primary difference is between requiring the base category $\mathcal{X}$ have all small coproducts or just binary coproducts. In most categories of interest finite cocompleteness usually also means cocompleteness, and so the existence of a dual adjunction between $\text{Alg}(L)$ and $\text{CoAlg}(T)$ essentially amounts to every $L$-algebra being expressive for its class of models.
*Example 36.*

1. Example 24 (1): Every $L$-algebra $(A, \alpha)$ is expressive for $\mathbf{Mod}(A, \alpha)$. The category $\mathbf{Alg}(L) \cong \mathbf{MA}$ (the category of modal algebras). Thus given a set of propositional variables, the free modal algebra over that set, quotiented by a set of axioms, represents a basic modal logic that is expressive for the image finite transition systems that are models for that logic.

2. Example 24 (2): Every $K_{\hat{O}}$-algebra $(A, \alpha)$ is expressive for $\mathbf{Mod}(A, \alpha)$. The category $\mathbf{Alg}(K_{\hat{O}})$ is isomorphic to the category of meet semilattices each with a set of order preserving unary operations of cardinality $|\hat{O}|$. Thus if

(a) $\hat{O} = O = M = \mathbb{N}$, the monoid with $(0, +)$, then $\mathbf{Alg}(K_{\hat{O}})$ is isomorphic to the algebras for the signature $\{\top, \wedge, \diamond_k\}_{k \in \mathbb{N}}$, where $\{\top, \wedge\}$ define a meet semilattice with top, and the $\diamond_k$ are order preserving. Thus the conjunction fragment of graded modal logic, over an arbitrary set of proposition variables and axioms, is expressive for the multi-transition systems that are models for that logic.

(b) Similarly, if $M = (\mathbb{R}^{\ge 0}, +, 0)$, $O = [0, 1]$, and $\hat{O} = \mathbb{Q} \cap [0, 1]$, then finite conjunction modal logic, over an arbitrary set of proposition variables and axioms, with the standard probabilistic modalities, is expressive for the Markov chains that are models for that logic.

3. Example 24 (3): Every $K$-algebra $(A, \alpha)$ is expressive for $\mathbf{Mod}(A, \alpha)$. The category $\mathbf{Alg}(K)$ is isomorphic to the category of meet semilattices each with a countable set of order preserving unary operations. Thus a modal logic with finite conjunctions and probabilistic modalities, over an arbitrary set of propositional variables and axioms, is expressive for the Markov processes that are models for that logic.

These examples are generalisations of the results in [6] to arbitrary $L$-algebras, not just the initial $L$-algebra, and thus in particular to modal logics with propositional variables and additional axioms. The results of [6] can be retrieved by taking the initial $L$-algebra, and then every $T$-coalgebra can be made into a model via a unique choice of theory map (forced by initiality).

# 8 Conclusions and Future Work

We have introduced internal models for a modal logic, and shown their utility for exploring properties of a logic. Indeed, it should be noted that with the exception of the proofs of the existence of colimits in $\mathbf{Mod}(A, \alpha)$ and $\mathbf{IntMod}_M(A, \alpha)$, and the proof that expressivity implies that models factor via internal models, the proofs using internal models are relatively short. Most of the structure of $\mathbf{Mod}(A, \alpha)$ is related to whether models always factor via internal models.

The category $\mathbf{IntMod}_M(A, \alpha)$ is not yet fully understood, and indeed, an obvious question is that, given that internal models can be thought of as generalisations of the canonical models of Kripke semantics, do internal models
have anything to say about completeness? To answer this will require a sys-
tematic treatment of the different possible notions of semantic consequence that
can be defined for the coalgebraic semantics of modal logics - local/global, and
frame/model.

Several authors have used enriched categories in their work on coalgebras
[5,7], and an interesting question is how much of the work of this paper will
translate to the enriched setting, and what new phenomena can be addressed
in such an enriched framework? Some preliminary work towards answering this
question has been started.

**Acknowledgements.** The author would like to thank Corina Cîrstea for the many interesting discussions, her invaluable guidance, and her careful proof reading. Many thanks also go to John Power for his detailed feedback on an early draft of this paper, and to the anonymous referees for their encouraging feedback and useful suggestions.

**References**

1. Adámek, J., Herrlich, H., Strecker, G.E.: Abstract and Concrete Categories. Wiley New York, 1990.

2. Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, 2001.

3. Danos, V., Desharnais, J., Laviolette, F., Panangaden, P.: Bisimulation and cocongruence for probabilistic systems. Information and Computation 204(4):503–523, 2006.

4. Doberkat, E.-E.: Stochastic Coalgebraic Logic. Springer Berlin Heidelberg, 2009.

5. Hasuo, I.: Generic forward and backward simulations. Lecture Notes in Computer Science 4137:406–420, 2006.

6. Jacobs, B., Sokolova, A.: Exemplaric Expressivity of Modal Logics. Journal of Logic and Computation 20(5):1041–1068, 2010.

7. Kapulkin, K., Kurz, A., Velebil, J.: Expressivity of Coalgebraic Logic over Posets. CMCS 2010 Short contributions CWI Technical report SEN-1004:16–17, 2010.

8. Klin, B.: Coalgebraic modal logic beyond sets. Electronic Notes in Theoretical Computer Science 173:177–201, 2007.

9. Kupke, C., Kurz, A., Pattinson, D.: Algebraic semantics for coalgebraic logics. Electronic Notes in Theoretical Computer Science 106:219–241, 2004.

10. Kupke, C., Kurz, A., Venema, Y.: Stone coalgebras. Theoretical Computer Science 327(1-2):109–134, 2004.

11. Kupke, C., Kurz, A., Pattinson, D.: Ultrafilter extensions for coalgebras. Lecture Notes in Computer Science 3629:263–277, 2005.

12. Pavlovic, D., Mislove, M., Worrell, J.: Testing Semantics: Connecting Processes and Process Logic. Lecture Notes in Computer Science 4019:308–322, 2006.

13. Rutten, J.J.M.M.: Universal coalgebra: a theory of systems. Theoretical Computer Science 249(1):3–80, 2000.

14. Schröder, L., Pattinson, D.: Strong completeness of coalgebraic modal logics. Leibniz International Proceedings in Informatics 3:673–684, 2009.