You are here
HomeKripke semantics for intuitionistic propositional logic
Primary tabs
Kripke semantics for intuitionistic propositional logic
A Kripe model for intuitionistic propositional logic PL${}_{i}$ is a triple $M:=(W,\leq,V)$, where
1. $W$ is a set, whose elements are called possible worlds,
2. $\leq$ is a preorder on $W$,
3. $V$ is a function that takes each wff (wellformed formula) $A$ in PL${}_{i}$ to a subset $V(A)$ of $W$, such that

if $p$ is a propositional variable, $V(p)$ is upper closed,

$V(A\land B)=V(A)\cap V(B)$,

$V(A\lor B)=V(A)\cup V(B)$,

$V(\neg A)=V(A)^{{\#}}$,

$V(A\to B)=(V(A)V(B))^{{\#}}$,
where $S^{{\#}}:=(\downarrow\!\!S)^{c}$, the complement of the lower closure of any $S\subseteq W$.

Remarks.

If $\perp$ were used as a primitive symbol instead of $\neg$, then we require that $V(\perp)=\varnothing$. Then introducing $\neg$ by $\neg A:=A\to\perp$, we get $V(\neg A)=V(A)^{{\#}}$.

Some simple properties of $\#$: for any subset $S$ of $W$, $S^{{\#}}$ is upper closed. This means that for any wff $A$, $V(A)$ is upper closed. Also, $S$ and $S^{{\#}}$ are disjoint, which means that $V(A\land\neg A)=\varnothing$ for any $A$.
One can also define a satisfaction relation $\models$ between $W$ and the set $L$ of wff’s so that
$\models_{w}A\qquad\mbox{iff}\qquad w\in V(A)$ 
for any $w\in W$ and $A\in L$. It’s easy to see that

for any propositional variable $p$, if $\models_{w}p$ and $w\leq u$, then $\models_{u}p$,

$\models_{w}A\land B$ iff $\models_{w}A$ and $\models_{w}B$,

$\models_{w}A\lor B$ iff $\models_{w}A$ or $\models_{w}B$,

$\models_{w}\neg A$ iff for all $u$ such that $w\leq u$, we have $\not\models_{u}A$

$\models_{w}A\to B$ iff for all $u$ such that $w\leq u$, we have $\models_{u}A$ implies $\models_{u}B$.
When $\models_{w}A$, we say that $A$ is true at world $w$.
Remark. Since $V(A)$ is upper closed, $\models_{w}A$ implies $\models_{u}A$ for any $u$ such that $w\leq u$. Now suppose $w\leq u$ and $u\leq w$, then $\models_{w}A$ iff $\models_{u}A$. This shows that, as far as validity of formulas is concerned, we can take $\leq$ to be a partial order in the definition above.
Some examples of Kripke models:
1. Let $M_{1}$ be the model consisting of $W=\{w,u\}$, $\leq=\{(w,w),(u,u),(w,u)\}$, with $V(p)=\{u\}$ and $V(q)=W$. Then $V(p)^{{\#}}=V(q)^{{\#}}=\varnothing$, and we have the following:

$V(p\lor\neg p)=\{u\}$.

$V(q\to p)=V(p)$, and $V(\neg p\to\neg q)=W$, so
$V((\neg p\to\neg q)\to(q\to p))=\{w\}^{{\#}}=\{u\}.$ 
$V(p\to q)=V(\neg q\to\neg p)=W$, so
$V((\neg q\to\neg p)\to(p\to q))=\varnothing^{{\#}}=W.$ 
$V((p\to q)\lor(q\to p))=W$.

In fact, for any wff’s $A,B$, either $V(A)\subseteq V(B)$ or $V(B)\subseteq V(A)$, since $\leq$ is linearly ordered, so that
$V((A\to B)\lor(B\to A))=V(A\to B)\cup V(B\to A)=W,$ assuming $V(A)\subseteq V(B)$.

2. Let $M_{2}$ be the model consisting of $W=\{w,u,v\}$, $\leq=\{(w,w),(u,u),(v,v),(w,u),(w,v)\}$, with $V(p)=\{u\}$ and $V(q)=\{v\}$. Then

$V(\neg p)=V(p)^{{\#}}=\{v\}$,

$V(\neg\neg p)=V(\neg p)^{{\#}}=\{u\}$,

so $V(\neg p\lor\neg\neg p)=\{u,v\}$.

$V(p\to q)=V(p)^{{\#}}=\{v\}$,

$V(q\to p)=V(q)^{{\#}}=\{u\}$,

so $V((p\to q)\lor(q\to p))=\{u,v\}$.

3. Let $M$ be an arbitrary model. Then

$V(A\land B\to A)=(V(A\land B)V(A))^{{\#}}=W$,

$V(A\to A\lor B)=(V(A)V(A\lor B))^{{\#}}=W$,

Suppose $V(A)=V(A\to B)=W$. Then $\varnothing=\downarrow\!\!(V(A)V(B))=\downarrow\!\!(V(B)^{c})$. Since $V(B)$ is upper, $V(B)^{c}$ is lower, so $\varnothing=\downarrow\!\!(V(B)^{c})=V(B)^{c}$, or $W=V(B)$. This shows that modus ponens preserves validity.

4. Let $W$ be any set and $\leq=W^{2}$. Then for any wff $A$, either $V(A)=W$ or $V(A)=\varnothing$. Therefore, $V(\neg\neg A)=V(A)$, and $V(\neg\neg A\to A)=W$.
The pair $\mathcal{F}:=(W,\leq)$ in a Kripke model $M:=(W,\leq,V)$ is also called a (Kripke) frame, and $M$ is said to be a model based on the frame $\mathcal{F}$. The validity of a wff $A$ at various levels can be found in the parent entry. Furthermore, $A$ is valid (with respect to Krikpe semantics) for PL${}_{i}$ if it is valid in the class of all frames.
Based on the examples above, we see that
1. $(\neg q\to\neg p)\to(p\to q)$ is valid in $M_{1}$, while $(\neg p\to\neg q)\to(q\to p)$ is not.
2. $(p\to q)\lor(q\to p)$ is valid in the class of linearly ordered frames, while it is not valid in $M_{2}$, and neither is $\neg p\lor\neg\neg p$.
3. It is not hard to see that $\neg A\lor\neg\neg A$ is valid in any weakly connected frame, that is, for any $w\in W$, the set $\{u\mid w\leq u\}$ is linear.
4. Any wff in any of the schemas $A\land B\to A$, $A\to A\lor B$, or $A\to(B\to A)$ is valid in PL${}_{i}$. See remark below for more detail.
5. Any theorem in the classical propositional logic is valid in any universal frame, that is, a frame with a universal relation.
Remark. It can be shown that every theorem of PL${}_{i}$ is valid. This is the soundness theorem of PL${}_{i}$. Conversely, every valid wff is a theorem. This is known as the completeness theorem of PL${}_{i}$. Furthermore, a wff valid in the class of finite frames is a theorem. This is the finite model property of PL${}_{i}$.
Mathematics Subject Classification
03B55 no label found03B20 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