This thesis shows how Gabbay's general methodology of Labelled Deductive Systems can be used to reformulate and generalise a class of normal modal logics, and to develop types of modal reasoning for which axiomatizations are not definable. In particular, it shows how standard modal logics can be extended to enable reasoning about structures of actual worlds, where each world has an arbitrary associated modal theory. In the predicate case, the method gives rise to a uniform deductive procedure for arbitrary varying domain semantics.
In Part I, a family of labelled deductive systems called propositional Modal Labelled Deductive Systems (MLDS) 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. Propositional MLDSs 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. Moreover, they can be extended to classes of Kripke frames which are not-modally definable. A model-theoretic semantics, based on first- order logic, is provided and its equivalence to Kripke semantics for the case of normal propositional modal logic is shown, whenever the initial configuration is a single point. A sound and complete natural deduction style proof system is also described, which shows how different "local" modal theories can interact with each other. Unlike traditional proof systems for modal logics, this system is uniform in the sense that every deduction rule is applicable to (the generalisation of) each normal modal logic, and to "new" modal logics obtainable by considering non modally definable classes of frames.
Part II extends the formalism developed in Part I to the predicate case. The resulting predicate MLDSs thus combine standard predicate modal logics with extensions of the labelling algebra given in Part I, and allow syntactic reference to (possibly different) elements existing in different actual worlds. The proof system of Part I is extended with natural deduction rules for quantifiers, and with visa rules for reasoning about relationships between objects in different accessible worlds. This allows semantic distinctions between different nestings of quantifiers and modal operators to be preserved within the deductive system. The first-order model-theoretic semantics described in Part I is also adopted here - different types of varying domain semantics are expressed in terms of many sorted first-order classical theories. Results are given showing that the predicate MLDSs are sound and complete with respect to the proposed semantics and that the latter is equivalent to varying domain Kripke semantics for a sub-class of systems which use only singleton initial configurations.
pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.