LACL, Université Paris-Est Créteil<EMAIL_ADDRESS>Julien Grange
[100]Theory of computation Finite Model Theory John Q. Open and Joan R. Access
2 42nd Conference on Very Important Topics (CVIT 2016) CVIT 2016 CVIT 2016
December 24–27, 2016 Little Whinging, United Kingdom 42 23

# Order-Invariance in the Two-Variable Fragment of First-Order Logic

Julien Grange

###### Abstract

We study the expressive power of the two-variable fragment of order-invariant
first-order logic. This logic departs from first-order logic in two ways:
first, formulas are only allowed to quantify over two variables. Second,
formulas can use an additional binary relation, which is interpreted in the
structures under scrutiny as a linear order, provided that the truth value of
a sentence over a finite structure never depends on which linear order is
chosen on its domain.

We prove that on classes of structures of bounded degree, any property
expressible in this logic is definable in first-order logic. We then show that
the situation remains the same when we add counting quantifiers to this logic.

###### keywords:

Finite model theory, two-variable logic, order-invariance

###### category:

##  1 Introduction

The restriction of first-order logic to two variables ($\textsc{FO}^{2}$)
holds an important place among the fragments of first-order logic (FO), since
it is the maximal fragment, with respect to the number of variables, for which
the finite and general satisfiability problems are decidable [12] \- see [4]
for a complete survey on these issues. They become undecidable as soon as we
allow formulas to make use of three variables, as three variables are enough
to encode grids. Tame as it is in this regard, $\textsc{FO}^{2}$ is still
fairly expressive (in particular, it embeds modal logic). It is thus natural
to investigate its order-invariant extension $<\\!\textup{-inv
}$$\textsc{FO}^{2}$.

In the order-invariant extension $<\\!\textup{-inv }\mathcal{L}$ of a logic
$\mathcal{L}$, one can make use in the $\mathcal{L}$-formulas of a linear
order on the vertices of the structures at hand, provided that the validity of
said formulas in a given finite structure does not depend on the choice of a
particular order.

If $\mathcal{L}=\textsc{FO}$, we get $<\\!\textup{-inv }$FO, whose syntax is
not recursively enumerable. It has however been proven by Harwath and Zeume
[17] that on the other hand, $<\\!\textup{-inv }$$\textsc{FO}^{2}$ has a
recursive syntax. The natural follow-up to this result is to study the
expressive power of $<\\!\textup{-inv }$$\textsc{FO}^{2}$. This shall be our
endeavor in this article.

Perhaps surprisingly, it has been shown by Gurevich (see Section 5.2 of [11])
that such an order can indeed bring additional expressive power to FO, even
when restricted in this way: there exist properties which are not definable in
FO, but which can be expressed as soon as the use of a linear order is
authorized, even in an invariant fashion. In symbols: $<\\!\textup{-inv
}\textsc{FO}\not\subseteq\textsc{FO}$. It is not hard to observe that
$<\\!\textup{-inv }\textsc{FO}^{2}\not\subseteq\textsc{FO}^{2}$ (for instance,
one can state in $<\\!\textup{-inv }$$\textsc{FO}^{2}$ that a set has at least
three elements, which is not possible in $\textsc{FO}^{2}$). It is however not
clear whether $<\\!\textup{-inv }\textsc{FO}^{2}\subseteq\textsc{FO}$, or
whether even when restricted to two variables, the addition of an order allows
one to express properties beyond the scope of FO. This question is asked in
[17]. Is this paper, we prove that on any class of bounded degree, the
inclusion $<\\!\textup{-inv }\textsc{FO}^{2}\subseteq\textsc{FO}$ indeed holds
- this is Theorem 2.1, whose proof is the object of Sections 3 and 4.

We then explain in Section 5 how to extend this result from $<\\!\textup{-inv
}$$\textsc{FO}^{2}$ to $<\\!\textup{-inv }$$\textsc{C}^{2}$, where
$\textsc{C}^{2}$ is the extension of $\textsc{FO}^{2}$ with counting
quantifiers. Precisely, we show with Theorem 5.1 that $<\\!\textup{-inv
}\textsc{C}^{2}\subseteq\textsc{FO}$ when the degree is bounded.

Let us already mention that both of these inclusions are strict. This matter
is further discussed in the conclusion.

#### Related work

The question of the order-invariance of an $\textsc{FO}^{2}$-sentence has been
shown to be decidable in [17]. The expressive power of $<\\!\textup{-inv
}$$\textsc{FO}^{2}$ is only mentioned there as a follow up question.

We borrow the dichotomy between rare and frequent neighborhood types when the
degree is bounded from [6]. Beyond that, the philosophies of the constructions
differ widely: in [6], successor relations are constructed in a very regular
way, in order to create as few neighborhood types as possible in the
structures with successor. On the other hand, we make sure to realize all the
possible types in our construction.

One line of research investigates the expressive power of $<\\!\textup{-inv
}$FO. Let us mention [2] and [7], which prove that $<\\!\textup{-inv }$FO has
the same expressive power as FO respectively on trees and on hollow trees. The
present paper focuses on a weaker logic, but in a broader setting.
Furthermore, while the techniques used in these papers involve the
construction of several intermediate orders, making only localized changes at
each step (in the fashion of [8], in which it is proved that $<\\!\textup{-inv
}$FO retains the locality of FO), we equip in one go each of our structures
with a linear order.

Although not directly related to our inquiries, [16] is also concerned with
the expressive power of $\textsc{FO}^{2}$ on ordered structures. This paper
establishes a strict hierarchy, based on the quantifier rank and quantifier
alternation, among properties definable in $\textsc{FO}^{2}$ on words.

##  2 Preliminaries

###  2.1 General definitions

We use the standard definition of first-order logic $\textsc{FO}(\Sigma)$ with
equality (written FO when $\Sigma$ is clear from the context) on a finite
signature $\Sigma$ composed of relation and constant symbols. By
$\textsc{FO}^{2}$ we denote the fragment of FO in which the only two variables
are $x$ and $y$.

Structures are denoted by a name that starts with (or consists of) a
calligraphic upper-case letter, while their universes are denoted by the same
name starting with a standard upper-case letter instead of the calligraphic
one; for instance, $E\\!x$ is the universe of the structure $\mathcal{E}\\!x$.
Throughout this paper, we consider only finite structures.

A sentence $\varphi\in\textsc{FO}^{2}(\Sigma\cup\\{<\\})$, where $<$ is a
binary relation symbol not belonging to $\Sigma$, is said to be order-
invariant if for every finite $\Sigma$-structure $\mathcal{A}$, and every pair
of strict linear orders $<_{0}$ and $<_{1}$ on $A$,
$(\mathcal{A},<_{0})\models\varphi$ iff $(\mathcal{A},<_{1})\models\varphi$.
It is then convenient to omit the interpretation for the symbol $<$, and to
write $\mathcal{A}\models\varphi$ iff $(\mathcal{A},<_{0})\models\varphi$ for
any (or, equivalently, every) linear order $<_{0}$.

The set of order-invariant sentences using two variables is denoted
$<\\!\textup{-inv }\textsc{FO}^{2}$.

Let $\mathcal{L},\mathcal{L}^{\prime}$ be two logics defined over the same
signature, and $\mathcal{C}$ be a class of finite structures on this
signature.

We say that a property $\mathcal{P}\subseteq\mathcal{C}$ is definable (or
expressible) in $\mathcal{L}$ if there exists an $\mathcal{L}$-sentence
$\varphi$ such that $\mathcal{P}=\\{\mathcal{A}\in\mathcal{C}:\
\mathcal{A}\models\varphi\\}$.

We say that $\mathcal{L}\subseteq\mathcal{L}^{\prime}$ on $\mathcal{C}$ if
every property on $\mathcal{C}$ definable in $\mathcal{L}$ is also definable
in $\mathcal{L}^{\prime}$.

It is quite clear that $\textsc{FO}^{2}\subseteq\ <\\!\textup{-inv
}\textsc{FO}^{2}$: any sentence which does not make use of the order is indeed
order-invariant. Furthermore, this inclusion is strict. For instance, over the
empty signature, the property of having at least three elements is not
definable in $\textsc{FO}^{2}$ (this can easily be seen with the tools
presented in Section 4.1), but can be expressed in $<\\!\textup{-inv
}$$\textsc{FO}^{2}$, for instance via the formula $\exists x\ \exists y\ (x<y\
\land\ (\exists x\ y<x))\,.$

The quantifier rank of a formula is the maximal number of quantifiers in a
branch of its syntactic tree. Given two $\Sigma$-structures $\mathcal{A}_{0}$
and $\mathcal{A}_{1}$, and $\mathcal{L}$ being one of
$\textsc{FO},\textsc{FO}^{2}$ and $<\\!\textup{-inv }\textsc{FO}^{2}$, we
write $\mathcal{A}_{0}\equiv^{\mathcal{L}}_{k}\mathcal{A}_{1}$ if
$\mathcal{A}_{0}$ and $\mathcal{A}_{1}$ satisfy the same
$\mathcal{L}$-sentences of quantifier rank at most $k$. In this case, we say
that $\mathcal{A}_{0}$ and $\mathcal{A}_{1}$ are $\mathcal{L}$-similar at
depth $k$.

We write $\mathcal{A}_{0}\simeq\mathcal{A}_{1}$ if $\mathcal{A}_{0}$ and
$\mathcal{A}_{1}$ are isomorphic.

#### Atomic types

Let $a$ be an element of a structure $\mathcal{A}$. The atomic type
$\text{tp}_{\mathcal{A}}^{0}(a)$ of $a$ in $\mathcal{A}$ is the set of atomic
formulas $\varphi$ with at most one free variable $x$ such that
$\mathcal{A},x\mapsto a\models\varphi$.

We define similarly the atomic type $\text{tp}_{\mathcal{A}}^{0}(a,b)$ of a
pair $(a,b)$ of elements of $\mathcal{A}$ as the set of atomic formulas
$\varphi$ with free variables in $\\{x,y\\}$ such that $\mathcal{A},x\mapsto
a,y\mapsto b\models\varphi$.

Given a linearly ordered $\Sigma$-structure $(\mathcal{A},<)$,
$\text{tp}_{(\mathcal{A},<)}^{0}(a,b)$ can be split into
$\text{tp}_{<}^{0}(a,b)$ and $\text{tp}_{\mathcal{A}}^{0}(a,b)$, where
$\text{tp}_{<}^{0}(a,b)$ is one of $\\{x<y\\},\\{x>y\\}$ and $\\{x=y\\}$.

#### Gaifman graphs

The Gaifman graph $\mathcal{G}_{\mathcal{A}}$ of a structure $\mathcal{A}$ is
defined as $(A,E)$ where $(a,b)\in E$ iff $a$ and $b$ appear in the same tuple
of a relation of $\mathcal{A}$. Notice that if a graph is seen as a structure
on the signature consisting of a single binary relation symbol, its Gaifman
graph is none other than the unoriented version of itself.

By $\text{dist}_{\mathcal{A}}(a,b)$, we denote the distance between $a$ and
$b$ in $\mathcal{G}_{\mathcal{A}}$.

For $B\subseteq A$, we note $N_{\mathcal{A}}(B)$ the set of elements at
distance exactly $1$ from $B$ in $\mathcal{G}_{\mathcal{A}}$. In particular,
$B\cap N_{\mathcal{A}}(B)=\emptyset$.

The degree of $\mathcal{A}$ is the maximal degree of its Gaifman graph, and a
class $\mathcal{C}$ of $\Sigma$-structures is said to have bounded degree if
there exists some $d\in\mathbb{N}$ such that the degree of every
$\mathcal{A}\in\mathcal{C}$ is at most $d$.

###  2.2 Main result

We are now able to state the main result of this article. Remember that
$<\\!\textup{-inv }$$\textsc{FO}^{2}$ allows us to express properties that are
beyond the scope of plain $\textsc{FO}^{2}$. We give an upper bound to its
expressive power, when the degree is bounded:

