Display Logic

Origin. Belnap, "Display logic" (Journal of Philosophical Logic, 1982); also called the display calculus. Wansing (1998) and Goré (1998) developed the modal and substructural instances. Generalized sequent calculus with display property. Structures can be rearranged ("displayed"). Modular: add connectives by adding rules. Foundation for proof-theoretic analysis of many logics.

Models. Sequents with structural connectives. Standard sequent: Γ ⊢ Δ (lists of formulas). Display: structures with structural operations. Display property: any substructure can be made principal. Enables uniform proof theory for modal, relevant, substructural logics.

Formalism.

Display structures: X ::= A | X ∘ X | X > X | *X | I | ...

A: formula
∘: structural conjunction (corresponds to ∧ or ⊗)
: structural implication
*: structural negation
I: structural unit

Sequent: X ⊢ Y (structure entails structure)

Display property: For any sequent X ⊢ Y and substructure Z of X or Y, there exists equivalent sequent with Z principal (alone on one side).

Display equivalences (display postulates): X ∘ Y ⊢ Z iff X ⊢ Y > Z iff Y ⊢ X > Z *X ⊢ Y iff *Y ⊢ X X ⊢ *Y iff Y ⊢ *X Double negation: * is an involution in the classical case, so *(*X) and X are interderivable.

The postulates for * are contrapositive, not commuting: *X ⊢ Y and X ⊢ *Y are not interderivable. Read * as negation and the two say different things — *X ⊢ Y is X ∨ Y, while X ⊢ *Y is ¬X ∨ ¬Y. What does hold is the swap on the same side, *X ⊢ Y iff *Y ⊢ X, both reading X ∨ Y.

The two residuations of ∘ are written with a single > only because ∘ is being taken commutative here. A display calculus for a non-commutative substructural logic needs two residuals, X ⊢ Z < Y and Y ⊢ X > Z, and collapsing them silently assumes the exchange rule the calculus exists to control.

Logical rules: Introduce connectives from structural counterparts. ∧-R: X ⊢ A Y ⊢ B / X ∘ Y ⊢ A ∧ B

Cut-elimination: Display calculi satisfy cut-elimination under conditions. Belnap's conditions: C1-C8 guarantee cut-elimination.

Symbols.

Symbol	Unicode	Name	Meaning
⊢	U+22A2	Turnstile	Entailment between structures, not between formula lists
∘	U+2218	Ring operator / Structural conjunction	Reads as ∧ or ⊗ depending on the logic
>	U+003E	Greater-than / Structural implication	Right residual of ∘
<	U+003C	Less-than / Structural implication	Left residual of ∘, needed once exchange is dropped
*	U+002A	Asterisk / Structural negation	Contraposition operator; involutive in the classical case
∧	U+2227	Conjunction	The formula connective introduced from ∘
⊗	U+2297	Tensor	The substructural reading of ∘
I	—	Structural unit	Neutral element for ∘
X, Y, Z	—	Structure variables	Arbitrary display structures
C1–C8	—	Belnap's conditions	The eight conditions on rules that yield cut elimination

Metatheory. Belnap (1982) proved one cut elimination theorem for the whole family: any display calculus whose rules satisfy eight conditions C1–C8 — governing the shape of rules, the treatment of principal and parametric occurrences, and the substitutability of congruent parameters — admits cut elimination, and the proof is uniform in the logic. Cut elimination thereby becomes a matter of rule design, checkable by inspection, rather than a fresh induction for each system. The display property itself follows from the display postulates, which are residuations: the structural connectives form residuated pairs, so a display calculus is the proof theory of a residuated algebra, and adding a connective means adding its structural counterpart together with its residuals. Kracht (1996) gave an exact characterization for modal logic — a logic is properly displayable precisely when it is axiomatized by primitive formulas. Wansing (1998) and Goré (1998) constructed the modal, relevant and substructural instances.

Applies to. Proof theory of modal logics. Relevant and substructural logics. Linear logic proof theory. Modular proof system design. Cut-elimination proofs. Comparing logics proof-theoretically.

Limitations. Displayability is bounded and the bound is exact: by Kracht's theorem a modal logic is properly displayable precisely when it is axiomatized by primitive formulas, so outside that class the absence of a display calculus is a theorem rather than a gap in ingenuity. The display postulates are reversible and applicable without bound, so although cut-free derivations satisfy the subformula property the search space is infinite unless a normal form for display sequences is imposed from outside the calculus, and decidability must be established separately in every case. Belnap's condition on cut is delicate rather than routine — whether Valentini's cut elimination for provability logic survived the contraction rule was disputed for years before Goré and Ramanayake (2012) settled it. And every family of connectives needs its own structural counterparts and residuals, so combining logics multiplies structure instead of reusing it.