# Cut rule

> Mediated Wiki article. Canonical URL: https://mediated.wiki/source/Cut_rule
> Markdown URL: https://mediated.wiki/source/Cut_rule.md
> Source: https://en.wikipedia.org/wiki/Cut_rule
> Source revision: 1350954366
> License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/)

Inference rule

This article relies largely or entirely on a single source. Please help improve this article by citing more sources. Find sources: "Cut rule" – news · newspapers · books · scholar · JSTOR (July 2017)

In [mathematical logic](/source/Mathematical_logic), the **cut rule** is an [inference rule](/source/Inference_rule) of [sequent calculus](/source/Sequent_calculus). It is a generalisation of the classical [modus ponens](/source/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](/source/Modus_ponens), such as how instances of *man* are eliminated from *Every man is mortal, [Socrates](/source/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](/source/Cut-elimination_theorem) for many proof systems in both [classical logic](/source/Classical_logic) and [non-classical logic](/source/Non-classical_logic).

## Formal notation

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

- Γ ⊢ A , Δ Γ ′ , A ⊢ Δ ′ Γ , Γ ′ ⊢ Δ , Δ ′ {\displaystyle {\begin{array}{c}\Gamma \vdash A,\Delta \quad \Gamma ',A\vdash \Delta '\\\hline \Gamma ,\Gamma '\vdash \Delta ,\Delta '\end{array}}} cut[1]

## Elimination

The cut rule is the subject of an important theorem, the [cut-elimination theorem](/source/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

1. **[^](#cite_ref-1)** ["cut rule in nLab"](https://ncatlab.org/nlab/show/cut+rule). *ncatlab.org*. Retrieved 2024-10-22.

This mathematical logic–related article is a stub. You can help Wikipedia by adding missing information.

- [v](https://en.wikipedia.org/wiki/Template:Mathlogic-stub)
- [t](/source/Template_talk%3AMathlogic-stub)
- [e](https://en.wikipedia.org/wiki/Special:EditPage/Template:Mathlogic-stub)

---
Adapted from the Wikipedia article [Cut rule](https://en.wikipedia.org/wiki/Cut_rule) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/Cut_rule?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.