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

Showing changes from revision #13 to #14: Added | Removed | Changed

This entry is about

  • 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 founded 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 SetSet-valued functor inductively defined by

K::=I|C|K 0+K 1|K 0×K 1|K DK::=I | C | K_0 + K_1 | K_0\times K_1 | K^D

where II denotes the identity functor, CC denotes the constant functor on an object CC, K 0+K 1K_0 +K_1 denotes the coproduct functor of two polynomial functors, and likewise for the product functor, K DK^D denotes the exponent functor XK(X) DX\mapsto K(X)^D.

A Kripke polynomial functor is inductively defined by

K::=I|C|K 0+K 1|K 0×K 1|K D|PKK::=I | C | K_0 + K_1 | K_0\times K_1 | K^D | P K

where PKP K denotes the composition of a polynomial functor KK with the power set functor PP.

(…)

(p.392) Kripke frames are PIPI-coalgebras, and Kripke models are coalgebras for the functor PProp×PIPProp\times PI.

Explanation: see modal logic

13 Modal logic and coalgebras

(p.406)

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

  • 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.

Introduction

Let ϕ\phi be a set of formulas.

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

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

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

Let 𝕊:=S,λ,R[]\mathbb{S}:=\langle S,\lambda,R[\cdot]\rangle be a modal model in coalgebraic shape(§9 Example 143). Then 𝕊,sϕ\mathbb{S},s\Vdash\nabla \phi iff (R[s],ϕ)(R[s],\phi) belongs to the relation lifting (§11) 𝒫¯( 𝕊)\overline{\mathcal{P}}(\Vdash_{\mathbb{S}}) of the satisfaction relation 𝕊S×ϕ\Vdash_{\mathbb{S}}\subseteq S\times \phi: Every φΦ\varphi\in \Phi must hold at some successor tR[s]t\in R[s], and at every successor tt 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

𝕊,s 𝕊Piff(P,σ(s))Ω¯( 𝕊).\mathbb{S},s\Vdash_{\mathbb{S}}\nabla P\;\text{iff}\; (P,\sigma(s))\in \overline{\Omega}(\Vdash_{\mathbb{S}}).

In this situation, the satisfaction relation is much like a bisimulation between a language and a coalgebra; for this see

  • A. Baltag. A logic for coalgebraic simulation. In

    • H. Reichel, editor. Coalgebraic Methods in Computer Science (CMCS’00), volume 33 of Electronic Notes in Theoretical Computer Science. Elsevier, 2000.

Definition

For the existence of the language of coalgebraic formulas for Ω\Omega it is necessary to allow class based algebras. This may be accomplished by letting Ω +\Omega^+ be the unique extension of Ω\Omega to a set based functor on the category SETSET having classes as objects and set-continuous (standard) set functors as morphisms. In examples these functors are often polynomial functors; e.g. Kripke functors are of this kind.

Definition

The initial algebra of the functor (P+Ω) +(P+\Omega)^+ is called the language of coalgebraic formulas for Ω\Omega and is denoted by

Ω,,.\langle\mathcal{L}_\Omega, \bigwedge,\nabla\rangle.

Unwinding this definition yields the following equivalent characterization.

Definition

Let Ω:SetSet\Omega:Set\to Set be (for convenience) be a set functor sending inlusions to inclusions (call this a standard set functor). Then the language of coalgebraic formulas denoted by Ω\mathcal{L}_\Omega is defined to be the least class CC such that

(1) ϕ Ω\phi\in \mathcal{L}_\Omega implies ϕ Ω\bigwedge\phi\in \mathcal{L}_\Omega.

(2) PΩ +( Ω)P\in \Omega^+(\mathcal{L}_\Omega) implies P Ω\nabla P\in \mathcal{L}_\Omega.Let Ω +\Omega^+ is the unique extension of Ω\Omega to a set based functor on the category SETSET having classes as objects and set-continuous (standard) set functors as morphisms.

Definition (p.411)

Let Ω:SetSet\Omega:\Set\to Set be a functor, let ν:ΩProp\nu:\Omega\to Prop be some natural transformation, let \bigwedge be some collection of natural transformations Ω𝒫\Omega\to \mathcal{P}. then ν,\mathcal{L}_{\nu,\bigwedge} is the standard modal language obtained by taking PropProp as the collection off propositional variables, and τ :={ λ|λ}\tau_\bigwedge:=\{\diamond_\lambda|\lambda\in \bigwedge\} as the modal similarity type.

Predicate liftings (from 𝒫S𝒫ΩS\mathcal{P} S\to \mathcal{P}\Omega S can be used to obtain modal operators.

Definition (p.412)

A predicate lifting for a set functor Ω\Omega is a natural transformation μ:𝒫ˇ𝒫ˇΩ\mu:\check{\mathcal{P}}\to \check{\mathcal{P}} \Omega where Pˇ\check{P} denotes the contravariant power set functor. Which each predicate lifting we can associate a modal operator μ\diamond_\mu with the following semantics:

𝕊,s λφiffσ(s)μ S([[φ]]).\mathbb{S},s\Vdash \diamond_\lambda \varphi\;\text{iff}\;\sigma(s)\in \mu_S([[\varphi]]).

References

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

Revision on May 19, 2013 at 18:31:29 by Stephan Alexander Spahn?. See the history of this page for a list of all contributions to it.