Cut Rule¶
A sequent-calculus inference rule that composes two derivations through a matched intermediate formula, discharging it from the result.
Core Idea¶
The cut rule combines two formal derivations through an intermediate formula. One derives \(A\); another uses \(A\) as an assumption. Cut yields a composed sequent in which that matched occurrence of \(A\) is discharged. In classical two-sided notation, \(\Gamma\vdash\Delta,A\) and \(A,\Pi\vdash\Lambda\) yield \(\Gamma,\Pi\vdash\Delta,\Lambda\), subject to the host calculus's context rules.[^ref-fd0632060f4f]
Cut is the inference rule, not the cut-elimination theorem. Gentzen's LK and LJ have a theorem allowing proofs with cuts to be transformed into proofs of the same endsequent without cuts; that result cannot be assumed for an arbitrary new logic.[ref-fd0632060f4f][ref-1296aed35d96]
Scope of Application¶
In classical sequent calculus, cut can express a lemma-mediated step. For example, cut a derivation of \(p,q\vdash p\land q\) against \(p\land q\vdash p\) to obtain \(p,q\vdash p\). The intermediate \(p\land q\) disappears from the endsequent; this simple conclusion also has a cut-free proof.[^ref-fd0632060f4f]
In Girard's linear-logic proof nets, a CUT-link joins dual occurrences \(A\) and \(A^{\perp}\) from proof structures. Linking two identity nets in this way leaves two other dual outputs, and identity-cut reduction reconnects them without the cut link. This is the same matching-and-discharge skeleton under a different, occurrence-sensitive resource discipline.[^ref-fbf21fcc23e6]
Clarity¶
The cut formula is the precise interface between a producer derivation and a consumer derivation. Their remaining contexts form the new judgment; matching is governed by the proof system, not by topical similarity. This separates cut from modus ponens, a generic lemma citation, and the separate metatheoretic act of eliminating cuts.[ref-fd0632060f4f][ref-1296aed35d96]
Manages Complexity¶
Cut lets a proof be organized around an intermediate result rather than exposing the producer's full derivation at every use. But the intermediate formula need not appear in the final sequent, complicating subformula-guided proof search. A cut-free proof in a suitable calculus restores the relevant subformula discipline; conversion can greatly increase proof height, so neither form is universally shorter.[^ref-fd0632060f4f]
Abstract Reasoning¶
To test a proposed cut, identify both valid premises, the formula occurrence established by one and used by the other, and the inherited contexts. Then check the host's structural rules before forming the conclusion. Do not infer from cut elimination that first-order predicate logic is decidable: quantifier instantiations can still range over infinitely many terms.[^ref-fd0632060f4f]
Knowledge Transfer¶
The producer–consumer–discharge relation transfers between classical sequent proofs and linear-logic proof nets, but LK's weakening and contraction rules do not transfer automatically to resource-sensitive logic. Live Inference Rule is the proposed strict parent because cut is a specified premise-to-conclusion schema with extra matching structure. A broader notion of mediated composition is a future-prime question, not a current parent inferred from the name.[ref-fd0632060f4f][ref-fbf21fcc23e6]
[^ref-fd0632060f4f]: 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. [^ref-fbf21fcc23e6]: Jean-Yves Girard, “Proof-Nets: The Parallel Syntax for Proof-Theory”, §1.1 Definition 1 and §2.3 Definition 14. [^ref-1296aed35d96]: Frank Pfenning, “Sequent Calculus,” ch. 3 of Automated Theorem Proving course handouts, Carnegie Mellon University, draft 22 January 2004, §§3.3–3.4.
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 (65th 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
- Cut-Elimination Theorem — 0.89
- Intuitionistic Type Theory — 0.86
- Proof calculus — 0.84
- Rule of replacement — 0.84
- Principle of Explosion — 0.83
Computed from structural-signature embeddings · 2026-10-08