= Solution
<Proof by contradiction>, or <reductio ad absurdum>, has the form
$$
\boxed{\frac{\Gamma,\neg\phi\vdash\bot}{\Gamma\vdash\phi}\quad\mathrm{RAA},}
$$
discharging the assumption $\neg\phi$. This is the classical rule that concludes $\phi$ directly, as opposed to the <negation introduction rule>, which concludes a negation.
To derive <double-negation elimination> using RAA without assuming <double-negation elimination> itself, use
``
1 ¬¬φ premise
2 | ¬φ assumption
3 | ⊥ ¬-elim 2,1
4 φ RAA 2–3
``
Here line 1 is the negation of line 2. Thus only <negation elimination rule> inside the <subproof>, followed by RAA, is needed.
Back to article page
