= Solution
The classical <proof by contradiction> rule, also called reductio ad absurdum, is
$$
\boxed{\frac{\Gamma,\neg\phi\vdash\bot}{\Gamma\vdash\phi}\ \mathrm{RAA},}
$$
with <assumption discharge> of the displayed $\neg\phi$. It differs from the <negation introduction rule> by concluding $\phi$ from a contradictory assumption of its <negation>.
To derive <double-negation elimination> using this rule, start with $\neg\neg\phi$, assume $\neg\phi$, and apply the <negation elimination rule> to those two formulas:
$$
\begin{array}{rll}
1&\neg\neg\phi&\text{premise}\\
2&[\neg\phi]^a&\text{assumption}\\
3&\quad\bot&\neg E\ 2,1\\
4&\phi&\mathrm{RAA}\ (2\text{--}3).
\end{array}
$$
No <double-negation elimination> occurs inside this derivation, so the argument is not circular.
Back to article page
