1 Foundations of Sequent Calculus

1.1 What Is a Sequent

1.1.1 Antecedent and Succedent

A sequent is a judgment written in the form \(\Gamma \vdash \Delta\). The collection \(\Gamma\) is called the antecedent and represents assumptions available in a proof. The collection \(\Delta\) is the succedent and represents what is to be established. In many standard presentations, the intended meaning is that if all formulas in \(\Gamma\) hold, then at least one formula in \(\Delta\) holds.

The two-sided structure is central: rather than embedding all information into a single formula, sequent calculus makes the assumption–goal split explicit. This organization supports rule sets that transform sequents while tracking logical dependence.

1.1.2 Sets, Multisets, and Sequences

The symbols \(\Gamma\) and \(\Delta\) are often treated as:

  • Sets, when order and multiplicity do not matter,
  • Multisets, when multiplicity matters but order still does not,
  • Sequences, when order matters.

Different sequent calculi choose different representations. Classical systems often allow structural rules that make order irrelevant (effectively behaving like multisets). Other variants restrict or omit structural rules so that multiplicity and/or order can become meaningful.

1.2 Core Intuition and Validity

1.2.1 Readings of \(\Gamma \vdash \Delta\)

A common semantic reading (especially in multi-succedent systems) is:

  • \(\Gamma \vdash \Delta\) means that under any interpretation, if every formula in \(\Gamma\) is true, then at least one formula in \(\Delta\) is true.

In single-succedent systems, where \(\Delta\) contains at most one formula, the judgment typically corresponds to ordinary entailment: \(\Gamma \vdash A\) means that from all assumptions in \(\Gamma\) one can derive \(A\).

Although the precise meaning depends on the variant (classical vs intuitionistic; single- vs multi-succedent), all variants follow the same proof-theoretic idea: sequents describe entailment-style goals with explicit left and right sides.

1.2.2 Multiple-Conclusion vs Single-Conclusion Views

  • Multiple-conclusion calculi permit \(\Delta\) to contain many formulas, reflecting the “at least one” nature of the right side.
  • Single-conclusion calculi restrict \(\Delta\) to one formula, aligning closely with entailment that produces a specific conclusion.

This distinction affects which structural and logical rules are used. It also influences how proof search proceeds: multi-succedent proofs can branch on which succedent formula is targeted, while single-succedent proofs often steer toward a unique goal formula.

1.3 Structural Rules

Structural rules regulate how assumptions and goals can be manipulated independently of the logical connectives. They embody properties like “you may reorder assumptions” or “you may add unused assumptions.”

1.3.1 Exchange

Exchange allows reordering of formulas within the antecedent or succedent (when those are treated as sequences rather than sets). If a calculus includes exchange, then the location of a formula in \(\Gamma\) or \(\Delta\) does not affect derivability.

Exchange is typically present in classical and intuitionistic sequent calculi based on multiset behavior. In substructural systems, exchange may be omitted so that order becomes informative.

1.3.2 Weakening

Weakening permits adding formulas to a side without changing provability. For instance, one can move from \(\Gamma \vdash \Delta\) to \(\Gamma, A \vdash \Delta\), or from \(\Gamma \vdash \Delta\) to \(\Gamma \vdash \Delta, A\), depending on the calculus.

Weakening expresses that having extra assumptions cannot hurt and extra available goals on the right does not reduce the power of a derivation. Omitting weakening yields systems where assumptions behave more like resources.

1.3.3 Contraction

Contraction collapses multiple occurrences of the same formula into one. For example, from \(\Gamma, A, A \vdash \Delta\) one may infer \(\Gamma, A \vdash \Delta\).

Contraction corresponds to the idea that repeated use of an assumption can be simulated by a single copy. Without contraction, the calculus distinguishes proofs that need multiple instances from those that do not, which again relates to resource-sensitive logics.

2 Inference Rules

Sequent calculi are defined by:

  1. Axioms (initial sequents),
  2. Logical rules that introduce or eliminate connectives and quantifiers,
  3. Structural rules (as applicable),
  4. A rule application discipline (often inductively defined derivations).

Rules are typically presented so that the conclusion sequent is derived from one or more premise sequents.

2.1 Axioms and Initial Sequents

2.1.1 Identity Axioms

The basic axiom is an identity principle: a formula entails itself. In sequent form, a typical identity axiom is: \[ A \vdash A. \] With structural rules, this extends to larger contexts, yielding derivations such as: \[ \Gamma, A \vdash \Delta, A \] (where exchange, weakening, and contraction determine how contexts can be rearranged or enlarged).

