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

Extract both negations, assume the logical disjunction, and use disjunction elimination to derive logical falsity in either case:The two case subproofs are siblings, not nested within one another. Therefore

Use negation introduction separately for each component, introducing the forbidden logical disjunction in each subproof:Both temporary assumptions have been discharged before the final conjunction introduction, so

In proof by contradiction, assume the negation of the desired conclusion and derive logical falsity; discharge that assumption and infer the desired conclusion. Its sequent rule isThis is a rule of classical propositional logic. It follows from the paper's negation introduction rule, which first yields $\neg \neg \varphi$, and double-negation elimination, which yields $\varphi$. This is stronger than merely deriving $\neg \varphi$ by showing that $\varphi$ leads to logical falsity.

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.