= Solution
Use <proof by contradiction>, expanding the final classical step explicitly into <negation introduction> followed by <double-negation elimination>. First the assumption $\neg(\neg P\lor\neg Q)$ forces $P$: otherwise $\neg P$ immediately gives the prohibited <logical disjunction>. It similarly forces $Q$. The formal <natural deduction> derivation is
$$
\begin{array}{rll}
1&\neg(P\land Q)&\text{premise}\\
2&\vert\ \neg(\neg P\lor\neg Q)&\text{assumption}\\
3&\vert\ \vert\ \neg P&\text{assumption}\\
4&\vert\ \vert\ \neg P\lor\neg Q&\lor\text{-intro-L }3\\
5&\vert\ \vert\ \bot&\neg\text{-elim }4,2\\
6&\vert\ \neg\neg P&\neg\text{-intro }3\text{--}5\\
7&\vert\ P&\neg\neg\text{-elim }6\\
8&\vert\ \vert\ \neg Q&\text{assumption}\\
9&\vert\ \vert\ \neg P\lor\neg Q&\lor\text{-intro-R }8\\
10&\vert\ \vert\ \bot&\neg\text{-elim }9,2\\
11&\vert\ \neg\neg Q&\neg\text{-intro }8\text{--}10\\
12&\vert\ Q&\neg\neg\text{-elim }11\\
13&\vert\ P\land Q&\land\text{-intro }7,12\\
14&\vert\ \bot&\neg\text{-elim }13,1\\
15&\neg\neg(\neg P\lor\neg Q)&\neg\text{-intro }2\text{--}14\\
16&\neg P\lor\neg Q&\neg\neg\text{-elim }15
\end{array}
$$
Hence
$$
\boxed{\neg(P\land Q)\ \vdash\ \neg P\lor\neg Q.}
$$
This direction of <De Morgan's laws> uses the classical rule supplied on the source rule sheet; it has not been silently treated as an available <inference rule>.
Back to article page
