= Solution
In <proof by contradiction>, assume the <negation> of a desired conclusion $A$, derive <logical falsity>, and discharge the assumption to infer $A$. A rule expressing this is
$$
\boxed{\frac{\begin{array}{c}[\neg A]^i\\\vdots\\\bot\end{array}}{A}\;\mathrm{RAA}\;(i).}
$$
Here the label $i$ identifies the assumption being discharged; any other open assumptions remain.
To derive this rule using the supplied rules, apply <negation introduction> to the <subproof> from $\neg A$ to $\bot$. This discharges $\neg A$ and yields $\neg\neg A$. Apply <double-negation elimination> to obtain $A$. Thus the extra rule is admissible because Figure 1 explicitly includes <double-negation elimination>.<Digital systems, linear algebra, introduction to formal proof examination paper by the University of Oxford (2013)>[Printed p. 9, Figure 1, double-negation elimination]{ref}
This is the classical form of <proof by contradiction>; simply deriving $\neg A$ from an assumption $A$ leading to <logical falsity> uses <negation introduction> alone.
Back to article page
