Kripke semantics for intuitionistic propositional logic

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

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

2. $\le$ is a preorder on $W$,

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\wedge B)=V(A)\cap V(B)$,

   • $V(A\vee B)=V(A)\cup V(B)$,

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

   • $V(A\to B)={(V(A)-V(B))}^{\mathrm{\#}}$,

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

Remarks.

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

• Some simple properties of $\mathrm{\#}$: for any subset $S$ of $W$, $S^{\mathrm{\#}}$ is upper closed. This means that for any wff $A$, $V(A)$ is upper closed. Also, $S$ and $S^{\mathrm{\#}}$ are disjoint, which means that $V(A\wedge \mathrm{\neg }A)=\mathrm{\varnothing }$ for any $A$.

One can also define a satisfaction relation $\vDash$ between $W$ and the set $L$ of wff’s so that

$${\vDash }_{w}A\mathit{\hspace{1em}\hspace{1em}}\text{iff}\mathit{\hspace{1em}\hspace{1em}}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 ${\vDash }_{w}p$ and $w\le u$, then ${\vDash }_{u}p$,

• ${\vDash }_{w}A\wedge B$ iff ${\vDash }_{w}A$ and ${\vDash }_{w}B$,

• ${\vDash }_{w}A\vee B$ iff ${\vDash }_{w}A$ or ${\vDash }_{w}B$,

• ${\vDash }_w\mathrm{\neg }A$ iff for all $u$ such that $w\le u$, we have ${\vDash ̸}_{u}A$

• ${\vDash }_{w}A\to B$ iff for all $u$ such that $w\le u$, we have ${\vDash }_{u}A$ implies ${\vDash }_{u}B$.

When ${\vDash }_{w}A$, we say that $A$ is true at world $w$.

Remark. Since $V(A)$ is upper closed, ${\vDash }_{w}A$ implies ${\vDash }_{u}A$ for any $u$ such that $w\le u$. Now suppose $w\le u$ and $u\le w$, then ${\vDash }_{w}A$ iff ${\vDash }_{u}A$. This shows that, as far as validity of formulas is concerned, we can take $\le$ 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\}$, $\le =\{(w,w),(u,u),(w,u)\}$, with $V(p)=\{u\}$ and $V(q)=W$. Then $V{(p)}^{\mathrm{\#}}=V{(q)}^{\mathrm{\#}}=\mathrm{\varnothing }$, and we have the following:

   • $V(p\vee \mathrm{\neg }p)=\{u\}$.

   • $V(q\to p)=V(p)$, and $V(\mathrm{\neg }p\to \mathrm{\neg }q)=W$, so

     $$V((\mathrm{\neg }p\to \mathrm{\neg }q)\to (q\to p))={\{w\}}^{\mathrm{\#}}=\{u\}.$$

   • $V(p\to q)=V(\mathrm{\neg }q\to \mathrm{\neg }p)=W$, so

     $$V((\mathrm{\neg }q\to \mathrm{\neg }p)\to (p\to q))={\mathrm{\varnothing }}^{\mathrm{\#}}=W.$$

   • $V((p\to q)\vee (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 $\le$ is linearly ordered, so that

     $$V((A\to B)\vee (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\}$, $\le =\{(w,w),(u,u),(v,v),(w,u),(w,v)\}$, with $V(p)=\{u\}$ and $V(q)=\{v\}$. Then

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

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

   • so $V(\mathrm{\neg }p\vee \mathrm{\neg }\mathrm{\neg }p)=\{u,v\}$.

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

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

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

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

   • $V(A\wedge B\to A)={(V(A\wedge B)-V(A))}^{\mathrm{\#}}=W$,

   • $V(A\to A\vee B)={(V(A)-V(A\vee B))}^{\mathrm{\#}}=W$,

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

   • Suppose $V(A)=V(A\to B)=W$. Then $\mathrm{\varnothing }=\downarrow (V(A)-V(B))=\downarrow (V{(B)}^c)$. Since $V(B)$ is upper, $V{(B)}^c$ is lower, so $\mathrm{\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 $\le =W^2$. Then for any wff $A$, either $V(A)=W$ or $V(A)=\mathrm{\varnothing }$. Therefore, $V(\mathrm{\neg }\mathrm{\neg }A)=V(A)$, and $V(\mathrm{\neg }\mathrm{\neg }A\to A)=W$.

The pair $ℱ:=(W,\le )$ in a Kripke model $M:=(W,\le ,V)$ is also called a (Kripke) frame, and $M$ is said to be a model based on the frame $ℱ$. 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. $(\mathrm{\neg }q\to \mathrm{\neg }p)\to (p\to q)$ is valid in $M_1$, while $(\mathrm{\neg }p\to \mathrm{\neg }q)\to (q\to p)$ is not.

2. $(p\to q)\vee (q\to p)$ is valid in the class of linearly ordered frames, while it is not valid in $M_2$, and neither is $\mathrm{\neg }p\vee \mathrm{\neg }\mathrm{\neg }p$.

3. It is not hard to see that $\mathrm{\neg }A\vee \mathrm{\neg }\mathrm{\neg }A$ is valid in any weakly connected frame, that is, for any $w\in W$, the set $\{u\mid w\le u\}$ is linear.

4. Any wff in any of the schemas $A\wedge B\to A$, $A\to A\vee 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$.

Title	Kripke semantics for intuitionistic propositional logic
Canonical name	KripkeSemanticsForIntuitionisticPropositionalLogic
Date of creation	2013-03-22 19:33:19
Last modified on	2013-03-22 19:33:19
Owner	CWoo (3771)
Last modified by	CWoo (3771)
Numerical id	35
Author	CWoo (3771)
Entry type	Definition
Classification	msc 03B55
Classification	msc 03B20
Related topic	AxiomSystemForIntuitionisticLogic