$\perp \Rightarrow p$ Syntactic Proof

Question

Given the following axioms $$\begin{aligned}&1. p\Rightarrow (q\Rightarrow p)\\&2. [p\Rightarrow (q\Rightarrow r )] \Rightarrow [(p\Rightarrow q)\Rightarrow (p\Rightarrow r)]\\&3. \neg\neg p \Rightarrow p \end{aligned}$$ and the deduction rule of modus ponens, I want to prove that $$\perp \Rightarrow p.$$ Can somebody give me a hint how to do that?

Answer 1

Proof :

1) $\bot \rightarrow ((p \rightarrow \bot) \rightarrow \bot)$ --- from Ax.1

2) $\bot \vdash (p \rightarrow \bot) \rightarrow \bot$ --- from 1) and modus ponens

3) $((p \rightarrow \bot) \rightarrow \bot) \rightarrow p$ --- from Ax.3, with the abbreviation : $\lnot p := p \rightarrow \bot$

4) $\bot \vdash p$ --- from 2) and 3), by modus ponens

5) $\vdash \bot \rightarrow p$ --- from 4) by Deduction Theorem.

---

Note : see Alonzo Church, Introduction to Mathematical Logic (1956), page 90.