Kripke semantics for modal propositional logic
A Kripe model for a modal propositional logic^{} PL${}_{M}$ is a triple $M:=(W,R,V)$, where

1.
$W$ is a set, whose elements are called possible worlds,

2.
$R$ is a binary relation^{} on $W$,

3.
$V$ is a function that takes each wff (wellformed formula) $A$ in PL${}_{M}$ to a subset $V(A)$ of $W$, such that

–
$V(\u27c2)=\mathrm{\varnothing}$,

–
$V(A\to B)=V{(A)}^{c}\cup V(B)$,

–
$V(\mathrm{\square}A)=V{(A)}^{\mathrm{\square}}$, where ${S}^{\mathrm{\square}}:=\{s\mid \uparrow s\subseteq S\}$, and $\uparrow s:=\{t\mid sRt\}$.

–
For derived connectives^{}, we also have $V(A\wedge B)=V(A)\cap V(B)$, $V(A\vee B)=V(A)\cup V(B)$, $V(\mathrm{\neg}A)=V{(A)}^{c}$, the complement^{} of $V(A)$, and $V(\diamond A)=V{(A)}^{\diamond}:=V{(A)}^{c\mathrm{\square}c}$.
One can also define a satisfaction relation $\vDash $ between $W$ and the set $L$ of wff’s so that
$${\vDash}_{w}A\mathit{\hspace{1em}\hspace{1em}}\text{iff}\mathit{\hspace{1em}\hspace{1em}}w\in V(A)$$ 
for any $w\in W$ and $A\in L$. It’s easy to see that

•
${\vDash \u0338}_{w}\u27c2$ for any $w\in W$,

•
${\vDash}_{w}A\to B$ iff ${\vDash}_{w}A$ implies ${\vDash}_{w}B$,

•
${\vDash}_{w}A\wedge B$ iff ${\vDash}_{w}A$ and ${\vDash}_{w}B$,

•
${\vDash}_{w}A\vee B$ iff ${\vDash}_{w}A$ or ${\vDash}_{w}B$,

•
${\vDash}_{w}\mathrm{\neg}A$ iff ${\vDash \u0338}_{w}A$,

•
${\vDash}_{w}\mathrm{\square}A$ iff for all $u$ such that $wRu$, we have ${\vDash}_{u}A$,

