A Systematic Proof Theory for Several Modal Logics

The family of normal propositional modal logic systems are given a highly systematic organisation by their model theory. This model theory is generally given using Kripkean frame semantics, and it is systematic in the sense that for the most important systems we have a clean, exact correspondence between their constitutive axioms as they are usually given in a Hilbert style and conditions on the accessibility relation on frames. By contrast, the usual structural proof theory of modal logic, as given in Gentzen systems, is ad-hoc. While we can formulate several modal logics in the sequent calculus that enjoy cut-elimination, their formalisation arises through system-by-system fine tuning to ensure that the cut-elimination holds, and the correspondence to the formulation in the Hilbert systems becomes opaque. We introduce a systematic presentation for the systems K, D, M, and S4 in the Calculus of structures, a structural proof theory that enjoys the deep inference property. Because of t...

• Type: Conference
• Year: 2004
• Where: AIML
• Authors: Charles Stewart, Phiniki Stouppa
• Keywords: AIML 2004, AIML 2008, Modal Logic Systems, Modal Logics, Structural Proof Theory