Cut-elimination theorem

The theorem that derivations using a cut rule can be transformed into derivations without it. In suitable proof systems, this yields consistency and subformula properties.

Sequent calculus: A formal proof system that derives sequents using inference rules. Cut elimination is most commonly formulated as a transformation of sequent-calculus derivations.
Consistency: The property of a formal theory that it does not prove a contradiction or, equivalently in classical logic, every statement. In standard classical sequent calculi, cut elimination rules out a cut-free derivation of the empty sequent.
Gerhard Gentzen: A German logician who founded sequent calculus and proved the Hauptsatz for classical and intuitionistic logic. Gentzen established the central cut-elimination theorem in his 1934–35 work.
Cut admissibility: The property that adding a cut rule does not enlarge the set of derivable conclusions. Admissibility states the theorem’s consequence without requiring cuts to be explicit in the formal system.
Cut rule: An inference rule that combines proofs using an intermediate formula, allowing that formula to disappear from the conclusion. The theorem’s central operation removes applications of this rule.
Proof search: The process of finding a formal derivation of a specified conclusion from rules or axioms. The subformula property can restrict the formulas needed when searching for cut-free proofs.
Hauptsatz: The name Gerhard Gentzen gave to his central theorem that cuts can be eliminated from certain derivations. Hauptsatz is the original name associated with the cut-elimination result.
Cut rule (linear logic): The composition rule in linear logic that connects a proof of a formula with a proof requiring that formula. Linear logic’s cut elimination must respect its resource-sensitive rules.
Principal reduction: A proof transformation that replaces a cut on a formula introduced by both premises with cuts on its subformulas. This is the key reduction when both sides of a cut introduce its formula.
Craig interpolation theorem: A theorem stating that a logical consequence between sentences can often be mediated by a sentence using only shared vocabulary. Cut elimination supplies a standard proof of interpolation in classical first-order logic.

Linked from 3 pages