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.
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)$
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).