 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.