Patrick Blackburn

We show that basic hybridization (adding nominals and @ operators) makes it possible to give straightforward Henkin-style completeness proofs even when the modal logic being hybridized is higher-order. The key ideas are to add nominals as expressions of type t, and to extend to arbitrary types the way we interpret $@_i$ in propositional and first-order hybrid logic. This means: interpret $@_i\alpha _a$ , where $\alpha _a$ is an expression of any type $a$ , as an expression of type $a$ that rigidly returns the value that $\alpha_a$ receives at the i-world. The axiomatization and completeness proofs are generalizations of those found in propositional and first-order hybrid logic, and (as is usual inhybrid logic) we automatically obtain a wide range of completeness results for stronger logics and languages. Our approach is deliberately low-tech. We don’t, for example, make use of Montague’s intensional type s, or Fitting-style intensional models; we build, as simply as we can, hybrid logicover Henkin’s logic

In this paper we discuss two hybrid languages, ℒ and ℒ, 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 A and ↓ to bind special state variables.This paper explores the consequences of hybridization for completeness. As we shall show, the challenge is to blend the modal idea of canonical models with the classical idea of witnessed maximal consistent sets. The languages ℒ and ℒ provide us with two extreme examples of the issues involved. In the case of ℒ, we can combine these ideas relatively straightforwardly with the aid of analogs of the Barcan axioms coupled with a modal theory of labeling. In the case of ℒ, 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 COV*, an infinite collection of additional rules of proof which has been used in a number of investigations of extended modal logic

A modal logic is developed to deal with finite ordered binary trees a they are used in linguistics. A modal language is introduced with operators for the ‘mother of’, ‘first daughter of’ and ‘second daughter of’ relations together with their transitive reflexive closures. The relevant class of tree models is defined and three linguistic applications of this language are discussed: context free grammars, command relations, and trees decorated with feature structures. An axiomatic proof system is given for which completeness is shown with respect to the class of finite ordered binary trees. A number of decidability results follow

This paper sings a song — a song created by bringing together the work of four great names in the history of logic: Hans Reichenbach, Arthur Prior, Richard Montague, and Leon Henkin. Although the work of the first three of these authors have previously been combined, adding the ideas of Leon Henkin is the addition required to make the combination work at the logical level. But the present paper does not focus on the underlying technicalities rather it focusses on the underlying instruments, and the way they work together. We hope the reader will be tempted to sing a long.

In this paper we argue that hybrid logic is the deductive setting most natural for Kripke semantics. We do so by investigating hybrid axiomatics for a variety of systems, ranging from the basic hybrid language (a decidable system with the same complexity as orthodox propositional modal logic) to the strong Priorean language (which offers full first-order expressivity).We show that hybrid logic offers a genuinely first-order perspective on Kripke semantics: it is possible to define base logics which extend automatically to a wide variety of frame classes and to prove completeness using the Henkin method. In the weaker languages, this requires the use of non-orthodox rules. We discuss these rules in detail and prove non-eliminability and eliminability results. We also show how another type of rule, which reflects the structure of the strong Priorean language, can be employed to give an even wider coverage of frame classes. We show that this deductive apparatus gets progressively simpler as we work our way up the expressivity hierarchy, and conclude the paper by showing that the approach transfers to first-order hybrid logic.

Combining logics has become a rapidly expanding enterprise that is inspired mainly by concerns about modularity and the wish to join together tailor made logical tools into more powerful but still manageable ones. A natural question is whether it offers anything new over and above existing standard languages. By analysing a number of applications where combined logics arise, we argue that combined logics are a potentially valuable tool in applied logic, and that endorsements of standard languages often miss the point. Using the history of quantified modal logic as our main example, we also show that the use of combined structures and logics is a recurring theme in the analysis of existing logical systems

Este artigo canta uma canção — uma canção criada ao unir o trabalho de quatro grandes nomes na história da lógica: Hans Reichenbach, Arthur Prior, Richard Montague, e Leon Henkin. Embora a obra dos primeiros três desses autores tenha sido previamente combinada, acrescentar as ideias de Leon Henkin é o acréscimo requerido para fazer com que essa combinação funcione no nível lógico. Mas o presente trabalho não se concentra nas tecnicalidades subjacentes (que podem ser encontradas em Areces, Blackburn, Huertas, e Manzano [no prelo]), e sim nos instrumentos subjacentes e no modo como trabalham em conjunto. Esperamos que o leitor fique tentado a cantar junto. DOI:10.5007/1808-1711.2011v15n2p225

