Sequent Calculus and Cut Elimination

The main theorem of proof theory — removing shortcuts does not change the conclusion

Goal of this page

Understand how to read a sequent $\Gamma \vdash \Delta$ and how proofs are built from left and right rules. Grasp the cut rule (the use of lemmas), the cut-elimination theorem which says cut can be removed, and its consequences — the subformula property and consistency.

1. What is a sequent?

A sequent has the form $\Gamma \vdash \Delta$. Both $\Gamma$ (the antecedent) and $\Delta$ (the succedent) are lists of formulas. It is read as follows.

$A_1, \dots, A_m \vdash B_1, \dots, B_n$ is read as “if $A_1$ and … and $A_m$ all hold, then at least one of $B_1$ or … or $B_n$ holds”. In other words, the left-hand side acts as a conjunction and the right-hand side as a disjunction. In classical logic this corresponds to reading $\Gamma \vdash \Delta$ as $(\bigwedge \Gamma) \to (\bigvee \Delta)$.

Whereas natural deduction (Basic) is a vertical proof tree deriving “a single conclusion”, the sequent calculus handles the relation between collections of assumptions and conclusions in one line. For each connective we give a rule for when it appears on the left (a left rule) and when it appears on the right (a right rule).

Examples of rules (conjunction and implication)

The starting point is the axiom $A \vdash A$ (the same formula can be derived from itself). From there we build downward.

$$A \vdash A \quad(\text{axiom}) \qquad \dfrac{\Gamma \vdash \Delta,\, A \quad \Gamma \vdash \Delta,\, B}{\Gamma \vdash \Delta,\, A \land B}\ (\land\text{R})$$ $$\dfrac{\Gamma \vdash \Delta,\, A \quad \Gamma,\, B \vdash \Delta}{\Gamma,\, A \to B \vdash \Delta}\ (\to\text{L})$$

$(\land\text{R})$ reads “to build $A \land B$ on the right, it suffices to show $A$ and $B$ separately”. $(\to\text{L})$ reads “when $A \to B$ is on the left (available), show $A$ and proceed assuming $B$”. Each connective comes with both a left and a right rule.

In addition there are structural rules (weakening, contraction, exchange) that add formulas, collapse duplicates, or swap the order. These are auxiliary rules that arrange “the number and order of the materials used”.

2. The cut rule — using lemmas

In mathematical proofs we often prove a lemma $A$ first and then use it as a tool to carry the main argument forward. The rule that captures this is cut.

The cut rule
$$\dfrac{\Gamma \vdash \Delta,\, A \qquad A,\, \Gamma \vdash \Delta}{\Gamma \vdash \Delta}\ (\text{Cut})$$

The left branch shows the lemma $A$ as a conclusion, and the right branch uses that $A$ as an assumption. As a result $A$ disappears from the final conclusion (it is cut). It is the very natural inference of “proceeding via $A$”. (Here we have aligned the contexts of both branches and written $\Gamma, \Delta$, but in general the contexts are independent: the standard form derives $\Gamma,\, \Pi \vdash \Delta,\, \Lambda$ from $\Gamma \vdash \Delta,\, A$ and $A,\, \Pi \vdash \Lambda$.)

Cut is convenient and makes proofs shorter and easier to read. On the other hand, the lemma $A$ that is cut does not appear anywhere in the final conclusion. That means a “formula unrelated to the conclusion” can appear in the middle of a proof. This matters later.

3. The cut-elimination theorem (Gentzen's Hauptsatz)

The cut-elimination theorem (Hauptsatz, 1934–35) that Gentzen proved states the following.

Theorem (cut elimination): any proof that uses the cut rule can be transformed into a proof that uses no cut at all.

In other words, the “shortcut” of a lemma is in principle unnecessary: everything can be expanded into a cut-free proof. The transformation is a mechanical procedure that pushes cuts upward and breaks them into smaller ones (during which the proof can grow explosively, but the process always terminates).

With cut ⊢ A A ⊢ (Cut) Γ ⊢ Δ Lemma A is not in the conclusion transform After cut elimination (cut-free) subformulas only Γ ⊢ Δ
Figure 1: Schematic of cut elimination. On the left, a proof goes via the lemma $A$ using the cut rule, but $A$ does not appear in the conclusion $\Gamma \vdash \Delta$. On the right, the cut has been removed and every formula that appears is a subformula of the conclusion. The proof may grow larger, but the conclusion is unchanged.
Read Figure 1 as text

The proof on the left joins a branch that proves the lemma $A$ as a conclusion ($\vdash A$) with a branch that uses $A$ as an assumption ($A \vdash$) via the cut rule, yielding the conclusion $\Gamma \vdash \Delta$. The lemma $A$ does not appear in the final conclusion. On the right is the proof after cut elimination: the cut is gone and every formula appearing in the proof is a subformula of the conclusion. The conclusion is the same, but the shape (and size) of the proof changes.

4. The subformula property and its consequences

Cut-free proofs have a striking property.

Subformula property: every formula appearing in a cut-free proof is a subformula of the conclusion (the bottom sequent).

No formula unrelated to the conclusion ever appears in the middle of the proof, because reading each rule from the bottom up simply removes one connective at a time. Important consequences follow.

  • Consistency: the empty sequent $\vdash$ (“a contradiction with no assumptions”) has no cut-free proof (with no formula in the bottom line, no rule can be applied). By cut elimination, there is then no cut-using proof of a contradiction either. This is the proof-theoretic basis for the consistency of propositional and first-order logic. (The consistency of arithmetic does not follow from this alone; Gentzen later proved it separately using transfinite induction up to $\varepsilon_0$.)
  • Proof search: since the formulas that appear are limited to subformulas, one can search for a proof mechanically upward from the conclusion. In propositional logic this yields a decision procedure (connecting to computability and decidability).
  • Correspondence with normalization: on the natural-deduction side, cut elimination corresponds to the normalization of proofs. Under the Curry–Howard correspondence, this is two sides of the same coin as the fact that reduction of typed terms terminates (strong normalization).

Summary

Key points

  • Sequent $\Gamma \vdash \Delta$: the left acts as a conjunction, the right as a disjunction
  • Give each connective a left rule and a right rule, and arrange the materials with structural rules (weakening, contraction, exchange)
  • Cut = the use of a lemma; the lemma does not appear in the final conclusion
  • Cut-elimination theorem (Gentzen): every cut can be removed; the conclusion is unchanged but the proof may grow larger
  • From the subformula property follow consistency, proof search (a decision procedure), and the correspondence with normalization

Frequently Asked Questions

What is the sequent calculus?

A proof system introduced by Gentzen that deals with sequents $\Gamma \vdash \Delta$. If all formulas on the left, $\Gamma$, hold, then at least one formula on the right, $\Delta$, holds. Each connective is given a left rule and a right rule, and a proof is built by decomposing formulas from the conclusion upward.

What is the cut-elimination theorem?

The cut rule is the inference “prove a lemma $A$, then use it to go forward”. The cut-elimination theorem (Gentzen's Hauptsatz) states that every proof using cut can be converted into one that uses no cut. Removing the shortcut of a lemma does not change the conclusion.

Why is the subformula property important?

In a cut-free proof every formula that appears is a subformula of the conclusion. Since no unrelated formula appears during the proof, one can search for proofs mechanically from the bottom up, and the empty sequent $\vdash$ has no proof. This is the basis for proofs of consistency and for decision procedures.