Kripke semantics

A Kripke frame (or simply a frame) $ℱ$ is a pair $(W,R)$ where $W$ is a non-empty set whose elements are called worlds or possible worlds, $R$ is a binary relation on $W$ called the accessibility relation. When $vRw$, we say that $w$ is accessible from $v$. A Kripke frame is said to have property $P$ if $R$ has the property $P$. For example, a symmetric frame is a frame whose accessibility relation is symmetric.

A Kripke model (or simply a model) $M$ for a propositional logical system (classical, intuitionistic, or modal) $\mathrm{\Lambda }$ is a pair $(ℱ,V)$, where $ℱ:=(W,R)$ is a Kripke frame, and $V$ is a function that takes each atomic formula of $\mathrm{\Lambda }$ to a subset of $W$. If $w\in V(p)$, we say that $p$ is true at world $w$. We say that $M$ is a $\mathrm{\Lambda }$-model based on the frame $ℱ$ if $M=(ℱ,V)$ is a model for the logic $\mathrm{\Lambda }$.

Remark. Associated with each world $w$, we may also define a Boolean-valued valuation $V_w$ on the set of all wff’s of $\mathrm{\Lambda }$, so that $V_w(p)=1$ iff $w\in V(p)$. In this sense, the Kripke semantics can be thought of as a generalization of the truth-value semantics for classical propositional logic. The truth-value semantics is just a Kripke model based on a frame with one world. Conversely, given a collection of valuations $\{V_w\mid w\in W\}$, we have model $(ℱ,V)$ where $w\in V(p)$ iff $V_w(p)=1$.

Since the well-formed formulas (wff’s) of $\mathrm{\Lambda }$ are uniquely readable, $V$ may be inductively extended so it is defined on all wff’s. The following are some examples:

• in classical propositional logic PL${}_c$, $V(A\to B):=V{(A)}^c\cup V(B)$, where $S^c:=W-S$,

• in the modal propositional logic $K$, $V(\mathrm{\square }A):=V{(A)}^{\mathrm{\square }}$, where $S^{\mathrm{\square }}:=\{u\mid \uparrow u\subseteq S\}$, and $\uparrow u:=\{w\mid uRw\}$, and

• in intuitionistic propositional logic PL${}_i$, $V(A\to B):={(V(A)-V(B))}^{\mathrm{\#}}$, where $S^{\mathrm{\#}}:={(\downarrow S)}^c$, and $\downarrow S:=\{u\mid uRw,w\in S\}$.

Truth at a world can now be defined for wff’s: a wff $A$ is true at world $w$ if $w\in V(A)$, and we write

$$M{\vDash }_{w}A\mathit{\hspace{1em}\hspace{1em}}\text{or}\mathit{\hspace{1em}\hspace{1em}}{\vDash }_{w}A$$

if no confusion arises. If $w\notin V(A)$, we write $M{\vDash ̸}_{w}A$. The three examples above can be now interpreted as:

• ${\vDash }_{w}A\to B$ means ${\vDash }_{w}A$ implies ${\vDash }_{w}B$ in PL${}_c$,

• ${\vDash }_w\mathrm{\square }A$ means for all worlds $v$ with $wRv$, we have ${\vDash }_{v}A$ in $K$, and

• ${\vDash }_{w}A\to B$ means for all worlds $v$ with $wRv$, ${\vDash }_{v}A$ implies ${\vDash }_{v}B$ in PL${}_i$.

A wff $A$ is said to be valid

• in a model $M$ if $A$ in true at all possible worlds $w$ in $M$,

• in a frame if $A$ is valid in all models $M$ based on $ℱ$,

• in a collection $𝒞$ of frames if $A$ is valid in all frames in $𝒞$.

We denote

$$M\vDash A,ℱ\vDash A,\text{or}\mathit{\hspace{1em}\hspace{1em}}𝒞\vDash A$$

if $A$ is valid in $M,ℱ$, or $𝒞$ respectively.

A logic $\mathrm{\Lambda }$, equipped with a deductive system, is sound in $𝒞$ if

$$⊢A\mathit{\hspace{1em}\hspace{1em}}\text{implies}\mathit{\hspace{1em}\hspace{1em}}𝒞\vDash A.$$

Here, $⊢A$ means that wff $A$ is a theorem deducible from the deductive system of $\mathrm{\Lambda }$. Conversely, if

$$𝒞\vDash A\mathit{\hspace{1em}\hspace{1em}}\text{implies}\mathit{\hspace{1em}\hspace{1em}}⊢A,$$

we say that $\mathrm{\Lambda }$ is complete in $𝒞$.

Title	Kripke semantics
Canonical name	KripkeSemantics
Date of creation	2013-03-22 19:31:15
Last modified on	2013-03-22 19:31:15
Owner	CWoo (3771)
Last modified by	CWoo (3771)
Numerical id	25
Author	CWoo (3771)
Entry type	Definition
Classification	msc 03B48
Classification	msc 03B20
Classification	msc 03B45
Defines	Kripke frame
Defines	possible world
Defines	accessibility relation
Defines	accessible
Defines	valid
Defines	sound
Defines	complete