The Sequent Calculus and Why Its Rules Are Invertible

A sequent is written A₁, …, Aₘ ⊢ B₁, …, Bₙ and read as: the conjunction of the formulas on the left entails the disjunction of the formulas on the right. Both sides are lists. Natural deduction has one formula on the right and a set of assumptions on the left; the sequent calculus puts a list on both sides and, in doing so, makes every rule a statement about one connective on one side. That regularity is what makes the calculus usable for proof search, and it is why implementations of tactic provers are usually built on it rather than on natural deduction.

Why the right side holds many formulas

In intuitionistic logic at most one formula sits on the right. In classical logic any number may. The difference is not notational. A sequent Γ ⊢ Δ with several formulas on the right asserts that if all of Γ hold then at least one of Δ holds, which is a disjunctive claim. Moving a formula from the right to the left negates it, so Γ ⊢ A, Δ and Γ, ¬A ⊢ Δ are inter-derivable, and that movement is exactly what classical reasoning permits and intuitionistic reasoning does not.

The multiple right side gives a clean formulation of excluded middle: the sequent ⊢ A, ¬A is derivable by an axiom step after a negation-right rule, because the axiom rule Γ, A ⊢ A, Δ holds for any context. In the single-conclusion formulation, the corresponding principle needs a special rule or a control operator in the term language.

Left and right rules

Every connective has a right rule, which introduces it in the conclusion, and a left rule, which introduces it in a premise. For implication:

   Γ ⊢ A, Δ      Γ, B ⊢ Δ
   ----------------------  (→L)
       Γ, A → B ⊢ Δ

      Γ, A ⊢ B, Δ
      -----------  (→R)
      Γ ⊢ A → B, Δ

The right rule is the familiar one: to prove an implication, assume the antecedent on the left and derive the consequent on the right. The left rule is the unfamiliar one: an implication on the left can be used by either supplying its antecedent as a new goal on the right, or by replacing it with its consequent on the left. Read bottom-up, it branches into two subgoals.

Conjunction has a right rule that splits into two premises, since a proof of A ∧ B needs a proof of each part, and a left rule with a single premise: Γ, A ∧ B ⊢ Δ is derivable whenever Γ, A, B ⊢ Δ is, because both conjuncts are available as assumptions. Disjunction is the mirror image, with a left rule that branches into two premises, one assuming each disjunct, and a right rule that does not: Γ ⊢ A ∨ B, Δ follows from Γ ⊢ A, Δ alone. In each case the rule that introduces the connective on a side has two premises when proving that side needs both parts, and one otherwise. The symmetry is the point. Each rule mentions exactly one connective, and that connective occurs only in the conclusion for a right rule and only in the premise for the corresponding left rule.

Reading rules backwards

Proof search runs the rules from conclusion to premises: given a sequent to prove, pick a rule whose conclusion matches it and recurse on the premises. For this to terminate predictably, the rules must be invertible: if the conclusion is derivable, every premise is derivable. A rule that is merely admissible in one direction forces a search to guess.

The implication-right rule is invertible. If Γ ⊢ A → B, Δ is derivable, then Γ, A ⊢ B, Δ is derivable by attaching the right rule, and conversely. The two directions together mean the rule can be applied whenever it matches, with no loss.

The implication-left rule is not invertible in the same way. Its two premises are Γ ⊢ A, Δ and Γ, B ⊢ Δ, and from the derivability of the conclusion neither premise follows. Applying it commits the search to a particular decomposition of the implication, and if that choice is wrong the search must backtrack. This asymmetry is why the left rules for implication and for the modal connectives are the expensive ones in any backward search, and why the choice of which formula to decompose next is a real decision rather than a formality.

The structural rules behave differently again. Weakening is invertible: a derivable sequent stays derivable when formulas are added to either side, so a search can ignore it. Contraction is not. From Γ, A, A ⊢ Δ the rule produces Γ, A ⊢ Δ, and the premise is strictly more informative than the conclusion, so deleting a duplicate assumption loses information that may have been needed. What both rules share is that they do not decompose a connective, which is why a search can usually absorb them into the other rules or control them explicitly: contraction applied backwards duplicates a formula and can make a naive search loop.

The identity and cut rules

