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, x R y ; Γ ⊢ 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	—	Labelled formula	A holds at world x
x R y	—	Relational atom	y is accessible from x
R	—	Accessibility	The frame relation, named in the calculus
G	—	Relational context	The graph of accessibility atoms
Γ, Δ	U+0393, U+0394	Greek capital gamma, delta	Antecedent and succedent of labelled formulas
;	U+003B	Semicolon	Separates the relational zone from the logical one
⊢	U+22A2	Turnstile	Sequent arrow
□	U+25A1	White square / Box	Necessity, introduced with a fresh label
◇	U+25C7	White diamond	Possibility, eliminated with a fresh label
x, y, z	—	Labels	Names for worlds, ranging over the frame
□R, □L	—	Right and left rules	Introduction on the succedent; on the antecedent
◇R, ◇L	—	Right and left rules	The dual pair
A	—	Schematic formula	An arbitrary formula of the object language

Metatheory. The claim the method rests on is modularity, and it is a theorem rather than a slogan. Simpson (1994) showed for natural deduction that adding a frame condition in Horn form as a rule on the relational context yields a system sound and complete for exactly the corresponding class of frames, with normalization proved once for the whole family. Negri (2005) sharpened this for sequent calculus: any frame condition expressible as a geometric implication converts mechanically into a rule under which weakening and contraction are height-preserving admissible and cut is admissible, so soundness, completeness and cut elimination are established uniformly rather than logic by logic. A failed proof search reads off a countermodel directly, since the relational context under construction is a Kripke frame, which is what makes the completeness argument constructive and gives decidability for those logics whose rules terminate under loop checking.

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

Limitations. The method reaches exactly the frame conditions expressible as geometric implications and no further, so the modal logics whose frames are not first-order definable fall outside the uniform treatment: the McKinsey axiom is not first-order definable at all, and the Löb axiom requires converse well-foundedness, which is not first-order either, so neither yields a rule of the standard form. The calculi are external rather than internal — sequents carry world labels and relational atoms, semantic vocabulary that occurs in no formula of the object language — so the subformula property holds only in a weakened version and the systems do not deliver a proof theory autonomous of the Kripke semantics, which is what the internal calculi (display, nested sequents, hypersequents) are for. Cut elimination does not yield decidability: transitivity rules generate labels without bound, and terminating proof search requires loop checking imposed from outside the calculus.