Fragmentary Memories

Carlos Areces

Based on work done in collaboration with Patrick Blackburn and Maarten Marx

who should actually be considered co-authors of this note.

Abstract

The modern approach to modal logics views them as particular fragmens of first-order logic, which enjoy nice properties like decidability, low complexity, interpolation, etc. If we take this idea at the heels, we can actually use modal logics to capture interesting fragments. In this note we will study one of such fragments, the set of formulas which are invariant under generated submodels. It will turn out to coincide precisely with a beautiful modal logic wich goes under the strange name of H(@, ↓).

Contents

1 Memories 2

2 Fragments 2

3 Hybrid logics 4 3.1 Translations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 3.2 Generated back-and-forth systems . . . . . . . . . . . . . . . . . 7 3.3 Hybrid bisimulations . . . . . . . . . . . . . . . . . . . . . . . . . 9 3.4 Expressivity over models . . . . . . . . . . . . . . . . . . . . . . . 12 3.5 Frames and completeness . . . . . . . . . . . . . . . . . . . . . . 13

4 ‘It’s a poor sort of memory that only works backwards’ 14 Those who know me will say that indeed my memory is fragmentary. But the title is not referring to that. It is just that this paper is about fragments and memories. Let’s start with the latter.

1 Memories

Now I am here, where ‘now’ is around March, 1999 and ‘here’ is ILLC, Amsterdam, The Netherlands. But less than three years ago I was finishing my first degree at the Computer Science Department in the University of Buenos Aires, Argentina. The topic of my thesis: Modal Logic and Software Engineering, in which I was making a case for the use of modal languages as specification languages not only in the very late stages of software development (Verification and Testing) but since the very begining (Design).

That was the culminating point of about two or three years of studying and working with modal logics^{1}. Again it’s not clear for me how I came to know the field. I think that I was already hooked into logic (“good old classical logic”), when somebody came to give a talk about software verification and I first heard about boxes and diamonds (was it Professor Ugo Montanari?).

In any case, the very appealing idea of taking simple propositional logic, adding only two new operators □ and ◇, and obtain such a beautiful landscape of possibilities shocked me.

Let me digress for a second to tell you some details about the Computer Science Department in Buenos Aires. First of all it is quite young, second it is quite small, third (at my time at least and I hope for many more years) it had a great director and excellent professors. Back to modal logics now.

So I was shocked with modal logics, and I wanted to know more about them. Well, I talked to friends. And me and my friends talked to the professors. And me and my friends and the professors talked to the director. And a course on Modal Logic was scheduled for the next semester. Because the department was young we could do these crazy things. Because it was small, organizing these things was easier. Because we had excellent people teaching us this was possible.

The professor in charge was Francisco Naishtat, the course was simply called “Modal Logic” and we were following Hughes and Cresswell’s book An Introduction to Modal Logic (yes, the 1968 edition).

2 Fragments

And we dived into modal systems: K, T, S4, …, the whole lot of them. Francisco Naishtat was an invited professor from the Philosophy Department (we had to “import” him because nobody at the Computer Science Department had ever worked with modal logics), and his point of view on Modal Logic was hence tuned to the classical meanings of Necessity and Possibility (only after we asked him we covered also some Temporal Systems, following Prior’s books mostly).

1There seems to be a lost fragment in my memory there, because even though I’ve been trying to, I cannot remember the exact year when I took my first course on modal logics.

We studied the deductive systems and we did (plenty of) completeness proofs. I still remember quite clearly how puzzled I was about some modal formulas “defining second order conditions” like Löb’s axiom. How comes that by just “modifying slightly” propositional logic you get to that!

After the first course was over I kept working on modal logics by myself. An then I came across Johan van Benthem’s “Correspondence Theory” chapter in the Handbook of Philosophical Logic [7] (a photocopy of the chapter I mean, I don’t think the library had a copy of the Handbook). And already in the third page I read

“After all, the clauses of the basic Kripke truth definition amount to a translation from modal formulas into classical ones … ”

That was the first time I thought of modal logics as fragments of first-order logic instead of extensions of propositional logic. The question about second order definability was explained away quickly in the following few pages of [5] by differentiating between model and frame validity.

Of course, this put a completely new map in my mind. For example, together with the modal logics course I’ve been studying Computability Theory where I learned about the undecidability of first order satisfiability; under that light modal logics appeared as ways to restrict the set of first-order theorems to achieve decidability.

After this adjustment, it didn’t take too long for me to get acquainted with things like the standard translation and the characterization of the modal fragment in terms of bisimulations. I simply got and read every article from van Benthem (and the Dutch group in general) I could lay my hands on. It was really like changing your old black and white TV for a new color one. Things were the same, but everything looked so different!

And FRAGMENTS was the name of the game: modal logics ARE ways of defining attractive subsets of full first-order logic (or even extensions like first-order plus fix points).

Going through the pages of van Benthem’s “Modal Logic and Classical Logic” (cf. [4]) is to find the fragment-theme once and again. In Chapter XV a very modal like fragment of first-order logic is introduced: the set of formulas which are invariant under generated subframes.