Identity axioms anchor the proof system and ensure that derivations can start without needing any logical structure.

2.1.2 Initial Sequents for Quantifiers

For quantifiers, initial sequents are typically formulated so that instantiation can begin. For example, identity remains available for quantified formulas, but derivations also need rule schemes that allow substitution of terms for bound variables under controlled conditions.

These starting points are usually combined with quantifier rules described below, rather than being a single axiom that directly handles arbitrary quantification.

2.2 Logical Rules for Connectives

Logical rules connect the syntactic structure of formulas with proof steps. They are designed so that introducing a connective on one side corresponds to distributing proof obligations across premises.

2.2.1 Rules for Conjunction

For a conjunction \(A \wedge B\), sequent rules reflect the idea that:

  • On the left (antecedent), a proof can use \(A \wedge B\) to obtain both \(A\) and \(B\).
  • On the right (succedent), establishing \(A \wedge B\) requires establishing both components.

Thus, rules typically separate left- and right-introduction patterns:

  • left-conjunction rules produce a premise where both conjuncts are added to \(\Gamma\),
  • right-conjunction rules split into premises that separately derive \(A\) and \(B\) in the relevant contexts.

2.2.2 Rules for Disjunction

For a disjunction \(A \vee B\), the patterns are dual to conjunction:

  • On the left, to use \(A \vee B\) one must be prepared for either case, producing premises that cover \(A\) and \(B\).
  • On the right, proving \(A \vee B\) can be accomplished by proving one side of the disjunction.

Accordingly, disjunction rules often have “branching” behavior on the left and “single choice” behavior on the right (or vice versa depending on single-/multi-succedent conventions).

2.2.3 Rules for Implication

Implication \(A \to B\) has a characteristic relation to entailment:

  • To use \(A \to B\) on the left, one typically attempts to establish \(A\), and then, with \(B\) as a consequence, continues toward the goal.
  • To prove \(A \to B\) on the right, one assumes \(A\) in the antecedent and derives \(B\).

Sequent calculus rules make this operational content explicit: implication rules embed a form of hypothesis management inside the derivation.

2.3 Rules for Negation

2.3.1 Left and Right Negation

Negation \(\neg A\) is handled by rules that link it to derivability of contradictions or to the impossibility of proving \(A\). In classical calculi, negation often interacts smoothly with structural rules like contraction and weakening.

In sequent form, a typical intuition is:

  • \(\neg A\) on the left can be viewed as a way to refute \(A\),
  • \(\neg A\) on the right can be viewed as establishing that \(A\) leads to inconsistency.

Exact formulations vary between classical and intuitionistic systems, but the left/right duality remains.

2.3.2 Interactions with Other Connectives

Negation rules are not isolated: they interact with rules for conjunction, disjunction, implication, and quantifiers through derivation patterns. For instance, De Morgan–style transformations and classical principles emerge at the proof-theoretic level via combinations of negation rules with other logical rules.

These interactions are particularly visible in cut elimination proofs, where negation introduction/elimination must be reconciled with the overall normalization strategy.

2.4 Quantifier Rules

Quantifier rules manage how formulas with \(\forall\) and \(\exists\) can be instantiated while respecting variable binding.

2.4.1 Universal Quantification (∀)

For a universal formula \(\forall x\, A(x)\):

  • On the left, one can typically instantiate with a term \(t\), adding \(A(t)\) to the antecedent.
  • On the right, proving \(\forall x\, A(x)\) requires proving \(A(x)\) for an arbitrary element, often represented by a special placeholder variable.

Such “arbitrary element” reasoning is implemented via constraints on eigenvariables (see below), ensuring soundness.

2.4.2 Existential Quantification (∃)

For an existential formula \(\exists x\, A(x)\):

  • On the right, one chooses a witness term \(t\) such that \(A(t)\) can be proven.
  • On the left, \(\exists x\, A(x)\) is used by assuming a generic instance \(A(x)\) (again with careful treatment of variables) to derive the target.

This yields the familiar asymmetry: existence on the right demands a particular example, while existence on the left supplies an assumed instance for further reasoning.

2.4.3 Eigenvariables and Substitution

A key technical device in quantifier rules is the use of eigenvariables: special variables introduced for rules that require “fresh” or “arbitrary” elements.

Eigenvariable conditions prevent illegitimate dependencies, such as using a variable that secretly depends on premises. In many standard presentations, eigenvariables must be chosen so they do not occur in certain parts of the sequent, thereby preserving soundness under substitution and renaming.

Substitution is the mechanism by which instantiation is performed. Rules ensure substitution does not capture variables incorrectly and respects binding structure.

