Item

Abstract

In this paper we discuss two {\em hybrid languages\/}, ${\cal L}(\forall)$ and ${\cal L}(\downarrow)$, and provide them with complete axiomatizations. Both languages combine features of modal and classical logic. Like modal languages, they contain modal operators and have a Kripke semantics. Unlike modal languages, in these systems it is possible to `label' states by using $\forall$ and $\downarrow$ to bind special {\em state variables\/}. This paper explores the consequences of hybridization for completeness. As we shall show, the challenge is to blend 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}(\downarrow)$ 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 analogs of the {\em Barcan\/} axioms coupled with a {\em modal theory of labeling\/}. In the case of ${\cal L}(\downarrow)$, on the other hand, although we can still formulate a theory of labeling, the Barcan analogs are not valid. We show how to overcome this difficulty by using $\mbox{{\it COV}}^{ \ \ast}$, an infinite collection of additional rules of proof which has been used in a number of investigations of extended modal logic.