Hybrid logic and its proof-theory (Q5961845)

This book grew out of nine research papers of the author, two of which are coauthored by T. Bolander and, respectively, V. de Paiva. The papers were converted into harmonically synchronized chapters of the book, which will certainly appeal to the reader. The topic of the book, hybrid logic, is an extension of modal logic originating from the work of the philosopher A. N. Prior. The fundamental and distinguishing characteristic of a hybrid logic is the concept of \textit{nominals,} i.e., propositional letters being true at exactly one state of the world. Hybrid logic was revitalized not so long ago, due to corresponding demands for adequately expressive systems in computer science and linguistics. Compared with the chapter on hybrid logic by \textit{C. Areces} and \textit{B. ten Cate} in [Handbook of modal logic. Studies in Logic and Practical Reasoning 3. Amsterdam: Elsevier (2007; Zbl 1114.03001)], the present book focuses on the proof theory of this logic. In contrast to ordinary modal logic, the proof theory of hybrid logic `behaves well'. This means that, in particular, key proof-theoretic principles, like inversion, normalization, or a suitable variant of the subformula property, can most often be established. The main reason for the good nature of hybrid logic regarding this is \textit{internalization,} i.e., capturing semantic features needed in proofs (e.g., worlds of a Kripke model) by expressive means of the object language (e.g., satisfaction operators associated with nominals). Internalization has already been discussed in the literature here and there, but Braüner gives a comprehensive account, systematically going through this matter. The book deals to a large extent with propositional versions of hybrid logic. First, the underlying language is introduced and discussed. Then the author develops the proof theory of propositional hybrid logic to the effect that natural deduction, Gentzen, and Hilbert-style axiom systems are considered. The next chapter is devoted to appropriate tableaux systems and decision procedures based thereon. A treatment of proof-theoretic functional completeness concludes the first half of the book. The proof theory of first-order and intensional first-order hybrid logic is the subject of the two following chapters. After returning to the propositional case, intuitionistic and paraconsistent hybrid logic are investigated. In the two last chapters of the book, the idea and the effect of internalization, see above, is treated thoroughly. There are a number of recurring storylines, giving the book a clear structure. The first and most important one is the author's preference of natural deduction systems, leading, among other things, to the above-mentioned principles for most of the logics considered here. (However, different approaches, such as axiom systems, are taken into account as well.) Another road map is soundness and completeness. The book contains lots of corresponding results, covering all important cases. A more special guideline is translation. The author spends a good deal of work on connecting hybrid languages to their natural (first-order) comparison languages and provides translations in this direction or that, if possible. The method is even extended to other contexts such as labelled deduction or the translation of proofs. The latter applies, in particular, when different natural deduction systems are compared. And anyway, comparing: it is very pleasing, since illuminating, how the existing literature is referred to in the author's work. A final point to be mentioned here is geometric theories, i.e., special first-order properties of the involved accessibility relation, by which many of the hybrid logics considered in the book can be extended `faithfully'. Undoubtedly, Braüner's monograph fills a gap in the hybrid logic literature in a desirable way.