= Solution
The <reductio ad absurdum> rule discharges an assumption $\neg\phi$ from a derivation of contradiction and concludes $\phi$. It is derivable using <negation introduction> followed by <double-negation elimination>:
$$
\frac{\Gamma,\neg\phi\vdash\bot}{\Gamma\vdash\neg\neg\phi}\ \neg I,\qquad
\frac{\Gamma\vdash\neg\neg\phi}{\Gamma\vdash\phi}\ \neg\neg E.
$$
Conversely, if RAA is supplied, <double-negation elimination> follows from this <natural deduction> derivation:
``
1. ¬¬φ premise
2. ¬φ assumption [i]
3. ⊥ ¬E, 1, 2
4. φ RAA, 2–3, discharging [i]
``
Thus replacing double-negation elimination by RAA leaves these classical deductions available. RAA is not being assumed as an intuitionistic rule.
Back to article page
