Cut rule
From Wikipedia, the free encyclopedia
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.
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 for many proof systems in both classical logic and non-classical logic.
