truth-value semantics for intuitionistic propositional logic is sound


We show that, for each positive integer n, every theorem of intuitionistic propositional logicPlanetmathPlanetmath is a tautologyMathworldPlanetmath for Vn. This amounts to showing that, for every interpretationMathworldPlanetmathPlanetmath v on Vn,

  • each axiom is true, and

  • modus ponensMathworldPlanetmath preserves truth.

Let us take care of the second one first. Suppose v(A)=v(AB)=n. If v(A)v(B), then v(B)=n. Otherwise, v(B)<v(A). But this means that n=v(AB)=v(B), forcingMathworldPlanetmath v(B)=n. Therefore, v(B)=n.

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

  1. 1.

    (AB)A and (AB)B.

    Since v(AB)=min{v(A),v(B)}v(A), we get v((AB)A)=n. The other one is proved similarly.

  2. 2.

    A(AB) and B(AB).

    Since v(A)max{v(A),v(B)}=v(AB), we get v(A(AB))=n. The other one is proved similarly.

  3. 3.


    If v(B)v(A), v(BA)=n, so that v(A(BA))=n as well. If v(A)<v(B), then v(BA)=v(A), so that v(A(BA))=n.

  4. 4.


    If v(A)v(B), v(AB)=n, so that v(¬A(AB))=n as well. If v(B)<v(A), then v(AB)=v(B). Also, v(B)<v(A) implies that v(A)>0, so that v(¬A)=0, and v(¬A(AB))=n as a result.

  5. 5.


    If v(B)=v(AB), then v(B)v(A) and v(B(AB))=n, so that v(A(B(AB))=n also. If on the other hand v(AB)<v(B), then


    so that

  6. 6.


    If v(B)=v(AB), then v(A)v(B), and


    so that


    as well. Otherwise, v(B)<v(A)=v(AB). This means that


    and therefore


    by 3 above.

  7. 7.


    It is clear that v(C)v(BC). If v(C)=v(BC), then


    so that


    too. If v(C)<v(BC), then v(BC)=n, which implies v(B)v(C). This in turn implies that v(AB)v(AC), so that


    But by 3 above,




    as a result.

  8. 8.


    Pick any C such that v(C)=0, such as D¬D. Then v(¬B)=v(BC), so that


    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(AB)=n.

  • if v(B)=0, then v(AB)=v(¬A).

  • if v(A)=n, then v(AB)=v(B).

  • v(B)v(AB).

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

    • v(AB)v(AC),

    • v(AB)v(AC),

    • v(AB)v(AC),

    • v(CA)v(BA).

From the facts above, one readily deduces:

  • if v(B)v(C), then v(¬C)v(¬B),

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

    • v(AB)=v(AC),

    • v(AB)=v(AC),

    • v(AB)=v(AC),

    • v(CA)=v(BA),

    • v(¬B)=v(¬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