Top Qs
Timeline
Chat
Perspective

Cut rule

Inference rule From Wikipedia, the free encyclopedia

Remove ads

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 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.

Remove ads

Formal notation

It is normally written in formal notation in sequent calculus notation as :

cut[1]
Remove ads

Elimination

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.

References

Loading related searches...

Wikiwand - on

Seamless Wikipedia browsing. On steroids.

Remove ads