sequents

A sequent is a formal expression used in logic to represent entailment. It consists of two sides: an antecedent, typically a multiset of formulas Γ placed on the left, and a succedent, a multiset Δ on the right. The sequent Γ ⊢ Δ is read as: from Γ, one can derive at least the formulas in Δ.

The sequent calculus is a proof system built around sequents. It was introduced by Gerhard Gentzen in the 1930s. A calculus has axioms (for example, A ⊢ A), structural rules such as weakening, contraction, and exchange, and logical rules that insert connectives on the left or right of the turnstile. A central rule is the cut, which composes proofs by introducing an intermediate formula. The celebrated cut-elimination theorem shows that every proof can be transformed into a cut-free one, ensuring a subformula property and aiding proof-theoretic analysis.

In classical sequent calculus, the succedent Δ may contain multiple formulas; in intuitionistic variants, Δ is restricted to at most one formula, reflecting a constructive notion of entailment.

An illustrative sequent is A, A→B ⊢ B, which expresses modus ponens in sequent form and is derivable via the left-implication and right rules.

Sequent calculus underpins many areas of proof theory, including automated theorem proving and formal verification. It has numerous variants for different logics, such as linear, modal, and relevance logics, as well as extensions like hypersequents and nested sequents.