$(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, YiFan Feb 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.

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

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

  • $\begingroup$ Thank you :) :) $\endgroup$ – Nick Kakl Feb 11 at 18:11

Not the answer you're looking for? Browse other questions tagged or ask your own question.