(draft … references to be added) … (up)
We assume here that the reader has seen some propositional and modal logic and is interested in how Kripke structures can be generalised to coalgebras. Coalgebraic logic can be seen as generalising modal logic along the following parameters:
To go through this in detail will take some time. Let us start by sketching how coalgebras generalise Kripke structures.
The notion of coalgebra is parameterised by that of a functor on some category of "spaces" . An object generalises the set of worlds of a Kripke frame, represents the type of transitions and the relation of a Kripke frame is a coalgebra when is the set of subsets of .
Similarly, modal logics can be parameterised by functors accounting for both modal operators such as and and axioms such as preserving meets and preserving joins.
Duality theory can be used to develop the theory of coalgebras together with their modal logics. In fact, often the functors and will be dual to each other in a precise mathematical sense, giving rise to automatic soundness, completeness and expressiveness results.
In the following we summarise the basic ingredients necessary to carry out this approach.
The paradigmatic example of the powerset functor is reviewed in some detail in this note on powerdomains.
We extend a basic dual adjunction between a category of "spaces" and a category of "algebras", to a dual adjunction between coalgebras for a functor on and algebras for a functor on .
In more detail, we have
We think of as mapping a space to its algebra of propositions or predicates. In many examples, is actually the powerset functor.
We think of as mapping an algebra to its spectrum, or the dual space of the algebra.
In addition, we have
We think of as the type functor of generalised transition systems and of as the functor building a language or logic over some atomic propositions.
We write for the category of coalgebras for the functor and for the category of algebras for the functor .
Proposition: If are a dual equivalence and , then is dually equivalent to .
Example: The duality of descriptive general frames and Boolean algebras with operators arises in this way.
If is only a dual adjunction, it lifts to coalgebras/algebras only under special circumstances.
The above framework is very abstract. When is it legitimate to think of coalgebras as transition systems and of algebras as logics?
The paradigmatic example is the one where
(Here we have only on finite sets.)
If we take instead
So even in the case of classical modal we have already three examples that show how varying the different parameters captures interesting modal logics. Moreover, these parameters can be modified independently of each other, creating quite a large space of possibilities.
But the main interest in coalgebras stems from the discovery made by Jan Rutten and others, that there is a great variety of functors .
The coalgebraic approach to modal logic is to expand the landscape of modal logics by systematically extending modal logic to a large variety of functors .
List some examples …
The category theoretic approach to coalgebras takes an axiomatic point of view. Clearly, we cannot expect all results of modal logic to survive modifcations of the parameters
On the other hand, the coalgebraic approach has shown that there is indeed a wide variety of instantiations of these parameters that allows us to extend many results of modal logic.
From a category theoretic point of view we can ask the following questions:
Jonsson-Tarski
Goldblatt
Abramsky
Bonsangue-Kurz
Kupke-Kurz-Venema
Kurz-Rosicky
Klin
…
to be completed
…
…