  Since the introduction of Gentzen’s sequent calculus (Gentzen 1935), we have known that the difference between classical logic and intuitionistic logic can also be understood as a difference of structural rules. Instead of considering sequents of the form \(X \vdash A\), in which we have a collection of antecedents and a single consequent, for classical logic it is fruitful to consider sequents of the form 