Kripke semantics for intuitionistic propositional logic

A Kripe model for intuitionistic propositional logic  PL${}_{i}$ is a triple $M:=(W,\leq,V)$, where

1. 1.

$W$ is a set, whose elements are called possible worlds,

2. 2.
3. 3.

$V$ is a function that takes each wff (well-formed 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. 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. 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. 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$,

• $V(A\to(B\to A))=(V(A)-V(B\to A))^{\#}=(V(A)-(V(B)-V(A))^{\#})^{\#}=W$. The last equation comes from the fact that for any upper set $S$, $S\subseteq S^{c\#}$.

• 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. 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. 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. 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. 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. 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. 5.

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

Title Kripke semantics for intuitionistic propositional logic KripkeSemanticsForIntuitionisticPropositionalLogic 2013-03-22 19:33:19 2013-03-22 19:33:19 CWoo (3771) CWoo (3771) 35 CWoo (3771) Definition msc 03B55 msc 03B20 AxiomSystemForIntuitionisticLogic