A complete classification of the expressiveness of interval logics of Allen’s relations: the general and the dense cases

Abstract

Interval temporal logics take time intervals, instead of time points, as their primitive temporal entities. One of the most studied interval temporal logics is Halpern and Shoham’s modal logic of time intervals HS, which associates a modal operator with each binary relation between intervals over a linear order (the so-called Allen’s interval relations). In this paper, we compare and classify the expressiveness of all fragments of HS on the class of all linear orders and on the subclass of all dense linear orders. For each of these classes, we identify a complete set of definabilities between HS modalities, valid in that class, thus obtaining a complete classification of the family of all 4096 fragments of HS with respect to their expressiveness. We show that on the class of all linear orders there are exactly 1347 expressively different fragments of HS, while on the class of dense linear orders there are exactly 966 such expressively different fragments.

1 Introduction

Interval reasoning naturally arises in various fields of computer science and artificial intelligence, ranging from hardware and real-time system verification to natural language processing, from constraint satisfaction to planning [4, 5, 19, 28, 29, 34]. Interval temporal logics make it possible to reason about interval structures over (linearly) ordered domains, where time intervals, rather than time points, are the primitive ontological entities. The distinctive features of interval temporal logics turn out to be useful in various application domains [9, 16, 27, 28, 34]. For instance, they allow one to model telic statements [32], that is, statements that express goals or accomplishments, e.g., the statement: ‘The airplane flew from Venice to Toronto’ (see, e.g., [15, Sect. II.B] and [27, p. 600]). Moreover, when we restrict ourselves to discrete linear orders, some interval temporal logics are expressive enough to constrain the length of intervals, thus allowing one to specify safety properties involving quantitative conditions [27]. This is the case, for instance, with the well-known ‘gas-burner’ example, originally presented in [34] and for which an encoding in a purely interval-based temporal logic has been proposed in [9]. Temporal logics with interval-based semantics have also been proposed as suitable formalisms for the specification and verification of hardware [28] and of real-time systems [34]. Finally, it is worth mentioning two system implementations recently proposed in the literature that are built on (either algebraic or logic) interval-based temporal formalisms: TERENCE [21] (an adaptive learning system for supporting poor comprehenders and their educators, which is based on the so-called Allen’s interval algebra) and RISMA [24] (an algorithm for performance and behavior analysis of real-time data systems, based on the well-known modal logic of Allen’s relations, which is the main focus of this paper).

The variety of binary relations between intervals in a linear order was first studied by Allen [4], who investigated their use in systems for time management and planning. In [22], Halpern and Shoham introduced and systematically analyzed the (full) modal logic of Allen’s relations, called HS in this paper, that features one modality for each Allen relation. In particular, they showed that HS is highly undecidable over most classes of linear orders. This result motivated the search for (syntactic) HS fragments offering a good balance between expressiveness and decidability/complexity [8, 10, 13–15, 25–27].

The problem of identifying expressive enough, yet decidable, fragments of HS that are suitable for specific classes of applications is a major research problem in the area. It requires a comparative analysis of the expressiveness of the variety of such fragments. This amounts to systematically studying mutual definabilities among the HS modalities. As an example, Bresolin et al. [11, 12] identify all decidable HS fragments with respect to the class of finite linear orders [11] and the class of strongly discrete linear orders [12], and classify them in terms of both their expressive power and their complexity.

A comparative analysis of the expressive power of the variety of HS fragments is far from being trivial, because some HS modalities are definable in terms of others, and thus syntactically different fragments may turn out to be equally expressive. To complicate matters, the definability of a specific modality by a given subset of HS modalities may depend on the class of linear orders over which the logic is interpreted. Thus, such classifications cannot, in general, be easily transferred from one class of linear orders to another: while definability does transfer from a class to all its proper sub-classes, proving a non-definability result amounts to providing a counterexample based on concrete linear orders from the considered class. As a matter of fact, different assumptions on the underlying linear orders give rise, in general, to different sets of definability equations.

Many classes of linear orders are of practical interest, including the class of all linear orders and the classes of all dense, discrete, and finite linear orders, as well as the particular linear orders on ${\mathbb {R}}$, ${\mathbb {Q}}$, ${\mathbb {Z}}$, and ${\mathbb {N}}$. In this paper, we give a complete classification of the expressiveness of HS fragments in two of the most important cases, namely, the general case (i.e., over the class of all linear orders) and the dense case (i.e., over the class of all dense linear orders).¹ Most of the arguments that we use to classify the expressive power of HS fragments over the class of all linear orders directly apply also to the class of all dense linear orders. Nevertheless, some extra effort is needed to obtain the classification over dense structures from the general one, since more definability equations hold in the dense case.

We identify a complete set of valid definability equations among HS modalities for both the considered classes of linear orders. While our proofs of undefinability results in the dense case are based on counterexamples referring to the linear order on ${\mathbb {R}}$, the proposed constructions can be easily modified to deal with other specific sub-classes of the class of all dense linear orders, e.g., the linear order on ${\mathbb {Q}}$. This means that the results presented in this paper yield complete classifications not only with respect to the two classes mentioned above, but also with respect to each of the linear orders on ${\mathbb {R}}$ and ${\mathbb {Q}}$. Eventually, we show that there are exactly 1347 expressively different HS fragments in the general case, and 966 ones in the dense case, out of 4096 syntactically distinct subsets of HS modalities.

The rest of the paper is organized as follows. In Sect. 2, we define the syntax and the semantics of the interval temporal logic HS, and we introduce the basic notions of definability and expressiveness. In Sect. 3, we give a short account of the main results of the paper. Sections 4 and 5 are devoted to the proofs of soundness and completeness of the proposed set of definability equations, respectively. The completeness proof turns out to be much harder than that of soundness, and thus it does not come as a surprise that Sect. 5 is much longer than Sect. 4. In the final section, we summarize in Theorem 1 the import of the collection of results shown in the previous sections, provide an assessment of the work done, and outline future research directions. Some of the most involved proofs are reported in a technical appendix.

2 Preliminaries

We denote the sets of natural numbers, integers, rationals, irrationals, and reals, as well as the linear orders based on them, respectively by ${\mathbb {N}}$, ${\mathbb {Z}}$, ${\mathbb {Q}}$, $\mathbb {\overline{Q}}$, and ${\mathbb {R}}$.

Let $\mathbb {D} = \langle D, <\rangle$ be a linearly ordered set. An interval over $\mathbb {D}$ is an ordered pair [a, b], where $a,b \in D$ and $a \le b$. An interval is called a point interval if $a=b$ and a strict interval if $a<b$. In this paper, we assume the strict semantics, that is, we exclude point intervals and only consider strict intervals. The adoption of the strict semantics, excluding point intervals, instead of the non-strict semantics, which includes them, conforms to the definition of interval adopted by Allen [4], but differs from the one given by Halpern and Shoham  [22]. It has at least two strong motivations: first, a number of representation paradoxes arise when the non-strict semantics is adopted, due to the presence of point intervals, as pointed out in [4]; second, when point intervals are included there seems to be no intuitive semantics for interval relations that makes them both pairwise disjoint and jointly exhaustive.

If we exclude the identity relation, there are 12 different relations between two strict intervals in a linear order, often called Allen’s relations [4]: the six relations $R_A$ (adjacent to), $R_L$ (later than), $R_B$ (begins), $R_E$ (ends), $R_D$ (during), and $R_O$ (overlaps), depicted in Fig. 1, and their inverses, that is, $R_{\overline{X}} = (R_{X})^{-1}$, for each $X \in \{ A, L, B, E, D, O \}$.

Fig. 1

Allen’s interval relations and the corresponding HS modalities

We interpret interval structures as Kripke structures, with Allen’s relations playing the role of the accessibility relations. Thus, we associate a modality $\langle X\rangle$ with each Allen relation $R_{X}$. For each $X \in \{ A, L, B, E, D, O \}$, the transpose of modality $\langle X \rangle$ is modality $\langle \overline{X} \rangle$, corresponding to the inverse relation $R_{\overline{X}}$ of $R_{X}$.

2.1 Syntax and semantics

Halpern and Shoham’s logic HS [22] is a multi-modal logic with formulae built from a finite, non-empty set ${\mathcal {AP}}$ of atomic propositions (also referred to as proposition letters), the propositional connectives $\vee$ and $\lnot$, and a modality for each Allen relation. With every subset $\{R_{X_1}, \ldots , R_{X_k}\}$ of these relations, we associate the fragment $\mathsf {X}_{\mathsf {1}} \mathsf {X}_{\mathsf {2}} \ldots \mathsf {X}_\mathsf {{k}}$ of HS, whose formulae are defined by the grammar:

$$\begin{aligned} \varphi \, {:}{:}{=}\, p \mid \lnot \varphi \mid \varphi \vee \varphi \mid \langle X_1\rangle \varphi \mid \ldots \mid \langle X_k\rangle \varphi , \end{aligned}$$

where $p \in {\mathcal {AP}}$. The other propositional connectives and constants (e.g., $\wedge$, $\rightarrow$, and $\top$), as well as the universal modalities (e.g., $[ A ] \varphi \equiv \lnot \langle A \rangle \lnot \varphi$), can be derived in the standard way. For a fragment ${\mathcal {F}} = \mathsf {X}_{\mathsf {1}} \mathsf {X}_{\mathsf {2}} \ldots \mathsf {X}_{\mathsf {k}}$ and a modality $\langle X \rangle$, we write $\langle X \rangle \in {\mathcal {F}}$ if $X \in \{X_1, \ldots , X_k\}$. Given two fragments ${\mathcal {F}}_1$ and ${\mathcal {F}}_2$, we write ${\mathcal {F}}_1 \subseteq {\mathcal {F}}_2$ if $\langle X \rangle \in {\mathcal {F}}_1$ implies $\langle X \rangle \in {\mathcal {F}}_2$, for every modality $\langle X \rangle$. Finally, for a fragment ${\mathcal {F}} = \mathsf {X}_{\mathsf {1}} \mathsf {X}_{\mathsf {2}} \ldots \mathsf {X}_{\mathsf {k}}$ and a formula $\varphi$, we write $\varphi \in {\mathcal {F}}$ or, equivalently, we say that $\varphi$ is an ${\mathcal {F}}$-formula, meaning that $\varphi$ belongs to the language of ${\mathcal {F}}$.

The (strict) semantics of HS is given in terms of interval models $M = \langle \mathbb {I(D)},V\rangle$, where ${\mathbb {D}}$ is a linear order, $\mathbb {I(D)}$ is the set of all (strict) intervals over $\mathbb {D}$, and V is a valuation function $V : {\mathcal {AP}} \rightarrow 2^{\mathbb {I(D)}}$, which assigns to every atomic proposition $p \in {\mathcal {AP}}$ the set of intervals V(p) on which p holds. The truth of a formula on a given interval [a, b] in an interval model M is defined by structural induction on formulae as follows:

• $M,[a,b] \Vdash p$ if and only if $[a,b]\in V(p)$, for each $p \in {\mathcal {AP}}$;

• $M,[a,b] \Vdash \lnot \psi$ if and only if it is not the case that $M,[a,b]\Vdash \psi$;

• $M,[a,b] \Vdash \varphi \vee \psi$ if and only if $M,[a,b]\Vdash \varphi$ or $M,[a,b]\Vdash \psi$;

• $M,[a,b] \Vdash \langle X\rangle \psi$ if and only if there exists an interval [c, d] such that $[a,b]R_{X}[c,d]$ and $M,[c,d]\Vdash \psi$, for each modality $\langle X\rangle$.

Formulae of HS can be interpreted over a given class of interval models. For the sake of brevity (and with a benign abuse of notation), for a given class of linear orders ${\mathcal {C}}$, we identify the class of interval models over linear orders in ${\mathcal {C}}$ with the class ${\mathcal {C}}$ itself. Thus, we will use, for example, the expression ‘formulae of HS are interpreted over the class ${\mathcal {C}}$ of linear orders’ instead of the extended one ‘formulae of HS are interpreted over the class of interval models over linear orders in ${\mathcal {C}}$’. Among others, we mention the following important classes of linear orders:

(i):

the class of all linear orders $\mathsf {Lin}$;

(ii):

the class of (all) dense linear orders $\mathsf {Den}$, that is, those in which for every pair of distinct points there exists at least one point in between them—e.g., ${\mathbb {Q}}$ and ${\mathbb {R}}$;

(iii):

the class of (all) discrete linear orders, that is, those in which every element, apart from the greatest element, if it exists, has an immediate successor, and every element, other than the least element, if it exists, has an immediate predecessor—e.g., ${\mathbb {N}}$, ${\mathbb {Z}}$, and ${\mathbb {Z}}+{\mathbb {Z}}$ ²;

(iv):

the class of (all) finite linear orders, that is, those having only finitely many points.

All the classes of linear orders we consider in this paper are (left/right) symmetric, namely, if a class ${\mathcal {C}}$ contains a linear order $\mathbb {D} = \langle D, \prec \rangle$, then it also contains (a linear order isomorphic to) its dual linear order $\mathbb {D}^d = \langle D, \succ \rangle$, where $\succ$ is the inverse of $\prec$.

A formula $\phi$ of HS is valid over a class ${\mathcal {C}}$ of linear orders, denoted by $\Vdash _{{\mathcal {C}}} \phi$, if it is true on every interval in every interval model belonging to ${\mathcal {C}}$. Two formulae $\phi$ and $\psi$ are equivalent relative to the class ${\mathcal {C}}$ of linear orders, denoted by $\phi \equiv _{{\mathcal {C}}} \psi$, if $\Vdash _{{\mathcal {C}}} \phi \leftrightarrow \psi$.

2.2 Definability and expressiveness

The following definition formalizes the notion of definability of modalities in terms of others.

Definition 1

(Definability) A modality $\langle X\rangle$ of HS is definable in an HS fragment ${\mathcal {F}}$ relative to a class ${\mathcal {C}}$ of linear orders, denoted $\langle X \rangle \lhd _{{\mathcal {C}}} {\mathcal {F}}$, if $\langle X\rangle p \equiv _{{\mathcal {C}}} \psi$ for some ${\mathcal {F}}$-formula $\psi$ over the atomic proposition p, for any $p \in {{\mathcal {AP}}}$. The equivalence $\langle X \rangle p \equiv _{{\mathcal {C}}} \psi$ is called a definability equation for $\langle X \rangle$ in ${\mathcal {F}}$ relative to ${\mathcal {C}}$. We write if $\langle X \rangle$ is not definable in ${\mathcal {F}}$ relative to ${\mathcal {C}}$.

In the rest of the paper, we will omit the class of linear orders when it is clear from the context (e.g., we will simply write $\langle X\rangle p \equiv \psi$ and $\langle X \rangle \lhd {\mathcal {F}}$ instead of $\langle X\rangle p \equiv _{{\mathcal {C}}} \psi$ and $\langle X \rangle \lhd _{{\mathcal {C}}} {\mathcal {F}}$, respectively). As we already noticed, smaller classes of linear orders inherit the definabilities holding for larger classes. Formally, if ${\mathcal {C}}_1$ and ${\mathcal {C}}_2$ are classes of linear orders such that ${\mathcal {C}}_1 \subset {\mathcal {C}}_2$, then all definabilities holding for ${\mathcal {C}}_2$ are also valid for ${\mathcal {C}}_1$. However, more definabilities can possibly hold for ${\mathcal {C}}_1$. On the other hand, undefinability results for ${\mathcal {C}}_1$ hold also for ${\mathcal {C}}_2$.

It is known from [22] that in the strict semantics all HS modalities are definable in the fragment containing modalities $\langle A \rangle$, $\langle B \rangle$, and $\langle E \rangle$, and their transposes $\langle \overline{A} \rangle$, $\langle \overline{B} \rangle$, and $\langle \overline{E} \rangle$. (In the non-strict semantics, the four modalities $\langle B \rangle$, $\langle E \rangle$, $\langle \overline{B} \rangle$, and $\langle \overline{E} \rangle$ suffice, as shown in [33].) For example, the modalities $\langle L \rangle$ and $\langle D \rangle$ are definable by means of the definability equations $\langle L \rangle p \equiv \langle A \rangle \langle A \rangle p$ and $\langle D \rangle p \equiv \langle B \rangle \langle E \rangle p$, respectively.

In this paper, we compare and classify the expressiveness of all HS fragments with respect to the class of all linear orders and to the class of all dense linear orders. Formally, let ${\mathcal {F}}_1$ and ${\mathcal {F}}_2$ be any pair of such fragments. For a given class ${\mathcal {C}}$ of linear orders, we say that:

• ${\mathcal {F}}_2$ is at least as expressive as ${\mathcal {F}}_1$, denoted by ${\mathcal {F}}_1 \preceq {\mathcal {F}}_2$, if each modality $\langle X\rangle \in {\mathcal {F}}_1$ is definable in ${\mathcal {F}}_2$;

• ${\mathcal {F}}_1$ is strictly less expressive than ${\mathcal {F}}_2$ (or, equivalently, ${\mathcal {F}}_2$ is strictly more expressive than ${\mathcal {F}}_1$), denoted by ${\mathcal {F}}_1 \prec {\mathcal {F}}_2$, if ${\mathcal {F}}_1 \preceq {\mathcal {F}}_2$ holds, but ${\mathcal {F}}_2 \preceq {\mathcal {F}}_1$ does not;

• ${\mathcal {F}}_1$ and ${\mathcal {F}}_2$ are equally expressive (or expressively equivalent), denoted by ${\mathcal {F}}_1 \equiv {\mathcal {F}}_2$, if both ${\mathcal {F}}_1 \preceq {\mathcal {F}}_2$ and ${\mathcal {F}}_2 \preceq {\mathcal {F}}_1$ hold;

• ${\mathcal {F}}_1$ and ${\mathcal {F}}_2$ are expressively incomparable if neither ${\mathcal {F}}_1 \preceq {\mathcal {F}}_2$ nor ${\mathcal {F}}_2 \preceq {\mathcal {F}}_1$ hold.

Now, we define the notion of optimal definability, relative to a class ${\mathcal {C}}$ of linear orders, as follows.

Definition 2

(Optimal definability) A definability $\langle X \rangle \lhd {\mathcal {F}}$ is optimal if for each fragment ${\mathcal {F}}'$ such that ${\mathcal {F}}' \prec {\mathcal {F}}$.

Our main technical contribution is to provide the complete (i.e., maximal with respect to set inclusion) set of optimal definabilities among modalities of HS. In other words, we identify a set of optimal definabilities and then we show that no more definabilities exist. In order to show non-definability of a given modality in an HS fragment, we use a standard technique in modal logic, based on the notion of bisimulation and the invariance of modal formulae with respect to bisimulations (see, e.g., [7, 23]).

Let ${\mathcal {F}}$ be an HS fragment. An ${\mathcal {F}}$-bisimulation between two interval models $M = \langle \mathbb {I(D)}, V \rangle$ and $M' = \langle \mathbb {I(D')}, V' \rangle$ over a set of proposition letters ${{\mathcal {AP}}}$ is a relation $Z \subseteq \mathbb {I(D)} \times \mathbb {I(D')}$ satisfying the following properties:

• local condition: Z-related intervals satisfy the same atomic propositions in ${{\mathcal {AP}}}$;

• forward condition: if $[a,b] Z [a',b']$ and $[a,b] R_X [c,d]$ for some $\langle X \rangle \in {\mathcal {F}}$, then there exists some $[c',d']$ such that $[a',b'] R_X [c',d']$ and $[c,d] Z [c',d']$;

• backward condition: if $[a,b] Z [a',b']$ and $[a',b'] R_X$ $[c',d']$ for some $\langle X \rangle \in {\mathcal {F}}$, then there exists some [c, d] such that $[a,b] R_X [c,d]$ and $[c,d] Z [c',d']$.

The important property of bisimulations used here is that every ${\mathcal {F}}$-bisimulation preserves the truth of all ${\mathcal {F}}$-formulae, that is, if $[a,b]Z[a',b']$ and Z is an ${\mathcal {F}}$-bisimulation, then [a, b] and $[a',b']$ satisfy exactly the same ${\mathcal {F}}$-formulae. Thus, in order to prove that a modality $\langle X\rangle$ is not definable in ${\mathcal {F}}$, it suffices to construct a pair of interval models $M = \langle \mathbb {I(D)}, V \rangle$ and $M' = \langle \mathbb {I(D')}, V' \rangle$, and an ${\mathcal {F}}$-bisimulation Z between them, relating a pair of intervals $[a,b] \in \mathbb {I(D)}$ and $[a',b'] \in \mathbb {I(D')}$, such that $M,[a,b] \Vdash \langle X\rangle p$ and $M',[a',b'] \not \Vdash \langle X\rangle p$. In this case, we say that Z violates $\langle X \rangle$. It is worth pointing out that non-definability results obtained using bisimulations are not restricted to the finitary logics we consider in this paper, but also apply to extensions with infinite disjunctions and with fixed-point operators (see, e.g., [7, App. A] or [31, Prop. 3, p. 71, and Prop. 2, p. 113]).

3 A summary of the results

As we have already pointed out, every subset of the set of the 12 modalities corresponding to Allen’s relations gives rise to a fragment of HS. There are $2^{12}$ (the cardinality of the powerset of the set of HS modalities) such fragments. Due to possible definabilities of some of these modalities in terms of others, not all these fragments are expressively different. We consider here the problem of obtaining a complete classification of all HS fragments with respect to their expressive power over the considered classes of linear orders. In other words, for any two HS fragments, we want to determine how they relate to each other with respect to expressiveness, that is, whether one is strictly less expressive than the other, or they are expressively equivalent, or they are incomparable.

In order to obtain such a classification, all we need to do is to provide a complete set of optimal definabilities between HS modalities. Indeed, having such a set, it is immediate to decide how any two given fragments relate with respect to their expressiveness. Table 1 presents such a complete set of optimal definabilities, partitioned in three groups (top, middle, and bottom). Some of them (group on the top) were already known from [22] to hold with respect to the class of all linear orders $\mathsf {Lin}$ and, consequently, with respect to the class of all dense linear orders $\mathsf {Den}$; the rest (group in the middle and group at the bottom) are the subject of the present work: the definabilities in the group in the middle hold for both classes $\mathsf {Lin}$ and $\mathsf {Den}$; the ones in the group at the bottom only hold for the class $\mathsf {Den}$.

Table 1 Complete set of optimal definabilities

This paper is devoted to proving that Table 1 does present a complete set of optimal definabilities. To this end, as a first step, we need to identify for each operator $\langle X\rangle$ all maximal HS fragments that cannot express $\langle X \rangle$ using the definabilities in Table 1. We call this task the MaxUndef problem. For those HS operators that are definable by means of only few definabilities, e.g., $\langle D \rangle$ and $\langle O \rangle$, or for those that are not definable at all in terms of the others, e.g., $\langle A \rangle$, $\langle B \rangle$, and $\langle E \rangle$, such a task is trivial and can be carried out by hand. However, in general solving MaxUndef turns out to be quite time consuming when the operator under consideration has a large number of definabilities (this is the case, for instance, with the HS modality $\langle L \rangle$ and the operators of the logic studied in [6]). To solve the MaxUndef problem for the modalities $\langle L \rangle$ and $\langle \overline{L} \rangle$, we have used the automated procedure designed and implemented in [1].

It is worth pointing out that the MaxUndef problem is interesting in its own right, thanks to its connections, established in [1], with other well-known classic problems in different areas of computer science, such as the problem of finding all the maximal models of a given Horn theory (which has been shown to be polynomially equivalent to MaxUndef), or the problem of enumerating all the hitting sets of a given hyper-graph (which can be seen as a restriction of MaxUndef to a specific, well-defined class of instances—see [1] for a detailed account).

