coalgebraic model for modal logic


Modal logics are said to be the logic of relational structures. The Kripke frame semantics of modal logics provides a clear picture of this:

Recall: A frame for the basic modal language ω(1)\mathcal{L}_\omega(1) is a pair 𝔉=(W,R)\mathfrak{F} = (W,R) with WW a non-empty set and RR a binary relation on WW.

At their ‘crudest’ the objects studied are just sets and binary relations on them. In the basic ‘many worlds’ interpretation, a world ww satisfies a modal formula ϕ\Box\phi if all worlds ww\prime accessible from ww (that is satisfying wRwwRw\prime) satisfy ϕ\phi.

Now convert RR into a mapping ρ:W𝒫(W)\rho : W\to \mathcal{P}(W), where ρ(w)\rho(w) is the set of worlds accessible from ww. It is easy to rephrase the notion of ‘satisfies’ in terms of ρ\rho, but (W,ρ)(W,\rho) is a coalgebra for the power set endofunctor on SetSet, so Kripke frames provide a simple example of a coalgebraic modal for modal formulae. There are many other types of coalgebras for endofunctors and many lead to modal logics.


Created on November 6, 2012 at 19:28:02. See the history of this page for a list of all contributions to it.