some theorem schemas of propositional logic (original) (raw)

First, some theorem schemas:

    1. A→¬⁢¬⁢A
    1. ¬⁢¬⁢A→A
    1. (law of the excluded middle) A∨¬⁢A
    1. (ex falso quodlibet) ⟂→A
    1. A↔A
    1. A∧B→A and A∧B→B
    1. (law of importation) (A→(B→C))→(A∧B→C)
    1. (A→B)→((B→(C→D))→(A∧C→D))
    1. (A→B)↔(A→(A→B))
Proof.

Many of these can be easily proved using the deduction theorem:

    1. we need to show A⊢¬⁢¬⁢A, which means we need to show A,¬⁢A⊢⟂. Since ¬⁢A is A→⟂, by modus ponensMathworldPlanetmath, A,¬⁢A⊢⟂.
    1. we observe first that ¬⁢A→¬⁢¬⁢¬⁢A is an instance of the above theorem schema, since (¬A→¬¬¬A)→(¬¬A→A) is an instance of one of the axiom schemasMathworldPlanetmath, we have ⊢¬⁢¬⁢A→A as a result.
    1. since A∨¬⁢A is ¬⁢A→¬⁢A, to show ⊢A∨¬⁢A, we need to show ¬⁢A⊢¬⁢A, but this is obvious.
    1. we need to show ⟂⊢A. Since ⟂,⟂→(A→⟂),A→⟂ is a deductionMathworldPlanetmathPlanetmath of A→⟂ from ⟂, and the result follows.
    1. this is because ⊢A→A, so ⊢(A→A)∧(A→A).
    1. this is the result of the first two theorem schemas above.

For the next four schemas, we need the the following meta-theorems (see here (http://planetmath.org/SomeMetatheoremsOfPropositionalLogic) for proofs):

  1. M1.
    Δ⊢A and Δ⊢B iff Δ⊢A∧B
  2. M2.
    Δ⊢A implies Δ⊢B iff Δ⊢A→B
    1. If ⊢A∧B, then ⊢A by M1, so ⊢A∧B→A by M2. Similarly, ⊢A∧B→B.
    1. ⊢A∧A→A comes from 7, and since ⊢A implies ⊢A∧A by M1, ⊢A→A∧A by M2. Therefore, ⊢A↔A∧A by M1.
    1. If ⊢A∧B, then ⊢A and ⊢B by M1, so ⊢B∧A by M1 again, and therefore ⊢A∧B→B∧A by M2. Similarly, ⊢B∧A→A∧B. Combining the two and apply M1, we have the result.
    1. If ⊢(A∧B)∧C, then ⊢A∧B and ⊢C, so ⊢A, ⊢B, and ⊢C by M1. By M1 again, we have ⊢A and ⊢B∧C, and another application of M1, ⊢A∧(B∧C). Therefore, by M2, ⊢(A∧B)∧C→A∧(B∧C), Similarly, ⊢A∧(B∧C)→(A∧B)∧C. Combining the two and applying M1, we have the result.
    1. A→B,B→C,A⊢C by modus ponens 3 times.
    1. A→(B→C),A∧B,A∧B→A,A,B→C,A∧B→B,B,C is a deduction of C from A→(B→C) and A∧B.
    1. A→B,B→(C→D),A∧C,A∧C→A,A,B,C→D,A∧C→C,C,D is a deduction of D from A→B,B→(C→D), and A∧C.
    1. (A→B)→(A→(A→B)) is just an axiom, while ⊢(A→(A→B))→(A→B) comes from two applications of the deduction theorem to A→(A→B),A⊢B, which is the result of the deduction A→(A→B),A,A→B,B of B from A→(A→B) and A.

∎