Generalising Propositional Modal Logic Using Labelled Deductive Systems

Abstract

A family of labelled deductive systems called Propositional Modal Labelled Deductive (PMLD) systems is described. These logics combine the standard syntax of propositional modal logic with a simple subset of first-order predicate logic, called a labelling algebra, to allow syntactic reference to a Kripke-like structure of possible worlds. PMLD systems are a generalisation of normal propositional modal logic in that they facilitate reasoning about what is true at different points in a (possibly singleton) structure of actual worlds, called a configuration. A model-theoretic semantics (based on first-order logic) is provided and its equivalence to Kripke semantics for normal propositional modal logics is shown whenever the initial configuration is a single point. A sound and complete natural deduction style proof system is also described. Unlike traditional proof systems for modal logics, this system is uniform in that every deduction rule is applicable to (the generalisation of) each normal modal logic extension of K obtained by adding combinations of the axiom schemas T, 4,5, D and B