In the next section I will introduce hybrid logics, which are modal logics with the ability to “name” worlds. The name “hybrid logics” is motivated because things that might look like terms (specifically, constants and variables) are used instead as formulas. They will turn to be the modal counterpart of the generated subframe invariant fragment of first-order logic. Things will be clearer soon (I hope!).

3 Hybrid logics

In the following sections things will start getting technical (continue only at your own risk!). If you want a quick resume of it all, we’ll just introduce a new logic and identify the first-order fragment it corresponds to. That’s it, and you are free to skip the next bunch of pages. But I had to tell you that it is a beautiful fragment! It will characterize a “very modal” fragment of firstorder logic: The set of first-order formulas which are invariant under generated submodels.

The following sections draw heavily on work I had (and I’m having) the pleasure to share with Patrick Blackburn and Maarten Marx (see [2] for the complete article). If you find mistakes below they are mine; if you find wonderful ideas they are probably theirs.

The first step to obtain a hybrid language is the following: extend the set of propositional letters PROP with a set NOM = {i_{1}, i_{2}, …} of nominals and a set WVAR = {x_{1}, x_{2}, …} of world variables. Then the well-formed formulas of the hybrid language are

φ := a | ¬φ | φ ∧ φ′ | □φ | ↓x_{j}.φ | @_{s}φ

where a ∈ ATOM = PROP ∪ NOM ∪ WVAR, x_{j} ∈ WVAR and s ∈ WSYM = NOM ∪ WVAR.

Why can we treat terms as formulas? Because modal formulas are evaluated locally (i.e., evaluation takes place at a particular point in the model). Then we can interpreted terms as the question “Does this term represent the actual world?” This is exactly how nominals and world variables will be understood. Furthermore, the ↓ binder lets us give a generic name to the actual world (compare to the English phrase “Let’s say that somebody, say John … ”) while the @ operator let us come back to a named world (“Well, this John, he … ”).

Formally, a hybrid model 𝔐 is a Kripke model 𝔐 = ⟨M, R, V ⟩ where V : PROP ∪ NOM → P ow(M) is such that for all nominals i ∈ NOM, V (i) is a singleton subset of M. We also need the notion of an assignment g : WVAR → M to handle variables. The x_{i}-variant g_{m}^{i} of g is defined as g_{m}^{i}(x_{j}) = g(x_{j}) for j ≠ i and g_{m}^{i}(x_{i}) = m.

Let 𝔐 = ⟨M, R, V ⟩ be a model, m ∈ M, and g an assignment. For any atom a, let [V, g](a) = {g(a)} if a is a world variable, and V (a) otherwise. Then the forcing relation is defined as follows

𝔐, g, m ⊩ a  iff m ∈ [V, g](a), a ∈ ATOM
𝔐, g, m ⊩↓x_{i}.φ iff 𝔐, g_{m}^{i}, m ⊩ φ
𝔐, g, m ⊩ @_{s}φ iff 𝔐, g, m′ ⊩ φ, where [V, g](s) = {m′}, s ∈ WSYM.

For the other operators the standard definitions apply.

It is perhaps interesting to play a little with the new operators. ↓ is specially powerful (and it is the main culprit of the undecidability of H(↓, @)). As we hinted above, using ↓ we plant a flag in the actual word which we can then use as a reference point “further on” in the formula. A wonderful tiny example is ↓x.□¬x, which when evaluated on frames forces the accessibility relation to be irreflexive. The intuitive reading is: “Say that this world is called x then every accessible worlds should not be x”, banning all reflexive arrows.

Axiomatizations, soundness and completeness for this language which is called H(↓, @) has already been established in [6]. But we are now interested in discovering which is the first-order fragment corresponding to H(↓, @).

We begin by providing a syntactic characterization. In particular, we shall first extend the standard translation (cf. [4]) to H(↓, @). The range of this translation will lie in certain bounded fragment of the first-order language, and we will define a reverse translation HT which maps this bounded fragment back into the hybrid language (in both cases preserving truth). This established a first full correspondence.

But how are these languages characterized semantically? H(↓, @) is a genuine hybrid also at this level as there are two obvious ways to proceed. The first is essentially first-order: we could look for a weaker notion of Ehrenfeucht-Fraïssé game [8]. The second is essentially modal: we could try defining a stronger notion of bisimulation. Both yield natural notions of equivalence between models, and by relating them (and drawing on our syntactic characterization) we can provide a detailed picture of what H(↓, @) offers.

3.1 Translations

We focus on two kinds of signature for first-order logic with equality. First, we have modal signatures (familiar from modal correspondence theory [4]) which consist of one binary predicate R, countably many unary predicates, and no constant symbols. It will be convenient to make the set of first-order variables at our disposal explicit in the signature thus, a modal signature has the form ⟨{R}∪ UN-REL, {}, VAR⟩. A hybrid signature is an expansion of the modal signature with countably many constant symbols, thus hybrid signatures have the form ⟨{R} ∪ UN-REL, CONS, VAR⟩. Note that any hybrid model 𝔐 = ⟨M, R, V ⟩ can be regarded as a first-order model with domain M, for the accessibility relation R can be used to interpret the binary predicate R, unary predicates can be interpreted by the subsets V assigns to propositional variables, and constants (if any) can be interpreted by the worlds that nominals name. So we let the context determine whether we are working with first-order or hybrid models, and continue to use the notation 𝔐 = ⟨M, R, V ⟩.

