You are here
HomeKripke semantics
Primary tabs
Kripke semantics
A Kripke frame (or simply a frame) $\mathcal{F}$ is a pair $(W,R)$ where $W$ is a nonempty 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) $\Lambda$ is a pair $(\mathcal{F},V)$, where $\mathcal{F}:=(W,R)$ is a Kripke frame, and $V$ is a function that takes each atomic formula of $\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 $\Lambda$model based on the frame $\mathcal{F}$ if $M=(\mathcal{F},V)$ is a model for the logic $\Lambda$.
Remark. Associated with each world $w$, we may also define a Booleanvalued valuation $V_{w}$ on the set of all wff’s of $\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 truthvalue semantics for classical propositional logic. The truthvalue 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 $(\mathcal{F},V)$ where $w\in V(p)$ iff $V_{w}(p)=1$.
Since the wellformed formulas (wff’s) of $\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}:=WS$,

in the modal propositional logic $K$, $V(\square A):=V(A)^{{\square}}$, where $S^{{\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))^{{\#}}$, where $S^{{\#}}:=(\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\models_{w}A\qquad\mbox{or}\qquad\models_{w}A$ 
if no confusion arises. If $w\notin V(A)$, we write $M\not\models_{w}A$. The three examples above can be now interpreted as:

$\models_{w}\square A$ means for all worlds $v$ with $wRv$, we have $\models_{v}A$ in $K$, and

$\models_{w}A\to B$ means for all worlds $v$ with $wRv$, $\models_{v}A$ implies $\models_{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 $\mathcal{F}$,

in a collection $\mathcal{C}$ of frames if $A$ is valid in all frames in $\mathcal{C}$.
We denote
$M\models A,\qquad\mathcal{F}\models A,\qquad\mbox{or}\qquad\mathcal{C}\models A$ 
if $A$ is valid in $M,\mathcal{F}$, or $\mathcal{C}$ respectively.
A logic $\Lambda$, equipped with a deductive system, is sound in $\mathcal{C}$ if
$\vdash A\qquad\mbox{implies}\qquad\mathcal{C}\models A.$ 
Here, $\vdash A$ means that wff $A$ is a theorem deducible from the deductive system of $\Lambda$. Conversely, if
$\mathcal{C}\models A\qquad\mbox{implies}\qquad\vdash A,$ 
we say that $\Lambda$ is complete in $\mathcal{C}$.
Mathematics Subject Classification
03B48 no label found03B20 no label found03B45 no label found Forums
 Planetary Bugs
 HS/Secondary
 University/Tertiary
 Graduate/Advanced
 Industry/Practice
 Research Topics
 LaTeX help
 Math Comptetitions
 Math History
 Math Humor
 PlanetMath Comments
 PlanetMath System Updates and News
 PlanetMath help
 PlanetMath.ORG
 Strategic Communications Development
 The Math Pub
 Testing messages (ignore)
 Other useful stuff
 Corrections