######  Theorem 2.1.

Let $\mathcal{C}$ be a class of structures of bounded degree.
Then $<\\!\textup{-inv }\textsc{FO}^{2}\subseteq\textsc{FO}$ on $\mathcal{C}$.

For the remainder of this paper, we fix a signature $\Sigma$, an integer $d$
and a class $\mathcal{C}$ of $\Sigma$-structures of degree at most $d$.

Let us now show the skeleton of our proof. The technical part of the proof
will be the focus of Sections 3 and 4.

Our general strategy is to show the existence of a function
$f:\mathbb{N}\to\mathbb{N}$ such that every formula $\varphi\in\
<\\!\textup{-inv }\textsc{FO}^{2}$ of quantifier rank $k$ is equivalent on
$\mathcal{C}$ (i.e. satisfied by the same structures of $\mathcal{C}$) to an
FO-formula $\psi$ of quantifier rank at most $f(k)$.

To prove this, it is enough to show that for any two structures
$\mathcal{A}_{0},\mathcal{A}_{1}\in\mathcal{C}$ such that
$\mathcal{A}_{0}\equiv^{\textsc{FO}}_{f(k)}\mathcal{A}_{1}$, we have
$\mathcal{A}_{0}\equiv^{<\\!\textup{-inv
}\textsc{FO}^{2}}_{k}\mathcal{A}_{1}$. Indeed, the class of structures
satisfying a formula $\varphi\in\ <\\!\textup{-inv }\textsc{FO}^{2}$ of
quantifier rank $k$ is a union of equivalence classes for the equivalence
relation $\equiv^{<\\!\textup{-inv }\textsc{FO}^{2}}_{k}$, whose intersection
with $\mathcal{C}$ is in turn the intersection of $\mathcal{C}$ with a union
of equivalence classes for $\equiv^{\textsc{FO}}_{f(k)}$. It is folklore (see,
e.g., [11]) that this relation has finite index, and that each of its
equivalence classes is definable by an FO-sentence of quantifier rank $f(k)$.
Then $\psi$ is just the finite disjunction of these FO-sentences.

In order to show that $\mathcal{A}_{0}\equiv^{<\\!\textup{-inv
}\textsc{FO}^{2}}_{k}\mathcal{A}_{1}$, we will construct in Section 3 two
particular orders $<_{0},<_{1}$ on these respective structures, and we will
prove in Section 4 that

$(\mathcal{A}_{0},<_{0})\equiv^{\textsc{FO}^{2}}_{k}(\mathcal{A}_{1},<_{1})\,.$
(1)

This concludes the proof, since any sentence $\theta\in\ <\\!\textup{-inv
}\textsc{FO}^{2}$ with quantifier rank at most $k$ holds in $\mathcal{A}_{0}$
iff it holds in $(\mathcal{A}_{0},<_{0})$ (by definition of order-invariance),
iff it holds in $(\mathcal{A}_{1},<_{1})$ (by (1)), iff it holds in
$\mathcal{A}_{1}$.

##  3 Constructing linear orders on $\mathcal{A}_{0}$ and $\mathcal{A}_{1}$

Recall from Section 2.2 that our goal is to find a function $f$ such that,
given two structures $\mathcal{A}_{0},\mathcal{A}_{1}$ in $\mathcal{C}$ such
that

$\mathcal{A}_{0}\equiv^{\textsc{FO}}_{f(k)}\mathcal{A}_{1}\,,$ (2)

we are able to construct two linear orders $<_{0},<_{1}$ such that
$(\mathcal{A}_{0},<_{0})\equiv^{\textsc{FO}^{2}}_{k}(\mathcal{A}_{1},<_{1})$.

In this section, we set $f$ and we detail the construction of such orders. The
proof of $<\\!\textup{-inv }$FO-similarity between $(\mathcal{A}_{0},<_{0})$
and $(\mathcal{A}_{1},<_{1})$ will be the focus of Section 4.

Let us now explain how we define $f$. For that, we need to introduce the
notion of neighborhood and neighborhood type. These notions are defined in
Section 3.1. We then explain in Section 3.2 how to divide neighborhood types
into rare ones and frequent ones. Finally, the details of the construction are
given in Section 3.3.

###  3.1 Neighborhoods

Let us now define the notion of neighborhood of an element in a structure.

Let $c$ be a new constant symbol, and let $\mathcal{A}\in\mathcal{C}$.

For $k\in\mathbb{N}$ and $a\in A$, the (pointed) $k$-neighborhood
$\mathcal{N}_{\mathcal{A}}^{k}(a)$ of $a$ in $\mathcal{A}$ is the
$(\Sigma\cup\\{c\\})$-structure whose restriction to the vocabulary $\Sigma$
is the substructure of $\mathcal{A}$ induced by the set
$N_{\mathcal{A}}^{k}(a)=\\{b\in A:\text{dist}_{\mathcal{A}}(a,b)\leq k\\}\,,$
and where $c$ is interpreted as $a$. In other words, it consists of all the
elements at distance at most $k$ from $a$ in $\mathcal{A}$, together with the
relations they share in $\mathcal{A}$; the center $a$ being marked by the
constant $c$. We sometimes refer to $N_{\mathcal{A}}^{k}(a)$ as the
$k$-neighborhood of $a$ in $\mathcal{A}$ as well, but the context will always
make clear whether we refer to the whole substructure or only its domain.

The $k$-neighborhood type $\tau=\text{neigh-tp}_{\mathcal{A}}^{k}(a)$ of $a$
in $\mathcal{A}$ is the isomorphism class of its $k$-neighborhood. We say that
$\tau$ is a $k$-neighborhood type over $\Sigma$, and that $a$ is an occurrence
of $\tau$. We denote by $|\mathcal{A}|_{\tau}$ the number of occurrences of
$\tau$ in $\mathcal{A}$, and we write
$\llbracket\mathcal{A}_{0}\rrbracket_{k}=^{t}\llbracket\mathcal{A}_{1}\rrbracket_{k}$
to mean that for every $k$-neighborhood type $\tau$,
$|\mathcal{A}_{0}|_{\tau}$ and $|\mathcal{A}_{1}|_{\tau}$ are either equal, or
both larger than $t$.

Let $\textsc{NeighType}_{k}^{d}$ denote the set of $k$-neighborhood types over
$\Sigma$ occurring in structures of degree at most $d$. Note that
$\textsc{NeighType}_{k}^{d}$ is a finite set.

The interest of this notion resides in the fact that when the degree is
bounded, FO is exactly able to count the number of occurrences of neighborhood
types up to some threshold [3]. We will only use one direction of this
characterization, namely:

######  Proposition 3.1.

For all integers $k$ and $t$, there exists some $\hat{f}(k,t)\in\mathbb{N}$
(which also depends on the bound $d$ on the degree of structures in
$\mathcal{C}$) such that for all structures
$\mathcal{A}_{0},\mathcal{A}_{1}\in\mathcal{C}$,

$\mathcal{A}_{0}\equiv^{\textsc{FO}}_{\hat{f}(k,t)}\mathcal{A}_{1}\quad\to\quad\llbracket\mathcal{A}_{0}\rrbracket_{k}=^{t}\llbracket\mathcal{A}_{1}\rrbracket_{k}\,.$

We now exhibit a function $\Theta:\mathbb{N}\to\mathbb{N}$ such that, if
$\llbracket\mathcal{A}_{0}\rrbracket_{k}=^{\Theta(k)}\llbracket\mathcal{A}_{1}\rrbracket_{k}$,
then one can construct $<_{0},<_{1}$ satisfying (1). Proposition 3.1 then
ensures that $f:k\mapsto\hat{f}(k,\Theta(k))$ fits the bill.

Let us now explain how the function $\Theta$ is chosen.

###  3.2 Frequency of a neighborhood type

Let us denote $|\textsc{NeighType}_{k}^{d}|$ as $N$.

Recall that every $\mathcal{A}\in\mathcal{C}$ has degree at most $d$. What
this means is that if we consider the $k$-neighborhood types that have enough
occurrences in $\mathcal{A}$, they must each have many occurrences that are
scattered across $\mathcal{A}$. Not only that, but we can also make sure that
such occurrences are far from all the occurrences of every other
$k$-neighborhood type (which have few occurrences in $\mathcal{A}$, by
definition). Since the degree is bounded, $N$ is bounded too, which prevents
our distinction (which will be formalized later on) between rare neighborhood
types and frequent neighborhood types from being circular.

Such a dichotomy is introduced and detailed in [6]; we simply adapt this
construction to our needs. In the remainder of this section, we describe this
construction at a high level, and leave the technical details (such as the
exact bounds) to the reader.

The proof of the following lemma (in the vein of [1]) is straightforward, and
relies on the degree boundedness hypothesis. Intuitively, Lemma 3.2 states
that when the degree is bounded, it is not possible for all the elements of
large sets to be concentrated in one corner of the structure, thus making it
possible to pick elements in each set that are scattered across the structure.

######  Lemma 3.2.

Given three integers $m$, $\delta$, $s$, there exists a threshold
$g(m,\delta,s)\in\mathbb{N}$ such that for all $\mathcal{A}\in\mathcal{C}$,
all $B\subseteq A$ of size at most $s$, and all subsets
$C_{1},\cdots,C_{n}\subseteq A$ (with $n\leq N$) of size at least
$g(m,\delta,s)$, it is possible to find elements
$c_{j}^{1},\cdots,c_{j}^{m}\in C_{j}$ for all $j\in\\{1,\cdots,n\\}$, such
that for all $j,j^{\prime}\in\\{1,\cdots,n\\}$ and
$i,i^{\prime}\in\\{1,\cdots,m\\}$,
$\text{dist}_{\mathcal{A}}(c_{j}^{i},B)>\delta$ and
$\text{dist}_{\mathcal{A}}(c_{j}^{i},c_{j^{\prime}}^{i^{\prime}})>\delta$ if
$(j,i)\neq(j^{\prime},i^{\prime})$.

Our goal is, given a structure $\mathcal{A}\in\mathcal{C}$, to partition the
$k$-neighborhood types into two classes: the frequent types, and the rare
types. The property we wish to ensure is that there exist in $\mathcal{A}$
some number $m$ (which will be made precise later on, but only depends on $k$)
of occurrences of each one of the frequent $k$-neighborhood types which are
both

  * •

at distance greater than $\delta$ (which, as for $m$, is a function of $k$ and
will be fixed in the following) from one another, and

  * •

at distance greater than $\delta$ from every occurrence of a rare
$k$-neighborhood type.

To establish this property, we would like to use Lemma 3.2, with $s$ being the
total number of occurrences of all the rare $k$-neighborhood types, and
$C_{1},\cdots,C_{n}$ being the sets of occurrences of the $n$ distinct
frequent $k$-neighborhood types.

The number $N$ of different $k$-neighborhood types of degree at most $d$ is
bounded by a function of $k$ (as well as $\Sigma$ and $d$, which are fixed).
Hence, we can proceed according to the following (terminating) algorithm to
make the distinction between frequent and rare types:

  1. 1.

First, let us mark every $k$-neighborhood type as frequent.

  2. 2.

Among the types which are currently marked as frequent, let $\tau$ be one with
the smallest number of occurrences in $\mathcal{A}$.

  3. 3.

If $|\mathcal{A}|_{\tau}$ is at least $g(m,\delta,s)$ ($g$ being the function
from Lemma 3.2) where $s$ is the total number of occurrences of all the
$k$-neighborhood types which are currently marked as rare, then we are done
and the marking frequent/rare is final. Otherwise, mark $\tau$ as rare, and go
back to step 2 if there remains at least one frequent $k$-neighborhood type.

