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.
$\endgroup$ 55 Answers
$\begingroup$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)$
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.
$\endgroup$ $\begingroup$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.
$\endgroup$ $\begingroup$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).
$\endgroup$ $\begingroup$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
$\endgroup$