Once the preliminary task MaxUndef has been performed, it is possible to disprove the existence of more definabilities using the notion of bisimulation as described at the end of Sect. 2. To this end, we provide, for each $\langle X \rangle$ and each maximal fragment ${\mathcal {F}}$ identified in the preliminary phase, an ${\mathcal {F}}$-bisimulation that violates $\langle X \rangle$. As a matter of fact, thanks to the symmetry of the classes of linear orders under consideration and using the intrinsic ‘duality’ between some HS modalities, it is enough to perform the above described process for only one modality in each pair of ‘dual’ modalities. Thus, before proceeding further, we formalize here the concepts of dual HS operators and dual HS fragments. We say that two HS operators $\langle X \rangle$ and $\langle Y \rangle$ are dual if and only if $(\langle X \rangle , \langle Y \rangle ) \in S$, where S is the relation defined as $S = \{ (\langle A \rangle , \langle \overline{A} \rangle ), (\langle \overline{A} \rangle , \langle A \rangle ),$ $(\langle L \rangle , \langle \overline{L} \rangle ), (\langle \overline{L} \rangle , \langle L \rangle ),$ $(\langle B \rangle , \langle E \rangle ), (\langle \overline{B} \rangle , \langle \overline{E} \rangle ),$ $(\langle E \rangle , \langle B \rangle ), (\langle \overline{E} \rangle , \langle \overline{B} \rangle ),$ $(\langle D \rangle , \langle D \rangle ), (\langle \overline{D} \rangle , \langle \overline{D} \rangle ),$ $(\langle O \rangle , \langle \overline{O} \rangle ), (\langle \overline{O} \rangle , \langle O \rangle ) \}$. To define the notion of dual fragments, we lift the relation S to a relation between fragments, denoted by $\hat{S}$ and defined as $\hat{S} = \{ ({\mathcal {F}}_1, {\mathcal {F}}_2) \mid \forall \langle X \rangle \in {\mathcal {F}}_1 \ \exists \langle Y \rangle \in {\mathcal {F}}_2 . (\langle X \rangle ,\langle Y \rangle ) \in S$ and $\forall \langle Y \rangle \in {\mathcal {F}}_2 \ \exists \langle X \rangle \in {\mathcal {F}}_1 . (\langle Y \rangle , \langle X \rangle ) \in S \}$. We say that two fragments ${\mathcal {F}}_1$ and ${\mathcal {F}}_2$ are dual if and only if $({\mathcal {F}}_1, {\mathcal {F}}_2) \in \hat{S}$. Not surprisingly, both relations S and $\hat{S}$ are symmetric. In addition, notice that they are, in fact, functions. Therefore, we may denote by $S(\langle X \rangle )$ (resp., $\hat{S}({\mathcal {F}}_1)$) the unique $\langle Y \rangle$ (resp., ${\mathcal {F}}_2$) such that $(\langle X \rangle ,\langle Y \rangle ) \in S$ (resp., $({\mathcal {F}}_1,{\mathcal {F}}_2) \in \hat{S}$). Now, we can state the following proposition, which will simplify our proofs in Sect. 5.

Proposition 1

Let $\langle X_1 \rangle$ and $\langle X_2 \rangle$ be two dual HS modalities and ${\mathcal {C}}$ be a symmetric class of linear orders. Then, $\langle X_1 \rangle$ is definable in an HS fragment ${\mathcal {F}}$ relative to the class ${\mathcal {C}}$ if and only if $\langle X_2 \rangle$ is definable in $\hat{S}({\mathcal {F}})$ relative to the class ${\mathcal {C}}$.

Proof

Let $\varphi$ be an ${\mathcal {F}}$-formula and M be a model in ${\mathcal {C}}$. The dual formula of $\varphi$, denoted by $\varphi ^D$, is obtained from $\varphi$ by replacing every modality with its dual. It is clear that $\varphi ^D \in \hat{S}({\mathcal {F}})$. The dual model of M, denoted by $M^D$, is defined as $M^D = \langle {\mathbb {I}}({\mathbb {D}}^D), V^D\rangle$, where:

• $\mathbb {D}^D \in {\mathcal {C}}$ is (a linear order isomorphic to) the dual of ${\mathbb {D}}$, whose existence is guaranteed by the symmetry of ${\mathcal {C}}$. By the duality of ${\mathbb {D}}$ and ${\mathbb {D}}^D$, there exists an order-preserving isomorphism between the elements of ${\mathbb {D}}$ and the ones of ${\mathbb {D}}^D$. Let us denote it by $\xi$;

• $V^D: {{\mathcal {AP}}} \rightarrow 2^{\mathbb {I(D^D)}}$ is defined as follows: $V^D(p) = \{ [\xi (b),\xi (a)] \in {\mathbb {I}}({\mathbb {D}}^D) \mid [a,b] \in V(p) \}$, for each $p \in {{\mathcal {AP}}}$.

Since ${\mathcal {C}}$ is symmetric, $M^D$ belongs to ${\mathcal {C}}$ as well. In order to prove the proposition, we use the following general observation, which can be easily shown using structural induction on formulae (we omit the details, which are straightforward):

$$\begin{aligned} M, [a,b] \Vdash \varphi \text { if and only if } M^D, [\xi (b),\xi (a)] \Vdash \varphi ^D, \end{aligned}$$

(1)

for each model $M \in {\mathcal {C}}$, each interval [a, b] over M, and each formula $\varphi \in {\mathcal {F}}$.

Now, let us suppose that $\langle X_1 \rangle$ is definable in ${\mathcal {F}}$ relative to the class ${\mathcal {C}}$, due to the definability equation $\langle X_1 \rangle p \equiv \psi$. This means that the formula $\langle X_1 \rangle p \leftrightarrow \psi$ is valid (over ${\mathcal {C}}$). Since $\langle X_1 \rangle p \leftrightarrow \psi$ and $\langle X_2 \rangle p \leftrightarrow \psi ^D$ are dual, it follows from (1) that $\langle X_2 \rangle p \leftrightarrow \psi ^D$ is valid (over ${\mathcal {C}}$), which implies that $\langle X_2 \rangle$ is definable in $\hat{S}({\mathcal {F}})$ relative to the class ${\mathcal {C}}$. The converse implication can be shown following the same argument. $\square$

Table 2 Maximal fragments that do not define $\langle X\rangle$ according to definabilities in Table 1

Table 2 shows the outcome of the preliminary step MaxUndef. Precisely, for each modality $\langle X\rangle$ (dual modalities are coupled together in the rows of the table) and for both the considered classes of linear orders $\mathsf {Lin}$ and $\mathsf {Den}$, the table lists all the maximal HS fragments ${\mathcal {F}}$ in which $\langle X \rangle$ is not definable using the definabilities of Table 1 (fourth column). In addition, for each such fragment ${\mathcal {F}}$, we identify the minimal fragment ${\mathcal {F}}'$ that is expressively equivalent to ${\mathcal {F}}$ (fifth column). Finally, the last column refers to the lemma or corollary containing the proof of non-definability of $\langle X \rangle$ in ${\mathcal {F}}$ relative to the classes of linear orders specified in the second and third column. For instance, consider the first two rows of the table. The first column tells us that they refer to the operator $\langle L \rangle$ (and to the dual operator $\langle \overline{L} \rangle$). The second and the third column discriminate the class of linear orders, which is, in the example under consideration, the class $\mathsf {Lin}$. The fourth column contains, on the left of the slash symbol ‘/’, the maximal HS fragments in which $\langle L \rangle$ is not definable using the definabilities of Table 1, namely $\mathsf {B E D O} \overline{\mathsf {A L E D O}}$ and $\mathsf {B D O}\overline{\mathsf {A L B E D O}}$, and, on the right of the slash symbol ‘/’, the maximal HS fragments in which $\langle \overline{L} \rangle$ is not definable using the definabilities of Table 1, namely $\mathsf {E B D}\overline{\mathsf {O}} \mathsf {A L}\overline{\mathsf {B D}}\mathsf {O}$ and $\mathsf {E D}\overline{\mathsf {O}} \mathsf {A L} \overline{\mathsf {E B D}}\mathsf {O}$. The fifth column contains the minimal fragments that are expressively equivalent to the ones listed in the fourth column, namely, $\mathsf {B E O}\overline{\mathsf {A E D}}$, $\mathsf {B D O}\overline{\mathsf {A B E}}$, $\mathsf {E B} \overline{\mathsf {O}} \mathsf {A} \overline{\mathsf {B D}}$, and $\mathsf {E D} \overline{\mathsf {O}} \mathsf {A}\overline{\mathsf {E B}}$, respectively. The last column refers to Lemma 3 and Lemma 4, which prove that $\langle L \rangle$ is definable neither in $\mathsf {B E D O} \overline{\mathsf {A L E D O}}$ nor in $\mathsf {B D O}\overline{\mathsf {A L B E D O}}$ relative to the class $\mathsf {Lin}$. Notice that fragments coupled together (in the same row) in either the fourth or the fifth column are always dual, since they correspond to dual modalities.

In what follows, we first prove in Sect. 4 the validity of the new definabilities given in this paper, that is, the ones that appear in the middle and bottom groups in Table 1; then, following the above-described pattern, we prove in Sect. 5 that Table 1 contains a complete set of optimal definabilities relative to each of the classes $\mathsf {Lin}$ and $\mathsf {Den}$. While proving soundness of the given sets of definability equations is quite straightforward, proving their completeness is a non-trivial task, which requires a deep understanding of the expressive power of a fragment of HS and the, often very delicate, construction of bisimulations relating carefully constructed interval models. We note that, even though all the definabilities for all the operators but $\langle L \rangle$ and $\langle \overline{L} \rangle$ have been known since [22], no proof of their completeness was available so far.

4 Soundness

We only need to prove the soundness of the set of definability equations listed in the second and third groups of Table 1. As already pointed out, since $\langle L \rangle$ and $\langle \overline{L} \rangle$ are dual, we focus on the definabilities for $\langle L \rangle$, and we will use the symmetry of the linear order to obtain the result for $\langle \overline{L} \rangle$ as well. The following lemma states the soundness of the only definability for $\langle L \rangle$ listed in the second group of Table 1.

Lemma 1

(soundness for $\langle L \rangle$   over $\mathsf {Lin}$) $\langle L \rangle$ is definable in $\overline{\mathsf {B}}\mathsf {E}$ relative to the class $\mathsf {Lin}$.

Proof

We have to prove that the equivalence $\langle L \rangle p \equiv \langle \overline{B} \rangle [ E ] \langle \overline{B} \rangle \langle E \rangle p$ holds over $\mathsf {Lin}$. First, we prove the left-to-right direction. To this end, suppose that $M,[a,b] \Vdash \langle L \rangle p$ for some model M and interval [a, b]. This means that there exists an interval [c, d] such that $b < c$ and $M,[c,d] \Vdash p$. We exhibit an interval [a, y], with $y > b$ such that, for every x (strictly) in between a and y, the interval [x, y] is such that there exist two points $y'$ and $x'$ such that $y'>y$, $x < x' < y'$, and $[x',y']$ satisfies p. Let y be equal to c. The interval [a, c], which is started by [a, b], is such that for any of its ending intervals, that is, for any interval of the form [x, c], with $a < x$, we have that $x < c < d$ and $M,[c,d] \Vdash p$. As for the other direction, we must show that $\langle \overline{B} \rangle [ E ] \langle \overline{B} \rangle \langle E \rangle p$ implies $\langle L \rangle p$. To this end, suppose that $M,[a,b] \Vdash \langle \overline{B} \rangle [ E ] \langle \overline{B} \rangle \langle E \rangle p$ for a model M and an interval [a, b]. Then, there exists an interval [a, c], for some $c>b$, such that $[ E ] \langle \overline{B} \rangle \langle E \rangle p$ is true on [a, c]. As a consequence, the interval [b, c] must satisfy $\langle \overline{B} \rangle \langle E \rangle p$, which means that there are two points x and y such that $y > c$, $b< x < y$, and [x, y] satisfies p. Since $x>b$, it follows that $M,[a,b] \Vdash \langle L \rangle p$.

$\square$

The following corollary, which is a direct consequence of Proposition 1 and Lemma 1, states the soundness of the only definabilities for $\langle \overline{L} \rangle$ listed in the second group of Table 1.

Corollary 1

(Soundness for $\langle \overline{L} \rangle$ over $\mathsf {Lin}$) $\langle \overline{L} \rangle$ is definable in $\mathsf {B\overline{E}}$ relative to the class $\mathsf {Lin}$.

In the following lemma, we prove the soundness of the definabilities for $\langle L \rangle$ holding over the class $\mathsf {Den}$ only (and not in $\mathsf {Lin}$—third group in Table 1).

Lemma 2

(Soundness for $\langle L \rangle$ over $\mathsf {Den}$) The following definabilities hold relative to the class $\mathsf {Den}$:

• $\langle L \rangle$ is definable in $\mathsf {D O}$,

• $\langle L \rangle$ is definable in $\overline{\mathsf {B}}\mathsf {D}$,

• $\langle L \rangle$ is definable in $\mathsf {E O}$,

• $\langle L \rangle$ is definable in $\mathsf {B O}$ and

• $\langle L \rangle$ is definable in $\overline{\mathsf {L}}\mathsf {O}$.

Proof

We only present here the proof for the definability of $\langle L \rangle$ in $\mathsf {D O}$. The proofs for the other definabilities can be found in “Appendix 7”.

