cut-elimination theorem a theorem stating that a certain type of inference rule (including a rule that corresponds to modus ponens) is not needed in classical logic. The idea was anticipated by J. Herbrand; the theorem was proved by G. Gentzen and generalized by S. Kleene. Gentzen formulated a sequent calculus – i.e., a deductive system with rules for statements about derivability. It includes a rule that we here express as ‘From (C Y D,M) and (M,C Y D), infer (C Y D)’ or ‘Given that C yields D or M, and that C plus M yields D, we may infer that C yields D’. This is called the cut rule because it cuts out the middle formula M. Gentzen showed that his sequent calculus is an adequate formalization of the predicate logic, and that the cut rule can be eliminated; anything provable with it can be proved without it. One important consequence of this is that, if a formula F is provable, then there is a proof of F that consists solely of subformulas of F. This fact simplifies the study of provability. Gentzen’s methodology applies directly to classical logic but can be adapted to many nonclassical logics, including some intuitionistic logics. It has led to some important theorems about consistency, and has illuminated the role of auxiliary assumptions in the derivation of consequences from a theory. See also CONSISTENCY, PROOF THEORY. D.H.