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.

  • $\begingroup$ I would assume that $p$ is any wff, am I correct? $\endgroup$
    – NasuSama
    Jul 9, 2013 at 0:35
  • 1
    $\begingroup$ Is it OK to make a premise and then discharge it? If not, I don't think it can be done. $\endgroup$ Jul 9, 2013 at 0:40
  • $\begingroup$ There does exist something of a way to do this, in a certain sense. $\endgroup$ Jul 9, 2013 at 12:33
  • $\begingroup$ 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. $\endgroup$ Jul 10, 2013 at 3:53
  • $\begingroup$ 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). $\endgroup$
    – Rob Arthan
    Nov 22, 2013 at 1:15

5 Answers 5


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)$
  • $\begingroup$ Yes, I see now. I also wasn't aware of what "natural deduction" meant. I have deleted my answer to reflect this. $\endgroup$ Jul 10, 2013 at 7:16
  • 2
    $\begingroup$ This is not correct. Line 8 should read $\lnot\lnot(p \lor \lnot p)$. $\endgroup$
    – Rob Arthan
    Nov 22, 2013 at 0:59
  • $\begingroup$ 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? $\endgroup$
    – Mygod
    Apr 18, 2017 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)



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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.