Consider the equivalence $\langle L \rangle p \equiv \langle O \rangle (\langle O \rangle \top \wedge [ O ] \langle D \rangle \langle O \rangle p)$ interpreted over the class $\mathsf {Den}$. First, suppose that $M,[a,b] \Vdash \langle L \rangle p$ for an interval [a, b] in a model M. We want to prove that $M,[a,b] \Vdash \langle O \rangle (\langle O \rangle \top \wedge [ O ] \langle D \rangle \langle O \rangle p)$ holds as well. By $M,[a,b] \Vdash \langle L \rangle p$, it follows that there exists an interval [c, d] in M such that $b < c$ and $M,[c,d] \Vdash p$. Consider an interval $[a',c]$, with $a < a' < b$ (the existence of such a point $a'$ is guaranteed by the density of the linear order). It is such that $[a,b] R_O [a',c]$ and it satisfies:

• $\langle O \rangle \top$, as $[a',c] R_O [b,d]$, and

• $[ O ] \langle D \rangle \langle O \rangle p$, as every interval [e, f], with $[a',c] R_O [e,f]$, is such that $e < c < f$, and thus, by density, there exists an interval $[e',f']$ such that $[e,f] R_D [e',f']$ and $[e',f'] R_O [c,d]$, which implies $M,[e,f] \Vdash \langle D \rangle \langle O \rangle p$, which in turn implies $M,[a',c] \Vdash [ O ] \langle D \rangle \langle O \rangle p$.

Hence, $M,[a',c] \Vdash \langle O \rangle \top \wedge [ O ] \langle D \rangle \langle O \rangle p$ and $M,[a,b] \Vdash \langle O \rangle (\langle O \rangle \top \wedge [ O ] \langle D \rangle \langle O \rangle p)$.

As for the opposite direction, let us assume that $M,[a,b] \Vdash \langle O \rangle (\langle O \rangle \top \wedge [ O ] \langle D \rangle \langle O \rangle p)$ for an interval [a, b] in a model M. That means that there exists an interval [c, d], with $[a,b] R_O [c,d]$, such that:

• $M,[c,d] \Vdash \langle O \rangle \top$, and thus there exists a point $e > d$, and

• $M,[c,d] \Vdash [ O ] \langle D \rangle \langle O \rangle p$.

The interval [b, e] is such that $[c,d] R_O [b,e]$, and thus, by the second condition above, it satisfies $\langle D \rangle \langle O \rangle p$. Therefore, there exist an interval [f, g] such that $[b,e] R_D [f,g]$, and an interval [h, i] such that $[f,g] R_O [h,i]$ and p holds over [h, i]. Since $h>b$, we conclude that $M,[a,b] \Vdash \langle L \rangle p$. $\square$

The following corollary, which immediately follows from Proposition 1 and Lemma 2, states the soundness of the remaining definabilities.

Corollary 2

The following definabilities hold relative to the class $\mathsf {Den}$:

• $\langle \overline{L} \rangle$ is definable in $\mathsf {D} \overline{\mathsf {O}}$,

• $\langle \overline{L} \rangle$ is definable in $\overline{\mathsf {E}}\mathsf {D}$,

• $\langle \overline{L} \rangle$ is definable in $\mathsf {B}\overline{\mathsf {O}}$,

• $\langle \overline{L} \rangle$ is definable in $\mathsf {E} \overline{\mathsf {O}}$ and

• $\langle \overline{L} \rangle$ is definable in $\mathsf {L}\overline{\mathsf {O}}$.

5 Completeness

As we have already pointed out, proving completeness of the set of definabilities is the most difficult task in obtaining the expressiveness classification we seek. Following the general pattern described in Sect. 3, we first compute, for each operator $\langle X\rangle$, the set ${\mathcal {M}}(X)$ (4th column of Table 2), containing all the maximal fragments ${\mathcal {F}}$ in which $\langle X\rangle$ is not definable using the definabilities of Table 1 (i.e., for each ${\mathcal {F}} \in {\mathcal {M}}(X)$). Then, for each modality $\langle X\rangle$ and each fragment ${\mathcal {F}} \in {\mathcal {M}}(X)$, we compute the minimal fragment ${\mathcal {F}}'$ such that ${\mathcal {F}}' \equiv {\mathcal {F}}$, according to the definabilities of Table 1 (note that there exists exactly one such a fragment ${\mathcal {F}}'$ for each operator $\langle X\rangle$ and each ${\mathcal {F}} \in {\mathcal {M}}(X)$). We collect such fragments in the set $\mu (X) = \{ {\mathcal {F}}' \mid {\mathcal {F}} \in {\mathcal {M}}(X)$ and ${\mathcal {F}}'$ is the minimal fragment such that ${\mathcal {F}}' \equiv {\mathcal {F}} \}$ (fifth column of Table 2). Finally, we provide an ${\mathcal {F}}'$-bisimulation that violates $\langle X \rangle$, for each modality $\langle X\rangle$ and each fragment ${\mathcal {F}}' \in \mu (X)$.

As we have already pointed out, thanks to the symmetry of the classes of linear orders and to the duality of HS modalities and fragments, it suffices to focus on one modality for each pair of dual modalities only. For the sake of readability, we omit the details for the most technical parts of most of the proofs in this section. For a more detailed account of the proofs, the interested reader can refer to the appendix.

5.1 Completeness for $\langle L \rangle /\langle \overline{L} \rangle$: case $\mathsf {Lin}$

In this subsection, we prove that the set of optimal definabilities listed in Table 1 for $\langle L \rangle$ and $\langle \overline{L} \rangle$ is complete relative to the class $\mathsf {Lin}$. To this end, we show that $\langle L \rangle$ is not definable in either of the maximal fragments $\mathsf {B E O \overline{A E D}}$ and $\mathsf {B D O\overline{A B E}}$ (see Table 2).

Lemma 3

$\langle L \rangle$ is not definable in $\mathsf {B E O \overline{A E D}}$ relative to the class $\mathsf {Lin}$.

Proof

Let $M_1 = \langle {\mathbb {I}}({\mathbb {N}}),V_1 \rangle$ and $M_2 = \langle {\mathbb {I}}({\mathbb {N}}), V_2 \rangle$ be two models and let $V_1$ and $V_2$ be such that $V_1 (p) = \{[2,3]\}$ and $V_2 (p) = \emptyset$, where p is the only proposition letter of the language. Moreover, let Z be a relation between (intervals of) $M_1$ and $M_2$ defined as:

$$\begin{aligned} Z = \{([0,1],[0,1])\}. \end{aligned}$$

It can be easily shown that Z is a $\mathsf {B E O \overline{A E D}}$-bisimulation. The local property is trivially satisfied since all Z-related intervals satisfy $\lnot p$. As for the forward and backward conditions, it suffices to notice that, starting from the interval [0, 1], it is not possible to reach any other interval using any of the modalities of the fragment. At the same time, Z violates $\langle L \rangle$. Indeed, [0, 1] Z [0, 1] and $M_1,$ $[0,1] \Vdash \langle L \rangle p$, but $M_2,[0,1] \Vdash \lnot \langle L \rangle p$. Thus, we can conclude that $\langle L \rangle$ is not definable in $\mathsf {B E O \overline{A E D}}$ relative to the class $\mathsf {Lin}$. $\square$

Lemma 4

$\langle L \rangle$ is not definable in $\mathsf {B D O\overline{A B E}}$ relative to the class $\mathsf {Lin}$.

Proof

Let $M_1 = \langle {\mathbb {I}}({\mathbb {Z}}^-),V_1 \rangle$ and $M_2 = \langle {\mathbb {I}}({\mathbb {Z}}^-), V_2 \rangle$ be two models based on the set ${\mathbb {Z}}^- = \{\ldots , -2,-1\}$ of the negative integers, and let $V_1$ and $V_2$ be such that $V_1 (p) = \{[-2,-1]\}$ and $V_2 (p) = \emptyset$, where p is the only proposition letter of the language. Moreover, let Z be the relation between (intervals of) $M_1$ and $M_2$ defined as follows:

$$\begin{aligned}{}[x,y] Z [w,z] \Leftrightarrow [x,y]=[w,z] \quad \text {and } [x,y] \ne [-2,-1]. \end{aligned}$$

We prove that Z is a $\mathsf {B D O\overline{A B E}}$-bisimulation. First, the local property is trivially satisfied since all Z-related intervals satisfy $\lnot p$. Moreover, starting from any interval, the only interval that satisfies p, viz., $[-2,-1]$, cannot be reached using the set of modal operators featured by our fragment. At the same time, Z violates $\langle L \rangle$, as $[-4,-3]Z[-4,-3]$ and $M_1,[-4,-3] \Vdash \langle L \rangle p$, but $M_2,[-4,-3] \Vdash \lnot \langle L \rangle p$. The thesis immediately follows. $\square$

By Proposition 1, Lemma 3, and Lemma 4, the following corollary holds.

Corollary 3

The following non-definabilities hold relative to the class $\mathsf {Lin}$:

• $\langle \overline{L} \rangle$ is not definable in $\mathsf {E B \overline{O} A \overline{B D}}$ and

• $\langle \overline{L} \rangle$ is not definable in $\mathsf {ED \overline{O} A \overline{E B}}$.

5.2 Completeness for $\langle L \rangle /\langle \overline{L} \rangle$: case $\mathsf {Den}$

The case $\mathsf {Den}$ is more complicated than the case $\mathsf {Lin}$. The bisimulations of this section, one for each of the three fragments indicated in Table 2, namely, $\mathsf {B\overline{A B E}}$, $\mathsf {B E\overline{A E D}}$, and $\mathsf {O\overline{B E O}}$, make use of the following observation. If ${\mathbb {D}}$ is a dense linear order without least and greatest elements, then for each $[a,b] \in \mathbb {I(D)}$ and $X \in \{ A, L, B, E, D, O, \overline{A}, \overline{L}, \overline{B}, \overline{E},$ $\overline{D}, \overline{O} \}$ there exists an interval $[c,d] \in \mathbb {I(D)}$ such that $[a,b] R_X [c,d]$. In addition, the following general result, which will be used in the proofs, holds.

Proposition 2

Let ${\mathcal {F}}$ be an HS fragment and Z be a symmetric relation between two interval models that satisfies the forward condition with respect to ${\mathcal {F}}$ (i.e., if $[a,b]Z[a',b']$ and $[a,b]R_X[c,d]$ hold for some modality $\langle X \rangle \in {\mathcal {F}}$, then there exists an interval $[c',d']$ such that $[a',b']R_X[c',d']$ and $[c,d]Z[c',d']$ hold as well). Then, Z satisfies the backward condition with respect to ${\mathcal {F}}$ as well (i.e., if $[a,b]Z[a',b']$ and $[a',b']R_X[c',d']$ hold for some modality $\langle X \rangle \in {\mathcal {F}}$, then there exists an interval [c, d] such that $[a,b]R_X[c,d]$ and $[c,d]Z[c',d']$ hold as well).

Proof

Suppose that $[a,b]Z[a',b']$ and $[a',b'] R_X [c',d']$ hold for some $\langle X \rangle \in {\mathcal {F}}$. We need to find an interval [c, d] such that $[a,b] R_X [c,d]$ and $[c,d] Z [c',d']$ hold. By symmetry, we have that $[a',b']Z[a,b]$ holds, as well. Then, by the forward condition, we know that there exists an interval [c, d] such that $[a,b] R_X [c,d]$ and $[c',d'] Z [c,d]$ hold. By symmetry $[c,d] Z [c',d']$ also holds, hence the backward condition is fulfilled. $\square$

Lemma 5

$\langle L \rangle$ is not definable in $\mathsf {B \overline{A B E}}$ relative to the class $\mathsf {Den}$.

Proof

Consider the two interval models M and $M'$, defined as $M = \langle \mathbb {I(R)}, V \rangle$ and $M' = \langle \mathbb {I(R)}, V' \rangle$, respectively, where $V(p) = \{[a,b] \mid a,b \in {\mathbb {Q}} \text { or } a,b \in \overline{\mathbb {Q}}\}$ and $V'(p) = \{[a',b'] \mid a' \le 0 \text { and } ( a',b' \in {\mathbb {Q}} \text { or } a',b' \in \overline{\mathbb {Q}})\}$ (recall that $\overline{\mathbb {Q}} = {\mathbb {R}} \setminus {\mathbb {Q}}$). Moreover, let $Z = \{ ([a,b],[a',b']) \mid a' \le -1$ and $M,[a,b] \Vdash p \text { iff } M',[a',b'] \Vdash p \}$.

It immediately follows from definition that the local condition is satisfied.

As for the forward condition, consider a pair $([a,b],[a',b'])$ of Z-related intervals. By definition of Z, it holds that $a' \le -1$ (and thus $a' \le 0$). Let $X \in \{ B, \overline{A}, \overline{B}, \overline{E} \}$. For every interval $[c',d']$, with $[a',b'] R_X [c',d']$, it holds that $c' \le -1$ (and thus $c' \le 0$).

Since ${\mathbb {Q}}$ and $\overline{\mathbb {Q}}$ are both dense and unbounded, there exist (i) an interval $[c'',d'']$, such that $[a',b'] R_X [c'',d'']$, with $c'',d'' \in {\mathbb {Q}}$ or $c'',d'' \in \overline{\mathbb {Q}}$, and (ii) an interval $[c''',d''']$, such that $[a',b'] R_X [c''',d''']$, with $c''' \in {\mathbb {S}}$, $d''' \in \mathbb {S'}$ for some ${\mathbb {S}}, {\mathbb {S}}' \in \{ {\mathbb {Q}}, \overline{\mathbb {Q}} \}$, with ${\mathbb {S}} \ne {\mathbb {S}}'$. Therefore, for every [c, d] such that $[a,b] R_X [c,d]$, there exists $[c',d']$ such that $[a',b'] R_X [c',d']$ and $[c,d] Z [c',d']$.

The backward condition can be checked with an analogous argument.

It is now immediate to check that $[-1,0] Z [-1,0]$, $M,[-1,0] \Vdash \langle L \rangle p$ (as $M, [1, 2] \Vdash p$) and $M',[-1,0] \Vdash \lnot \langle L \rangle p$ (as no interval [c, d], with $c>0$, satisfies p in $M'$). Thus, Z is a $\mathsf {B \overline{A B E}}$-bisimulation that violates $\langle L \rangle$, from which the thesis follows. $\square$

In order to build a $\mathsf {B E\overline{A E D}}$-bisimulation that violates $\langle L \rangle$ (Lemma 7 below), we use the following technical result, whose proof is trivial and thus omitted. Consider the function $f: {\mathbb {R}} \rightarrow \{ x \in {\mathbb {R}} \mid x < 1 \}$, defined as follows:

$$\begin{aligned} f(x) = \left\{ \begin{array}{l@{\quad }l} x-1 &{} \text {if } x \le 1 \\ 1-\frac{1}{x} &{} \text {if } x > 1 \\ \end{array} \right. \end{aligned}$$

(2)

Lemma 6

The function f is a monotonically increasing bijection from ${\mathbb {R}}$ to $(-\infty ,1)$ such that $f(x) < x$ for every $x \in {\mathbb {R}}$.

Using the above lemma, we are now ready to prove the following result.

Lemma 7

$\langle L \rangle$ is not definable in $\mathsf {B E\overline{A E D}}$ relative to the class $\mathsf {Den}$.

Proof

Consider two interval models M and $M'$, defined as $M = M' = \langle \mathbb {I(R)}, V \rangle$, where $V(p) = \{[a,b] \mid a = f(b) \}$ and where f is the function defined as in (2). In addition, let $Z = \{ ([a,b],[a',b']) \mid a \sim f(b), a' \sim f(b') \text { where } \sim \in \{ <,=,> \} \}$ (see Fig. 2). It is immediate to check that $[-1,0] Z [0,1]$ (as $f(0) = -1$ and $f(1) = 0$), $M,[-1,0] \Vdash \langle L \rangle p$ (as $M, [0.5, 2] \Vdash p$ because $f(2) = 0.5$), and $M',[0,1] \Vdash \lnot \langle L \rangle p$ (as no interval [c, d], with $c>1$, satisfies p, given that no $c>1$ is in the image of f).

In order to show that Z is a $\mathsf {B E\overline{A E D}}$-bisimulation, consider a pair $([a,b],[a',b'])$ of Z-related intervals. The following chain of double implications holds:

$$\begin{aligned} M,[a,b] \Vdash p \Leftrightarrow a = f(b)\Leftrightarrow a' = f(b')\Leftrightarrow M',[a',b'] \Vdash p. \end{aligned}$$

This implies that the local condition holds.

The proof for the forward condition is technically involved, so we omit its details here and refer the interested reader to “Appendix 11” for the full proof. Since Z is symmetric, the backward condition immediately follows from Proposition 2.

This allows us to conclude that Z is a $\mathsf {B E \overline{A E D}}$-bisimulation that violates $\langle L \rangle$, and thus the thesis. $\square$

Fig. 2

$\mathsf {B E \overline{A E D}}$-bisimulation that violates $\langle L \rangle$, relative to $\mathsf {Den}$

Fig. 3

$\mathsf {O \overline{B E O}}$-bisimulation that violates $\langle L \rangle$, relative to $\mathsf {Den}$

Lemma 8

$\langle L \rangle$ is not definable in $\mathsf {O \overline{B E O}}$ relative to the class $\mathsf {Den}$.

Proof

Consider the two interval models M and $M'$, defined as $M = M' = \langle \mathbb {I(R)}, V \rangle$, where $V(p) = \{[-a,a] \mid a \in {\mathbb {R}} \}$ (observe that no interval [c, d], with $c \ge 0$, satisfies p). Moreover, let $Z = \{ ([a,b],[a',b']) \mid -a \sim b \text { and } -a' \sim b' \text { for some } \sim \in \{ <, =, > \} \}$ (see Fig. 3). It is immediate to check that $[-4,-2] Z [-4,2]$, $M,[-4,-2] \Vdash \langle L \rangle p$ (as $M, [-1, 1] \Vdash p$), and $M',[-4,2] \Vdash \lnot \langle L \rangle p$ (as no interval [c, d], with $c>0$, satisfies p).

To show that Z is an $\mathsf {O\overline{B E O}}$-bisimulation, consider a pair $([a,b],[a',b'])$ of Z-related intervals. The following chain of equivalences hold:

$$\begin{aligned} M,[a,b] \Vdash p \Leftrightarrow -a = b\Leftrightarrow -a' = b' \Leftrightarrow M,[a',b'] \Vdash p. \end{aligned}$$

This implies that the local condition is satisfied.

The proof for the forward condition is technically involved, so we omit its details here and refer the interested reader to “Appendix 12” for the full proof. Since the relation Z is symmetric, by Proposition 2 we have that the backward condition is satisfied as well.

Therefore, Z is an $\mathsf {O \overline{B E O}}$-bisimulation that violates $\langle L \rangle$, and the thesis follows. $\square$

By Proposition 1, Lemma 5, Lemma 7, and Lemma 8, the following corollary holds.

Corollary 4

The following non-definabilities hold relative to the class $\mathsf {Den}$:

• $\langle \overline{L} \rangle$ is not definable in $\mathsf {E A} \overline{\mathsf {E B}}$,

• $\langle \overline{L} \rangle$ is not definable in $\mathsf {E B A} \overline{\mathsf {B D}}$ and

• $\langle \overline{L} \rangle$ is not definable in $\overline{\mathsf {O}} \overline{\mathsf {E B}} \mathsf {O}$.

5.3 Completeness for $\langle E \rangle /\langle \overline{E} \rangle /\langle B \rangle /\langle \overline{B} \rangle$: cases $\mathsf {Lin}$ and $\mathsf {Den}$

Lemma 9

$\langle E \rangle$ is not definable in $\mathsf {A B D O\overline{A B E}}$ relative to the classes $\mathsf {Lin}$ and $\mathsf {Den}$.

Proof

Let $M_1 = \langle {\mathbb {I}}({\mathbb {R}}), V_1 \rangle$ and $M_2 = \langle {\mathbb {I}}({\mathbb {R}}), V_2 \rangle$, where

• p is the only proposition letter of the language,

• the valuation function $V_1: {{\mathcal {AP}}} \rightarrow 2^{{\mathbb {I}}({\mathbb {R}})}$ is defined as: $[x,y] \in V_1(p) \Leftrightarrow x \in {\mathbb {Q}}$ if and only if $y \in {\mathbb {Q}}$, and

• the valuation function $V_2: {{\mathcal {AP}}} \rightarrow 2^{{\mathbb {I}}({\mathbb {R}})}$ is given by: $[w,z] \in V_2(p) \Leftrightarrow w \in {\mathbb {Q}}$ if and only if $z \in {\mathbb {Q}}$, and $[0,3]R_E[w,z]$ does not hold.

Moreover, let Z be a relation between (intervals of) $M_1$ and $M_2$ defined as follows: $[x,y]Z[w,z] {\Leftrightarrow } [x,y] \in V_1(p)$ if and only if $[w,z] \in V_2(p)$. It is easy to verify that [0, 3]Z[0, 3] and $M_1,[0,3] \Vdash \langle E \rangle p$, but $M_2,[0,3] \Vdash \lnot \langle E \rangle p$.

We show now that Z is an $\mathsf {A B D O\overline{A B E}}$-bisimulation between $M_1$ and $M_2$.

The local condition immediately follows from the definition.

The proof for the forward condition is technically involved, so we omit its details here and refer the interested reader to “Appendix 13” for the full proof. The backward condition follows from Proposition 2.

Therefore, Z is an $\mathsf {A B D O\overline{A B E}}$-bisimulation that violates $\langle E \rangle$, and thus the thesis. $\square$

Lemma 10

$\langle \overline{E} \rangle$ is not definable in $\mathsf {A B E\overline{A B D O}}$ relative to the classes $\mathsf {Lin}$ and $\mathsf {Den}$.

Proof

The bisimulation we use to prove this result is very similar to the one used in the proof of Lemma 9, and it is defined as follows. Let $M_1 = \langle {\mathbb {I}}({\mathbb {R}}), V_1 \rangle$ and $M_2 = \langle {\mathbb {I}}({\mathbb {R}}), V_2 \rangle$, where

• p is the only proposition letter of the language,

• the valuation function $V_1: {{\mathcal {AP}}} \rightarrow 2^{{\mathbb {I}}({\mathbb {R}})}$ is defined as: $[x,y] \in V_1(p) \Leftrightarrow x \in {\mathbb {Q}}$ if and only if $y \in {\mathbb {Q}}$, and

• the valuation function $V_2: {{\mathcal {AP}}} \rightarrow 2^{{\mathbb {I}}({\mathbb {R}})}$ is given by: $[w,z] \in V_2(p) \Leftrightarrow w \in {\mathbb {Q}}$ if and only if $z \in {\mathbb {Q}}$, and $[0,3] R_{\overline{E}} [w,z]$ does not hold.

The relation Z is defined exactly as in the proof of Lemma 9: $[x,y] Z [w,z] {\Leftrightarrow } [x,y] \in V_1(p)$ if and only if $[w,z] \in V_2(p)$. Notice that the only difference between the previous bisimulation for $\langle E \rangle$ and the new one for $\langle \overline{E} \rangle$ is in the definition of the valuation function $V_2$: in the former bisimulation, an interval [w, z] satisfies $\lnot p$ if it is a suffix of [0, 3], that is, $[0,3] R_E [w,z]$, in the latter one, [w, z] satisfies $\lnot p$ if [0, 3] is a suffix of it, that is, $[0,3] R_{\overline{E}} [w,z]$.

Following the lines of the proof of Lemma 9, it is not difficult to verify that the newly-defined relation Z is an $\mathsf {A B E \overline{A B D O}}$-bisimulation that violates $\langle \overline{E} \rangle$. The thesis immediately follows. $\square$

The following corollary is an immediate consequence of Proposition 1, Lemma 9, and Lemma 10.

Corollary 5

The following non-definabilities hold relative to the classes $\mathsf {Lin}$ and $\mathsf {Den}$:

• $\langle B \rangle$ is not definable in $\overline{\mathsf {A}} \mathsf {E D} \overline{\mathsf {O}}A \overline{\mathsf {E B}}$ and

• $\langle \overline{B} \rangle$ is not definable in $\overline{\mathsf {A}} \mathsf {E B A} \overline{\mathsf {E D}} \mathsf {O}$.

5.4 Completeness for $\langle A \rangle /\langle \overline{A} \rangle$: cases $\mathsf {Lin}$ and $\mathsf {Den}$

The following property of the set of real numbers ${\mathbb {R}}$ is needed here and in the next subsection: ${\mathbb {R}}$ can be partitioned into any finite or countably infinite number of pairwise disjoint subsets, each one of which is dense in ${\mathbb {R}}$, that is, for each pair of real numbers x and y, and for each set S in the partition of ${\mathbb {R}}$, there exists a real number $w \in S$ such that $x < w < y$. To convince oneself of the validity of such a claim, see, e.g., [30, Thm 7.11], where the property has been proved for ${\mathbb {Q}}$; likewise, it holds for $\overline{\mathbb {Q}}$ and, consequently, for ${\mathbb {R}}$. More formally, the claim is that there are countably many nonempty sets ${\mathbb {R}}_i$ (resp., ${\mathbb {Q}}_i$, $\overline{\mathbb {Q}}_i$), with $i \in {\mathbb {N}}$, such that, for each $i \in {\mathbb {N}}$, ${\mathbb {R}}_i$ (resp., ${\mathbb {Q}}_i$, $\overline{\mathbb {Q}}_i$) is dense in ${\mathbb {R}}$, ${\mathbb {R}} = \bigcup _{i \in {\mathbb {N}}} {\mathbb {R}}_i$ (resp., ${\mathbb {Q}} = \bigcup _{i \in {\mathbb {N}}} {\mathbb {Q}}_i$, $\overline{\mathbb {Q}} = \bigcup _{i \in {\mathbb {N}}} \overline{\mathbb {Q}}_i$), and ${\mathbb {R}}_{i} \cap {\mathbb {R}}_j = \emptyset$, (resp., ${\mathbb {Q}}_{i} \cap {\mathbb {Q}}_j = \emptyset$, $\overline{\mathbb {Q}}_{i} \cap \overline{\mathbb {Q}}_j = \emptyset$), for each $i,j \in {\mathbb {N}}$, with $i \ne j$.

Lemma 11

$\langle A \rangle$ is not definable in $\mathsf {B E\overline{A B E}}$ relative to the classes $\mathsf {Lin}$ and $\mathsf {Den}$.

Proof

Let $M_1 = \langle {\mathbb {I}}({\mathbb {R}}), V_1 \rangle$ and $M_2 = \langle {\mathbb {I}}({\mathbb {R}}), V_2 \rangle$ be two models built on the only proposition letter p. In order to define the valuation functions $V_1$ and $V_2$, we make use of two partitions of the set ${\mathbb {R}}$, one for $M_1$ and the other for $M_2$, each of them consisting of four sets that are dense in ${\mathbb {R}}$. Formally, for $j = 1, 2$ and $i = 1, \ldots , 4$, let ${\mathbb {R}}_j^i$ be dense in ${\mathbb {R}}$. Moreover, for $j = 1, 2$, let ${\mathbb {R}} = \bigcup _{i=1}^4 {\mathbb {R}}_j^i$ and ${\mathbb {R}}_j^i \cap {\mathbb {R}}_j^{i'} = \emptyset$ for each $i,i' \in \{ 1,2,3,4 \}$, with $i \ne i'$. For the sake of simplicity, we impose the two partitions to be equal and thus we can safely omit the subscript, that is, ${\mathbb {R}}_1^{i} = {\mathbb {R}}_2^{i} = {\mathbb {R}}^{i}$ for each $i \in \{ 1,2,3,4 \}$. Thanks to this condition, the bisimulation relation Z, that we define below, is symmetric. We force points in ${\mathbb {R}}^1$ (resp., ${\mathbb {R}}^2$, ${\mathbb {R}}^3$, ${\mathbb {R}}^4$) to behave in the same way with respect to the truth of $p / \lnot p$ over the intervals they initiate and terminate by imposing the following constraints. For $j = 1,2$:

$$\begin{aligned}&\forall x, y \text { } (\text {if } x \in {\mathbb {R}}^1, \text { then } M_j,[x,y] \Vdash \lnot p); \\&\forall x, y \text { } (\text {if } x \in {\mathbb {R}}^2, \text { then } M_j,[x,y] \Vdash \lnot p); \\&\forall x, y \text { } (\text {if } x \in {\mathbb {R}}^3, \text { then } (M_j,[x,y] \Vdash p \text { iff } y \in {\mathbb {R}}^1 \cup {\mathbb {R}}^3)); \\&\forall x, y \text { } (\text {if } x \in {\mathbb {R}}^4, \text { then } (M_j,[x,y] \Vdash p \text { iff } y \in {\mathbb {R}}^2 \cup {\mathbb {R}}^4)). \end{aligned}$$

It can be easily shown that, from the given constraints, it immediately follows that:

$$\begin{aligned}&\forall x, y \text { } (\text {if } y \in {\mathbb {R}}^1, \text { then } (M_j,[x,y] \Vdash p \text { iff } x \in {\mathbb {R}}^3)); \\&\forall x, y \text { } (\text {if } y \in {\mathbb {R}}^2, \text { then } (M_j,[x,y] \Vdash p \text { iff } x \in {\mathbb {R}}^4)); \\&\forall x, y \text { } (\text {if } y \in {\mathbb {R}}^3, \text { then } (M_j,[x,y] \Vdash p \text { iff } x \in {\mathbb {R}}^3)); \\&\forall x, y \text { } (\text {if } y \in {\mathbb {R}}^4, \text { then } (M_j,[x,y] \Vdash p \text { iff } x \in {\mathbb {R}}^4)). \end{aligned}$$

The above constraints together induce the following definition of the valuation functions $V_j(p) : {{\mathcal {AP}}} \rightarrow 2^{{\mathbb {I}}({\mathbb {R}})}$:

$$\begin{aligned}{}[x,y] \in V_j(p) \Leftrightarrow (x \in {\mathbb {R}}^3 \wedge y \in {\mathbb {R}}^1 \cup {\mathbb {R}}^3) \vee (x \in {\mathbb {R}}^4 \wedge y \in {\mathbb {R}}^2 \cup {\mathbb {R}}^4). \end{aligned}$$

Now, let Z be the relation between (intervals of) $M_1$ and $M_2$ defined as follows. Two intervals [x, y] and [w, z] are Z-related if and only if at least one of the following conditions holds:

• 1. $x \in {\mathbb {R}}^1 \cup {\mathbb {R}}^2 \text { and } w \in {\mathbb {R}}^1 \cup {\mathbb {R}}^2;$

• 2. $x \in {\mathbb {R}}^3 \text {, } w \in {\mathbb {R}}^3, \text { and } (y \in {\mathbb {R}}^1 \cup {\mathbb {R}}^3 \text { iff } z \in {\mathbb {R}}^1 \cup {\mathbb {R}}^3);$

• 3. $x \in {\mathbb {R}}^3 \text {, } w \in {\mathbb {R}}^4, \text { and } (y \in {\mathbb {R}}^1 \cup {\mathbb {R}}^3 \text { iff } z \in {\mathbb {R}}^2 \cup {\mathbb {R}}^4);$

• 4. $x \in {\mathbb {R}}^4 \text {, } w \in {\mathbb {R}}^3, \text { and } (y \in {\mathbb {R}}^2 \cup {\mathbb {R}}^4 \text { iff } z \in {\mathbb {R}}^1 \cup {\mathbb {R}}^3);$

• 5. $x \in {\mathbb {R}}^4 \text {, } w \in {\mathbb {R}}^4, \text { and } (y \in {\mathbb {R}}^2 \cup {\mathbb {R}}^4 \text { iff } z \in {\mathbb {R}}^2 \cup {\mathbb {R}}^4).$

It is worth pointing out that two intervals [x, y] and [w, z] that are Z-related are such that if, for instance, both x and w belong to ${\mathbb {R}}^3$ (second clause), then either y and z both occur in odd-numbered partitions or they both occur in even-numbered partitions. Moreover, since the two partitions are equal, Z is symmetric.

Let us consider now two intervals [x, y] and [w, z] such that $x \in {\mathbb {R}}^1$, $w \in {\mathbb {R}}^1$, $y \in {\mathbb {R}}^3$, and $z \in {\mathbb {R}}^1$. By definition of Z, [x, y] and [w, z] are Z-related, and by definition of $V_1$ and $V_2$, there exists $y'> y$ such that $M_1,[y,y'] \Vdash p$, but there is no $z' > z$ such that $M_2,[z,z'] \Vdash p$. Thus, $M_1,[x,y] \Vdash \langle A \rangle p$ and $M_2,[w,z] \Vdash \lnot \langle A \rangle p$ hold.

To complete the proof, it suffices to show that the relation Z is a $\mathsf {B E \overline{A B E}}$-bisimulation. It can be easily checked that every pair ([x, y], [w, z]) of Z-related intervals is such that either $[x,y] \in V_1(p)$ and $[w,z] \in V_2(p)$, or $[x,y] \not \in V_1(p)$ and $[w,z] \not \in V_2(p)$.

The proof for the forward condition is technically involved, so we omit its details here and refer the interested reader to “Appendix 14” for the full proof. The backward condition follows from the forward one, by applying Proposition 2.

Therefore, Z is a $\mathsf {B E\overline{A B E}}$-bisimulation that violates $\langle A \rangle$, and the thesis immediately follows. $\square$

The following corollary follows from Proposition 1 and Lemma 11.

Corollary 6

$\langle \overline{A} \rangle$ is not definable in $\mathsf {E B A \overline{E B}}$ relative to the classes $\mathsf {Lin}$ and $\mathsf {Den}$.

5.5 Completeness for $\langle D \rangle /\langle \overline{D} \rangle /\langle O \rangle /\langle \overline{O} \rangle$: cases $\mathsf {Lin}$ and $\mathsf {Den}$

In this section, we prove our completeness result for $\langle D \rangle$ (Lemma 12 and Corollary 7), $\langle \overline{D} \rangle$ (Lemma 13 and Corollary 8), $\langle O \rangle$ (Lemma 14 and Lemma 15), and $\langle \overline{O} \rangle$ (Corollary 9).

Lemma 12

$\langle D \rangle$ is not definable in $\mathsf {A B O\overline{A B E}}$ relative to the classes $\mathsf {Lin}$ and $\mathsf {Den}$.

Proof

As a first step, we define a pair of functions that will be used in the definition of the models involved in the bisimulation relation Z. Let ${\mathcal {P}}({\mathbb {Q}})= \{{\mathbb {Q}}_q \mid q \in {\mathbb {Q}}\}$ and ${\mathcal {P}}(\overline{\mathbb {Q}}) = \{\overline{\mathbb {Q}}_q \mid q \in {\mathbb {Q}}\}$ be countably infinite partitions of ${\mathbb {Q}}$ and $\overline{\mathbb {Q}}$, respectively, such that for every $q \in {\mathbb {Q}}$, both ${\mathbb {Q}}_q$ and $\overline{\mathbb {Q}}_q$ are dense in ${\mathbb {R}}$. For every $q \in {\mathbb {Q}}$, let ${\mathbb {R}}_q = {\mathbb {Q}}_q \cup \overline{\mathbb {Q}}_q$. We define a function $g: {\mathbb {R}} \rightarrow {\mathbb {Q}}$ that maps every real number x to the index q (a rational number) of the class ${\mathbb {R}}_{q}$ it belongs to. Formally, for every $x \in {\mathbb {R}}$, $g(x) = q$, where $q \in {\mathbb {Q}}$ is the unique rational number such that $x \in {\mathbb {R}}_{q}$. The two functions $f_1: {\mathbb {R}} \rightarrow {\mathbb {Q}}$ and $f_2: {\mathbb {R}} \rightarrow {\mathbb {Q}}$ are defined as follows:

