Displaying modal logic (Q1817696)

Display Logic, proposed by N. Belnap, is an important refinement of Gentzen's sequent calculus to provide a uniform framework for sequential proof systems of modal and tense logics. This book is the first comprehensive introduction to Display Logic in the context of generalized Gentzen calculi. The author begins with reviewing several standard and non-standard sequential proof systems for modal and tense logics, with which Display Logic is motivated and developed not only from a formal proof-theoretical but also from a philosophical point of view. One of the main features of Display Logic is that in this framework a proof-theoretical characterization can be given for display sequent calculi enjoying a general strong cut-elimination property so as to cover many well-known modal and tense logics. On the base of such fundamental results for Display Logic, a proof-theoretic semantics for modal operators is introduced with which the functional completeness problem is discussed in a general setting. The proof-theoretic approach by Display Logic is also applied to several logical systems which have already been introduced in the literature by other means of formalization, such as labelled tableaux, structured consequence relation, and so on, including logic of constructive negation, some sub-intuitionistic logics, as well as first-order predicate modal logics. By displaying several logics in this way, the book provides also a survey of current proof-theoretical studies in non-classical logics which are closely related to computer science.