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 (well-formed formula) $A$ in PL${}_M$ to a subset $V(A)$ of $W$, such that

   • $V(⟂)=\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 ̸}_w⟂$ 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 ̸}_{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 $ℱ:=(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 $ℱ$. 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	2013-03-22 19:33:22
Last modified on	2013-03-22 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