$$\begin{aligned}&f_1(x) = \left\{ \begin{array}{l@{\quad }l} g(x) &{} \text {if } x < g(x) \text {, } x \ne 1, \text { and } x \ne 0 \\ 2 &{} \text {if } x = 1 \\ \lceil x+3 \rceil &{} \text {otherwise} \end{array} \right. \\&f_2(x) = \left\{ \begin{array}{l@{\quad }l} g(x) &{} \text {if } x < g(x) \text { and } x \not \in [0,3) \\ \lceil x+3 \rceil &{} \text {otherwise} \end{array} \right. \end{aligned}$$

It is not difficult to check that the above-defined functions $f_i$, with $i \in \{ 1,2 \}$, satisfy the following properties:

• (i) for every $x \in {\mathbb {R}}$, $f_i(x) > x$,

• (ii) for every $x \in {\mathbb {Q}}$, both $f_i^{-1} (x) \cap {\mathbb {Q}}$ and $f_i^{-1} (x) \cap \overline{{\mathbb {Q}}}$ are left-unbounded (notice that surjectivity of $f_i$ immediately follows), and

• (iii) for every $x,y \in {\mathbb {R}}$, if $x < y$, then there exists $u_1 \in {\mathbb {Q}}$ (resp., $u_2 \in \overline{{\mathbb {Q}}}$) such that $x < u_1 < y$ (resp., $x < u_2 < y$) and $y < f_i(u_1)$ (resp., $y < f_i(u_2)$).

Now, we can define two models $M_1$ and $M_2$, built on the only proposition letter p, as follows: for each $i \in \{ 1,2 \}$, $M_i = \langle {\mathbb {I}}({\mathbb {R}}), V_i \rangle$, where $V_i : {{\mathcal {AP}}} \rightarrow 2^{{\mathbb {I}}({\mathbb {R}})}$ ($i \in \{ 1,2 \}$) is defined as follows: $[x,y] \in V_i(p)\Leftrightarrow y \ge f_i(x)$. Finally, we define the relation Z as:

$$\begin{aligned}{}[x,y]Z[w,z] \Leftrightarrow x \equiv w \text {, } y \equiv z, \quad \text {and }\quad [x,y] \equiv _l [w,z], \end{aligned}$$

where we define $u \equiv v \Leftrightarrow u \in {\mathbb {Q}}$ iff $v \in {\mathbb {Q}}$, and $[u,u'] \equiv _l [v,v'] \Leftrightarrow u' \sim f_1(u)$ and $v' \sim f_2(v)$, for $\sim \in \{<,=,>\}$.

Let us consider the interval [0, 3] in $M_{1}$ and the interval [0, 3] in $M_{2}$. It is immediate to see that these two intervals are Z-related. However, $M_{1},[0,3] \Vdash \langle D \rangle p$ (as $M_{1},[1,2] \Vdash p$), but $M_{2},[0,3] \Vdash \lnot \langle D \rangle p$.

We are left to show that Z is an $\mathsf {A B O\overline{A B E}}$-bisimulation between $M_{1}$ and $M_{2}$. Let [x, y] and [w, z] be two Z-related intervals. By definition, $y \sim f_1(x)$ and $z \sim f_2(w)$ for some $\sim \in \{ <,=,$ $> \}$. If $\sim \in \{=,>\}$, then both [x, y] and [w, z] satisfy p; otherwise, both of them satisfy $\lnot p$. Thus, the local condition is satisfied.

The proof for the forward condition is technically involved, so we omit its details here and refer the interested reader to “Appendix 8” for the full proof. The backward condition can be verified in a very similar way and the details are omitted.

Thus, Z is an $\mathsf {A B O\overline{A B E}}$-bisimulation that violates $\langle D \rangle$, and the thesis follows. $\square$

Since $\mathsf {A B O\overline{A B E}}$ and $\mathsf {A E \overline{A B E O}}$ are dual (and since the dual of $\langle D \rangle$ is $\langle D \rangle$ itself), the following corollary is an immediate consequence of Proposition 1 and Lemma 12.

Corollary 7

$\langle D \rangle$ is not definable in $\mathsf {A E \overline{A B E O}}$ relative to the classes $\mathsf {Lin}$ and $\mathsf {Den}$.

Lemma 13

$\langle \overline{D} \rangle$ is not definable in $\mathsf {A B E \overline{A B O}}$ relative to the classes $\mathsf {Lin}$ and $\mathsf {Den}$.

Proof

The bisimulation we use to prove this result is very similar to the one used to prove Lemma 12, and it is defined as follows. The models $M_1$ and $M_2$ are defined as in the proof of Lemma 12, but they make use of a different pair of functions $f_1$, $f_2$ in the definition of the valuation functions (indeed, in this case, $f_1 = f_2$). Formally, for each $i \in \{ 1,2 \}$, $M_i = \langle {\mathbb {I}}({\mathbb {R}}), V_i \rangle$, where $V_i : {{\mathcal {AP}}} \rightarrow 2^{{\mathbb {I}}({\mathbb {R}})}$ ($i \in \{ 1,2 \}$) is defined as follows: $[x,y] \in V_i(p)\Leftrightarrow y \ge f_i(x)$, where $f_1 (= f_2 ) : {\mathbb {R}} \rightarrow {\mathbb {Q}}$ is such that:

$$\begin{aligned}&f_1(x) = \left\{ \begin{array}{l@{\quad }l} g(x) &{} \text {if } x < g(x) \le 1 \\ \lceil x+1 \rceil &{} \text {otherwise} \end{array} \right. \end{aligned}$$

with g being the same function used before. It is not difficult to check that the newly-defined functions $f_i$ ($i \in \{ 1,2 \}$) satisfy the following properties: (i) for every $x \in {\mathbb {R}}$, $x < f_i(x) < x+2$, (ii) for every $y \in {\mathbb {Q}}$ and every $\epsilon > 0$, there exist $x_1, x_2 \in {\mathbb {Q}}$ and $\overline{x}_1, \overline{x}_2 \in \overline{{\mathbb {Q}}}$ such that $y - 1 < x_1 < \overline{x}_1 < y - 1 + \epsilon$, $y - \epsilon < x_2 < \overline{x}_2 < y$, and $f_i (x_1) = f_i (\overline{x}_1) = f_i (x_2) = f_i (\overline{x}_2) = y$, and (iii) for every $x,y \in {\mathbb {R}}$, if $x < y$, then there exists $u_1 \in {\mathbb {Q}}$ (resp., $u_2 \in \overline{{\mathbb {Q}}}$) such that $x < u_1 < y$ (resp., $x < u_2 < y$) and $y < f(u_1)$ (resp., $y < f(u_2)$). Finally, the relation Z is defined as in the proof of Lemma 12. By following a technique analogous to the one exploited in the proof of Lemma 12, and making use of the properties of $f_1$ and $f_2$, it is not difficult to verify that Z is an $\mathsf {A B E \overline{A B O}}$-bisimulation.

Now, suppose that $0 \in {\mathbb {Q}}_q$, for some $q \in {\mathbb {Q}}$. By property (ii) of $f_1$, there exists $x \in {\mathbb {Q}}$ such that $-0.5 < x < 0$ and $f_1(x) = 0$. Thus, the interval [x, 0.1] in $M_1$ is such that $f_1(x) < 0.1$. Consider the interval [2, 4] in $M_2$. By property (i) of $f_2$, it must be $f_2(2) < 4$. Thus, [x, 0.1]Z[2, 4]. However, on the one hand, $M_1,[x,0.1] \Vdash \langle \overline{D} \rangle \lnot p$, because, for example, by property (ii) of $f_1$, there exists a point $x'$ such that $0.5 < x' < x$ and $f_1(x') = 0.5$. Thus, $[x',0.4]$ is such that $0.4 < f_1(x')$, which means that $M_1, [x',0.4] \Vdash \lnot p$. On the other hand, $M,[2,4] \Vdash \lnot \langle \overline{D} \rangle \lnot p$, because every interval [w, z], with $w < 2 < 4 < z$, is such that $f_2(w) < z$ (as $z > w+2$), and thus $M,[w,z] \Vdash p$. This allows us to conclude that Z is an $\mathsf {A B E \overline{A B O}}$-bisimulation that violates $\langle \overline{D} \rangle$, hence the thesis. $\square$

Since $\mathsf {A B E \overline{A B O}}$ and $\mathsf {A B E O \overline{A E}}$ are dual (and since the dual of $\langle \overline{D} \rangle$ is $\langle \overline{D} \rangle$ itself), the following corollary immediately follows from Proposition 1 and Lemma 13.

Corollary 8

$\langle \overline{D} \rangle$ is not definable in $\mathsf {A B E O \overline{A E}}$ relative to the classes $\mathsf {Lin}$ and $\mathsf {Den}$.

Lemma 14

$\langle O \rangle$ is not definable in $\mathsf {A B E\overline{A E D}}$ relative to the classes $\mathsf {Lin}$ and $\mathsf {Den}$.

Proof

The bisimulation we use here is very similar to those constructed for the modalities $\langle E \rangle$ and $\langle \overline{E} \rangle$ in the proofs of Lemma 9 and Lemma 10, respectively. Let $M_1 = \langle {\mathbb {I}}({\mathbb {R}}), V_1 \rangle$ and $M_2 = \langle {\mathbb {I}}({\mathbb {R}}), V_2 \rangle$ be two models over the set of proposition letters ${{\mathcal {AP}}} = \{p\}$, where the valuation functions $V_1: {{\mathcal {AP}}} \rightarrow 2^{{\mathbb {I}}({\mathbb {R}})}$ and $V_2: {{\mathcal {AP}}} \rightarrow 2^{{\mathbb {I}}({\mathbb {R}})}$ are, respectively, defined as follows:

• $[x,y] \in V_1(p) \Leftrightarrow x \in {\mathbb {Q}}$ iff $y \in {\mathbb {Q}}$, and

• $[w,z] \in V_2(p) \Leftrightarrow w \in {\mathbb {Q}}$ iff $z \in {\mathbb {Q}}$, and $[0,3]R_O[w,z]$ does not hold (that is, it is not the case that $0 < w < 3 < z$).

Then, we define the relation Z between intervals of $M_1$ and intervals of $M_2$ as follows: $[x,y]Z[w,z] \Leftrightarrow [x,y] \in V_1(p)$ iff $[w,z] \in V_2(p)$. It is immediate to see that [0, 3]Z[0, 3], $M_1,[0,3] \Vdash \langle O \rangle p$, but $M_2,[0,3] \Vdash \lnot \langle O \rangle p$.

Let us show that Z is an $\mathsf {A B E \overline{A E D}}$-bisimulation between $M_1$ and $M_2$.

The local condition immediately follows from the definition.

The proof for the forward condition is technically involved, so we omit its details here and refer the interested reader to “Appendix 9” for the full proof. The backward condition can be verified in a very similar way and thus we omit the details.

Therefore, Z is an $\mathsf {A B E\overline{A E D}}$-bisimulation that violates $\langle O \rangle$. The thesis immediately follows. $\square$

Lemma 15

$\langle O \rangle$ is not definable in $\mathsf {A B D\overline{A B E}}$ relative to the classes $\mathsf {Lin}$ and $\mathsf {Den}$.

Proof

The $\mathsf {A B D\overline{A B E}}$-bisimulation that we present here has some similarities with the $\mathsf {A B O\overline{A B E}}$-bisimulation that violates $\langle D \rangle$, presented in the proof of Lemma 12. However, we need to ‘rearrange’ the partitions of ${\mathbb {Q}}$ and $\overline{{\mathbb {Q}}}$ that we exploited in the proof of Lemma 12. More precisely, we still need two infinite and countable partitions ${\mathcal {P}}({\mathbb {Q}})$ of ${\mathbb {Q}}$ and ${\mathcal {P}}(\overline{\mathbb {Q}})$ of $\overline{\mathbb {Q}}$, whose elements are dense in ${\mathbb {R}}$, but it is useful to provide a more suitable enumeration for both of them, as follows: ${\mathcal {P}}({\mathbb {Q}}) = \{ {\mathbb {Q}}_q^c \mid c \in \{a,b\}, q \in {\mathbb {Q}} \}$ and ${\mathcal {P}}(\overline{\mathbb {Q}}) = \{ \overline{\mathbb {Q}}_q^c \mid c \in \{a,b\}, q \in {\mathbb {Q}} \}$. Analogously to Lemma 12, we require these partitions to be such that, for each $c \in \{a,b\}$ and $q \in {\mathbb {Q}}$, sets ${\mathbb {Q}}_q^c$ and $\overline{\mathbb {Q}}_q^c$ are dense in ${\mathbb {R}}$. Now, we define the partition ${\mathcal {P}}({\mathbb {R}})$ of ${\mathbb {R}}$ as: ${\mathcal {P}}({\mathbb {R}}) = \{ {\mathbb {R}}_q^c \mid c \in \{a,b\}, q \in {\mathbb {Q}}\}$, where ${\mathbb {R}}_q^c = {\mathbb {Q}}_q^c \cup \overline{\mathbb {Q}}_q^c$, for each $c \in \{a,b\}$ and $q \in {\mathbb {Q}}$. We use ${\mathbb {Q}}^c$ (resp., $\overline{\mathbb {Q}}^c$, $\mathbb {R}^c$) as an abbreviation for $\bigcup _{q \in {\mathbb {Q}}} {\mathbb {Q}}_q^c$ (resp., $\bigcup _{q \in {\mathbb {Q}}} \overline{\mathbb {Q}}_q^c$, $\bigcup _{q \in {\mathbb {Q}}} {\mathbb {R}}_q^c$), for each $c \in \{a,b\}$. In addition, we define ${\mathcal {S}}_1,{\mathcal {S}}_2 \subseteq {\mathbb {I}}({\mathbb {R}})$ as follows:

$$\begin{aligned} {\mathcal {S}}_1= & {} \{[x,y] \mid x,y \in {\mathbb {R}}^c, c \in \{a,b\} \}, \text { and} \\ {\mathcal {S}}_2= & {} \{[w,z] \mid w,z \in {\mathbb {R}}^c, c \in \{a,b\} \} {\setminus } \{[w,z] \mid 0 < w < 3 < z \}. \end{aligned}$$

Finally, for each $i \in \{1,2\}$, we use $\overline{\mathcal {S}}_i$ to denote the set ${\mathbb {I}}({\mathbb {R}}) {\setminus } {\mathcal {S}}_i$. It is easy to verify that, for every pair of points $x,y \in {\mathbb {I}}({\mathbb {R}})$, if $x < y$, then there exist $y_1,y_2,y_3,y_4 \in {\mathbb {R}}$ such that $x < y_i < y$, for each $i \in \{1,2,3,4\}$, and:

$$\begin{aligned} \begin{aligned}&y_1 \in {\mathbb {Q}} \text { and } [x,y_1] \in {\mathcal {S}}_1 (\text {resp., } {\mathcal {S}}_2 ), \\&y_2 \in {\mathbb {Q}} \text { and } [x,y_2] \in \overline{\mathcal {S}}_1 (\text {resp., } \overline{\mathcal {S}}_2 ), \\&y_3 \in \overline{\mathbb {Q}} \text { and } [x,y_3] \in {\mathcal {S}}_1 (\text {resp., } {\mathcal {S}}_2 ), \\&y_4 \in \overline{\mathbb {Q}} \text { and } [x,y_4] \in \overline{\mathcal {S}}_1 (\text { resp., } \overline{\mathcal {S}}_2). \end{aligned} \end{aligned}$$

(3)

We define now a pair of functions that will be used in the definition of the models involved in the bisimulation relation Z. Let $g: {\mathbb {R}} \rightarrow {\mathbb {Q}}$ be a function defined as follows (notice the strong similarity with the definition of g in Lemma 12): for each $x \in {\mathbb {R}}$, $g(x) = q$, where $q \in {\mathbb {Q}}$ is the unique rational number such that $x \in {\mathbb {R}}_{q}^a \cup R_{q}^b$. The functions $f_1: {\mathbb {R}} \rightarrow {\mathbb {Q}}$ and $f_2: {\mathbb {R}} \rightarrow {\mathbb {Q}}$ are defined as follows:

$$\begin{aligned}&f_1(x) = \left\{ \begin{array}{l@{\quad }l} g(x) &{} \quad \text {if } x < g(x) \\ \lceil x+3 \rceil &{} \quad \text {otherwise} \end{array} \right. \\&f_2(x) = \left\{ \begin{array}{ll} g(x) &{} \quad \text {if } x < g(x) \text { and } ([0,3],[x,g(x)]) \not \in R_O \\ \lceil x+3 \rceil &{} \quad \text {if } x \ge g(x) \text { and } x \not \in (0,3) \\ a_{n'} &{} \quad \text {otherwise} \end{array} \right. \end{aligned}$$

where $a_{n'}$ is the least element of the series $a_n = 3-(\frac{1}{n})$ ($n\ge 1$) such that $x < a_{n'}$. It is not hard to verify that the functions $f_i$ ($i \in \{ 1,2 \}$) fulfill the following conditions:

(i):

$f_i(x) > x$ for every $x \in {\mathbb {R}}$;

(ii):

for each $x \in {\mathbb {Q}}$, $f_i^{-1} (x) \cap {\mathbb {Q}}^a$, $f_i^{-1} (x) \cap {\mathbb {Q}}^b$, $f_i^{-1} (x) \cap \overline{\mathbb {Q}}^a$, and $f_i^{-1} (x) \cap \overline{{\mathbb {Q}}}^b$ are left-unbounded (notice that surjectivity of $f_i$ immediately follows);

(iii):

for each $x,y \in {\mathbb {R}}$, if $x < y$, then there exist:

• $u_1 \in {\mathbb {Q}}^a$ such that $x < u_1 < y$ and $y > f_i(u_1)$,

• $u_2 \in {\mathbb {Q}}^b$ such that $x < u_2 < y$ and $y > f_i(u_2)$,

• $u_3 \in \overline{{\mathbb {Q}}}^a$ such that $x < u_3 < y$ and $y > f_i(u_3)$, and

• $u_4 \in \overline{{\mathbb {Q}}}^b$ such that $x < u_4 < y$ and $y > f_i(u_4)$.

In addition, function $f_2$ satisfies the following property:

(iv):

for each $w \in (0,3)$, $f_2(w) < 3$.

At this point, we are ready to define the models $M_1$ and $M_2$, and the bisimulation relation between their intervals. Let $i \in \{1,2\}$ and $M_{i} = \langle {\mathbb {I}}({\mathbb {R}}), V_{f_i} \rangle$, where the valuation functions $V_{i} : {{\mathcal {AP}}} \rightarrow 2^{{\mathbb {I}}({\mathbb {R}})}$ is defined as follows:

$$\begin{aligned}{}[x,y] \in V_i(p) \Leftrightarrow \text {either } y = f_i(x) \text { or both } y < f_i(x) \text { and } [x,y] \in {\mathcal {S}}_i. \end{aligned}$$

The relation Z is defined as follows:

$$\begin{aligned}{}[x,y]Z[w,z] \Leftrightarrow x \equiv w \text {, } y \equiv z \text {, and } [x,y] \equiv _l [w,z], \end{aligned}$$

where the relations $\equiv$ and $\equiv _l$ are defined, respectively, in the following way:

$$\begin{aligned}&x \equiv w \Leftrightarrow x \in {\mathbb {Q}} \text { iff } w \in {\mathbb {Q}} \\&[x,y] \equiv _l [w,z] \Leftrightarrow \left\{ \begin{array}{l@{\quad }l} \text {either} &{} y > f_1(x) \text { and } z > f_2(w) \\ \text {or} &{} y = f_1(x) \text { and } z = f_2(w) \\ \text {or} &{} y < f_1(x) \text {, } z < f_2(w) \text {, and } ([x,y] \in {\mathcal {S}}_1 \text { iff } [w,z] \in {\mathcal {S}}_2) \end{array} \right. \end{aligned}$$

Now, by the definition of Z, we have that [0, 3]Z[0, 3] (notice that this is also a consequence of the facts that $f_1(0) = f_2(0)$ and $[0,3]R_O[0,3]$ does not hold). Moreover, it is easy to see that $M_{1},[0,3] \Vdash \langle O \rangle p$, while $M_{2},[0,3] \Vdash \lnot \langle O \rangle p$ (this is a direct consequence of property (iv) of $f_2$ and of the fact that $f_1(x) > 3$ for some $x \in (0,3)$).

We show that Z is an $\mathsf {A B D\overline{A B E}}$- bisimulation.

For the local condition, consider two intervals [x, y] and [w, z] such that [x, y]Z[w, z]. First, we assume that $[x,y] \in V_1(p)$ and we show that $[w,z] \in V_2(p)$ follows. Since $[x,y] \in V_1(p)$, either $y = f_1(x)$ holds or both $y < f_1(x)$ and $[x,y] \in {\mathcal {S}}_1$ hold. In the former case, by the definition of Z, it must be $z = f_2(w)$, which implies $[w,z] \in V_2(p)$. In the latter case, by the definition of Z, both $z < f_2(w)$ and $[w,z] \in {\mathcal {S}}_2$ hold, and thus $[w,z] \in V_2(p)$. Second, we assume that $[w,z] \in V_2(p)$ and we show that $[x,y] \in V_1(p)$ follows. Since $[w,z] \in V_2(p)$, either $z = f_2(w)$ holds or both $z < f_2(w)$ and $[w,z] \in {\mathcal {S}}_2$ hold. In the former case, by the definition of Z, it must be $y = f_1(x)$, which implies $[x,y] \in V_1(p)$. In the latter case, by the definition of Z, both $y < f_1(x)$ and $[x,y] \in {\mathcal {S}}_1$ hold, and thus $[x,y] \in V_1(p)$.

The proof for the forward condition is technically involved, so we omit its details here and refer the interested reader to “Appendix 10” for the full proof. The backward condition can be verified in a very similar way and thus we omit the details.

Therefore, Z is an $\mathsf {A B D\overline{A B E}}$-bisimulation that violates $\langle O \rangle$, hence the thesis. $\square$

The following corollary follows from Proposition 1, Lemma 14, and Lemma 15.

Corollary 9

The following non-definabilities hold relative to the classes $\mathsf {Lin}$ and $\mathsf {Den}$:

• $\langle \overline{O} \rangle$ is not definable in $\overline{\mathsf {A}} \mathsf {E B A} \overline{\mathsf {B D}}$ and

• $\langle \overline{O} \rangle$ is not definable in $\overline{\mathsf {A}} \mathsf {E D A} \overline{\mathsf {E D}}$.

6 Harvest

In this paper, we have compared and classified all fragments of HS with respect to their expressiveness, relative to the class of all linear orders and its subclass containing all dense linear orders. For each of these classes, we have identified a complete set of definabilities among HS modalities, valid in that class, thus obtaining a complete classification of the family of all $2^{12}=4096$ fragments of HS with respect to their expressive power. The final outcome is that there are exactly 1347 expressively different fragments of HS, when we interpret them over the class of all linear orders, while such a number reduces to 966, when we restrict our attention to the subclass of all dense linear orders. Formally, the collection of results shown in the previous sections enables us to prove the following theorem.

Theorem 1

Table 1 presents a complete set of optimal definabilities relative to:

• the class $\mathsf {Lin}$ (definabilities in the groups on the top and in middle);

• the class $\mathsf {Den}$, and, in general, every (left/right) symmetric class of dense linear orders containing at least one linear order isomorphic to ${\mathbb {R}}$ or to ${\mathbb {Q}}$ (all the definabilities).

Proof

For the class $\mathsf {Lin}$, the class $\mathsf {Den}$, and all symmetric classes of dense linear orders containing at least a linear order isomorphic to ${\mathbb {R}}$, the result is an immediate consequence of the results in Sects. 4 and  5. As for other symmetric classes of linear orders containing at least a linear order isomorphic to ${\mathbb {Q}}$, it is enough to observe that we have never made use of the Dedekind-completeness property (that distinguishes between ${\mathbb {Q}}$ and ${\mathbb {R}}$) and that, consequently, all the constructions given in Sect. 5 with respect to ${\mathbb {R}}$ can be easily adapted to ${\mathbb {Q}}$ instead. $\square$

The proposed set of definability equations and the resulting classification of HS fragments are not appropriate any more if we change the semantics (from strict to non-strict) or if we interpret HS fragments over a different class of linear orders. For instance, if the non-strict semantics is assumed, then $\langle A \rangle$ (resp., $\langle \overline{A} \rangle$) can be defined in $\overline{\mathsf {B}} \mathsf {E}$ (resp., $\mathsf {B} \overline{\mathsf {E}}$), as shown in [33]. Similarly, if we commit to the strict semantics, but we restrict our attention to the class of all discrete linear orders, $\langle A \rangle$ can be defined in $\overline{\mathsf {B}} \mathsf {E}$ as well: $\langle A \rangle p \equiv \varphi (p) \vee \langle E \rangle \varphi (p)$, where $\varphi (p)$ is a shorthand for $[ E ] \bot \wedge \langle \overline{B} \rangle ([ E ] [ E ] \bot \wedge \langle E \rangle (p \vee \langle \overline{B} \rangle p))$; likewise, $\langle \overline{A} \rangle$ is definable in $\mathsf {B} \overline{\mathsf {E}}$.

The classification of the expressive power of HS fragments with respect to other interesting classes of linear orderings, such as the class of all finite linear orders and the class of all discrete linear orders, is currently under investigation and will be reported in a forthcoming publication (see [3] for some results in this direction). The classification of HS fragments with respect to the various classes of linear orders when the non-strict semantics is assumed, as well as that of HS fragments enriched with point-based modalities borrowed from classical temporal logics [20], are still open problems. As a further research direction, it would also be natural to study extensions of classic logical formalisms with Allen’s relations between intervals. As a contribution to that line of research, Conradie and Sciavicco identify in [17] the set of expressively different extensions of first-order logic with Allen’s relations between intervals.

Appendices

Appendix 1: Complete proof of Lemma 2

Lemma 2 (Soundness for $\langle L \rangle$ over $\mathsf {Den}$) The following definabilities hold relative to the class $\mathsf {Den}$:

• $\langle L \rangle$  is definable in $\mathsf {D O}$,

• $\langle L \rangle$  is definable in $\overline{\mathsf {B}}\mathsf {D}$,

• $\langle L \rangle$  is definable in $\mathsf {E O}$,

• $\langle L \rangle$  is definable in $\mathsf {B O}$ and

• $\langle L \rangle$  is definable in $\overline{\mathsf {L}}\mathsf {O}$.

Proof

The proof of the first claim is on page 11 in the main body of the paper. Consider now the definability equation $\langle L \rangle p \equiv \langle \overline{B} \rangle [ D ] \langle \overline{B} \rangle \langle D \rangle \langle \overline{B} \rangle p$. Suppose that $M,[a,b] \Vdash \langle L \rangle p$ for an interval [a, b] in a model M. Thus, as before, there exists an interval [c, d] in M such that $b < c$ and $M,[c,d] \Vdash p$. By definition of $R_{\overline{B}}$, it holds that $[a,b] R_{\overline{B}} [a,c]$. We now show that [a, c] satisfies $[ D ] \langle \overline{B} \rangle \langle D \rangle \langle \overline{B} \rangle p$. First, every interval [e, f], with $[a,c] R_D [e,f]$, is such that $e < c$. We claim that $M,[e,f] \Vdash \langle \overline{B} \rangle \langle D \rangle \langle \overline{B} \rangle p$. To see this, let us consider the interval [e, d]. We observe that $[e,f] R_{\overline{B}} [e,d]$ holds. Moreover, by the density of M, there exists a point $d'$, with $c < d' < d$, such that $[e,d] R_{D} [c,d']$ holds and $[c,d']$ satisfies $\langle \overline{B} \rangle p$, because p holds over [c, d] and $[c,d'] R_{\overline{B}} [c,d]$. Thus, $M,[e,f] \Vdash \langle \overline{B} \rangle \langle D \rangle \langle \overline{B} \rangle p$, as claimed.

As for the opposite direction, suppose that $M,[a,b] \Vdash \langle \overline{B} \rangle [ D ] \langle \overline{B} \rangle \langle D \rangle \langle \overline{B} \rangle p$ for an interval [a, b] in a model M. That means that there exists a point $c > b$ such that the interval [a, c] satisfies $[ D ] \langle \overline{B} \rangle \langle D \rangle \langle \overline{B} \rangle p$. As a particular instance of the latter formula, every interval [e, f] such that $b < e < f < c$ (the existence of such an interval [e, f] is guaranteed by the density of M) must satisfy $\langle \overline{B} \rangle \langle D \rangle \langle \overline{B} \rangle p$ which means that there exists a point $g > f$ such that $M,[e,g] \Vdash \langle D \rangle \langle \overline{B} \rangle p$, which implies, in turn, the existence of two points h, i, with $e < h < i$, such that $M,[h,i] \Vdash p$. Since $h>b$, we have that $M,[a,b] \Vdash \langle L \rangle p$.

Next, let us focus on $\langle L \rangle p \equiv \langle O \rangle [ E ] \langle O \rangle \langle O \rangle p$. Suppose that $M,[a,b] \Vdash \langle L \rangle p$ for an interval [a, b] in a model M. Once again, this means that there exists an interval [c, d] in M such that $b < c$ and $M,[c,d] \Vdash p$. Consider an interval $[a',c]$, with $a < a' < b$ (the existence of such a point $a'$ is guaranteed by the density of M). It holds that $[a,b] R_O [a',c]$. We prove that $M,[a',c] \Vdash [ E ] \langle O \rangle \langle O \rangle p$. Indeed, for every interval [e, c], with $[a',c] R_E [e,c]$, by the density of M, there exist a point f, with $e < f < c$, and a point g, with $c < g < d$, such that the interval [f, g] satisfies $\langle O \rangle p$ as $[f,g] R_O [c,d]$. Thus, $M,[e,c] \Vdash \langle O \rangle \langle O \rangle p$, $M,[a',c] \Vdash [ E ] \langle O \rangle \langle O \rangle p$, and $M,[a,b] \Vdash \langle O \rangle [ E ] \langle O \rangle \langle O \rangle p$.

In order to prove the converse direction, suppose that $M,[a,b] \Vdash \langle O \rangle [ E ] \langle O \rangle \langle O \rangle p$ for an interval [a, b] in a model M. That means that there exists an interval [c, d] such that $[a,b] R_O [c,d]$ and $M,[c,d] \Vdash [ E ] \langle O \rangle \langle O \rangle p$. As a particular instance, the interval [e, d], for some e such that $b < e < d$ (the existence of such a point e is guaranteed by the density of M), satisfies $\langle O \rangle \langle O \rangle p$, that implies the existence of an interval [f, g], with $f > e$ $(> b)$, satisfying p. It immediately follows that $M,[a,b] \Vdash \langle L \rangle p$.

Consider now $\langle L \rangle p \equiv \langle O \rangle (\langle O \rangle \top \wedge [ O ] \langle B \rangle \langle O \rangle \langle O \rangle p )$. Suppose that $M,[a,b] \Vdash \langle L \rangle p$ for an interval [a, b] in a model M, which implies, as before, that there exists an interval [c, d] in M such that $b < c$ and $M,[c,d] \Vdash p$. Consider an interval $[a',c]$, with $a < a' < b$ (the existence of such a point $a'$ is guaranteed by the density of M). This interval is such that $[a,b] R_O [a',c]$ and it satisfies:

• $\langle O \rangle \top$, as $[a',c] R_O [b,d]$, and

• $[ O ] \langle B \rangle \langle O \rangle \langle O \rangle p$, as every interval [e, f], with $[a',c] R_O [e,f]$, is such that $e < c < f$; thus, the interval [e, c] is such that $[e,f] R_B [e,c]$, and, by the density of M, there exists an interval [g, h] such that $[e,c] R_O [g,h]$ and $[g,h] R_O [c,d]$, and this implies $M,[e,c] \Vdash \langle O \rangle \langle O \rangle p$, which in turn implies $M,[a',c] \Vdash [ O ] \langle B \rangle \langle O \rangle \langle O \rangle p$.

Hence, $M,[a',c] \Vdash \langle O \rangle \top \wedge [ O ] \langle B \rangle \langle O \rangle \langle O \rangle p$, and thus $M,[a,b] \Vdash \langle O \rangle (\langle O \rangle \top \wedge [ O ] \langle B \rangle \langle O \rangle \langle O \rangle p)$.

Conversely, suppose that $M,[a,b] \Vdash \langle O \rangle (\langle O \rangle \top \wedge [ O ] \langle B \rangle \langle O \rangle \langle O \rangle p )$ for an interval [a, b] in a model M. That means that there exists an interval [c, d] such that:

• $[a,b] R_O [c,d]$,

• $M,[c,d] \Vdash \langle O \rangle \top$, and thus there exists a point $f > d$, and

• $M,[c,d] \Vdash [ O ] \langle B \rangle \langle O \rangle \langle O \rangle p$.

By the density of M, there exists a point e, with $b < e < d$. The interval [e, f] is such that $[c,d] R_O [e,f]$, and thus, by the third condition above, it satisfies $\langle B \rangle \langle O \rangle \langle O \rangle p$, which implies the existence of an interval [g, h], with $g > e (> b)$, satisfying p. It immediately follows that $M,[a,b] \Vdash \langle L \rangle p$.

Finally, consider $\langle L \rangle p \equiv \langle O \rangle (\langle O \rangle \top \wedge [ O ] [ \overline{L} ] \langle O \rangle \langle O \rangle p)$. Suppose that M, [a,  $b] \Vdash \langle L \rangle p$ for an interval [a, b] in a model M. Thus, there exists an interval [c, d] in M such that $b < c$ and $M,[c,d] \Vdash p$. Consider an interval $[a',c]$, with $a < a' < b$ (the existence of such a point $a'$ is guaranteed by the density of M). This interval is such that $[a,b] R_O [a',c]$ and it satisfies both $\langle O \rangle \top$, as $[a',c] R_O [b,d]$, and $[ O ] [ \overline{L} ] \langle O \rangle \langle O \rangle p$, thanks to the following argument. Every interval [e, f], with $[a',c] R_O [e,f]$, is such that $e < c$. Thus, every interval [g, h], with $[e,f] R_{\overline{L}} [g,h]$, satisfies $\langle O \rangle \langle O \rangle p$ (by the density of M, there exist $g < i < h$ and $c < j < d$ such that both $[g,h] R_O [i,j]$ and $[i,j] R_O [c,d]$ hold). Therefore, we have that $M,[a',c] \Vdash [ O ] [ \overline{L} ] \langle O \rangle \langle O \rangle p$, which implies $M,[a,b] \Vdash \langle O \rangle (\langle O \rangle \top \wedge [ O ] [ \overline{L} ] \langle O \rangle \langle O \rangle p)$.

As for the other direction, suppose that $M,[a,b] \Vdash \langle O \rangle (\langle O \rangle \top \wedge [ O ] [ \overline{L} ] \langle O \rangle \langle O \rangle p)$ for an interval [a, b] in a model M. That means that there exists an interval [c, d] such that $[a,b] R_O [c,d]$, $M, [c,d] \Vdash \langle O \rangle \top$ (and thus, there exists a point $f > d$), and that $M, [c,d] \Vdash [ O ] [ \overline{L} ] \langle O \rangle \langle O \rangle p$. As a specific instance, consider the interval [e, f], for some e such that $b < e < d$ (the existence of such a point e is guaranteed by the density of M). Since $[c,d] R_O [e,f]$, then we have $M, [e,f] \Vdash [ \overline{L} ] \langle O \rangle \langle O \rangle p$, which in turn, together with the density assumption, implies the existence of an interval [g, h], with $b < g < h < e$, that satisfies $\langle O \rangle \langle O \rangle p$. Thus, there exists an interval [i, j], with $i > g (> b)$, which satisfies p. It immediately follows that $M,[a,b] \Vdash \langle L \rangle p$. $\square$

Appendix 2: Complete proof of Lemma 7

Lemma 7 $\langle L \rangle$ is not definable in $\mathsf {B E\overline{A E D}}$ relative to the class $\mathsf {Den}$.

Proof

Consider two interval models M and $M'$, defined as $M = M' = \langle \mathbb {I(R)}, V \rangle$, where $V(p) = \{[a,b] \mid a = f(b) \}$ and where f is the function defined at the beginning of Sect. 5.2. In addition, let $Z = \{ ([a,b],[a',b']) \mid a \sim f(b), a' \sim f(b') \text { where } \sim \in \{ <,=,> \} \}$ (see Fig. 2). It is immediate to check that $[-1,0] Z [0,1]$ (as $f(0) = -1$ and $f(1) = 0$), that $M,[-1,0] \Vdash \langle L \rangle p$ (as $M, [0.5, 2] \Vdash p$ because $f(2) = 0.5$) and that $M',[0,1] \Vdash \lnot \langle L \rangle p$ (as no interval [c, d], with $c>1$, satisfies p because c is not in the image of f for each $c>1$). Now, in order to show that Z is a $\mathsf {B E\overline{A E D}}$-bisimulation, consider a pair $([a,b],[a',b'])$ of Z-related intervals. The following chain of double implications holds:

$$\begin{aligned} M,[a,b] \Vdash p \Leftrightarrow a = f(b)\Leftrightarrow a' = f(b')\Leftrightarrow M',[a',b'] \Vdash p. \end{aligned}$$

This implies that the local condition holds. As for the forward condition, consider three intervals [a, b], $[a',b']$, and [c, d] such that $[a,b]Z[a',b']$ and $[a,b]R_X[c,d]$ for some $X \in \{ B, E, \overline{A}, \overline{E}, \overline{D} \}$. We need to exhibit an interval $[c',d']$ such that $[a',b'] R_X [c',d']$ and $[c,d] Z [c',d']$. We distinguish three cases.

• If $a > f(b)$ and $a' > f(b')$, then we distinguish the following sub-cases.

  • If $X = B$, then [c, d] is such that $a = c < d < b$. By the monotonicity of f, we have that $f(d) < f(b) < a = c$. Moreover, by the monotonicity of f, for every interval $[c',d']$, with $[a',b']R_B[c',d']$, $f(d') < c'$ holds, and thus $[c,d] Z [c',d']$.

  • If $X = E$, then [c, d] is such that $a < c < b = d$. Thus, $f(d) = f(b) < a < c$. For every interval $[c',d']$, with $[a',b']R_E[c',d']$, $f(d') < c'$ holds, and thus $[c,d] Z [c',d']$.

  • If $X = \overline{A}$, then [c, d] is such that $c < d = a$. Now, if $c < f(d) = f(a)$, then, by the definition of f and Lemma 6, there exists a point $c'$ such that $c' < f(a') < a'$. Thus, the interval $[c',d']$, with $d' = a'$, is such that $[a',b'] R_{\overline{A}} [c',d']$ and $[c,d] Z [c',d']$. If $c = f(d) = f(a)$, then take $c' =$ $f(a')$ $< a'$. The interval $[c',d']$, with $d' = a'$, is such that $[a',b'] R_{\overline{A}} [c',d']$ and $[c,d] Z [c',d']$. If $c > f(d) = f(a)$, then, by the density of ${\mathbb {R}}$, the definition of f, and Lemma 6, there exists a point $c'$ such that $f(a') < c' < a'$. The interval $[c',d']$, with $d' = a'$, is such that $[a',b'] R_{\overline{A}} [c',d']$ and $[c,d] Z [c',d']$.

  • If $X = \overline{E}$, then [c, d] is such that $c < a < b = d$. There are three possibilities. If $c < f(d)$, then, by the definition of f, there exists a point $c'$ such that $c' < f(b') < a'$. Thus, the interval $[c',d']$, with $d' = b'$, is such that $[a',b'] R_{\overline{E}} [c',d']$ and $[c,d] Z [c',d']$. If $c = f(d)$, then the interval $[c',d']$, with $d' = b'$ and $c' = f(d')$, is such that $[a',b'] R_{\overline{E}} [c',d']$ and $[c,d] Z [c',d']$. If $c > f(d)$, then, by the density of ${\mathbb {R}}$, there exists a point $c'$ such that $f(b') < c' < a'$, and the interval $[c',d']$, with $d' = b'$, is such that $[a',b'] R_{\overline{E}} [c',d']$ and $[c,d] Z [c',d']$.

  • If $X = \overline{D}$, then [c, d] is such that $c < a < b < d$. If $c < f(d)$, then, take $c' = f(a')$ and any $d' > b'$. The interval $[c',d']$ is such that $[a',b'] R_{\overline{D}} [c',d']$ and $[c,d] Z [c',d']$. If $c = f(d)$ (resp., $c > f(d)$), then, by the density of ${\mathbb {R}}$ and the monotonicity and the surjectivity of f, there exist two points $c',d'$ such that $c' < a' < b' < d'$ and $c' = f(d')$ (resp., $c' > f(d')$). Thus, the interval $[c',d']$ is such that $[a',b'] R_{\overline{D}} [c',d']$ and $[c,d] Z [c',d']$.

• If $a < f(b)$ and $a' < f(b')$, then we distinguish the following sub-cases.

  • If $X = B$, then [c, d] is such that $a = c < d < b$. Now, if $c < f(d)$ (resp., $c = f(d)$, $c > f(d)$), then, by the density of ${\mathbb {R}}$ and by the monotonicity and the surjectivity of f, there exists a point $d'$ such that $a' < d' < b'$ and $a' < f(d')$ (resp., $a' = f(d')$, $a' > f(d')$). Thus, the interval $[c',d']$, with $c' = a'$, is such that $[a',b'] R_{B} [c',d']$ and $[c,d] Z [c',d']$.

  • If $X = E$, then [c, d] is such that $a < c < b = d$. Now, if $c < f(d)$ (resp., $c = f(d)$, $c > f(d)$), then, by the density of ${\mathbb {R}}$, there exists a point $c'$ such that $a' < c' < b'$ and $c' < f(b')$ (resp., $c' = f(b')$, $c' > f(b')$). Thus, the interval $[c',d']$, with $d' = b'$, is such that $[a',b'] R_{E} [c',d']$ and $[c,d] Z [c',d']$.

  • If $X = \overline{A}$, then the same argument of the case when $a > f(b)$ and $a' > f(b')$ (and $X = \overline{A}$) applies.

  • If $X = \overline{E}$, then [c, d] is such that $c < a < b = d$. Thus, $c < a < f(b) = f(d)$. For every interval $[c',d']$, with $[a',b']R_{\overline{E}}[c',d']$, it holds $c' < f(d')$, and thus $[c,d] Z [c',d']$.

  • If $X = \overline{D}$, then [c, d] is such that $c < a < b < d$. Thus, by the monotonicity of f, $c < a < f(b) < f(d)$ holds. For every interval $[c',d']$, with $[a',b']R_{\overline{D}}[c',d']$, it holds, by the monotonicity of f, that $c' < f(d')$, and thus $[c,d] Z [c',d']$.

• If $a = f(b)$ and $a' = f(b')$, then we distinguish the following sub-cases.

  • If $X = B$, then [c, d] is such that $a = c < d < b$. Thus, $f(d) < f(b) = a = c$ holds by the monotonicity of f. For every interval $[c',d']$, with $[a',b']R_{B}[c',d']$, by the monotonicity of f, we have that $f(d') < c'$, and thus $[c,d] Z [c',d']$.

  • If $X = E$, then [c, d] is such that $a < c < b = d$. Thus, $c > a = f(b) = f(d)$ holds. For every interval $[c',d']$, with $[a',b']R_{E}[c',d']$, we have that $c' > f(d')$, and thus $[c,d] Z [c',d']$.

  • If $X = \overline{A}$, then the same argument of the case when $a > f(b)$ and $a' > f(b')$ (and $X = \overline{A}$) applies.

  • If $X = \overline{E}$, then [c, d] is such that $c < a < b = d$. Thus, $c < a = f(b) = f(d)$. For every interval $[c',d']$, with $[a',b']R_{\overline{E}}[c',d']$, $c' < f(d')$ holds, and thus $[c,d] Z [c',d']$.

  • If $X = \overline{D}$, then [c, d] is such that $c < a < b < d$. Thus, $c < a = f(b) < f(d)$ holds by the monotonicity of f. For every interval $[c',d']$, with $[a',b']R_{\overline{D}}[c',d']$, by the monotonicity of f, we have that $c' < f(d')$, and thus $[c,d] Z [c',d']$.

