# Kripke semantics

A Kripke frame (or simply a frame) $\mathcal{F}$ 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) $\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 Boolean-valued 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 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 $(\mathcal{F},V)$ where $w\in V(p)$ iff $V_{w}(p)=1$.

Since the well-formed 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}:=W-S$,

• 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}A\to B$ means $\models_{w}A$ implies $\models_{w}B$ in PL${}_{c}$,

• $\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}$.

 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