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

 $\models_{w}A\qquad\mbox{iff}\qquad w\in V(A)$

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 (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 $\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:

 $\square(A\to B)\to(\square A\to\square B)$
###### Proof.

Let $w$ be any world in $M$. Suppose $\models_{w}\square(A\to B)$. Then for all $u$ such that $wRu$, $\models_{u}A\to B$, or $\models_{u}A$ implies $\models_{u}B$, or for all $u$ such that $wRu$, $\models_{u}A$, implies that for all $u$ such that $wRu$, $\models_{u}B$, or $\models_{w}\square A$ implies $\models_{w}\square B$, or $\models_{w}(\square A\to\square B)$. Therefore, $\models_{w}\square(A\to B)\to(\square A\to\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. 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.

Title Kripke semantics for modal propositional logic KripkeSemanticsForModalPropositionalLogic 2013-03-22 19:33:22 2013-03-22 19:33:22 CWoo (3771) CWoo (3771) 30 CWoo (3771) Definition msc 03B45 ModalLogic