3 Common Variants

Sequent calculus is not one monolithic system. Variants differ in the treatment of classical vs intuitionistic reasoning, the presence of the cut rule, and which structural principles are allowed.

3.1 Gentzen’s LK and LJ

3.1.1 Classical Sequent Calculus (LK)

LK is Gentzen’s sequent calculus for classical logic. It typically allows multiple formulas on the right side, and supports classical principles such as proof by contradiction as derivable behavior depending on the rule set.

LK includes standard structural rules (exchange, weakening, contraction), and its logical rules are crafted so that classical tautologies correspond to derivable sequents.

3.1.2 Intuitionistic Sequent Calculus (LJ)

LJ is Gentzen’s system for intuitionistic logic. The principal difference often lies in restricting the succedent to a single formula, which blocks some forms of classical reasoning that rely on multi-conclusion flexibility.

LJ aims to reflect intuitionistic entailment: from assumptions one derives a specific conclusion, rather than “one of many possible outcomes.” This restriction influences the shape of implication and negation proofs.

3.2 Single-Succedent vs Multi-Succedent Systems

As noted earlier, succedent size distinguishes entailment styles. Single-succedent systems correspond closely to intuitionistic logic, while multi-succedent systems naturally express disjunctive goals.

The choice also affects rule design: some logical rules for disjunction or implication can be implemented differently depending on whether \(\Delta\) contains several formulas or exactly one.

3.3 Cut Rule and Its Role

3.3.1 Cut Admissibility

The cut rule allows one to “splice” proofs: if one can derive \(\Gamma \vdash \Delta, A\) and also derive \(\Gamma', A \vdash \Delta'\), then one can derive a sequent that combines the contexts without that intermediate formula \(A\). This can shorten proofs but introduces a detour through a lemma.

A major metatheorem is cut admissibility: even if cut is not included as a primitive rule, it can be simulated. This is closely tied to cut elimination results.

3.3.2 When Cut Is Included Explicitly

Some presentations include cut explicitly to simplify proof exposition. Others omit it and rely on metatheorems to justify that nothing essential is lost. The inclusion affects proof search because cut can create non-goal-directed steps; removing it typically yields a more systematic normal form.

3.4 Substructural Sequent Calculi

3.4.1 Relevance and Linear Constraints (Overview)

Substructural calculi modify or remove structural rules to model logics where assumptions behave like resources or where relevance constraints apply. For example:

  • Omitting contraction corresponds to disallowing unrestricted reuse of assumptions.
  • Omitting weakening corresponds to requiring that every assumption be used.

These changes alter the operational meaning of derivations and create proof theories with distinct computational interpretations.

3.4.2 Omitting Structural Rules

When structural rules are removed, sequents can no longer be treated purely as sets or multisets. The calculus must track how often and where formulas occur, and proof rules become sensitive to these details.

The result is often a different proof complexity profile and different normalization behavior, though many metatheorems still have analogs in modified form.

4 Proof-Theoretic Properties

Proof-theoretic properties explain what the calculus guarantees and how derivations can be transformed.

4.1 Cut Elimination (Cut Reduction)

Cut elimination is the central normalization result: derivations that use cut can be transformed into derivations that do not.

4.1.1 Reduction Strategies

Reduction proofs show how to systematically replace a cut step with a sequence of cuts of lower “complexity,” eventually reaching a stage where no cuts remain.

Strategies typically proceed by induction on the structure of the cut formula and on derivation height. The details depend on whether structural rules are present and on whether the calculus is classical or intuitionistic.

4.1.2 Consequences of Cut Elimination

Cut elimination implies that:

  • Proofs can be normalized into a form where intermediate lemmas are not needed as cut bridges.
  • If a sequent is derivable, there is a derivation with the subformula property (in many settings).
  • The proof system becomes closely connected to computational interpretations, since normalization resembles evaluation steps.

It also supports decidability and complexity analysis in certain fragments of logic.

4.2 Soundness and Completeness

4.2.1 Soundness of Inference Rules

A calculus is sound if every derivation corresponds to a valid semantic entailment: whenever \(\Gamma \vdash \Delta\) is derivable, the semantic interpretation makes the entailment true.

Soundness is proven by verifying that each inference rule preserves validity, usually using the intended semantics for sequents.

4.2.2 Completeness Relative to Semantics

A calculus is complete if every semantic entailment has a corresponding derivation: if \(\Gamma\) semantically entails \(\Delta\), then \(\Gamma \vdash \Delta\) is derivable.

Completeness proofs often construct derivations using countermodel arguments, canonical models, or saturation-style techniques, depending on the logic and fragment.

