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 ⊢ Δ, [G] ────────────────── □L Γ, □A ⊢ Δ, [G], [A ⊢]

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

Propagation rules: For S4 (reflexivity + transitivity): Γ, A ⊢ Δ, [G] ────────────────── (ref) Γ, □A ⊢ Δ, [G], [□A ⊢]

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

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

Symbols.

Symbol	Unicode	Name	Meaning
[ ]	—	Nesting	Nested sequent
⊢	U+22A2	Turnstile	Sequent
□	U+25A1	Box	Necessity
{}	—	Context	Position marker

Metatheory. Cut elimination via nested cuts. Decidability. Subformula property. Correspondence to Kripke semantics.

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

Limitations. Complex notation. Rule proliferation for different logics. Implementation challenges. Deep inference required.