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 | Γ, A ⊢ Δ | Π ⊢ A, Σ ─────────────────────────── com G | Γ, Π ⊢ Δ, Σ

Density rule (fuzzy): G | Γ ⊢ A, Δ | A, Π ⊢ Σ ────────────────────────── density 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
\|	—	Bar	Hypersequent separator
G	—	Component	Single sequent
com	—	Communication	Cross-component
⊢	U+22A2	Turnstile	Sequent

Metatheory. Cut elimination via parallel cuts. Decidability preserved. Modularity: add rules for different logics. Subformula property.

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

Limitations. External structure overhead. Rule design non-trivial. Some logics still resist. Complexity analysis harder.