Notice that we can go at most $N$ times through step 2 \- $N$ depending only
on $k$. Furthermore, each time we add a type to the set of rare
$k$-neighborhood types, we have the guarantee that this type has few
occurrences (namely, less than $g(m,\delta,s)$, where $s$ can be bounded by a
function of $k$).

It is thus apparent that the threshold $t$ such that a $k$-neighborhood type
$\tau$ is frequent in $\mathcal{A}$ iff $|\mathcal{A}|_{\tau}\geq t$ can be
bounded by some $T$ depending only on $k$ \- importantly, $T$ is the same for
all structures of $\mathcal{C}$.

Let us now make the above more formal. For $t\in\mathbb{N}$ and
$\mathcal{A}\in\mathcal{C}$, let $\textsc{Freq}[\mathcal{A}]_{k}^{\geq
t}\subseteq\textsc{NeighType}_{k}^{d}$ denote the set of $k$-neighborhood
types which have at least $t$ occurrences in $\mathcal{A}$.

By applying the procedure presented above, we derive the following lemma:

######  Lemma 3.3.

Let $k,m,\delta\in\mathbb{N}$. There exists $T\in\mathbb{N}$ such that for
every $\mathcal{A}\in\mathcal{C}$, there exists some $t\leq T$ such that

$t\geq g(m,\delta,\sum_{\tau\notin\textsc{Freq}[\mathcal{A}]_{k}^{\geq
t}}|\mathcal{A}|_{\tau})\,.$

Let $\textsc{Freq}[\mathcal{A}]_{k}:=\textsc{Freq}[\mathcal{A}]_{k}^{\geq t}$
for the smallest threshold $t$ given in Lemma 3.3.

Some $k$-neighborhood type $\tau\in\textsc{NeighType}_{k}^{d}$ is said to be
frequent in $\mathcal{A}\in\mathcal{C}$ if it belongs to
$\textsc{Freq}[\mathcal{A}]_{k}$; that is, if $|\mathcal{A}|_{\tau}\geq t$.
Otherwise, $\tau$ is said to be rare. With the definition of $g$ in mind,
Lemma 3.3 can then be reformulated as follows: in every structure
$\mathcal{A}\in\mathcal{C}$, one can find $m$ occurrences of each frequent
$k$-neighborhood type which are at distance greater than $\delta$ from one
another and from the set of occurrences of every rare $k$-neighborhood type.

All that remains is for us to give a value (depending only on $k$) to the
integers $m$ and $\delta$: let
$M:=\max\\{|\tau|:\tau\in\textsc{NeighType}_{k}^{d}\\}$ ($M$ indeed exists,
and is a function of $k$ \- recall that the signature $\Sigma$ and the degree
$d$ are assumed to be fixed). Let us consider

$m:=2\cdot(k+1)\cdot M!\qquad\text{and}\qquad\delta:=4k\,.$ (3)

We then define $\Theta(k)$ as the integer $T$ provided by Lemma 3.3 for these
values of $m$ and $\delta$. The threshold $\Theta(k)$ indeed only depends on
$k$.

Finally, notice that if
$\llbracket\mathcal{A}_{0}\rrbracket_{k}=^{\Theta(k)}\llbracket\mathcal{A}_{1}\rrbracket_{k}\,,$
then
$\textsc{Freq}[\mathcal{A}_{0}]_{k}=\textsc{Freq}[\mathcal{A}_{1}]_{k}\,.$

As discussed in Section 3.1, there exists a function $f$ such that
$\mathcal{A}_{0}\equiv^{\textsc{FO}}_{f(k)}\mathcal{A}_{1}$ entails
$\llbracket\mathcal{A}_{0}\rrbracket_{k}=^{\Theta(k)}\llbracket\mathcal{A}_{1}\rrbracket_{k}$.
We also make sure that $f(k)\geq\Theta(k)\cdot N+1$ for every $k$.

Let us now consider $\mathcal{A}_{0},\mathcal{A}_{1}\in\mathcal{C}$ such that
$\mathcal{A}_{0}\equiv^{\textsc{FO}}_{f(k)}\mathcal{A}_{1}$ for such an $f$.

If $\textsc{Freq}[\mathcal{A}_{0}]_{k}=\emptyset$, then
$|\mathcal{A}_{0}|\leq\Theta(k)\cdot N$. This guarantees that
$\mathcal{A}_{0}\simeq\mathcal{A}_{1}$, and in particular that
$\mathcal{A}_{0}\equiv^{<\\!\textup{-inv
}\textsc{FO}^{2}}_{k}\mathcal{A}_{1}$. From now on, we suppose that there is
at least one frequent $k$-neighborhood type.

The construction of two linear orders $<_{0}$ and $<_{1}$ satisfying
$(\mathcal{A}_{0},<_{0})\equiv^{\textsc{FO}^{2}}_{k}(\mathcal{A}_{1},<_{1})$
is the object of Section 3.3.

###  3.3 Construction of $<_{0}$ and $<_{1}$

This section is dedicated to the definition of two linear orders $<_{0},<_{1}$
on $\mathcal{A}_{0},\mathcal{A}_{1}\in\mathcal{C}$. We then prove in Section 4
that $(\mathcal{A}_{0},<_{0})$ and $(\mathcal{A}_{1},<_{1})$ are
$\textsc{FO}^{2}$-similar at depth $k$.

Recall that by hypothesis, $\mathcal{A}_{0}$ and $\mathcal{A}_{1}$ are FO-
similar at depth $f(k)$, which entails that they have the same number of
occurrences of each $\tau\in\textsc{NeighType}_{k}^{d}$ up to a threshold
$\Theta(k)$.

To construct our two linear orders, we need to define the notion of
$k$-environment.

Given $\mathcal{A}\in\mathcal{C}$, a linear order $<$ on $A$, $k\in\mathbb{N}$
and an element $a\in A$, we define the $k$-environment
$\mathcal{E}\text{nv}_{(\mathcal{A},<)}^{k}(a)$ of $a$ in $(\mathcal{A},<)$ as
the restriction of $(\mathcal{A},<)$ to the $k$-neighborhood of $a$ in
$\mathcal{A}$, where $a$ is the interpretation of the constant symbol $c$.
Note that the order is not taken into account when determining the domain of
the substructure (it would otherwise be $A$, given that any two distinct
elements are adjacent for $<$).

The $k$-environment type $\text{env-tp}_{(\mathcal{A},<)}^{k}(a)$ is the
isomorphism class of $\mathcal{E}\text{nv}_{(\mathcal{A},<)}^{k}(a)$.

In other words, $\text{env-tp}_{(\mathcal{A},<)}^{k}(a)$ contains the
information of $\mathcal{N}_{\mathcal{A}}^{k}(a)$ together with the order of
its elements in $(\mathcal{A},<)$.

Given $\tau\in\textsc{NeighType}_{k}^{d}$, we define $\textsc{Env}(\tau)$ as
the set of $k$-environment types whose underlying $k$-neighborhood type is
$\tau$.

For $i\in\\{0,1\\}$, we aim to partition $A_{i}$ into $2(2k+1)+2$ segments:

$A_{i}=X_{i}\cup\bigcup_{j=0}^{2k}(L_{i}^{j}\cup R_{i}^{j})\cup M_{i}\,.$

Once we have set a linear order on each segment, the linear order $<_{i}$ on
$A_{i}$ will result from the concatenation of the orders on the segments as
follows:

$(A_{i},<_{i}):=X_{i}\cdot L_{i}^{0}\cdot L_{i}^{1}\cdots L_{i}^{2k}\cdot
M_{i}\cdot R_{i}^{2k}\cdots R_{i}^{1}\cdot R_{i}^{0}\,.$

Each segment $L_{i}^{j}$, for $j\in\\{0,\cdots,2k\\}$ is itself decomposed
into two segments $N\\!L_{i}^{j}\cdot U\\!L_{i}^{j}$. The $U\\!L_{i}^{j}$ for
$j\in\\{k+1,\cdots,2k\\}$ will be empty; they are defined solely in order to
keep the notations uniform. The ’N’ stands for “neighbor” and the ’U’ for
“universal”, for reasons that will soon become apparent.

Symmetrically, each $R_{i}^{j}$ is decomposed into $U\\!R_{i}^{j}\cdot
N\\!R_{i}^{j}$, with empty $U\\!R_{i}^{j}$ as soon as $j\geq k+1$.

For $i\in\\{0,1\\}$ and $r\in\\{0,\cdots,2k\\}$, we define $S_{i}^{r}$ as

$S_{i}^{r}:=X_{i}\cup\bigcup_{j=0}^{r}(L_{i}^{j}\cup R_{i}^{j})\,.$

Let us now explain how the segments are constructed in $\mathcal{A}_{0}$; see
Figure 1 for an illustration.

$\cdots$$\cdots$$\cdots$$X_{0}$$N\\!L_{0}^{0}$$U\\!L_{0}^{0}$$N\\!L_{0}^{1}$$U\\!L_{0}^{1}$$N\\!L_{0}^{k}$$U\\!L_{0}^{k}$$N\\!L_{0}^{k+1}$$N\\!L_{0}^{2k}$$M_{0}$$N\\!R_{0}^{2k}$$U\\!R_{0}^{1}$$N\\!R_{0}^{1}$$U\\!R_{0}^{0}$$L_{0}^{0}$$L_{0}^{1}$$L_{0}^{k}$$L_{0}^{k+1}$$L_{0}^{2k}$$R_{0}^{2k}$$R_{0}^{1}$$R_{0}^{0}$
Figure 1: The black curvy edges represent the edges between elements belonging
to different segments. Edges between elements of the same segment are not
represented here. The order $<_{0}$ grows from the left to the right.

For every $\tau\in\textsc{Freq}[\mathcal{A}_{0}]_{k}$, let
$\tau_{1},\cdots,\tau_{|\textsc{Env}(\tau)|}$ be an enumeration of
$\textsc{Env}(\tau)$.

Recall that we defined $M$ in Section 3.2 as
$\max\\{|\tau|:\tau\in\textsc{NeighType}_{k}^{d}\\}$. Thus, we have
$|\textsc{Env}(\tau)|\leq M!$ for every $\tau\in\textsc{NeighType}_{k}^{d}$.

In particular, by definition of frequency, and by choice of $m$ and $\delta$
in (3), Lemma 3.3 ensures that we are able to pick, for every
$\tau\in\textsc{Freq}[\mathcal{A}_{0}]_{k}$, every
$l\in\\{1,\cdots,|\textsc{Env}(\tau)|\\}$ and every $j\in\\{0,\cdots,k\\}$,
two elements $a[\tau_{l}]_{L}^{j}$ and $a[\tau_{l}]_{R}^{j}$ which have $\tau$
as $k$-neighborhood type in $\mathcal{A}_{0}$, such that all the
$a[\tau_{l}]_{*}^{j}$ are at distance at least $4k+1$ from each other and from
any occurrence of a rare $k$-neighborhood type in $\mathcal{A}_{0}$.

#### Construction of $X_{0}$ and $N\\!L_{0}^{0}$

We start with the set $X_{0}$, which contains all the occurrences of rare
$k$-neighborhood types, together with their $k$-neighborhoods.

Formally, the domain of $X_{0}$ is $\bigcup_{a\in A_{0}:\ \text{neigh-
tp}_{\mathcal{A}_{0}}^{k}(a)\notin\textsc{Freq}[\mathcal{A}_{0}]_{k}}N_{\mathcal{A}_{0}}^{k}(a)\,.$
We set $N\\!L_{0}^{0}:=N_{\mathcal{A}_{0}}(X_{0})$ (the set of neighbors of
elements of $X_{0}$), and define the order $<_{0}$ on $X_{0}$ and on
$N\\!L_{0}^{0}$ in an arbitrary way.

#### Construction of $U\\!L_{0}^{j}$

If $k<j\leq 2k$, then we set $U\\!L_{0}^{j}:=\emptyset$.

