Cut rule

Template:Short description 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.

Formal notation

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

$\begin{array}{c}\mathrm{\Gamma }⊢A,\mathrm{\Delta }{\mathrm{\Gamma }}^{\prime },A⊢{\mathrm{\Delta }}^{\prime }\\ \mathrm{\Gamma },{\mathrm{\Gamma }}^{\prime }⊢\mathrm{\Delta },{\mathrm{\Delta }}^{\prime }\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.

References

Template:Asbox