truth-value semantics for intuitionistic propositional logic is sound


Proof.

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.

    A(BA).

    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.

    ¬A(AB).

    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.

    A(B(AB)).

    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

    v(A)=v(AB)andv(B(AB))=v(AB),

    so that

    v(A(B(AB)))=v(A(AB))=n.
  6. 6.

    (AC)((BC)((AB)C)).

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

    v((BC)((AB)C))=v((BC)(BC))=n,

    so that

    v((AC)((BC)((AB)C)))=n

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

    v((BC)((AB)C)))=v((BC)(AC)),

    and therefore

    v((AC)((BC)((AB)C)))=v((AC)((BC)(AC)))=n

    by 3 above.

  7. 7.

    (AB)((A(BC))(AC)).

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

    v((A(BC))(AC))=v((AC)(AC))=n,

    so that

    v((AB)((A(BC))(AC)))=n

    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

    v((AC)((A(BC))(AC)))v((AB)((A(BC))(AC))).

    But by 3 above,

    v((AC)((A(BC))(AC)))=n,

    hence

    v((AB)((A(BC))(AC)))=n

    as a result.

  8. 8.

    (AB)((A¬B)¬A).

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

    v((AB)((A¬B)¬A))=v((AB)((A(BC))(AC)))=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(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