hide
Free keywords:
-
Abstract:
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.
