Prove that $\vdash p \lor \lnot p$ is true using natural deduction I'm trying to prove that $p \lor \lnot p$ is true using natural deduction. I want to do this without using any premises.
As it's done in a second using a truth table and because it is so intuitive, I would think that this proof shouldn't be too difficult, but I not able to construct one. 
 A: I would like not to use de morgan law, as you would need to include that as a premise. I was thinking of this proof.


*

*
*

*$\lnot (p \lor \lnot p) \quad \quad \quad (H)$


*
*

*
*

*$p \quad \quad \quad \quad \quad (H)$



*
*

*
*

*$p \lor \lnot p \quad \quad \; \;(\lor \text{I} 2)$



*
*

*
*

*$ \bot \quad \quad \quad \quad \;\;(\lnot \text{E}1,3)$



*
*

*$\lnot p \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\; \; (\lnot \text{I}2 - 4)$  


*
*

*$p \lor \lnot p \;\;\;\;\;\;\;\;\; \;\;\;\;\;\,(\lor \text{I}5)$


*
*

*$\bot \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\,(\lnot \text{E}1,6)$


*$p \lor \lnot p \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\,\;\;\;(\bot \text{E}1-7)$

A: The "standard" Natural Deduction proof of it is :
1) $\lnot (p \lor \lnot p)$ --- assumed [a]
2) $p$ --- assumed [b]
3) $p \lor \lnot p$ --- 2) : $\lor$I
4) $\bot$ --- 1), 3) : $\rightarrow$E
5) $\lnot p$ --- 2), 4) : $\rightarrow$I, discharging [b]
6) $p \lor \lnot p$ --- 5) : $\lor$I
7) $\bot$ --- 1), 6) : $\rightarrow$E

8) $p \lor \lnot p$ --- 1), RAA, discharging [a]


As expected, we need the classical rule for indirect proof (RAA, which is equivalent to Double Negation) to prove it, because Excluded Middle : $p \lor \lnot p$ is not intuitionistically valid.
A: It's a proof by contradiction. Some of these answers are wrong because they (wrongly) miss the double negation that one would get by negating the original premise, that is, ¬(p∨¬p). Others are more complicated than they need to be. The strategy one employs is to exploit the fact that given an assumption one is always valid in introducing a disjunction, because we know from our assumption that at least one disjunct is true. So assume the negation of P ∨ ¬P, show that a contradiction arises for either P or ¬P, thus contradicting the original premise.
The proof is:


*

*¬(P ∨ ¬P) --- (Hyp)

*P ------------- (Hyp)

*P ∨ ¬P ------- (2, ∨ introduction)

*⊥ ------------- (1, 3, contradiction)

*¬P------------ (2, 4, negation introduction) (Perhaps 1 is true, but 2 is false.)

*P ∨ ¬P ------- (5, ∨ introduction)

*⊥ ------------- (1, 6, contradiction) (Since we only assume 1 at this point, we now must reject it)

*¬¬(P ∨ ¬P)-- (1, negation introduction)

*P ∨ ¬P ------- (8, negation elimination)


QED. 
A: First assume any thesis $\alpha$ as an assumption.  Then show that the thesis can have the same scope as ApNp.  Then infer C$\alpha$ApNp.  Then prove $\alpha$ and use conditional-out.  I use Polish notation, and I can give you formation rules if you like:


*

*
*

*Cpp assumption


*
*

*
*

*NApNp assumption



*
*

*
*

*
*

*p assumption




*
*

*
*

*
*

*ApNp 3 A-in




*
*

*
*

*
*

*⊥ 3, 4. K-in




*
*

*
*

*Np 3-5 N-in



*
*

*
*

*ApNp 6 A-in



*
*

*
*

*⊥ 2, 7 K-in



*
*

*ApNp 2-8 N-out


*CCppApNp 1-9 C-in

*
*

*p assumption


*Cpp 11-11 C-in

*ApNp 10, 12 C-out 


Note that we did not prove |-ApNp at any point (though we did prove Cpp|-ApNp).
A: If you have the definition Cpq := ANpq and you have that A-commutes, and Cpp, then you can do this really quickly.  Since we have Cpp, by the definition we have ANpp.  By A-commutation we then have ApNp.
More formally, I'll first point out that natural deduction allows for definitions as well as uniform substitution on theses.  So, again, here's our definition
Cpq := ANpq.  (or C := AN for short)
First one of the lemmas:


*

*
*

*p hypothesis


*Cpp 1-1 C-in
Now for another of the lemmas:


*

*
*

*Apq hypothesis


*
*

*
*

*p hypothesis



*
*

*
*

*Aqp 2 A-in



*
*

*CpAqp 2-3 C-in


*
*

*
*

*q hypothesis



*
*

*
*

*Aqp 5 A-in



*
*

*CqAqp 5-6 A-in


*
*

*Aqp 1, 4, 7 A-out


*CApqAqp


Now we have the following sequence of theses:
1 Cpp  by the above
2 CApqAqp by the above
3 ANpp  definition applied to thesis 1
4 CANppApNp  2 p/Np, q/p (meaning in thesis 2 we substitue p with Np and q with p)
5 ApNp  3, 4 C-out
