Logic for Computer Scientists/Modal Logic/Kripke Semantics

Definition 1

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

A Kripke model is a triple $⟨W,R,V⟩$, with $W$ and $R$ as above and $V$ is a mapping $𝒫\mapsto 2^W$, where $𝒫$ 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 $⟨W,R,V⟩$ and a world $w\in W$, we define the satisfaction relation $\models$ by:

$\begin{array}{ccc}w\models p& \text{iff }& w\in V(p)\\ w\models \mathrm{\neg }A& \text{iff }& w\models ̸A\\ w\models A\wedge B& \text{iff }& w\models A\text{ and }w\models B\\ w\models A\vee B& \text{iff }& w\models A\text{ or }w\models B\\ w\models A\to B& \text{iff }& w\models ̸A\text{ or }w\models B\\ w\models ◻A& \text{iff }& \text{for all }v\in W,(w,v)\in ̸R\text{ or }v\models A\\ w\models \diamond A& \text{iff }& \text{there exists some }v\in W,\text{ with }(w,v)\in R\text{ and }v\models A\end{array}$

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

Lemma 1

The operators $\diamond$ and $◻$ are dual, i.e. for all formulae $A$ and all frames $⟨W,R⟩$, the equivalence $\diamond A\leftrightarrow \mathrm{\neg }◻\mathrm{\neg }A$ holds.