Otherwise, for $j\in\\{0,\cdots,k\\}$, once we have constructed
$L_{0}^{0},\cdots,L_{0}^{j-1}$ and $N\\!L_{0}^{j}$, we construct
$U\\!L_{0}^{j}$ as follows.

The elements of $U\\!L_{0}^{j}$ are
$\bigcup_{\tau\in\textsc{Freq}[\mathcal{A}_{0}]_{k}}\bigcup_{l=1}^{|\textsc{Env}(\tau)|}N_{\mathcal{A}_{0}}^{k}(a[\tau_{l}]_{L}^{j})\,.$

Note that $U\\!L_{0}^{j}$ does not intersect the previously constructed
segments, by choice of the $a[\tau_{l}]_{L}^{j}$ and of $\delta=4k$ in (3).
Furthermore, the $N_{\mathcal{A}_{0}}^{k}(a[\tau_{l}]_{L}^{j})$ are pairwise
disjoint, hence we can fix $<_{0}$ freely and independently on each of them.

Unsurprisingly, we order each $N_{\mathcal{A}_{0}}^{k}(a[\tau_{l}]_{L}^{j})$
so that $\text{env-
tp}_{(\mathcal{A}_{0},<_{0})}^{k}(a[\tau_{l}]_{L}^{j})=\tau_{l}$. This is
possible because for every $\tau\in\textsc{Freq}[\mathcal{A}_{0}]_{k}$ and
each $l$, $\text{neigh-tp}_{\mathcal{A}_{0}}^{k}(a[\tau_{l}]_{L}^{j})=\tau$ by
choice of $a[\tau_{l}]_{L}^{j}$.

Once each $N_{\mathcal{A}_{0}}^{k}(a[\tau_{l}]_{L}^{j})$ is ordered according
to $\tau_{l}$, the linear order $<_{0}$ on $U\\!L_{0}^{j}$ can be completed in
an arbitrary way.

Note that every possible $k$-environment type extending a frequent
$k$-neighborhood type in $\mathcal{A}_{0}$ occurs in each $U\\!L_{0}^{j}$. The
$U\\!L_{0}^{j}$ are _universal_ in that sense.

#### Construction of $N\\!L_{0}^{j}$

Now, let us see how the $N\\!L_{0}^{j}$ are constructed. For
$j\in\\{1,\cdots,2k\\}$, suppose that we have constructed
$L_{0}^{0},\cdots,L_{0}^{j-1}$.

The domain of $N\\!L_{0}^{j}$ consists of all the neighbors (in
$\mathcal{A}_{0}$) of the elements of $L_{0}^{j-1}$ not already belonging to
the construction so far. Formally,
$N_{\mathcal{A}_{0}}(L_{0}^{j-1})\setminus\big{(}X_{0}\cup\bigcup_{m=0}^{j-2}L_{0}^{m}\big{)}.$

The order $<_{0}$ on $N\\!L_{0}^{j}$ is chosen arbitrarily.

#### Construction of $R_{0}^{j}$

We construct similarly the $R_{0}^{j}$, for $j\in\\{0,\cdots,2k\\}$, starting
with $N\\!R_{0}^{0}:=\emptyset$, then $U\\!R_{0}^{0}$ which contains each
$a[\tau_{l}]_{R}^{0}$ together with its $k$-neighborhood in $\mathcal{A}_{0}$
ordered according to $\tau_{l}$, then
$N\\!R_{0}^{1}:=N_{\mathcal{A}_{0}}(R_{0}^{0})$, then $U\\!R_{0}^{1}$, etc.

Note that the $a[\tau_{l}]_{R}^{j}$ have been chosen so that they are far
enough in $\mathcal{A}_{0}$ from all the segments that have been constructed
so far, allowing us once more to order their $k$-neighborhood in
$\mathcal{A}_{0}$ as we see fit.

#### Construction of $M_{0}$

$M_{0}$ contains all the elements of $A_{0}$ besides those already belonging
to $S_{0}^{2k}$. The order $<_{0}$ chosen on $M_{0}$ is arbitrary.

#### Transfer on $\mathcal{A}_{1}$

Suppose that we have constructed $S_{0}^{2k}$.

We can make sure, retrospectively, that the index $f(k)$ in (2) is large
enough so that there exists a set $S\subseteq A_{1}$ so that
$\mathcal{A}_{0}|_{S_{0}^{2k}\cup
N_{\mathcal{A}_{0}}(S_{0}^{2k})}\simeq\mathcal{A}_{1}|_{S}$ (this is ensured
as long as $f(k)\geq|S_{0}^{2k}\cup N_{\mathcal{A}_{0}}(S_{0}^{2k})|+1$, which
can be bounded by a function of $k$, independent of $\mathcal{A}_{0}$ and
$\mathcal{A}_{1}$).

Let
$\varphi_{0}:\mathcal{A}_{0}|_{S_{0}^{2k}}\to\mathcal{A}_{1}|_{S^{\prime}}$ be
the restriction to $S_{0}^{2k}$ of said isomorphism, and let $\varphi_{1}$ be
its converse. By construction, the $k$-neighborhood of every $a\in S_{0}^{k}$
is included in $S_{0}^{2k}$; hence every such $a$ has the same
$k$-neighborhood type in $\mathcal{A}_{0}$ as has $\varphi_{0}(a)$ in
$\mathcal{A}_{1}$.

We transfer alongside $\varphi_{0}$ all the segments, with their order, from
$(\mathcal{A}_{0},<_{0})$ to $\mathcal{A}_{1}$, thus defining
$X_{1},N\\!L_{1}^{j},U\\!L_{1}^{j},\cdots$ as the respective images by
$\varphi_{0}$ of $X_{0},N\\!L_{0}^{j},U\\!L_{0}^{j},\cdots$, and define
$M_{1}$ as the counterpart to $M_{0}$. Note that the properties concerning
neighborhood are transferred; e.g. all the neighbors of an element in
$L_{1}^{j}$, $1\leq j<2k$, belong to $L_{1}^{j-1}\cup L_{1}^{j}\cup
L_{1}^{j+1}\,.$

By construction, we get the following lemma:

######  Lemma 3.4.

For each $a\in S_{0}^{k},$ we have $\text{env-
tp}_{(\mathcal{A}_{0},<_{0})}^{k}(a)=\text{env-
tp}_{(\mathcal{A}_{1},<_{1})}^{k}(\varphi_{0}(a))\,.$

Lemma 3.4 has two immediate consequences:

  * •

The set $X_{1}$ contains the occurrences in $\mathcal{A}_{1}$ of all the rare
$k$-neighborhood types (just forget about the order on the $k$-environments,
and remember that $\mathcal{A}_{0}$ and $\mathcal{A}_{1}$ have the same number
of occurrences of each rare $k$-neighborhood type).

  * •

All the universal segments $U\\!L_{1}^{j}$ and $U\\!R_{1}^{j}$, for $0\leq
j\leq k$, contain at least one occurrence of each environment in
$\textsc{Env}(\tau)$, for each $\tau\in\textsc{Freq}[\mathcal{A}_{0}]_{k}$.

Our construction also guarantees the following result:

######  Lemma 3.5.

For each $a,b\in S_{0}^{k},$ we have
$\text{tp}_{(\mathcal{A}_{0},<_{0})}^{0}(a,b)=\text{tp}_{(\mathcal{A}_{1},<_{1})}^{0}(\varphi_{0}(a),\varphi_{0}(b))\,.$

In particular, for $a=b\in S_{0}^{k}$, we have
$\text{tp}_{(\mathcal{A}_{0},<_{0})}^{0}(a)=\text{tp}_{(\mathcal{A}_{1},<_{1})}^{0}(\varphi_{0}(a))\,.$

##  4 Proof of the $\textsc{FO}^{2}$-similarity of $(\mathcal{A}_{0},<_{0})$
and $(\mathcal{A}_{1},<_{1})$

In this section, we aim to show the following result:

######  Proposition 4.1.

We have that
$(\mathcal{A}_{0},<_{0})\equiv^{\textsc{FO}^{2}}_{k}(\mathcal{A}_{1},<_{1})\,.$

###  4.1 The two-pebble Ehrenfeucht-Fraïssé game

To establish Proposition 4.1, we use Ehrenfeucht-Fraïssé games with two
pebbles. These games have been introduced by Immerman and Kozen [9]. Let us
adapt their definition to our context.

The $k$-round two-pebble Ehrenfeucht-Fraïssé game on $(\mathcal{A}_{0},<_{0})$
and $(\mathcal{A}_{1},<_{1})$ is played by two players: the spoiler and the
duplicator. The spoiler tries to expose differences between the two
structures, while the duplicator tries to establish their
indistinguishability.

There are two pebbles associated with each structure: $p_{0}^{x}$ and
$p_{0}^{y}$ on $(\mathcal{A}_{0},<_{0})$, and $p_{1}^{x}$ and $p_{1}^{y}$ on
$(\mathcal{A}_{1},<_{1})$. Formally, these pebbles can be seen as the
interpretations in each structure of two new constant symbols, but it will be
convenient to see them as moving pieces.

At the start of the game, the duplicator places $p_{0}^{x}$ and $p_{0}^{y}$ on
elements of $(\mathcal{A}_{0},<_{0})$, and $p_{1}^{x}$ and $p_{1}^{y}$ on
elements of $(\mathcal{A}_{1},<_{1})$. The spoiler wins if the duplicator is
unable to ensure that
$\text{tp}_{(\mathcal{A}_{0},<_{0})}^{0}(p_{0}^{x},p_{0}^{y})=\text{tp}_{(\mathcal{A}_{1},<_{1})}^{0}(p_{1}^{x},p_{1}^{y})$.
Otherwise, the proper game starts. Note that in the usual definition of the
starting position, the pebbles are not on the board; however, it will be
convenient to have them placed in order to uniformize our invariant. This
change is not profound and does not affect the properties of the game.

For each of the $k$ rounds, the spoiler starts by choosing a structure and a
pebble in this structure, and places this pebble on a element of the chosen
structure. In turn, the duplicator must place the corresponding pebble in the
other structure on an element of that structure. The spoiler wins at once if
$\text{tp}_{(\mathcal{A}_{0},<_{0})}^{0}(p_{0}^{x},p_{0}^{y})\neq\text{tp}_{(\mathcal{A}_{1},<_{1})}^{0}(p_{1}^{x},p_{1}^{y})$.
Otherwise, another round is played.

If the spoiler hasn’t won after $k$ rounds, then the duplicator wins.

The main interest of these games is that they capture the expressive power of
$\textsc{FO}^{2}$. We will only need the fact that these games are correct:

######  Theorem 4.2.

If the duplicator has a winning strategy in the $k$-round two-pebble
Ehrenfeucht-Fraïssé game on $(\mathcal{A}_{0},<_{0})$ and
$(\mathcal{A}_{1},<_{1})$, then
$(\mathcal{A}_{0},<_{0})\equiv^{\textsc{FO}^{2}}_{k}(\mathcal{A}_{1},<_{1})\,.$

Thus, in order to prove Proposition 4.1, we show that the duplicator wins the
$r$-round two-pebble Ehrenfeucht-Fraïssé game on $(\mathcal{A}_{0},<_{0})$ and
$(\mathcal{A}_{1},<_{1})\,.$

For that, let us show by a decreasing induction on $r=k,\cdots,0$ that the
duplicator can ensure, after $k-r$ rounds, that the three following properties
(described below) hold:

$\displaystyle\forall i\in\\{0,1\\},\forall\alpha\in\\{x,y\\},\
p_{i}^{\alpha}\in S_{i}^{r}\ \to\
p_{1-i}^{\alpha}=\varphi_{i}(p_{i}^{\alpha})$ ($S_{r}$)
$\displaystyle\forall\alpha\in\\{x,y\\},\ \text{env-
tp}_{(\mathcal{A}_{0},<_{0})}^{r}(p_{0}^{\alpha})=\text{env-
tp}_{(\mathcal{A}_{1},<_{1})}^{r}(p_{1}^{\alpha})$ ($E_{r}$)
$\displaystyle\text{tp}_{(\mathcal{A}_{0},<_{0})}^{0}(p_{0}^{x},p_{0}^{y})=\text{tp}_{(\mathcal{A}_{1},<_{1})}^{0}(p_{1}^{x},p_{1}^{y})$
($T_{r}$)

