Proof with natural deduction

Question

$(p\rightarrow \bot)\rightarrow \bot \vdash p$

I need to prove this using natural deduction.

I tried assuming that $\neg p$ is true, so I can prove $p$ by contradiction. I do not have $\neg p$ defined as $p\rightarrow \bot$.

Answer 1

Using the set of rules of Michael Huth & Mark Ryan, Logic in Computer Science : Modelling and Reasoning about Systems (Cambridge UP, 2004), page 27.

1) $(p→⊥)→⊥$ --- premise

$\quad$2) $\lnot p$ --- assumed [a]

$\qquad$3) $p$ --- assumed [b]

$\qquad$4) $\bot$ --- from 2) and 3) by $\lnot$-elim

$\quad$5) $p \to \bot$ --- from 3) and 4) by $\to$-intro, discharging [b]

$\quad$6) $\bot$ --- from 1) and 5) by $\to$-elim

7) $p$ --- from 2) and 6) by $\lnot \lnot$-elim, discharging [a].