4.3 Consistency and Normal Forms

4.3.1 Normal Proofs

A normal proof is a derivation with no reducible detours—typically those that would be eliminated by cut reduction or by administrative commuting conversions. In cut-free calculi, normal proofs often coincide with cut-free derivations that follow canonical rule ordering.

Normalization provides a canonical witness of provability and improves the predictability of proof search.

Cut elimination often aligns with backward reasoning: one works from goals toward axioms, applying rules that reduce the complexity of the target sequent.

Forward search can also be used, but it may generate larger structures before reaching closure. The relationship between normal forms and proof search strategy is a key computational aspect of sequent calculus.

4.4 Subformula Property

4.4.1 Why Normal Proofs Matter

In many standard systems, cut elimination yields the subformula property: every formula that appears in a cut-free derivation is a subformula of some formula in the original sequent (up to renaming).

This constraint is crucial for proof search: it bounds which formulas might need to be considered, preventing derivations from introducing “unrelated” lemmas.

4.4.2 Implications for Complexity

Because the set of relevant formulas is limited, decision procedures for fragments of logic can exploit this finiteness. Complexity depends strongly on the logical fragment, but the subformula property is often a starting point for deriving upper bounds.

In turn, it can clarify why some theorem-proving tasks are manageable while others remain difficult.

5 Proof Search and Computation

Sequent calculus is not only a theoretical foundation; it supports algorithmic reasoning.

5.1 Backward Reasoning in Sequent Calculus

5.1.1 Goal-Directed Rule Application

Backward reasoning begins with a target sequent and applies rules in reverse to generate premises closer to axioms. This style is well-suited to sequent calculi because many rules are naturally interpreted as decomposing goals:

  • For a conjunctive goal, break it into subgoals for each conjunct.
  • For an implication goal, introduce its antecedent as an assumption.

The approach tends to keep proof attempts focused on satisfying the succedent(s).

5.1.2 Termination Considerations

Termination is not guaranteed in full first-order logic due to quantifier instantiation possibilities. However, in well-chosen fragments or with proof-search heuristics, termination or practical efficiency can be achieved.

Termination can also depend on how eigenvariables are managed and on whether proof search uses depth limits or memoization to avoid repeating equivalent sequents.

5.2 Decision Procedures (High-Level)

5.2.1 Relation to Tableaux and Resolution

Sequent calculus proof search is related to other proof methods:

  • Tableaux correspond to branching expansions that attempt to refute or satisfy formulas via systematic case splitting.
  • Resolution operates on clauses and unification, often viewed as a specialized derivation system for certain normal forms.

Although the underlying representations differ, many search strategies can be transformed or compared through shared ideas like decomposition, branching, and saturation.

5.2.2 Proof Complexity Perspectives

The complexity of deciding provability depends on the logic’s expressiveness. In propositional fragments, cut-free proof search often aligns with structured expansions whose size can be bounded. For first-order logic, complexity typically grows substantially due to quantifier handling.

Studying these behaviors helps determine which fragments of sequent calculus-based reasoning are computationally tractable.

5.3 Extraction of Computational Content (Overview)

5.3.1 Curry–Howard Connections (General Idea)

The Curry–Howard correspondence relates proofs in certain logical systems to programs and types in computation. While the exact match depends on the chosen calculus and logic, the broad concept is that proof normalization corresponds to computation.

In settings where sequent calculus supports a suitable fragment, cut elimination and normal proof properties can be interpreted as producing executable content.

5.3.2 Programs from Proofs

Under Curry–Howard-like interpretations, a derivation can correspond to a program that transforms inputs into outputs, or that provides evidence for a specification.

Sequent calculus is helpful because its rule structure mirrors program constructors:

  • conjunction-like structure resembles pairing,
  • implication resembles functions,
  • quantifiers correspond to polymorphism or parametric reasoning in some accounts.

6 Examples and Worked Derivations

Examples illustrate how the rules operate and how derivations can be read.

6.1 Deriving a Simple Propositional Theorem

6.1.1 Typical Rule Sequencing

Consider a basic goal such as deriving \(A \vdash A \wedge A\) in a system where conjunction has right-introduction rules. A typical approach is:

  1. Start from identity \(A \vdash A\).
  2. Derive the two needed premises to build \(A \wedge A\) on the right.
  3. Apply the right-conjunction rule to combine them.

In a sequent calculus derivation, each step is a rule instance transforming one sequent into one or more simpler sequents until axioms are reached.

6.2 A Sample Quantified Proof

6.2.1 Using Quantifier Rules Carefully