The first property, $(S_{r})$, guarantees that if a pebble is close (in a
sense that depends on the number of rounds left in the game) to one of the
$<_{i}$-minimal or $<_{i}$-maximal elements, the corresponding pebble in the
other structure is located at the same position with respect to this
$<_{i}$-extremal element.

As for $(E_{r})$, it states that two corresponding pebbles are always placed
on elements sharing the same $r$-environment type. Once again, the satefy
distance decreases with each round that goes.

Finally, $(T_{r})$ controls that both pebbles have the same relative position
(both with respect to the order and the original vocabulary) in the two
ordered structures.

In particular, the duplicator wins the game if $(T_{r})$ is satisfied at the
begining of the game, and after each of the $k$ rounds of the game.

###  4.2 Base case: proofs of $(S_{k})$, $(E_{k})$ and $(T_{k})$

We start by proving $(S_{k})$, $(E_{k})$ and $(T_{k})$.

At the start of the game, the duplicator places both $p_{0}^{x}$ and
$p_{0}^{y}$ on the $<_{0}$-minimal element of $(\mathcal{A}_{0},<_{0})$, and
both $p_{1}^{x}$ and $p_{1}^{y}$ on the $<_{1}$-minimal element of
$(\mathcal{A}_{1},<_{1})$. In particular,

$p_{1}^{x}=p_{1}^{y}=\varphi_{0}(p_{0}^{x})=\varphi_{0}(p_{0}^{y})\,.$

This ensures that $(S_{k})$ holds, while $(E_{k})$ and $(T_{k})$ respectively
follow from Lemma 3.4 and Lemma 3.5.

###  4.3 Strategy for the duplicator

We now describe the duplicator’s strategy to ensure that $(S_{r})$, $(E_{r})$
and $(T_{r})$ hold no matter how the spoiler plays.

Suppose that we have $(S_{r+1})$, $(E_{r+1})$ and $(T_{r+1})$ for some $0\leq
r<k$, after $k-r-1$ rounds of the game.

Without loss of generality, we may assume that, in the $(k-r)$-th round of the
Ehrenfeucht-Fraïssé game between $(\mathcal{A}_{0},<_{0})$ and
$(\mathcal{A}_{1},<_{1})$, the spoiler moves $p_{0}^{x}$ in
$(\mathcal{A}_{0},<_{0})$.

Let us first explain informally the general idea behind the duplicator’s
strategy.

  1. 1.

If the spoiler plays around the endpoints (by which we mean the elements that
are $<_{i}$-minimal and maximal), the duplicator has no choice but to play a
tit-for-tat strategy, i.e. to respond to the placement of $p_{i}^{\alpha}$
near the endpoints by moving $p_{1-i}^{\alpha}$ on
$\varphi_{i}(p_{i}^{\alpha})$.

There are two main reasons which explain these forced moves.

First, if at some point, $p_{0}^{x}$ and $p_{1}^{x}$ are placed near the
endpoints of their respective ordered structures (say, at respective distance
$d_{0},d_{1}$ along $<_{i}$ from the $<_{i}$-maximal element), but not at the
same $<_{i}$-distance from the endpoints (say $d_{0}<d_{1}$), then the spoiler
can play in the structure $(\mathcal{A}_{1},<_{1})$ by placing $p_{1}^{y}$ on
the element that is the $<_{1}$-successor of $p_{1}^{x}$. The duplicator will
have to place $p_{0}^{y}$ to the right of $p_{0}^{x}$. Then the duplicator
follows this move by placing $p_{1}^{x}$ on the $<_{1}$-successor of
$p_{1}^{y}$, and so on. After at most $d_{1}$ such moves, it won’t be possible
for the duplicator to find a suitable element to the right of the current
position of the pebbles in $(\mathcal{A}_{0},<_{0})$. Of course, the
duplicator must not only maintain
$\text{tp}_{<_{0}}^{0}(p_{0}^{x},p_{0}^{y})=\text{tp}_{<_{1}}^{0}(p_{1}^{x},p_{1}^{y})$
at all time, but also make sure that
$\text{tp}_{\mathcal{A}_{0}}^{0}(p_{0}^{x},p_{0}^{y})=\text{tp}_{\mathcal{A}_{1}}^{0}(p_{1}^{x},p_{1}^{y})$.
Hence, a small right shift by the spoiler in $(\mathcal{A}_{1},<_{1})$ may
force the duplicator to make a big right shift in $(\mathcal{A}_{0},<_{0})$,
and it might take less than $d_{1}$ rounds for the spoiler to win the game in
this situation; in other words, the borders around the endpoints in which the
duplicator must apply the tit-for-tat strategy are larger than just the number
of rounds in the game.

Second, the occurrences of rare neighborhood types are located in
$(\mathcal{A}_{i},<_{i})$ near the $<_{i}$-minimal element. If the duplicator
does not play according to $\varphi_{0}$ in this area, it will be easy enough
for the spoiler to win the game.

The reason we introduced the segments
$N\\!L_{i}^{j},U\\!L_{i}^{j},N\\!R_{i}^{j}$ and $U\\!R_{i}^{j}$ is precisely
to bound the area in which the duplicator must implement the tit-for-tat
strategy. Indeed, as soon as a pebble is placed in $M_{i}$, there is no way
for the spoiler to join the endpoints in less than $k$ moves while forcing the
duplicator’s hand.

The case where the spoiler plays near the endpoints corresponds to Case (I)
below, and is detailed in Section 4.4.

  2. 2.

Next, suppose that the spoiler places a pebble, say $p_{0}^{x}$, next (in
$\mathcal{A}_{0}$) to $p_{0}^{y}$, i.e. such that $p_{0}^{x}\in
N_{\mathcal{A}_{0}}^{1}(p_{0}^{y})$. The duplicator must place $p_{1}^{x}$ on
an element whose relative position to $p_{1}^{y}$ is the same as the relative
position of $p_{0}^{x}$ with respect to $p_{0}^{y}$. Note that once this is
done, the spoiler can change variable, and place $p_{0}^{y}$ (or $p_{1}^{y}$,
if they decide to play in $(\mathcal{A}_{1},<_{1})$) in
$N_{\mathcal{A}_{0}}^{1}(p_{0}^{x})$, thus forcing the duplicator to play near
$p_{1}^{x}$. In order to prevent the spoiler from being able, in $k$ such
moves, to expose the difference between $(\mathcal{A}_{0},<_{0})$ and
$(\mathcal{A}_{1},<_{1})$, the duplicator must make sure, with $r$ rounds
left, that $p_{0}^{x}$ and $p_{1}^{x}$ (as well as $p_{0}^{y}$ and
$p_{1}^{y}$) share the same $r$-environment in $(\mathcal{A}_{0},<_{0})$ and
$(\mathcal{A}_{1},<_{1})$. This will guarantee that the duplicator can play
along if the spoiler decides to take $r$ moves adjacent (in $\mathcal{A}_{i}$)
to one another.

The case where the spoiler places a pebble next (in the structure without
ordering) to the other pebble is our Case (II), and is treated in Section 4.5.

  3. 3.

Suppose now that the spoiler’s move does not fall under the previous
templates. Let us assume that the spoiler plays in $(\mathcal{A}_{0},<_{0})$,
and moves $p_{0}^{x}$ to the left of $p_{0}^{y}$ (i.e. such that
$(\mathcal{A}_{0},<_{0})\models p_{0}^{x}<p_{0}^{y}$).

In order to play according to the remarks from Cases 1 and 2, the duplicator
must place $p_{1}^{x}$ on an element which shares the same $r$-environment
with $p_{0}^{x}$ (where $r$ is the number of rounds left in the game), which
is not near the endpoints.

It must be the case that the $k$-neighborhood type of $p_{0}^{x}$ in
$\mathcal{A}_{0}$ is frequent, since it is not near the endpoints of
$(\mathcal{A}_{0},<_{0})$, hence not in $X_{0}$. By construction, every
universal segment $U\\!L_{1}^{j}$, for $0\leq j\leq k$, contains elements of
each $k$-environment type extending any frequent $k$-neighborhood type. In
particular, it contains an element having the same $r$-environment as
$p_{0}^{x}$. The duplicator will place $p_{1}^{x}$ on such an element in the
leftmost segment $U\\!L_{1}^{j}$ which is not considered to be near the
endpoints (this notion depends on the number $r$ of rounds left in the game).
This is detailed in Cases (III) and (V) (for the symmetrical case where
$p_{0}^{x}$ is placed to the right of $p_{0}^{y}$) below.

However, we have to consider a subcase, where $p_{1}^{y}$ is itself in the
leftmost segment $L_{1}^{j}$ which is not near the endpoints. Indeed, in this
case, placing $p_{1}^{x}$ as discussed may result in $p_{1}^{x}$ being to the
right of $p_{1}^{y}$, or being in $N_{\mathcal{A}_{1}}^{1}(p_{1}^{y})$; either
of which being game-losing to the duplicator. However, since $p_{1}^{y}$ was
considered to be near the endpoints in the previous round of the game, we know
that the duplicator played a tit-for-tat strategy at that point, which allows
us to replicate the placement of $p_{0}^{x}$ according to $\varphi_{0}$. This
subcase, as well as the equivalent subcase where the spoiler places
$p_{0}^{x}$ to the right of $p_{0}^{y}$, are formalized in Cases (IV) and (VI)
below.

We are now ready to describe formally the strategy implemented by the
duplicator:

  1. (I)

If $p_{0}^{x}\in S_{0}^{r}$, then the duplicator responds by placing
$p_{1}^{x}$ on $\varphi_{0}(p_{0}^{x})$.

This corresponds to the tit-for-tat strategy implemented when the spoiler
plays near the endpoints, as discussed in Case 1.

  2. (II)

Else, if $p_{0}^{x}\notin S_{0}^{r}$, and $p_{0}^{x}\in
N_{\mathcal{A}_{0}}^{1}(p_{0}^{y})$, then $(E_{r+1})$ ensures that there
exists an isomorphism
$\psi:\mathcal{E}\text{nv}_{(\mathcal{A}_{0},<_{0})}^{r+1}(p_{0}^{y})\to\mathcal{E}\text{nv}_{(\mathcal{A}_{1},<_{1})}^{r+1}(p_{1}^{y})\,.$
The duplicator responds by placing $p_{1}^{x}$ on $\psi(p_{0}^{x})$.

This makes formal the duplicator’s response to a move next to the other
pebble, as discussed in Case 2 above.

  3. (III)

Else suppose that $(\mathcal{A}_{0},<_{0})\models p_{0}^{x}<p_{0}^{y}$ and
$p_{0}^{y}\notin L_{0}^{r+1}$. Note that $\tau:=\text{neigh-
tp}_{\mathcal{A}_{0}}^{k}(p_{0}^{x})\in\textsc{Freq}[\mathcal{A}_{0}]_{k}$,
since $p_{0}^{x}\notin X_{0}$. Let $\tau_{l}:=\text{env-
tp}_{(\mathcal{A}_{0},<_{0})}^{k}(p_{0}^{x})$.

The duplicator responds by placing $p_{1}^{x}$ on
$\varphi_{0}(a[\tau_{l}]_{L}^{r+1})$.

  4. (IV)

Else, if $(\mathcal{A}_{0},<_{0})\models p_{0}^{x}<p_{0}^{y}$ and
$p_{0}^{y}\in L_{0}^{r+1}$, then the duplicator moves $p_{1}^{x}$ on
$\varphi_{0}(p_{0}^{x})$ (by $(S_{r+1})$, $p_{0}^{x}$ indeed belongs to the
domain of $\varphi_{0}$).

  5. (V)

