Basic Coalgebraic Logic

(draft ... references to be added)

Idea¶

We continue from the introduction.

Let

• $\mathcal X$ the category of sets

• $\mathcal A$ the category of Boolean algebras

• $T$ the powerset functor, $Coalg(T)$ the category of Kripke frames

Then there is a functor

• $L:BA\to BA$ such that $Alg(L)$ is the category of BAOs

where BAOs is the category of Boolean algebras with operators, the standard algebraic semantics of classical modal logic.

In particular,

• the initial $L$-algebra is (the Lindenbaum-Tarski algebra of) basic modal logic. ^[1]

Moreover,

• LA is the free Boolean algebra over $\Box a$, $a\in A$ module the equations

The category theoretic approach¶

(should this section go into the intro?)

Here are some simplifications that the category theoretic approach offers:

• Restricting to the one-step case: $TX$ describes the possible successors, here sets of states. $LPX$ describes one-step modal formulas over sets of successors. ^[2] By directly relating $TX$ and $LPX$ we can prove many results of modal logic in a one-step form without ever having to nest modal operators.

• Restricting to the finite case: Since Boolean algebras are defined by operations with finite arity, it is enough to describe $L$ on the category $BA_\omega$ of finite Boolean algebras. (Note that $BA_\omega$ can also be described as the category of finitely presentable BAs and the category of finitely generated BAs.) This has the benefit that we can make explicit use of the fact that $Set_\omega$ and $BA_\omega$ are dually equivalent.

In both situations, the move from the special case to the general case can then be performed by appealing to generic categorical techniques.

The category theoretic approach has also the advantage that the duality of $T$ and $L$ yields, once established, a range of results such as

• invariance under bisimilarity

• completeness

• expressiveness (Hennessy-Milner, bisimulation somewhere else, ...)

• normal forms

• proof systems

• decidability

• complexity

We need to emphasise that the best results of the coalgebraic approach to modal logic generalise the results from basic modal logic from Kripke frames to other functors $T$ on a category of “spaces” $\mathcal X$. Thus, when we talk about completeness, decidability, complexity, etc this refers to the logics of the functors, not to more general logics that are obtained by adding additional axioms to these logics.

(We need to elaborate on the last point above somewhere!)

Finding the logic of a functor¶

Starting from a functor $T:Set\to Set$, what is the modal logic of $T$-coalgebras?

According to the discussion above, the task is to find a functor $L:BA\to BA$ such that, restricted to finite sets and finite Boolean algebras, $L$ is the dual of $T$. More precisely, we have to find $L$ and $\delta$ such that

is an isomorphism. ^[3]

We do this in two steps. The first step is to describe

for $L'P$ being freely generated by enough modal operators so that $\delta'$ is injective. This means that the logical one-step language $L'$ is expressive enough to describe all elements of $PTX$ uniquely.

The second step is then to quotient

in such a way that

becomes an isomorphism. This quotient then describes the axioms of the modal logic. Completeness, as well as other nice properties of the modal logic $L$ then follow for free from the category theoretic approach hinted at in the previous subsection.

How general is this methodology?

In order to find a nice presentation of $L$ by generators (modal operators) and relations (modal axioms) one, of course, needs to understand the particular functor $T$ and this can require a lot of work. But there are general theorems that for all functors $T$ there exists a functor $L$. And, conversely, all functors preserving so-called sifted colimits describe a modal logic given by operations and equations.

Finding the logic of the powerset functor¶

Let $T=\mathcal P$ be the powerset functor. $T$-coalgebras are precisely Kripke frames.

Step 1: The Language and Modal Operations¶

For now we side-step the question of how to find the language. We start from the language we know and love, namely the one given by one modal operation $\Box$. We also know the standard Kripke semantics of the $\Box$ via sets of successors. The aim is to show a methodology of how to find the axioms.

The functor $L'$ is represented by the language without the axioms. It is defined as

where $FX$ denotes the free Boolean algebra over $X$. Categorically $F$ is the left adjoint of the forgetful functor $U:BA\to Set$.

The semantics of the language is given by

This definition expresses that a set of successors $S$ satisfies $\Box a$ if the $S$ is contained in $a$.

To regain the usual semantics with respect to Kripke frames (ie $T$-coalgebras) consider a coalgebra $\xi:X\to TX$. Note the following, where $P\xi$ denotes the inverse image of $\xi$:

• The collection $\Phi$ of all modal formulas is the initial $L$-algebra $L\Phi\to\Phi$.

• $LPX\stackrel{\delta'_X}{\longrightarrow} PTX\stackrel{P\xi}{\longrightarrow} PX$ is what is known as the “complex algebra” of $(X,\xi)$ in modal logic.

• The universal property of the initial algebra induces a unique

interpreting formulas as subsets of $X$.

Spelling this out in detail, gives us back the usual definition of the semantics of modal logic:

The first three lines come from $\sem{-}$ being a Boolean algebra morphism and the fourth one from being an $L$-algebra morphism.

Step 2: Finding the Normal Form of Operations¶

We now turn to the task of finding the axioms via normal forms. This involves finding a map

such that $\delta'\circ nf = id$. Since $PTX$ is a Boolean algebra, it is enough to define $nf$ on generators and since we can assume $X$ to be finite, it is enough to give $nf$ on singletons $\{t\}$ with $t\in TX$. Since $T=\mathcal P$, $t$ is a subset of $X$.

Thus, the task is to find a formula in $L'PX$ that expresses $t\in TX$. This formula is well-known in modal logic

(what are the historical references?)