Sequent¶

Package antecedent and succedent formula contexts into a two-sided formal judgment whose interpretation and admissible transformations are fixed by a proof calculus.

Version: v2 · 2026-08-30 · History
Domain-specific #: 2756
Origin domain: mathematical logic
Subdomain: proof theory
Aliases: Sequent judgment

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.^[1]^[2]

That classical formula is an interpretation, not a license to collapse every sequent into an implication formula. A calculus fixes what the contexts are—sequences, multisets, sets, or richer structures—how the sequent sign is read, which structural operations are available, and whether the succedent may contain many formulas, at most one, or some other constrained shape. Classical LK normally permits multiple succedents; intuitionistic LJ is commonly single-succedent; substructural calculi may make order or multiplicity semantically and proof-theoretically load-bearing by withholding exchange, weakening, or contraction.^[1]^[3]

The sequent is therefore a judgment form, not a truth bearer considered in isolation from a system. It can be well formed yet underivable. It can be semantically valid under an interpretation yet still require a completeness theorem before semantic validity guarantees derivability. Conversely, writing Γ ⇒ Δ does not itself exhibit a derivation. The structure packages a proof state—what is available on the left and what must be established on the right—so rules can expose, move, duplicate, discard, or decompose formulas in a controlled way.

Structural Signature¶

Sig role-phrases:

the object-language formulas — well-formed expressions supplied by a declared logical language
the antecedent context Γ — the finite, possibly empty collection of formulas placed to the left of the sequent sign
the succedent context Δ — the finite, possibly empty collection of formulas placed to the right, with its permitted cardinality fixed by the calculus
the sequent sign ⇒ or ⊢ — a syntactic separator whose judgmental meaning must be declared rather than inferred from typography alone
the context discipline — sequence, multiset, set, or structured-context conventions determining whether order and multiplicity matter
the logical rules — left and right rules that decompose a connective where it occurs in the judgment
the structural rules — exchange, weakening, contraction, and cut when admitted or admissible, governing contexts rather than one connective
the derivability relation — the calculus-relative status of whether a finite rule tree has the sequent as its end-sequent
the empty-side conventions — the unit cases that make empty antecedent, empty succedent, and the fully empty sequent meaningful

Recognition test. Identify the object language and calculus; locate two declared formula contexts and their separator; state whether each side may be empty and whether the right side may contain zero, one, or many formulas; state whether contexts are sequences, multisets, sets, or richer structures; and show which inference rules transform the judgment. Then keep three questions separate: is the expression a well-formed sequent, is it derivable in the calculus, and is it valid in the intended semantics? An implication formula, an informal premise list, or a completed proof tree fails this signature.

What It Is Not¶

Not an implication formula. In classical logic a sequent may correspond semantically to one implication with a conjunctive left and disjunctive right, but the contexts and structural rules live at the judgment level and need not be object-language connectives.
Not semantic entailment by notation alone. The model-theoretic relation Γ ⊨ A says every model of Γ satisfies A; a sequent is syntactic data whose validity and derivability must be assessed relative to specified semantics and rules.
Not a proof or derivation. A sequent is one node or end-judgment. A derivation is a finite rule-governed tree of sequents whose leaves are initial sequents and whose root is the end-sequent.^[2]
Not sequent calculus as a whole. The calculus is the formal system of initial sequents and inference rules; sequents are the expressions it transforms.
Not necessarily multiple-conclusion. Classical presentations often allow many formulas on the right, but intuitionistic and other calculi can restrict the succedent. The restriction is part of the system, not a failure to be a sequent.^[3]
Not necessarily an ordered pair of literal lists. Some calculi use sequences, others multisets or sets, and still others use structured contexts. The representation must preserve exactly the distinctions on which the rules depend.
Not automatically true because it is written. P ⇒ Q is a well-formed sequent even when no rule tree derives it and no intended semantics validates it.

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.^[1]
Intuitionistic and constructive logic. Single-succedent restrictions encode the discipline that a constructive derivation establishes one stated conclusion rather than an undifferentiated classical disjunction.^[3]
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.^[4]
Programming-language metatheory. Typing, evaluation, and logical-relation judgments often use context-turnstile-conclusion forms whose context management and rule inversion inherit sequent reasoning.

The abstraction is a poor fit when the left/right collections have no formal grammar, the separator has no rule-governed status, or an informal argument merely happens to list premises before a conclusion.

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.

