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 / iii / Solution

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).