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.