We first extend the standard translation to H(↓, @). The function ST from the hybrid language over ⟨PROP, NOM, WVAR⟩ into first-order logic over the signature ⟨{R} ∪ {P_{j} | p_{j} ∈ PROP}, NOM, WVAR ∪ {x, y}⟩ is defined by mutual recursion between two functions ST_{x} and ST_{y}. Recall that φ[x/y] means “replace all free instances of x in φ by y.”

ST_{x}(p_{j})  = P_{j}(x), p_{j} ∈ PROP. ST_{y}(p_{j})  = P_{j}(y), p_{j} ∈ PROP.
ST_{x}(i_{j})  = x = i_{j}, i_{j} ∈ NOM.  ST_{y}(i_{j})  = y = i_{j}, i_{j} ∈ NOM.
ST_{x}(x_{j})  = x = x_{j}, x_{j} ∈ WVAR. ST_{y}(x_{j})  = y = x_{j}, x_{j} ∈ WVAR.
ST_{x}(¬φ)  = ¬ST_{x}(φ).  ST_{y}(¬φ)  = ¬ST_{y}(φ).
ST_{x}(φ ∧ ψ) = ST_{x}(φ) ∧ ST_{x}(ψ). ST_{y}(φ ∧ ψ) = ST_{y}(φ) ∧ ST_{y}(ψ).
ST_{x}(◇φ) = ∃y.(Rxy ∧ ST_{y}(φ)). ST_{y}(◇φ) = ∃x.(Ryx ∧ ST_{x}(φ)).
ST_{x}(↓x_{j}.φ) = (ST_{x}(φ))[x_{j}/x].  ST_{y}(↓x_{j}.φ) = (ST_{y}(φ))[x_{j}/y].
ST_{x}(@_{s}φ) = (ST_{x}(φ))[x/s].  ST_{y}(@_{s}φ) = (ST_{y}(φ))[y/s].

For m an element in the domain of a given model 𝔐 we will often write ST_{m}(φ) as shorthand for ST_{x}(φ)[m].

Of course, we took care that the translation preserve truth of formulas.

Proposition 3.1 (ST Preserves Truth) Let φ be a hybrid formula, then for all hybrid models 𝔐, m ∈ M and assignments g, 𝔐, g, m ⊩ φ iff 𝔐 ⊧ ST_{m}(φ)[g].

Proof. A straightforward extension of the induction familiar from ordinary modal logics. The only cases which are new are ST_{x}(↓ x_{j}.φ) and ST_{x}(@_{s}φ). 𝔐, g, m ⊩↓ x_{j}.φ, iff 𝔐, g_{m}^{x_{j}}, m ⊩ φ. By inductive hypothesis this is the case if and only if 𝔐 ⊧ ST_{m}(φ)[g_{m}^{x_{j}}], iff 𝔐 ⊧ (ST_{m}(φ))[x_{j}/x] [g]. The argument for ST_{x}(@_{s}φ) is similar. qed

Now for the interesting question: what is the range of ST? In fact it belongs to a bounded fragment of first-order logic. It was Professor van Benthem who suggested this connection with the bounded fragment. I cannot avoid digressing again

It was after Maarten Marx presented in a seminar our first ideas about the Hybrid Language and its semantics characterization in terms of bisimulations (next section!). Johan van Benthem was attending the talk, and he seemed busy going through a batch of articles while half listening to Maarten (or so I thought). When the time for questions and discussion arrived, I discovered that somehow he had managed to understand the key ideas without effort. Furthermore, he had already made the connection with the bounded fragment introduced in [4]. He invited us for a short meeting afterwards to put things in order. Just in case we missed any detail he sent us a mail the same night with the main points of the proof of the syntactic characterization. And I would bet, he also finished reading the big bunch of paper he was reviewing in the afternoon!

The bounded fragment now. Given the first-order signature ⟨{R} ∪ UN-REL, CONS, VAR⟩ we define the bounded fragment as the set of formulas obtained as:

φ = Rtt′ | P_{j}t | t = t′ | ¬φ | φ ∧ φ′ | ∃x_{i}.(Rtx_{i} ∧ φ) (for x_{i} ≠ t)^{2}

2The side-condition on the generation of existentially quantified formulas is crucial: it prevents sentences like ∃x.(Rxx∧x = x) (which are not preserved under generated submodels)

from falling into the fragment.

where x_{i} ∈ VAR and t, t′ ∈ VAR ∪ CONS.

Clearly ST maps hybrid formulas into formulas in the bounded fragment. Crucially, however, we can also translate the bounded fragment into H(↓, @). The translation HT from the bounded fragment over ⟨{R} ∪ UN-REL, CONS, VAR⟩ into the hybrid language over ⟨UN-REL, CONS, VAR⟩ is defined as follows:

