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

The classical proof by contradiction rule, also called reductio ad absurdum, iswith assumption discharge of the displayed $\neg \varphi$. It differs from the negation introduction rule by concluding $\varphi$ from a contradictory assumption of its negation.

To derive double-negation elimination using this rule, start with $\neg \neg \varphi$, assume $\neg \varphi$, and apply the negation elimination rule to those two formulas:No double-negation elimination occurs inside this derivation, so the argument is not circular.