# 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. 1.

$A\to B\lor A$,

2. 2.

$B\to B\lor A$,

3. 3.

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

4. 4.

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

5. 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. 1.

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

2. 2.

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

3. 3.

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

4. 4.

$A\land B$,

5. 5.

$C$,

6. 6.

$A\land B\to A$,

7. 7.

$A\land B\to B$,

8. 8.

$A$,

9. 9.

$B$,

10. 10.

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

11. 11.

$C\to B\land C$,

12. 12.

$B\land C$,

13. 13.

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

14. 14.

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

15. 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. 1.

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

2. 2.

$A\to B$,

3. 3.

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

4. 4.

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

5. 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. 1.

$A\land\neg A\to A$,

2. 2.

$A\land\neg A\to\neg A$,

3. 3.

$A\land\neg A$,

4. 4.

$\neg A$,

5. 5.

$A$,

6. 6.

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

7. 7.

$A\to B$,

8. 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. 1.

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

2. 2.

$A$,

3. 3.

$\neg A\to A$,

4. 4.

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

5. 5.

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

6. 6.

$\neg A\to\neg A$,

7. 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. 1.

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

2. 2.

$A\to\neg\neg A$,

3. 3.

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

4. 4.

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

5. 5.

$\neg\neg\neg A$,

6. 6.

$A\to\neg\neg\neg A$,

7. 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. 1.

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

2. 2.

$A\to B$,

3. 3.

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

4. 4.

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

5. 5.

$\neg B$,

6. 6.

$A\to\neg B$,

7. 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. 1.

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

2. 2.

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

3. 3.

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

4. 4.

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

5. 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. 1.

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

2. 2.

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

3. 3.

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

4. 4.

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

5. 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. 1.

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

2. 2.

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

3. 3.

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

4. 4.

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

5. 5.

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

6. 6.

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

7. 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. 8.

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

9. 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. 1.

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

2. 2.

$A$,

3. 3.

$\perp$,

4. 4.

$\perp\to B$,

5. 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 SomeTheoremSchemasOfIntuitionisticPropositionalLogic 2013-03-22 19:31:21 2013-03-22 19:31:21 CWoo (3771) CWoo (3771) 22 CWoo (3771) Definition msc 03B20 msc 03F55 AxiomSystemForIntuitionisticLogic