= Solution
Temporarily deny the desired <logical disjunction>. If $\neg P$ held, it would introduce that very <logical disjunction>, producing <logical falsity>; <double-negation elimination> therefore gives $P$. The same argument gives $Q$, contradicting the premise. The complete <natural deduction> derivation is:
\Table[
|| Line
|| Open assumptions
|| Formula
|| Justification
| 1
| 1
| $\neg (P\land Q)$
| Premise
| 2
| 1, 2
| $\neg (\neg P\lor\neg Q)$
| <Temporary assumption>
| 3
| 1, 2, 3
| $\neg P$
| <Temporary assumption>
| 4
| 1, 2, 3
| $\neg P\lor\neg Q$
| <disjunction introduction> L 3
| 5
| 1, 2, 3
| $\bot$
| <negation elimination rule> 4, 2
| 6
| 1, 2
| $\neg \neg P$
| <negation introduction> 3, 5
| 7
| 1, 2
| $P$
| <double-negation elimination> 6
| 8
| 1, 2, 8
| $\neg Q$
| <Temporary assumption>
| 9
| 1, 2, 8
| $\neg P\lor\neg Q$
| <disjunction introduction> R 8
| 10
| 1, 2, 8
| $\bot$
| <negation elimination rule> 9, 2
| 11
| 1, 2
| $\neg \neg Q$
| <negation introduction> 8, 10
| 12
| 1, 2
| $Q$
| <double-negation elimination> 11
| 13
| 1, 2
| $P\land Q$
| <conjunction introduction> 7, 12
| 14
| 1, 2
| $\bot$
| <negation elimination rule> 13, 1
| 15
| 1
| $\neg \neg (\neg P\lor\neg Q)$
| <negation introduction> 2, 14
| 16
| 1
| $\neg P\lor\neg Q$
| <double-negation elimination> 15
]
{title=Classical derivation of the disjunction of negations}
Consequently
$$
\boxed{\neg P\lor\neg Q.}
$$
The uses of <double-negation elimination> are justified by the supplied rules. This distinguishes the proof from the preceding constructive direction of <De Morgan's laws>.
Back to article page
