# 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 assume that $p$ is any wff, am I correct? – NasuSama Jul 9 '13 at 0:35
• Is it OK to make a premise and then discharge it? If not, I don't think it can be done. – Fred Rickey Jul 9 '13 at 0:40
• There does exist something of a way to do this, in a certain sense. – Doug Spoonwood Jul 9 '13 at 12:33
• Truth tables and proofs don't necessarily correspond all that well. The truth table for EEEpqrEpEqr only takes up 8 rows, but proving that in a natural deduction system, from what I know of them takes a lot more work. – Doug Spoonwood Jul 10 '13 at 3:53
• You are going to need something in your natural deduction system that implies classical rather than intuitionistic logic. (See en.wikipedia.org/wiki/Intuitionistic_logic.) E.g., double negation elimination: $\lnot \lnot p \implies p$ or the law of excluded middle: $p \lor \lnot p$ (i.e., the statement you want to prove). – Rob Arthan Nov 22 '13 at 1:15

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)$
1. $p \lor \lnot p \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\,\;\;\;(\bot \text{E}1-7)$
• Yes, I see now. I also wasn't aware of what "natural deduction" meant. I have deleted my answer to reflect this. – Ryan Sullivant Jul 10 '13 at 7:16
• This is not correct. Line 8 should read $\lnot\lnot(p \lor \lnot p)$. – Rob Arthan Nov 22 '13 at 0:59
• The question is to prove the law of excluded middle. But you used the law of excluded middle in step 5 and 8. Why is this acceptable? – Mygod Apr 18 '17 at 16:34

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.

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:

1. ¬(P ∨ ¬P) --- (Hyp)
2. P ------------- (Hyp)
3. P ∨ ¬P ------- (2, ∨ introduction)
4. ⊥ ------------- (1, 3, contradiction)
5. ¬P------------ (2, 4, negation introduction) (Perhaps 1 is true, but 2 is false.)
6. P ∨ ¬P ------- (5, ∨ introduction)
7. ⊥ ------------- (1, 6, contradiction) (Since we only assume 1 at this point, we now must reject it)
8. ¬¬(P ∨ ¬P)-- (1, negation introduction)
9. P ∨ ¬P ------- (8, negation elimination)

QED.

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
1. CCppApNp 1-9 C-in
• p assumption
2. Cpp 11-11 C-in
3. ApNp 10, 12 C-out

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

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
1. 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
1. 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