THE SEQUENT CALCULUS

Gentzen's symmetric proof system: sequents Γ ⊢ Δ read "the conjunction of Γ implies the disjunction of Δ." Left and right rules for every connective, plus one detour rule — CUT — and the theorem that CUT can always be removed. Cut-elimination is the source of consistency and of the subformula property. Every claim below is computed live by exhaustive truth table, not asserted.

source Gentzen, Untersuchungen über das logische Schließen. I, Math. Zeitschrift 39 (1935) 176–210 · doi:10.1007/BF01201353 Rendered, not quoted.

Blue team · builds & defends
3

The model

A formula is built from atoms by ¬ ∧ ∨ →. A sequent Γ ⊢ Δ pairs a multiset of assumptions Γ with a multiset of alternatives Δ.

It is valid iff for every valuation, (∧Γ) → (∨Δ) holds — empty Γ is true, empty Δ is false.

LK builds proofs from the axiom A ⊢ A upward by left/right rules. Each rule is sound: if its premises are valid, so is its conclusion — verified here over the full truth table.

5

The lineage

LK is the-natural-deduction made symmetric. Where natural deduction hides structure in a single conclusion, Gentzen split it into two-sided sequents so introduction/elimination become tidy left/right pairs. The payoff is the Hauptsatz: CUT is admissible. Cut-elimination gives consistency (no proof of the empty sequent ⊢) and the subformula property — the structural core of proof theory.
7

The witness · live re-check

Re-runs the cut-integrity guarantee against the engine's current state. Sound cuts (matching cut-formula) preserve validity; an unsound cut is caught because its conclusion fails the truth-table check.

—

Press TAMPER (window 6): this badge flips to CAUGHT.

The machine
4

Data in in ↓

End-sequent to prove (transitivity of implication):

Rule kit: axiom, ∧L/∧R, ∨L/∨R, ¬L/¬R, →L/→R, and CUT. The engine will build one proof with cut and one cut-free proof of the same sequent.

● ↓ ●
0

The panel lit

Validity of the end-sequent — exhaustive over all valuations:
PROOF WITH CUT — cut-formula q as a lemma / detour
CUT-FREE PROOF — same end-sequent, subformula property holds
● ↓ ●
8

Data out out ↓

—

Red team · attacks & breaks
1

The adversary

wall "Cut is just modus ponens — drop it and nothing changes."
False and true at once. Cut is admissible (removable) but not free: Gentzen's elimination procedure can blow proof size up by a non-elementary tower. The provable sequents are unchanged; the short proofs are not. Cut is where lemmas — and speed — live.
2

The graveyard

"A sequent is valid iff Γ and Δ share a formula."
Sharing (the axiom case) is sufficient, not necessary. p∧q ⊢ q is valid with no shared formula.
"Cut-free means no lemmas, so the calculus is weak."
Same theorems — completeness is preserved. Only the form of proofs is constrained (analytic).
"Empty right side Γ ⊢ is meaningless."
It asserts Γ is contradictory (implies the empty disjunction = false).
"Cut-elimination works for every logic." amber
Assumed only for the systems Gentzen proved (LK/LJ, propositional here). It can fail or need care with naive rules.
6

The tamper

Planted void: perform a cut on two non-matching cut-formulas — combine … ⊢ …, (r∨¬r) on the left premise with …, (s∧¬s) ⊢ … on the right. Both premises are valid, but the "cut" splices different formulas, so the conclusion p ⊢ q is not valid.

The witness (window 7) catches it: the spliced conclusion fails the truth-table check.