theorem guarantees this meta-theoretic harmony. The cut rule,

represents a form of semantic gluing; its admissibility demonstrates that the proof system is internally consistent and analytic, i.e., proofs need not reference extraneous concepts, e.g., formula , that are not present in the conclusion. The successful reduction of a cut on a complex formula to cuts on its subformulas, via key-case reductions between left and right rules,e.g., reducing a cut on introduced by both (R) and (L), is the computational manifestation of the perfect