= 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 is
$$
\boxed{\frac{\Gamma,\neg\phi\vdash\bot}{\Gamma\vdash\phi}.}
$$
This is a rule of <classical propositional logic>. It follows from the paper's <negation introduction rule>, which first yields $\neg\neg\phi$, and <double-negation elimination>, which yields $\phi$. This is stronger than merely deriving $\neg\phi$ by showing that $\phi$ leads to <logical falsity>.
Back to article page
