Hypersequents

Origin. Avron (1987), Pottinger (1983). Generalize sequent calculus. Multiple sequents in parallel. Capture intermediate logics, fuzzy logics. Cut elimination for difficult systems.

Models. Hypersequent: disjunction of sequents. G | G': either G or G' provable. Communication rules between components. Modular proof theory.

Formalism.

Hypersequent: G₁ | G₂ | ... | Gₙ where each Gᵢ = Γᵢ ⊢ Δᵢ is a sequent.

Interpretation: G₁ | G₂ | ... | Gₙ means: at least one Gᵢ holds. External disjunction of sequents.

Structural rules: External weakening: G / G | H External contraction: G | H | H / G | H External exchange: G | H₁ | H₂ / G | H₂ | H₁

Communication rule (example): Gödel-Dummett (LC): G | Γ₁, Γ₂ ⊢ Δ G | Π₁, Π₂ ⊢ Σ ─────────────────────────────────── com G | Γ₁, Π₁ ⊢ Δ | Γ₂, Π₂ ⊢ Σ

Density rule (fuzzy): G | Γ ⊢ p, Δ | p, Π ⊢ Σ ────────────────────────── density (p a variable not in the conclusion) G | Γ, Π ⊢ Δ, Σ

Cut elimination: Hypersequent cut: G | Γ ⊢ A, Δ H | A, Π ⊢ Σ ─────────────────────────────── G | H | Γ, Π ⊢ Δ, Σ

Systems captured: Gödel-Dummett (LC) Łukasiewicz logic S5 modal logic Abelian logic

Symbols.

Symbol	Unicode	Name	Meaning
\|	U+007C	Vertical line / Hypersequent bar	Separates components; read as external disjunction
⊢	U+22A2	Turnstile	The sequent arrow inside one component
Γ, Δ	U+0393, U+0394	Gamma, Delta	Antecedent and succedent of a component
Π, Σ	U+03A0, U+03A3	Pi, Sigma	Antecedent and succedent of a second component
G	—	Side hypersequent	A component, or the unchanged remainder of the hypersequent
com	—	Communication rule	Exchanges material across two components
density	—	Density rule	Splits a component through a new formula
LC	—	Gödel–Dummett logic	Intermediate logic of linear Kripke frames; the motivating example

Metatheory. Pottinger (1983) and Avron (1987) introduced hypersequents independently. Avron's calculus for Gödel–Dummett logic LC adds the communication rule to LJ and admits cut elimination, giving an analytic presentation of a logic that has no cut-free ordinary sequent calculus; the same device yields cut-free calculi for S5. The theory was made systematic by Ciabattoni, Galatos and Terui (2008), who arranged substructural axioms into a hierarchy: every axiom in class N₂ converts algorithmically into an ordinary structural sequent rule preserving cut elimination, and every acyclic axiom in class P₃ converts into a hypersequent structural rule, after a completion step that restores cut elimination. Density elimination is the other characteristic result: Ciabattoni and Metcalfe (2008) eliminated the density rule proof-theoretically, and since density elimination yields standard completeness, hypersequents give syntactic proofs that fuzzy logics are complete for their intended semantics on [0,1].

Applies to. Intermediate logics. Fuzzy logics. Modal S5. Substructural logics. Proof theory of non-classical logics.

Limitations. A hypersequent adds exactly one dimension to the sequent format, and that dimension is a flat disjunction, so logics whose derivations need genuine tree structure — the modal logics presented by nested sequents, or intuitionistic modal logics — are out of reach. The conversion results stop at the third level of the substructural hierarchy: axioms above P₃ have no known algorithmic translation into hypersequent rules, and which modal frame conditions become hypersequent rules is itself a restricted class (Lahav 2013). Cut elimination does not deliver decidability; external contraction enlarges the search space and termination still requires loop checking imposed from outside the calculus. And the calculi are not canonical — inequivalent hypersequent systems exist for the same logic, so the format underdetermines the proof theory.