# How to prove this using natural deduction

$$⊢ P ∨ ¬P$$

I found this question on the net. I know the solution, but I find it complicated.

How should I approach this sort of question? Or can you provide me with another solution?

• What sort of question? – Git Gud Dec 29 '14 at 21:04
• You can find here a slightly different proof. – Mauro ALLEGRANZA Dec 30 '14 at 9:18
• As far as I can tell, the accepted answer misses a step (as pointed out by a comment). It only proves $\neg \neg(p \vee \neg p)$. – Stefan Perko Dec 30 '14 at 9:43
• What proof system is the given proof derived in? If you found the image online can you provide a source? – Calculemus Jan 8 '15 at 4:39
• @Calculemus danielclemente.com/logica/dn.en-node38.html – MUSE Jan 9 '15 at 15:11

I don't know, whether you really find this helpful, but you could prove a bunch of other (generally useful) statements / rules first:

• $\neg(p \wedge q) \Rightarrow \neg p \vee \neg q$ (DM)
• $\neg(p \wedge \neg p)$ (PNC)
• $(p \vee q, p\vdash p', q \vdash q') \vdash p' \vee q'$ (CDL)

and then it should be easy:

1. $\neg(p\wedge \neg p)$ (by PNC)

2. $\neg p \vee \neg \neg p$ (by DM, 1.)

3. $\neg p \vdash \neg p$ (Assumption rule)

4. $\neg \neg p \vdash p$ (by $\neg\neg E$)

5. $p \vee \neg p$ (by CDL, 2.,3.,4.)

Here, for example, the proof for (PNC):

1. $p \wedge \neg p$ (H)
2. $\,\,\,\,$ $p$ $\,\,\,\,$ ($\wedge E1, 1.$)
3. $\,\,\,\,$ $\neg p$ $\,\,\,$ ($\wedge E2, 1.$)
4. $\,\,\,\,$ $\perp$ $\,\,\,\,$ ($\Rightarrow E$, 2., 3.)
5. $\neg(p \wedge \neg p)$ ($\Rightarrow I$, 1., 4.)
• What does PNC and CDL stand for? – MUSE Dec 29 '14 at 20:32
• Doesn't really matter, I just gave them names to refer to them. But it stands for "principle of non-contradiction" and "constructive dilemma". (I don't think, this a standard abbreviation) – Stefan Perko Dec 29 '14 at 20:40

$$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}$$ That is almost correct.   You were aiming at a proof by contradiction, and that needs to use just one subproof (also by contradiction). $$\fitch{}{\fitch{1.~\lnot(p\vee\lnot p)\hspace{10ex}\text{H (assumption or hypothesis)}}{\fitch{2.~p\hspace{15ex}\text{H (assumption)}}{3.~p\vee\lnot p\hspace{10ex}\text{I\lor 2 (disjunction introduction)}\\4.~\lnot(p\lor\lnot p)\hspace{6.5ex}\text{IT1 (reiteration)}}\\5.~\lnot p\hspace{17.5ex}\text{I\lnot2,3,4 (negation introduction)}\\6.~p\vee\lnot p\hspace{14ex}\text{I\lor 5 (disjunction introduction)}\\7.~\lnot(p\lor\lnot p)\hspace{10.5ex}\text{IT1 (reiteration)}}\\8.~\lnot\lnot(p\vee\lnot p)\hspace{12.5ex}\text{I\lnot 1,6,7 (negation introduction)}\\9.~p\vee\lnot p\hspace{17.5ex}\text{E\lnot\lnot (double negation elimination, aka DNE)}}$$

Thus the Law of Excluded Middle (LEM) is provable, iff you accept the Double Negation Elimination (DNE) rule of inference.

Note: Some rules systems combine inferences on lines 8 and 9 into one step, and call that the rule of negation elimination (or indirect proof)

$$\fitch{}{\fitch{1.~\lnot(p\vee\lnot p)\hspace{10ex}\text{H (assumption or hypothesis)}}{\fitch{2.~p\hspace{15ex}\text{H (assumption)}}{3.~p\vee\lnot p\hspace{10ex}\text{I\lor 2 (disjunction introduction)}\\4.~\lnot(p\lor\lnot p)\hspace{6.5ex}\text{IT1 (reiteration)}}\\5.~\lnot p\hspace{17.5ex}\text{I\lnot2,3,4 (negation introduction)}\\6.~p\vee\lnot p\hspace{14ex}\text{I\lor 5 (disjunction introduction)}\\7.~\lnot(p\lor\lnot p)\hspace{10.5ex}\text{IT1 (reiteration)}}\\8.~p\vee\lnot p\hspace{17.5ex}\text{E\lnot 1,6,7 (negation elimination, aka indirect proof)}}$$

Thus is the Law of Excluded Middle (LEM) provable iff you allow the Indirect Proof (IP) rule of inference... or other equivalent formulations.