= Solution
Use <negation introduction> separately for each component, introducing the forbidden <logical disjunction> in each <subproof>:
$$
\begin{array}{rll}
1&\neg(P\lor Q)&\text{premise}\\
2&\vert\ P&\text{assumption}\\
3&\vert\ P\lor Q&\lor\text{-intro-L }2\\
4&\vert\ \bot&\neg\text{-elim }3,1\\
5&\neg P&\neg\text{-intro }2\text{--}4\\
6&\vert\ Q&\text{assumption}\\
7&\vert\ P\lor Q&\lor\text{-intro-R }6\\
8&\vert\ \bot&\neg\text{-elim }7,1\\
9&\neg Q&\neg\text{-intro }6\text{--}8\\
10&\neg P\land\neg Q&\land\text{-intro }5,9
\end{array}
$$
Both <temporary assumptions> have been discharged before the final <conjunction introduction>, so
$$
\boxed{\neg(P\lor Q)\ \vdash\ \neg P\land\neg Q.}
$$
Back to article page