\begin{aligned}HT (Rtt′) & = & @_{t}◇t′. \\ HT (P_{j}t) & = & @_{t}p_{j}. \\ HT (t = t′) & = & @_{t}t′. \\ HT (¬φ) & = & ¬HT (φ). \\ HT (φ ∧ ψ) & = & HT (φ) ∧ HT (ψ). \\ HT (∃v.(Rtv ∧ φ)) & = & @_{t}◇ ↓v.HT (φ). \end{aligned}

By construction, HT (φ) is a hybrid formula, but furthermore it is a boolean combination of @-formulas (formulas whose main operator is @). We can now prove the following strong truth preservation result. Recall that 𝔐, g ⊩ ϕ, abbreviates “(for all m ∈ M) 𝔐, g, m ⊩ ϕ”.

Proposition 3.2 (HT Preserves Truth) Let φ be a bounded formula. Then for every first-order model 𝔐 and for every assignment g, 𝔐 ⊧ φ[g] iff 𝔐, g ⊩ HT (φ).

Proof. The proof uses the following fact about boolean combination of @- formulas. Let φ be such a formula, let 𝔐 and g be given and let m ∈ M. Then 𝔐, g, m ⊩ φ iff 𝔐, g ⊩ φ.

The proof is by induction and there is only one interesting case: HT (∃v.(Rtv ∧ φ)). Now 𝔐 ⊧ ∃v.(Rtv ∧ φ)[g] iff 𝔐 ⊧ (Rtv ∧ φ)[g_{m}^{v}] for some m ∈ M. Let m′ be the interpretation of t in 𝔐 under g_{m}^{v}. Because of the restriction on variables in bounded quantification, t ≠ v, whence m′ is also the interpretation of t in 𝔐 under g. So Rm′m holds in 𝔐 and 𝔐 ⊧ φ[g_{m}^{v}]. By the inductive hypothesis, 𝔐, g_{m}^{v} ⊩ HT (φ) iff 𝔐, g, m ⊩↓v.HT (φ), iff 𝔐, g, m′ ⊩ ◇ ↓v.HT (φ) iff 𝔐, g, m′ ⊩ @_{t}◇ ↓v.HT (φ) iff 𝔐, g ⊩ @_{t}◇ ↓v.HT (φ). qed

As simple corollaries we have:

Corollary 3.3 Let φ(x) be a bounded formula with only x free, then for all models 𝔐 and for all m ∈ M, 𝔐 ⊧ φ(m) iff 𝔐, m ⊩↓x.HT (φ).

Corollary 3.4 Let φ be a first-order formula in the hybrid signature. Then the following are equivalent.

i. φ is equivalent to the standard translation of a hybrid formula.

ii. φ is equivalent to a formula in the bounded fragment. Moreover, there are effective translations between H(↓, @) and the bounded fragment.

3.2 Generated back-and-forth systems

We now turn to the problem of providing semantic characterizations of H(↓, @) (or equivalently, of the bounded fragment). In this section we define generated back-and-forth systems —basically a restricted form of Ehrenfeucht-Fraïssé game— and link it to the concept of generated submodels.

Generated back-and-forth systems Let 𝔐 and 𝔑 be two first-order models in the hybrid signature. A generated back-and-forth system between 𝔐 and 𝔑 is a non-empty family F of finite partial isomorphisms between 𝔐 and 𝔑 satisfying the following two extension rules:

(◇-extension)

- (forth) if h ∈ F, x in its domain and R^{𝔐}xy, then h ∪ {⟨y, y′⟩} ∈ F

for some y′ ∈ N.

- (back) if h ∈ F, x in its range and R^{𝔑}xy, then h ∪ {⟨y′, y⟩} ∈ F for

some y′ ∈ M.

(nominal extension)

- (forth) if h ∈ F and there exists an x ∈ M such that V^{𝔐}(i) = {x} for some nominal i, then there exists an x′ ∈ N such that h ∪ {⟨x, x′⟩} ∈ F.

- (back) a similar condition backwards.

Let m̄ (n̄) be a tuple in ^{k}M (^{k}N). Then (𝔐, m̄) ≡_{R} (𝔑, n̄) means that there exists a generated back-and-forth system between 𝔐 and 𝔑, containing a partial isomorphism which sends m(i) to n(i).

Note how closely this definition follows the familiar one from first-order logic (cf. e.g., [8]). In fact, if we think of such a system as describing an Ehrenfeucht-Fraïssé game, then the sole difference is that in the “generated back-and-forth game” the universal player must choose his moves from R-successors or worlds named by a nominal, whereas he can play whatever he likes in the full first-order game. Unsurprisingly, restricting the play to accessible worlds puts generated back-and-forth systems very close to generated submodels.

Definition 3.5 (Generated Submodel) Let 𝔐 = ⟨M, R, V ⟩ be a hybrid model and S ⊆ M. Let NOM denote the subset of M whose elements are in the interpretation of some nominal. The submodel of 𝔐 generated by S is the substructure of 𝔐 with domain {m ∈ M | exists s ∈ S ∪ NOM s.t. R^{∗}sm}, where R^{∗} is the reflexive and transitive closure of R.

