= Solution
Abbreviate $H=(\neg P)\to Q$ and $K=(\neg P)\to\neg Q$. Use the primitive <natural deduction> rules, including <double-negation elimination>:
``
1 H premise
2 | H assumption
3 | | K assumption
4 | | | ¬P assumption
5 | | | Q →-elim 2,4
6 | | | ¬Q →-elim 3,4
7 | | | ⊥ ¬-elim 5,6
8 | | ¬¬P ¬-intro 4–7
9 | | P ¬¬-elim 8
10 | K → P →-intro 3–9
11 H → (K → P) →-intro 2–10
``
The outer premise is redundant: the proof uses the locally assumed $H$, so the conclusion is already a theorem. Keeping the redundant premise is allowed. The successive discharges give \b[$((\neg P)\to Q)\to(((\neg P)\to\neg Q)\to P)$] with exactly the requested assumption scopes.
Back to article page