Two rules have no connective. The identity rule closes a branch:

   -----------  (Id)
   Γ, A ⊢ A, Δ

The cut rule composes two derivations:

   Γ ⊢ A, Δ      Γ, A ⊢ Δ
   ----------------------  (Cut)
          Γ ⊢ Δ

Cut is the sequent-calculus form of lemma introduction: prove an intermediate statement A, then use it. Nothing in the other rules produces it, and nothing removes it automatically. Gentzen’s cut-elimination theorem states that any derivation using cut can be transformed into one that does not, and the transformation is effective.

The theorem is the central result of proof theory, and its consequences are what make the calculus useful. A cut-free derivation has the subformula property: every formula appearing anywhere in it is a subformula of a formula in the end sequent. Since the end sequent is fixed, the search space for a proof is bounded by its subformulas, and a backward search that never applies cut is searching a finite space. This is the property exploited by every bottom-up prover, and it is developed further in Cut Elimination and the Subformula Property.

Cut elimination is not free. The standard proof is a double induction with a nested case analysis, and the transformation can produce a derivation much larger than the original. The blow-up is real: there are statements whose cut-free proofs are astronomically longer than their proofs with cut, and in some systems the increase is not bounded by any elementary function. The theorem guarantees existence, not feasibility.

What the calculus does better than natural deduction

The two presentations prove the same theorems. Their difference is in what the rules look like and therefore what can be done with them mechanically.

In natural deduction, an elimination rule removes a connective from a premise while the conclusion is something else entirely. Modus ponens takes an implication and its antecedent and concludes an arbitrary B. The rule does not say what B is, and in a backward search that means the rule cannot be applied without knowing the conclusion in advance. In the sequent calculus, the corresponding left rule rewrites the formula in place and keeps the conclusion fixed, so the search always knows what it is trying to prove.

Natural deduction also has assumptions that are discharged at a distance. A proof of an implication binds an assumption introduced several steps earlier, and a checker must track scopes. In the sequent calculus, the context is explicit in every rule and discharge is local: the right rule for implication simply moves A from the right side to the left in the premise. There is no bracket notation and no scope to maintain, which is why sequent derivations are easier to represent as data.

The cost is that sequent derivations are less natural to read. A human proof of a theorem does not usually proceed by systematically decomposing one connective at a time in a fixed order. Natural deduction tracks ordinary argumentative structure; the sequent calculus tracks the combinatorics of proof transformation. Each is the right tool for a different job.

Focused and uniform systems

A naive backward search applies any rule that matches, in any order, and the resulting tree is enormous. Modern presentations impose discipline. Focused systems distinguish invertible rules, which can be applied eagerly without loss, from non-invertible ones, which require a commitment, and they restrict the search to alternating phases: decompose the right side while invertible rules are available, then commit to one side of the sequent and apply only the non-invertible rules that belong to it, then decompose the results of that step. In the standard formulation the two phases are called asynchronous and synchronous, and the polarity of the connective being decomposed determines which phase its rules belong to.

The discipline is not a heuristic bolted onto the calculus. It is a theorem about which sequences of rule applications are complete, and it shrinks the search space without excluding any proof. Implementations of theorem provers and of logic programming languages rest on versions of it.

A second refinement is uniform proof, in which the identity rule is restricted to atomic formulas and the cut rule is eliminated entirely. Uniform derivations make the correspondence with computation sharper: a uniform proof of a hereditary Harrop formula is a computation, with the search itself acting as the interpreter. The same discipline of committing to one formula at a time is what makes the constraint solving in Elaboration predictable rather than combinatorial.

Where the rules stop being about logic

The sequent presentation generalises past connectives. Linear logic, introduced by Girard in 1987, removes the structural rules of weakening and contraction from the core and reintroduces them as explicit modalities, so that a formula can be used exactly once unless it is marked otherwise. The resulting calculus has a resource reading: a sequent is a statement about consuming inputs and producing outputs, and cut elimination becomes a statement about composing processes.

The same shift appears in type theory. A sequent-style typing derivation assigns types to a term while tracking the resources available, and the correspondence with natural deduction becomes a correspondence between two presentations of the same typing judgment. Which presentation a system uses is a design choice about how easy it is to prove metatheorems, not a choice about what the system can express.