Sequent Calculi for Normal Modal Propositional Logics

Publisher Website
Google Scholar
Abstract
In this paper a systematic sequent-style proof theory for the most important systems of normal modal propositional logic based on classical propositional logic CPL is presented. After discussing philosophical, methodological, and computational aspects of the problem of Gentzenizing modal logic, a variant of Belnap's display logic is introduced. It is shown that within this proof theory the modal axiom schemes D, T, 4, 5, and B (and some others) can be captured by characteristic structural inference rules. For all sequent systems under consideration (i) cut is admissible, (ii) the subformula property holds, and (iii) all connectives are uniquely characterized. Also modal systems based on substructural subsystems of CPL are briefly dealt with.

This publication has 0 references indexed in Scilit: