Translation of Hypersequents into Display Sequents

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


As we have seen in Chapter 2, the study of nonclassical and modal logics has led to the development of many generalizations of the ordinary notion of sequent. In view of the diversity of these types of proof systems it becomes increasingly important to investigate their interrelations and their advantages and disadvantages. In this chapter, we shall consider the relation between display logic and the method of hypersequents independently introduced by G. Pottinger [134] and A. Avron [7]. It will be shown that hypersequents can be simulated by display sequents. Whereas hypersequents are finite sequences of ordinary sequents, display sequents are obtained by enriching the structural language of sequents, thus turning the antecedent and the succedent of a sequent into ‘Gentzen terms’, see also [41]. As Avron [12, p. 3] points out, “although a hypersequent is certainly a more complex data structure than an ordinary sequent, it is not much more complicated, and goes in fact just one step further”. The translation of hypersequents into display sequents illuminates how display sequents generalize ordinary sequents still further than hypersequents. In contradistinction to the application of hypersequents to modal logics, the modal display calculus comprises introduction rules for the modal and tense logical operators which can arguably be interpreted as meaning assignments; see Chapter 1. Therefore the translation of hypersequents into display sequents has something to recommend preferring display logic over the hypersequential formalism. We shall consider three case-studies of translating hypersequents into display sequents, corresponding with three different interpretations of hypersequents in [12].


Modal Logic Proof System Structural Rule Sequent Calculus Introduction Rule 
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