Since Z is symmetric, the backward condition immediately follows from Proposition 2. Therefore, Z is a $\mathsf {B E \overline{A E D}}$-bisimulation that violates $\langle L \rangle$, hence the thesis. $\square$

Appendix 3: Complete proof of Lemma 8

Lemma 8 $\langle L \rangle$ is not definable in $\mathsf {O \overline{B E O}}$ relative to the class $\mathsf {Den}$.

Proof

Consider the two interval models M and $M'$, defined as $M = M' = \langle \mathbb {I(R)}, V \rangle$, where $V(p) = \{[-a,a] \mid a \in {\mathbb {R}} \}$ (observe that no interval [c, d], with $c \ge 0$, satisfies p). Moreover, let $Z = \{ ([a,b],[a',b']) \mid -a \sim b \text { and } -a' \sim b' \text { for some } \sim \in \{ <, =, > \} \}$ (see Fig. 3). It is immediate to check that $[-4,-2] Z [-4,2]$, that $M,[-4,-2] \Vdash \langle L \rangle p$ (as $M, [-1, 1] \Vdash p$) and that $M',[-4,2] \Vdash \lnot \langle L \rangle p$ (as no interval [c, d], with $c>0$, satisfies p). In order to complete the proof for this fragment, we now proceed to show that Z is an $\mathsf {O\overline{B E O}}$-bisimulation. To this end, consider a pair $([a,b],[a',b'])$ of Z-related intervals. The following chain of equivalences hold:

$$\begin{aligned} M,[a,b] \Vdash p \Leftrightarrow -a = b\Leftrightarrow -a' = b' \Leftrightarrow M,[a',b'] \Vdash p. \end{aligned}$$

This implies that the local condition is satisfied. As for the forward condition, consider three intervals [a, b], $[a',b']$, and [c, d] such that $[a,b]Z[a',b']$ and $[a,b]R_X[c,d]$ for some $X \in \{ O, \overline{B}, \overline{E}, \overline{O} \}$. We need to exhibit an interval $[c',d']$ such that $[a',b'] R_X [c',d']$ and $[c,d] Z [c',d']$. We distinguish three cases.

