4
$\begingroup$

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

$\endgroup$
3
  • 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$
    – Taroccoesbrocco
    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$
    – Alex Kruckman
    Jan 4, 2022 at 22:06

1 Answer 1

Reset to default
8
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

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