# Proof with natural deduction [closed]

$$(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$$.

## closed as off-topic by Xander Henderson, mrtaurho, Gibbs, Brahadeesh, YiFanFeb 11 at 20:24

This question appears to be off-topic. The users who voted to close gave this specific reason:

• "This question is missing context or other details: Please provide additional context, which ideally explains why the question is relevant to you and our community. Some forms of context include: background and motivation, relevant definitions, source, possible strategies, your current progress, why the question is interesting or important, etc." – Xander Henderson, mrtaurho, Gibbs, Brahadeesh, YiFan
If this question can be reworded to fit the rules in the help center, please edit the question.

• What have you tried so far? Where do you get stuck? – Taroccoesbrocco Feb 11 at 17:46
• i assumed that ~p is true, so i can prove p by contradiction – Nick Kakl Feb 11 at 17:49
• What set of rules are you using ? Is $\lnot p$ defined as $p \to \bot$ ? – Mauro ALLEGRANZA Feb 11 at 18:01
• no it is not :( – Nick Kakl Feb 11 at 18:03

## 1 Answer

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

• Thank you :) :) – Nick Kakl Feb 11 at 18:11