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: X ∘ Y ⊢ Z iff X ⊢ Y > Z iff Y ⊢ X > Z *X ⊢ Y iff X ⊢ *Y (in classical case)

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	Entails
∘	U+2218	Structure-and	Structural connective
>	—	Structure-implies	Structural implication
*	—	Structure-not	Structural negation
I	—	Unit	Structural unit
X, Y	—	Structures	Display structures

Metatheory. Display property enables modular cut-elimination. Belnap's conditions: sufficient for cut-elimination. Many logics displayable: modal, relevant, linear, bunched. Conservativity results. Subformula property for display calculi.

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. Structures complex — harder to read. Not all logics displayable. Belnap conditions must be verified. Proof search less direct. Learning curve from standard sequents. Display equivalences must be managed.