max planck institut
informatik
informatik
MPI-I-97-2-007. July 1997, 33 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry
Abstract in LaTeX format:
In this paper we discuss two {\em hybrid languages\/}, ${\cal
L}(\forall)$ and ${\cal L}(\dn)$, and provide them with
axiomatisations which we prove complete. Both languages combine
features of modal and classical logic. Like modal languages, they
contain modal operators and have a Kripke semantics. In addition,
however, they contain {\em state variables\/} which can be explicitly
bound by the binders $\forall$ and $\downarrow^0$.
The primary purpose of this paper is to explore the consequences of
hybridisation for completeness theory. As we shall show, the
principle challenge is to find ways of blending the modal idea of {\em
canonical models\/} with the classical idea of {\em witnessed\/}
maximal consistent sets. The languages ${\cal L}(\forall)$ and ${\cal
L}(\dn)$ provide us with two extreme examples of the issues involved.
In the case of ${\cal L}(\forall)$, we can combine these ideas
relatively straightforwardly with the aid of the {\em Barcan\/} axioms
coupled with a {\em modal theory of labeling\/}. In the case of ${\cal
L}(\dn)$, on the other hand, although we can still formulate a theory
of labeling, the Barcan axioms are no longer valid. We show how this
difficulty may be overcome by making use of $\cov$, an infinite
collection of additional rules of inference which has been used in a
number of investigations of extended modal logic.
Acknowledgement:
References to related material:
| To download this research report, please select the type of document that fits best your needs. | Attachement Size(s): |
|---|---|
| 355 KBytes | |
| Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView | |
BibTeX