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

Proof.

From the deduction

1. $A\to B\vee A$,

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

3. $(A\to B\vee A)\to ((B\to B\vee A)\to (A\vee B\to B\vee A))$,

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

5. $A\vee B\to B\vee A$,

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

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

Proof.

From the deduction

1. $(A\wedge B)\wedge C\to A\to B$,

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

3. $(A\wedge B)\wedge C$,

4. $A\wedge B$,

5. $C$,

6. $A\wedge B\to A$,

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

8. $A$,

9. $B$,

10. $B\to (C\to B\wedge C)$,

11. $C\to B\wedge C$,

12. $B\wedge C$,

13. $A\to (B\wedge C\to A\wedge (B\wedge C))$,

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

15. $A\wedge (B\wedge C)$,

so $(A\wedge B)\wedge C{⊢}_{i}A\wedge (B\wedge C)$, and therefore ${⊢}_i(A\wedge B)\wedge C\to A\wedge (B\wedge 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{⊢}_{i}A\to C$. By two applications of the deduction theorem, ${⊢}_i(A\to (B\to C))\to ((A\to B)\to (A\to C))$.∎

4. $A\wedge \mathrm{\neg }A\to B$

Proof.

From the deduction

1. $A\wedge \mathrm{\neg }A\to A$,

2. $A\wedge \mathrm{\neg }A\to \mathrm{\neg }A$,

3. $A\wedge \mathrm{\neg }A$,

4. $\mathrm{\neg }A$,

5. $A$,

6. $\mathrm{\neg }A\to (A\to B)$,

7. $A\to B$,

8. $B$

so $A\wedge \mathrm{\neg }A{⊢}_{i}B$. By the deduction theorem, ${⊢}_{i}A\wedge \mathrm{\neg }A\to B$.∎

5. $A\to \mathrm{\neg }\mathrm{\neg }A$

Proof.

From the deduction

1. $A\to (\mathrm{\neg }A\to A)$,

2. $A$,

3. $\mathrm{\neg }A\to A$,

4. $(\mathrm{\neg }A\to A)\to ((\mathrm{\neg }A\to \mathrm{\neg }A)\to \mathrm{\neg }\mathrm{\neg }A)$,

5. $(\mathrm{\neg }A\to \mathrm{\neg }A)\to \mathrm{\neg }\mathrm{\neg }A$,

6. $\mathrm{\neg }A\to \mathrm{\neg }A$,

7. $\mathrm{\neg }\mathrm{\neg }A$,

so $A{⊢}_i\mathrm{\neg }\mathrm{\neg }A$. By the deduction theorem, ${⊢}_{i}A\to \mathrm{\neg }A\mathrm{\neg }A$.∎

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

6. $\mathrm{\neg }\mathrm{\neg }\mathrm{\neg }A\to \mathrm{\neg }A$

Proof.

From the deduction

1. $(A\to \mathrm{\neg }\mathrm{\neg }A)\to ((A\to \mathrm{\neg }\mathrm{\neg }\mathrm{\neg }A)\to \mathrm{\neg }A)$,

2. $A\to \mathrm{\neg }\mathrm{\neg }A$,

3. $(A\to \mathrm{\neg }\mathrm{\neg }\mathrm{\neg }A)\to \mathrm{\neg }A$,

4. $\mathrm{\neg }\mathrm{\neg }\mathrm{\neg }A\to (A\to \mathrm{\neg }\mathrm{\neg }\mathrm{\neg }A)$,

5. $\mathrm{\neg }\mathrm{\neg }\mathrm{\neg }A$,

6. $A\to \mathrm{\neg }\mathrm{\neg }\mathrm{\neg }A$,

7. $\mathrm{\neg }A$,

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

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

7. $(A\to B)\to (\mathrm{\neg }B\to \mathrm{\neg }A)$

Proof.

From the deduction

1. $(A\to B)\to ((A\to \mathrm{\neg }B)\to \mathrm{\neg }A)$,

2. $A\to B$,

3. $(A\to \mathrm{\neg }B)\to \mathrm{\neg }A$,

4. $\mathrm{\neg }B\to (A\to \mathrm{\neg }B)$,

5. $\mathrm{\neg }B$,

6. $A\to \mathrm{\neg }B$,

7. $\mathrm{\neg }A$,

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

8. $\mathrm{\neg }(A\wedge \mathrm{\neg }A)$

Proof.

From the deduction

1. $(A\wedge \mathrm{\neg }A\to B)\to ((A\wedge \mathrm{\neg }A\to \mathrm{\neg }B)\to \mathrm{\neg }(A\wedge \mathrm{\neg }A))$,

2. $A\wedge \mathrm{\neg }A\to B$,

3. $(A\wedge \mathrm{\neg }A\to \mathrm{\neg }B)\to \mathrm{\neg }(A\wedge \mathrm{\neg }A)$,

4. $A\wedge \mathrm{\neg }A\to \mathrm{\neg }B$,

5. $\mathrm{\neg }(A\wedge \mathrm{\neg }A)$.

Since ${⊢}_{i}A\wedge \mathrm{\neg }A\to B$ and ${⊢}_{i}A\wedge \mathrm{\neg }A\to \mathrm{\neg }B$ are instances of theorem schema 4 above, ${⊢}_i\mathrm{\neg }(A\wedge \mathrm{\neg }A)$ as a result.∎

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

9. $(B\to A\wedge \mathrm{\neg }A)\to \mathrm{\neg }B$

Proof.

From the deduction

1. $B\to A\wedge \mathrm{\neg }A$,

2. $(B\to A\wedge \mathrm{\neg }A)\to ((B\to \mathrm{\neg }(A\wedge \mathrm{\neg }A))\to \mathrm{\neg }B)$,

3. $(B\to \mathrm{\neg }(A\wedge \mathrm{\neg }A))\to \mathrm{\neg }B$,

4. $B\to \mathrm{\neg }(A\wedge \mathrm{\neg }A)$,

5. $\mathrm{\neg }B$,

so $B\to A\wedge \mathrm{\neg }A{⊢}_i\mathrm{\neg }B$. Applying the deduction theorem gives us ${⊢}_i(B\to A\wedge \mathrm{\neg }A)\to \mathrm{\neg }B$.∎

10. $\mathrm{\neg }\mathrm{\neg }(A\vee \mathrm{\neg }A)$

Proof.

From the deduction

1. $A\to (A\vee \mathrm{\neg }A)$,

2. $(A\to (A\vee \mathrm{\neg }A))\to (\mathrm{\neg }(A\vee \mathrm{\neg }A)\to \mathrm{\neg }A)$,

3. $\mathrm{\neg }(A\vee \mathrm{\neg }A)\to \mathrm{\neg }A$,

4. $\mathrm{\neg }A\to (A\vee \mathrm{\neg }A)$,

5. $(\mathrm{\neg }A\to (A\vee \mathrm{\neg }A))\to (\mathrm{\neg }(A\vee \mathrm{\neg }A)\to \mathrm{\neg }\mathrm{\neg }A)$,

6. $\mathrm{\neg }(A\vee \mathrm{\neg }A)\to \mathrm{\neg }\mathrm{\neg }A$,

7. $(\mathrm{\neg }(A\vee \mathrm{\neg }A)\to \mathrm{\neg }A)\to ((\mathrm{\neg }(A\vee \mathrm{\neg }A)\to \mathrm{\neg }\mathrm{\neg }A)\to \mathrm{\neg }\mathrm{\neg }(A\vee \mathrm{\neg }A))$,

8. $(\mathrm{\neg }(A\vee \mathrm{\neg }A)\to \mathrm{\neg }\mathrm{\neg }A)\to \mathrm{\neg }\mathrm{\neg }(A\vee \mathrm{\neg }A)$,

9. $\mathrm{\neg }\mathrm{\neg }(A\vee \mathrm{\neg }A)$,

∎

Remark. Again from this entry (http://planetmath.org/AxiomSystemForIntuitionisticLogic), if we use the second axiom system instead, keeping in mind that $\mathrm{\neg }A$ means $A\to ⟂$, 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 \mathrm{\neg }B)\to \mathrm{\neg }A)$. This is just $(A\to B)\to ((A\to (B\to ⟂))\to (A\to ⟂))$, an instance of the theorem schema above.

3. $\mathrm{\neg }A\to (A\to B)$.

Proof.

From the deduction

1. $\mathrm{\neg }A$ (which is $A\to ⟂$),

2. $A$,

3. $⟂$,

4. $⟂\to B$,

5. $B$

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