Basic Coalgebraic Logic

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

(13)#\[\begin{align} \Box\top &= \top \\ \Box(a\wedge b) & = \Box a\wedge \Box b \end{align}\]

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 $$\delta:LP\to PT$$

is an isomorphism. [3]

We do this in two steps. The first step is to describe $$\delta':L'P\to PT$$

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 $$ L'P\to LP$$

in such a way that $$PT\to L'P\to LP$$

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 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 $$ nf: PTX\to L'PX$$

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?)

\[\sem{...}\]