Cut rule

It is a generalisation of the classical modus ponens inference rule.

Its meaning is that, if a formula A appears as a conclusion in one proof and a hypothesis in another, then another proof in which the formula A does not appear can be deduced.

It is normally written in formal notation in sequent calculus notation as : The cut rule is the subject of an important theorem, the cut-elimination theorem.

It states that any sequent that has a proof in the sequent calculus making use of the cut rule also has a cut-free proof, that is, a proof that does not make use of the cut rule.

This mathematical logic-related article is a stub.