Note that if NOM = ∅, we obtain the familiar modal notion of a generated submodel; and that if in addition S is a singleton set, we have the usual notion of a point-generated submodel.

We now define two kinds of invariance. The first is taken from [4]. A firstorder formula φ(x̄) in free variables x̄ in a signature with one binary relation R, unary predicates and constants (and equality) is invariant for generated submodels if for all models (𝔐, m̄) and (𝔐′, m̄) such that 𝔐′ is the m̄-generated submodel of 𝔐, 𝔐 ⊧ φ(m̄) iff 𝔐′ ⊧ φ(m̄). In a similar spirit, we shall say that a first-order formula φ(x̄) in the same signature is invariant for generated back-and-forth systems if for all models (𝔐, m̄) and (𝔑, n̄), (𝔐, m̄) ≡_{R} (𝔑, n̄) implies (𝔐 ⊧ φ(m̄) iff 𝔑 ⊧ φ(n̄)).

Theorem 3.6 Let φ(x̄) be a first-order formula in the hybrid signature. Then the following are equivalent.

i. φ(x̄) is equivalent to a formula in the bounded fragment.

ii. φ(x̄) is invariant for generated submodels.

iii. φ(x̄) is invariant for generated back-and-forth systems.

Proof. i. ⇒ ii. is obvious. ii. ⇒ iii. First note that φ(x̄) is invariant for generated submodels if and only if ¬φ(x̄) is. Now suppose φ(x̄) is invariant for generated submodels but not preserved under generated back-and-forth systems. Then we have models (𝔐, m̄) and (𝔑, n̄), a generated back-and-forth system linking m̄ and n̄, and 𝔐 ⊧ φ(m̄) while 𝔑 ⊧ ¬φ(n̄).

Let 𝔐′ (𝔑′) be the m̄- (n̄) generated submodel of 𝔐 (𝔑). Then still 𝔐′ ⊧ φ(m̄) and 𝔑′ ⊧ ¬φ(n̄), by invariance. Clearly (𝔐′, m) ≡_{R} (𝔑′, n). But then (𝔐′, m) and (𝔑′, n) have the same first-order theory by the following argument. Because (𝔐′, m) ≡_{R} (𝔑′, n) holds, ∃loise (the existential player) has a winning strategy in all games where ∀belard (the universal player) only plays immediate R-successors or points named by a nominal. But since the models are generated, in the first-order back-and-forth game he can only play worlds which are accessible by a finite R-transition from either the root or one of the named worlds. But then she can compute a winning answer for the classic Ehrenfeucht-Fraïssé game from her winning generated back-and-forth strategy. This contradicts the claim that 𝔐′ ⊧ φ(m̄) and 𝔑′ ⊧ ¬φ(n̄). iii. ⇒ i. We use a “van Benthem style” diagram-chasing argument. We only provide the outline. Let φ(x̄) be as in the hypothesis and BC(φ(x̄)) be the bounded consequences of φ(x̄) (that is, the consequences of φ(x̄) that belong to the bounded fragment). We will show that BC(φ(x̄)) ⊧ φ(x̄), from which the result follows by compactness. (In this notation we interpret the x̄ as constants, or equivalently we use the local version of first-order consequence.)

If BC(φ(x̄)) is inconsistent we are done. Otherwise, let 𝔐, m̄ be a model of BC(φ(x̄)) and 𝔑, n̄ be a model of φ(x̄) together with the bounded theory of 𝔐, m̄. (Such a model can easily be shown to exist.) Take ω-saturated extensions 𝔐^{+}, m̄ and 𝔑^{+}, n̄. Create a family F of finite functions between M^{+} and N^{+} as follows: f : x̄ → ȳ is in F iff 𝔐^{+}, x̄ and 𝔑^{+}, ȳ make the same bounded formulas true. It is easy to show that F is a generated back and forth system linking m̄ and n̄. Now we can start diagram chasing: 𝔑 ⊧ φ(n̄) then (by elementary extension) 𝔑^{+} ⊧ φ(n̄), then (by invariance) 𝔐^{+} ⊧ φ(m̄), then (passing to an elementary submodel) 𝔐 ⊧ φ(m̄) as desired. qed

3.3 Hybrid bisimulations

We have just seen that by weakening the notion of an Ehrenfeucht-Fraïssé game we can link the bounded fragment (and hence H(↓, @)) with generated submodels. But in spite of its binding apparatus, H(↓, @) has a distinctly modal flavor. Isn’t it also possible to strengthen the notion of bisimulation (the standard notion of equivalence between models used in modal logic) with clauses for ↓ and @, and so characterize H(↓, @) in intrinsically modal terms? That’s what we will do in this section. The approach has an advantage over the use of generated back-and-forth systems: preservation results can be easily obtained for reducts as well.

Recall that for ordinary propositional modal logics, bisimulations are nonempty binary relations linking the domains of models, with the restriction that only worlds with identical atomic information and matching accessibility relations should be connected (see Definition 3.7 [4]; here bisimulations are called p-relations). Now, if we want to extend this notion to H(↓, @), we need to take care of assignments to world variables as well. To this end, hybrid bisimulations will not simply link worlds, rather they will link pairs (m̄, m), where m is a world and m̄ is an assignment. We start by defining k-bisimulations, which are the correct notion of bisimulation for formulas φ such that WVAR(φ) ⊆ {x_{1}, …, x_{k}}.

