= 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>.
$$
\begin{array}{rll}
1.&P\to Q&\text{premise}\\
2.&\quad Q\to\neg P&\text{assumption }[i]\\
3.&\qquad P&\text{assumption }[j]\\
4.&\qquad Q&\to\text{-elimination, }1,3\\
5.&\qquad\neg P&\to\text{-elimination, }2,4\\
6.&\qquad\bot&\neg\text{-elimination, }3,5\\
7.&\quad\neg P&\neg\text{-introduction, }3\text{--}6;\ [j]\text{ discharged}\\
8.&(Q\to\neg P)\to\neg P&\to\text{-introduction, }2\text{--}7;\ [i]\text{ discharged}.
\end{array}
$$
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.
Back to article page
