A natural deduction proofs using only 11 inference rules and no axioms

Question

In this Wikipedia page https://en.wikipedia.org/wiki/Propositional_calculus, specifically in the section "Example 2. Natural deduction system", it mentions 11 inference rules and no axioms for a natural deduction system. I wanted to know how we can prove the following formulas using only the 11 rules mentioned in that page:

1. ¬A∨A
2. ¬(¬A∧A)
3. (A→¬A)→¬A
4. A→(B→C) → (A∧B)→C

And most importantly, please show all of that using a sequence of numbered lines, instead of any tree-proofs or diagrams.

Answer 1

The first three all have a similar technique to use, so I’ll just prove $A \lor \neg A$. The last one should be fairly easy.

1. $\neg (A \lor \neg A)\hspace{20ex}$ [H]

2. $A\hspace{27ex}$ [H]

3. $A \land \neg (A \lor \neg A)\hspace{13.5ex}$ [1,2 $\land$ I]

4. $\neg (A \lor \neg A)\hspace{18ex}$ [3 $\land$ E]

5. $A \to \neg (A \lor \neg A)\hspace{14.5ex}$ [2-4 $\to$ I]

6. $A\hspace{27ex}$ [H]

7. $A \lor \neg A\hspace{21ex}$ [6 $\lor$ I]

8. $A \to (A \lor \neg A)\hspace{16ex}$ [6-7 $\to$ I]

9. $\neg A\hspace{28ex}$ [5,8 $\neg$ I]

10. $A \lor \neg A\hspace{23ex}$ [9 $\lor$ I]

11. $\neg (A \lor \neg A) \to (A \lor \neg A)\hspace{6.5ex}$ [1-10 $\to$ I]

12. $\neg (A \lor \neg A)\hspace{18ex}$ [H]

13. $\neg (A \lor \neg A) \to \neg (A \lor \neg A)\hspace{5ex}$ [12-12 $\to$ I]

14. $\neg \neg (A \lor \neg A)\hspace{20ex}$ [11,13 $\neg$ I]

15. $(A \lor \neg A)\hspace{23ex}$ [14 DNE]

Note that this system requires you to use rules for other operators to prove things for negation, reiteration, etc. The general strategy is the same as for a simpler ND system, but you just have to translate those rules to these ones.