Second, derivability is proof-theoretic. Write C ⊢ Γ ⇒ Δ, or another explicitly scoped notation, to say calculus C has a finite derivation whose end-sequent is Γ ⇒ Δ. The symbol inside the displayed sequent should not be allowed to do double duty silently as both separator and external derivability predicate.

Third, validity is semantic. In the classical reading, Γ ⇒ Δ is valid when every valuation making all formulas in Γ true makes at least one formula in Δ true. Soundness takes derivability to validity; completeness takes validity to derivability. Neither metatheorem is part of one bare sequent.

Empty contexts reveal the units. With empty antecedent, ⇒ Δ requires the disjunction of Δ without assumptions. With empty succedent, Γ ⇒ says the conjunction of Γ cannot all hold; in a proof system it often presents inconsistency or refutation. With both sides empty, ⇒ corresponds classically to ⊤ → ⊥ and is not valid in the ordinary consistent semantics.^[2] These are genuine judgment forms, not malformed punctuation.

Context representation also matters. If exchange is built into a multiset convention, A,B and B,A are already the same context. If contexts are sequences and exchange is a rule, they are different expressions connected by a derivation step. If contraction is absent, two occurrences of A need not be interchangeable with one. Clear sequent prose therefore declares the representation before drawing conclusions from commas.

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.^[3]

Backward proof search uses that structure as a decomposition engine. Start from an end-sequent, select a principal formula, and replace the goal with the premises of an applicable rule. Invertible rules can often be applied without backtracking; noninvertible choices mark genuine search branches. The context preserves side formulas while one connective is analyzed, preventing the proof state from losing assumptions or targets during decomposition.

Structural rules make another layer explicit. Weakening controls unused formulas, contraction controls duplicate use, exchange controls order, and cut composes a derivation of an intermediate formula with a derivation that uses it. Cut can compress proofs by naming lemmas, but cut elimination shows when such detours can be removed and is central to consistency, subformula, and proof-analysis results originating in Gentzen's work.^[1]^[3]

The representation also localizes failure. If proof search stalls, one can ask whether the goal is invalid, the calculus incomplete, a rule inapplicable because of an eigenvariable or context condition, or a strategic choice premature. Those diagnoses are sharper than “the proof does not work” because the open sequent records the exact assumptions and alternatives at the failure point.

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.

Invert rules to analyze goals. To understand Γ ⇒ Δ, A ∧ B, inspect the right-conjunction rule and the premise sequents it demands. To use A ∧ B on the left, inspect the left-conjunction rule. The principal formula's side determines the appropriate analysis.

Track structural permissions. Adding a formula by weakening, merging duplicates by contraction, or permuting by exchange is legitimate only when the calculus admits the relevant rule or bakes the equivalence into its context representation.

Use emptiness as information. An empty antecedent represents theoremhood without local assumptions; an empty succedent represents refutation of the entire left context. Empty contexts should trigger a semantic and proof-theoretic check, not deletion as if they were missing data.

Separate an open goal from its witness. A sequent states what a proof must establish. A derivation or proof term is the witness. This prevents circular explanations in which restating Γ ⇒ Δ is mistaken for proving it.

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. This is literal transfer only when the system gives the context and target formal status and operations preserve a declared judgment. Lean, for example, displays constants and hypotheses above ⊢ target; tactics transform that proof state and eventually construct a proof term checked by the kernel.^[4]

Beyond formal reasoning, “premises on the left, alternatives on the right” is usually analogy. A legal brief, decision table, or diagnostic workup may resemble a sequent visually, but without an object language, a context discipline, and mechanically checkable transformation rules it instantiates broader Deductive Reasoning or Formalization rather than Sequent.

The transferable parent lesson is to make assumptions and obligations explicit. The domain-specific residue is stronger: two contexts with calculus-relative structural behavior, logical left/right rules, empty-side units, and a distinction among well-formedness, derivability, and validity.

Examples¶

Canonical: derive commutativity of conjunction in a classical sequent calculus¶

Work in a standard LK presentation with multiset contexts. The target is

P ∧ Q ⇒ Q ∧ P.

Identity gives Q ⇒ Q and P ⇒ P. Left weakening supplies P,Q ⇒ Q and P,Q ⇒ P. The right rule for conjunction combines those two premise sequents into P,Q ⇒ Q ∧ P. The left rule for conjunction then packages the two antecedent formulas into P ∧ Q, yielding the target. The target sequent is not the proof: the rule tree just described is its derivation. Reading the end-sequent classically gives (P ∧ Q) → (Q ∧ P), but the derivation exposes how the left and right occurrences of conjunction are handled by different rules.^[2]

