# Is this proof for $\vdash p\vee\neg p$ correct and what other proof would you suggest?

1. $\;\bullet\;\neg(p\vee\neg p)$ --- assumption
2. $\;\bullet\;\neg p\wedge\neg\neg p$ --- DM 1 (De Morgan Law)
3. $\;\bullet\;\neg p$ --- $\wedge$ elim 2
4. $\;\bullet\;\neg\neg p$ --- $\wedge$ elim 2
5. $\;\bullet\;\bot$ --- $\bot$ intro 3,4
6. $\;p\vee\neg p$ --- RAA 1 - 5
• which rule is given, RAA or DNE? – Kenny Lau Sep 21 '17 at 16:29
• I've included proofs here – Kenny Lau Sep 21 '17 at 16:31
• actually I'm learning it from internet and not a specific book, can't quite understand what you mean but RAA is a derived rule and standing for Reductio Ad Absurdum and has a separate proof – Pooria Sep 21 '17 at 16:31
• Indeed, Pooria! – amWhy Sep 21 '17 at 16:41
• See also the post prove that $\vdash p \lor \lnot p$ is true using natural deduction – Mauro ALLEGRANZA Sep 22 '17 at 6:17

Your proof is alright apart from the fact that you used DM1, which although is true in intuitionistic logic, is usually not a given (it is also not given in the natural deduction system you linked).

This is because DM2 is invalid in intuitionistic logic.

So, here's a proof using RAA but not DM1:

  01. ¬[p∨¬p]   assumption
02. p       assumption
03. p∨¬p    ∨intro 02
05. ¬p        ¬intro 02-04
06. p∨¬p      ∨intro 05