Spahn algebraic- and coalgebraic semantics of modal logic (Rev #9, changes)

Showing changes from revision #8 to #9: Added | Removed | Changed

• Yde Venema, Algebras and Coalgebras, §6 (p.332-426)in Blackburn, van Benthem, Wolter, Handbook of modal logic, Elsevier, 2007.

The bibliography lists many articles of Robert Goldblatt and Bart Jacobs on modal logic.

1 Introduction

(p.332)

(…)

An important difference of the coalgebraic approach compared to the algebraic one is that coalgebras generalize rather than dualize the model theory of modal logic. One may generalize the concept of modal logic from Kripke frames to arbitrary coalgebras. In fact the link between modal logic and coalgebra is so strong that one may claim that modal logic is the natural logic for coalgebras (just like equational logic is that for algebra)

9 Coalgebras: an introduction

(p.389)

The notion of coalgebra was formed in the sixties but the topic attracted a wider attention only when was realized that coalgebras can be seen as a general uniform theory of dynamic systems.

We list some applications (or examples) of the theory of coalgebras.

• The main examples for coalgebras are Kripke frames.

• Aczel in [non-well founded sets] models transition systems and non-well fondet sets as coalgebras.

• Barwise-Moss in [Vicious Circles] discuss notions of circularity and self-reference (and many (other) applications).

• Rutten [Automata and coinduction] on coalgebras and deterministic automata.

(Definition 146, p.392) A polynomial functor is a $Set$-valued functor inductively defined by

$K::=I | C | K_0 + K_1 | K_0\times K_1 | K^D$

where $I$ denotes the identity functor, $C$ denotes the constant functor on an object $C$, $K_0 +K_1$ denotes the coproduct functor of two polynomial functors, and likewise for the product functor, $K^D$ denotes the exponent functor $X\mapsto K(X)^D$.

A Kripke polynomial functor is inductively defined by

$K::=I | C | K_0 + K_1 | K_0\times K_1 | K^D | P K$

where $P K$ denotes the composition of a polynomial functor with the power set functor.

(…)

13 Modal logic and coalgebras

(p.406)

$\nabla \phi:=\Box\bigvee \phi \wedge \bigwedge \diamond\phi$

The initial ideas in this section are attributed to L. Moss:

where $\diamond \phi:=\{\diamond \varphi|\varphi\in \phi\}$ and likewise $\Box\phi$. Then we have

• Coalgebraic logic. Annals of Pure and Applied Logic, 96:277–317, 1999. (Erratum published Ann.P.Appl.Log. 99:241–259, 1999).

• J. Barwise and L. Moss. Vicious Circles, volume 60 of CSLI Lecture Notes. CSLI Publications, 1996.

 \nabla \phi:=\Box\bigvee \phi \wedge \bigwedge \diamond\phi \simeq \nabla\{\phi,\top\}
$\Box \varphi\simeq\nabla\varnothing\vee\nabla\{\varphi\}$

where $\diamond \phi:=\{\diamond \varphi|\varphi\in \phi\}$ and likewise $\Box\phi$. Then we have

Let $\mathbb{S}:=\langle S,\lambda,R[\cdot]\rangle$ be a modal model in coalgebraic shape. Then $\mathbb{S},s\Vvdash$

$\diamond\phi \simeq \nabla\{\phi,\top\}$
$\Box \varphi\simeq\nabla\varnothing\vee\nabla\{\varphi\}$

Let $\mathbb{S}:=\langle S,\lambda,R[\cdot]\rangle$ be a modal model in coalgebraic shape(§9 Example 143). Then $\mathbb{S},s\Vdash\nabla \phi$ iff $(R[s],\phi)$ belongs to the relation lifting (§11) $\overline{\mathcal{P}}(\Vdash_{\mathbb{S}})$ of the satisfaction relation $\Vdash_{\mathbb{S}}\subseteq S\times \phi$: Every $\varphi\in \Phi$ must hold at some successor $t\in R[s]$, and at every successor $t$ of some $\varphi\in \phi$ must hold. The previous lines are the founding insights to coalgebraic logic in which the same principle is applied to an arbitrary set functor $\Omega$ and the basic idea is to have

$\mathbb{S},s\Vdash_{\mathbb{S}}\nabla P\;\text{iff}\; (P,\sigma(s))\in \overline{\Omega}(\Vdash_{\mathbb{S}}).$

References

For polynomial functors see also the references at polynomial functor. In particular

Revision on February 18, 2013 at 08:50:07 by Stephan Alexander Spahn?. See the history of this page for a list of all contributions to it.