Mapped back: P ∧ Q is the antecedent context; Q ∧ P is the succedent context; ⇒ is the sequent sign; identity, weakening, ∧R, and ∧L are the structural and logical rules; the ordered rule tree establishes derivability; and the single formulas on each side satisfy this example's context discipline.

Applied / In Practice: a Lean proof state¶

Consider the Lean declaration theorem swap (p q : Prop) (h : p ∧ q) : q ∧ p := by .... At the start of tactic mode, Lean presents a local context containing p q : Prop and h : p ∧ q, followed by the target ⊢ q ∧ p. The tactic proof can close the goal with exact ⟨h.2, h.1⟩. The display is sequent-shaped: declarations and hypotheses form a context, the turnstile separates them from one target, and tactics replace open goals until none remain. Lean's kernel ultimately checks a proof term in dependent type theory, so the interface should not be mislabeled as Gentzen LK; it is a literal single-target judgment presentation with the same context-versus-obligation structure.^[4]

Mapped back: the local declarations and h are the antecedent context; q ∧ p is the single succedent target; ⊢ is the judgment separator; tactic steps are proof-state transformations; the completed term is the proof witness, deliberately distinguished from the displayed sequent-shaped goal.

Structural Tensions¶

T1: Context convenience versus structural meaning. Sets and multisets remove bookkeeping, while sequences expose order and duplicate occurrences. But choosing a representation can silently build exchange or contraction into equality of contexts. Diagnostic: Which distinctions between contexts are syntactic identities, and which require explicit structural rules?

T2: Multiple conclusions versus constructive commitment. A multiple-succedent classical sequent gives left/right symmetry and compact disjunctive alternatives; a single-succedent discipline records that one conclusion must be constructed. Diagnostic: Does the right-context cardinality match the logic being formalized, or has a classical interpretation been imported without justification?

T3: Syntactic derivability versus semantic validity. A rule tree provides a checkable witness, while semantics explains truth across models. Confusing the two hides the separate work of soundness and completeness. Diagnostic: Is the current claim about a derivation in a named calculus, validity in a named semantics, or a proved bridge between them?

T4: Local decomposition versus global lemma use. Analytic left/right rules expose subformulas and support proof search; cut composes proofs through an intermediate formula that may not appear in the end-sequent. Cut compresses reasoning but can obscure analytic structure. Diagnostic: Is the intermediate formula a useful abstraction boundary, and can the derivation be normalized when subformula visibility matters?

T5: Empty-side expressiveness versus reader error. Empty antecedents and succedents give exact unit cases for theoremhood and refutation, but readers often treat them as omitted text. Diagnostic: Has the calculus stated what each empty context means and whether the fully empty sequent is derivable or valid?

T6: Autonomy versus reduction. Formal System supplies the symbolic language and rules, and Deductive Reasoning supplies the broad truth-preserving activity, but neither identifies a two-context judgment with calculus-sensitive structural behavior. Diagnostic: If antecedent/succedent contexts, side-specific rules, and empty-side cases are removed, can the remaining parent concepts still recognize and repair a sequent proof state? If not, the domain node remains autonomous.

Structural–Framed Character¶

Sequent is mixed-structural. Its mathematical role is structurally exact, but literal recognition remains tied to formal languages and proof calculi.

Vocabulary travels (0.75). Context, turnstile, antecedent, succedent, derivability, cut, and structural rule recur across logic, type theory, and automated reasoning, but not as substrate-free ordinary-language roles.

Evaluative weight (0.0). A sequent may be derivable, underivable, valid, or invalid; the abstraction itself carries no social or normative approval.

Institutional origin (0.0). Particular calculi are designed conventions, but the correctness of a derivation follows from formal definitions rather than organizational authority.

Human-practice boundedness (0.0). Formal systems are human artifacts, yet once specified their sequents and rule applications are mechanically determined.

Import versus recognition (0.75). Proof theory and theorem proving recognize the same judgment structure. Calling an informal premises-and-conclusion layout a sequent normally imports a model without its defining rule system.

The portable skeleton is explicit assumptions paired with an obligation inside a rule-governed Formal System. Its character: strongly structural within mathematical logic, with enough specialist syntax and proof-theoretic machinery to remain domain-specific.

Structural Core vs. Domain Accent¶

This section explains why Sequent is a domain-specific abstraction rather than a prime.

