Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Digital systems, linear algebra, introduction to formal proof / 7 / c / 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 isHere 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 $\perp$. 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.^[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.