Else, suppose that $(\mathcal{A}_{0},<_{0})\models p_{0}^{y}<p_{0}^{x}$ and
$p_{0}^{y}\notin R_{0}^{r+1}$. This case is symmetric to Case (III).

Similarly, the duplicator opts to play $p_{1}^{x}$ on
$\varphi_{0}(a[\tau_{l}]_{R}^{r+1})$, where $\tau_{l}:=\text{env-
tp}_{(\mathcal{A}_{0},<_{0})}^{k}(p_{0}^{x})$.

  6. (VI)

If we are in none of the cases above, it means that the spoiler has placed
$p_{0}^{x}$ to the right of $p_{0}^{y}$, and that $p_{0}^{y}\in R_{0}^{r+1}$.
This case is symmetric to Case (IV).

Once again, the duplicator places $p_{1}^{x}$ on $\varphi_{0}(p_{0}^{x})$.

Let us now prove that this strategy indeed satisfies our invariants: under the
inductive assumption that $(S_{r+1})$, $(E_{r+1})$ and $(T_{r+1})$ hold, for
some $0\leq r<k$, we show that this strategy ensures that $(S_{r})$, $(E_{r})$
and $(T_{r})$ hold.

We treat each case in its own section: Section 4.4 is devoted to Case (I)
while Section 4.5 covers Case (II). Both Cases (III) and (IV) are treated in
Section 4.6. Cases (V) and (VI), being their exact symmetric counterparts, are
left to the reader.

######  Note 4.3.

Note that some properties need no verification. Since $p_{0}^{y}$ and
$p_{1}^{y}$ are left untouched by the players, $(S_{r+1})$ ensures that half
of $(S_{r})$ automatically holds, namely that

$\forall i\in\\{0,1\\},\quad p_{i}^{y}\in S_{i}^{r}\quad\to\quad
p_{1-i}^{y}=\varphi_{i}(p_{i}^{y})\,.$

Similarly, the part of $(E_{r})$ concerning $p_{0}^{y}$ and $p_{1}^{y}$
follows from $(E_{r+1})$:

$\text{env-tp}_{(\mathcal{A}_{0},<_{0})}^{r}(p_{0}^{y})=\text{env-
tp}_{(\mathcal{A}_{1},<_{1})}^{r}(p_{1}^{y})\,.$

Lastly, notice that once we have shown that $(E_{r})$ holds, it follows that

