### Coalgebraic Modal Logic

#### Posted by David Corfield

Recently I’ve been looking into the coalgebra community’s take on modal logic, which in a phrase states simply that

The key idea is to start from a dual adjunction between the semantics and syntax of propositional theories, as explained on page 3 of Exemplaric Expressivity of Modal Logics. Typically this is a Stone-style duality between (Lindenbaum algebras of) propositions and spaces of models or valuations for a propositional theory.

Modalities are then introduced on the syntactic side in the shape of an endofunctor, where the new modal propositional theories are algebras for this functor. Meanwhile, on the semantic side, we have a endofunctor whose coalgebras provide the semantics for the modal propositional theories. If all goes well, we end up lifting the Stone adjunction to one between coalgebras on one side and algebras on the other. It would be handy at this point if I’d learned how to draw suitable diagrams. As I haven’t you can see what’s going on on page 2 of Coalgebras and Their Logics.

To relate all this to something perhaps familiar, when you introduce the necessity operator $\square$ into a propositional theory, semantically you start thinking about the accessibility of one world from another. So, $\square P$ (it is necessarily the case that $P$) holds in my world if $P$ holds in all worlds accessible from my world. This accessibility relation is thus a relation $R$ between worlds, or in other words a coalgebra for the powerset functor:

$R: X \to P(X).$

Properties of the modalities, such as $\square P \vdash \square \square P$, correspond to properties of the relation, here transitivity.

But there are many other modalities we might want to consider, as explained here:

One large class of logics is the vast and growing family of modal logics, which are characterised by having operators that qualify formulas as holding in a certain way, e.g. ‘necessarily’, ‘in the future’, ‘everywhere’, ‘probably’, ‘as everyone knows’, or ‘normally’. (p. 1)

All of these are needed to analyse typical statements:

In a seemingly simple piece of knowledge such as ‘Normally, the likelihood of road congestion is smaller on weekends’, one implicitly makes use of default logics (‘normally’), probabilistic reasoning (‘the likelihood’) and temporal knowledge (‘weekends’) under a quantitative regime (‘smaller’).

In the case of probabilistic modalities, we might want modal operators such as

it is at least $p \%$ probable that at the next step $\phi$.

On the semantic side of this operator, we will need to revist our old friend the Giry monad which sends a set to the set of subprobability distributions it supports. Coalgebras for this functor are Markov chains. The resulting logic is Probabilistic modal logic.

We can even consider the $\pi$-calculus as a modal logic:

we use the presheaf category $N$ of functors from finite sets (of channel names) with injective renamings to a certain category of domains (representing observable behaviour in the presence of recursion). (p. 5)

The endofunctor on the semantic side, i.e., on $N$ is

$Pi(X) = \mathcal{P}(X + N \times X^N + N \times (N \times X) + N \times \delta X).$

We read

Pias follows. The possible one-step behaviours of a process are non-deterministic (due to $\mathcal{P}$) and may be one of the following alternatives: A silent step (the $X$ component), an input of a name $(X^N)$ over a channel $(N)$, the output of a free name over a channel (due to $N \times N \times X$) or the allocation and sending of a fresh name (the $N \times \delta(X)$-part). (p. 5)

This results in a “new fully abstract, sound and complete modal logic for the $\pi$-calculus”. For more details see Pi-Calculus in Logical Form.

Perhaps we can now start to glimpse connections between two pieces of work out of Carnegie-Mellon that we have commented on before. On the one hand, there’s the syntax-semantics duality of first-order theories due to Forssell. Here the dualising object is no longer $2$ but rather the category $Set$. Just as $2$ can be taken as equipped with many structures, so with $Set$.

For example, $Set$ is a category with finite products, and an object in the category, $\mathcal{F} \mathcal{P}$, of such categories with finite product preserving functors. But it is also a category with all limits and colimits, and an object in the category, $\mathcal{G}$, of such categories with functors which preserve limits, filtered colimits, and regular epimorphisms. This allows for the following duality, as Forssell explains,

- Models = $Hom_{\mathcal{F} \mathcal{P}} (Algebraic theory, Set)$
- Algebraic theory = $Hom_{\mathcal{G}} (Models, Set)$.

He goes on to show the duality between Boolean coherent categories (corresponding to first-order theories) and topological groupoids (corresponding to their models). We might hope then for modalities acting on the first-order syntax and semantics to be functors (maybe 2-functors) of a certain kind on these Boolean coherent categories.

We can think of the transition systems between models or worlds of *propositional* theories as telling us which members of a set of worlds are close to one another. For any ordered pair can we move from the first to the second – Yes or No? Now with first-order theories we’re working in a category of worlds and we want to know for any objects not just *whether* we can get from one to another, but *how*.

The trivial choice of transition system for a set is where $a R b$ if and only if $a = b$. This corresponds to the coalgebra $\a \mapsto \{a\}$. The equivalent for categories is, I would guess, the Yoneda embedding as a 2-coalgebra. Here an object relates to another via the arrows in the category itself. But presumably there must be other transition systems to work with.

The second piece of Carnegie-Mellon work may give us a clue as to how to proceed. It’s Awodey and Kishida’s sheaf semantics for first order modal logic. Here we model first-order modal logic by a sheaf over a space of worlds. A fibre contains the individuals living in the world indexed by a point in the base space.

So the question is: can these sheaf models for a first-order modal theory be seen as (2)-coalgebras for some endofunctor on the category of models of the nonmodal first-order theory?

The thrust of the coalgebraic approach to modal propositional logic is summarised as:

First,

the coalgebraic modelis flexible. That is, it can incorporate many different types of behaviour and interaction, e.g. location awareness, mobility and quantitative uncertainty, to name but a few. Second,the coalgebraic model is compositional: both on the logical and the semantical level it allows us to combine computational features and reason about their interaction. Third,the coalgebraic model is uniform, i.e. all computational aspects of the model share the same meta-theory. This in particular leads to software tools that are easier to design, to maintain and to implement. Finally,the coalgebraic model is compatiblein the sense that it subsumes nearly all existing formal notions of state based system as special cases. (p. 10)

It would fun to extend this to first-order theories. There must be quite a space of logics out there.

## Re: Coalgebraic Modal Logic

When I was learning about monads, the monad for monoids was a particularly helpful example, as was seeing how $\mathbb{Z}_2$ is an algebra of the monad. So, can you walk us through an example of coalgebras? Like, is there such a thing as a comonoid? If so, can you show how a particular comonoid (is there such a thing as co-$\mathbb{Z}_2$?) arises as a coalgebra of the comonad for comonoids?