Spahn modal logic (Rev #2, changes)

Showing changes from revision #1 to #2: Added | ~~Removed~~ | ~~Chan~~ged

Definitions

Classical definition

A modal formula is derived from the language of a logic $L$ inductively by: if $A$ is a formula of $L$ , then $\box A$ is a modal formula. We denote the collection of modal formulas by $M$ .

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

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

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

(2) $\Vdash_R(s,A\to B)$ iff $(s,A)$ is not in $\Vdash_R$ or $A,B\in \Vdash_R$

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

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

A formula $D$ is called to be valid in a model resp. valid in a frame resp. valid in a class $F$ of frames if $(s,A)\in \Vdash_R$ for all $s\in S$ resp. $(s,A)\in \Vdash_R$ for all $s\in S$ all relations $R\subseteq S\times S$ resp. $(s,A)\in \Vdash_R$ for all $(S,R)\in F$ for all $s\in S$ all relations $R\subseteq S\times S$ .

Definition in terms of coalgebras for Kripke polynomial functors

~~(Definition~~ ~~146,~~ ~~p.392)~~ A binary relation~~polynomial functor~~ $R\subseteq S\times S$ is equivalently a function $Set R [\cdot] : S \to P (S)$ ~~Set~~ R[\cdot]:S\to P(S) ~~-valued~~ ~~functor~~ where ~~inductively~~ ~~defined~~ by $P$ denotes the (covariant) power set functor sending an $s\in S$ to the set of its $R$ -successors $R[s]$ and a morphism $f\mapsto(X\mapsto \{f(x)|x\in X\})$ . In other words: a frame is a coalgebra for the power set functor.

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

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

~~where~~ Kripke models ~~$I$~~ one obtains as coalgebras of the functor ~~denotes the identity functor,~~ $X\mapsto P(Prop)\times P(X)$ ~~$C$~~ where ~~denotes the constant functor on an object~~ $Prop$ ~~$C$~~ is the set of propositional variables. To see this note that a , valuation ~~$K_0 +K_1$~~ ~~denotes the coproduct functor of two polynomial functors, and likewise for the product functor,~~ $V:Prop\to P(S)$ ~~$K^D$~~ is equivalently a ~~denotes the exponent functor~~ $P(Prop)$ -coloring of $S$ ~~$X\mapsto K(X)^D$~~ : a functor $K: s\mapso \{p\in Prop|s\in V(p)\}$ .

The functors $P$ and $K$ from above are examples of Polynomial functors.

(…

(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 $K$ with the power set functor $P$ .

(…)

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

Reference

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

Revision on February 25, 2013 at 09:47:34 by Stephan Alexander Spahn?. See the history of this page for a list of all contributions to it.