What is skeletal. A system separates available conditions from an obligation, keeps both visible, and applies explicit transformations that preserve a target relation. Formal System carries the symbolic substrate, formation rules, and mechanical derivation. Deductive Reasoning carries the broader premise-to-conclusion discipline. Those patterns travel across domains without requiring Greek contexts or a turnstile.

What is domain-bound. A sequent requires object-language formulas, antecedent and succedent contexts, a calculus-defined separator, left/right rules, structural rules or their deliberate absence, and derivability as a rule tree. Multiple-conclusion disjunctive semantics, single-succedent restrictions, empty contexts, eigenvariable conditions, and cut are proof-theoretic commitments. Remove the two contexts and their calculus-sensitive behavior and the object is no longer a sequent; it becomes a generic conditional, inference, or task state.

Why this does not clear the prime bar. Outside logic and formal verification, the vocabulary transfers mainly as a diagrammatic metaphor. A decision memo can put conditions on the left and options on the right, but no mechanically specified left/right rules determine derivability. The general lesson—externalize assumptions and conclusions under rules—is already carried by Formal System and Deductive Reasoning. Sequent earns a separate node because those parents lose exactly the specialist information needed to diagnose exchange, contraction, empty-side, and derivability errors; its cross-domain reach nevertheless belongs to those parents rather than to the name itself.

Sequent strictly presupposes prime:formal_system. The object-language formulas, context formation, initial sequents, and inference rules exist only relative to a formal symbolic system. Formal System can exist without using sequents, while removing it makes a sequent's well-formedness and derivability undefined.

prime:deductive_reasoning is a close relation but not a proposed parent. Deduction is an activity or inferential relation; a sequent is a judgment object and can be underivable or invalid. Treating every sequent as a subtype of successful deduction would erase that boundary.

prime:proof_by_contradiction is a proof strategy that may be represented using an empty succedent or a falsity target, but most sequents do not encode indirect proof and the strategy does not supply the judgment form.

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

Show alternative path (1)

Neighborhood in Abstraction Space¶

Sequent sits in a sparse region of the domain-specific corpus (73^rd 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

Not to Be Confused With¶

Implication formula. An object-language formula such as (A ∧ B) → C may express a classical reading of a sequent. Tell: Are the commas and arrow connectives inside one formula, or are formulas arranged in calculus-governed contexts around a judgment separator?
Semantic entailment. Γ ⊨ A quantifies over interpretations or models. Tell: Is the claim established by model satisfaction, or by a syntactic expression and derivation rules?
Derivability relation. Γ ⊢_C A states that a proof exists in calculus C; a written sequent may be the object whose derivability is at issue. Tell: Is the turnstile separating the sequent's contexts or asserting the external existence of a derivation?
Proof or derivation. A proof is a rule-governed tree or proof term. Tell: Is there only an end-judgment, or is there a witness connecting initial judgments to it?
Sequent calculus. A calculus supplies initial sequents and inference rules. Tell: Is the item one judgment transformed by rules, or the entire rule system?
Natural-deduction judgment. Natural deduction also writes assumptions and a conclusion, but its introduction/elimination rules and discharge structure organize proofs differently. Tell: Are rule applications acting symmetrically on formulas in two contexts, or discharging assumptions in natural-deduction form?
Clause. A classical clause is a disjunction of literals and can correspond to a restricted sequent representation. Tell: Does the object retain two arbitrary formula contexts with declared rules, or only a normalized disjunction used by a resolution procedure?

References¶

[1] Gerhard Gentzen, “Untersuchungen über das logische Schließen I” and “II”, Mathematische Zeitschrift 39, 1934–1935, pp. 176–210 and 405–431. Introduces natural deduction and the LK/LJ sequent calculi, structural rules, and cut elimination. registry ↩a ↩b ↩c ↩d

[2] Open Logic Project, The Sequent Calculus, 2025 release, Chapter 10. Defines finite possibly empty antecedent and succedent sequences, the classical conjunction-to-disjunction reading, logical and structural rules, and derivations as trees of sequents. registry ↩a ↩b ↩c ↩d

[3] Sara Negri and Jan von Plato, Structural Proof Theory, Cambridge University Press, 2001. Authoritative treatment of sequent calculus, intuitionistic and classical variants, structural rules, proof analysis, and extensions. registry ↩a ↩b ↩c ↩d ↩e

[4] Lean Project, Theorem Proving in Lean 4: Tactics and Lean Language Reference: Tactic Proofs, accessed 2026-08-26. Official documentation for context-and-target goal displays, tactic-driven proof-state transformation, and proof terms. registry ↩a ↩b ↩c