Girish Mahajan (Editor)

Cut rule

Updated on
Edit
Like
Comment
Share on FacebookTweet on TwitterShare on LinkedInShare on Reddit

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.

Contents

Formal notation

Formal notation in sequent calculus notation :

cut
Γ A , Δ Γ , A Δ Γ , Γ Δ , Δ

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.

References

Cut rule Wikipedia


Similar Topics