Logic for Computer Scientists/Modal Logic/Kripke Semantics

Definition 1Edit

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 1Edit

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.

Last modified on 13 July 2009, at 14:09