truth-value semantics for intuitionistic propositional logic is sound

Proposition 1.

The truth-value semantics for intuitionistic propositional logic is sound.

Proof.

We show that, for each positive integer $n$, every theorem of intuitionistic propositional logic is a tautology for $V_n$. This amounts to showing that, for every interpretation $v$ on $V_n$,

• each axiom is true, and

• modus ponens preserves truth.

Let us take care of the second one first. Suppose $v(A)=v(A\to B)=n$. If $v(A)\le v(B)$, then $v(B)=n$. Otherwise, . But this means that $n=v(A\to B)=v(B)$, forcing $v(B)=n$. Therefore, $v(B)=n$.

Now, we verify that each of the axiom schemas below are true:

1. $(A\wedge B)\to A$ and $(A\wedge B)\to B$.

   Since $v(A\wedge B)=\min \{v(A),v(B)\}\le v(A)$, we get $v((A\wedge B)\to A)=n$. The other one is proved similarly.

2. $A\to (A\vee B)$ and $B\to (A\vee B)$.

   Since $v(A)\le \max \{v(A),v(B)\}=v(A\vee B)$, we get $v(A\to (A\vee B))=n$. The other one is proved similarly.

3. $A\to (B\to A)$.

   If $v(B)\le v(A)$, $v(B\to A)=n$, so that $v(A\to (B\to A))=n$ as well. If , then $v(B\to A)=v(A)$, so that $v(A\to (B\to A))=n$.

4. $\mathrm{\neg }A\to (A\to B)$.

   If $v(A)\le v(B)$, $v(A\to B)=n$, so that $v(\mathrm{\neg }A\to (A\to B))=n$ as well. If , then $v(A\to B)=v(B)$. Also, implies that $v(A)>0$, so that $v(\mathrm{\neg }A)=0$, and $v(\mathrm{\neg }A\to (A\to B))=n$ as a result.

5. $A\to (B\to (A\wedge B))$.

   If $v(B)=v(A\wedge B)$, then $v(B)\le v(A)$ and $v(B\to (A\wedge B))=n$, so that $v(A\to (B\to (A\wedge B))=n$ also. If on the other hand , then

   $$v(A)=v(A\wedge B)\mathit{\hspace{1em}}\text{and}\mathit{\hspace{1em}}v(B\to (A\wedge B))=v(A\wedge B),$$

   so that

   $$v(A\to (B\to (A\wedge B)))=v(A\to (A\wedge B))=n.$$

6. $(A\to C)\to ((B\to C)\to ((A\vee B)\to C))$.

   If $v(B)=v(A\vee B)$, then $v(A)\le v(B)$, and

   $$v((B\to C)\to ((A\vee B)\to C))=v((B\to C)\to (B\to C))=n,$$

   so that

   $$v((A\to C)\to ((B\to C)\to ((A\vee B)\to C)))=n$$

   as well. Otherwise, . This means that

   $$v((B\to C)\to ((A\vee B)\to C)))=v((B\to C)\to (A\to C)),$$

   and therefore

   $$v((A\to C)\to ((B\to C)\to ((A\vee B)\to C)))=v((A\to C)\to ((B\to C)\to (A\to C)))=n$$

   by 3 above.

7. $(A\to B)\to ((A\to (B\to C))\to (A\to C))$.

   It is clear that $v(C)\le v(B\to C)$. If $v(C)=v(B\to C)$, then

   $$v((A\to (B\to C))\to (A\to C))=v((A\to C)\to (A\to C))=n,$$

   so that

   $$v((A\to B)\to ((A\to (B\to C))\to (A\to C)))=n$$

   too. If , then $v(B\to C)=n$, which implies $v(B)\le v(C)$. This in turn implies that $v(A\to B)\le v(A\to C)$, so that

   $$v((A\to C)\to ((A\to (B\to C))\to (A\to C)))\le v((A\to B)\to ((A\to (B\to C))\to (A\to C))).$$

   But by 3 above,

   $$v((A\to C)\to ((A\to (B\to C))\to (A\to C)))=n,$$

   hence

   $$v((A\to B)\to ((A\to (B\to C))\to (A\to C)))=n$$

   as a result.

8. $(A\to B)\to ((A\to \mathrm{\neg }B)\to \mathrm{\neg }A)$.

   Pick any $C$ such that $v(C)=0$, such as $D\wedge \mathrm{\neg }D$. Then $v(\mathrm{\neg }B)=v(B\to C)$, so that

   $$v((A\to B)\to ((A\to \mathrm{\neg }B)\to \mathrm{\neg }A))=v((A\to B)\to ((A\to (B\to C))\to (A\to C)))=n$$

   by 7.

∎

Note that the proofs of the axioms employ some elementary facts, for any wff’s $A,B,C$:

• If $v(B)=n$ or $v(A)=0$, then $v(A\to B)=n$.

• if $v(B)=0$, then $v(A\to B)=v(\mathrm{\neg }A)$.

• if $v(A)=n$, then $v(A\to B)=v(B)$.

• $v(B)\le v(A\to B)$.

• if $v(B)\le v(C)$, then

  • $v(A\vee B)\le v(A\vee C)$,

  • $v(A\wedge B)\le v(A\wedge C)$,

  • $v(A\to B)\le v(A\to C)$,

  • $v(C\to A)\le v(B\to A)$.

From the facts above, one readily deduces:

• if $v(B)\le v(C)$, then $v(\mathrm{\neg }C)\le v(\mathrm{\neg }B)$,

• if $v(B)=v(C)$, then

  • $v(A\vee B)=v(A\vee C)$,

  • $v(A\wedge B)=v(A\wedge C)$,

  • $v(A\to B)=v(A\to C)$,

  • $v(C\to A)=v(B\to A)$,

  • $v(\mathrm{\neg }B)=v(\mathrm{\neg }C)$.

Title	truth-value semantics for intuitionistic propositional logic is sound
Canonical name	TruthvalueSemanticsForIntuitionisticPropositionalLogicIsSound
Date of creation	2013-03-22 19:31:38
Last modified on	2013-03-22 19:31:38
Owner	CWoo (3771)
Last modified by	CWoo (3771)
Numerical id	21
Author	CWoo (3771)
Entry type	Definition
Classification	msc 03B20