Labelled Deduction

Origin. Gabbay (1990s). Labels encode semantic information. Worlds as labels in proof system. Relational atoms for accessibility. Uniform proof theory for modal logics.

Models. Formulas labelled by worlds: x:A. Relational formulas: Rxy. Proof rules manipulate labels. Embeds Kripke semantics into proofs.

Formalism.

Labelled formulas: x : A (A holds at world x) x R y (y accessible from x)

Sequents: G ; Γ ⊢ Δ G: relational context Γ, Δ: labelled formulas

Labelled rules for □: G ; Γ ⊢ y : A, Δ y fresh for G, Γ, Δ ──────────────────────────────────────────── □R G ; Γ ⊢ x : □A, Δ

G, x R y ; Γ, y : A ⊢ Δ ───────────────────────── □L G, x R y ; Γ, x : □A ⊢ Δ

Labelled rules for ◇: G, x R y ; Γ ⊢ y : A, Δ ────────────────────────── ◇R G, x R y ; Γ ⊢ x : ◇A, Δ

G, x R y ; Γ, y : A ⊢ Δ y fresh ───────────────────────────────────── ◇L G ; Γ, x : ◇A ⊢ Δ

Frame conditions as rules: Reflexivity: ─── (x R x added freely) Transitivity: x R y, y R z implies x R z Encoded as structural rules on G.

Benefits: Uniform treatment of different logics. Cut-elimination proofs simpler. Semantic intuition in proofs.

Symbols.

Symbol	Unicode	Name	Meaning
x : A	—	Label	A at world x
R	—	Accessibility	Relation
G	—	Graph	Relational context
;	—	Separator	Zones

Metatheory. Soundness/completeness wrt Kripke. Cut elimination. Modular: add frame rules for logic. Decidability preserved. Proof search as graph construction.

Applies to. Modal proof theory. Description logic reasoning. Hybrid logic. Tableau methods. Proof assistants for modal logic.

Limitations. Labels obscure proof structure. Frame rule permutation. Infinite label generation possible. Efficiency considerations.