Solution (source code)

= Solution

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 $\bot$, 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>, obtaining
$$
(\neg P\to\neg Q)\to((\neg P\to Q)\to P).
$$
All three temporary assumptions have now been discharged; no premise remains.