Modal labelled deductive systems

Abstract

We present a formalization of propositional modal logic in the framework of Labelled Deductive Systems (LDS) in which modal theory is presented as a "configuration" of several "local actual worlds". We define a natural deduction style proof system for a propositional modal labelled deductive system (MLDS). We describe a model-theoretical semantics (based on first-order logic) and we show that the natural deduction proof system is sound and complete with respect to this semantics. We also show that the semantics given here is equivalent to Kripke semantics for a normal modal logic whenever the initial configuration is a single point. Finally we discuss how this logic can be extended to the predicate case, we sketch some natural deduction rules for quantifiers and we discuss how such rules solve certain problems associated with the nesting of quantifiers within the scope of modal operators.