Tsinghua University – University of Amsterdam Joint Research Centre for Logic

Expressivity and Inference in Hybrid Logic


Patrick Blackburn(Section for Philosophy and Science Studies, IKH, Roskilde


Beijing Time:  3:20 pm ~ 5:50 pm


on Tsinghua campus: to be announced

Zoom: to be announced

Course Description:

This course introduces hybrid logic, a form of modal logic in which it is possible to name worlds (or times, or computational states, or people) and reason about them. The course has three main goals. First, to make the ideas and intuitions that have guided the development of hybrid logic clear. Second, to prove some key results about hybrid inference and completeness. Third, to examine the ways in which hybrid logic is related to first-order logic.


Course Outline

Lecture 1: From modal to hybrid logic

We begin by revising the basic syntax and semantics of ordinary propositional modal logic, and then talk about topics like the standard translation, decidability, bisimulations, and what modal languages can say about frames. Next we create basic hybrid logic by adding nominals i, j, k, . . . and satisfaction operators @i, @j , @k, . . . and see what this changes. In this first lecture we concentrate on the new things we can express with the language; we’ll turn to the new things we can infer in Lectures 2 and 3.

Lecture 2: Hybrid inference

In this lecture we discuss hybrid inference, and how it differs from ordinary modal inference. We do so by defining tableau proof systems for the basic hybrid logic and for a number of stronger “pure hybrid logics” as well. We then look more closely at the crucial new tableau rule (with the help of the standard translation), and discuss why “pure hybrid logics” are well-behaved with respect to frame validity. As we will see, hybrid inference has a lot in common with first-order inference.

Lecture 3: Hybrid completeness

In this lecture we turn to hybrid axiom systems and completeness, and prove a general completeness result that covers basic hybrid logic, and all stronger “pure hybrid logics” as well. We don’t use the usual modal style canonical model construction to prove this. Instead we use a first-order style Henkin model construction, and show that it creates a “named model”. We discuss the new proof rules that make this possible, and show how they are related to the tableau rules we met in Lecture 2.

Lecture 4: Adding downarrow

The downarrow binder ↓ lets us “name the present state” by binding a nominal to it. We begin the lecture with give examples from temporal logic and computer science to see why this expressivity is useful. We then show that adding ↓ means giving up the finite model property and decidability. On the other hand, we also see that it simplifies the proof theory, and leads to general interpolation results.

Lecture 5: Arthur Prior and strong hybrid languages

In the final lecture we discuss the earliest (and strongest) form of hybrid logic, which was introduced by Arthur Prior in the mid 1960s. These languages let us “reverse” the standard translation: we can translate the first-order correspondence language back into hybrid logic. We will also meet the universal modality, make some links with description logic, and describe the hybrid expressivity hierarchy in more detail.

Background Knowledge

This course introduces hybrid logic without assuming that you have seen it before. Although makes contact with ideas from philosophy, computer science and linguistics, it is primarily a course in logic, and it is important that you understand the syntax and semantics of first-order logic, and propositional modal logic. A book which introduces both of these very clearly is Fitting and Mendohlson’s book First-order modal logic; it is also a great introduction to tableau systems for propositional modal logic.

If you have not encountered hybrid logic before, I suggest that you read my paper “Representation, reasoning, and relational structures: a hybrid logic manifesto”. It introduces several topics (nominals, @, tableau systems, ↓) that you will meet in the lectures, and has lots of examples.

During the lectures I will be introducing and working with such concepts as: the standard translation, bisimulations, disjoint unions, generated subframes, Lindenbaum’s lemma, canonical models, Henkin models, and undecidability via tiling games. I will be explaining all these things, but if any of them are totally new to you, you might find it useful to read a little about them in advance. All of them are discussed (in more detail than you will need for this course) in Modal Logic, by Blackburn, de Rijke and Venema, so you might find it helpful to glance at the basic definitions and examples there.

Slides and notes

  1. Slides and notes for the first lecture
  2. Slides and notes 1 and 2 for the second lecture
  3. Slides for the third lecture
  4. Slides for the fourth lecture
  5. Slides for the fifth lecture

Home Assignments

(submitted to chenq21@mails.tsinghua.edu.cn)

  1. The first assignment (due: before the class on Tuesday, June 28th) solution
  2. The second assignment (due: before the class on Wednesday, June 29th) solution
  3. The third assignment (due: before the class on Thursday, June 30th)
  4. Take-home exam (due: before 12:00 pm on Sunday, July 3rd)

General References

  • Areces, Carlos, and Balder ten Cate, “Hybrid logics”, in Handbook of Modal Logic, Blackburn, van Benthem and Wolter (editors), Elsevier, 821-868, 2007. An excellent technical survey of hybrid logic.
  • Blackburn, Patrick, “Representation, reasoning, and relational structures: a hybrid logic manifesto”, Logic Journal of the IGPL , vol 3, 339-365, 2000.
  • Blackburn, Patrick, Maarten De Rijke, and Yde Venema, Modal logic, Cambridge University Press, 2002.
  • Blackburn, Patrick, “Arthur Prior and Hybrid Logic”, Synthese, 150: 329-372, 2006.
  • Blackburn, Patrick, and Seligman, Jeremy, “Hybrid languages”, Journal of Logic, Language and Information, 4.3: 251-272, 1995.
  • Braüner, Torben, “Hybrid Logic”, The Stanford Encyclopedia of Philosophy (Spring 2022 Edition), Edward N. Zalta (editor), https://plato.stanford.edu/entries/logic-hybrid/.

An accessible overview of hybrid logic; useful references and historical background.

  • Braüner, Torben, Hybrid Logic and its Proof-Theory (Applied Logic Series: Volume37), Dordrecht-Heidelberg-Berlin-New York: Springer, 2011.

Useful monograph, focussing on hybrid natural deduction and sequent calculus.

  • Fitting, Melvin, and Richard Mendelsohn. First-order modal logic, Springer, 2012.

Excellent background material on modal logic, first-order logic, and tableaus.

  • Gargov, George, and Valentin Goranko, “Modal logic with names”, Journal of Philosophical Logic, 22.6: 607-636, 1993.
  • Passy, Solomon, and Tinko Tinchev, “An essay in combinatory dynamic logic”, Information and computation, 93.2: 263-332, 1991.