Proof. Both items can be proved by a straightforward induction on the complexity of $\varphi $ . We omit the details.

Proof. Given a cell C of , we fix some formula $\chi _{C}$ in $\mathtt {GML}^{\infty }_{q,n}$ , as given by Theorem 3.4; that is, $\chi _{C}$ characterises the pointed models in C.

Let $q,n$ and K be as in the formulation of the proposition. Define $\chi _{K} \mathrel {:=} \bigvee \chi _{C}$ , where we take the disjunction over all cells C of that contain a pointed model in K. Observe that the formula $\chi _{K}$ is well formed since the relation has finite index. We claim that $\chi _{K}$ characterises K, in the sense that, for any pointed model $(\mathbb {S},s)$ :

$$\begin{align*}(\mathbb{S},s) \text{ belongs to } K \text{ iff } \mathbb{S},s \Vdash \chi_{K}. \end{align*}$$

To see this, fix a pointed model $(\mathbb {S},s)$ , and let C be its equivalence class under the relation . It follows by Theorem 3.4 that $\mathbb {S},s \Vdash \chi _{C}$ .

If $(\mathbb {S},s)$ belongs to K then by definition of $\chi _{K}$ the formula $\chi _{C}$ will be one of the disjuncts of $\chi _{K}$ , so that we find $\mathbb {S},s \Vdash \chi _{K}$ as required. Conversely, if $\mathbb {S},s \Vdash \chi _{K}$ then by definition of $\chi _{K}$ we have that $\mathbb {S},s \Vdash \chi _{C'}$ for some -cell $C'$ which contains a pointed model $(\mathbb {S}',s')$ in K. It follows from $\mathbb {S},s \Vdash \chi _{C'}$ that $C' = C$ , and so both $(\mathbb {S},s)$ and $(\mathbb {S}',s')$ belong to this class. This means that , and from this we find $(\mathbb {S},s)$ in K by the assumption that K is -saturated.

Proof. Fix a formula $\varphi (x) \in \mathtt {FO}^{\infty }$ of quantifier depth q, and assume that $\varphi $ is invariant under taking disjoint unions. Define $n \mathrel {:=} 3^{q}$ , and let $(\mathbb {S},s)$ be an arbitrary pointed model. In order to prove the proposition, by invariance under taking disjoint unions it obviously suffices to prove that

(3) $$ \begin{align} \mathbb{S} \uplus \mathbb{D} \models \varphi[s] \text{ iff } \mathbb{B} \uplus \mathbb{D} \models \varphi[s], \end{align} $$

where $\mathbb {B} \mathrel {:=} \mathbb {B}^{\mathbb {S}}(s,n)$ and $\mathbb {D}$ is the disjoint union of q many copies of $\mathbb {S}$ and q many copies of $\mathbb {B}$ . As mentioned, our proof of (3) will be game-theoretic in nature. In view of Proposition 2.29 it suffices to show the following:

(4) $$ \begin{align} \text{Duplicator has a winning strategy in } \texttt{EF}_{q}^{\infty}(\mathbb{S} \uplus \mathbb{D}, \mathbb{B} \uplus \mathbb{D})@(s,s). \end{align} $$

To formulate our proof of (4), we need to introduce some further terminology and notation. To start with, we need some more detail in our notation for the models $\mathbb {S} \uplus \mathbb {D}$ and $\mathbb {B} \uplus \mathbb {D}$ . For $i \in \{-q,\ldots ,q\}$ we let $\mathbb {S}_{i}$ be the isomorphic copy of $\mathbb {S}$ based on the set $S_{i} = S \times \{i\}$ , where the projection map $\pi _{i}: S_{i} \to S$ is the witnessing isomorphism, and similarly for $\mathbb {B}_{i}$ . We identify $\mathbb {S}_{0}$ with $\mathbb {S}$ and $\mathbb {B}_{0}$ with $\mathbb {B}$ , and define

$$\begin{align*}\mathbb{D} \mathrel{:=} \biguplus_{-q \leq i < 0} \mathbb{S}_{i} \;\uplus\; \biguplus_{0 < i \leq q} \mathbb{B}_{i}, \end{align*}$$

so that we may think of $\mathbb {S} \uplus \mathbb {D}$ as the structure $\biguplus _{-q \leq i \leq 0} \mathbb {S}_{i} \;\uplus \; \biguplus _{0 < i \leq q} \mathbb {B}_{i}$ , and of $\mathbb {B} \uplus \mathbb {D}$ as the structure $\biguplus _{-q \leq i < 0} \mathbb {S}_{i} \;\uplus \; \biguplus _{0 \leq i \leq q} \mathbb {B}_{i}$ . We will refer to a point u in $\mathbb {S} \uplus \mathbb {D}$ as being $\mathbb {K}$ -type, with $\mathbb {K} \in \{ \mathbb {S},\mathbb {B} \}$ , if u belongs to $\mathbb {K}_{i}$ for some $i\in \{-q,..q\}$ .

Given a k-configuration $(\overline {u},\overline {u}')$ arising during a match of the game, we let $N_{k}(\overline {u})$ and $N_{k}(\overline {u}')$ be the sets

$$\begin{align*}N_{k}(\overline{u}) \mathrel{:=} \bigcup_{i} N^{\mathbb{S}\uplus\mathbb{D}}(u_{i},3^{q-k}), \quad N^{\prime}_{k}(\overline{u}^{\prime}) \mathrel{:=} \bigcup_{i} N^{\mathbb{B}\uplus\mathbb{D}}(u^{\prime}_{i},3^{q-k}), \end{align*}$$

respectively. In other words, $N_{k}(\overline {u})$ is the union of the $3^{q-k}$ -neighbourhoods of the different worlds in $\overline {u}$ . In particular, every point in $N_{k}(\overline {u})$ is, at most, at a distance $3^{q-k}$ from one of the worlds in $\overline {u}$ . Analogous observations apply to $N^{\prime }_{k}(\overline {u}^{\prime })$ .

The key observation in the proof of (4) is that Duplicator can maintain the condition that, where $(\overline {u},\overline {u}')$ is any configuration reached during a play of $\texttt {EF}_{q}^{\infty }(\mathbb {S} \uplus \mathbb {D}, \mathbb {B} \uplus \mathbb {D})@(s,s)$ ,

• (†) there is a local isomorphism $f: N_{k}(\overline {u}) \to N^{\prime }_{k}(\overline {u}^{\prime })$ such that $f(u_{i}) = u^{\prime }_{i}$ , for all i.

It should be clear that this condition holds at the start of the game, where $k = 0$ .

Now assume that, inductively, for some $k<q$ the condition (†) holds for some k-configuration $(\overline {u},\overline {u}')$ , witnessed by some local isomorphism f. We need to prove that to any challenge of Spoiler, Duplicator has a response that guarantees the resulting $k+1$ -configuration to again satisfy (†). We show this by distinguishing cases, as to the kind of move Spoiler makes.

• Case 1. First assume that Spoiler makes a first-order move. In this case we proceed very much in the same way as Goranko and Otto in [Reference Goranko, Otto, Blackburn, Benthem and Wolter16]. Without loss of generality we may assume that he picks an element, say, u, of the structure $\mathbb {S} \uplus \mathbb {D}$ ; then we need to identify a point $u'$ in $\mathbb {B} \uplus \mathbb {D}$ as a suitable reply for Duplicator. We make a further case distinction as to whether u is close to one of the points in the existing tuple $\overline {u}$ or not.

  • Case 1a. $\mathit {gaif}(u,u_{i}) \leq 2 \cdot 3^{q-(k+1)}$ for some $i \in \{0,\ldots ,k\}$ . The crucial observation in this case is that we have $N_{k+1}(\overline {u}\cdot u) \subseteq N_{k}(\overline {u})$ ; the verification of this statement is a simple exercise in Gaifman metric. We then simply define $u' \mathrel {:=} f(u)$ , and it is straightforward to check that f restricts to a local isomorphism from $N_{k+1}(\overline {u}\cdot u)$ to $N^{\prime }_{k+1}(\overline {u}^{\prime }\cdot u^{\prime })$ . Since we have $f(u_{i}) = u^{\prime }_{i}$ by assumption and $f(u) = u'$ by definition, this shows that indeed Duplicator can keep the condition (†) for one more round.

  • Case 1b. $\mathit {gaif}(u,u_{i})> 2 \cdot 3^{q-(k+1)}$ for all $i \in \{0,\ldots ,k\}$ . The crucial statement is now that the set $N^{\mathbb {S}\uplus \mathbb {D}}(u,3^{q-(k+1)})$ does not overlap with any set $N^{\mathbb {S}\uplus \mathbb {D}}(u_{i},3^{q-(k+1)})$ , so that $N_{k+1}(\overline {u}\cdot u)$ is the disjoint union of the sets $\bigcup _{i} N^{\mathbb {S}\uplus \mathbb {D}}(u_{i},3^{q-(k+1)})$ and $N^{\mathbb {S}\uplus \mathbb {D}}(u,3^{q-(k+1)})$ . We will assume that u is an $\mathbb {S}$ -type point of $\mathbb {S}\uplus \mathbb {D}$ (the case where u is $\mathbb {B}$ -type is dealt with analogously). That is, u belongs to $\mathbb {S}_{j}$ for some j, and we may write $u = (\pi _{j}(u),j)$ with $\pi _{j}(u)$ in $\mathbb {S}$ .

    Since $\overline {u}'$ comprises at most $k+1$ elements, where $k < q$ , $\mathbb {D}$ contains q distinct copies of $\mathbb {S}$ , and the initial state $u^{\prime }_{0}$ does not belong to $\mathbb {D}$ (but to $\mathbb {B}$ ), the target structure $\mathbb {B} \uplus \mathbb {D}$ will have a “fresh” copy of $\mathbb {S}$ , so to speak. That is, we may consider some r such that $\mathbb {S}_{r}$ contains none of the $u^{\prime }_{i}$ . We now define $u' \mathrel {:=} (\pi _{j}(u),r)$ ; in other words, we use the obvious isomorphism between $\mathbb {S}_{j}$ and $\mathbb {S}_{r}$ to find $u'$ . Now consider the following map $f'$ on $N_{k+1}(\overline {u}\cdot u)$ :

    (5) $$ \begin{align} f'(s) \mathrel{:=} \left\{ \begin{array}{ll} f(s), & \text{if } s \in \bigcup_{i} N^{\mathbb{S}\uplus\mathbb{D}}(u_{i},3^{q-(k+1)}), \\[2mm] (\pi_{j}(s),r), & \text{if } s \in N^{\mathbb{S}\uplus\mathbb{D}}(u,3^{q-(k+1)}). \end{array} \right. \end{align} $$
    It is then a routine exercise to verify that $f'$ is well defined, and that it provides the required local isomorphism between $N_{k+1}(\overline {u}\cdot u)$ and $N^{\prime }_{k+1}(\overline {u}^{\prime }\cdot u^{\prime })$ . Since again we have $f^{\prime }(u_{i}) = u^{\prime }_{i}$ by assumption and $f'(u) = u'$ by definition, it follows that in this case as well, Duplicator can keep the condition (†) for one more round.

• Case 2. Now assume that Spoiler makes a second-order move. Without loss of generality we may assume that he picks an infinite subset, say, U, of the structure $\mathbb {S}\uplus \mathbb {D}$ . Similar to Case 1, we make a further case distinction, but now as to whether infinitely many elements of U are close to one of the points in the existing tuple $\overline {u}$ or not.

  • Case 2a. There are infinitely many $u \in U$ such that $\mathit {gaif}(u,u_{i}) \leq 2 \cdot 3^{q-(k+1)}$ for some $i \in \{0,\ldots ,k\}$ .

    Let $X \subseteq U$ be the set of all these elements, then the key observation—as in the first-order move case—is that for each $u \in X$ we have $N_{k+1}(\overline {u}\cdot u) \subseteq N_{k}(\overline {u})$ . Let

    $$\begin{align*}U' \mathrel{:=} f[X] \end{align*}$$
    be Duplicator’s response to Spoiler’s move U. Since f is a bijection between $N_{k}(\overline {u})$ and $N^{\prime }_{k}(\overline {u}^{\prime })$ , we immediately see that $U'$ is an infinite subset of $N^{\prime }_{k}(\overline {u}')$ . Now suppose that, continuing the match, Spoiler picks an element $u' \in U'$ ; then by definition there is a $u \in X$ such that $u' = f(u)$ , and Duplicator will pick this u as her response to Spoiler’s move $u'$ . As in Case 1 above, it is then straightforward to verify that the restriction of f to the set $N_{k+1}(\overline {u}\cdot u)$ witnesses that Duplicator has maintained (†) for one more round.

  • Case 2b. There are infinitely many $u \in U$ such that $\mathit {gaif}(u,u_{i})> 2 \cdot 3^{q-(k+1)}$ for all $i \in \{0,\ldots ,k\}$ .

    Let $X \subseteq U$ be the set of all these elements, then the key observation is, as in Case 1b, that for each $u \in X$ we have

    $$\begin{align*}N_{k+1}(\overline{u}\cdot u) \;=\; \bigcup_{i} N^{\mathbb{S}\uplus\mathbb{D}}(u_{i},3^{q-(k+1)}) \;\uplus\; N^{\mathbb{S}\uplus\mathbb{D}}(u,3^{q-(k+1)}). \end{align*}$$
    Furthermore, by the pigeonhole principle, X must contain either infinitely many $\mathbb {S}$ -type points or infinitely many $\mathbb {B}$ -type points. We assume the first (again, the other case is very similar). For $j \in \{-q,\ldots ,0\}$ , let $X_{j}$ be the set of points in X that belong to $\mathbb {S}_{j}$ ; then, once more by the pigeonhole principle, there is an index j such that $X_{j}$ is infinite. As in Case 1b we may then take some r such that $\mathbb {S}_{r}$ contains none of the $u^{\prime }_{i}$ . We are now ready to define Duplicator’s response to Spoiler’s move U:
    $$\begin{align*}U' \mathrel{:=} \{ (\pi_{j}(u),r) \mid u \in X_{j} \}. \end{align*}$$
    That is, again we use the obvious isomorphism between $\mathbb {S}_{j}$ and $\mathbb {S}_{r}$ to find $U'$ in $\mathbb {S}_{r}$ as the counterpart of $X_{j}$ in $\mathbb {S}_{j}$ . Clearly then, $U'$ is infinite, so that it constitutes a legitimate move for Duplicator. Now assume that Spoiler continues the match by picking an element $u' \in U$ . Then by definition $u'$ is of the form $u' = (\pi _{j}(u),r)$ for some $u \in X_{j}$ , and since $X_{j} \subseteq U$ , Duplicator may pick this element u as her response to Spoiler.

    As discussed in Case 1b, it is now straightforward to verify that the map $f'$ as defined in (5), is a local isomorphism from $N_{k+1}(\overline {u}\cdot u)$ to $N^{\prime }_{k+1}(\overline {u}^{\prime }\cdot u^{\prime })$ that witnesses the fact that Duplicator has carried the condition (†) one round further.

This finishes the proof of (4), and, as discussed, this suffices to prove the proposition.

Proof. It is almost immediate from the definition that the relation of being q-companions is an equivalence relation. A routine inductive argument shows that this equivalence relation has finite index if we restrict to nodes of arbitrary but fixed height. From this the proposition is immediate.

Proof. Let $\mathbb {T},\mathbb {T}',t$ and $t'$ be as in the formulation of the lemma.

For the proof of item 1 we first consider the special case where v is a successor of t. By Theorem 3.4 there is a formula $\chi \in \mathtt {GML}^{\infty }_{q-h(v),q}$ characterising the -cell of $(\mathbb {T},v)$ . It follows from $\mathbb {T},v \Vdash \chi $ that $\mathbb {T},t \Vdash \lozenge \chi $ . Observe that the formula $\lozenge \chi $ belongs to the set $\mathtt {GML}^{\infty }_{(q-h(v))+1,q} = \mathtt {GML}^{\infty }_{q-h(t),q}$ , where the equality holds as $h(t) = h(v)-1$ . By the q-companionship of t and $t'$ we obtain that $\mathbb {T}',t'\Vdash \lozenge \chi $ , so that $t'$ must have a successor $v'$ such that $\mathbb {T}', v' \Vdash \chi $ . It is then immediate by Theorem 3.4 that , and since t and $t'$ are q-companions it easily follows that v and $v'$ must be q-companions as well.

The general case, where v is an arbitrary (not necessarily one-step) descendant of t, is then easily derived from the special case via a straightforward induction on the distance from t to v.

For the proof of item 2, let V be an infinite set of nodes in $\mathbb {T}$ that all belong to the same q-companion class. Clearly then all nodes in V have the same height, a number that we will denote as $h(V)$ . Furthermore, since all nodes in V are q-companions of one another, there is a formula $\chi \in \mathtt {GML}^{\infty }_{q-h(V),q}$ characterising the -cell of the nodes in V. This means in particular that $\mathbb {T},v \Vdash \chi $ for all $v \in V$ .

Now consider an arbitrary common ancestor u of all nodes in V; it is easy to see that u has the same distance to each node in V, so that it makes sense to talk about the distance $d(u,V)$ of u to the set V. We will prove, by induction on this distance, that u has a q-companion $u'$ which has infinitely many descendants that all belong to the q-companion class of V. Clearly this suffices to prove item 2.

In the base step of this induction we assume that $d(u,V) = 1$ ; that is, $V \subseteq R(u)$ . Since V is infinite this means that $\mathbb {T},u \Vdash \lozenge ^{\infty } \chi $ . Now observe that as $\chi $ belongs to the set $\mathtt {GML}_{q - h(V),q}^{\infty ,q}$ , we find that $\lozenge ^{\infty } \chi \in \mathtt {GML}_{(q - h(V)) + 1,q}^{\infty } = \mathtt {GML}_{q - h(u),q}^{\infty }$ . From this and the assumption on u and $u'$ it follows that $\mathbb {T}',u' \Vdash \lozenge ^{\infty } \chi $ . In other words, there is an infinite set $V'$ of successors of $u'$ , such that each $v'\in V'$ satisfies the characteristic formula $\chi $ . By Theorem 3.4 this means that , for each $v' \in V'$ and $v \in V$ , and since the predecessor $u'$ of any such $v'$ is a q-companion of the predecessor u of any such v, we find that every $v' \in V'$ is a q-companion of every $v \in V$ . But then we are done, since $V'$ is an infinite set of descendants of $u'$ .

For the inductive step, assume that $d(u,V) = k + 1$ . We make a case distinction.

First assume that u has a successor w such that $|V \cap R^{k}(w)|$ is infinite. By (the proof of) item 1, $u'$ has a successor $w'$ which is a q-companion of w. Clearly we have $d(w,V) = d(u,V) -1$ , so that we may apply the inductive hypothesis to w. This yields an infinite set $V'$ of descendants of $w'$ , all belonging to the same q-companion class as the nodes in V. It is not hard to see that this set $V'$ meets the required conditions with respect to u and V as well.

If, on the other hand, u has no successor w such that $|V \cap R^{k}(w)|$ is infinite, then it must have an infinite set W of successors, each of which has at least one descendant in V. Without loss of generality we may assume that all nodes in W are q-companions of one another (if not, by Lemma 3.11 W would have an infinite subset with this property, and we could continue with this subset). This means in particular that the nodes in W belong to the same cell of the equivalence relation . Writing $\psi \in \mathtt {GML}^{\infty }_{q-(h(u)+1),q}$ for the characteristic formula of this equivalence class, we clearly have that u satisfies the formula $\lozenge ^{\infty }\psi $ . But since this formula belongs to the set $\mathtt {GML}^{\infty }_{q-h(u),q}$ , it must hold at the q-companion $u'$ of u as well, i.e., there is an infinite set $W'$ of successors of $u'$ , all satisfying the formula $\psi $ . As before we may derive from this that every $w' \in W'$ is a q-companion of every $w \in W$ . But then by item 1 every $w' \in W'$ has a descendant $v^{\prime }_{w^{\prime }}$ that is a q-companion of some descendant in V of some successor w of u. From this we easily derive that the set $V^{\prime } \mathrel {:=} \{ v^{\prime }_{w^{\prime }} \mid w^{\prime } \in W^{\prime } \}$ has the required properties—note that the set is infinite since $W'$ is infinite and $\mathbb {T}^{\prime }$ is a tree model.

Proof. Let $\mathbb {T},\mathbb {T}',\overline {u}$ and $\overline {u}'$ be as in the formulation of the lemma. Write $\overline {u} = u_{0}\cdots u_{k}$ and $\overline {u}^{\prime } = u^{\prime }_{0}\cdots u^{\prime }_{k}$ , and recall that $u_{0}$ and $u^{\prime }_{0}$ are the roots of $\mathbb {T}$ and $\mathbb {T}^{\prime }$ , respectively. Let $f: \mathbb {T}_{\overline {u}} \to \mathbb {T}^{\prime }_{\overline {u}^{\prime }}$ be an isomorphism witnessing the q-similarity of $\overline {u}$ and $\overline {u}'$ .

We first prove item 1. Let u be an arbitrary node in $\mathbb {T}$ . The case where u is actually a node of $\mathbb {T}_{\overline {u}}$ is easily dealt with by taking $u' \mathrel {:=} f(u)$ , so assume otherwise.

Consider the set

$$\begin{align*}X_{u} \mathrel{:=} \{ \mathit{lca}(u_{i},u) \mid 0 \leq i \leq k \}. \end{align*}$$

Since u does not belong to $T_{\overline {u}}$ , clearly each node in $X_{u}$ is a proper ancestor of u, and $X_{u}$ is linearly ordered by the ancestor relation. In particular, $X_{u}$ has a last element in this order, which we shall denote as $d_{u}$ . Let $Y_{u}$ be the set of nodes $u_{i}$ in $\overline {u}$ for which $d_{u} \neq u_{i}$ but $d_{u} = \mathit {lca}(u_{i},u)$ . If $Y_{u} = \emptyset $ it must be the case that for some i, $d_{u} = u_{i}$ while $d_{u} \not \in {\downarrow }(u_{j})$ for any $u_{j}\neq u_{i}$ . This case can be easily dealt with using Lemma 3.12(1), so in the sequel we assume that $Y_{u}$ is not empty. Note that $u_{0}$ , being the root of $\mathbb {T}$ , does not belong to $Y_{u}$ .

Consider the set $R(d_{u})$ of successors of $d_{u}$ . For each $x \in Y_{u} \cup \{ u \}$ we let $z_{x}$ denote the unique successor of $d_{u}$ which is an ancestor of x, and define $Z_{Y} \mathrel {:=} \{ z_{y} \mid y \in Y_{u} \}$ . It follows from the assumptions that $Z_{Y} \neq \emptyset $ and that $u_{0}, z_{u} \not \in Z_{Y}$ . Furthermore we obviously have $|Z_{Y}| \leq |Y_{u}|$ , and since $Y_{u} \subseteq \{ u_{i} \mid 0 < i \leq k \}$ we may use the assumption $k<q$ to obtain that $|Z_{Y}| < q$ .

Now we claim that $f(d_{u})$ has a successor $z_{u}'$ which is a q-companion of $z_{u}$ , but is not of the form $f(z)$ for any $z \in Z_{Y}$ . To see this, let $\chi \in \mathtt {GML}^{\infty }_{q-h(z_{u}),q}$ be a characteristic formula of the -cell of $z_{u}$ , and let m be the number of elements of $Z_{Y}$ that satisfy $\chi $ . Obviously then we have $\mathbb {T},d_{u} \Vdash \lozenge ^{\geq m+1}\chi $ , and since $m \leq |Z_{Y}| < q$ , the formula $\lozenge ^{\geq m+1}\chi $ belongs to the set $\mathtt {GML}^{\infty }_{(q- h(z_{u}))+1,q} = \mathtt {GML}^{\infty }_{q-h(u),q}$ . Since $d_{u}$ and $f(d_{u})$ are q-companions, the formula $\lozenge ^{\geq m+1}\chi $ must be preserved, so that $f(d_{u})$ must satisfy $\lozenge ^{\geq m+1}\chi $ as well. Hence $f(d)$ has at least $m+1$ successors satisfying $\chi $ . Using the facts that f is an isomorphism between $\mathbb {T}_{\overline {u}}$ and $\mathbb {T}^{\prime }_{\overline {u}^{\prime }}$ and that $\mathbb {T},z \Vdash \chi $ iff $\mathbb {T}',f(z) \Vdash \chi $ for all $z \in R(u)$ , we may conclude that $|\{ z' \in R'(f(d_{u})) \cap f[Z_{Y}] \mid \mathbb {T}',z' \Vdash \chi \}| = m$ . That is, there are exactly m successors of $f(d_{u})$ that are in the image of $f[Z_{Y}]$ and make $\chi $ true. But then there must a successor $z_{u}'$ of $f(d)$ that satisfies $\chi $ but does not belong to the set $f[Z_{Y}]$ . This node $z_{u}'$ is then the successor of $f(d_{u})$ that we are looking for (Figure 1).

Fig. 1

Lemma 3.14(1).

To finish the proof of the first item, observe that as $z_{u}$ and $z_{u}'$ are q-companions, it follows from Lemma 3.12(1) that $z^{\prime }_{u}$ has a descendant $u'$ which is a q-companion of u. It is then a fairly routine exercise to check that we may extend f to an isomorphism $g: \mathbb {T}_{\overline {u}\cdot u} \to \mathbb {T}^{\prime }_{\overline {u}^{\prime }\cdot u^{\prime }}$ which satisfies in addition that $g(z_{u}) = z^{\prime }_{u}$ and $g(u) = u'$ and that x and $g(x)$ are q-companions, for every x in $\mathbb {T}_{\overline {u}\cdot u}$ . This suffices to show that $\mathbb {T},\overline {u}\cdot u \approx ^{\downarrow }_{q} \mathbb {T}^{\prime },\overline {u}'\cdot u^{\prime }$ .

We now turn to the proof of item 2. Let U be some infinite subset of $\mathbb {T}$ . From the constraints on the set $U'$ that we are looking for, it follows that instead of working with U we may work with any subset of U that is guaranteed to be infinite—we will use this observation repeatedly (without explicit reference). For instance, by Lemma 3.11 we may without loss of generality assume that all nodes in U are q-companions of one another.

Similarly, since $T_{\overline {u}}$ is finite we may, without loss of generality assume that $U \cap T_{\overline {u}} = \emptyset $ . In addition, we may assume that all nodes in U have the same height and belong to the same q-companion class. Then for each $u \in U$ we define the set $X_{u}$ , the node $d_{u}$ , and the set $Y_{u}$ , exactly as in the proof of the first item. Since each $d_{u}$ belongs to the (finite) set of nodes of $\mathbb {T}_{\overline {u}}$ , and each $Y_{u}$ is a subset of the finite set $\{ u_{i} \mid 0 < i \leq k \}$ , we may without loss of generality assume that $d_{u} = d_{v}$ and $Y_{u} = Y_{v}$ , for all $u,v \in U$ . Hence we may drop subscripts and simply write d and Y. If $Y = \emptyset $ it must be the case that $d = u_{i}$ for some i, and as in the proof of item 1 we leave it for the reader to check that this case can be easily dealt with using Lemma 3.12 (in this case with item (2)).

As in the proof of item 1 of this lemma, we now focus on the set $R(d)$ of direct successors of d. For $x \in Y \cup U$ , we define $z_{x}$ to be the unique element of $R(d)$ which is an ancestor of x, and we set $Z_{Y} \mathrel {:=} \{ z_{y} \mid y \in Y \}$ and $Z_{U} \mathrel {:=} \{ z_{u} \mid u \in U \}$ . Similarly as before we have that $Z_{Y} \cap Z_{U} = \emptyset $ and $|Z_{Y}| < q$ . We now make a case distinction.

If $Z_{U}$ is finite, then we may without loss of generality assume that it is a singleton, say, $Z_{U} = \{ z \}$ where z is an ancestor of every $u \in U$ (Figure 2). In the same way as in the proof of item 1, we may show that $f(d)$ has a successor $z'$ which is a q-companion of z. It then follows by Lemma 3.12(2) that $\mathbb {T}'$ contains an infinite collection $U'$ of nodes that are all descendants of $z'$ and q-companions of the nodes in U. From this it is easily verified that any $u' \in U'$ and any $u \in U$ satisfy $\mathbb {T},\overline {u}\cdot u \approx ^{\downarrow }_{q} \mathbb {T}^{\prime },\overline {u}^{\prime }\cdot u^{\prime }$ , and this certainly suffices to prove the statement of item 2.

Fig. 2

Lemma 3.14(2) case a.

If, on the other hand, $Z_{U}$ is infinite (Figure 3), our first observation is that all nodes in $Z_{U}$ belong to the same q-companion class: this easily follows from the assumption (discussed above) that all nodes $u \in U$ are q-companions of one another. Define $\chi \in \mathtt {GML}^{\infty }_{q-h(z),q}$ as the characteristic formula of the -cell of some/any $z \in Z_{U}$ , then we have $\mathbb {T},d \Vdash \lozenge ^{\infty }\chi $ . From this we may use the q-companionship of d and $f(d)$ to derive that $\mathbb {T}',f(d) \Vdash \lozenge ^{\infty }\chi $ , so that $f(d)$ has an infinite set $W'$ of successors that all satisfy the formula $\chi $ . From this it readily follows that each $w' \in W'$ is a q-companion of each $z \in Z_{U}$ . Then by Lemma 3.12 each $w' \in W'$ has a descendant $u^{\prime }_{w^{\prime }}$ which is a q-companion of the nodes in U. Finally, it is a routine exercise to show that the set $U^{\prime } \mathrel {:=} \{ u^{\prime }_{w^{\prime }} \mid w^{\prime } \in W^{\prime }\}$ meets all the conditions as specified in the lemma.

Fig. 3

Lemma 3.14(2) case b.

Proof of Theorem 3.9

Fix some natural number $q \geq 1$ , let $\mathbb {T}$ and $\mathbb {T}'$ be tree models of height q, with roots r and $r'$ , respectively, and assume that . Obviously then, r and $r'$ are q-companions, and from this we readily see that, seen as two $1$ -tuples, they are q-similar: $\mathbb {T},r\approx ^{\downarrow }_{q}\mathbb {T}',r'$ . It then follows from successive applications of Lemma 3.12 that in the Ehrenfeucht–Fraïssé game $\texttt {EF}_{q}^{\infty }$ between $\mathbb {T},r$ and $\mathbb {T}',r'$ , Duplicator has a strategy ensuring that every configuration, that is reached in a match of this game, will consist of two q-similar tuples. Playing such a strategy, Duplicator thus guarantees that the final q-configuration $(\overline {u},\overline {u}')$ will be such that $\mathbb {T},\overline {u} \approx ^{\downarrow }_{q} \mathbb {T}',\overline {u}'$ . That is, there is a isomorphism f from $\mathbb {T}_{\overline {u}}$ to $\mathbb {T}^{\prime }_{\overline {u}^{\prime }}$ such that $f(u_{i}) = u^{\prime }_{i}$ , for all i; in particular then, f is a local isomorphism from $\overline {u}$ to $\overline {u}^{\prime }$ . In other words, any such strategy is a winning strategy for her.

This finishes the proof of Theorem 3.9.

Proof of Theorem 2.25

We focus on the forward direction of the proof. The backwards direction can be easily proved by induction on the complexity of the formula $\psi $ .

Fix some bisimulation invariant formula $\mathtt {FO}^{\infty }$ formula $\varphi (x)$ , and let q be its quantifier depth. Define $n \mathrel {:=} 3^{q}$ , then it follows from Proposition 3.7 that $\varphi $ is n-local. We first prove that $\varphi $ is -invariant (cf. (2)).

For that purpose, let $\mathbb {S},s$ and $\mathbb {S}',s'$ be two pointed Kripke models such that . We will prove that

(6) $$ \begin{align} \mathbb{S} \models \varphi[s] \text{ if and only if } \mathbb{S}' \models \varphi[s']. \end{align} $$

For a proof of (6), let $\mathbb {U}_{\infty }(\mathbb {S},s)$ be the unravelling of $(\mathbb {S},s)$ . That is, $\mathbb {U}_{\infty }(\mathbb {S},s)$ is a tree model whose states are the finite paths of $\mathbb {S}$ that start with s, and whose accessibility relation and valuation are defined in the obvious way. We refer to [Reference Blackburn, de Rijke and Venema5] for the details, and leave it for the reader to verify that , an observation that we will refer to below as (bisimulation invariance).

We let $\mathbb {U}_{n}(\mathbb {S},s)$ be the structure that is based on the n-neighbourhood of s in $\mathbb {U}_{\infty }(\mathbb {S},s)$ —this structure is sometimes referred to as the n-unravelling of $(\mathbb {S},s)$ , since its states correspond to the paths in $\mathbb {S}$ of length at most n that start at s. It follows by locality that $\mathbb {U}_{\infty }(\mathbb {S},s) \models \varphi [s]$ iff $\mathbb {U}_{n}(\mathbb {S},s) \models \varphi [s]$ , and of course a similar observation applies to the unravellings of $(\mathbb {S}',s')$ .

Furthermore, it is not hard to see that implies . From this we may derive by Theorem 3.9 that $\mathbb {U}_{n}(\mathbb {S},s),s \mathrel {\cong ^{\infty }_{n}} \mathbb {U}_{n}(\mathbb {S}',s'),s'$ , and so by Proposition 2.29 we find that $\mathbb {U}_{n}(\mathbb {S},s) \models \varphi [s]$ iff $\mathbb {U}_{n}(\mathbb {S}',s') \models \varphi [s']$ (*).

