Isn the calculus of structures just a trivial notational variation of the sequent calculus?
No, the calculus of structures uses deep inference, abolishes the distinction between formula and sequent and exploits a symmetry between premiss and conclusion in inference rules: these are not features of the sequent calculus and they require new techniques. There are other formalisms which use deep inference, but none (as far as we know) allows for the same kind of proof-theoretical analysis of the sequent calculus, for example cut elimination. The only exception is Schütte’s presentation of logic, which uses deep inference, but doesn’t drop the distinction between formula and sequent and does not exploit a premiss-conclusion symmetry (for example, its cut rule has two premisses). The proof theory of Schütte doesn’t differ significantly from the usual (Gentzen) one, and does not achieve more. One can argue that the display calculus uses a form of deep inference, but again the two other features of the calculus of structures are not exploited.
