some theorem schemas of intuitionistic propositional logic
We present some theorem schemas of intuitionistic propositional logic and their deductions
, based on the axiom system given in this entry (http://planetmath.org/AxiomSystemForIntuitionisticLogic).
1. A∨B→B∨A
Proof.
From the deduction
-
1.
A→B∨A,
-
2.
B→B∨A,
-
3.
(A→B∨A)→((B→B∨A)→(A∨B→B∨A)),
-
4.
(B→B∨A)→(A∨B→B∨A),
-
5.
A∨B→B∨A,
so we get A∨B⊢iB∨A, and therefore ⊢iA∨B→B∨A by the deduction theorem.
∎
2. (A∧B)∧C→A∧(B∧C)
Proof.
From the deduction
-
1.
(A∧B)∧C→A→B,
-
2.
(A∧B)∧C→C,
-
3.
(A∧B)∧C,
-
4.
A∧B,
-
5.
C,
-
6.
A∧B→A,
-
7.
A∧B→B,
-
8.
A,
-
9.
B,
-
10.
B→(C→B∧C),
-
11.
C→B∧C,
-
12.
B∧C,
-
13.
A→(B∧C→A∧(B∧C)),
-
14.
B∧C→A∧(B∧C),
-
15.
A∧(B∧C),
so (A∧B)∧C⊢iA∧(B∧C), and therefore ⊢i(A∧B)∧C→A∧(B∧C) by the deduction theorem. ∎
3. (A→(B→C))→((A→B)→(A→C))
Proof.
From the deduction
-
1.
(A→B)→((A→(B→C))→(A→C)),
-
2.
A→B,
-
3.
(A→(B→C))→(A→C),
-
4.
A→(B→C),
-
5.
A→C,
so A→(B→C),A→B⊢iA→C. By two applications of the deduction theorem, ⊢i(A→(B→C))→((A→B)→(A→C)). ∎
4. A∧¬A→B
Proof.
From the deduction
-
1.
A∧¬A→A,
-
2.
A∧¬A→¬A,
-
3.
A∧¬A,
-
4.
¬A,
-
5.
A,
-
6.
¬A→(A→B),
-
7.
A→B,
-
8.
B
so A∧¬A⊢iB. By the deduction theorem, ⊢iA∧¬A→B. ∎
5. A→¬¬A
Proof.
From the deduction
-
1.
A→(¬A→A),
-
2.
A,
-
3.
¬A→A,
-
4.
(¬A→A)→((¬A→¬A)→¬¬A),
-
5.
(¬A→¬A)→¬¬A,
-
6.
¬A→¬A,
-
7.
¬¬A,
so A⊢i¬¬A. By the deduction theorem, ⊢iA→¬A¬A. ∎
In the proof above, we use the schema B→B in step 6 of the deduction, because ⊢iB→B, as a result of applying the deduction theorem to B⊢iB.
6. ¬¬¬A→¬A
Proof.
From the deduction
-
1.
(A→¬¬A)→((A→¬¬¬A)→¬A),
-
2.
A→¬¬A,
-
3.
(A→¬¬¬A)→¬A,
-
4.
¬¬¬A→(A→¬¬¬A),
-
5.
¬¬¬A,
-
6.
A→¬¬¬A,
-
7.
¬A,
so A→¬¬A,¬¬¬A⊢i¬A. By the deduction theorem, A→¬¬A,⊢i¬¬¬A→¬A. Since ⊢iA→¬A¬A, ⊢i¬¬¬A→¬A as a result. ∎
In the above proof, we use the fact that if ⊢iC and C⊢iD, then ⊢iD. This is the result of the following fact: if ⊢iC and ⊢iC→D, then ⊢iD.
7. (A→B)→(¬B→¬A)
Proof.
From the deduction
-
1.
(A→B)→((A→¬B)→¬A),
-
2.
A→B,
-
3.
(A→¬B)→¬A,
-
4.
¬B→(A→¬B),
-
5.
¬B,
-
6.
A→¬B,
-
7.
¬A,
so A→B,¬B⊢i¬A. Applying the deduction theorem twice gives us ⊢i(A→B)→(¬B→¬A). ∎
8. ¬(A∧¬A)
Proof.
From the deduction
-
1.
(A∧¬A→B)→((A∧¬A→¬B)→¬(A∧¬A)),
-
2.
A∧¬A→B,
-
3.
(A∧¬A→¬B)→¬(A∧¬A),
-
4.
A∧¬A→¬B,
-
5.
¬(A∧¬A).
Since ⊢iA∧¬A→B and ⊢iA∧¬A→¬B are instances of theorem schema 4 above, ⊢i¬(A∧¬A) as a result. ∎
This also shows that ⊢iB→¬(A∧¬A), which is the result of applying modus ponens to ¬(A∧¬A) to ¬(A∧¬A)→(B→¬(A∧¬A)).
9. (B→A∧¬A)→¬B
Proof.
From the deduction
-
1.
B→A∧¬A,
-
2.
(B→A∧¬A)→((B→¬(A∧¬A))→¬B),
-
3.
(B→¬(A∧¬A))→¬B,
-
4.
B→¬(A∧¬A),
-
5.
¬B,
so B→A∧¬A⊢i¬B. Applying the deduction theorem gives us ⊢i(B→A∧¬A)→¬B. ∎
10. ¬¬(A∨¬A)
Proof.
From the deduction
-
1.
A→(A∨¬A),
-
2.
(A→(A∨¬A))→(¬(A∨¬A)→¬A),
-
3.
¬(A∨¬A)→¬A,
-
4.
¬A→(A∨¬A),
-
5.
(¬A→(A∨¬A))→(¬(A∨¬A)→¬¬A),
-
6.
¬(A∨¬A)→¬¬A,
-
7.
(¬(A∨¬A)→¬A)→((¬(A∨¬A)→¬¬A)→¬¬(A∨¬A)),
-
8.
(¬(A∨¬A)→¬¬A)→¬¬(A∨¬A),
-
9.
¬¬(A∨¬A),
∎
Remark. Again from this entry (http://planetmath.org/AxiomSystemForIntuitionisticLogic), if we use the second axiom system instead, keeping in mind that ¬A means A→⟂, the following are theorem schemas:
1. . The proof of this is essentially the same as the proof of the third theorem schema above.
2. . This is just , an instance of the theorem schema above.
3. .
Proof.
From the deduction
-
1.
(which is ),
-
2.
,
-
3.
,
-
4.
,
-
5.
so . By two applications of the deduction theorem, we get . ∎
Title | some theorem schemas of intuitionistic propositional logic |
---|---|
Canonical name | SomeTheoremSchemasOfIntuitionisticPropositionalLogic |
Date of creation | 2013-03-22 19:31:21 |
Last modified on | 2013-03-22 19:31:21 |
Owner | CWoo (3771) |
Last modified by | CWoo (3771) |
Numerical id | 22 |
Author | CWoo (3771) |
Entry type | Definition |
Classification | msc 03B20 |
Classification | msc 03F55 |
Related topic | AxiomSystemForIntuitionisticLogic |