MPI-I-97-2-007

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.