Cut Rule¶

A sequent-calculus inference rule that composes two derivations through a matched intermediate formula, discharging it from the result.

Version: v1 · 2026-10-03 · History
Domain-specific #: 13119
Domain group: Formal Sciences
Origin domain: Mathematics
Subdomains: Proof Theory, Sequent Calculus → Mathematics
Aliases: Rule of cut

Core Idea¶

The cut rule is a formal way to use an intermediate result inside a proof. One derivation establishes a formula \(A\); another derivation uses \(A\) as an assumption. Cut composes the two derivations into a new one whose conclusion no longer requires that matched occurrence of \(A\). In a classical two-sided sequent notation, a common form is

\[\frac{\Gamma\vdash\Delta,A\qquad A,\Pi\vdash\Lambda}{\Gamma,\Pi\vdash\Delta,\Lambda}\;\mathrm{Cut}.\]

The contexts and their exchange, weakening, contraction, or resource conditions belong to the host calculus; this display is the ordinary classical form, not a license to import classical structural rules into every logic. The rule's identity is the matched intermediate-formula composition. A lemma may make a proof easier to construct or understand even though the lemma formula disappears from the endsequent.^[1]^[2]

Cut itself is an inference rule. Cut elimination is a separate metatheorem showing, for a specified calculus, that derivations using the rule can be transformed into derivations of the same endsequent without it. Gentzen's classical and intuitionistic sequent calculi have that property; one must prove it again, under the relevant conditions, for other systems. Neither eliminability nor a particular normalization algorithm is a constituent of an individual cut step.^[3]^[1]^[2]

Structural Signature¶

Sig role-phrases: host proof calculus and sequents — producer derivation — consumer derivation — matched cut formula — context-preserving composed conclusion.

Host proof calculus and sequents. A calculus specifies which judgments count as derivable and how formula occurrences and contexts are handled. Classical LK allows structural rules that resource-sensitive linear logic restricts; the inference must respect its own host rather than a generic informal syllogism.^[1]^[4]
Producer derivation. The first premise yields the intermediate formula in a conclusion/right position. In a graphical proof-net presentation, it exposes a formula occurrence that can be linked to a dual occurrence.^[1]^[4]
Consumer derivation. The second premise has a matching formula available as an assumption/left occurrence, or a dual proof-net port. It is a genuine derivation, not simply an asserted desired conclusion.^[1]^[2]^[4]
Matched cut formula. The formula \(A\) in the classical display, or the pair \(A,A^{\perp}\) in a one-sided linear-logic proof net, supplies the interface. The matching is syntactic and typed by the calculus; cutting unrelated formulas would not be the same legal rule.^[1]^[4]
Context-preserving composed conclusion. The nonmatched surrounding contexts remain, subject to the calculus's context discipline; the matched intermediate occurrence is removed from the new judgment. This is why the rule is a proof-composition operation rather than a report that one proof happens to mention another.^[1]

Subformula behavior and cut elimination are consequences to investigate, not additional roles in the rule's signature. A rule instance remains cut even if its host calculus has not established a general cut-elimination theorem.^[1]

What It Is Not¶

The rule is not cut elimination: applying cut adds or uses an intermediate interface, while eliminating cuts rewrites a proof to remove such inferences. It is not the subformula property either. A cut formula need not appear in the endsequent, so a proof containing cut need not have the simple endsequent-subformula discipline of an appropriate cut-free sequent proof.^[1]

It is not identical to modus ponens. Modus ponens derives \(B\) from \(A\) and \(A\to B\); cut composes two derivations with a matched formula and propagates their contexts. Modus ponens can be represented with sequent rules in suitable systems, but that relationship is not synonymy. A cut in a graph, an optimization cutting plane, and ordinary editing of a proof are separate identities despite the shared word.^[1]^[2]

Scope of Application¶

In classical sequent calculus, a cut permits a proof to pass through a lemma not visible in the final sequent. Girard's Proofs and Types gives the multi-conclusion classical rule and analyzes Gentzen's result that cut can be removed from its standard calculus. The theorem is significant because cut-free derivations regain a subformula discipline, not because every cut-free proof is shorter.^[1]

In linear-logic proof nets, Girard gives a CUT-link with two dual formula occurrences, \(A\) and \(A^{\perp}\), as premises and no conclusion. The representation is graphical and occurrence-sensitive rather than a two-sided LK proof tree. The same producer–consumer match is present, but linear logic's restrictions on contraction and weakening cannot be discarded when carrying the idea across.^[4]^[1]

In intuitionistic sequent calculus, the succedent is restricted to at most one formula; Pfenning presents a single-conclusion cut form and proves admissibility and elimination for that specified calculus. These are genuinely different host rules around a shared core. The name should not be used as a guarantee that an arbitrary newly designed calculus enjoys cut elimination.^[2]

Clarity¶