k-bisimulation. Let 𝔐 and 𝔑 be two hybrid models. Let ∼^{k} be a binary relation between ^{k}M × M and ^{k}N × N. So ∼^{k} relates tuples ((m_{1}, …, m_{k}), m) with tuples ((n_{1}, …, n_{k}), n). We write these tuples as (m̄, m). Notice that m̄ can be seen as an assignment over (x_{1}, …, x_{k}). A non-empty relation ∼^{k} is called a k-bisimulation if it satisfies the following properties

(prop) If (m̄, m) ∼^{k} (n̄, n), then m ∈ V^{𝔐}(a) iff n ∈ V^{𝔑}(a), for a ∈ PROP ∪ NOM.

(var) If (m̄, m) ∼^{k} (n̄, n), then for all j ≤ k, m_{j} = m iff n_{j} = n.

(forth) If (m̄, m) ∼^{k} (n̄, n) and R^{𝔐}mm′, then there exists an n′ ∈ N such that

R^{𝔑}nn′ and (m̄, m′) ∼^{k} (n̄, n′).

(back) A similar condition from 𝔑 to 𝔐.

(@) If (m̄, m) ∼^{k} (n̄, n), then for every nominal i ∈ NOM, if m′ ∈ V^{𝔐}(i) and

n′ ∈ V^{𝔑}(i) then (m̄, m′) ∼^{k} (n̄, n′), and for every j ≤ k, (m̄, m_{j}) ∼^{k} (n̄, n_{j})

(↓) If (m̄, m) ∼^{k} (n̄, n), then for every j ≤ k, (m̄_{m}^{j}, m) ∼^{k} (n̄_{n}^{j}, n).

Note that since ↓ and @ are self-dual, we can collapse the back and forth clauses for these modalities into one. We write 𝔐 ∼^{k} 𝔑 if there exists a k-bisimulation between the two models.

To extend the notion to the full language we need to add only one further condition.

ω-bisimulation. Let 𝔐 and 𝔑 be two hybrid models. An ω-bisimulation between 𝔐 and 𝔑 is a non-empty family of k-bisimulations satisfying the following storage rule:

(sto) If (m̄, m) ∼^{k} (n̄, n), then ((m̄, m), m) ∼^{k+1} ((n̄, n), n).

Let m̄ (n̄) be a tuple in ^{k}M (^{k}N). Then (𝔐, m̄) ∼^{ω} (𝔑, n̄) means that there exists an ω-bisimulation between 𝔐 and 𝔑 such that (m̄, m̄(0)) ∼^{k} (n̄, n̄(0)).

Notice that the modular definition of k and ω-bisimulation will lead to results for reducts of the language as well. For instance if we delete ↓ from the language, we just delete the (↓) clause from the definition of bisimulation and we obtain the appropriate notion for the language H(@). Of course, if we through away the variables we don’t need the assignment tuples anymore, and the bisimulation becomes just a relation between worlds, as usual. Then for the language without ↓, @ and variables, the standard definition of bisimulation applies (the condition (prop) takes care of the nominals). If we add @ to this language, we just have to add the following clause

(@′) For all nominals i, if V^{𝔐}(i) = {m} and V^{𝔑}(i) = {n}, then m ∼ n.

Preservation results for all these alternatives can be given (the required proofs follow much the same lines as the proofs below).

The first important fact about hybrid bisimulations is that they preserve truth:

Proposition 3.7 Let 𝔐 and 𝔑 be two hybrid models, m ∈ M, n ∈ N. Then,

i. If 𝔐 ∼^{k} 𝔑, then for all formulas φ over the signature ⟨PROP, NOM, {x_{1},

…, x_{k}}⟩, (m̄, m) ∼^{k} (n̄, n) implies 𝔐, m̄, m ⊩ φ ⇔ 𝔑, n̄, n ⊩ φ.

ii. If (𝔐, m) ∼^{ω} (𝔑, n), then for all sentences φ over the signature ⟨PROP, NOM, WVAR⟨, 𝔐, m ⊩ φ ⇔ 𝔑, n ⊩ φ. (Recall that for sentences the choice of assignment is irrelevant.)

Proof.

i. By a straightforward inductive argument.

ii. Let (𝔐, m) ∼^{ω} (𝔑, n) and let φ be a hybrid sentence. Then it contains some variables, say {x_{1}, …, x_{k}}. We have (⟨m⟩, m) ∼^{1} (⟨n⟩, n), so k −1 applications of the storage rule gives (m̄, m) ∼^{k} (n̄, n), where m̄ is a k-tuple consisting of m’s and similarly for n̄. By i., 𝔐, m̄, m ⊩ φ ⇔ 𝔑, n̄, n ⊩ φ, whence since φ is a sentence 𝔐, m ⊩ φ ⇔ 𝔑, n ⊩ φ. qed

The notion of k-bisimulation has a distinct modal flavor. But a very first-order notion is hidden behind: partial isomorphism.

