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

Keep the premise $P\to Q$ open. Assume $Q\to \neg P$, then temporarily assume $P$. Two applications of the implication elimination rule produce $Q$ and then $\neg P$, contradicting the temporary $P$. Discharge $P$ using the negation introduction rule, then discharge $Q\to \neg P$ using the implication introduction rule.This natural deduction proof uses only the supplied introduction and elimination rules. Line 6 is an application of the negation elimination rule; no classical contradiction principle is needed.