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) $\mathrm{\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 $\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 $\mathcal{F}$ if $M=(\mathcal{F},V)$ is a model for the logic $\mathrm{\Lambda}$.
Remark. Associated with each world $w$, we may also define a Booleanvalued 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 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 $\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}:=WS$,

•
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 \u0338}_{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 $\mathcal{F}$,

•
in a collection $\mathcal{C}$ of frames if $A$ is valid in all frames in $\mathcal{C}$.
We denote
$$M\vDash A,\mathcal{F}\vDash A,\text{or}\mathit{\hspace{1em}\hspace{1em}}\mathcal{C}\vDash A$$ 
if $A$ is valid in $M,\mathcal{F}$, or $\mathcal{C}$ respectively.
A logic $\mathrm{\Lambda}$, equipped with a deductive system, is sound in $\mathcal{C}$ if
$$\u22a2A\mathit{\hspace{1em}\hspace{1em}}\text{implies}\mathit{\hspace{1em}\hspace{1em}}\mathcal{C}\vDash A.$$ 
Here, $\u22a2A$ means that wff $A$ is a theorem^{} deducible^{} from the deductive system of $\mathrm{\Lambda}$. Conversely, if
$$\mathcal{C}\vDash A\mathit{\hspace{1em}\hspace{1em}}\text{implies}\mathit{\hspace{1em}\hspace{1em}}\u22a2A,$$ 
we say that $\mathrm{\Lambda}$ is complete^{} in $\mathcal{C}$.
Title  Kripke semantics 
Canonical name  KripkeSemantics 
Date of creation  20130322 19:31:15 
Last modified on  20130322 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 