= Solution
First derive $A$ by <double-negation elimination>, then derive $\neg B$ by <negation introduction>. The <logical falsity elimination rule> is used only inside the attempt to derive $A$.
``
1 ¬(A → B) premise
2 | ¬A assumption
3 | | A assumption
4 | | ⊥ ¬-elim 3,2
5 | | B ⊥-elim 4
6 | A → B →-intro 3–5
7 | ⊥ ¬-elim 6,1
8 ¬¬A ¬-intro 2–7
9 A ¬¬-elim 8
10 | B assumption
11 | | A assumption
12 | | B reiteration 10
13 | A → B →-intro 11–12
14 | ⊥ ¬-elim 13,1
15 ¬B ¬-intro 10–14
16 A ∧ ¬B ∧-intro 9,15
``
Reiteration at line 12 merely uses an assumption that remains in scope. The final \b[$A\land\neg B$] follows by <conjunction introduction>. This explicitly supplies the classical step needed to obtain $A$ rather than just $\neg\neg A$.
Back to article page
