 Cut-inductivity is one aspect of a procedure which has traditionally been a professional obsession of proof-theorists: the provision of ‘Cut Elimination’ theorems to the effect that this or that sequent calculus with the rule (Cut) can have this rule removed without the loss of any provable sequents. Obviously more is needed to show this than the Cut-inductivity of the (pairs of) rules, since there are also, inter alia, potential interactions with the other structural (and operational) rules to be taken care of. Such results are of interest because much follows from the subformula property—any sequent provable has a proof in which the only formulas to appear are subformulas of those in the sequent concerned—which itself follows from the result since all the remaining rules insert material rather than remove it in the course of the  proof.[29]  But from the perspective of the philosophy of logic, Cut-inductivity and its somewhat less well-publicized companion, Id-inductivity, should be considered on a par, as the following somewhat impressionistic semantical remark (Girard, Taylor and Lafont 1989, p. 31) of Girard suggests, apropos of (Cut), in which C represents the cut formula (and (Id) with C on the left and right of the “≻”):