Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Digital systems, linear algebra, introduction to formal proof / 7 / c / iv / 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\vee \neg Q)$ forces $P$: otherwise $\neg P$ immediately gives the prohibited logical disjunction. It similarly forces $Q$. The formal natural deduction derivation isHenceThis 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.