Spahn
modal logic

Definitions

Classical definition

A modal formula is derived from the language of a logic LL inductively by: if AA is a formula of LL, then boxA\box A is a modal formula. We denote the collection of modal formulas by MM.

A Kripke frame aka. modal frame is a pair (S,R)(S,R) of a set SS and a binary relation RS×SR\subset S\times S. a relation RS×SR\subseteq S\times S is equivalently a function R[]:SP(S)R[\cdot]:S\to P(S) sending ss to the set R[s]R[s] of its successors.

A Kripke model is a triple (S,R, R)(S,R,\Vdash_R) where (S,R)(S,R) is a Kripke frame and a relation S×M\Vdash\subset S\times M (sometimes called forcing relation) subject to the following list of axioms:

(1) R(s,¬A)\Vdash_R(s, \neg A) iff (s,A)(s,A) is not in R\Vdash_R.

(2) R(s,AB)\Vdash_R(s,A\to B) iff (s,A)(s,A) is not in R\Vdash_R or A,B RA,B\in \Vdash_R

(3) R(s,A)\Vdash_R(s,\Box A) iff (t,A) R(t,A)\in \Vdash_R for all tt with (s,t)R(s,t)\in R

(Note that we used here the notation R(s,A)\Vdash_R(s, A) to express the “propositional interpretation” of being a member of the relation.)

A formula DD is called to be valid in a model resp. valid in a frame resp. valid in a class FF of frames if (s,A) R(s,A)\in \Vdash_R for all sSs\in S resp. (s,A) R(s,A)\in \Vdash_R for all sSs\in S all relations RS×SR\subseteq S\times S resp. (s,A) R(s,A)\in \Vdash_R for all (S,R)F(S,R)\in F for allsSs\in S all relations RS×SR\subseteq S\times S.

Definition in terms of coalgebras for Kripke polynomial functors

A binary relation RS×SR\subseteq S\times S is equivalently a function R[]:SP(S)R[\cdot]:S\to P(S) where PP denotes the (covariant) power set functor sending an sSs\in S to the set of its RR-successors R[s]R[s] and a morphism f(X{f(x)|xX})f\mapsto(X\mapsto \{f(x)|x\in X\}). In other words: a frame is a coalgebra for the power set functor.

Generalizing this construction for relations of higher arity one obtains coalgebras for the functor S dtP(S arity(d)S\mapsto \product_{d\in t} P(S^{arity(d}) for any modal similarity type tt.

Kripke models one obtains as coalgebras of the functor XP(Prop)×P(X)X\mapsto P(Prop)\times P(X) where PropProp is the set of propositional variables. To see this note that a valuation V:PropP(S)V:Prop\to P(S) is equivalently a P(Prop)P(Prop)-coloring of SS: a functor K:smapso{pProp|sV(p)}K: s\mapso \{p\in Prop|s\in V(p)\}.

The functors PP and KK from above are examples of Polynomial functors.

(…

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

Reference

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

Last revised on February 25, 2013 at 21:40:22. See the history of this page for a list of all contributions to it.