of a sequent, , where are finite multisets of formulas, establishes a fundamental duality between antecedents (left) and succedents (right). This duality is explicitly realized by the left and right introduction rules for each logical connective. For example, the rules for conjunction () and disjunction () are dual:

This left-right symmetry reflects a deeper harmony between the syntactic meaning of a connective, defined solely by its introduction rules,via the principle of inversion, and its eliminative behavior. The cut-elimination