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 / 7 / c / iii / Solution

In proof by contradiction, assume the negation of the desired conclusion and derive logical falsity; discharge that assumption and infer the desired conclusion. Its sequent rule isThis is a rule of classical propositional logic. It follows from the paper's negation introduction rule, which first yields $\neg \neg \varphi$, and double-negation elimination, which yields $\varphi$. This is stronger than merely deriving $\neg \varphi$ by showing that $\varphi$ leads to logical falsity.