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

1. 1.

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

2. 2.

   $R$ is a binary relation on $W$,

3. 3.

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

   • $V(\perp)=\varnothing$,

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

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

For derived connectives, we also have $V(A\land B)=V(A)\cap V(B)$, $V(A\lor B)=V(A)\cup V(B)$, $V(\neg A)=V(A)^{c}$, the complement of $V(A)$, and $V(\diamond A)=V(A)^{{\diamond}}:=V(A)^{{c\square c}}$.

One can also define a satisfaction relation $\models$ between $W$ and the set $L$ of wff’s so that

for any $w\in W$ and $A\in L$. It’s easy to see that

• $\not\models_{w}\perp$ for any $w\in W$,

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

• $\models_{w}A\land B$ iff $\models_{w}A$ and $\models_{w}B$,

• $\models_{w}A\lor B$ iff $\models_{w}A$ or $\models_{w}B$,

• $\models_{w}\neg A$ iff $\not\models_{w}A$,

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

• $\models_{w}\diamond A$ iff there is a $u$ such that $wRu$ and $\models_{u}A$.

When $\models_{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.

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 $\models_{w}A$ and $\models_{w}A\to B$. Since $\models_{w}A$ implies $\models_{w}B$, and $\models_{w}A$ by assumption, we have $\models_{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 $\models_{w}A$ and $\models_{w}B$, then $\models_{w}A$, so $\models_{w}B\to A$.

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

• $(\neg A\to\neg B)\to(B\to A)$: we use a different approach to show this:

  	$\displaystyle V((\neg A\to\neg B)\to(B\to A))$	$\displaystyle=$	$\displaystyle V(\neg A\to\neg B)^{c}\cup V(B\to A)$
  		$\displaystyle=$	$\displaystyle(V(\neg A)\cap V(\neg B)^{c})\cup V(B)^{c}\cup V(A)$
  		$\displaystyle=$	$\displaystyle(V(A)^{c}\cap V(B))\cup V(B)^{c}\cup V(A)$
  		$\displaystyle=$	$\displaystyle(V(A)^{c}\cup V(B)^{c})\cup V(A)=W.$

In addition, the rule of necessitation preserves validity as well: suppose $\models_{w}A$ for all $w$, then certainly $\models_{u}A$ for all $u$ such that $wRu$, and therefore $\models_{w}\square A$.

There are also valid formulas that are not tautologies. Here’s one:

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

   $A\to\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\square A$, and $M$ a model based on $(W,R)$, with $V(p)=\{w\}$. Then $\models_{w}p$. So $\models_{w}\square p$, or $\models_{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 $\models_{w}A$. If $wRu$, then $u=w$, which means $\models_{u}A$ for all $u$ such that $wRu$. In other words, $\models_{w}\square A$, and therefore, $\models_{w}A\to\square A$. ∎

2. 2.

   $\square A$ is valid in a frame $(W,R)$ iff $R=\varnothing$.

   Proof.

   First, suppose $\square A$ is valid in $(W,R)$, and $M$ a model based on $(W,R)$, with $V(p)=\varnothing$. Since $\models_{w}\square p$, $\models_{u}p$ for any $u$ such that $wRu$. Since no such $u$ exists, and $w$ is arbitrary, $R=\varnothing$.

   Conversely, given a model $M$ based on $(W,\varnothing)$, and a world $w$ in $M$, it is vacuously true that $\models_{u}A$ for any $u$ such that $wRu$, since no such $u$ exists. Therefore $\models_{w}\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.