Help Privacy Policy Disclaimer
  Advanced SearchBrowse




Journal Article

Hybrid Completeness


Tzakova,  Miroslava
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available

Blackburn, P., & Tzakova, M. (1998). Hybrid Completeness. Logic Journal of the IGPL, 6(4), 625-650.

Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-3841-4
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.