Cut rule

In mathematical logic, the cut rule is an inference rule of sequent calculus. It is a generalisation of the classical modus ponens inference rule. The meaning of the cut rule 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. This applies to cases of modus ponens, such as how instances of man are eliminated from Every man is mortal, Socrates is a man to deduce Socrates is mortal.

Proofs in systems that include the cut rule often don't have the sub formula property, meaning that there can be formulas in the proof that are not sub formulas of the conclusion. This can cause issues in some proof search methods. Because of this it is often useful to reason about systems without the cut rule. This has led to many cut-elimination theorems for many proof systems in both classical logic and non-classical logic.

Formal notation

The cut rule is normally written in formal notation in sequent calculus as :

${\begin{array}{c}\Gamma \vdash A,\Delta \quad \Gamma ',A\vdash \Delta '\\\hline \Gamma ,\Gamma '\vdash \Delta ,\Delta '\end{array}}$cut

Elimination

The cut rule is the subject of an important theorem, the cut-elimination theorem. This 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.