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\lor B\to B\lor A$

Proof.

From the deduction

1.

$A\to B\lor A$ ,
2.

$B\to B\lor A$ ,
3.

$(A\to B\lor A)\to((B\to B\lor A)\to(A\lor B\to B\lor A))$ ,
4.

$(B\to B\lor A)\to(A\lor B\to B\lor A)$ ,
5.

$A\lor B\to B\lor A$ ,

so we get $A\lor B\vdash_{i}B\lor A$ , and therefore $\vdash_{i}A\lor B\to B\lor A$ by the deduction theorem. ∎

2. $(A\land B)\land C\to A\land(B\land C)$

Proof.

From the deduction

1.

$(A\land B)\land C\to A\to B$ ,
2.

$(A\land B)\land C\to C$ ,
3.

$(A\land B)\land C$ ,
4.

$A\land B$ ,
5.

$C$ ,
6.

$A\land B\to A$ ,
7.

$A\land B\to B$ ,
8.

$A$ ,
9.

$B$ ,
10.

$B\to(C\to B\land C)$ ,
11.

$C\to B\land C$ ,
12.

$B\land C$ ,
13.

$A\to(B\land C\to A\land(B\land C))$ ,
14.

$B\land C\to A\land(B\land C)$ ,
15.

$A\land(B\land C)$ ,

so $(A\land B)\land C\vdash_{i}A\land(B\land C)$ , and therefore $\vdash_{i}(A\land B)\land C\to A\land(B\land C)$ by the deduction theorem. ∎

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

Proof.

From the deduction

1.

$(A\to B)\to((A\to(B\to C))\to(A\to C))$ ,
2.

$A\to B$ ,
3.

$(A\to(B\to C))\to(A\to C)$ ,
4.

$A\to(B\to C)$ ,
5.

$A\to C$ ,

so $A\to(B\to C),A\to B\vdash_{i}A\to C$ . By two applications of the deduction theorem, $\vdash_{i}(A\to(B\to C))\to((A\to B)\to(A\to C))$ . ∎

4. $A\land\neg A\to B$

Proof.

From the deduction

1.

$A\land\neg A\to A$ ,
2.

$A\land\neg A\to\neg A$ ,
3.

$A\land\neg A$ ,
4.

$\neg A$ ,
5.

$A$ ,
6.

$\neg A\to(A\to B)$ ,
7.

$A\to B$ ,
8.

$B$

so $A\land\neg A\vdash_{i}B$ . By the deduction theorem, $\vdash_{i}A\land\neg A\to B$ . ∎

5. $A\to\neg\neg A$

Proof.

From the deduction

1.

$A\to(\neg A\to A)$ ,
2.

$A$ ,
3.

$\neg A\to A$ ,
4.

$(\neg A\to A)\to((\neg A\to\neg A)\to\neg\neg A)$ ,
5.

$(\neg A\to\neg A)\to\neg\neg A$ ,
6.

$\neg A\to\neg A$ ,
7.

$\neg\neg A$ ,

so $A\vdash_{i}\neg\neg A$ . By the deduction theorem, $\vdash_{i}A\to\neg A\neg A$ . ∎

In the proof above, we use the schema $B\to B$ in step 6 of the deduction, because $\vdash_{i}B\to B$ , as a result of applying the deduction theorem to $B\vdash_{i}B$ .

6. $\neg\neg\neg A\to\neg A$

Proof.

From the deduction

1.

$(A\to\neg\neg A)\to((A\to\neg\neg\neg A)\to\neg A)$ ,
2.

$A\to\neg\neg A$ ,
3.

$(A\to\neg\neg\neg A)\to\neg A$ ,
4.

$\neg\neg\neg A\to(A\to\neg\neg\neg A)$ ,
5.

$\neg\neg\neg A$ ,
6.

$A\to\neg\neg\neg A$ ,
7.

$\neg A$ ,

so $A\to\neg\neg A,\neg\neg\neg A\vdash_{i}\neg A$ . By the deduction theorem, $A\to\neg\neg A,\vdash_{i}\neg\neg\neg A\to\neg A$ . Since $\vdash_{i}A\to\neg A\neg A$ , $\vdash_{i}\neg\neg\neg A\to\neg A$ as a result. ∎

