Logic for Computer Scientists/Modal Logic/Kripke Semantics

Definition 1

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

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

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

${\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 $w$ satisfies $A$ iff $w\models A$ (without mentioning the valuation $V$ ). A formula $A$ is called satisfiable in a model $\langle W,R,V\rangle$ , iff there exists some $w\in W$ , such that $w\models A$ . A formula $A$ is called satisfiable in a frame $\langle W,R\rangle$ , iff there exists some valuation $V$ and some world $w\in W$ , such that $w\models A$ . A formula $A$ is called valid in a model $\langle W,R,V\rangle$ , written as $\langle W,R,V\rangle \models A$ iff it is true at every world in $W$ . A formula $A$ is valid in a frame $\langle W,R\rangle$ , written as $\langle W,R\rangle \models A$ iff it is valid in all models $\langle W,R,V\rangle$ .

Lemma 1

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