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 $𝒞$.