Past exam of the year 1 of the computer science course of the University of Oxford / 2017 / Digital systems, linear algebra, introduction to formal proof / 7

Use conjunction elimination to obtain both premises needed for a contradiction under a temporary implication assumption. The following natural deduction derivation discharges precisely assumption 4:Here $\to E$ is the implication elimination rule and $\neg I$ is negation introduction. The original conjunction remains the only undischarged premise.

Proof by contradiction is the derived ruleGiven the subproof under $\neg A$, first discharge it by negation introduction to get $\Gamma ⊢\neg \neg A$. Apply double-negation elimination to obtain $A$. This justification uses the stated classical rules; unrestricted RAA would not follow from intuitionistic rules alone.

Put $H=\neg (P\to \neg Q)$. First derive $Q$, then $P$, using the derived proof by contradiction rule. Indentation records the subproofs:Line 11 uses explosion; lines 5 and 12 discharge only their inner assumptions. Each RAA step can be expanded into negation introduction followed by double-negation elimination, as in part (ii).

Use a biconditional introduction rule that discharges the two displayed temporary assumptions:Suitable elimination rules areThese are equivalent to using the biconditional elimination rule to extract the two implications and then applying modus ponens rule. Together they express both directions, with no extra arbitrary assumption retained after introduction.

Apply the biconditional introduction rule from part (iv) to the two already established derivations:The left numerator is part (iii), the right is part (i). Introduction discharges both displayed assumptions, so the result has no premises.

Assume the two implications in turn, then derive a contradiction from $\neg P$. The natural deduction proof isHere RAA is the derived proof by contradiction rule. The last two assumption discharge steps establish the requested right-associated implication as a theorem.

Under the negation of the desired disjunction, derive both negated propositions and contradict the premise. The natural deduction derivation isThe proof uses disjunction introduction, conjunction introduction and the classical RAA rule; it does not silently replace the required derivation by a truth-table check.