• If $-a > b$ and $-a' > b'$, then, as a preliminary step, we show that the following facts hold: $(i)\, a < 0$ and $a' < 0$; $(ii)\,|a| > |b|$ and $|a'| > |b'|$. We only show the proofs for $a < 0$ and $|a| > |b|$ and we omit the ones for $a' < 0$ and $|a'| > |b|$, which are analogous. As for the former claim above, it is enough to observe that, if $a \ge 0$, then $a \ge 0 \ge -a > b$, which implies $b < a$, leading to a contradiction with the fact that [a, b] is an interval (thus $a < b$). Notice that, as an immediate consequence, we have that $|a| = -a$ holds. As for the latter claim above, firstly we suppose, by contradiction, that $|a| = |b|$ holds. Then, $-a = |a| = |b|$ holds and this implies either $b = -a$, contradicting the hypothesis that $-a > b$, or $b = a$, contradicting the fact that [a, b] is an interval. Secondly, we suppose, again by contradiction, that $|a| < |b|$ holds. Then, by the former claim, we have that $0 < -a = |a| < |b|$ holds, which implies $b \ne 0$. Now, we show that both $b < 0$ and $b > 0$ lead to a contradiction. If $b < 0$, then $|b| = -b$, and thus it holds $-a < -b$, which amounts to $a > b$, contradicting the fact that [a, b] is an interval. If $b > 0$, then $|b| = b$, and thus $-a < b$ holds, which contradicts the hypothesis that $-a > b$. This proves the two claims above. Now, we distinguish the following sub-cases.

  • If $X = O$, then [c, d] is such that $a < c < b < d$. We distinguish the following cases.

    • If $-c > d$, then take some $c'$ such that $a' < c' < -|b'| < 0$ (notice also that $c' < -|b'| \le b'$ trivially holds), and $d'$ such that $b' < d' < |c'| = -c'$ (the existence of such points $c',d'$ is guaranteed by the density of ${\mathbb {R}}$). The interval $[c',d']$ is such that $[a',b'] R_O [c',d']$ and $[c,d] Z [c',d']$.

    • If $-c = d$, then take some $c'$ such that $a' < c' < -|b'| < 0$, and $d' = -c'$ (the existence of such a point $c'$ is guaranteed by the density of ${\mathbb {R}}$). The interval $[c',d']$ is such that $[a',b'] R_O [c',d']$ and $[c,d] Z [c',d']$.

    • If $-c < d$, then take $c'$ such that $a' < c' < -|b'| < 0$, and any $d' > -c'$ (the existence of such a point $c'$ is guaranteed by the density of ${\mathbb {R}}$). The interval $[c',d']$ is such that $[a',b'] R_O [c',d']$ and $[c,d] Z [c',d']$.

  • If $X = \overline{B}$, then [c, d] is such that $a = c < b < d$. We distinguish the cases below.

    • If $-c > d$, then take $c' = a'$ and $d'$ such that $b' < d' < -a' = -c'$ (the existence of such a point $d'$ is guaranteed by the density of ${\mathbb {R}}$). The interval $[c',d']$ is such that $[a',b'] R_{\overline{B}} [c',d']$ and $[c,d] Z [c',d']$.

    • If $-c = d$, then take $c' = a'$ and $d' = -c' (= -a' > b')$. The interval $[c',d']$ is such that $[a',b'] R_{\overline{B}} [c',d']$ and $[c,d] Z [c',d']$.

    • If $-c < d$, then take $c' = a'$ and any $d' > -c' (= -a' > b')$. The interval $[c',d']$ is such that $[a',b'] R_{\overline{B}} [c',d']$ and $[c,d] Z [c',d']$.

  • If $X = \overline{E}$, then [c, d] is such that $c < a < b = d$. Notice that $|c| = -c > -a = |a|$ holds, because $c < a < 0$. Thus $-c > -a > b = d$ also holds. Then, take $d' = b'$ and any $c' < a'$. We have that $-c' > -a' > b' = d'$. The interval $[c',d']$ is therefore such that $[a',b'] R_{\overline{E}} [c',d']$ and $[c,d] Z [c',d']$.

  • If $X = \overline{O}$, then [c, d] is such that $c < a < d < b$. Notice that $|c| = -c > -a = |a|$ holds, because $c < a < 0$. Thus $-c > -a > b > d$ also holds. Then, take some $d'$ such that $a' < d' < b'$ and any $c' < a'$ (the existence of such a point $d'$ is guaranteed by the density of ${\mathbb {R}}$). Thus, it holds $-c' > -a' > b' > d'$. The interval $[c',d']$ is therefore such that $[a',b'] R_{\overline{O}} [c',d']$ and $[c,d] Z [c',d']$.

• If $-a = b$ and $-a' = b'$, then we have that $a < 0$ (resp., $a' < 0$) and $b > 0$ (resp., $b' > 0$). Indeed, if $a \ge 0$ held, then $b = -a \le 0 \le a$ would also hold, contradicting the fact that [a, b] is an interval (and thus $b > a$). From $a < 0$ and $-a = b$, it immediately follows that $b > 0$. The facts that $a' < 0$ and $b' > 0$ can be shown analogously. Notice also that, from $-a = b$ and $-a' = b'$, it follows that $|a| = |b|$ and $|a'| = |b'|$. Now, we distinguish the following sub-cases.

  • If $X = O$, then [c, d] is such that $a < c < b < d$. Notice that $-c \le |c| < |a| = |b| = b < d$ holds. Then, take $c' = 0$ and any $d' > b' (> 0)$. We have that $-c' < d'$. The interval $[c',d']$ is such that $[a',b'] R_{O} [c',d']$ and $[c,d] Z [c',d']$.

  • If $X = \overline{B}$, then [c, d] is such that $a = c < b < d$. Notice that $-c = - a = b < d$ holds. Then, take $c' = a'$ and any $d' > b'$. We have that $-c' = -a' = b' < d'$. The interval $[c',d']$ is such that $[a',b'] R_{\overline{B}} [c',d']$ and $[c,d] Z [c',d']$.

  • If $X = \overline{E}$, then [c, d] is such that $c < a < b = d$. Notice that $|c| = -c > -a = |a|$ holds, because $c < a < 0$. Thus $-c > -a = b = d$ also holds. Then, take $d' = b'$ and any $c' < a'$. We have that $-c' > -a' = b' = d'$. The interval $[c',d']$ is such that $[a',b'] R_{\overline{E}} [c',d']$ and $[c,d] Z [c',d']$.

  • If $X = \overline{O}$, then [c, d] is such that $c < a < d < b$. Notice that $|c| = -c > -a = |a|$ holds, because $c < a < 0$. Thus $-c > -a = b > d$ also holds. Then, take $d' = 0$ and any $c' < a' (< 0)$. We have that $-c' > d'$. The interval $[c',d']$ is such that $[a',b'] R_{\overline{O}} [c',d']$ and $[c,d] Z [c',d']$.

• If $-a < b$ and $-a' < b'$, then the following facts hold: $(i)\, b>0$ (otherwise, $-a < b \le 0$ would hold, which implies $a > 0 \ge b$, contradicting the fact that [a, b] is an interval), $(ii)\,|b| = b$ (this follows directly from $b>0$), and $(iii)\,|a| < |b|$ (otherwise, $|a| \ge |b| = b$ would hold, which implies either $a \ge b$, contradicting the fact that [a, b] is an interval, or $-a \ge b$, contradicting the hypothesis that $-a < b$). Now, we distinguish the following sub-cases.

  • If $X = \overline{O}$, then [c, d] is such that $c < a < d < b$. We distinguish the cases below.

    • If $-c < d$, then take some $d'$ and $c'$ such that $|a'| < d' < |b'| = b'$ and $-d' < c' < |a'| = -c$ (the existence of points $c', d'$ is guaranteed by the density of ${\mathbb {R}}$). The interval $[c',d']$ is such that $[a',b'] R_{\overline{O}} [c',d']$ and $[c,d] Z [c',d']$.

    • If $-c = d$, then take some $d'$ such that $|a'| < d' < |b'| = b'$ and $c' = -d'$ (the existence of such a point $d'$ is guaranteed by the density of ${\mathbb {R}}$). The interval $[c',d']$ is such that $[a',b'] R_{\overline{O}} [c',d']$ and $[c,d] Z [c',d']$.

    • If $-c > d$, then take some $d'$ and $c'$ such that $|a'| < d' < |b'| = b'$ and $c' < -d'$ (the existence of points $c', d'$ is guaranteed by the left-unboundedness and the density of ${\mathbb {R}}$, respectively). The interval $[c',d']$ is such that $[a',b'] R_{\overline{O}} [c',d']$ and $[c,d] Z [c',d']$.

  • If $X = \overline{E}$, then [c, d] is such that $c < a < b = d$. We distinguish the following cases.

    • If $-c < d$, then take $d' = b'$ and some $c'$ such that $-d' < c' < a'$ (the existence of such a point $c'$ is guaranteed by the density of ${\mathbb {R}}$). The interval $[c',d']$ is such that $[a',b'] R_{\overline{E}} [c',d']$ and $[c,d] Z [c',d']$.

    • If $-c = d$, then take $d' = b'$ and $c' = -d' (= -b' < a')$. The interval $[c',d']$ is such that $[a',b'] R_{\overline{E}} [c',d']$ and $[c,d] Z [c',d']$.

    • If $-c > d$, then take $d' = b'$ and any $c' < -d' (= -b' < a')$. The interval $[c',d']$ is such that $[a',b'] R_{\overline{E}} [c',d']$ and $[c,d] Z [c',d']$.

  • If $X = \overline{B}$, then [c, d] is such that $a = c < b < d$. Notice that $-d < -b < a = c$. Then, take $c' = a'$ and any $d' > b'$. It holds that $c' = a' > -b' > -d'$. The interval $[c',d']$ is such that $[a',b'] R_{\overline{B}} [c',d']$ and $[c,d] Z [c',d']$.

  • If $X = O$, then [c, d] is such that $a < c < b < d$. Notice that $-d < -b < a < c$. Then, take some $c'$ such that $a' < c' < b'$ (the existence of such a point $c'$ is guaranteed by the density of ${\mathbb {R}}$) and any $d' > b'$. It holds that $c' > a' > -b' > -d'$. The interval $[c',d']$ is such that $[a',b'] R_{O} [c',d']$ and $[c,d] Z [c',d']$.

Since the relation Z is symmetric, by Proposition 2 we have that the backward condition is verified, too. Therefore, Z is an $\mathsf {O \overline{B E O}}$-bisimulation that violates $\langle L \rangle$, and the thesis follows. $\square$

Appendix 4: Complete proof of Lemma 9

Lemma 9 $\langle E \rangle$ is not definable in $\mathsf {A B D O\overline{A B E}}$ relative to the classes $\mathsf {Lin}$ and $\mathsf {Den}$.

Proof

Let $M_1 = \langle {\mathbb {I}}({\mathbb {R}}), V_1 \rangle$ and $M_2 = \langle {\mathbb {I}}({\mathbb {R}}), V_2 \rangle$, where

• p is the only proposition letter of the language,

• the valuation function $V_1: {{\mathcal {AP}}} \rightarrow 2^{{\mathbb {I}}({\mathbb {R}})}$ is defined as: $[x,y] \in V_1(p) \Leftrightarrow x \in {\mathbb {Q}}$ if and only if $y \in {\mathbb {Q}}$, and

• the valuation function $V_2: {{\mathcal {AP}}} \rightarrow 2^{{\mathbb {I}}({\mathbb {R}})}$ is given by: $[w,z] \in V_2(p) \Leftrightarrow w \in {\mathbb {Q}}$ if and only if $z \in {\mathbb {Q}}$, and $([0,3],[w,z]) \notin R_E$.

Moreover, let Z be a relation between (intervals of) $M_1$ and $M_2$ defined as follows: $[x,y]Z[w,z] {\Leftrightarrow } [x,y] \in V_1(p)$ if and only if $[w,z] \in V_2(p)$. It is easy to verify that [0, 3]Z[0, 3], $M_1,[0,3] \Vdash \langle E \rangle p$, but $M_2,[0,3] \Vdash \lnot \langle E \rangle p$. We show now that Z is an $\mathsf {A B D O \overline{A B E}}$-bisimulation between $M_1$ and $M_2$. The local condition immediately follows from the definition. As for the forward condition, it can be checked as follows. Let [x, y] and [w, z] be two Z-related intervals, and let us assume that $[x,y] R_X [x',y']$ holds for some $X \in \{ A, B, D, O, \overline{A}, \overline{B}, \overline{E} \}$. We have to exhibit an interval $[w',z']$ such that $[x',y']$ and $[w',z']$ are Z-related, and [w, z] and $[w',z']$ are $R_X$-related. We proceed by considering each case in turn.

• If $X=A$, then $y = x'$. We can always find a point $z'$ such that $z' > \max \{ 3, z \}$ and $z' \in {\mathbb {Q}}$ if and only if $y' \in {\mathbb {Q}}$ (since both ${\mathbb {Q}}$ and $\overline{\mathbb {Q}}$ are right-unbounded). This implies that $[x',y']$ and $[z,z']$ are Z-related. Since [w, z] and $[z,z']$ are obviously $R_A$-related, we have the thesis.

• If $X=B$, the argument is similar to the previous one, but, in this case, the density of ${\mathbb {Q}}$ and $\overline{\mathbb {Q}}$ plays a major role. We choose a point $z'$ such that $w < z' < z$, $z' \ne 3$, and $z' \in {\mathbb {Q}}$ if and only if $y' \in {\mathbb {Q}}$. The interval $[w,z']$ is such that $[x',y']$ and $[w,z']$ are Z-related, and [w, z] and $[w,z']$ are $R_B$-related.

• If $X = D$, it suffices to choose two points $w'$ and $z'$ such that $w < w' < z' < z$, $z' \ne 3$, $w'$ belongs to ${\mathbb {Q}}$ if and only if $x'$ does, and $z'$ belongs to ${\mathbb {Q}}$ if and only if $y'$ does. The existence of such points is guaranteed by the density of ${\mathbb {Q}}$ and $\overline{\mathbb {Q}}$. The interval $[w',z']$ is such that $[w,z] R_D [w',z']$ and $[x',y'] Z [w',z']$.

• If $X=O$, then $w'$ and $z'$ are required to be such that $w < w' < z < z'$, and both density and right-unboundedness of ${\mathbb {Q}}$ and $\overline{\mathbb {Q}}$ must be exploited in order to choose a point $w'$ such that $w < w' < z$ and $w' \in {\mathbb {Q}}$ if and only if $x'$ does, and a point $z'$ such that $z' > \max \{ 3, z \}$ and $z'$ belongs to ${\mathbb {Q}}$ if and only if $y'$ does. The interval $[w',z']$ is such that $[w,z] R_O [w',z']$ and $[x',y'] Z [w',z']$.

• If $X=\overline{A}$, then there exists a point $w''$ such that $w'' < \min \{ 0, w \}$ and $w'' \in {\mathbb {Q}}$ if and only if w does (and thus $M', [w'',w] \Vdash p$) and there exists a point $w'''$ such that $w''' < w$ and $w''' \in {\mathbb {Q}}$ if and only if $w \in \overline{{\mathbb {Q}}}$ (and thus $M', [w''',w] \Vdash \lnot p$). We choose $w' = w''$ if $M,[x',y'] \models p$, otherwise we choose $w' = w'''$. The interval $[w',w]$ is such that $[w,z] R_{\overline{A}} [w',w]$ and $[x',y'] Z [w',w]$.

• If $X=\overline{B}$, then there exists a point $z''$ such that $z'' > \max \{ 3, z \}$ and $z'' \in {\mathbb {Q}}$ if and only if w does (and thus $M', [w,z''] \Vdash p$) and there exists a point $z'''$ such that $z''' > z$ and $z''' \in {\mathbb {Q}}$ if and only if $w \in \overline{{\mathbb {Q}}}$ (and thus $M', [w,z'''] \Vdash \lnot p$). We choose $z' = z''$ if $M,[x',y'] \models p$, otherwise we choose $z' = z'''$. The interval $[w,z']$ is such that $[w,z] R_{\overline{B}} [w,z']$ and $[x',y'] Z [w,z']$.

• If $X=\overline{E}$, then there exists a point $w''$ such that $w'' < \min \{ 0, w \}$ and $w'' \in {\mathbb {Q}}$ if and only if z does (and thus $M', [w'',z] \Vdash p$) and there exists a point $w'''$ such that $w''' < w$ and $w''' \in {\mathbb {Q}}$ if and only if $z \in \overline{{\mathbb {Q}}}$ (and thus $M', [w''',z] \Vdash \lnot p$). We choose $w' = w''$ if $M,[x',y'] \models p$, otherwise we choose $w' = w'''$. The interval $[w',z]$ is such that $[w,z] R_{\overline{E}} [w',z]$ and $[x',y'] Z [w',z]$.

The backward condition follows from Proposition 2. Therefore, Z is an $\mathsf {A B D O\overline{A B E}}$-bisimulation that violates $\langle E \rangle$, hence the thesis. $\square$

Appendix 5: Complete proof of Lemma 11

Lemma 11 $\langle A \rangle$ is not definable in $\mathsf {B E\overline{A B E}}$ relative to the classes $\mathsf {Lin}$ and $\mathsf {Den}$.

Proof

Let $M_1 = \langle {\mathbb {I}}({\mathbb {R}}), V_1 \rangle$ and $M_2 = \langle {\mathbb {I}}({\mathbb {R}}), V_2 \rangle$ be two models built on the only proposition letter p. In order to define the valuation functions $V_1$ and $V_2$, we make use of two partitions of the set ${\mathbb {R}}$, one for $M_1$ and the other for $M_2$, each of them consisting of four sets that are dense in ${\mathbb {R}}$. Formally, for $j = 1, 2$ and $i = 1, \ldots , 4$, let ${\mathbb {R}}_j^i$ be dense in ${\mathbb {R}}$. Moreover, for $j = 1, 2$, let ${\mathbb {R}} = \bigcup _{i=1}^4 {\mathbb {R}}_j^i$ and ${\mathbb {R}}_j^i \cap {\mathbb {R}}_j^{i'} = \emptyset$ for each $i,i' \in \{ 1,2,3,4 \}$, with $i \ne i'$. For the sake of simplicity, we impose the two partitions to be equal and thus we can safely omit the subscript, that is, ${\mathbb {R}}_1^{i} = {\mathbb {R}}_2^{i} = {\mathbb {R}}^{i}$ for each $i \in \{ 1,2,3,4 \}$. Thanks to this condition, the bisimulation relation Z, that we define below, is symmetric. We force points in ${\mathbb {R}}^1$ (resp., ${\mathbb {R}}^2$, ${\mathbb {R}}^3$, ${\mathbb {R}}^4$) to behave in the same way with respect to the truth of $p / \lnot p$ over the intervals they initiate and terminate by imposing the following constraints. For $j = 1,2$:

$$\begin{aligned}&\forall x, y \text { } (\text {if } x \in {\mathbb {R}}^1, \text { then } M_j,[x,y] \Vdash \lnot p); \\&\forall x, y \text { } (\text {if } x \in {\mathbb {R}}^2, \text { then } M_j,[x,y] \Vdash \lnot p); \\&\forall x, y \text { } (\text {if } x \in {\mathbb {R}}^3, \text { then } (M_j,[x,y] \Vdash p \text { iff } y \in {\mathbb {R}}^1 \cup {\mathbb {R}}^3)); \\&\forall x, y \text { } (\text {if } x \in {\mathbb {R}}^4, \text { then } (M_j,[x,y] \Vdash p \text { iff } y \in {\mathbb {R}}^2 \cup {\mathbb {R}}^4)). \end{aligned}$$

It can be easily shown that, from the given constraints, it immediately follows that:

$$\begin{aligned}&\forall x, y \text { } (\text {if } y \in {\mathbb {R}}^1, \text { then } (M_j,[x,y] \Vdash p \text { iff } x \in {\mathbb {R}}^3)); \\&\forall x, y \text { } (\text {if } y \in {\mathbb {R}}^2, \text { then } (M_j,[x,y] \Vdash p \text { iff } x \in {\mathbb {R}}^4)); \\&\forall x, y \text { } (\text {if } y \in {\mathbb {R}}^3, \text { then } (M_j,[x,y] \Vdash p \text { iff } x \in {\mathbb {R}}^3)); \\&\forall x, y \text { } (\text {if } y \in {\mathbb {R}}^4, \text { then } (M_j,[x,y] \Vdash p \text { iff } x \in {\mathbb {R}}^4)). \end{aligned}$$

The above constraints together induce the following definition of the valuation functions $V_j(p) : {{\mathcal {AP}}} \rightarrow 2^{{\mathbb {I}}({\mathbb {R}})}$:

$$\begin{aligned}{}[x,y] \in V_j(p) \Leftrightarrow (x \in {\mathbb {R}}^3 \wedge y \in {\mathbb {R}}^1 \cup {\mathbb {R}}^3) \vee (x \in {\mathbb {R}}^4 \wedge y \in {\mathbb {R}}^2 \cup {\mathbb {R}}^4). \end{aligned}$$

Now, let Z be the relation between (intervals of) $M_1$ and $M_2$ defined as follows. Two intervals [x, y] and [w, z] are Z-related if and only if at least one of the following conditions holds:

• 1. $x \in {\mathbb {R}}^1 \cup {\mathbb {R}}^2 \text { and } w \in {\mathbb {R}}^1 \cup {\mathbb {R}}^2;$

• 2. $x \in {\mathbb {R}}^3 \text {, } w \in {\mathbb {R}}^3, \text { and } (y \in {\mathbb {R}}^1 \cup {\mathbb {R}}^3 \text { iff } z \in {\mathbb {R}}^1 \cup {\mathbb {R}}^3);$

• 3. $x \in {\mathbb {R}}^3 \text {, } w \in {\mathbb {R}}^4, \text { and } (y \in {\mathbb {R}}^1 \cup {\mathbb {R}}^3 \text { iff } z \in {\mathbb {R}}^2 \cup {\mathbb {R}}^4);$

• 4. $x \in {\mathbb {R}}^4 \text {, } w \in {\mathbb {R}}^3, \text { and } (y \in {\mathbb {R}}^2 \cup {\mathbb {R}}^4 \text { iff } z \in {\mathbb {R}}^1 \cup {\mathbb {R}}^3);$

• 5. $x \in {\mathbb {R}}^4 \text {, } w \in {\mathbb {R}}^4, \text { and } (y \in {\mathbb {R}}^2 \cup {\mathbb {R}}^4 \text { iff } z \in {\mathbb {R}}^2 \cup {\mathbb {R}}^4).$

It is worth pointing out that two intervals [x, y] and [w, z] that are Z-related are such that if, for instance, both x and w belong to ${\mathbb {R}}^3$ (second clause), then either y and z both occur in odd-numbered partitions or they both occur in even-numbered partitions. Moreover, since the two partitions are equal, Z is symmetric.

Let us consider now two intervals [x, y] and [w, z] such that $x \in {\mathbb {R}}^1$, $w \in {\mathbb {R}}^1$, $y \in {\mathbb {R}}^3$, and $z \in {\mathbb {R}}^1$. By definition of Z, [x, y] and [w, z] are Z-related, and by definition of $V_1$ and $V_2$, there exists $y'> y$ such that $M_1,[y,y'] \Vdash p$, but there is no $z' > z$ such that $M_2,[z,z'] \Vdash p$. Thus, $M_1,[x,y] \Vdash \langle A \rangle p$ and $M_2,[w,z] \Vdash \lnot \langle A \rangle p$ hold.

To complete the proof, it suffices to show that the relation Z is a $\mathsf {B E \overline{A B E}}$-bisimulation. It can be easily checked that every pair ([x, y], [w, z]) of Z-related intervals is such that either $[x,y] \in V_1(p)$ and $[w,z] \in V_2(p)$, or $[x,y] \not \in V_1(p)$ and $[w,z] \not \in V_2(p)$.

In order to verify the forward condition, let [x, y] and [w, z] be two Z-related intervals. For each modality $\langle X \rangle$ of the language and each interval $[x',y']$ such that $[x,y] R_X [x',y']$, we have to exhibit an interval $[w',z']$ such that $[x',y']Z[w',z']$ and $[w,z]R_X[w',z']$. We proceed by considering each case in turn.

• Let $X=B$. If $x \in {\mathbb {R}}^1 \cup {\mathbb {R}}^2$ and $w \in {\mathbb {R}}^1 \cup {\mathbb {R}}^2$, then for any $z'$ such that $w < z' < z$, both $[x,y']Z[w,z']$ and $[w,z] R_B [w,z']$ hold. If $x \in {\mathbb {R}}^i$ and $w \in {\mathbb {R}}^i$, for some $i \in \{3,4\}$, and $y' \in {\mathbb {R}}^k$, for some $k \in \{1,2,3,4\}$, then for any $z'$ such that $w < z' < z$ and $z' \in {\mathbb {R}}^k$, it holds that $[x,y']Z[w,z']$ and $[w,z] R_B [w,z']$ (the existence of $z'$ is guaranteed by density of ${\mathbb {R}}^k$ in ${\mathbb {R}}$). Finally, if $x \in {\mathbb {R}}^i$ and $w \in {\mathbb {R}}^{i'}$ for $i,i' \in \{3,4\}$, with $i \ne i'$, and, in addition, $y' \in {\mathbb {R}}^1 \cup {\mathbb {R}}^3$ (resp., $y' \in {\mathbb {R}}^2 \cup {\mathbb {R}}^4$), then for any $z'$ such that $w < z' < z$ and $z' \in {\mathbb {R}}^2 \cup {\mathbb {R}}^4$ (resp., $z' \in {\mathbb {R}}^1 \cup {\mathbb {R}}^3$), it holds that $[x,y']Z[w,z']$ and $[w,z] R_B [w,z']$ (density of ${\mathbb {R}}^2$ and ${\mathbb {R}}^4$, resp., ${\mathbb {R}}^1$ and ${\mathbb {R}}^3$, in ${\mathbb {R}}$ is used).

• Let $X=E$. As $[x,y] R_E [x',y']$, we have that $y = y'$. We distinguish the following cases, where we tacitly use the density of the relevant sets in ${\mathbb {R}}$: (i) if $x' \in {\mathbb {R}}^1 \cup {\mathbb {R}}^2$, then we choose $w'$ such that $w < w' < z$ and $w' \in {\mathbb {R}}^1$; (ii) if either $x' \in {\mathbb {R}}^3$ and $y \in {\mathbb {R}}^1 \cup {\mathbb {R}}^3$, or $x' \in {\mathbb {R}}^4$ and $y \in {\mathbb {R}}^2 \cup {\mathbb {R}}^4$, then we choose $w'$ such that $w < w' < z$ and either $w' \in {\mathbb {R}}^3$ (if $z \in {\mathbb {R}}^1 \cup {\mathbb {R}}^3$), or $w' \in {\mathbb {R}}^4$ (if $z \in {\mathbb {R}}^2 \cup {\mathbb {R}}^4$); (iii) if either $x' \in {\mathbb {R}}^3$ and $y \in {\mathbb {R}}^2 \cup {\mathbb {R}}^4$, or $x' \in {\mathbb {R}}^4$ and $y \in {\mathbb {R}}^1 \cup {\mathbb {R}}^3$, then we choose $w'$ such that $w < w' < z$ and either $w' \in {\mathbb {R}}^3$ (if $z \in {\mathbb {R}}^2 \cup {\mathbb {R}}^4$), or $w' \in {\mathbb {R}}^4$ (if $z \in {\mathbb {R}}^1 \cup {\mathbb {R}}^3$). In all cases, we have that $[x',y]Z[w',z]$ and $[w,z] R_E [w',z]$.

• Let $X=\overline{A}$. As $[x,y] R_{\overline{A}} [x',y']$, we have that $x = y'$. We distinguish the following cases: (i) if $x' \in {\mathbb {R}}^1 \cup {\mathbb {R}}^2$, then we choose $w'$ such that $w' < w$ and $w' \in {\mathbb {R}}^1$; (ii) if either $x' \in {\mathbb {R}}^3$ and $x \in {\mathbb {R}}^1 \cup {\mathbb {R}}^3$, or $x' \in {\mathbb {R}}^4$ and $x \in {\mathbb {R}}^2 \cup {\mathbb {R}}^4$, then we choose $w'$ such that $w' < w$ and either $w' \in {\mathbb {R}}^3$ (if $w \in {\mathbb {R}}^1 \cup {\mathbb {R}}^3$), or $w' \in {\mathbb {R}}^4$ (if $w \in {\mathbb {R}}^2 \cup {\mathbb {R}}^4$); (iii) if either $x' \in {\mathbb {R}}^3$ and $x \in {\mathbb {R}}^2 \cup {\mathbb {R}}^4$, or $x' \in {\mathbb {R}}^4$ and $x \in {\mathbb {R}}^1 \cup {\mathbb {R}}^3$, then we choose $w'$ such that $w' < w$ and either $w' \in {\mathbb {R}}^3$ (if $w \in {\mathbb {R}}^2 \cup {\mathbb {R}}^4$), or $w' \in {\mathbb {R}}^4$ (if $w \in {\mathbb {R}}^1 \cup {\mathbb {R}}^3$). In all cases, we have that $[x',x]Z[w',w]$ and $[w,z] R_{\overline{A}} [w',w]$.

• Let $X=\overline{B}$. Since $[x,y] R_{\overline{B}} [x',y']$, we have that $x = x'$. If $x \in {\mathbb {R}}^1 \cup {\mathbb {R}}^2$ and $w \in {\mathbb {R}}^1 \cup {\mathbb {R}}^2$, then for any $z' > z$, both $[x,y']Z[w,z']$ and $[w,z] R_{\overline{B}} [w,z']$ hold. If $x \in {\mathbb {R}}^i$ and $w \in {\mathbb {R}}^i$, for some $i \in \{3,4\}$, and $y' \in {\mathbb {R}}^k$, for some $k \in \{1,2,3,4\}$, then for any $z' > z$ such that $z' \in {\mathbb {R}}^k$, it holds that $[x,y']Z[w,z']$ and $[w,z] R_{\overline{B}} [w,z']$ (the existence of $z'$ is guaranteed by density of ${\mathbb {R}}^k$ in ${\mathbb {R}}$). Finally, if $x \in {\mathbb {R}}^i$ and $w \in {\mathbb {R}}^{i'}$ for $i,i' \in \{3,4\}$, with $i \ne i'$, and, in addition, $y' \in {\mathbb {R}}^1 \cup {\mathbb {R}}^3$ (resp., $y' \in {\mathbb {R}}^2 \cup {\mathbb {R}}^4$), then for any $z' > z$ such that $z' \in {\mathbb {R}}^2 \cup {\mathbb {R}}^4$ (resp., $z' \in {\mathbb {R}}^1 \cup {\mathbb {R}}^3$), it holds that $[x,y']Z[w,z']$ and $[w,z] R_{\overline{B}} [w,z']$ (density of ${\mathbb {R}}^2$ and ${\mathbb {R}}^4$, resp., ${\mathbb {R}}^1$ and ${\mathbb {R}}^3$, in ${\mathbb {R}}$ is used).

• Let $X=\overline{E}$. Since $[x,y] R_{\overline{E}} [x',y']$, we have that $y = y'$. We distinguish the following cases: (i) if $x' \in {\mathbb {R}}^1 \cup {\mathbb {R}}^2$, then we choose $w'$ such that $w' < w$ and $w' \in {\mathbb {R}}^1$; (ii) if either $x' \in {\mathbb {R}}^3$ and $y \in {\mathbb {R}}^1 \cup {\mathbb {R}}^3$, or $x' \in {\mathbb {R}}^4$ and $y \in {\mathbb {R}}^2 \cup {\mathbb {R}}^4$, then we choose $w'$ such that $w' < w$ and either $w' \in {\mathbb {R}}^3$ (if $z \in {\mathbb {R}}^1 \cup {\mathbb {R}}^3$), or $w' \in {\mathbb {R}}^4$ (if $z \in {\mathbb {R}}^2 \cup {\mathbb {R}}^4$); (iii) if either $x' \in {\mathbb {R}}^3$ and $y \in {\mathbb {R}}^2 \cup {\mathbb {R}}^4$, or $x' \in {\mathbb {R}}^4$ and $y \in {\mathbb {R}}^1 \cup {\mathbb {R}}^3$, then we choose $w'$ such that $w' < w$ and either $w' \in {\mathbb {R}}^3$ (if $z \in {\mathbb {R}}^2 \cup {\mathbb {R}}^4$) or $w' \in {\mathbb {R}}^4$ (if $z \in {\mathbb {R}}^1 \cup {\mathbb {R}}^3$). In all cases, we have that $[x',y]Z[w',z]$ and $[w,z] R_{\overline{E}} [w',z]$.

The backward condition follows from the forward one by Proposition 2. Therefore, Z is a $\mathsf {B E\overline{A B E}}$-bisimulation that violates $\langle A \rangle$, and the thesis immediately follows. $\square$

Appendix 6: Complete proof of Lemma 12

Lemma 12 $\langle D \rangle$ is not definable in $\mathsf {A B O\overline{A B E}}$ relative to the classes $\mathsf {Lin}$ and $\mathsf {Den}$.

Proof

As a first step, we define a pair of functions that will be used in the definition of the models involved in the bisimulation relation Z. Let ${\mathcal {P}}({\mathbb {Q}})= \{{\mathbb {Q}}_q \mid q \in {\mathbb {Q}}\}$ and ${\mathcal {P}}(\overline{\mathbb {Q}}) = \{\overline{\mathbb {Q}}_q \mid q \in {\mathbb {Q}}\}$ be countably infinite partitions of ${\mathbb {Q}}$ and $\overline{\mathbb {Q}}$, respectively, such that for every $q \in {\mathbb {Q}}$, both ${\mathbb {Q}}_q$ and $\overline{\mathbb {Q}}_q$ are dense in ${\mathbb {R}}$. For every $q \in {\mathbb {Q}}$, let ${\mathbb {R}}_q = {\mathbb {Q}}_q \cup \overline{\mathbb {Q}}_q$. We define a function $g: {\mathbb {R}} \rightarrow {\mathbb {Q}}$ that maps every real number x to the index q (a rational number) of the class ${\mathbb {R}}_{q}$ it belongs to. Formally, for every $x \in {\mathbb {R}}$, $g(x) = q$, where $q \in {\mathbb {Q}}$ is the unique rational number such that $x \in {\mathbb {R}}_{q}$. The two functions $f_1: {\mathbb {R}} \rightarrow {\mathbb {Q}}$ and $f_2: {\mathbb {R}} \rightarrow {\mathbb {Q}}$ are defined as follows:

$$\begin{aligned}&f_1(x) = \left\{ \begin{array}{l@{\quad }l} g(x) &{} \quad \text {if } x < g(x) \text {, } x \ne 1, \text { and } x \ne 0 \\ 2 &{} \quad \text {if } x = 1 \\ \lceil x+3 \rceil &{} \quad \text {otherwise} \end{array} \right. \\&f_2(x) = \left\{ \begin{array}{ll} g(x) &{} \quad \text {if } x < g(x) \text { and } x \not \in [0,3) \\ \lceil x+3 \rceil &{} \quad \text {otherwise} \end{array} \right. \end{aligned}$$

It is not difficult to check that the above-defined functions $f_i$ ($i \in \{ 1,2 \}$) satisfy the following properties:

• (i) for every $x \in {\mathbb {R}}$, $f_i(x) > x$,

• (ii) for every $x \in {\mathbb {Q}}$, both $f_i^{-1} (x) \cap {\mathbb {Q}}$ and $f_i^{-1} (x) \cap \overline{{\mathbb {Q}}}$ are left-unbounded (notice that surjectivity of $f_i$ immediately follows), and

• (iii) for every $x,y \in {\mathbb {R}}$, if $x < y$, then there exists $u_1 \in {\mathbb {Q}}$ (resp., $u_2 \in \overline{{\mathbb {Q}}}$) such that $x < u_1 < y$ (resp., $x < u_2 < y$) and $y < f_i(u_1)$ (resp., $y < f_i(u_2)$).

Now, we can define two models $M_1$ and $M_2$, built on the only proposition letter p, as follows: for each $i \in \{ 1,2 \}$, $M_i = \langle {\mathbb {I}}({\mathbb {R}}), V_i \rangle$, where $V_i : {{\mathcal {AP}}} \rightarrow 2^{{\mathbb {I}}({\mathbb {R}})}$ ($i \in \{ 1,2 \}$) is defined as follows: $[x,y] \in V_i(p)\Leftrightarrow y \ge f_i(x)$. Finally, we define the relation Z as:

$$\begin{aligned} ([x,y],[w,z]) \in Z \Leftrightarrow x \equiv w \text {, } y \equiv z \text {, and } [x,y] \equiv _l [w,z], \end{aligned}$$

where we define $u \equiv v \Leftrightarrow u \in {\mathbb {Q}}$ if and only if $v \in {\mathbb {Q}}$ and $[u,u'] \equiv _l [v,v'] \Leftrightarrow u' \sim f_1(u)$ and $v' \sim f_2(v)$, for $\sim \in \{<,=,>\}$.

Let us consider the interval [0, 3] in $M_{1}$ and the interval [0, 3] in $M_{2}$. It is immediate to see that these two intervals are Z-related. However, $M_{1},[0,3] \Vdash \langle D \rangle p$ (as $M_{1},[1,2] \Vdash p$), but $M_{2},[0,3] \Vdash \lnot \langle D \rangle p$.

To complete the proof, it suffices to show that Z is an $\mathsf {A B O\overline{A B E}}$-bisimulation between $M_{1}$ and $M_{2}$.

Let [x, y] and [w, z] be two Z-related intervals. By definition, $y \sim f_1(x)$ and $z \sim f_2(w)$ for some $\sim \in \{ <,=,$ $> \}$. If $\sim \in \{=,>\}$, then both [x, y] and [w, z] satisfy p; otherwise, both of them satisfy $\lnot p$. Thus, the local condition is satisfied.

As for the forward condition, let [x, y] and $[x',y']$ be two intervals in $M_{1}$ and [w, z] an interval in $M_{2}$. We have to prove that if [x, y] and [w, z] are Z-related, then, for each modality $\langle X \rangle$ of $\mathsf {A B O \overline{A B E}}$ such that $[x,y] R_X [x',y']$, there exists an interval $[w',z']$ such that $[x',y']$ and $[w',z']$ are Z-related and $[w,z] R_X [w',z']$. Once again, we proceed by examining each case in turn.

• Let $X = A$. By definition of $\langle A \rangle$, $x' = y$ and we are forced to choose $w' = z$. By $y \equiv z$, it immediately follows that $x' \equiv w'$. We must find a point $z'>z$ such that $y' \equiv z'$ and both $y' \sim f_1(y)$ and $z' \sim f_2(z)$ for some $\sim \in \{<,=,>\}$. Let us suppose that $y' < f_1(y)$. In such a case, we choose a point $z'$ such that $z < z' < f_2(z)$ and $y' \equiv z'$. The existence of such a point is guaranteed by property (i) of $f_2$ above and by the density of ${\mathbb {Q}}$ and $\overline{\mathbb {Q}}$ in ${\mathbb {R}}$. Otherwise, if $y' = f_1(y)$, we choose $z' = f_2(z)$. By definition of $f_1$ and $f_2$ (the codomain of $f_1$ and $f_2$ is ${\mathbb {Q}}$), both $y'$ and $z'$ belong to ${\mathbb {Q}}$ and thus $y' \equiv z'$. Finally, if $y' > f_1(y)$, we choose $z' > f_2(z)$ such that $y' \equiv z'$. The existence of such a point is guaranteed by right-unboundedness of ${\mathbb {Q}}$ and $\overline{\mathbb {Q}}$, and the interval $[z,z']$ is such that $[x',y']Z[z,z']$ and $[w,z] R_A [z,z']$.

• Let $X = B$. In this case, $x = x'$ and $y' < y$. We distinguish the following cases.

  • If $y' > f_1(x)$ and $y' \in {\mathbb {Q}}$ (resp., $y' \in \overline{{\mathbb {Q}}}$), then $y > f_1(x)$ holds as well (as $y' < y$), which implies $z > f_2(w)$. Thus, we can choose any point $z' \in {\mathbb {Q}}$ (resp., $z' \in \overline{{\mathbb {Q}}}$), with $f_2(w) < z' < z$ (the existence of such a point is guaranteed by density of ${\mathbb {Q}}$ and $\overline{{\mathbb {Q}}}$, respectively).

  • If $y' = f_1(x)$, then $y' \in {\mathbb {Q}}$ (by definition of $f_1$) and $y > f_1(x)$ holds (as $y' < y$). The latter implies $z > f_2(w)$, and thus we choose $z' = f_2(w)$. Note that $f_2(w) \in {\mathbb {Q}}$ by the definition of $f_2$.

  • If $y' < f_1(x)$ and $y' \in {\mathbb {Q}}$ (resp., $y' \in \overline{{\mathbb {Q}}}$), then we choose a point $z' \in {\mathbb {Q}}$ (resp., $z' \in \overline{{\mathbb {Q}}}$) such that $w < z' < \min \{ z, f_2(w) \}$ (the existence of such a point is guaranteed by density of ${\mathbb {Q}}$ and $\overline{{\mathbb {Q}}}$, respectively).

  In all cases, the interval $[w,z']$ is such that $[x,y']Z[w,z']$ and $[w,z] R_B [w,z']$.

• Let $X = O$. Firstly, we choose a point $w'$ such that $w < w' < z$, $w' \in {\mathbb {Q}}$ iff $x' \in {\mathbb {Q}}$, and $f_2(w') > z$ (the existence of such a point is guaranteed by property (iii) of $f_2$ on page 19). Secondly, we choose a point $z'$ such that $z' \in {\mathbb {Q}}$ iff $y' \in {\mathbb {Q}}$, and

  • if $y' < f_1(x')$, then $z < z' < f_2(w')$ (density of ${\mathbb {Q}}$ and $\overline{{\mathbb {Q}}}$ is used here),

  • if $y' > f_1(x')$, then $z' > f_2(w')$ (right-unboundedness of ${\mathbb {Q}}$ and $\overline{{\mathbb {Q}}}$ is used here),

  • if $y' = f_1(x')$, then $z' = f_2(w')$.

  In all cases, the interval $[w',z']$ is such that $[x',y']Z[w',z']$ and $[w,z] R_O [w',z']$.

• Let $X = \overline{A}$. In this case, $y' = x$. We distinguish the following cases.

  • If $f_1(x') < y' (=x)$, then consider any point $\overline{w} \in {\mathbb {Q}}$, with $\overline{w} < w$. By property (ii) on page 19, there exist both a point $w'' \in {\mathbb {Q}}$ and a point $w''' \in \overline{{\mathbb {Q}}}$ such that $w'' < \overline{w}$, $w''' < \overline{w}$, and $f_2(w'') = f_2(w''') = \overline{w}$. We select $w' = w''$ if $x' \in {\mathbb {Q}}$, and $w' = w'''$ if $x' \in \overline{{\mathbb {Q}}}$.

  • If $f_1(x') > y' (=x)$, then consider any point $\overline{w} \in {\mathbb {Q}}$, with $w < \overline{w}$. By property (ii), there exist both a point $w'' \in {\mathbb {Q}}$ and a point $w''' \in \overline{{\mathbb {Q}}}$ such that $w'' < w$, $w''' < w$, and $f_2(w'') = f_2(w''') = \overline{w}$. We select $w' = w''$ if $x' \in {\mathbb {Q}}$, and $w' = w'''$ if $x' \in \overline{{\mathbb {Q}}}$.

  • If $f_1(x') = y' (=x)$, then $x,w \in {\mathbb {Q}}$. By property (ii), there exist both a point $w'' \in {\mathbb {Q}}$ and a point $w''' \in \overline{{\mathbb {Q}}}$ such that $w'' < w$, $w''' < w$, and $f_2(w'') = f_2(w''') = w$. We select $w' = w''$ if $x' \in {\mathbb {Q}}$, and $w' = w'''$ if $x' \in \overline{{\mathbb {Q}}}$.

  In all cases, the interval $[w',w]$ is such that $[x',x]Z[w',w]$ and $[w,z] R_{\overline{A}} [w',w]$.

• Let $X = \overline{B}$. In this case $x' = x$. We distinguish the following cases.

  • If $y' < f_1(x)$ and $y' \in {\mathbb {Q}}$ (resp., $y' \in \overline{{\mathbb {Q}}}$), then $y < f_1(x)$ holds as well (as $y < y'$), which implies $z < f_2(w)$. Thus, we can choose any point $z' \in {\mathbb {Q}}$ (resp., $z' \in \overline{{\mathbb {Q}}}$), with $z < z' < f_2(w)$ (the existence of such a point is guaranteed by density of ${\mathbb {Q}}$ and $\overline{{\mathbb {Q}}}$, respectively).

  • If $y' = f_1(x)$, then $y' \in {\mathbb {Q}}$ (by definition of $f_1$) and $y < f_1(x)$ holds (as $y < y'$). The latter implies $z < f_2(w)$, and thus we choose $z' = f_2(w)$. Note that $f_2(w) \in {\mathbb {Q}}$ by the definition of $f_2$.

  • If $y' > f_1(x)$ and $y' \in {\mathbb {Q}}$ (resp., $y' \in \overline{{\mathbb {Q}}}$), then we choose a point $z' \in {\mathbb {Q}}$ (resp., $z' \in \overline{{\mathbb {Q}}}$) such that $z' > \max \{ z, f_2(w) \}$ (the existence of such a point is guaranteed by right-unboundedness of ${\mathbb {Q}}$ and $\overline{{\mathbb {Q}}}$, respectively).

  In all cases, the interval $[w,z']$ is such that $[x',y']Z[w,z']$ and $[w,z] R_{\overline{B}} [w,z']$.

• Let $X = \overline{E}$. In this case $y = y'$ and $x' < x$. We distinguish the following cases.

  • If $f_1(x') < y' (=y)$, then consider any point $\overline{w} \in {\mathbb {Q}}$, with $\overline{w} < z$. By property (ii) on page 19, there exist both a point $w'' \in {\mathbb {Q}}$ and a point $w''' \in \overline{{\mathbb {Q}}}$ such that $w'' < w$, $w''' < w$, and $f_2(w'') = f_2(w''') = \overline{w}$. We select $w' = w''$ if $x' \in {\mathbb {Q}}$, and $w' = w'''$ if $x' \in \overline{{\mathbb {Q}}}$.

  • If $f_1(x') > y' (=y)$, then consider any point $\overline{w} \in {\mathbb {Q}}$, with $z < \overline{w}$. By property (ii) on page 19, there exist both $w'' \in {\mathbb {Q}}$ and $w''' \in \overline{{\mathbb {Q}}}$ such that $w'' < w$, $w''' < w$, and $f_2(w'') = f_2(w''') = \overline{w}$. We select $w' = w''$ if $x' \in {\mathbb {Q}}$, and $w' = w'''$ if $x' \in \overline{{\mathbb {Q}}}$.

  • If $f_1(x') = y' (=y)$, then $y,z \in {\mathbb {Q}}$. By property (ii) on page 19, there exist both $w'' \in {\mathbb {Q}}$ and $w''' \in \overline{{\mathbb {Q}}}$ such that $w'' < w$, $w''' < w$, and $f_2(w'') = f_2(w''') = z$. We select $w' = w''$ if $x' \in {\mathbb {Q}}$, and $w' = w'''$ if $x' \in \overline{{\mathbb {Q}}}$.

  In all cases, the interval $[w',z]$ is such that $[x',y]Z[w',z]$ and $[w,z] R_{\overline{E}} [w',z]$.

The backward condition can be verified in a very similar way and thus the details of the proof are omitted. Hence, Z is an $\mathsf {A B O\overline{A B E}}$-bisimulation that violates $\langle D \rangle$, hence the thesis. $\square$

Appendix 7: Complete proof of Lemma 14

Lemma 14 $\langle O \rangle$ is not definable in $\mathsf {A B E\overline{A E D}}$ relative to the classes $\mathsf {Lin}$ and $\mathsf {Den}$.

Proof

The bisimulation we use here is very similar to those constructed for the operators $\langle E \rangle$ and $\langle \overline{E} \rangle$ in the proofs of Lemma 9 and Lemma 10, respectively. Let $M_1 = \langle {\mathbb {I}}({\mathbb {R}}), V_1 \rangle$ and $M_2 = \langle {\mathbb {I}}({\mathbb {R}}), V_2 \rangle$ be two models over the set of proposition letters ${{\mathcal {AP}}} = \{p\}$, where the valuation functions $V_1: {{\mathcal {AP}}} \rightarrow 2^{{\mathbb {I}}({\mathbb {R}})}$ and $V_2: {{\mathcal {AP}}} \rightarrow 2^{{\mathbb {I}}({\mathbb {R}})}$ are, respectively, defined as follows:

• $[x,y] \in V_1(p) \Leftrightarrow x \in {\mathbb {Q}}$ iff $y \in {\mathbb {Q}}$ and

• $[w,z] \in V_2(p) \Leftrightarrow w \in {\mathbb {Q}}$ iff $z \in {\mathbb {Q}}$, and $[0,3]R_O[w,z]$ does not hold (that is, it is not the case that $0 < w < 3 < z$).

Then, we define the relation Z between intervals of $M_1$ and intervals of $M_2$ as: $[x,y]Z[w,z] \Leftrightarrow [x,y] \in V_1(p)$ iff $[w,z] \in V_2(p)$. It is immediate to see that [0, 3]Z[0, 3], $M_1,[0,3] \Vdash \langle O \rangle p$, but $M_2,[0,3] \Vdash \lnot \langle O \rangle p$.

We show that Z is an $\mathsf {A B E \overline{A E D}}$-bisimulation between $M_1$ and $M_2$. The local condition immediately follows from the definition. As for the forward condition, it can be checked as follows. Let [x, y] and [w, z] be two Z-related intervals, and let us assume that $[x,y] R_X [x',y']$ holds for some $X \in \{ A, B, E, \overline{A}, \overline{E}, \overline{D} \}$. We have to exhibit an interval $[w',z']$ such that $[x',y']$ and $[w',z']$ are Z-related, and [w, z] and $[w',z']$ are $R_X$-related. We proceed by a case analysis on $X \in \{ A, B, E, \overline{A}, \overline{E}, \overline{D} \}$.

• If $X=A$, then we distinguish the following cases: (a) if $0 < z < 3$, then we select a point $z'$ such that $z < z' < 3$ and $z' \in {\mathbb {Q}}$ iff $y' \in {\mathbb {Q}}$ (the existence of such a point is guaranteed by density of ${\mathbb {Q}}$ and $\overline{\mathbb {Q}}$); (b) otherwise, we select a point $z'$ such that $z' > z$ and $z' \in {\mathbb {Q}}$ iff $y' \in {\mathbb {Q}}$ (the existence of such a point is guaranteed by right-unboundedness of ${\mathbb {Q}}$ and $\overline{\mathbb {Q}}$). In both cases, the interval $[z,z']$ is such that $[x',y']Z[z,z']$ and $[w,z]R_A[z,z']$.

• If $X=B$, the argument is similar to the previous one. We distinguish the following cases: (a) if $0 < w < 3$, then we choose a point $z'$ such that $w < z' < \min \{ 3,z \}$ and $z' \in {\mathbb {Q}}$ iff $y' \in {\mathbb {Q}}$; (b) otherwise, we choose a point $z'$ such that $w < z' < z$ and $z' \in {\mathbb {Q}}$ iff $y' \in {\mathbb {Q}}$. In both cases, the interval $[w,z']$ is such that $[x',y']Z[w,z']$ and $[w,z]R_B[w,z']$.

• If $X = E$, then we distinguish the following cases: (a) if $z > 3$, then we choose a point $w'$ such that $\max \{ 3,w \} < w' < z$ and $w' \in {\mathbb {Q}}$ iff $x' \in {\mathbb {Q}}$; (b) otherwise, we choose a point $w'$ such that $w < w' < z$ and $w' \in {\mathbb {Q}}$ iff $x' \in {\mathbb {Q}}$. In both cases, the interval $[w',z]$ is such that $[x',y']Z[w',z]$ and $[w,z]R_E[w',z]$.

• If $X = \overline{A}$, then we choose a point $w'$ such that $w' < \min \{ 0,w \}$ and $w' \in {\mathbb {Q}}$ iff $x' \in {\mathbb {Q}}$. The interval $[w',w]$ is such that $[x',y']Z[w',w]$ and $[w,z]R_{\overline{A}}[w',w]$.

• If $X = \overline{E}$, then we choose a point $w'$ such that $w' < \min \{ 0,w \}$ and $w' \in {\mathbb {Q}}$ iff $x' \in {\mathbb {Q}}$. The interval $[w',z]$ is such that $[x',y']Z[w',z]$ and $[w,z]R_{\overline{E}}[w',z]$.

• If $X = \overline{D}$, then we first choose a point $w'$ such that $w' < \min \{ 0,w \}$ and $w' \in {\mathbb {Q}}$ iff $x' \in {\mathbb {Q}}$. Next, we choose a point $z'$ such that $z' > z$ and $z' \in {\mathbb {Q}}$ iff $y' \in {\mathbb {Q}}$. The interval $[w',z']$ is such that $[x',y']Z[w',z']$ and $[w,z]R_{\overline{D}}[w',z']$.

The backward condition can be verified in a very similar way and thus we omit the details of the proof. Therefore, Z is an $\mathsf {A B E\overline{A E D}}$-bisimulation that violates $\langle O \rangle$. The thesis immediately follows. $\square$

Appendix 8: Complete proof of Lemma 15

Lemma 15 $\langle O \rangle$ is not definable in $\mathsf {A B D\overline{A B E}}$ relative to the classes $\mathsf {Lin}$ and $\mathsf {Den}$.

Proof

The $\mathsf {A B D\overline{A B E}}$-bisimulation that we present here has some similarities with the $\mathsf {A B O\overline{A B E}}$-bisimulation that violates $\langle D \rangle$, presented in the proof of Lemma 12. However, we need to ‘rearrange’ the partitions of ${\mathbb {Q}}$ and $\overline{{\mathbb {Q}}}$ that we exploited to prove Lemma 12. More precisely, we still need two infinite countable partitions ${\mathcal {P}}({\mathbb {Q}})$ of ${\mathbb {Q}}$ and ${\mathcal {P}}(\overline{\mathbb {Q}})$ of $\overline{\mathbb {Q}}$, whose elements are dense in ${\mathbb {R}}$, but it is useful to provide a more suitable enumeration for both of them, as follows: ${\mathcal {P}}({\mathbb {Q}}) = \{ {\mathbb {Q}}_q^c \mid c \in \{a,b\}, q \in {\mathbb {Q}} \}$ and ${\mathcal {P}}(\overline{\mathbb {Q}}) = \{ \overline{\mathbb {Q}}_q^c \mid c \in \{a,b\}, q \in {\mathbb {Q}} \}$. Analogously to Lemma 12, we require these partitions to be such that, for each $c \in \{a,b\}$ and $q \in {\mathbb {Q}}$, sets ${\mathbb {Q}}_q^c$ and $\overline{\mathbb {Q}}_q^c$ are dense in ${\mathbb {R}}$. Now, we define the partition ${\mathcal {P}}({\mathbb {R}})$ of ${\mathbb {R}}$ as: ${\mathcal {P}}({\mathbb {R}}) = \{ {\mathbb {R}}_q^c \mid c \in \{a,b\}, q \in {\mathbb {Q}}\}$, where ${\mathbb {R}}_q^c = {\mathbb {Q}}_q^c \cup \overline{\mathbb {Q}}_q^c$, for each $c \in \{a,b\}$ and $q \in {\mathbb {Q}}$. We use ${\mathbb {Q}}^c$ (resp., $\overline{\mathbb {Q}}^c$, $\mathbb {R}^c$) as an abbreviation for $\bigcup _{q \in {\mathbb {Q}}} {\mathbb {Q}}_q^c$ (resp., $\bigcup _{q \in {\mathbb {Q}}} \overline{\mathbb {Q}}_q^c$, $\bigcup _{q \in {\mathbb {Q}}} {\mathbb {R}}_q^c$), for each $c \in \{a,b\}$. In addition, we define ${\mathcal {S}}_1,{\mathcal {S}}_2 \subseteq {\mathbb {I}}({\mathbb {R}})$ as follows:

$$\begin{aligned} {\mathcal {S}}_1= & {} \{[x,y] \mid x,y \in {\mathbb {R}}^c, c \in \{a,b\} \} \quad \text {and} \\ {\mathcal {S}}_2= & {} \{[w,z] \mid w,z \in {\mathbb {R}}^c, c \in \{a,b\} \} {\setminus } \{[w,z] \mid 0 < w < 3 < z \}. \end{aligned}$$

Finally, for each $i \in \{1,2\}$, we use $\overline{\mathcal {S}}_i$ to denote the set ${\mathbb {I}}({\mathbb {R}}) \setminus {\mathcal {S}}_i$. It is easy to verify that, for every pair of points $x,y \in {\mathbb {I}}({\mathbb {R}})$, if $x < y$, then there exist $y_1,y_2,y_3,y_4 \in {\mathbb {R}}$ such that $x < y_i < y$, for each $i \in \{1,2,3,4\}$, and:

$$\begin{aligned}&y_1 \in {\mathbb {Q}} \text { and } [x,y_1] \in {\mathcal {S}}_1 (\text {resp., } {\mathcal {S}}_2 ), \nonumber \\&y_2 \in {\mathbb {Q}} \text { and } [x,y_2] \in \overline{\mathcal {S}}_1 (\text {resp., } \overline{\mathcal {S}}_2 ), \nonumber \\&y_3 \in \overline{\mathbb {Q}} \text { and } [x,y_3] \in {\mathcal {S}}_1 (\text {resp., } {\mathcal {S}}_2 ), \nonumber \\&y_4 \in \overline{\mathbb {Q}} \text { and } [x,y_4] \in \overline{\mathcal {S}}_1 (\text {resp., } \overline{\mathcal {S}}_2 ). \end{aligned}$$

(4)

We define now a pair of functions that will be used in the definition of the models involved in the bisimulation relation Z. Let $g: {\mathbb {R}} \rightarrow {\mathbb {Q}}$ be a function defined as follows (notice the strong similarity with the definition of g in Lemma 12): for each $x \in {\mathbb {R}}$, $g(x) = q$, where $q \in {\mathbb {Q}}$ is the unique rational number such that $x \in {\mathbb {R}}_{q}^a \cup R_{q}^b$. The functions $f_1: {\mathbb {R}} \rightarrow {\mathbb {Q}}$ and $f_2: {\mathbb {R}} \rightarrow {\mathbb {Q}}$ are defined as follows:

$$\begin{aligned}&f_1(x) = \left\{ \begin{array}{l@{\quad }l} g(x) &{} \text {if } x < g(x) \\ \lceil x+3 \rceil &{} \text {otherwise} \end{array} \right. \\&f_2(x) = \left\{ \begin{array}{l@{\quad }l} g(x) &{} \text {if } x < g(x) \text { and } ([0,3],[x,g(x)]) \not \in R_O \\ \lceil x+3 \rceil &{} \text {if } x \ge g(x) \text { and } x \not \in (0,3) \\ a_{n'} &{} \text {otherwise} \end{array} \right. \end{aligned}$$

where $a_{n'}$ is the least element of the series $a_n = 3-(\frac{1}{n})$ ($n\ge 1$) such that $x < a_{n'}$. It is not hard to verify that the functions $f_i$ ($i \in \{ 1,2 \}$) fulfill the following conditions:

(i):

$f_i(x) > x$ for every $x \in {\mathbb {R}}$;

(ii):

for each $x \in {\mathbb {Q}}$, $f_i^{-1} (x) \cap {\mathbb {Q}}^a$, $f_i^{-1} (x) \cap {\mathbb {Q}}^b$, $f_i^{-1} (x) \cap \overline{\mathbb {Q}}^a$, and $f_i^{-1} (x) \cap \overline{{\mathbb {Q}}}^b$ are left-unbounded (notice that surjectivity of $f_i$ immediately follows);

(iii):

for each $x,y \in {\mathbb {R}}$, if $x < y$, then there exist:

• $u_1 \in {\mathbb {Q}}^a$ such that $x < u_1 < y$ and $y > f_i(u_1)$,

• $u_2 \in {\mathbb {Q}}^b$ such that $x < u_2 < y$ and $y > f_i(u_2)$,

• $u_3 \in \overline{{\mathbb {Q}}}^a$ such that $x < u_3 < y$ and $y > f_i(u_3)$, and

• $u_4 \in \overline{{\mathbb {Q}}}^b$ such that $x < u_4 < y$ and $y > f_i(u_4)$.

In addition, function $f_2$ satisfies the following property:

(iv):

for each $w \in (0,3)$, $f_2(w) < 3$.

At this point, we are ready to define the models $M_1$ and $M_2$, and the bisimulation relation between their intervals. Let $i \in \{1,2\}$ and $M_{i} = \langle {\mathbb {I}}({\mathbb {R}}), V_{f_i} \rangle$, where the valuation functions $V_{i} : {{\mathcal {AP}}} \rightarrow 2^{{\mathbb {I}}({\mathbb {R}})}$ is defined as follows:

$$\begin{aligned}{}[x,y] \in V_i(p) \Leftrightarrow \text {either } y = f_i(x) \text { or both } y < f_i(x) \text { and } [x,y] \in {\mathcal {S}}_i. \end{aligned}$$

The relation Z is defined as follows:

$$\begin{aligned}{}[x,y]Z[w,z] \Leftrightarrow x \equiv w \text {, } y \equiv z \text {, and } [x,y] \equiv _l [w,z], \end{aligned}$$

where the relations $\equiv$ and $\equiv _l$ are defined, respectively, in the following way:

$$\begin{aligned}&x \equiv w \Leftrightarrow x \in {\mathbb {Q}} \text { iff } w \in {\mathbb {Q}} \\&[x,y] \equiv _l [w,z] \Leftrightarrow \left\{ \begin{array}{l@{\quad }l} \text {either} &{} y > f_1(x) \text { and } z > f_2(w) \\ \text {or} &{} y = f_1(x) \text { and } z = f_2(w) \\ \text {or} &{} y < f_1(x) \text {, } z < f_2(w) \text {, and } ([x,y] \in {\mathcal {S}}_1 \text { iff } [w,z] \in {\mathcal {S}}_2) \end{array} \right. \end{aligned}$$

Now, by the definition of Z, we have that [0, 3]Z[0, 3] (notice that this is also a consequence of the facts that $f_1(0) = f_2(0)$ and that $[0,3]R_O,[0,3]$ does not hold). Moreover, it is easy to see that $M_{1},[0,3] \Vdash \langle O \rangle p$, while $M_{2},[0,3] \Vdash \lnot \langle O \rangle p$ (this is a direct consequence of property (iv) of $f_2$ and of the fact that $f_1(x) > 3$ for some $x \in (0,3)$).

We show that Z is an $\mathsf {A B D\overline{A B E}}$- bisimulation. For the local condition, consider two intervals [x, y] and [w, z] such that [x, y]Z[w, z]. First, we assume that $[x,y] \in V_1(p)$ and we show that $[w,z] \in V_2(p)$ follows. Since $[x,y] \in V_1(p)$, either $y = f_1(x)$ holds or both $y < f_1(x)$ and $[x,y] \in {\mathcal {S}}_1$ hold. In the former case, by the definition of Z, it must be $z = f_2(w)$, which implies $[w,z] \in V_2(p)$. In the latter case, by the definition of Z, both $z < f_2(w)$ and $[w,z] \in {\mathcal {S}}_2$ hold, and thus $[w,z] \in V_2(p)$. Second, we assume that $[w,z] \in V_2(p)$ and we show that $[x,y] \in V_1(p)$ follows. Since $[w,z] \in V_2(p)$, either $z = f_2(w)$ holds or both $z < f_2(w)$ and $[w,z] \in {\mathcal {S}}_2$ hold. In the former case, by the definition of Z, it must be $y = f_1(x)$, which implies $[x,y] \in V_1(p)$. In the latter case, by the definition of Z, both $y < f_1(x)$ and $[x,y] \in {\mathcal {S}}_1$ hold, and thus $[x,y] \in V_1(p)$.

In order to prove that the forward condition is satisfied, we assume that [x, y]Z[w, z] and $[x,y] R_X [x',y']$, for some $X \in \{ A, B, D, \overline{A}, \overline{B}, \overline{E} \}$ and some $[x,y], [w,z], [x',y'] \in {\mathbb {I}}({\mathbb {R}})$, and we show the existence of an interval $[w',z']$ such that $[x',y']Z[w',z']$ and $[w,z] R_X [w',z']$. As usual, we proceed by considering each case in turn.

• If $X = A$, then we distinguish three cases.

  • If $y' > f_1(x')$ and $y' \in {\mathbb {Q}}$ (resp., $y' \in \overline{{\mathbb {Q}}}$), then we select $z'$ such that $z' > f_2(z)$ and $z' \in {\mathbb {Q}}$ (resp., $z' \in \overline{{\mathbb {Q}}}$).

  • If $y' = f_1(x')$, then $y' \in {\mathbb {Q}}$, and we select $z' = f_2(z)$.

  • If $y' < f_1(x')$ and $y' \in {\mathbb {Q}}$ (resp., $y' \in \overline{{\mathbb {Q}}}$), then, by property (3) on page 21, there exists a point $z' \in {\mathbb {Q}}$ (resp., $z' \in \overline{{\mathbb {Q}}}$) such that $z < z' < f_2(z)$ and $[x',y'] \in {\mathcal {S}}_1$ iff $[z,z'] \in {\mathcal {S}}_2$ (notice that property (i) of $f_2$ plays a role here).

  In all cases, the interval $[z,z']$ is such that $[x',y']Z[z,z']$ and $[w,z] R_A [z,z']$.

• If $X = B$, then we distinguish three cases.

  • If $y' > f_1(x')$ and $y' \in {\mathbb {Q}}$ (resp., $y' \in \overline{{\mathbb {Q}}}$), then it must be $y > f_1(x)$ (as $y > y'$ and $x = x'$), which implies $z > f_2(w)$, and we select $z'$ such that $f_2(w) < z' < z$ and $z' \in {\mathbb {Q}}$ (resp., $z' \in \overline{{\mathbb {Q}}}$).

  • If $y' = f_1(x')$, then $y' \in {\mathbb {Q}}$ and $y > f_1(x)$ (as $y > y'$ and $x = x'$), which implies $z > f_2(w)$, and we select $z' = f_2(w)$.

  • If $y' < f_1(x')$ and $y' \in {\mathbb {Q}}$ (resp., $y' \in \overline{{\mathbb {Q}}}$), then, by property (3) on page 21, there exists a point $z' \in {\mathbb {Q}}$ (resp., $z' \in \overline{{\mathbb {Q}}}$) such that $w < z' < f_2(w)$ and $[x',y'] \in {\mathcal {S}}_1$ iff $[w,z'] \in {\mathcal {S}}_2$ (notice that property (i) of $f_2$ plays a role here).

  In all cases, the interval $[w,z']$ is such that $[x',y']Z[w,z']$ and $[w,z] R_B [w,z']$.

• If $X = D$, then we first select a point $w'$ such that $w < w' < z$, $w' \in {\mathbb {Q}}$ iff $x' \in {\mathbb {Q}}$, and $f_2(w') < z$ (the existence of such a point is guaranteed by property (iii) of $f_2$). Then, we select a point $z'$ as follows.

  • If $y' > f_1(x')$ and $y' \in {\mathbb {Q}}$ (resp., $y' \in \overline{{\mathbb {Q}}}$), then we select $z'$ such that $f_2(w) < z' < z$ and $z' \in {\mathbb {Q}}$ (resp., $z' \in \overline{{\mathbb {Q}}}$).

  • If $y' = f_1(x')$, then $y' \in {\mathbb {Q}}$, and we select $z' = f_2(w)$. Notice that $z' \in {\mathbb {Q}}$ as well.

  • If $y' < f_1(x')$ and $y' \in {\mathbb {Q}}$ (resp., $y' \in \overline{{\mathbb {Q}}}$), then, by property (3) on page 21, there exists a point $z' \in {\mathbb {Q}}$ (resp., $z' \in \overline{{\mathbb {Q}}}$), such that $w' < z' < f_2(w')$ and $[x',y'] \in {\mathcal {S}}_1$ iff $[w',z'] \in {\mathcal {S}}_2$ (notice that property (i) of $f_2$ plays a role here).

  In all cases, the interval $[w',z']$ is such that $[x',y']Z[w',z']$ and $[w,z] R_D [w',z']$.

• If $X = \overline{A}$, then we distinguish three cases.

  • If $y' > f_1(x')$ and $x' \in {\mathbb {Q}}$ (resp., $x' \in \overline{{\mathbb {Q}}}$), then consider a point $\overline{z} \in {\mathbb {Q}}$ such that $\overline{z} < w$. We select a point $w' \in {\mathbb {Q}}$ (resp., $w' \in \overline{{\mathbb {Q}}}$) such that $w' < \overline{z} < w$ and $f_2(w') = \overline{z}$ (the existence of such a point is guaranteed by property (ii) of $f_2$).

  • If $y' = f_1(x')$ and $x' \in {\mathbb {Q}}$ (resp., $x' \in \overline{{\mathbb {Q}}}$), then $y' = x \in {\mathbb {Q}}$, which implies $w \in {\mathbb {Q}}$. We select a point $w' \in {\mathbb {Q}}$ (resp., $w' \in \overline{{\mathbb {Q}}}$) such that $w' < w$ and $f_2(w') = w$ (the existence of such a point is guaranteed by property (ii) of $f_2$).

  • If $y' < f_1(x')$ and $x' \in {\mathbb {Q}}$ (resp., $x' \in \overline{{\mathbb {Q}}}$), then consider a point $\overline{z} \in {\mathbb {Q}}$ such that $\overline{z} > w$. We select a point $w' \in {\mathbb {Q}}$ (resp., $w' \in \overline{{\mathbb {Q}}}$) such that $w' < \min \{ 0,w \}$, $f_2(w') = \overline{z}$, and $[w',w] \in {\mathcal {S}}_2$ iff $[x',y'] \in {\mathcal {S}}_1$ (the existence of such a point is guaranteed by property (ii) of $f_2$). Notice that, since $w' < 0$, it is not the case that $[0,3] R_O [w',w]$.

  In all cases, the interval $[w',w]$ is such that $[x',y']Z[w',w]$ and $[w,z] R_{\overline{A}} [w',w]$.

• If $X = \overline{B}$, then we distinguish three cases.

  • If $y' > f_1(x')$ and $y' \in {\mathbb {Q}}$ (resp., $y' \in \overline{{\mathbb {Q}}}$), then we select $z'$ such that $z' > z$ and $z' \in {\mathbb {Q}}$ (resp., $z' \in \overline{{\mathbb {Q}}}$),

  • If $y' = f_1(x')$, then $y' \in {\mathbb {Q}}$ and $y < f_1(x)$ (as $y < y'$ and $x = x'$), which implies $z < f_2(w)$, and we select $z' = f_2(w)$.

  • If $y' < f_1(x')$ and $y' \in {\mathbb {Q}}$ (resp., $y' \in \overline{{\mathbb {Q}}}$), then it must be the case that $y < f_1(x)$ (as $y < y'$ and $x = x'$). This yields $z < f_2(w)$, and we select $z' \in {\mathbb {Q}}$ (resp., $z' \in \overline{{\mathbb {Q}}}$) such that $z < z' < f_2(w)$ and $[x',y'] \in {\mathcal {S}}_1$ iff $[w,z'] \in {\mathcal {S}}_2$ Notice that the existence of such a point strongly depends on the fact that it is not the case that $[0,3] R_O [w,z']$. By way of contradiction, suppose that $[0,3] R_O [w,z']$ holds. Then, we have $0 < w < 3 < z'$. By property (iv) of $f_2$, $0 < w < 3$ implies $f_2(w) < 3$, and thus $z' < 3$ (as $z' < f_2(w)$), contradicting the fact that $0 < w < 3 < z'$ holds.

  In all cases, the interval $[w,z']$ is such that $[x',y']Z[w,z']$ and $[w,z] R_{\overline{B}} [w,z']$.

• If $X = \overline{E}$, then we distinguish three cases.

  • If $y' > f_1(x')$ and $x' \in {\mathbb {Q}}$ (resp., $x' \in \overline{{\mathbb {Q}}}$), then consider a point $\overline{z} \in {\mathbb {Q}}$ such that $\overline{z} < z$. We select a point $w' \in {\mathbb {Q}}$ (resp., $w' \in \overline{{\mathbb {Q}}}$) such that $w' < w$ and $f_2(w') = \overline{z}$ (the existence of such a point is guaranteed by property (ii) of $f_2$).

  • If $y' = f_1(x')$ and $x' \in {\mathbb {Q}}$ (resp., $x' \in \overline{{\mathbb {Q}}}$), then $y' = y \in {\mathbb {Q}}$, which implies $z \in {\mathbb {Q}}$. We select a point $w' \in {\mathbb {Q}}$ (resp., $w' \in \overline{{\mathbb {Q}}}$) such that $w' < w$ and $f_2(w') = z$ (the existence of such a point is guaranteed by property (ii) of $f_2$).

  • If $y' < f_1(x')$ and $x' \in {\mathbb {Q}}$ (resp., $x' \in \overline{{\mathbb {Q}}}$), then consider a point $\overline{z} \in {\mathbb {Q}}$ such that $\overline{z} > z$. We select a point $w' \in {\mathbb {Q}}$ (resp., $w' \in \overline{{\mathbb {Q}}}$) such that $w' < \min \{ 0,w \}$, $f_2(w') = \overline{z}$, and that $[w',w] \in {\mathcal {S}}_2$ if and only if $[x',y'] \in {\mathcal {S}}_1$ (the existence of such a point is guaranteed by property (ii) of $f_2$). Notice that, since $w' < 0$, it is not the case that $[0,3] R_O [w',z]$.

  In all cases, the interval $[w',z]$ is such that $[x',y']Z[w',z]$ and $[w,z] R_{\overline{E}} [w',z]$.

The backward condition can be verified in a very similar way and thus we omit the details of the proof. Therefore, Z is an $\mathsf {A B D\overline{A B E}}$-bisimulation that violates $\langle O \rangle$, hence the thesis. $\square$