For a formula like \(\forall x\, P(x) \vdash P(t)\) (where \(t\) is a term), a standard proof pattern uses the left \(\forall\)-rule:

  1. Instantiate the universally quantified assumption \(\forall x\, P(x)\) with the term \(t\).
  2. Use identity (or weakening) to conclude \(P(t)\).

This example highlights how substitution is the operational mechanism for universal elimination inside the sequent framework.

6.3 Demonstrating Cut Elimination in a Toy Case

6.3.1 Replacing a Cut Step

A toy scenario can show how a derivation using a lemma \(A\) can be replaced by a cut-free derivation. Suppose one has:

  • a derivation of \(\Gamma \vdash \Delta, A\),
  • and a derivation of \(\Gamma', A \vdash \Delta'\).

The cut rule combines these. Cut elimination replaces the use of the lemma \(A\) by pushing the proof of \(A\) upward and integrating it with the inference structure that used \(A\). In simple cases, the result can be visualized as directly substituting the derivation for \(A\) into the place where \(A\) was consumed, while adjusting rule applications to maintain correctness.

7 Relationship to Other Proof Systems

Sequent calculus fits into a larger landscape of proof representations.

7.1 Connection with Natural Deduction

7.1.1 Translating Between Systems (Overview)

Natural deduction typically uses introduction and elimination rules directly on formulas, maintaining assumptions as local contexts under discharge of hypotheses. Sequent calculus rearranges this into explicit left/right entailment goals.

Translations between systems exist:

  • a sequent derivation can be converted into a natural deduction proof by interpreting left contexts as active assumptions,
  • a natural deduction proof can be organized into sequent rules by tracking how introduction and elimination correspond to sequent steps.

The translation is complicated slightly by quantifier variable conditions and by whether the system is classical or intuitionistic.

7.2 Relation to Tableaux

7.2.1 Branching vs Sequent Expansion

Tableaux methods systematically build trees that represent possible ways formulas can fail or succeed, often using branching to reflect disjunction and negation structure.

Sequent calculus organizes branching differently: it expands sequents by applying rules that may have one premise or multiple premises, and it often keeps derivations more “balanced” in a proof-search sense.

Both approaches can be seen as proof search procedures with different bookkeeping, and they share underlying principles about decomposing logical structure.

7.3 Relation to Hilbert-Style Systems

7.3.1 Rule Granularity and Expressiveness

Hilbert-style systems use axiom schemas and modus ponens. They are compact but less directly goal-directed. Sequent calculus uses many small inference rules, which:

  • make the proof structure more transparent,
  • support systematic bottom-up proof construction,
  • facilitate metatheorems like cut elimination.

Expressiveness is comparable for standard logics, but sequent calculi often yield stronger proof-theoretic insights about normalization and subformula behavior.

7.4 Correspondence with Semantic Approaches

Semantic proof methods—such as model checking, canonical model construction, or semantic tableau—focus on interpretations rather than explicit syntactic steps.

Sequent calculus bridges syntax and semantics via soundness and completeness: derivability corresponds to semantic validity (or entailment). This link is strengthened by cut elimination, which can be viewed as separating essential inference content from auxiliary lemma usage.

8 Applications and Uses

8.1 Metatheory of Formal Logics

Sequent calculus is a standard tool for proving metatheorems about logical systems, including:

  • cut elimination,
  • consistency or conservativity results,
  • completeness for semantics,
  • interpolation properties in certain settings.

The explicit structure of sequents and the explicit separation of assumptions and goals make these proofs manageable and systematic.

8.2 Automated Theorem Proving (Overview)

8.2.1 Structure of Search in Sequent Calculi

Automated theorem provers often use search strategies that mimic proof construction in sequent-style systems:

  • goal-directed backward search,
  • simplification and normalization steps,
  • caching of previously encountered sequents.

Because sequents explicitly encode what is needed, the search can often be constrained by relevant subformulas, especially when cut-free search is targeted.

8.3 Educational Value for Proof Construction

For learners, sequent calculus can be easier to navigate than some other formalisms because:

  • each rule has a clear logical meaning tied to connectives and quantifiers,
  • the left/right structure reveals how assumptions contribute to goals,
  • proof search strategies align with common reasoning patterns.

Worked derivations provide concrete examples of how formal reasoning decomposes complex formulas.

8.4 Foundations for Studying Proof Normalization

Proof normalization studies how proofs can be transformed into canonical forms while preserving validity. Sequent calculus supplies the main framework in which normalization results are articulated via cut elimination and related reductions.

These foundations also inform computational interpretations, since normalization corresponds to computation steps in proof-as-program paradigms.