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 / a

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.