Displaying modal logic
type: Item
instance of: scholarly article
title: Displaying modal logic
zbMATH Open document ID: 0955.03006
published in: Trends in Logic -- Studia Logica Library
publication date: 2000-01-04T00:00:00Z
review text: 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.
reviewed by: Osamu Sonobe
Mathematics Subject Classification ID: 03-02
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 03B44
Mathematics Subject Classification ID: 03B47
Mathematics Subject Classification ID: 03B53
Mathematics Subject Classification ID: 03F03
zbMATH DE Number: 1382803
zbMATH Keywords: display logic
zbMATH Keywords: Gentzen-type sequent system
zbMATH Keywords: modal logic
zbMATH Keywords: tense logic
zbMATH Keywords: proof theoretic semantics
zbMATH Keywords: strong cut-elimination
zbMATH Keywords: functional completeness
zbMATH Keywords: constructive negation
author: Heinrich Wansing
MaRDI profile type: Publication
Recommended article: Displaying the modal logic of consistency
Recommended article: Q3099659
Recommended article: Q4700366
Recommended article: Displaying updates in logic
Recommended article: Q5688807
Recommended article: Bunched logics displayed
Recommended article: Sharing actions and attributes in modal action logic
Recommended article: Display calculi and other modal calculi: a comparison
Recommended article: Modeling and Using Context
Recommended article: Linear logic displayed
description: scientific article; zbMATH DE number 1382803