The rule clarifies which formula is the proof interface. In \(\Gamma\vdash\Delta,A\), \(A\) is available as a derived conclusion; in \(A,\Pi\vdash\Lambda\), it is a used assumption. It is their matched occurrence—not any common topic or merely similar symbol—that licenses the combined judgment. The conclusion's contexts are inherited from the two premises under the host calculus's structural conventions.^[1]

It also separates three questions often collapsed into one: Can cut be stated as a legal inference in this proof system? Is cut admissible if not primitive? Can a proof with cut be effectively normalized, and at what cost? The first is about the rule's form; the others are system-specific theorems and complexity questions.^[1]^[2]

Manages Complexity¶

A cut packages a possibly long intermediate derivation behind the interface formula \(A\). A reader or proof constructor can establish \(A\) once and then use it in a continuation that assumes \(A\), rather than exposing the whole derivation at the point of use. This is a modularity benefit, not a theorem that every cut shortens every proof.^[2]

The hidden interface has a cost for proof search. Starting from an endsequent, the cut formula may be arbitrarily chosen rather than read from the final formulas. A cut-free presentation in a suitable calculus restores a subformula-guided search discipline, but the normalization itself can cause severe proof growth. Girard's original authored analysis gives a hyperexponential worst-case height bound for the classical elimination construction; that does not assert that each concrete proof expands by that amount.^[1]

Abstract Reasoning¶

Given two proposed premises, first verify that the producer's succedent formula and consumer's antecedent formula really match under the calculus. Then remove only those matched occurrences and combine the residual contexts according to the host's exchange/resource rules. In LK, one may cut a derivation of \(p,q\vdash p\land q\) against a derivation of \(p\land q\vdash p\), obtaining \(p,q\vdash p\). The intermediate \(p\land q\) is absent from the endsequent. A cut-free proof of \(p,q\vdash p\) also exists from identity and weakening, illustrating admissibility in this small case without pretending that the example proves the general theorem.^[1]

For a proof-search question, the same analysis warns against a false conclusion: cut elimination plus the subformula property does not make first-order predicate logic decidable. Quantifier rules still admit indefinitely many term substitutions. Girard states that limitation explicitly.^[1]

Knowledge Transfer¶

The core inference relation transfers from two-sided LK sequents to one-sided linear-logic proof nets: a derived occurrence and a complementary used occurrence connect two proof structures, and the joined result hides their interface. What does not transfer unchanged is LK's treatment of weakening and contraction. In proof nets, the graphical CUT-link links dual occurrences; that is a representational and resource-sensitive translation of the relation, not a license to reuse the LK display verbatim.^[1]^[4]

Under suitable proofs-as-programs interpretations, composing proofs through a cut can correspond to computational composition, and reducing the cut can correspond to normalization. That is an interpretation in particular calculi, not the definition of every cut or a claim that arbitrary programs evaluate by Gentzen's exact procedure.^[1]^[2]

Examples¶

A classical LK lemma. Derive \(p,q\vdash p\land q\) using the conjunction-right rule, and separately derive \(p\land q\vdash p\) using conjunction-left. Cut on \(p\land q\) to get \(p,q\vdash p\). The endsequent does not contain the lemma formula, and this simple result is also obtainable cut-free.^[1] Mapped back: host proof calculus and sequents = classical two-sided LK; producer derivation = \(p,q\vdash p\land q\); consumer derivation = \(p\land q\vdash p\); matched cut formula = \(p\land q\) in opposite sequent positions; context-preserving composed conclusion = \(p,q\vdash p\) with that intermediate discharged.

A linear-logic proof-net connection. Begin with two identity links, each exposing dual conclusions \(A\) and \(A^{\perp}\). Attach one \(A\) occurrence from the first to one \(A^{\perp}\) occurrence from the second with Girard's CUT-link. The other two dual occurrences remain external; applying the documented identity-cut reduction removes the CUT-link and produces the remaining identity connection. This is a small constructed net instance, not a claim about arbitrary net normalization time.^[4] Mapped back: host proof calculus and sequents = Girard's occurrence-sensitive proof-net syntax; producer derivation = first identity net with an \(A\) output; consumer derivation = second identity net with an \(A^{\perp}\) port; matched cut formula = those dual occurrences; context-preserving composed conclusion = remaining dual outputs after the cut link is reduced to an identity link.

Structural Tensions¶

Modular lemma versus analytic search. Cut lets a proof be organized around an intermediate statement chosen for explanatory or construction value. But that formula may be invisible in the endsequent, weakening the subformula-bounded search discipline. Removing cuts restores the analytic shape in suitable systems but may greatly enlarge a derivation; neither representation is automatically best for every purpose.^[1]^[2] Diagnostic: Is the goal a readable/composable proof, or a cut-free normal form for controlled proof search, and what normalization cost is acceptable?

Shared skeleton versus calculus-specific resource rules. Treating LK and linear-logic cuts as one abstract pattern reveals how intermediate derivations connect. Yet importing LK's unrestricted weakening or contraction into linear logic would change what a valid proof can use or discard. Transfer of the relation is useful only when the host's formula-occurrence and context constraints stay explicit.^[1]^[4] Diagnostic: Which structural rules and duality conventions does this calculus actually permit around the cut?

