Sequent¶
Package antecedent and succedent formula contexts into a two-sided formal judgment whose interpretation and admissible transformations are fixed by a proof calculus.
Core Idea¶
A sequent is a formal judgment with two formula contexts separated by a sequent sign:
Γ ⇒ Δ.
Γ is the antecedent and Δ the succedent. Each context is finite and may be empty. In a standard classical multiple-conclusion reading, if Γ = A₁, …, Aₘ and Δ = B₁, …, Bₙ, the sequent represents the conditional claim.
(A₁ ∧ … ∧ Aₘ) → (B₁ ∨ … ∨ Bₙ).
Thus all antecedents are taken together, while at least one succedent must hold. Gentzen's sequent calculi made these two contexts the objects transformed by logical and structural inference rules; a derivation is a tree whose nodes are sequents, not a single sequent enlarged into a proof.
Scope of Application¶
Sequents travel literally where formal deduction is organized around context-bearing judgments. Their habitats are proof-theoretic rather than metaphorical.
- Classical proof theory. Multiple-conclusion sequents make left/right connective rules systematic and expose structural rules for exchange, weakening, contraction, and cut.
- Intuitionistic and constructive logic. Single-succedent restrictions encode the discipline that a constructive derivation establishes one stated conclusion rather than an undifferentiated classical disjunction.
- Substructural logics. Linear, relevant, ordered, and related calculi change or remove structural rules, so formula order and multiplicity can record consumable resources or dependency discipline.
- Modal and nonclassical proof systems. Labelled, nested, display, hypersequent, and focused systems enrich the context or judgment shape while retaining sequent-based rule analysis.
- Automated proof search. A proof-search state is represented by one or more open sequents; backward application of an inference rule replaces a goal sequent with simpler premise sequents.
- Proof assistants and type theory. Interactive systems display local hypotheses and a target in a sequent-shaped goal state, even when the kernel's underlying formalism is dependent type theory rather than Gentzen's
LK. - Programming-language metatheory. Typing, evaluation, and logical-relation judgments often use context-turnstile-conclusion forms whose context management and rule inversion inherit sequent reasoning.
Clarity¶
Three levels must be named independently.
First, well-formedness is syntactic. The formulas must belong to the object language, the contexts must satisfy the calculus's shape constraints, and the separator must be the system's judgment form. A multiple-succedent expression may be well formed in LK but not in a single-succedent presentation of LJ.
Manages Complexity¶
Sequents externalize local proof obligations. Instead of treating a theorem as one opaque formula, a calculus distributes work across the formulas assumed, the formulas sought, and the connective currently exposed. A left rule explains how an assumed compound formula can be used; a right rule explains how a compound target can be established. This left/right symmetry makes proof search and metatheoretic induction inspectable.
Abstract Reasoning¶
Read a context by its structural operators. On the classical left, commas behave like conjunction; on the classical right, like disjunction. In a resource-sensitive calculus that reading changes, so first inspect which structural rules are available.
Move between object and judgment levels carefully. The connective → belongs to the object language; ⇒ separates contexts in a judgment; an external ⊢ may state derivability. A deduction theorem or soundness theorem may relate levels, but typography does not identify them.
Knowledge Transfer¶
Within logic, sequents transfer by literal mechanism. The formulas and rules change from classical to intuitionistic, modal, linear, labelled, or focused calculi, but the role package remains: declared contexts, a judgment separator, side-sensitive inference rules, and derivability as a tree of rule instances.
The same package appears in theorem-prover interfaces and typing judgments when local assumptions are displayed to the left of a turnstile and a target type or proposition to the right.
Relationships to Other Abstractions¶
Current abstraction Sequent Domain-specific
Parents (1) — more general patterns this builds on
-
Sequent presupposes Formal System Prime
Sequent strictly presupposes
prime:formal_system.
Hierarchy paths (2) — routes to 2 parentless roots
- Sequent → Formal System → Formalization → Representation → Abstraction
Neighborhood in Abstraction Space¶
Sequent sits in a sparse region of the domain-specific corpus (73rd percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.
Family — Formal Languages, Types & Programs (41 abstractions)
Nearest neighbors
- Formal Theory — 0.87
- Abstract Syntax Tree — 0.83
- Spider Diagram — 0.83
- Is-Ought Problem — 0.83
- Preferred label — 0.83
Computed from structural-signature embeddings · 2026-09-08