•
${\vDash}_{w}\diamond A$ iff there is a $u$ such that $wRu$ and ${\vDash}_{u}A$.
When ${\vDash}_{w}A$, we say that $A$ is true at world $w$.
The pair $\mathcal{F}:=(W,R)$ in a Kripke model $M:=(W,R,V)$ is also called a (Kripke) frame, and $M$ is said to be a model based on the frame $\mathcal{F}$. The validity of a wff $A$ at different levels (in a model, a frame, a collection^{} of frames) is defined in the parent entry (http://planetmath.org/KripkeSemantics).
For example, any tautology^{} is valid in any model.
Now, to prove that any tautology is valid, by the completeness of PL${}_{c}$, every tautology is a theorem, which is in turn the result of a deduction^{} from axioms using modus ponens^{}.
First, modus ponens preserves validity: for suppose ${\vDash}_{w}A$ and ${\vDash}_{w}A\to B$. Since ${\vDash}_{w}A$ implies ${\vDash}_{w}B$, and ${\vDash}_{w}A$ by assumption, we have ${\vDash}_{w}B$. Now, $w$ is arbitrary, the result follows.
Next, we show that each axiom of PL${}_{c}$ is valid:

•
$A\to (B\to A)$: If ${\vDash}_{w}A$ and ${\vDash}_{w}B$, then ${\vDash}_{w}A$, so ${\vDash}_{w}B\to A$.

•
$(A\to (B\to C))\to ((A\to B)\to (A\to C))$: Suppose ${\vDash}_{w}A\to (B\to C)$, ${\vDash}_{w}A\to B$, and ${\vDash}_{w}A$. Then ${\vDash}_{w}B\to C$ and ${\vDash}_{w}B$, and therefore ${\vDash}_{w}C$.

•
$(\mathrm{\neg}A\to \mathrm{\neg}B)\to (B\to A)$: we use a different approach to show this:
$V((\mathrm{\neg}A\to \mathrm{\neg}B)\to (B\to A))$ $=$ $V{(\mathrm{\neg}A\to \mathrm{\neg}B)}^{c}\cup V(B\to A)$ $=$ $(V(\mathrm{\neg}A)\cap V{(\mathrm{\neg}B)}^{c})\cup V{(B)}^{c}\cup V(A)$ $=$ $(V{(A)}^{c}\cap V(B))\cup V{(B)}^{c}\cup V(A)$ $=$ $(V{(A)}^{c}\cup V{(B)}^{c})\cup V(A)=W.$
In addition, the rule of necessitation^{} preserves validity as well: suppose ${\vDash}_{w}A$ for all $w$, then certainly ${\vDash}_{u}A$ for all $u$ such that $wRu$, and therefore ${\vDash}_{w}\mathrm{\square}A$.
There are also valid formulas^{} that are not tautologies. Here’s one:
$$\mathrm{\square}(A\to B)\to (\mathrm{\square}A\to \mathrm{\square}B)$$ 
Proof.
Let $w$ be any world in $M$. Suppose ${\vDash}_{w}\mathrm{\square}(A\to B)$. Then for all $u$ such that $wRu$, ${\vDash}_{u}A\to B$, or ${\vDash}_{u}A$ implies ${\vDash}_{u}B$, or for all $u$ such that $wRu$, ${\vDash}_{u}A$, implies that for all $u$ such that $wRu$, ${\vDash}_{u}B$, or ${\vDash}_{w}\mathrm{\square}A$ implies ${\vDash}_{w}\mathrm{\square}B$, or ${\vDash}_{w}(\mathrm{\square}A\to \mathrm{\square}B)$. Therefore, ${\vDash}_{w}\mathrm{\square}(A\to B)\to (\mathrm{\square}A\to \mathrm{\square}B)$. ∎
From this, we see that Kripke semantics is appropriate only for normal modal logics.
Below are some examples of Kripke frames and their corresponding validating logics:

1.
$A\to \mathrm{\square}A$ is valid in a frame $(W,R)$ iff $R$ weak identity^{}: $wRu$ implies $w=u$.
Proof.
Let $(W,R)$ be a frame validating $A\to \mathrm{\square}A$, and $M$ a model based on $(W,R)$, with $V(p)=\{w\}$. Then ${\vDash}_{w}p$. So ${\vDash}_{w}\mathrm{\square}p$, or ${\vDash}_{u}p$ for all $u$ such that $wRu$. But then $u\in V(p)$, or $u=w$. Hence $R$ is the relation^{}: if $wRu$, then $w=u$.
Conversely, suppose $(W,R)$ is weak identity, $M$ based on $(W,R)$, and $w$ a world in $M$ with ${\vDash}_{w}A$. If $wRu$, then $u=w$, which means ${\vDash}_{u}A$ for all $u$ such that $wRu$. In other words, ${\vDash}_{w}\mathrm{\square}A$, and therefore, ${\vDash}_{w}A\to \mathrm{\square}A$. ∎

2.
$\mathrm{\square}A$ is valid in a frame $(W,R)$ iff $R=\mathrm{\varnothing}$.
Proof.
First, suppose $\mathrm{\square}A$ is valid in $(W,R)$, and $M$ a model based on $(W,R)$, with $V(p)=\mathrm{\varnothing}$. Since ${\vDash}_{w}\mathrm{\square}p$, ${\vDash}_{u}p$ for any $u$ such that $wRu$. Since no such $u$ exists, and $w$ is arbitrary, $R=\mathrm{\varnothing}$.
Conversely, given a model $M$ based on $(W,\mathrm{\varnothing})$, and a world $w$ in $M$, it is vacuously true that ${\vDash}_{u}A$ for any $u$ such that $wRu$, since no such $u$ exists. Therefore ${\vDash}_{w}\mathrm{\square}A$. ∎
A logic is said to be sound if every theorem is valid, and complete^{} if every valid wff is a theorem. Furthermore, a logic is said to have the finite model property if any wff in the class of finite frames is a theorem.
Title  Kripke semantics for modal propositional logic 

Canonical name  KripkeSemanticsForModalPropositionalLogic 
Date of creation  20130322 19:33:22 
Last modified on  20130322 19:33:22 
Owner  CWoo (3771) 
Last modified by  CWoo (3771) 
Numerical id  30 
Author  CWoo (3771) 
Entry type  Definition 
Classification  msc 03B45 
Related topic  ModalLogic 