$\left\\{\begin{array}[]{l}\text{tp}_{\mathcal{A}_{0}}^{0}(p_{0}^{x})=\text{tp}_{\mathcal{A}_{1}}^{0}(p_{1}^{x})\\\
\text{tp}_{\mathcal{A}_{0}}^{0}(p_{0}^{y})=\text{tp}_{\mathcal{A}_{1}}^{0}(p_{1}^{y})\end{array}\right.$

###  4.4 When the spoiler plays near the endpoints: Case (I)

In this section, we treat the case where the spoiler places $p_{0}^{x}$ near
the $<_{0}$-minimal or $<_{0}$-maximal element of $(\mathcal{A}_{0},<_{0})$.
Obviously, what “near” means depends on the number of rounds left in the game;
the more rounds remain, the more the duplicator must be cautious regarding the
possibility for the spoiler to reach an endpoint and potentially expose a
difference between $(\mathcal{A}_{0},<_{0})$ and $(\mathcal{A}_{1},<_{1})$.

As we have stated in Case (I), with $r$ rounds left, we consider a move on
$p_{0}^{x}$ by the spoiler to be near the endpoints if it is made in
$S_{0}^{r}$. In that case, the duplicator responds along the tit-for-tat
strategy, namely by placing $p_{1}^{x}$ on $\varphi_{0}(p_{0}^{x})$.

Let us now prove that this strategy guarantees that $(S_{r})$, $(E_{r})$ and
$(T_{r})$ hold. Recall from Note 4.3 that part of the task is already taken
care of.

#### Proof of $(S_{r})$ in Case (I)

We have to show that $\forall i\in\\{0,1\\},\ p_{i}^{x}\in S_{i}^{r}\ \to\
p_{1-i}^{x}=\varphi_{i}(p_{i}^{x})\,.$ This follows directly from the
duplicator’s strategy, since $p_{1}^{x}=\varphi_{0}(p_{0}^{x})$ (thus
$p_{0}^{x}=\varphi_{1}(p_{1}^{x})$).

#### Proof of $(E_{r})$ in Case (I)

We need to prove that $\text{env-
tp}_{(\mathcal{A}_{0},<_{0})}^{r}(p_{0}^{x})=\text{env-
tp}_{(\mathcal{A}_{1},<_{1})}^{r}(p_{1}^{x})\,,$ which is a consequence of
Lemma 3.4 given that $p_{1}^{x}=\varphi_{0}(p_{0}^{x})$ and $r<k$.

#### Proof of $(T_{r})$ in Case (I)

First, suppose that $p_{0}^{y}\in S_{0}^{r+1}$. By $(S_{r+1})$, we know that
$p_{1}^{y}=\varphi_{0}(p_{0}^{y})$. Thus, Lemma 3.5 allows us to conclude that
$\text{tp}_{(\mathcal{A}_{0},<_{0})}^{0}(p_{0}^{x},p_{0}^{y})=\text{tp}_{(\mathcal{A}_{1},<_{1})}^{0}(p_{1}^{x},p_{1}^{y})$.

Otherwise, $p_{0}^{y}\notin S_{0}^{r+1}$ and $(S_{r+1})$ entails that
$p_{1}^{y}\notin S_{1}^{r+1}$.

We have two points to establish:

$\displaystyle\text{tp}_{\mathcal{A}_{0}}^{0}(p_{0}^{x},p_{0}^{y})=\text{tp}_{\mathcal{A}_{1}}^{0}(p_{1}^{x},p_{1}^{y})$
(4)
$\displaystyle\text{tp}_{<_{0}}^{0}(p_{0}^{x},p_{0}^{y})=\text{tp}_{<_{1}}^{0}(p_{1}^{x},p_{1}^{y})$
(5)

Notice that

$\left\\{\begin{array}[]{l}\text{tp}_{\mathcal{A}_{0}}^{0}(p_{0}^{x},p_{0}^{y})=\text{tp}_{\mathcal{A}_{0}}^{0}(p_{0}^{x})\cup\text{tp}_{\mathcal{A}_{0}}^{0}(p_{0}^{y})\\\
\text{tp}_{\mathcal{A}_{1}}^{0}(p_{1}^{x},p_{1}^{y})=\text{tp}_{\mathcal{A}_{1}}^{0}(p_{1}^{x})\cup\text{tp}_{\mathcal{A}_{1}}^{0}(p_{1}^{y})\end{array}\right.$

This is because, by construction, the neighbors in $\mathcal{A}_{i}$ of an
element of $S_{i}^{r}$ all belong to $S_{i}^{r+1}$. Equation (4) follows from
this remark and Note 4.3.

As for Equation (5), either

$p_{0}^{x}\in X_{0}\cup\bigcup_{0\leq j\leq r}L_{0}^{j}\quad\text{and}\quad
p_{1}^{x}\in X_{1}\cup\bigcup_{0\leq j\leq r}L_{1}^{j}\,,$

in which case
$\text{tp}_{<_{0}}^{0}(p_{0}^{x},p_{0}^{y})=\\{x<y\\}=\text{tp}_{<_{1}}^{0}(p_{1}^{x},p_{1}^{y})\,,$
or

$p_{0}^{x}\in\bigcup_{0\leq j\leq r}R_{0}^{j}\quad\text{and}\quad
p_{1}^{x}\in\bigcup_{0\leq j\leq r}R_{1}^{j}\,,$

in which case
$\text{tp}_{<_{0}}^{0}(p_{0}^{x},p_{0}^{y})=\\{x>y\\}=\text{tp}_{<_{1}}^{0}(p_{1}^{x},p_{1}^{y})\,.$

###  4.5 When the spoiler plays next to the other pebble: Case (II)

Suppose now that the spoiler places $p_{0}^{x}$ next to the other pebble in
$\mathcal{A}_{0}$ (i.e. $p_{0}^{x}\in N_{\mathcal{A}_{0}}^{1}(p_{0}^{y})$),
but not in $S_{0}^{r}$ (for that move would fall under the jurisdiction of
Case (I)).

In that case, the duplicator must place $p_{1}^{x}$ so that the relative
position of $p_{1}^{x}$ and $p_{1}^{y}$ is the same as that of $p_{0}^{x}$ and
$p_{0}^{y}$.

For that, we can use $(E_{r+1})$, which guarantees that $\text{env-
tp}_{(\mathcal{A}_{0},<_{0})}^{r+1}(p_{0}^{y})=\text{env-
tp}_{(\mathcal{A}_{1},<_{1})}^{r+1}(p_{1}^{y})\,.$ Thus there exists an
isomorphism $\psi$ between
$\mathcal{E}\text{nv}_{(\mathcal{A}_{0},<_{0})}^{r+1}(p_{0}^{y})$ and
$\mathcal{E}\text{nv}_{(\mathcal{A}_{1},<_{1})}^{r+1}(p_{1}^{y})$. Note that
this isomorphism is unique, by virtue of $<_{0}$ and $<_{1}$ being linear
orders.

The duplicator’s response is to place $p_{1}^{x}$ on $\psi(p_{0}^{x})$. Let us
now prove that this strategy is correct with respect to our invariants
$(S_{r})$, $(E_{r})$ and $(T_{r})$.

#### Proof of $(S_{r})$ in Case (II)

Because the spoiler’s move does not fall under Case (I), we know that
$p_{0}^{x}\notin S_{0}^{r}$.

Let us now show that $p_{1}^{x}$ is not near the endpoints either: suppose
that $p_{1}^{x}\in S_{1}^{r}$. By construction, since $p_{1}^{x}$ and
$p_{1}^{y}$ are neighbors in $\mathcal{A}_{1}$, this entails that
$p_{1}^{y}\in S_{1}^{r+1}$. But then, we know by $(S_{r+1})$ that
$p_{0}^{y}=\varphi_{1}(p_{1}^{y})$; and because $\psi$ is the unique
isomorphism between
$\mathcal{E}\text{nv}_{(\mathcal{A}_{0},<_{0})}^{r+1}(p_{0}^{y})$ and
$\mathcal{E}\text{nv}_{(\mathcal{A}_{1},<_{1})}^{r+1}(p_{1}^{y})$, $\psi$ is
equal to the restriction $\widetilde{}\varphi_{0}$ of $\varphi_{0}$:

$\widetilde{}\varphi_{0}\ :\
\mathcal{E}\text{nv}_{(\mathcal{A}_{0},<_{0})}^{r+1}(p_{0}^{y})\ \to\
\mathcal{E}\text{nv}_{(\mathcal{A}_{1},<_{1})}^{r+1}(p_{1}^{y})\,.$

Thus
$p_{0}^{x}=\psi^{-1}(p_{1}^{x})=\widetilde{}\varphi_{0}^{-1}(p_{1}^{x})=\varphi_{1}(p_{1}^{x})$,
and by definition of the segments on $(\mathcal{A}_{1},<_{1})$, which are just
a transposition of the segments of $(\mathcal{A}_{0},<_{0})$ via
$\varphi_{0}$, $p_{1}^{x}\in S_{1}^{r}$ then entails that $p_{0}^{x}\in
S_{0}^{r}$, which is absurd.

Since we neither have $p_{0}^{x}\in S_{0}^{r}$ nor $p_{1}^{x}\in S_{1}^{r}$,
$(S_{r})$ holds - recall from Note 4.3 that the part concerning $p_{0}^{y}$
and $p_{1}^{y}$ is always satisfied.

#### Proof of $(E_{r})$ in Case (II)

Recall that the duplicator placed $p_{1}^{x}$ on the image of $p_{0}^{x}$ by
the isomorphism

$\psi:\mathcal{E}\text{nv}_{(\mathcal{A}_{0},<_{0})}^{r+1}(p_{0}^{y})\to\mathcal{E}\text{nv}_{(\mathcal{A}_{1},<_{1})}^{r+1}(p_{1}^{y})\,.$

It is easy to check that the restriction $\widetilde{\psi}$ of $\psi$:
$\widetilde{\psi}\ :\
\mathcal{E}\text{nv}_{(\mathcal{A}_{0},<_{0})}^{r}(p_{0}^{x})\ \to\
\mathcal{E}\text{nv}_{(\mathcal{A}_{1},<_{1})}^{r}(p_{1}^{x})$ is well
defined, and is indeed an isomorphism.
This ensures that $\text{env-
tp}_{(\mathcal{A}_{0},<_{0})}^{r}(p_{0}^{x})=\text{env-
tp}_{(\mathcal{A}_{1},<_{1})}^{r}(p_{1}^{x})\,,$ thus completing the proof of
$(E_{r})$.

#### Proof of $(T_{r})$ in Case (II)

This follows immediately from the fact that the isomorphism $\psi$ maps
$p_{0}^{x}$ to $p_{1}^{x}$ and $p_{0}^{y}$ to $p_{1}^{y}$: all the atomic
facts about these elements are preserved.

###  4.6 When the spoiler plays to the left: Cases (III) and (IV)

We now treat our last case, which covers both Cases (III) and (IV), i.e. the
instances where the spoiler places $p_{0}^{x}$ to the left of $p_{0}^{y}$
(formally: such that $(\mathcal{A}_{0},<_{0})\models p_{0}^{x}<p_{0}^{y}$),
which do not already fall in Cases (I) and (II).

Note that the scenario in which the spoiler plays to the right of the other
pebble is the exact symmetric of this one (since the $X_{i}$ play no role in
this case, left and right can be interchanged harmlessly).

The idea here is very simple: since the spoiler has placed $p_{0}^{x}$ to the
left of $p_{0}^{y}$, but neither in $S_{0}^{r}$ nor in
$N_{\mathcal{A}_{0}}^{1}(p_{0}^{y})$, the duplicator responds by placing
$p_{1}^{x}$ on an element of $U\\!L_{1}^{r+1}$ (the leftmost universal segment
not in $S_{1}^{r}$) sharing the same $k$-environment.

This is possible by construction of the universal segments: if
$\tau_{l}:=\text{env-tp}_{(\mathcal{A}_{0},<_{0})}^{k}(p_{0}^{x})$ (which must
extend a frequent $k$-neighborhood type, since $p_{0}^{x}\notin X_{0}$), then
$\varphi_{0}(a[\tau_{l}]_{L}^{r+1})$ satisfies the requirements.

There is one caveat to this strategy. If $p_{1}^{y}$ is itself in
$L_{1}^{r+1}$, two problems may arise: first, it is possible for $p_{1}^{x}$
and $p_{1}^{y}$ to be in the wrong order (i.e. such that
$(\mathcal{A}_{1},<_{1})\models p_{1}^{x}>p_{1}^{y}$). Second, it may be the
case that $p_{1}^{x}$ and $p_{1}^{y}$ are neighbors in $\mathcal{A}_{1}$,
which, together with the fact that $p_{0}^{x}$ and $p_{0}^{y}$ are orthogonal
in $\mathcal{A}_{0}$ (i.e.
$\text{tp}_{\mathcal{A}_{0}}^{0}(p_{0}^{x},p_{0}^{y})=\text{tp}_{\mathcal{A}_{0}}^{0}(p_{0}^{x})\cup\text{tp}_{\mathcal{A}_{0}}^{0}(p_{0}^{y})$),
would break $(T_{r})$.

This is why the duplicator’s strategy depends on whether $p_{1}^{y}\in
L_{1}^{r+1}$:

  * •

if this is not the case, then the duplicator places $p_{1}^{x}$ on
$\varphi_{0}(a[\tau_{l}]_{L}^{r+1})$. This corresponds to Case (III).

  * •

if $p_{1}^{y}\in L_{1}^{r+1}$, then $(S_{r+1})$ guarantees that $p_{0}^{y}\in
L_{0}^{r+1}$. Hence $p_{0}^{x}$, which is located to the left of $p_{0}^{y}$,
is in the domain of $\varphi_{0}$: the duplicator moves $p_{1}^{x}$ to
$\varphi_{0}(p_{0}^{x})$. This situation corresponds to Case (IV).

Let us prove that $(S_{r})$, $(E_{r})$ and $(T_{r})$ hold in both of these
instances.

#### Proof of $(S_{r})$ in Case (III)

Since the spoiler’s move does not fall under Case (I), we have that
$p_{0}^{x}\notin S_{0}^{r}$.

By construction, $a[\tau_{l}]_{L}^{r+1}\in L_{0}^{r+1}$, thus
$\varphi_{0}(a[\tau_{l}]_{L}^{r+1})\in L_{1}^{r+1}$, and $p_{1}^{x}\notin
S_{1}^{r}$.

#### Proof of $(E_{r})$ in Case (III)

It follows from $\text{env-
tp}_{(\mathcal{A}_{0},<_{0})}^{k}(a[\tau_{l}]_{L}^{r+1})=\tau_{l}$ together
with Lemma 3.4 that

$\text{env-tp}_{(\mathcal{A}_{0},<_{0})}^{k}(p_{0}^{x})=\text{env-
tp}_{(\mathcal{A}_{1},<_{1})}^{k}(p_{1}^{x})\,.$

A fortiori, $\text{env-tp}_{(\mathcal{A}_{0},<_{0})}^{r}(p_{0}^{x})=\text{env-
tp}_{(\mathcal{A}_{1},<_{1})}^{r}(p_{1}^{x})$.

#### Proof of $(T_{r})$ in Case (III)

Because the spoiler’s move does not fall under Case (II), $p_{0}^{x}\notin
N_{\mathcal{A}_{0}}^{1}(p_{0}^{y})$. In other words,

$\text{tp}_{\mathcal{A}_{0}}^{0}(p_{0}^{x},p_{0}^{y})=\text{tp}_{\mathcal{A}_{0}}^{0}(p_{0}^{x})\cup\text{tp}_{\mathcal{A}_{0}}^{0}(p_{0}^{y})\,.$

Recall the construction of $U\\!L_{0}^{r+1}$: the whole $k$-neighborhood of
$a[\tau_{l}]_{L}^{r+1}$ was included in this segment. In particular,
$N_{\mathcal{A}_{1}}^{1}(p_{1}^{x})=N_{\mathcal{A}_{1}}^{1}(\varphi_{0}(a[\tau_{l}]_{L}^{r+1}))\subseteq
U\\!L_{1}^{r+1}\,.$ By assumption, $p_{1}^{y}\notin L_{1}^{r+1}$, which
entails that
$\text{tp}_{\mathcal{A}_{1}}^{0}(p_{1}^{x},p_{1}^{y})=\text{tp}_{\mathcal{A}_{1}}^{0}(p_{1}^{x})\cup\text{tp}_{\mathcal{A}_{1}}^{0}(p_{1}^{y})\,.$
It then follows from the last observation of Note 4.3 that
$\text{tp}_{\mathcal{A}_{0}}^{0}(p_{0}^{x},p_{0}^{y})=\text{tp}_{\mathcal{A}_{1}}^{0}(p_{1}^{x},p_{1}^{y})\,.$

Let us now prove that $\text{tp}_{<_{1}}^{0}(p_{1}^{x},p_{1}^{y})=\\{x<y\\}$.
We claim that $p_{1}^{y}\notin X_{1}\cup\bigcup_{0\leq j\leq r+1}L_{1}^{j}$.
Suppose otherwise: $(S_{r+1})$ would entail that $p_{0}^{y}\in
X_{0}\cup\bigcup_{0\leq j\leq r+1}L_{0}^{j}$ which, together with the
hypothesis $p_{0}^{y}\notin L_{0}^{r+1}$ and $p_{0}^{x}<p_{0}^{y}$, would
result in $p_{0}^{x}$ being in $S_{0}^{r}$, which is absurd.
Thus,
$\text{tp}_{<_{1}}^{0}(p_{1}^{x},p_{1}^{y})=\\{x<y\\}=\text{tp}_{<_{0}}^{0}(p_{0}^{x},p_{0}^{y})$,
which concludes the proof of $(T_{r})$.

#### Proof of $(S_{r})$, $(E_{r})$ and $(T_{r})$ in Case (IV)

Let us now move to the case where $p_{1}^{y}\in L_{1}^{r+1}$. Recall that
under this assumption, $p_{0}^{y}=\varphi_{1}(p_{1}^{y})\in L_{0}^{r+1}$ and
since $p_{0}^{x}<p_{0}^{y}$ and $p_{0}^{x}\notin S_{0}^{r}$, we have that
$p_{0}^{x}\in L_{0}^{r+1}$.

The duplicator places the pebble $p_{1}^{x}$ on $\varphi_{0}(p_{0}^{x})$; in
particular, $p_{1}^{x}\in L_{1}^{r+1}$.

The proof of $(S_{r})$ follows from the simple observation that
$p_{0}^{x}\notin S_{0}^{r}$ and $p_{1}^{x}\notin S_{1}^{r}$.

As for $(E_{r})$ and $(T_{r})$, they follow readily from Lemma 3.4 and 3.5 and
the fact that $p_{1}^{x}=\varphi_{0}(p_{0}^{x})$ and
$p_{1}^{y}=\varphi_{0}(p_{0}^{y})$.

##  5 Counting quantifiers

We now consider the extension $\textsc{C}^{2}$ of $\textsc{FO}^{2}$, where one
is allowed to use counting quantifiers of the form $\exists^{\geq i}x$ and
$\exists^{\geq i}y$, for $i\in\mathbb{N}$. Such a quantifier, as expected,
expresses the existence of at least $i$ elements satisfying the formula which
follows it.

This logic $\textsc{C}^{2}$ has been extensively studied. On an expressiveness
standpoint, $\textsc{C}^{2}$ stricly extends $\textsc{FO}^{2}$ (which cannot
count up to three), and contrary to the latter, $\textsc{C}^{2}$ does not
enjoy the small model property. However, the satisfiability problem for
$\textsc{C}^{2}$ is still decidable [5, 14, 15]. To the best of our knowledge,
it is not known whether $<\\!\textup{-inv }\textsc{C}^{2}$ has a decidable
syntax.

Let us now explain how the proof of Theorem 2.1 can be adapted to show the
following stronger version:

######  Theorem 5.1.

Let $\mathcal{C}$ be a class of structures of bounded degree.

Then $<\\!\textup{-inv }\textsc{C}^{2}\subseteq\textsc{FO}$ on $\mathcal{C}$.

######  Proof 5.2.

The proof is very similar as to that of Theorem 2.1. The difference is that we
now need to show, at the end of the construction, that the structures
$(\mathcal{A}_{0},<_{0})$ and $(\mathcal{A}_{1},<_{1})$ are not only
$\textsc{FO}^{2}$-similar, but $\textsc{C}^{2}$-similar. More precisely, we
show that for every $k\in\mathbb{N}$, there exists some $f(k)\in\mathbb{N}$
such that if $\mathcal{A}_{0}\equiv^{\textsc{FO}}_{f(k)}\mathcal{A}_{1}$, then
it is possible to construct two linear orders $<_{0}$ and $<_{1}$ such that
$(\mathcal{A}_{0},<_{0})$ and $(\mathcal{A}_{1},<_{1})$ agree on all
$\textsc{C}^{2}$-sentences of quantifier rank at most $k$, and with counting
indexes at most $k$, which we denote
$(\mathcal{A}_{0},<_{0})\equiv^{\textsc{C}^{2}}_{k,k}(\mathcal{A}_{1},<_{1})\,.$

This is enough to complete the proof, as these classes of
$\textsc{C}^{2}$-sentences cover all the $\textsc{C}^{2}$-definable
properties.

In order to prove that
$(\mathcal{A}_{0},<_{0})\equiv^{\textsc{C}^{2}}_{k,k}(\mathcal{A}_{1},<_{1})$,
we need an Ehrenfeucht-Fraïssé-game capturing $\equiv^{\textsc{C}^{2}}_{k,k}$.
It is not hard to derive such a game from the Ehrenfeucht-Fraïssé-game for
$\textsc{C}^{2}$ [10].

This game only differs from the two-pebble Ehrenfeucht-Fraïssé-game in that in
each round, once the spoiler has chosen a structure (say
$(\mathcal{A}_{0},<_{0})$) and a pebble to move (say $p_{0}^{x}$), the spoiler
picks not only one element of that structure, but a set $P_{0}$ of up to $k$
elements. Then the duplicator must respond with a set $P_{1}$ of same
cardinality in $(\mathcal{A}_{1},<_{1})$. The spoiler then places $p_{1}^{x}$
on any element of $P_{1}$, to which the duplicator responds by placing
$p_{0}^{x}$ on some element of $P_{0}$. As usual, the spoiler wins after this
round if
$\text{tp}_{(\mathcal{A}_{0},<_{0})}^{0}(p_{0}^{x},p_{0}^{y})\neq\text{tp}_{(\mathcal{A}_{1},<_{1})}^{0}(p_{1}^{x},p_{1}^{y})\,.$
Otherwise, the games goes on until $k$ rounds are played.

It is not hard to establish that this game indeed captures
$\equiv^{\textsc{C}^{2}}_{k,k}$, in the sense that
$(\mathcal{A}_{0},<_{0})\equiv^{\textsc{C}^{2}}_{k,k}(\mathcal{A}_{1},<_{1})$
if and only if the duplicator has a winning strategy for $k$ rounds of this
game. The restriction on the cardinal of the set chosen by the spoiler (which
is at most $k$) indeed corresponds to the fact that the counting indexes of
the formulas are at most $k$. As for the number of rounds (namely, $k$), it
corresponds as usual to the quantifier rank. This can be easily derived from a
proof of Theorem 5.3 in [10], and is left to the reader.

Let us now explain how to modify the construction of $<_{0}$ and $<_{1}$
presented in Section 3 in order for the duplicator to maintain similarity for
$k$-round in such a game. The only difference lies in the choice of the
universal elements. Recall that in the previous construction, we chose, for
each $k$-environment type $\tau_{l}$ extending a frequent $k$-neighborhood
type and each segment $U\\!L_{0}^{j}$, an element $a[\tau_{l}]_{L}^{j}$ whose
$k$-environment type in $(\mathcal{A}_{0},<_{0})$ is destined to be $\tau_{l}$
(and similarly for $U\\!R_{0}^{j}$ and $a[\tau_{l}]_{R}^{j}$).

In the new construction, we pick $k$ such elements, instead of just one. Just
as previously, all these elements must be far enough from one another in the
Gaifman graph of $\mathcal{A}_{0}$. Once again, this condition can be met by
virtue of the $k$-neighborhood type $\tau$ underlying $\tau_{l}$ being
frequent, and thus having many occurrences scattered across $\mathcal{A}_{0}$
(remember that we have a bound on the degree of $\mathcal{A}_{0}$, thus all
the occurrences of $\tau$ cannot be concentrated). We only need to multiply
the value of $m$ by $k$ in (3).

When the spoiler picks a set of elements of size at most $k$ in one of the
structures (say $P_{0}$ in $(\mathcal{A}_{0},<_{0})$), the duplicator responds
by selecting, for each one of the elements of $P_{0}$, an element in
$(\mathcal{A}_{1},<_{1})$ along the strategy for the $\textsc{FO}^{2}$-game
explained in Section 4.3. All that remains to be shown is that it is possible
for the duplicator to answer each element of $P_{0}$ with a different element
in $(\mathcal{A}_{1},<_{1})$.

Note that if the duplicator follows the strategy from Section 4.3, they will
never answer two moves by the spoiler falling under different cases among
Cases (I)-(VI) with the same element. Thus we can treat separately each one of
these cases; and for each case, we show that if the spoiler chooses up to $k$
elements in $(\mathcal{A}_{0},<_{0})$ falling under this case in $P_{0}$, then
the duplicator can find the same number of elements in
$(\mathcal{A}_{1},<_{1})$, following the aforementionned strategy.

  * •

For Case (I), this is straightforward, since the strategy is based on the
isomorphism between the borders of the linear orders. The same goes for Cases
(II), (IV) and (VI), as the strategy in these cases also relies on an
isomorphism argument.

  * •

Suppose now that $p_{0}^{y}\notin L_{0}^{r+1}$, and assume that the spoiler
chooses several elements to the left of $p_{0}^{y}$, but outside of
$S_{0}^{r}$ and not adjacent to $p_{0}^{y}$. This corresponds to Case (III).
Recall that our new construction guarantees, for each $k$-environment type
extending a frequent $k$-neighborhood type, the existence in $L_{1}^{r+1}$ of
$k$ elements having this environment. This lets us choose, in $L_{1}^{r+1}$, a
distinct answer for each element in the set selected by the spoiler, sharing
the same $k$-environment type. Case (V) is obviously symmetric.

This concludes the proof of Theorem 5.1.

##  6 Conclusion

$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$
Figure 2: Illustration of two linear orders (growing from left to right) on a
cycle (left figure) and the disjoint union of a cycle and a triangle (right
figure), which are indistinguishable by any $\textsc{C}^{2}$-sentence of small
enough quantifier rank and maximal counting index (where “small” is understood
with respect to the length of the cycles).

We have established that, when the degree is bounded, properties definable in
the order-invariant extension of the two-variable fragment of first-order
logic with counting are definable in first-order logic.

From there, there seem to be three axes in which one can try to complete the
picture.

First, a natural question is whether this inclusion of expressiveness still
holds when we release the hypothesis on the degree. The classical examples
separating $<\\!\textup{-inv }$FO from FO seem to require at least three
variables (for example, the Potthoff separating example [13] can be expressed
with three variables, thus proving that $<\\!\textup{-inv
}\textsc{FO}^{3}\not\subseteq\textsc{FO}$). It would be very interesting to
know whether such a separating example exists for $<\\!\textup{-inv
}$$\textsc{C}^{2}$, or even for $<\\!\textup{-inv }$$\textsc{FO}^{2}$.

Second, it is quite clear that the inclusion $<\\!\textup{-inv
}\textsc{C}^{2}\subseteq\textsc{FO}$ when the degree is bounded is a severe
over-approximation of the expressive power of $<\\!\textup{-inv
}$$\textsc{C}^{2}$. For instance, it is not hard to prove that
$<\\!\textup{-inv }$$\textsc{C}^{2}$ cannot define the class of triangle-free
graphs: no sentence from $<\\!\textup{-inv }$$\textsc{C}^{2}$ can make a
distinction between a large enough cycle and the disjoint union of a large
enough cycle together with a triangle. This can be seen, following the general
strategy detailed in Section 2.2, by constructing two carefully chosen linear
orders on these graphs. Figure 2 illustrates the construction of such orders.
Notice that there are only three kinds of elements: those whose two neighbors
are on their left, those for which they are on their right, and those which
have one neighbor on each side. By making sure to always respond to a move by
the spoiler with an element of the same kind (and, of course, by implementing
a tit-for-tat strategy near the endpoints), the duplicator can easily win the
Ehrenfeucht-Fraïssé-game capturing $\equiv^{\textsc{C}^{2}}_{k,k}$, provided
that the cycles are long enough with respect to $k$.

It would be interesting to find upper bounds for $<\\!\textup{-inv
}$$\textsc{FO}^{2}$ and $<\\!\textup{-inv }$$\textsc{C}^{2}$ tighter than FO\-
that is, tighter than the fragment
$\exists^{*}\forall^{*}\exists^{*}\textsc{FO}$, to which FO collaspes when the
degree is bounded [3] (since already in this fragment, one can count the
number of occurrences of neighborhood types up to some threshold). Let us
briefly explain why we fall short of giving such a bound: in such an attempt,
the initial assumption about the similarity between $\mathcal{A}_{0}$ and
$\mathcal{A}_{1}$ would be weaker than FO-similarity, and it would not be
possible to base our work on neighborhoods. In this context, the starting
hypothesis on the two structures would lack the rigidity which seems necessary
to construct linear orders preserving $\textsc{FO}^{2}$\- or
$\textsc{C}^{2}$-similarity. Establishing such a tighter bound thus seems to
call for new techniques.

Last, we conjecture that the inclusion still holds when we lift the
restriction on the number of variables; namely that $<\\!\textup{-inv
}\textsc{FO}=\textsc{FO}$ when the degree is bounded. This would generalize
the equality $\textup{Succ-inv }\textsc{FO}=\textsc{FO}$ when the degree is
bounded, obtained in [6]. Our hope is that a construction inspired by this one
- albeit significantly refined - and in particular by the alternation of
universal and neighbors segments, could possibly lead to establish such a
result.

We leave these three questions, as well as the issue of the syntactic
decidability of $<\\!\textup{-inv }$$\textsc{C}^{2}$, for further research.

## References

  * [1] Albert Atserias, Anuj Dawar, and Martin Grohe.  Preservation under extensions on well-behaved finite structures.  SIAM Journal on Computing, 2008.
  * [2] Michael Benedikt and Luc Segoufin.  Towards a characterization of order-invariant queries over tame graphs.  J. Symb. Log., 2009.
  * [3] Ronald Fagin, Larry J. Stockmeyer, and Moshe Y. Vardi.  On monadic NP vs. monadic co-NP.  Inf. Comput., 1995.
  * [4] Erich Grädel and Martin Otto.  On logics with two variables.  Theor. Comput. Sci., 1999.
  * [5] Erich Grädel, Martin Otto, and Eric Rosen.  Two-variable logic with counting is decidable.  In LICS, 1997.
  * [6] Julien Grange.  Successor-invariant first-order logic on classes of bounded degree.  In LICS, Logic in Computer Science, 2020.
  * [7] Julien Grange and Luc Segoufin.  Order-Invariant First-Order Logic over Hollow Trees.  In Computer Science Logic, CSL, 2020.
  * [8] Martin Grohe and Thomas Schwentick.  Locality of order-invariant first-order formulas.  ACM Trans. Comput. Log., 2000.
  * [9] Neil Immerman and Dexter Kozen.  Definability with bounded number of bound variables.  Inf. Comput., 1989.
  * [10] Neil Immerman and Eric Lander.  Describing graphs: A first-order approach to graph canonization.  In Complexity theory retrospective. Springer, 1990.
  * [11] Leonid Libkin.  Elements of Finite Model Theory.  Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004\.
  * [12] Michael Mortimer.  On languages with two variables.  Math. Log. Q., 1975.
  * [13] Andreas Potthoff.  Logische klassifizierung regulärer baumsprachen.  Universität Kiel. Institut für Informatik und Praktische Mathematik, 1994.
  * [14] Ian Pratt-Hartmann.  Complexity of the guarded two-variable fragment with counting quantifiers.  J. Log. Comput., 2007.
  * [15] Ian Pratt-Hartmann.  The two-variable fragment with counting revisited.  In WoLLIC, 2010.
  * [16] Philipp Weis and Neil Immerman.  Structure theorem and strict alternation hierarchy for FO^2 on words.  Log. Methods Comput. Sci., 2009.
  * [17] Thomas Zeume and Frederik Harwath.  Order-invariance of two-variable logic is decidable.  In LICS, 2016.