= Solution
Under the premise, assuming either disjunct would introduce the forbidden <logical disjunction>. Discharging those two assumptions gives the two separate <negations>, which can then be conjoined.
\Table[
|| Line
|| Open assumptions
|| Formula
|| Justification
| 1
| 1
| $\neg (P\lor Q)$
| Premise
| 2
| 1, 2
| $P$
| <Temporary assumption>
| 3
| 1, 2
| $P\lor Q$
| <disjunction introduction> L 2
| 4
| 1, 2
| $\bot$
| <negation elimination rule> 3, 1
| 5
| 1
| $\neg P$
| <negation introduction> 2, 4
| 6
| 1, 6
| $Q$
| <Temporary assumption>
| 7
| 1, 6
| $P\lor Q$
| <disjunction introduction> R 6
| 8
| 1, 6
| $\bot$
| <negation elimination rule> 7, 1
| 9
| 1
| $\neg Q$
| <negation introduction> 6, 8
| 10
| 1
| $\neg P\land\neg Q$
| <conjunction introduction> 5, 9
]
{title=Derivation of the two negated disjuncts}
Thus
$$
\boxed{\neg P\land\neg Q.}
$$
The redundant closing parenthesis printed after the conclusion on p. 8 does not alter the readable <propositional formula>.<Digital systems, linear algebra, introduction to formal proof examination paper by the University of Oxford (2013)>[Printed p. 8, Question 7(d)(i)]{ref}
Back to article page
