(draft … references to be added) … (up)
We continue from the introduction.
Let
Then there is a functor
where BAOs is the category of Boolean algebras with operators, the standard algebraic semantics of classical modal logic.
In particular,
Moreover,
(should this section go into the intro?)
Here are some simplifications that the category theoretic approach offers:
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 and yields, once established, a range of results such as
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 on a category of "spaces" . 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!)
Starting from a functor , what is the modal logic of -coalgebras?
According to the discussion above, the task is to find a functor such that, restricted to finite sets and finite Boolean algebras, is the dual of . More precisely, we have to find and such that
is an isomorphism. [3]
We do this in two steps. The first step is to describe
for being freely generated by enough modal operators so that is injective. This means that the logical one-step language is expressive enough to describe all elements of 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 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 by generators (modal operators) and relations (modal axioms) one, of course, needs to understand the particular functor and this can require a lot of work. But there are general theorems that for all functors there exists a functor . And, conversely, all functors preserving so-called sifted colimits describe a modal logic given by operations and equations.
Let be the powerset functor. -coalgebras are precisely Kripke frames.
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 is represented by the language without the axioms. It is defined as
where denotes the free Boolean algebra over . Categorically is the left adjoint of the forgetful functor .
The semantics of the language is given by
This definition expresses that a set of successors satisfies if the is contained in .
To regain the usual semantics with respect to Kripke frames (ie -coalgebras) consider a coalgebra . Note the following, where denotes the inverse image of :
The collection of all modal formulas is the initial -algebra .
is what is known as the "complex algebra" of in modal logic.
The universal property of the initial algebra induces a unique
interpreting formulas as subsets of .
Spelling this out in detail, gives us back the usual definition of the semantics of modal logic:
The first three lines come from being a Boolean algebra morphism and the fourth one from being an -algebra morphism.
We now turn to the task of finding the axioms via normal forms. This involves finding a map
such that . Since is a Boolean algebra, it is enough to define on generators and since we can assume to be finite, it is enough to give on singletons with . Since , is a subset of .
Thus, the task is to find a formula in that expresses . This formula is well-known in modal logic
(what are the historical references?)
More precisely, the initial -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 -algebra over the Boolean algebra freely generated by the set of atomic propositions. ↩︎
More precisely, has formulas in which every generator is under the scope of exactly one modal operation. For example is of rank 1 but neither are nor . Intuitively, expresses a relationship between states in and and between states in and , whereas formulas in express only relationships between states in . ↩︎
and are functors . Hence should be an arrow in the category of functors , that is, we require to be a natural transformation such that all components are isomorphisms. ↩︎