I ask this because here there's a proof for double negation elimination, problem is it uses law of excluded middle, and proofs for law of excluded middle use DNE/RAA themselves as I've seen which doesn't make sense!

  • 3
    $\begingroup$ LEM, DNE and RAA are equivalent: you can prove them from each other using intuitionistic logic. However, if you eliminate them all and use only intuitionistic logic, then you can't get LEM. $\endgroup$ – Kenny Lau Sep 21 '17 at 18:55
  • $\begingroup$ And you still have to specify the system you are using. $\endgroup$ – Kenny Lau Sep 21 '17 at 18:55
  • $\begingroup$ hmmm... interesting, and fun fact is I dunno the specific system I'm using as I said I've started to learn natural deduction from the internet :D $\endgroup$ – Pooria Sep 21 '17 at 19:00
  • $\begingroup$ At least you can know if you're using intuitionstic logic or classical logic. $\endgroup$ – Kenny Lau Sep 21 '17 at 19:02
  • 2
    $\begingroup$ As always, it all depends on what specific rules you are using. Some systems define $\neg$ Elim as going from $\neg \neg \phi$ to $\phi$ $\endgroup$ – Bram28 Sep 22 '17 at 1:18

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.