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. Its meaning is that, if a formula A appears as a conclusion in one proof and an hypothesis in another, then another proof in which the formula A does not appear can be deduced. In the particular case of the modus ponens, for example occurrences of man are eliminated of Every man is mortal, Socrates is a man to deduce Socrates is mortal.

Formal notation

Formal notation in sequent calculus notation :

cut: $\cfrac{\Gamma \vdash A, \Delta \qquad \Gamma', A \vdash \Delta'} {\Gamma, \Gamma' \vdash \Delta, \Delta'}$

Elimination

The cut rule is the subject of an important theorem, the cut elimination theorem. It states that any judgement that possesses a proof in the sequent calculus that makes use of the cut rule also possesses a cut-free proof, that is, a proof that does not make use of the cut rule.

This article is issued from Wikipedia - version of the 4/17/2015. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.