Into the History and the Bibliography
The existing literature on hybrid languages is still relatively small and scattered, though it is growing fast. Here's a swift overview of what is available.
The original idea of using ``formulas as terms'' is due to Arthur Prior [Prior 1967] and [Prior 1968], who was influenced by unpublished work of C. A. Meredith. The idea played an important role in Prior's work, for it was the key to presenting a genuinely modal approach to temporal logic (one of Prior's main philosophical goals). Prior usually worked with strong hybrid languages, in which nominals could be bound with . The Stanford Encyclodepia of Philosophy has, among other things, a very interesting entry on Prior.
The ideas of Prior were later investigated by his then student Robert Bull. [Bull 1970] deserves to be far more widely read: it contains important technical ideas, and introduces a third sort of propositional variable: as well as using nominals to name points, Bull makes use of special ``course of history'' nominals to name paths through models. The paper is a (too long overlooked) classic of temporal logic. Like Prior, Bull worked with strong hybrid languages, in which nominals could be bound with .
The next step was taken by the Sofia School, who independently reinvented the idea of nominals and hybrid languages in the mid 1980s. The work of Passy and Tinchev [Passy and Tinchev 1985,Passy and Tinchev 1991] focusses on nominals in hybrid languages built over Propositional Dynamic Logic. Like Prior and Bull, they examined hybrid languages containing , but they also examined binder-free systems, thus initiating the trend towards weaker hybrid languages that dominates recent work.
Current work on hybrid logic concentrates on weaker systems, and two paths to developing weaker systems have been followed. First, you can simply drop the idea of binding nominals altogether, and just work with straight nominals (together perhaps with , and maybe other modalities; popular choices here are the universal modality and the difference operator). Early references on such approaches are [Gargov and Goranko 1993] and [Blackburn 1993b].
There has been a lot of recent work on such binder-free hybrid languages. For a start, in many interesting cases not only are they decidable, they are no more computationally complex than the underlying modal language. Recent complexity results concerning both standard and temporal basic hybrid logics over various classes of models (arbitrary, transitive, linear and branching) can be found in [Areces, Blackburn and Marx 1999].
The other route to weaker hybrid languages is not to drop binding altogether, but to restrict it. Several options have been explored, but definitely seems to be the most interesting: although the restriction to does not lead to decidability, turns out to be natural in many other respects. [Blackburn and Seligman 1998] and [Blackburn and Tzakova 1999] are basic references for hybrid logics containing , and an interesting discussion of as part of a stronger system can be found in [Goranko 1996].
The model-theoretic properties of hybrid logics containing (and many of their subfragments) were studied in [Areces, Blackburn and Marx 1998], where the basic hybrid logic containing is characterized as equivalent to the fragment of first-order logic that is invariant under the formation of generated submodels. This article also explores the interpolation property and Beth definability.
Although there has been a number of recent paper on proof theory for hybrid languages, the earliest work, that of Jerry Seligman, dates back almost a decade; see [Seligman 1991,Seligman 1997]. Seligman's work deals with -based systems, but many of the key ideas underlying hybrid deduction (in particular, the deductive significance of ) were first explored there, and they are still the only source we know of for discussion of natural deduction techniques for hybrid logics. Another series of proof-theoretically driven papers includes Beata Konikowska's proof systems for modal logics of information systems; see [Konikowska 1997a], [Konikowska 1987], and [Konikowska 1997b].
Recent proof theoretical papers include [Blackburn 1998], which presents -driven tableau and sequent rules, and discusses the link with Gabbay-style Hilbert rules; [Demri 1999], which presents a sequent system for nominal tense logic without ; [Demri and Goré 1999], which presents a display calculi for nominal tense logic enriched with the difference operator; and [Tzakova 1999], which presents a Fitting -style prefix calculus for a number of Hybrid languages.