In this paper back-and-forth structures are applied to the semantics of natural language. Back-and-forth structures consist of an event structure and an interval structure communicating via a relational link; transitions in the one structure correspond to transitions in the other. Such entities enable us to view temporal constructions (such as tense, aspect, and temporal connectives) as methods of moving systematically between information sources. We illustrate this with a treatment of the English present perfect, and progressive aspect, that draws on ideas developed in Moens & Steedman (1988), and discuss the role of rich ontologies in formal semantics.

Hybrid languages have both modal and first-order characteristics: a Kripke semantics, and explicit variable binding apparatus. This paper motivates the development of hybrid languages, sketches their history, and examines the expressive power of three hybrid binders. We show that all three binders give rise to languages strictly weaker than the corresponding first-order language, that full first-order expressivity can be gained by adding the universal modality, and that all three binders can force the existence of infinite models and have undecidable satisfiability problems.

Craig's interpolation lemma (if φ → ψ is valid, then φ → θ and θ → ψ are valid, for θ a formula constructed using only primitive symbols which occur both in φ and ψ) fails for many propositional and first order modal logics. The interpolation property is often regarded as a sign of well-matched syntax and semantics. Hybrid logicians claim that modal logic is missing important syntactic machinery, namely tools for referring to worlds, and that adding such machinery solves many technical problems. The paper presents strong evidence for this claim by defining interpolation algorithms for both propositional and first order hybrid logic. These algorithms produce interpolants for the hybrid logic of every elementary class of frames satisfying the property that a frame is in the class if and only if all its point-generated subframes are in the class. In addition, on the class of all frames, the basic algorithm is conservative: on purely modal input it computes interpolants in which the hybrid syntactic machinery does not occur

The idea of combining logics, structures, and theories has recently been attracting interest in areas as diverse as constraint logic programming, theorem proving, verification, computational linguistics, artificial intelligence and indeed, various branches of logic itself. It would be an exaggeration to claim that these (scattered, and by-and-large independent) investigations have crystallized into an enterprise meriting the title "combined methods"; nonetheless, a number of interesting themes are emerging. This introduction notes some prominent ones and relates them to the papers in this special issue

Many of the formalisms used in Attribute Value grammar are notational variants of languages of propositional modal logic, and testing whether two Attribute Value Structures unify amounts to testing for modal satisfiability. In this paper we put this observation to work. We study the complexity of the satisfiability problem for nine modal languages which mirror different aspects of AVS description formalisms, including the ability to express re-entrancy, the ability to express generalisations, and the ability to express recursive constraints. Two main techniques are used: either Kripke models with desirable properties are constructed, or modalities are used to simulate fragments of Propositional Dynamic Logic. Further possibilities for the application of modal logic in computational linguistics are noted.

This paper is about a special version of PDL, proposed by Marcus Kracht, for reasoning about sibling ordered trees. It has four basic programs corresponding to the child, parent, left- and right-sibling relations in such trees. The original motivation for this language is rooted in the field of model-theoretic syntax. Motivated by recent developments in the area of semi-structured data, and, especially, in the field of query languages for XML (eXtensible Markup Language) documents, we revisit the language. This renewed interest comes with a special focus on complexity and expressivity aspects of the language, aspects that have so far largely been ignored. We survey and derive complexity results, and spend most of the paper on the most important open question concerning the language: what is its expressive power? We approach this question from two angles: Which first-order properties can be expressed? And which second-order properties? While we are still some way from definitive answers to these questions, we discuss two first-order fragments of the PDL language for ordered trees, and show how the language can be used to express some typical (second-order) problems, like the boolean circuit and the frontier problem.

Quantified hybrid logic is quantified modal logic extended with apparatus for naming states and asserting that a formula is true at a named state. While interpolation and Beth's definability theorem fail in a number of well-known quantified modal logics , their counterparts in quantified hybrid logic have these properties. These are special cases of the main result of the paper: the quantified hybrid logic of any class of frames definable in the bounded fragment of first-order logic has the interpolation property, irrespective of whether varying, constant, expanding, or contracting domains are assumed