A systematic sequent style proof theory for many important systems of normalmodal propositional logic based on Classical Propositional Logic (CPL) is presented. Philosophical, methodological, and computational aspects of the problem of Gentzenizing modal logic are discussed and a variant of Belnap's Display Logic is introduced. 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. It is shown that for all sequent systems under consideration: cut is admissible; the subformula property holds; and all connectives are uniquely characterized. Modal systems based on substructural subsystems of CPL are also addressed.
展开▼
