Translation of Hypersequents into Display Sequents
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  and A. Avron . 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 . 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 .
KeywordsModal Logic Proof System Structural Rule Sequent Calculus Introduction Rule
Unable to display preview. Download preview PDF.