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

Use natural deduction with labelled temporary assumptions. Assume $\neg P\to \neg Q$ under label $a$, then $\neg P\to Q$ under label $b$, then $\neg P$ under label $c$. Two applications of the modus ponens rule give $\neg Q$ and $Q$. The negation elimination rule gives $\perp$, and the supplied reductio ad absurdum rule discharges $c$ to conclude $P$.

Discharge $b$ using the implication introduction rule, obtaining $(\neg P\to Q)\to P$ under $a$. Discharge $a$ with the implication introduction rule, obtainingAll three temporary assumptions have now been discharged; no premise remains.