Sequent Calculus

Sequent calculus is a family of formal systems in logic whose inference rules operate on expressions called sequents, representing a relationship between assumptions and possible conclusions. A formal proof is organized as a tree of sequents rather than simply a sequence of formulas. Introduced by Gerhard Gentzen in work published in 1935, sequent calculus provides a central framework for proof theory, particularly the analysis of proof structure and the elimination of intermediate lemmas. Its best-known systems are LK for classical logic and LJ for intuitionistic logic. (geodesic.mathdoc.fr)

Sequents and their interpretation

A two-sided sequent is commonly written

where $\Gamma$, the antecedent, and $\Delta$, the succedent, are finite collections of formulas. Depending on the presentation, these collections are sequences, multisets, or sets. The symbol $\vdash$, sometimes replaced by $\Rightarrow$, separates the two contexts; it is not a connective within the formulas themselves. (cs.uwaterloo.ca)

Under classical logic, its semantic interpretation is that whenever every formula in $\Gamma$ is true, at least one formula in $\Delta$ is true. Thus $A,B\vdash C,D$ corresponds to the validity of

An empty antecedent imposes no assumptions, while an empty succedent means that the assumptions cannot all hold. Importantly, several formulas on the right do not mean that each is separately derivable: the context has a disjunctive interpretation. (cs.uwaterloo.ca)

In Gentzen’s standard formulation of intuitionistic logic, the succedent contains at most one formula. The sequent $\Gamma\vdash A$ then expresses derivability of a particular conclusion from the assumptions. This restriction, together with the corresponding logical rules, distinguishes LJ from LK. (cs.cmu.edu)

Logical and structural rules

Derivations begin with initial sequents, or axioms, typically $A\vdash A$, and proceed through rule applications. Many presentations allow contextual initial sequents $\Gamma,A\vdash A,\Delta$. Logical rules introduce a connective into a formula on either the left or the right. For example, familiar intuitionistic conjunction rules are

The first requires proofs of both conjuncts; the second permits a conjunctive assumption to be used through its components. (cl.cam.ac.uk)

Implication has a right-introduction rule

For example, starting with $A,B\vdash A$, conjunction-left gives $A\land B\vdash A$, and implication-right gives $\vdash(A\land B)\to A$. These rules cover propositional logic; first-order logic adds quantifier rules. Universal-right and existential-left require an appropriately fresh variable or parameter, preventing conclusions that depend on an unjustified choice of individual. (cl.cam.ac.uk)

Structural rules govern contexts independently of particular connectives:

• Exchange rearranges formulas.
• Weakening adds an unused formula.
• Contraction merges repeated occurrences.

In standard sequence-based LK these operations can be explicit. Set-based presentations or specially designed logical rules may incorporate their effects implicitly. Consequently, superficially different calculi can express the same consequence relation while producing different proof structures. (cl.cam.ac.uk)

Cut and cut elimination

The cut rule composes deductions through an intermediate formula:

Here $A$ is the cut formula. Cut formalizes the use of a lemma: one deduction establishes it, and another uses it to reach a further conclusion. Unlike connective rules read backward, cut can introduce an arbitrary formula not already present in the goal. (cs.cmu.edu)

Gentzen’s cut-elimination theorem, also called the Hauptsatz, states that every sequent derivable in LK or LJ has a derivation without cut. Equivalently, cut is admissible in the corresponding cut-free calculus: if its premises have cut-free proofs, so does its conclusion. Standard proofs reduce cuts to simpler formulas and move them upward through other inferences, using carefully organized inductions. Eliminating cuts may substantially increase proof length. (cs.cmu.edu)

Cut-free proofs have an important subformula property: in propositional systems, formulas occurring in the proof are subformulas of the end sequent. First-order formulations require qualifications for substitution instances of quantified formulas. This analytic structure supports consistency arguments and constrains proof search. Cut elimination concerns the rules of a specified calculus; adding arbitrary nonlogical axioms does not automatically preserve the same result. (cs.cmu.edu)

Metatheory and proof search

For standard classical calculi, soundness means that every derivable sequent is semantically valid, while completeness means that every valid sequent is derivable. These properties relate formal derivations to interpretations, whereas cut elimination concerns transformations between proofs. (cs.uwaterloo.ca)

In automated theorem proving, rules can be applied backward, replacing a goal sequent with simpler premises. Analytic calculi support terminating decision procedures for propositional fragments, but unrestricted first-order proof search need not terminate. Quantifier instantiation and repeated use of assumptions remain significant sources of search complexity. Focusing organizes rule applications into phases, reducing irrelevant choices without changing provability in suitable systems. (cs.cmu.edu)

Related systems and applications

Natural deduction organizes reasoning through introduction and elimination rules, often with discharged assumptions. Sequent calculus instead makes the surrounding assumptions explicit and distinguishes left from right rules. Cut elimination is closely related to proof normalization in natural deduction. (cs.cmu.edu)

Restricting structural rules produces resource-sensitive systems such as linear logic, where assumptions cannot generally be discarded or duplicated freely. Sequent calculi also provide foundations for type theory and computational interpretations of proofs. In proof assistants, they can support automated reasoning and proof tactics; Isabelle’s documented LK framework includes explicit sequent rules and tactics for using cuts to structure deductions into lemmas. (cs.cmu.edu)