Now consider the following chain of equivalences:

$$ \begin{align*} \mathbb{S} \models \varphi[s] \text{ iff } & \mathbb{U}_{\infty}(\mathbb{S},s) \models \varphi[s] & \text{(bisimulation invariance)} \\ \text{ iff } & \mathbb{U}_{n}(\mathbb{S},s) \models \varphi[s] & \text{(locality, Theorem 2.25)} \\ \text{ iff } & \mathbb{U}_{n}(\mathbb{S}',s') \models \varphi[s'] & \text{((*) above)} \\ \text{ iff } & \mathbb{U}_{\infty}(\mathbb{S}',s') \models \varphi[s'] & \text{(locality, Theorem 2.25)} \\ \text{ iff } & \mathbb{S}' \models \varphi[s']. & \text{(bisimulation invariance)} \end{align*} $$

This finishes the proof of (6).

But if $\varphi $ is -invariant, then the class of pointed models satisfying $\varphi $ is -saturated (i.e., a union of -cells). It is then immediate from Proposition 3.5 that $\varphi $ is equivalent to some formula in $\mathtt {GML}^{\infty }_{n,n}$ .

Proof. The implication from (1) to (2) follows by Corollary 2.18, and the implication from (2) to (3) is trivial. The implications from (3) to (4) and from (4) to (5) will be proved in the Sections 4.4 and 4.3, respectively. Finally, the implication from (5) to (1) states that our axiomatisation is sound. The verification of this statement is a routine exercise which we leave to the reader.