= Solution
Put $F=(\neg P)\to Q$ and $G=(\neg P)\to\neg Q$. Use the printed <implication elimination rule>, <negation elimination rule>, <negation introduction rule>, <double-negation elimination> and <implication introduction rule>:
$$
\begin{array}{rll}
1&F&\text{premise}\\
2&[F]^a&\text{assumption}\\
3&\quad[G]^b&\text{assumption}\\
4&\qquad[\neg P]^c&\text{assumption}\\
5&\qquad\quad Q&\to E\ 4,2\\
6&\qquad\quad\neg Q&\to E\ 4,3\\
7&\qquad\quad\bot&\neg E\ 5,6\\
8&\qquad\neg\neg P&\neg I\ (4\text{--}7)\\
9&\qquad P&\neg\neg E\ 8\\
10&\quad G\to P&\to I\ (3\text{--}9)\\
11&F\to(G\to P)&\to I\ (2\text{--}10).
\end{array}
$$
Line 1 is the given premise; the argument actually establishes the conclusion without needing it, since line 2 supplies its own copy of $F$. Introducing and discharging this separate <temporary assumption> preserves the exact printed conclusion.
$$
\boxed{(\neg P)\to Q\ \vdash\ ((\neg P)\to Q)\to(((\neg P)\to\neg Q)\to P).}
$$
Back to article page
