Display Logic

  • Heinrich Wansing
Part of the Trends in Logic book series (TREN, volume 3)


The present chapter introduces display logic, DL a general proof-theoretic schema developed by Nuel Belnap, see [16], [17], [18]. A very general strong cut-elimination theorem for DL and M. Kracht’s syntactic and semantic characterization of the properly displayable modal and tense logics will be treated separately in Chapter 4. As will become evident, DL satisfies all the methodological requirements examined in Chapter 1. The following features may be seen as characteristic of DL:
  1. 1.

    DL extends the structural language of ordinary sequents in a natural way by introducing abstract operations on structures.

  2. 2.

    Antecedent (succedent) parts of a sequent s can be displayed as the entire antecedent (succedent) of a sequent s′ structurally equivalent to s.

  3. 3.

    The introduction rules for the logical operations exploit a certain duality between the antecedent and the succedent position of the sequent arrow. In particular, the introduction rules for the normal modal and tense logical operators rely on the ideas of residuation and Galois connection.

  4. 4.

    There may be more than just one family of structural operations.



Normal Form Logical Operation Structure Connective Structural Rule Residuated Pair 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer Science+Business Media Dordrecht 1998

Authors and Affiliations

  • Heinrich Wansing
    • 1
  1. 1.Institute of Logic and Philosophy of ScienceUniversity of LeipzigLeipzigGermany

Personalised recommendations