Structural–Framed Character¶

Cut is strongly structural within its formal proof-theory frame. Its matched-interface composition is stable across classical sequent trees and linear-logic proof nets, but formulas, derivations and legal context propagation are not removable accents. The five criteria give that placement precision. Evaluative weight: cut is a formal inference, not intrinsically good or bad; modular readability and search cost are different assessments. Human-practice dependence: mathematicians design and choose proofs, but rule validity is fixed by the formal calculus, not by a community preference. Institutional origin: Gentzen and later authors supplied formulations, yet no particular institution's authority makes a cut instance valid. Vocabulary travel: “cut” persists across sequent and proof-net presentations, while graph and optimization uses of the word are not the same identity. Import versus recognition: the cross-calculus relation is recognized by matching producer, consumer and discharged interface; importing LK's context rules into a resource-sensitive calculus would be a category error.^[1]^[4]

Its character: a precise, reusable domain-specific inference-rule abstraction, close to the structural end inside logic but not a substrate-independent prime. The named rule's admissibility and consequences remain matters for each host system.

Structural Core vs. Domain Accent¶

The core is the formal match-and-compose operation: a producer derives an intermediate formula, a consumer uses a corresponding occurrence, and the rule yields a composed conclusion with that occurrence discharged. The domain-bound mechanism is an inference within sequents or corresponding proof objects, governed by typed formula occurrence and context rules. LK's multi-succedent notation, LJ's single succedent, and linear-logic CUT-links are different accents; none individually defines the whole identity.^[1]^[2]^[4]

Remove the proof calculus, formula match and judgment transformation and one has only the broader idea of mediated composition. That broader skeleton is an explicit future-prime question. It is not a license to call cut itself a prime, or to assert an unsourced edge to live Composition. The actual proposed typed parent is Inference Rule, whose formal-schema commitments every cut instance satisfies.

This entry is a kind of Inference Rule.

The proposed DAG has one strict subsumption edge to live Inference Rule. A cut is a formal, repeatable premise-to-conclusion schema in a specified proof system; it adds the matched, discharged intermediate formula that other inference rules need not have. This is an asymmetric subtype relation, not a synonym and not a claim that Inference Rule presupposes cut.

There is no asserted prime parent. Generic composition is an analogy unless its full live signature and typed relation are justified. Modus Ponens is a related inference rule, not the parent: its two formula premises do not themselves express the composition of two derivation trees with inherited contexts.^[1]

Relationships to Other Abstractions¶

Current abstraction Cut Rule Domain-specific

Parents (1) — more general patterns this builds on

Cut Rule is a kind of Inference Rule Domain-specific

Cut is a formal inference-rule schema with two derivational premises, a matched intermediate formula, and a context-preserving conclusion.

Hierarchy path (1) — routes to 1 parentless root

Cut Rule → Inference Rule

Neighborhood in Abstraction Space¶

Cut Rule sits in a sparse region of the domain-specific corpus (65^th percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.

Family — Formal Logic & Language Constructs (20 abstractions)

Nearest neighbors

Computed from structural-signature embeddings · 2026-10-08

Not to Be Confused With¶

Cut elimination: a theorem or reduction procedure removing cut steps in a specified calculus, not the cut inference step itself.^[1]
Modus ponens: from \(A\) and \(A\to B\) infer \(B\); it can interact with sequent proofs but does not state the same two-derivation context-composition schema.^[2]
A subformula rule: cut can introduce an intermediate not present in the final sequent; cut-free proofs regain the relevant subformula discipline only under the host calculus's hypotheses.^[1]
A universal decidability theorem: cut elimination does not decide first-order predicate logic.^[1]
Graph cuts or optimization cutting planes: neither has the typed producer/consumer proof relation defined here.
Unqualified program evaluation: proof normalization can have computational interpretations, but that is not every cut's identity.^[1]

References¶

[1] Jean-Yves Girard, Proofs and Types, translated with appendices by Paul Taylor and Yves Lafont, Cambridge University Press (1989), ch. 5 §§5.1.4, 5.2.2 and ch. 13 §13.3; author's/translator's freely available edition. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k ↩l ↩m ↩n ↩o ↩p ↩q ↩r ↩s ↩t ↩u ↩v ↩w ↩x ↩y ↩z ↩27 ↩28 ↩29

[2] Frank Pfenning, “Sequent Calculus,” ch. 3 of Automated Theorem Proving course handouts, Carnegie Mellon University, draft 22 January 2004, §§3.3–3.4. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k

[3] Gerhard Gentzen, “Untersuchungen über das logische Schließen I”, Mathematische Zeitschrift 39 (1935), 176–210; original historical publication record. The technical claims here are checked against the accessible authored sources above. registry ↩

[4] Jean-Yves Girard, “Proof-Nets: The Parallel Syntax for Proof-Theory”, original research paper, §1.1 Definition 1 and §2.3 Definition 14 for CUT/ID links and identity-cut reduction. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j