= Solution
The derived <proof by contradiction> rule is
$$
\frac{\Gamma,\neg\phi\vdash\bot}{\Gamma\vdash\phi}\quad\mathrm{RAA},
$$
where the displayed assumption $\neg\phi$ is discharged. Replace each use by <negation introduction>, giving $\Gamma\vdash\neg\neg\phi$, followed by <double-negation elimination>, giving $\Gamma\vdash\phi$. Applying this replacement recursively removes all RAA occurrences while preserving the final conclusion and open premises. This uses the classical double-negation rule already supplied in the paper; it is not a general derivation of classical RAA from intuitionistic rules alone.
Back to article page
