Try   HackMD

Coalgebraic Logic: Basic Modal Logic

(draft references to be added) (up)

Idea

We continue from the introduction.

Let

  • X
    the category of sets
  • A
    the category of Boolean algebras
  • T
    the powerset functor,
    Coalg(T)
    the category of Kripke frames

Then there is a functor

  • L:BABA
    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
    a
    ,
    aA
    module the equations
    =(ab)=ab

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ω
    of finite Boolean algebras. (Note that
    BAω
    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ω
    and
    BAω
    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"
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:SetSet, what is the modal logic of
T
-coalgebras?

According to the discussion above, the task is to find a functor

L:BABA such that, restricted to finite sets and finite Boolean algebras,
L
is the dual of
T
. More precisely, we have to find
L
and
δ
such that
δ:LPPT

is an isomorphism. [3]

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

δ:LPPT

for

LP being freely generated by enough modal operators so that
δ
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

LPLP

in such a way that

PTLPLP

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=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

. We also know the standard Kripke semantics of the
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

L:BABAAF{aaA}

where

FX denotes the free Boolean algebra over
X
. Categorically
F
is the left adjoint of the forgetful functor
U:BASet
.

The semantics of the language is given by

δX:LPXPTXa{SPTXSa}

This definition expresses that a set of successors

S satisfies
a
if the
S
is contained in
a
.

To regain the usual semantics with respect to Kripke frames (ie

T-coalgebras) consider a coalgebra
ξ:XTX
. Note the following, where
Pξ
denotes the inverse image of
ξ
:

  • The collection

    Φ of all modal formulas is the initial
    L
    -algebra
    LΦΦ
    .

  • LPXδXPTXPξPX is what is known as the "complex algebra" of
    (X,ξ)
    in modal logic.

  • The universal property of the initial algebra induces a unique

    [[]]:ΦPX

    interpreting formulas as subsets of

    X.

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

[[]]=X[[ϕψ]]=[[ϕ]][[ψ]][[¬ϕ]]=X[[ϕ]][[ϕ]]={xXξ(x)[[ϕ]]}

The first three lines come from

[[]] 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

nf:PTXLPX

such that

δ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
tTX
. Since
T=P
,
t
is a subset of
X
.

Thus, the task is to find a formula in

LPX that expresses
tTX
. This formula is well-known in modal logic

(what are the historical references?)

[[...]]


  1. More precisely, the initial

    L-algebra will be the Lindenbaum-Tarski algebra of classical modal logic with no atomic propositions. To account for a set of atomic proposisions, one takes the free
    L
    -algebra over the Boolean algebra freely generated by the set of atomic propositions. ↩︎

  2. More precisely,

    LPX has formulas in which every generator
    aPX
    is under the scope of exactly one modal operation. For example
    (ab)
    is of rank 1 but neither are
    aa
    nor
    aa
    . Intuitively,
    aa
    expresses a relationship between states in
    X
    and
    TX
    and
    aa
    between states in
    TTX
    and
    TX
    , whereas formulas in
    LPX
    express only relationships between states in
    TX
    . ↩︎

  3. PT and
    LP
    are functors
    SetBA
    . Hence
    δ
    should be an arrow in the category of functors
    SetBA
    , that is, we require
    δ
    to be a natural transformation such that all components
    δX:PTXLPX
    are isomorphisms. ↩︎