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. 

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