In the above proof, we use the fact that if $\vdash_{i}C$ and $C\vdash_{i}D$ , then $\vdash_{i}D$ . This is the result of the following fact: if $\vdash_{i}C$ and $\vdash_{i}C\to D$ , then $\vdash_{i}D$ .

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

Proof.

From the deduction

1.

$(A\to B)\to((A\to\neg B)\to\neg A)$ ,
2.

$A\to B$ ,
3.

$(A\to\neg B)\to\neg A$ ,
4.

$\neg B\to(A\to\neg B)$ ,
5.

$\neg B$ ,
6.

$A\to\neg B$ ,
7.

$\neg A$ ,

so $A\to B,\neg B\vdash_{i}\neg A$ . Applying the deduction theorem twice gives us $\vdash_{i}(A\to B)\to(\neg B\to\neg A)$ . ∎

8. $\neg(A\land\neg A)$

Proof.

From the deduction

1.

$(A\land\neg A\to B)\to((A\land\neg A\to\neg B)\to\neg(A\land\neg A))$ ,
2.

$A\land\neg A\to B$ ,
3.

$(A\land\neg A\to\neg B)\to\neg(A\land\neg A)$ ,
4.

$A\land\neg A\to\neg B$ ,
5.

$\neg(A\land\neg A)$ .

Since $\vdash_{i}A\land\neg A\to B$ and $\vdash_{i}A\land\neg A\to\neg B$ are instances of theorem schema 4 above, $\vdash_{i}\neg(A\land\neg A)$ as a result. ∎

This also shows that $\vdash_{i}B\to\neg(A\land\neg A)$ , which is the result of applying modus ponens to $\neg(A\land\neg A)$ to $\neg(A\land\neg A)\to(B\to\neg(A\land\neg A))$ .

9. $(B\to A\land\neg A)\to\neg B$

Proof.

From the deduction

1.

$B\to A\land\neg A$ ,
2.

$(B\to A\land\neg A)\to((B\to\neg(A\land\neg A))\to\neg B)$ ,
3.

$(B\to\neg(A\land\neg A))\to\neg B$ ,
4.

$B\to\neg(A\land\neg A)$ ,
5.

$\neg B$ ,

so $B\to A\land\neg A\vdash_{i}\neg B$ . Applying the deduction theorem gives us $\vdash_{i}(B\to A\land\neg A)\to\neg B$ . ∎

10. $\neg\neg(A\lor\neg A)$

Proof.

From the deduction

1.

$A\to(A\lor\neg A)$ ,
2.

$(A\to(A\lor\neg A))\to(\neg(A\lor\neg A)\to\neg A)$ ,
3.

$\neg(A\lor\neg A)\to\neg A$ ,
4.

$\neg A\to(A\lor\neg A)$ ,
5.

$(\neg A\to(A\lor\neg A))\to(\neg(A\lor\neg A)\to\neg\neg A)$ ,
6.

$\neg(A\lor\neg A)\to\neg\neg A$ ,
7.

$(\neg(A\lor\neg A)\to\neg A)\to((\neg(A\lor\neg A)\to\neg\neg A)\to\neg\neg(A% \lor\neg A))$ ,
8.

$(\neg(A\lor\neg A)\to\neg\neg A)\to\neg\neg(A\lor\neg A)$ ,
9.

$\neg\neg(A\lor\neg A)$ ,

∎

Remark. Again from this entry (http://planetmath.org/AxiomSystemForIntuitionisticLogic), if we use the second axiom system instead, keeping in mind that $\neg A$ means $A\to\perp$ , the following are theorem schemas:

1. $(A\to B)\to((A\to(B\to C))\to(A\to C))$ . The proof of this is essentially the same as the proof of the third theorem schema above.

2. $(A\to B)\to((A\to\neg B)\to\neg A)$ . This is just $(A\to B)\to((A\to(B\to\perp))\to(A\to\perp))$ , an instance of the theorem schema above.

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

Proof.

From the deduction

1.

$\neg A$ (which is $A\to\perp$ ),
2.

$A$ ,
3.

$\perp$ ,
4.

$\perp\to B$ ,
5.

$B$

so $\neg A,A\vdash_{i}B$ . By two applications of the deduction theorem, we get $\vdash_{i}\neg A\to(A\to B)$ . ∎

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