Prove that $\vdash p \lor \lnot p$ is true using natural deduction

Question

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.

Answer 1

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.

1. • $\lnot (p \lor \lnot p) \quad \quad \quad (H)$
2. • • $p \quad \quad \quad \quad \quad (H)$
3. • • $p \lor \lnot p \quad \quad \; \;(\lor \text{I} 2)$
4. • • $ \bot \quad \quad \quad \quad \;\;(\lnot \text{E}1,3)$
5. • $\lnot p \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\; \; (\lnot \text{I}2 - 4)$
6. • $p \lor \lnot p \;\;\;\;\;\;\;\;\; \;\;\;\;\;\,(\lor \text{I}5)$
7. • $\bot \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\,(\lnot \text{E}1,6)$
8. $p \lor \lnot p \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\,\;\;\;(\bot \text{E}1-7)$

Answer 2

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:

1. • Cpp assumption
2. • • NApNp assumption
3. • • • p assumption
4. • • • ApNp 3 A-in
5. • • • ⊥ 3, 4. K-in
6. • • Np 3-5 N-in
7. • • ApNp 6 A-in
8. • • ⊥ 2, 7 K-in
9. • ApNp 2-8 N-out
10. CCppApNp 1-9 C-in
11. • p assumption
12. Cpp 11-11 C-in
13. ApNp 10, 12 C-out

Note that we did not prove |-ApNp at any point (though we did prove Cpp|-ApNp).

Answer 3

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:

1. • p hypothesis

2. Cpp 1-1 C-in

Now for another of the lemmas:

1. • Apq hypothesis
2. • • p hypothesis
3. • • Aqp 2 A-in
4. • CpAqp 2-3 C-in
5. • • q hypothesis
6. • • Aqp 5 A-in
7. • CqAqp 5-6 A-in
8. • Aqp 1, 4, 7 A-out
9. 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