Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof (resit) / 7 / c / Solution

The derived proof by contradiction rule iswhere the displayed assumption $\neg \varphi$ is discharged. Replace each use by negation introduction, giving $\Gamma ⊢\neg \neg \varphi$, followed by double-negation elimination, giving $\Gamma ⊢\varphi$. 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.