Modal Labelled Deductive Systems
Abstract
A family of labelled deductive systems called Modal Labelled
Deductive Systems (MLDS) is described. Modal theories are here defined as
(possibly singleton) structures of local actual worlds, called ``configurations''.
A model-theoretical semantics is given (based on first-order logic) and its
equivalence to Kripke semantics for normal modal logic is shown whenever the
initial configuration is a single actual world.
A natural deduction style proof system is defined for a wide family of propositional
MLDS and its soundness and completeness proved with respect to the given semantics.
Finally, an extension to the predicate case is sketched in terms of some
natural deduction rules for quantifiers showing also how this approach
could solve problems associated with the nesting of quantifiers within the scope of
modal operators.
This 99 page report is available over the Web in postscript form:
PMLDSreport.ps