Proposition 3.8 Let k ≥ 2, and let 𝔐 ∼^{k} 𝔑. If (m̄, m) ∼^{k} (n̄, n), then the function f defined as f(m) = n and f(m(i)) = n(i) is a partial isomorphism between {m(1), …, m(k), m} and {n(1), …, n(k), n}.

Proof. The map f is a bijection by (var) and (@). By (prop) and (@), f preserves nominals and propositional variables. To see that it preserves the accessibility relation suppose R^{𝔐}xy. There are three cases.

(Case 1: x = m, y = m_{i}.) Then by (forth) there exists an n′ such that R^{𝔑}nn′ and (m̄, m_{i}) ∼^{k} (n̄, n′). But m̄(i) = m_{i}, so by (var), n′ = n̄(i), whence R^{𝔑}nf(m(i)).

(Case 2: x = m_{i}, y = m.) Let j ≠ i. Such a j exists because we assumed that k ≥ 2. By (↓), (m̄_{m}^{j}, m) ∼^{k} (n̄_{n}^{j}, n). Then by (@), (m̄_{m}^{j}, m_{i}) ∼^{k} (n̄_{n}^{j}, n_{i}). Now continue as in case 1.

(Case 3: x = m_{i}, y = m_{j}.) By (@), (m̄, m_{i}) ∼^{k} (n̄, n_{i}). Now continue as in case 1. Thus R^{𝔐}xy implies R^{𝔑}f(x)f(y). For the other direction use (back) in the same way. qed

Thus there is a clear link with our earlier work on generated back-and-forth systems. After Proposition 3.8 the following theorem shouldn’t come as a surprise:

Theorem 3.9 Let (𝔐, m̄) and (𝔑, n̄) be two models. Then the following are equivalent:

i. (𝔐, m̄) ∼^{ω} (𝔑, n̄).

ii. (𝔐, m̄) ≡_{R} (𝔑, n̄).

It is time to draw together the threads developed in the previous section. First we note their consequences for expressivity over models. Then we note the consequences for frames and what this tells us about hybrid completeness.

3.4 Expressivity over models

We have the following five-fold characterization of H(↓, @):

Theorem 3.10 Let φ(x̄) be a first-order formula in the hybrid signature (with equality). Then the following are equivalent.

i. φ(x̄) is equivalent to the standard translation of a H(↓, @) formula.

ii. φ(x̄) is invariant for generated submodels.

iii. φ(x̄) is invariant for generated back-and-forth systems.

iv. φ(x̄) is invariant for ω-bisimulation.

v. φ(x̄) is equivalent to a formula in the bounded fragment of first-order logic.

Proof. By Corollary 3.4, Theorem 3.6 and Proposition 3.7. qed

But these have obvious consequences for the ordinary modal correspondence language. In particular, if we consider nominal-free hybrid sentences, then we obtain a five-fold characterization of the fragment of first-order logic in the classical modal signature which is invariant for generated submodels:

Corollary 3.11 Let φ(x) be a first-order formula in the modal signature with equality. Then the following are equivalent.

i. φ(x) is equivalent to the standard translation of a nominal-free H(↓, @) sentence.

ii. φ(x) is invariant for generated submodels (now in the standard modal sense).

iii. φ(x) is invariant for R-generated back-and-forth systems, where an Rgenerated back-and-forth system is a back-and-forth system satisfying only the ◇-extension rule.

iv. φ(x) is invariant for ω-bisimulation.

v. φ(x) is equivalent to a formula in the bounded fragment of first-order logic without constants.

3.5 Frames and completeness

Recall that a frame 𝔉 is a pair ⟨W, R⟩ (that is, a model without a valuation). Since the late 1950s, one of the central topics in modal logic has been linking modal formulas to properties of frames and investigating when they give rise to complete axiomatizations for the frame classes they define. The work in the previous section easily yields a characterization of the frame-defining abilities of pure nominal-free sentences. Moreover, the axiomatic investigations of [6] show that there is a perfect match between definability and completeness for pure nominal-free sentences. By combining these results we obtain matching definability and completeness results for a wide range of first-order definable frame classes.

In modal correspondence theory, the first-order language (with equality) over the signature consisting simply of a binary symbol R is called the (firstorder) frame language. We shall call a formula φ in the frame language containing exactly one free variable a frame condition. The class of frames defined by a frame condition φ(x) is the class in which the universal closure ∀x.φ(x) is true; we call this class frames(∀x.φ(x)).

Before proceeding further, two simple observations are in order. First, note that if we apply the standard translation ST to a pure nominal-free sentence α , then ST (α) is a frame condition with free-variable x. Furthermore, note that for any frame 𝔉 = ⟨W, R⟩ we have that 𝔉 ⊩ α iff 𝔉 ⊩ ∀x.ST (α); this is an immediate consequence of the definition of frame validity.

Theorem 3.12 Let K[H(↓, @)] be the axiomatization for H(↓, @) given in [6], and for any hybrid sentence α let K[H(↓, @)] + α be the system obtained by adding α as an additional axiom. Then, if φ(x) is a frame condition and φ(x) is invariant under generated submodels (in the usual modal sense) we have that:

