I am trying to prove that $\neg A \to \bot \vdash A$, I can only use double negation elimination to get the conclusion, but I don't know how to prove double negation elimination.

Below is my proof for $\neg A \to \bot \vdash A$:

1 $\neg A\to\bot$

2 $\neg A$ (assumption)

3 $\bot$ ($\to$e 1, 2)

4 $\neg\neg A$ ($\neg$i 2-3)

5 $A$ (DNE 4)

The rules that can be used would be the basic rules of natural deduction: enter image description here

  • 2
    $\begingroup$ What do you mean precisely when you say that you want to prove double negation elimination? What rules are you allowed to use? $\endgroup$ Jan 4, 2022 at 17:49
  • $\begingroup$ $\wedge$e, i. $\vee$e, i. $\to$e, i. $\neg$e, i. $\bot$e, i. $\endgroup$
    – KOMAX233
    Jan 4, 2022 at 18:35
  • 2
    $\begingroup$ What precisely are your rules $\lnot E$, $\lnot I$, $\bot E$, and $\bot I$? Not everyone uses the same names for the same rules. Please edit these into your question. $\endgroup$ Jan 4, 2022 at 22:06

1 Answer 1


The rules you list comprise a natural deduction system for intuitionistic logic. The sequent $\lnot A\to \bot\vdash A$ is not valid in intuitionistic logic, so it is not provable in your system.

To prove $\lnot A\to \bot\vdash A$, you need to be working with a natural deduction system for classical logic, which means adding an additional rule to your system. One common choice is to add double negation elimination itself; this makes your proof a valid one. Other common choices are adding reductio ad absurdum (proof by contradiction) or the law of excluded middle.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .