# Is there a proof for $\neg\neg p\vdash p$ that doesn't use law of excluded middle?

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!

• 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. – Kenny Lau Sep 21 '17 at 18:55
• And you still have to specify the system you are using. – Kenny Lau Sep 21 '17 at 18:55
• 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 – Pooria Sep 21 '17 at 19:00
• At least you can know if you're using intuitionstic logic or classical logic. – Kenny Lau Sep 21 '17 at 19:02
• 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$ – Bram28 Sep 22 '17 at 1:18