Logic for Computer Scientists/Modal Logic/Kripke Semantics

Definition 1Edit

A Kripke frame is a pair ${\displaystyle \langle W,R\rangle }$ , where ${\displaystyle W}$  is a non-empty set (of possible worlds) and ${\displaystyle R}$  a binary relation on ${\displaystyle W}$ . We write ${\displaystyle wRw'}$  iff ${\displaystyle (w,w')\in R}$  and we say that world ${\displaystyle w'}$  is accessible from world ${\displaystyle w}$ , or that ${\displaystyle w'}$  is reachable from ${\displaystyle w}$ , or that ${\displaystyle w'}$  is a successor of ${\displaystyle w}$ .

A Kripke model is a triple ${\displaystyle \langle W,R,V\rangle }$ , with ${\displaystyle W}$  and ${\displaystyle R}$  as above and ${\displaystyle V}$  is a mapping ${\displaystyle {\mathcal {P}}\mapsto 2^{W}}$ , where ${\displaystyle {\mathcal {P}}}$  is the set of propositional variables. ${\displaystyle V(p)}$  is intended to be the set of worlds at which ${\displaystyle p}$  is true under the valuation ${\displaystyle V}$ .

Given a model ${\displaystyle \langle W,R,V\rangle }$  and a world ${\displaystyle w\in W}$ , we define the satisfaction relation ${\displaystyle \models }$  by:

${\displaystyle {\begin{matrix}w\models p&{\mbox{iff }}&w\in V(p)\\w\models \lnot A&{\mbox{iff }}&w\not \models A\\w\models A\land B&{\mbox{iff }}&w\models A{\mbox{ and }}w\models B\\w\models A\lor B&{\mbox{iff }}&w\models A{\mbox{ or }}w\models B\\w\models A\to B&{\mbox{iff }}&w\not \models A{\mbox{ or }}w\models B\\w\models \Box A&{\mbox{iff }}&{\mbox{for all }}v\in W,(w,v)\not \in R{\mbox{ or }}v\models A\\w\models \diamond A&{\mbox{iff }}&{\mbox{there exists some }}v\in W,{\mbox{ with }}(w,v)\in R{\mbox{ and }}v\models A\\\end{matrix}}}$

We say that ${\displaystyle w}$  satisfies ${\displaystyle A}$  iff ${\displaystyle w\models A}$  (without mentioning the valuation ${\displaystyle V}$ ). A formula ${\displaystyle A}$  is called satisfiable in a model ${\displaystyle \langle W,R,V\rangle }$ , iff there exists some ${\displaystyle w\in W}$ , such that ${\displaystyle w\models A}$ . A formula ${\displaystyle A}$  is called satisfiable in a frame ${\displaystyle \langle W,R\rangle }$ , iff there exists some valuation ${\displaystyle V}$  and some world ${\displaystyle w\in W}$ , such that ${\displaystyle w\models A}$ . A formula ${\displaystyle A}$  is called valid in a model ${\displaystyle \langle W,R,V\rangle }$ , written as ${\displaystyle \langle W,R,V\rangle \models A}$  iff it is true at every world in ${\displaystyle W}$ . A formula ${\displaystyle A}$  is valid in a frame ${\displaystyle \langle W,R\rangle }$ , written as ${\displaystyle \langle W,R\rangle \models A}$  iff it is valid in all models ${\displaystyle \langle W,R,V\rangle }$ .

Lemma 1Edit

The operators ${\displaystyle \diamond }$  and ${\displaystyle \square }$  are dual, i.e. for all formulae ${\displaystyle A}$  and all frames ${\displaystyle \langle W,R\rangle }$ , the equivalence ${\displaystyle \diamond A\leftrightarrow \lnot \square \lnot A}$  holds.