Nested Sequents

Origin. Kashima (1994), Brünnler (2009). Tree-structured sequents. Nesting captures modal depth. Natural cut elimination. Proof theory for modal logics.

Models. Sequents can contain sequents. Tree structure mirrors Kripke frames. Internal and external formulas. Modular modal proof theory.

Formalism.

Nested sequent: Γ ⊢ Δ, [G₁], [G₂], ... where each [Gᵢ] is itself a nested sequent.

Tree structure: Root: main sequent. Children: nested sequents (in brackets). Modal depth = nesting depth.

Modal rules (K): Γ ⊢ Δ, [Π ⊢ Σ, A] ─────────────────── □R Γ ⊢ Δ, [Π ⊢ Σ], □A

Γ, □A ⊢ Δ, [Π, A ⊢ Σ] ───────────────────────── □L Γ, □A ⊢ Δ, [Π ⊢ Σ] □A is retained in the conclusion: contraction is built into the rule.

Deep inference: Rules apply at any depth. Context: Γ ⊢ Δ, [... [Π ⊢ Σ] ...]

Propagation rules (extensions): Γ, □A, A ⊢ Δ ───────────── (t) reflexivity Γ, □A ⊢ Δ

Γ, □A ⊢ Δ, [Π, □A ⊢ Σ] ────────────────────────── (4) transitivity Γ, □A ⊢ Δ, [Π ⊢ Σ] S4 = K + (t) + (4).

Structural rules: Nesting operations. Merge, split nested components.

Example (S5): All nested components share formulas. Flattenable to hypersequents.

Symbols.

Symbol	Unicode	Name	Meaning
[ ]	U+005B, U+005D	Square brackets / Nesting	Delimit a nested component, read as one step of accessibility
⊢	U+22A2	Turnstile	Sequent arrow within a component
□	U+25A1	Box / Necessity	The modality the nesting interprets
◇	U+25C7	Diamond / Possibility	Dual of □; a box in antecedent position behaves as ◇
Γ, Δ	U+0393, U+0394	Gamma, Delta	Antecedent and succedent at the root
Π, Σ	U+03A0, U+03A3	Pi, Sigma	Antecedent and succedent inside a nested component
{ }	—	Context hole	The position at which a deep rule is applied
G	—	Component	An arbitrary nested sequent
t, 4	—	Propagation rules	Reflexivity and transitivity as rules, not axioms

Metatheory. Kashima (1994) introduced nested sequents for tense logics; Brünnler (2009) and Poggiolesi (2009), the latter under the name tree-hypersequents, developed them for modal logic independently. Brünnler gave deep systems for every logic in the modal cube — K extended by any combination of D, T, B, 4 and 5 — with a syntactic cut elimination proof and admissibility of weakening and contraction, so the calculi are analytic and the structural rules are dispensable rather than merely restricted. Nested sequents are internal calculi: every nested sequent translates back into a formula of the modal language, the nesting read as a box, so a derivation reasons about formulas rather than about a semantic structure, which is what separates them from labelled calculi. Fitting (2012) showed prefixed tableaux and nested sequents are notational variants, and Fitting and Kuznets (2015) extracted constructive Craig interpolation from nested derivations for a range of modal logics.

Applies to. Modal logics (K, T, K4, S4, S5). Tense logics. Epistemic logic. Provability logic. Proof search.

Limitations. Coverage is not general. Brünnler's systems reach the modal cube, but there is no recipe carrying an arbitrary frame condition into a nested rule comparable to Negri's translation of geometric implications into labelled rules; grammar and path-axiom logics need propagation rules computed by automata (Tiu, Ianovski and Goré, 2012), and each extension is a fresh cut elimination proof rather than an instance of a theorem. Deep inference is constitutive of the format, not an option: rules apply at every position in the tree, so the number of applicable instances grows with the size of the sequent, and analyticity does not deliver termination — proof search still needs blocking or loop checking supplied from outside the calculus. Where the logic is flat the format is redundant: for S5 nesting beyond depth one is unnecessary and the calculus collapses to hypersequents.