i. If φ(x) is in the bounded fragment, then the pure nominal free sentence ↓ x.HT (φ(x)) defines frames(∀x.φ(x)). Moreover, the logic K[H(↓, @)] + ↓x.HT (φ(x)) is strongly complete with respect to frames(∀x.φ(x)).

ii. If φ(x) is not in the bounded fragment, there is a nominal free sentence α such that α defines frames(∀x.φ(x)), and ST (α) is equivalent to φ(x). Moreover, K[H(↓, @)] + α is strongly complete with respect to frames(∀x.φ(x)).

Conversely, if α is a pure nominal-free sentence, then α defines the class of frames frames(∀x.ST (α(x))), and K[H(↓, @)] + α is complete with respect to frames(∀x.ST (α(x))).

Proof. The converse condition was proved in [6], so we examine the other direction.

For item i., we first remark that as φ(x) belongs to the frame language, it contains no unary predicate symbols, hence HT (φ(x)) is a pure formula; that ↓ x.HT (φ(x)) is a pure nominal-free sentence is thus clear. Now, by Corollary 3.3, for any model 𝔐 = (𝔉, V) and any m ∈ M,

(𝔉, V) ⊧ φ[m] iff (𝔉, V), m ⊩↓x.HT (φ).

But this means that

(𝔉, V) ⊧ ∀x.φ iff (𝔉, V) ⊩↓x.HT (φ).

As φ(x) contains no unary predicate symbols (and ↓x.HT (φ) no propositional variables) V is irrelevant, and hence

𝔉 ⊧ ∀x.φ(x) iff 𝔉 ⊩↓x.HT (φ).

This implies that ↓x.HT (φ(x)) defines frames(∀x.φ(x)). Completeness follows using the arguments of [6].

For item ii., we know that φ(x) being invariant under generated submodels is equivalent to a formula in the bounded fragment; but is it equivalent to a frame condition φ′(x)? In fact, this can be established by modifying the diagram chasing argument used in the proof of Theorem 3.6. The key point to observe is that instead of showing that BC(φ(x)) ⊧ φ(x), we can show by the same method that FC(φ(x)) ⊧ φ(x), where FC are all the frame conditions implied by φ(x). Thus there is an equivalent frame condition φ′(x), and we can take α to be ↓x.HT (φ′(x)). The remainder of the proof is as for item i. qed

4 ‘It’s a poor sort of memory that only works backwards’

As the Queen in Alice through the Looking-Glass pointed out, wouldn’t it be more satisfying if we could just remember a bit of what is to come? To remember (even if vaguely) of when we will be able to understand how to define the correct modal fragment for a given, specific need; and have general results that will let us measure in advance which is the minimal complexity and which are the properties of such a language?

Some beautiful results have already been given to us, e.g. the guarded fragments of Andréka, van Benthem and Németi [1] (“if a logic can be mapped here then it is decidable”) or the work on complexity of modal logics of Edith Spaan [9] (“if a logic is able to express this then it has at least this complexity). Also the conditions for failure of interpolation provided in [3] are in a similar line.

Which are the well behaved fragments and, most interestingly, why? These are indeed important questions which the modern approach to modal logics is starting to unravel.

And hybrid logics? Are they just one of the many? Play with them for a while and you will perhaps answer the question by yourself. Nominals seems to add to modal logic a new dimension (like filling a hole that only now we notice it was there). Modal logic is locality itself; this is the main reason of its good behavior. And once a local point of view is adopted, once we evaluate formulas in a particular point in the model, then the concept of “terms as formulas” comes just so naturally.

Hybrid logics will probably play a role in the next years. They offer high expressive power, an elegant proof theory and plenty of connections with other fields like temporal reasoning and knowledge representation. For the moment they taught us a bit more about the structure of the landscape of fragments we are swimming in.

References

[1] H. Andréka, J. van Benthem, and I. Németi. Back and forth between modal logic and classical logic. Bulletin of the Interest Group in Pure and Applied Logics, 3(3):685–720, 1995.

[2] C. Areces, P. Blackburn, and M. Marx. Hybrid logics. Characterization, interpolation and complexity. Submitted to the Journal of Symbolic Logic, February 1999.

[3] C. Areces and M. Marx. Failure of interpolation in combined modal logics, 1997. To appear in the Notre Dame Journal of Formal Logic.

[4] J. van Benthem. Modal Logic and Classical Logic. Bibliopolis, Naples, 1983.

[5] J. van Benthem. Correspondence theory. In Gabbay and Guenthner [7], pages 167–248. Extensions of classical logic.

[6] P. Blackburn and M. Tzakova. Hybrid languages and temporal logics. Logic Journal of the IGPL, 7(1):27–54, 1999.

[7] D. Gabbay and F. Guenthner, editors. volume 165 of Synthese Library. D. Reidel Publishing Co., Dordrecht, 1984. Extensions of classical logic.

[8] W. Hodges. Model theory. Cambridge University Press, Cambridge, 1993.

[9] E. Spaan. Complexity of modal logics. PhD thesis, University of Amsterdam, Institute for Logic, Language and Computation, 1993.