[a] [b]

# About the Expressive Power and Complexity of Order-Invariance with Two
Variables

Bartosz Bednarczyk  and  Julien Grange  Computational Logic Group, TU Dresden
& Institute of Computer Science, University of Wrocław
<EMAIL_ADDRESS>LACL, Université Paris-Est Créteil, France
<EMAIL_ADDRESS>
###### Abstract.

Order-invariant first-order logic is an extension of first-order logic (FO)
where formulae can make use of a linear order on the structures, under the
proviso that they are order-invariant, that their truth value is the same for
all linear orders. We continue the study of the two-variable fragment of
order-invariant first-order logic initiated by Zeume and Harwath, and study
its complexity and expressive power. We first establish coNExpTime-
completeness for the problem of deciding if a given two-variable formula is
order-invariant, which tightens and significantly simplifies the coN2ExpTime
proof by Zeume and Harwath. Second, we address the question of whether every
property expressible in order-invariant two-variable logic is also expressible
in first-order logic without the use of a linear order. we suspect that the
answer is “no”. To justify our claim, we present a class of finite tree-like
structures (of unbounded degree) in which a relaxed variant of order-invariant
two-variable FO expresses properties that are not definable in plain FO. On
the other hand, we show that if one restricts their attention to classes of
structures of bounded degree, then the expressive power of order-invariant
two-variable FO is contained within FO.

###### Key words and phrases:

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

##  1\. Introduction

The main goal of finite model theory is to understand formal languages
describing finite structures: their complexity and their expressive power.
Such languages are ubiquitous in computer science, starting from descriptive
complexity, where they are used to provide machine-independent
characterisations of complexity classes, and ending up on database theory and
knowledge-representation, where formal languages serve as fundamental querying
formalism. A classical idea in finite model theory is to employ invariantly-
used relations, capturing the data-independence principle in databases: it
makes sense to give queries the ability to exploit the presence of the order
in which the data is stored in the memory, but at the same time we would like
to make query results independent of this specific ordering. It is not
immediately clear that the addition of an invariantly-used linear order to
first-order logic (FO) allow us to gain anything on the standpoint of
expressive power. And indeed, as long as we consider arbitrary (not
necessarily finite) structures it does not, which is a direct consequence of
FO having the Craig Interpolation Property. However, as it was first shown by
Gurevich [Lib04, Thm. 5.3], the claim holds true over finite structures:
order-invariant FO is more expressive than plain FO (already the four-variable
fragment of FO can express properties that are not FO-definable).

Unfortunately, order-invariant FO is poorly understood. As stated in [BL16],
one of the reasons why progress in understanding order-invariance is rather
slow is the lack of logical toolkit. The classical model-theoretic methods
based on types were proposed only recently [BL16], and order-invariant FO is
not even a logic in the classical sense, as its syntax is undecidable.
Moreover, the availability of locality-based methods is limited: order-
invariant FO is known to be Gaifman-local [GS00, Thm. 2] but the status of its
Hanf-locality remains open. This suggests that a good way to understand order-
invariant FO is to first look at its fragments, the fragments with a limited
number of variables.

##### Our contribution

We continue the line of research initiated in [ZH16], which aims to study the
complexity and the expressive power of order-invariant $\textsc{FO}^{2}$, the
two-variable fragment of order-invariant FO. From a complexity point of view,
it is known that order-invariant $\textsc{FO}^{2}$ has a coNExpTime-complete
validity problem (which is inherited from $\textsc{FO}^{2}$ with a single
linear order, see [Ott01, Thm. 1.2]), and that whether a given
$\textsc{FO}^{2}$-formula is order-invariant is decidable in coN2ExpTime
[ZH16, Thm. 12]. From an expressive power point of view, order-invariant
$\textsc{FO}^{2}$ is more expressive than plain $\textsc{FO}^{2}$ as it can
count globally, see [ZH16, Example 2]. It remains open [ZH16, Sec. 7],
however, whether it is true that every order-invariant
$\textsc{FO}^{2}$-formula is equivalent to an FO-formula without the linear
order predicate. This paper contributes to the field in the three following
ways:

  * •

We provide a tight bound for deciding order-invariance for $\textsc{FO}^{2}$;
namely, we show that this problem is coNExpTime-complete. Our proof method
relies on establishing an exponential-size counter-model property, and is
significantly easier than the proof of [ZH16, Thm. 12].

  * •

We present a class $\mathdutchcal{C}_{\textit{tree}}$ of tree-like structures,
inspired by [Pot94], and show that there exists an $\textsc{FO}^{2}$-formula
that is _order-invariant over_ $\mathdutchcal{C}_{\textit{tree}}$ (but not
over all finite structures!) which is not equivalent to any FO-formula without
the linear order predicate. This leads us to believe that the answer to the
question of [ZH16, Sec. 7] of whether the expressive power of order-invariant
$\textsc{FO}^{2}$ lies inside FO is “ _no_ ”. The problem remains open,
though.

  * •

In stark contrast to the previous result, we show that order-invariant
$\textsc{FO}^{2}$ cannot express properties beyond the scope of FO over
classes of structures of bounded degree. We show that this upper bound remains
when adding counting to $\textsc{FO}^{2}$.

This work is an extended version of [Bed22] and [Gra23].

##  2\. Preliminaries

We employ standard terminology from finite model theory, assuming that the
reader is familiar with the syntax and the semantics of first-order logic (FO)
[Lib04, Sec. 2.1], basics on computability and complexity [Lib04, Secs.
2.2–2.3], and order-invariant queries [Lib04, Secs. 5.1–5.2]. By
$\textsc{FO}(\Sigma)$ we denote the first-order logic 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

Structures are denoted by calligraphic upper-case letters
$\mathcal{A},\mathcal{B}$ and their domains are denoted by the corresponding
Roman letters $A,B$. We assume that structures have non-empty, _finite_
domains. We write $\varphi[{R}{/}{S}]$ to denote the formula obtained from
$\varphi$ by replacing each occurrence of the symbol $R$ with $S$. We write
$\varphi(\bar{x})$ to indicate that all the free variables of $\varphi$ are in
$\bar{x}$. A sentence is a formula without free variables. By
$\mathcal{A}\mathord{\upharpoonright}_{\Delta}$ we denote the substructure of
the structure $\mathcal{A}$ restricted to the set $\Delta\subseteq A$.

##### Order-invariance

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$ if and only if
$(\mathcal{A},<_{1})\models\varphi$. It is then convenient to omit the
interpretation for the symbol $<$, and to write $\mathcal{A}\models\varphi$ if
$(\mathcal{A},<)\models\varphi$ for any (or, equivalently, every) linear order
$<$. Note that $\varphi$ is _not_ order-invariant if there is a structure
$\mathcal{A}$ and two linear orders $<_{0},<_{1}$ on $A$ such that
$(\mathcal{A},<_{0})\models\varphi$ and
$(\mathcal{A},<_{1})\not\models\varphi$. The set of order-invariant sentences
using two variables is denoted $<\\!\textup{-inv }\textsc{FO}^{2}$. While
determining whether an FO-sentence is order-invariant is undecidable [Lib04,
Ex. 9.3], the situation improves when we allow only two variables: checking
order-invariance for $\textsc{FO}^{2}$-formulae was shown to be in coN2ExpTime
in [ZH16, Thm. 12].111The authors of [ZH16] incorrectly stated the complexity
in their Thm. 12, mistaking “invariance” with “non-invariance”.

##### Decision problems

The _finite satisfiability_ (resp. _validity_) _problem_ for a logic
$\mathcal{L}$ asks whether an input sentence $\varphi$ from $\mathcal{L}$ is
satisfied in some (resp. every) finite structure. Recall that the finite
satisfiability and validity for FO are undecidable [Tur38, Tra50], while for
$\textsc{FO}^{2}$ they are respectively NExpTime-complete and coNExpTime-
complete, see [GKV97, Thm. 5.3] and [Für83, Thm. 3]. Note that $\varphi$ is
finitely valid iff $\neg\varphi$ is finitely unsatisfiable.

##### Definability and similarity

Let $\mathcal{L}$, $\mathcal{L}^{\prime}$ be two logics defined over the same
signature, and $\mathdutchcal{C}$ be a class of finite structures on this
signature. We say that a property $\mathdutchcal{P}\subseteq\mathdutchcal{C}$
is _definable_ (or expressible) in $\mathcal{L}$ on $\mathdutchcal{C}$ if
there exists an $\mathcal{L}$-sentence $\varphi$ such that
$\mathdutchcal{P}=\\{\mathcal{A}\in\mathdutchcal{C}:\
\mathcal{A}\models\varphi\\}$. When $\mathdutchcal{C}$ is the class of all
finite structures, we omit it. We say that
$\mathcal{L}\subseteq\mathcal{L}^{\prime}$ on $\mathdutchcal{C}$ if every
property on $\mathdutchcal{C}$ definable in $\mathcal{L}$ is also definable in
$\mathcal{L}^{\prime}$. Since a sentence which does not mention the linear
order predicate is trivially order-invariant, we get the inclusion
$\textsc{FO}^{2}\subseteq\ <\\!\textup{-inv }\textsc{FO}^{2}$. This inclusion
is strict [ZH16, Example 2].

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 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

An (atomic) _$1$ -type_ over $\Sigma$ is a maximal satisfiable set of atoms or
negated atoms from $\Sigma$ with a free variable $x$. Similarly, an (atomic)
_$2$ -type_ over $\Sigma$ is a maximal satisfiable set of atoms or negated
atoms with variables $x,y$. We stress that it is not necessary that all
variables are mentioned in an atom. Note that the total number of atomic $1$\-
and $2$-types over $\tau$ is bounded exponentially in $|\Sigma|$. We often
identify a type with the conjunction of all its elements. The sets of
$1$-types and $2$-types over the signature consisting of the symbols appearing
in $\varphi$ are respectively denoted
$\mbox{\large\boldmath$\alpha$}_{\varphi}$ and
$\mbox{\large\boldmath$\beta$}_{\varphi}$. Given a structure $\mathcal{A}$ and
an element $a\in A$ we say that $a$ _realises_ a $1$-type $\alpha$ if $\alpha$
is the unique $1$-type such that $\mathcal{A}\models\alpha[a]$ ($a$ satisfies
$\alpha$ in $\mathcal{A}$). We then write $\text{tp}_{\mathcal{A}}^{0}(a)$ to
refer to this type. Similarly, for (non-necessarily distinct) $a,b\in A$, we
denote by $\text{tp}_{\mathcal{A}}^{0}(a,b)$ the unique $2$-type _realised_ by
the pair $(a,b)$, the $2$-type $\beta$ such that
$\mathcal{A}\models\beta[a,b]$ (the pair $a,b$ satisfies $\beta$ in
$\mathcal{A}$).. Finally, given a linearly ordered $\Sigma$-structure
$(\mathcal{A},<)$, we split $\text{tp}_{(\mathcal{A},<)}^{0}(a,b)$ into
$\text{tp}_{\mathcal{A}}^{0}(a,b)$ and $\text{tp}_{<}^{0}(a,b)$, where
$\text{tp}_{<}^{0}(a,b)$ contains (and is fully determined by) one of the
atoms “$x<y$”, “$x>y$” and “$x=y$”.

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

A common way to prove similarity (with respect to some logic) between two
structures is to use Ehrenfeucht-Fraïssé games. Such a game is played between
two players: one tries to highlight the differences between the two
structures, while the other attempts to show that they are identical. There
exists a whole family of those games, each characterizing a specific logic, in
the sense that the second player wins exactly when the two structures cannot
be distinguished by the corresponding logic. These games differ by the kind of
moves allowed, which reflect the particulars of the logic they characterize.

As we are interested in two-variable first-order logic, let us define the two-
pebble FO game, which captures exactly the expressive power of
$\textsc{FO}^{2}$. This flavor of Ehrenfeucht-Fraïssé game has been introduced
by Immerman and Kozen [IK89].

Let us consider two structures $\mathcal{A}_{0}$ and $\mathcal{A}_{1}$. The
_$k$ -round two-pebble Ehrenfeucht-Fraïssé game on $\mathcal{A}_{0}$ and
$\mathcal{A}_{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}$, and $p_{1}^{x}$ and $p_{1}^{y}$ on
$\mathcal{A}_{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}$, and $p_{1}^{x}$ and $p_{1}^{y}$ on elements of
$\mathcal{A}_{1}$. The spoiler wins if the duplicator is unable to ensure 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})$.
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 invariants in
Section 5.4. 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 an 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}(p_{0}^{x},p_{0}^{y})\neq\text{tp}_{\mathcal{A}_{1}}^{0}(p_{1}^{x},p_{1}^{y})$.
Otherwise, another round is played. If the spoiler has not 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 1.

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

##### Gaifman graphs and degree

The _Gaifman graph_ $\mathcal{G}_{\mathcal{A}}$ of a structure $\mathcal{A}$
is the simple graph with vertices in $A$ and undirected edges between any pair
of distinct elements that appear in the same tuple of some relation of
$\mathcal{A}$. By $\text{dist}_{\mathcal{A}}(a,b)$ we denote the distance
between $a$ and $b$ in $\mathcal{G}_{\mathcal{A}}$, defined in the usual way.
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. The class $\mathdutchcal{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\mathdutchcal{C}$ is at most $d$.

##  3\. Complexity of the invariance problem

We study the complexity of the problem of deciding if an input formula
$\varphi\in\textsc{FO}^{2}$ is order-invariant and establish its coNExpTime-
completeness. Starting from the lower bound first, let us consider the
following program, inspired by slides of Schweikardt [Sch13, Slide 9]. This
provides a Turing reduction from finite $\textsc{FO}^{2}$-validity to testing
order-invariance of $\textsc{FO}^{2}$-sentences: Procedure 1 returns True iff
its input is finitely valid.

Input: An $\textsc{FO}^{2}$-formula $\varphi$.

1

If $\neg\varphi$ has a model with a single-element domain, return False.

// a corner case

2

3Let $\psi_{<}:=\exists{x}\left(P(x)\land\forall{y}(y\leq x)\right)$ for a
fresh unary predicate $P$.

// not $<$-inv on all $P$-expansions of $\mathcal{A}$ as soon as $|A|\geq 2$

4

Return True if $(\neg\varphi)\to\psi_{<}$ is $<$-invariant and False
otherwise.

// the reduction

Procedure 1 From finite validity to $<$-invariance

Correctness of Procedure 1 follows from a straightforward case analysis.
Indeed:

######  Lemma 2.

Procedure 1 returns True iff $\varphi$ is finitely valid.

######  Proof 3.1.

We consider the following two cases:

  * •

If $\varphi$ is finitely valid then Procedure 1 returns True. Note that since
$\varphi$ is finitely valid then $\neg\varphi$ is finitely unsatisfiable.
Hence, the first step of the algorithm is skipped. For the second step, note
that the formula $(\neg\varphi)\to\psi$ is logically equivalent to $\top$
(over finite structures we have $\neg\varphi\equiv\bot$) and hence, trivially
$<$-invariant. Thus Procedure 1 returns True.

  * •

If $\varphi$ is not finitely valid then Procedure 1 returns False. Indeed, in
that case $\neg\varphi$ has a finite model. If it has a model with a single
domain element, then the first step of Procedure 1 returns False. Otherwise,
it has a model with at least $2$ domain elements: call it $\mathcal{A}$ and
enumerate its elements with $a_{1},a_{2},\ldots,a_{n}$. Let $\mathcal{B}$ be
the finite structure with $P^{\mathcal{B}}=\\{a_{n}\\}$ whose $\tau$-reduct is
$\mathcal{A}$. Clearly $\mathcal{B}\models\neg\varphi$, since the predicate
$P$ is fresh. Finally, let $<_{1},<_{2}$ be two linear orders on $B$: the
first one orders the elements $a_{i}$ of $B$ according to their subscript
numbering, while the second ordering is like the first one but swaps the
positions of $a_{1}$ and $a_{n}$. Now note that
$(\mathcal{B},<_{1})\models(\neg\varphi)\to\psi_{<}$ but
$(\mathcal{B},<_{2})\not\models(\neg\varphi)\to\psi_{<}$ (the formula
$\psi_{<}$ basically states that the maximal element of $<_{i}^{\mathcal{B}}$
satisfies $P$). Hence, the formula $(\neg\varphi)\to\psi_{<}$ is not
$<$-invariant and Procedure 1 returns False.

Hence, applying Lemma 2 and coNExpTime-hardness of finite validity problem for
$\textsc{FO}^{2}$ [Für83, Thm. 3], we conclude:

######  Theorem 3.

Testing whether an $\textsc{FO}^{2}$ formula is order-invariant is coNExpTime-
hard.

Our upper bound uses the following fact, immediate from the definition of
order-invariance.

######  Fact 4.

An $\textsc{FO}^{2}$ sentence $\varphi$ is _not_ order-invariant iff the
sentence $\varphi[{<}{/}{<_{0}}]\land\neg\varphi[{<}{/}{<_{1}}]$ is finitely
satisfiable over structures interpreting $<_{0}$ and $<_{1}$ as linear orders
over the domain.

Let $\textsc{FO}^{2}_{-}[<_{0},<_{1}]$ be composed of sentences of the shape
$\varphi[{<}{/}{<_{0}}]\land\neg\varphi[{<}{/}{<_{1}}]$ for all sentences
$\varphi\in\textsc{FO}^{2}(\Sigma\cup\\{<\\})$ over all signatures $\Sigma$.
To simplify the reasoning about such formulae, we rewrite them into the so-
called _Scott Normal Form_.

######  Lemma 5.

For any $\textsc{FO}^{2}_{-}[<_{0},<_{1}]$-sentence $\varphi$ there is
polynomial-time computable $\textsc{FO}^{2}_{-}[<_{0},<_{1}]$-sentence
$\varphi_{\textit{scott}}$ (over a relational signature composed of predicates
of arity only $1$ or $2$) of size polynomial w.r.t. $\varphi$ such that having
the form:

$\varphi_{\textit{scott}}\coloneq\bigwedge_{i=0}^{1}\left(\forall{x}\forall{y}\;\chi_{i}(x,y)\land\bigwedge\limits_{j=1}^{m_{i}}\forall{x}\exists{y}\
\gamma_{i}^{j}(x,y)\right),$

where the decorated $\chi$ and $\gamma$ are quantifier-free and the $<_{i}$ do
not appear in $\chi_{1-i}$ and $\gamma_{1-i}^{j}$, such that $\varphi$ is
finitely satisfiable over structures interpreting $<_{0}$ and $<_{1}$ as
linear orders over the domain if and only if $\varphi_{\textit{scott}}$ is.

######  Proof 3.2.

The logic $\textsc{ESO}^{2}$ is a fragment of existential second-order logic,
in which formulae take the form $\exists{\bar{R}}\varphi$, where $\bar{R}$ is
a tuple of relations and $\varphi$ uses only the variables $x$ and $y$ and
relational symbols from $\bar{R}$. Without loss of generality [ZH16, p.3,
col.1] we can assume that $\bar{R}$ contains only relation symbols of arity at
most two. Clearly any $\textsc{FO}^{2}$-sentence over the vocabulary
$\Sigma\cup\\{<_{0},<_{1}\\}$ can be seen as an $\textsc{ESO}^{2}$ sentence
over $\\{<_{0},<_{1}\\}$ and vice-versa. We say that
$\textsc{ESO}^{2}$-formulae $\varphi$ and $\varphi^{\prime}$ over
$\\{<_{0},<_{1}\\}$ are _order-equivalent_ if for all
$\\{<_{0},<_{1}\\}$-structures $\mathcal{A}$ we have
$\mathcal{A}\models\varphi$ if and only if
$\mathcal{A}\models\varphi^{\prime}$. Zeume and Harwath [ZH16, Lemma 1] proved
that for any $\textsc{ESO}^{2}$ sentence $\varphi$ one can compute in
polynomial-time an order-equivalent $\textsc{ESO}^{2}$ sentence
$\varphi_{\textit{zh}}$ of the form
$\forall{x}\forall{y}\;\psi(x,y)\land\bigwedge_{i}\forall{x}\exists{y}\
\psi_{i}(x,y)$, where $\psi$ and all $\psi_{i}$ are quantifier-free and all
symbols used in $\varphi_{\textit{zh}}$ are of arity at most two.

Let $\varphi\coloneq\varphi_{0}\land\varphi_{1}$ be an
$\textsc{FO}^{2}_{-}[<_{0},<_{1}]$-sentence, where
$\varphi_{i}\coloneq\varphi[{<}{/}{<_{i}}]$. Note that $<_{1}$ does not appear
in $\varphi_{0}$, and $<_{0}$ does not appear in $\varphi_{1}$. Let
$\varphi^{\prime}\coloneq\exists{\bar{R}}(\varphi_{0}\land\varphi_{1})$ be the
corresponding $\textsc{ESO}^{2}$-sentence. Clearly
$\exists{\bar{R}}(\varphi_{0}\land\varphi_{1})$ is finitely satisfiable over
structures interpreting $<_{0}$ and $<_{1}$ as linear orders over the domain
if and only if $\varphi$ is. Now apply the result222The proof goes via a
routine renaming by replacing formulae with a single free variable with a
fresh unary predicate and sharpening its interpretation. We take the maximally
nested subformula starting from a single quantifier, e.g.
$\exists{x}\lambda(x,y)$. We then replace the formula $\exists{x}\lambda(x,y)$
with $A(y)$ for a fresh unary predicate $A$, and append the conjunct
$\forall{y}\ (\exists{x}\lambda(x,y))\leftrightarrow A(y)$. We then split
equivalence into two implications, yielding the formulae of the form
$\forall\forall\theta$ and $\forall\exists\xi$. By repeating the procedure and
regrouping formulae, we obtain the desired equivalent formula in normal form.
of Zeume and Harwath [ZH16, Lemma 1] to $\exists{\bar{R}}\varphi_{0}$ and
$\exists{\bar{R}}(\varphi_{1})$ in order to compute (in polynomial time) a
polynomially larger order-equivalent formulae
$\exists{\bar{R}_{0}}\varphi_{0}$ and $\exists{\bar{R}_{1}}\varphi_{1}$. After
a renaming, we can assume that $\bar{R}_{0}$ and $\bar{R}_{1}$ have no common
symbols. Moreover, note that $\varphi_{i}$ does not employ the order predicate
$<_{1{-}i}$. Clearly the formulae
$(\exists{\bar{R}}\varphi_{0})\land(\exists{\bar{R}}\varphi_{1})$ and
$\exists{\bar{R}_{0}}\exists{\bar{R}_{1}}\varphi_{0}\land\varphi_{1}$ are
order-equivalent. Hence, $\varphi$ has is finitely satisfiable over structures
interpreting $<_{0}$ and $<_{1}$ as linear orders over the domain if and only
if $\varphi_{0}\land\varphi_{1}$ is. After shifting positions and regrouping
subformulae of $\varphi_{0}\land\varphi_{1}$, we obtain the formula in the
desired shape as in the statement of the lemma.

For brevity we speak about $\forall\forall$ and $\forall\exists$-conjuncts of
$\varphi$ in the normal form given above, meaning the appropriate subformulae
of $\varphi$ starting from the mentioned prefix of quantifiers. Given a model
$\mathcal{A}\models\varphi$ of a formula $\varphi$ in Scott’s normal form
given above and elements $a,b\in A$ such that
$\mathcal{A}\models\gamma_{i}^{j}(a,b)$, we call $b$ a
$\gamma_{i}^{j}$-_witness_ for $a$ (or simply a witness). The core of our
upper bound proof is the following small model theorem, employing the circular
witnessing scheme by Grädel, Kolaitis, and Vardi [GKV97, Thm. 4.3].

######  Lemma 6.

If an $\textsc{FO}^{2}_{-}[<_{0},<_{1}]$ sentence $\varphi$ (in normal form of
Lemma 5) has a finite model (that interprets $<_{0},<_{1}$ as linear orders
over the domain) then there exists such a finite model with
$\mathcal{O}(|\varphi|^{3}\cdot 2^{|\varphi|})$ elements.

######  Proof 3.3.

Let $M\coloneq m_{0}+m_{1}$ be the total number of $\forall\exists$-conjuncts
of $\varphi$, and let $\mbox{\large\boldmath$\alpha$}_{\varphi}$ be the set of
all $1$-types over the set of unary symbols of $\varphi$. Recall that $M$ is
polynomial in $|\varphi|$ and $\mbox{\large\boldmath$\alpha$}_{\varphi}$ is
exponential w.r.t. $|\varphi|$. Suppose that $\mathcal{A}$ is a finite model
of $\varphi$ that interprets $<_{0},<_{1}$ as linear orders over the domain,
and let us explain our proof plan.

Intuition and proof plan. In what follows, we employ a variant of the circular
witnessing scheme by Grädel, Kolaitis, and Vardi [GKV97, Thm. 4.3] in order to
distinguish three disjoint sets of domain elements of $\mathcal{A}$, namely
$W_{0},W_{1},W_{2}$ whose union $W\coloneq W_{0}\cup W_{1}\cup W_{2}$ will
serve as a “base” of a new “small” model of $\varphi$. In order to satisfy
$\varphi$, the universal $(\forall\forall)$ and the existential
$(\forall\exists)$ conjuncts of $\varphi$ must be fulfilled. In our
construction, we first distinguish a set $W_{0}$ of elements of $\mathcal{A}$
that contains elements of $\mathcal{A}$ with $1$-types that do not appear
“frequently” in $\mathcal{A}$ together with the first and last $M$
realisations w.r.t. $<_{0}$ and w.r.t. $<_{1}$ of each $1$-type needed later
in the construction. Unfortunately, $\mathcal{A}$ restricted to $W_{0}$ may
not be a model of $\varphi$. Indeed, while such a structure satisfies the
universal part of $\varphi$, some elements from $W_{0}$ may violate
$\forall\exists$-conjuncts of $\varphi$. To “repair” the resulting structure,
we construct the set $W_{1}$ by taking the minimal number of elements in
$\mathcal{A}$ so that all elements from $W_{0}$ have all the required
$\gamma_{i}^{j}$-witnesses in $\mathcal{A}$ restricted to $W_{0}\cup W_{1}$.
Note that $W_{1}$ has no more than $M\cdot|W_{0}|$ elements. The situation is
a bit better now: the $\mathcal{A}$ restricted to $W_{0}\cup W_{1}$ again
satisfies the $\forall\forall$-subformula of $\varphi$ (as the universal
formulae are preserved under taking substructures), all elements from $W_{0}$
have their required witnesses for subformulae $\gamma_{i}^{j}$, but there may
be still some elements $W_{1}$ may violate $\forall\exists$-conjuncts of
$\varphi$. We “repair” the resulting structure one final time by constructing
the set $W_{2}$ analogously to the case of $W_{1}$, so that all the required
$\gamma_{i}^{j}$-witnesses for the elements from $W_{1}$ in $\mathcal{A}$ are
in the set $W_{0}\cup W_{1}\cup W_{2}$. Unfortunately, for the same reason as
before, some elements from $W_{2}$ may violate some
$\forall\exists$-subformulae of $\varphi$. To fix the problem, for each of
such elements $a$, we suitably select $M$ pairwise-different elements
$b_{1},b_{2},\ldots,b_{M}$ from $W_{0}$ and alter binary relations between $a$
and all of $b$ in order to provide suitable witnesses for $a$. By our choice
of $W_{0}$ such _different_ elements will always exist. The resulting $2$-type
between $a$ and other $b_{i}$ will be one of the $2$-types already present in
$\mathcal{A}$, which ensures that we do not accidentally violate the
$\forall\forall$-subformulae of $\varphi$.333It would be unwise to apply the
same approach to $W_{1}$, as such elements are already constrained by the
construction of $W_{0}$ (while $W_{2}$ are not!). Finally, by construction,
all the selected elements have the required witnesses in $W_{0}\cup W_{1}\cup
W_{2}$, and hence the $\forall\exists$-subformulae of $\varphi$ are also
satisfied in the altered structure $\mathcal{A}$ restricted to $W_{0}\cup
W_{1}\cup W_{2}$. This yields a desired “small” model of the formula $\varphi$
and concludes the proof.

The construction of $W_{0}$. Call a $1$-type
$\alpha\in\mbox{\large\boldmath$\alpha$}_{\varphi}$ _rare_ if it is realised
by at most $4M$ elements in $\mathcal{A}$ (the factor $4$ comes from the fact
that we consider maximal and minimal elements w.r.t. $<_{0}$ and $<_{1}$ and
$M$ is the number of $\forall\exists$-conjuncts of $\varphi$). For every
$1$-type $\alpha\in\mbox{\large\boldmath$\alpha$}_{\varphi}$ that is not rare,
we select $M$ minimal and $M$ minimal elements w.r.t. each of the orders
$<_{0}$ and $<_{1}$ that realise $\alpha$. Let $W_{0}$ be the set of the
selected elements from $\mathcal{A}$ together with all elements of
$\mathcal{A}$ realising rare $1$-types.

The construction of $W_{1}$ and $W_{2}$. We next close $W_{0}$ twice under
taking witnesses. More precisely, let $W_{1}$ be any $\subseteq$-minimal
subset of $A$ so that all elements from $W_{0}$ have all the required
$\gamma_{i}^{j}$-witnesses in $W_{0}\cup W_{1}$. Similarly, we define $W_{2}$
to be any $\subseteq$-minimal subset of $A$ so that all elements from
$W_{0}\cup W_{1}$ have all the required $\gamma_{i}^{j}$-witnesses in
$W_{0}\cup W_{1}\cup W_{2}$. As they are only $M$ different
$\gamma_{i}^{j}$-formulae in $\varphi$, we have that:

$|W_{1}|\leq M|W_{0}|\leq
4M^{2}|\mbox{\large\boldmath$\alpha$}_{\varphi}|\;\text{and}\;|W_{2}|\leq
M|W_{0}\cup W_{1}|\leq
M\cdot(4M+4M^{2})|\mbox{\large\boldmath$\alpha$}_{\varphi}|\leq
8M^{3}|\mbox{\large\boldmath$\alpha$}_{\varphi}|.$

The construction of $\mathcal{B}$. Consider the structure
$\mathcal{B}\coloneq\mathcal{A}\mathord{\upharpoonright}_{W_{0}\cup W_{1}\cup
W_{2}}$. We see that:

$|B|\leq|W_{0}|+|W_{1}|+|W_{2}|\leq(4M+4M^{2}+8M^{3})|\cdot|\mbox{\large\boldmath$\alpha$}_{\varphi}|\leq
16M^{3}\cdot|\mbox{\large\boldmath$\alpha$}_{\varphi}|\leq 16\
|\varphi|^{3}\cdot 2^{|\varphi|}.$

Hence, the size of $\mathcal{B}$ is as desired. Note that universal formulae
are preserved under substructures, thus
$<_{0}^{\mathcal{B}},<_{1}^{\mathcal{B}}$ are linear orders over $B$ and
$\mathcal{B}$ satisfies the $\forall\forall$-conjuncts of $\varphi$. Hence, by
the construction of $W_{1}$ and $W_{2}$, the only reason for $\mathcal{B}$ to
not be a model of $\varphi$ is the lack of required $\gamma_{i}^{j}$-witnesses
for elements from the set $W_{3}$. We fix this issue by reinterpreting binary
relational symbols between the sets $W_{3}$ and $W_{1}$.

Reinterpreting binary relations in $\mathcal{B}$. Let us fix an element $a$
from $W_{2}$ that violate some of the $\forall\exists$-conjuncts of $\varphi$
in $\mathcal{B}$, as well as a $\forall\exists$-conjunct
$\psi\coloneq\forall{x}\exists{y}\ \gamma_{i}^{j}(x,y)$ whose satisfaction is
violated by $a$. We stress that there are at most $M$ such conjuncts, and
$\gamma_{i}^{j}$ does not use the $<_{1{-}i}$ predicate. Since
$\mathcal{A}\models\varphi$ we know that there is an element $b\in A$
(different from $a$) such that $b$ is a $\gamma_{i}^{j}$-witness for $a$ and
$\gamma_{i}^{j}$ in $\mathcal{A}$. Let $\alpha$ be the $1$-type of $b$ in
$\mathcal{A}$. Note that $\alpha$ is not rare. Indeed, otherwise $b\in W_{0}$,
and hence $b\in B$. Moreover either $b<_{i}^{\mathcal{A}}a$ or
$a<_{i}^{\mathcal{A}}b$ holds. Suppose that $b<_{i}^{\mathcal{A}}a$ holds (the
other case is analogous), and pick an element $a^{\prime}$ from $W_{0}$ among
$M$-minimal (w.r.t. $<_{i}$) realisations of the $1$-type $\alpha$. In case
$a^{\prime}$ was already selected to provide a missing witness for $a$, we
take yet another one. Note that such an element exists due to the fact that
there are only $M$ $\forall\exists$-conjuncts in $\varphi$ and we selected $M$
minimal and maximal realisations of every non-rare $1$-type for each of the
orders $<_{0}$ and $<_{1}$. We now alter the binary relations between $a$ and
$a^{\prime}$ in $\mathcal{B}$ so that the equality holds
$\text{tp}^{0}_{\mathcal{A}}(a,b)=\text{tp}^{0}_{\mathcal{B}}(a,b)$ holds
(which can be done as $a^{\prime}$ and $b$ have equal $1$-type). We repeat the
process to provide all missing witnesses for $a$. Observe that all elements
from $B$ that had $\gamma_{i}^{j}$-witnesses before our redefinition of
certain $2$-types, still do have them (as we did do not touch $2$-types
between them and their witnesses), $\mathcal{B}$ still satisfies the
$\forall\forall$-component of $\varphi$ (since the modified $2$-type does not
violate $\varphi$ in $\mathcal{A}$ it does not violate $\varphi$ in
$\mathcal{B}$) and $a$ has all required witnesses. By repeating the strategy
for all the other elements from $W_{3}$ violating $\varphi$, we obtain the
desired “small” model of $\varphi$.

Lemma 6 yields an NExpTime algorithm for deciding satisfiability of
$\textsc{FO}^{2}_{-}[<_{0},<_{1}]$ formulae: convert an input into Scott’s
normal form, guess its exponential size model and verify the modelhood with a
standard model-checking algorithm (in PTime [GO99, Prop. 4.1]). After applying
Fact 4 and Theorem 3 we conclude:

######  Theorem 7.

Checking if an $\textsc{FO}^{2}$-formula is order-invariant is coNExpTime-
complete.

##  4\. Can order-invariant $\textsc{FO}^{2}$ express properties beyond the
scope of FO?

While we do not solve the question stated in the heading of this section, we
provide a partial solution. Let $\mathdutchcal{C}$ be some class of 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 over $\mathdutchcal{C}$_ if for every finite
$\Sigma$-structure $\mathcal{A}$ _in $\mathdutchcal{C}$_, and every pair of
strict linear orders $<_{0}$ and $<_{1}$ on $A$,
$(\mathcal{A},<_{0})\models\varphi$ iff $(\mathcal{A},<_{1})\models\varphi$.
Note that this is a weakening of the classical condition of order-invariance,
and that the usual definition is recovered when $\mathdutchcal{C}$ is the
class of all finite structures.

In what follows, we present a class $\mathdutchcal{C}$ over the vocabulary
$\Sigma:=\\{T,D,S\\}$ of tree-like finite structures, and a sentence
$\varphi\in\textsc{FO}^{2}(\Sigma\cup\\{<\\})$ “expressing even depth” that is
order-invariant over $\mathdutchcal{C}$ but not equivalent to any first-order
sentence over $\Sigma$.

A _dendroid_ is a finite $\Sigma$-structure $\mathcal{A}$ that, intuitively,
is a complete directed binary tree decorated with a binary parent-child
relation $T^{\mathcal{A}}$, a descendant relation $D^{\mathcal{A}}$, and a
sibling relation $S^{\mathcal{A}}$. Formally, a $\Sigma$-structure
$\mathcal{A}$ is called a _dendroid_ if there is a positive integer $n$ such
that

  * •

$A=\\{0,1\\}^{\leq n}$ (the set of all binary words of length at most $n$),

  * •

$T^{\mathcal{A}}=\\{(w,w0),(w,w1)\;\mid\;w\in A,|w|<n\\}$,

  * •

$D^{\mathcal{A}}=(T^{\mathcal{A}})^{+}$ ($D^{\mathcal{A}}$ is the transitive
closure of $T^{\mathcal{A}}$), and

  * •

$S^{\mathcal{A}}=\\{(w0,w1),(w1,w0)\;\mid\;w\in A,|w|<n\\}$.

We call the number $n$ the _depth_ of $\mathcal{A}$, and call the length of a
node $v\in A$ the _level_ of $v$. We also use the terms “root” and “leaf” in
the usual way.

The following is a variant of a classical exercise stating that for every
threshold $q$ we have that trees that are exponentially deep w.r.t. $q$ are
$\textsc{FO}_{q}$-equivalent. Indeed:

######  Lemma 8.

For all $q\in\mathbb{N}$, whenever $\mathcal{A},\mathcal{B}$ are dendroids of
depth $\geq 2^{q{+}1}$ then $\mathcal{A}\equiv_{q}^{\textsc{FO}}\mathcal{B}$.

######  Proof 4.1.

This is a tedious generalisation of the winning strategy for the duplicator in
the $q$-round Ehrenfeucht-Fraïssé games on linear orders [Lib04, Thm 3.6 Proof
#1].

As an immediate corollary we get:

######  Corollary 9.

There is no $\textsc{FO}(\Sigma)$-formula $\varphi_{\textrm{even}}$ such that
for every $\mathcal{A}\in\mathdutchcal{C}$ we have
$\mathcal{A}\models\varphi_{\textrm{even}}$ iff the depth of $\mathcal{A}$ is
even.

In contrast to Corollary 9, we show that the even depth query can be defined
with an $\textsc{FO}^{2}(\Sigma\cup\\{<\\})$-formula which is order-invariant
over $\mathdutchcal{C}$ (but unfortunately not over the class of all finite
structures). Henceforth we considered _ordered dendroids_ , dendroids that are
additionally linearly-ordered by $<$. Given such an ordered dendroid
$\mathcal{T}$, and an element $c$ with children $a,b$ we say that $a$ is the
_left child_ of $c$ iff $a<^{\mathcal{T}}b$ holds. Otherwise we call $a$ the
_right child_ of $c$. A _zig-zag_ in the ordered $\mathcal{T}$ is a sequence
of elements $a_{0},a_{1},\ldots,a_{n}$, where $a_{n}$ is a leaf of
$\mathcal{T}$, $a_{0}$ is the root of $\mathcal{T}$, $a_{2i{+}1}$ is the right
child of $a_{2i}$ for any $i\geq 0$ and $a_{2i}$ is the left child of
$a_{2i{-}1}$ for any $\frac{n}{2}\geq i\geq 1$. A zig-zag is _even_ if its
last element is the left child of its parent, and _odd_ otherwise. The
underlying trees in dendroids are complete and binary, thus: An ordered
dendroid $\mathcal{T}$ has an even zig-zag iff $\mathcal{T}$ is of even depth.
Moreover, if $\mathcal{T}$ is a dendroid of even (resp. odd) depth then for
any linear order $<$ over its domain the ordered dendroid $(\mathcal{T},<)$
has an even (resp. odd) zig-zag.

######  Proof 4.2.

Immediate by induction after observing that
$\mathcal{A}\mathord{\upharpoonright}_{\\{0,1\\}^{\leq n}}$, for any positive
integer $n$ smaller than the depth of $\mathcal{A}$, is also a dendroid.

The above lemma suggests that a good way to express the evenness of the depth
of a dendroid is to state the existence of an even zig-zag; this is precisely
the property that we are going to describe with an $\textsc{FO}^{2}$-formula.
Let us first introduce a few useful macros:

$\mathtt{ROOT}(x):=\neg\exists{y}\;T(y,x)\qquad\mathtt{LEAF}(x):=\neg\exists{y}\;T(x,y)\qquad\mathtt{2nd}(x):=\exists{y}\;T(y,x)\land\mathtt{ROOT}(y)$
$\mathtt{LS}(x):=\exists{y}\;S(x,y)\land
x<y\qquad\mathtt{RS}(x):=\exists{y}\;S(x,y)\land y<x$

The first two macros have an obvious meaning. The third macro identifies a
child of the root, while the last two macros identify, respectively, the left
and the right siblings (according to the linear order $<$). Our desired
formula $\varphi_{\textrm{even-zig-zag}}$ is then:

$\exists{x}\;\Big{(}\;\;\;\;[\mathtt{LEAF}(x)\land\mathtt{LS}(x)]\land[\forall{y}\;(\mathtt{2nd}(y)\land
D(y,x))\to\mathtt{RS}(y)]$
$\land[\forall{y}\;(\neg\mathtt{ROOT}(y)\land\neg\mathtt{2nd}(y)\land
D(y,x)\land\mathtt{RS}(y))\to\exists{x}\;T(x,y)\land\mathtt{LS}(x)]$
$\land[\forall{y}\;(\neg\mathtt{ROOT}(y)\land\neg\mathtt{2nd}(y)\land
D(y,x)\land\mathtt{LS}(y))\to\exists{x}\;T(x,y)\land\mathtt{RS}(x)]\;\;\;\;\Big{)}$

Note that the above formula, by fixing a leaf, fixes the whole path from such
a leaf to the root (since root-to-leaf paths in trees are unique). To say that
such a path is an even zig-zag, we need a base of induction (the first line)
stating that the selected leaf is a left child and the root’s child lying on
this path is its right one, as well as an inductive step stating that every
left (resp. right) child on the path has a parent which is itself a right
(resp. left) child, with the obvious exception of the root and its child. From
there, it is easily shown that:

######  Proposition 10.

An ordered dendroid $\mathcal{T}$ satisfies $\varphi_{\textrm{even-zig-zag}}$
iff it has even depth.

######  Proof 4.3.

To prove the right-to-left implication, we use Observation 4 to infer the
existence of an even zig-zag $a_{0},a_{1},\ldots,a_{2n}$ in $\mathcal{T}$.
Taking $a_{2n}$ as a witness for the existential quantifier in front of
$\varphi_{\textrm{even-zig-zag}}$ and going back to the definition of an even
zig-zag, we get $\mathcal{T}\models\varphi_{\textrm{even-zig-zag}}$. For the
other direction, consider a leaf $a$ satisfying the properties enforced in
$\varphi_{\textrm{even-zig-zag}}$. There is a unique path
$\rho=a_{0},a_{1},\ldots,a_{n}=a$ from the root of $\mathcal{T}$ to $a$. The
first line of $\varphi_{\textrm{even-zig-zag}}$ guarantees that $a_{n}$ is a
left child and $a_{1}$ is a right child. We then show by induction, relying on
the last two lines of $\varphi_{\textrm{even-zig-zag}}$, that for any $i\geq
0$, $a_{2i{+}1}$ is the right child of $a_{2i}$, and for $i\geq 1$, $a_{2i}$
is the left child of $a_{2i{-}1}$. Thus $\rho$ is an even zig-zag. By invoking
Observation 4 again, we get that $\mathcal{T}$ has even depth.

As a direct consequence of the previous statement, observe that our formula
$\varphi_{\textrm{even-zig-zag}}$ is order-invariant over $\mathdutchcal{C}$:
whether an ordered dendroid has even depth only depends on the underlying
dendroid, and not on the particulars of its linear order. Recalling Corollary
9, we conclude the following:

######  Theorem 11.

There exists a class of finite structures $\mathdutchcal{C}$ and an
$\textsc{FO}^{2}(\Sigma\cup\\{<\\})$-sentence which is order-invariant over
$\mathdutchcal{C}$, but is not equivalent to any $\textsc{FO}(\Sigma)$
sentence.

##  5\. Expressive power when the degree is bounded

We have seen in the previous section that if we relax the order-invariant
constraint (namely, by requiring invariance only on a restricted class of
structures), then one is able to define, with two variables, properties that
lie beyond the expressive power of FO. We conjecture that this is still the
case when requiring invariance over the class of all finite structures.

In this section, we go the other way, and show that when one considers only
classes of bounded degree, then $<\\!\textup{-inv }\textsc{FO}^{2}$ can only
express FO-definable properties. Note that although the class
$\mathdutchcal{C}$ from Section 4 contains tree-like structures, the
descendant relation makes this a dense class of structures (as it contains
cliques of arbitrarily large size), and in particular $\mathdutchcal{C}$ does
not have a bounded degree.

###  5.1. Overview of the result

We give an upper bound to the expressive power of order-invariant
$\textsc{FO}^{2}$ when the degree is bounded:

######  Theorem 12.

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

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

Let us now detail the outline of the proof. The technical parts of the proof
will be the focus of Sections 5.3 and 5.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 $\mathdutchcal{C}$ (satisfied by the same structures of
$\mathdutchcal{C}$) to an FO-formula $\psi$ of quantifier rank at most $f(k)$.

To prove the existence of such an equivalent FO-formula $\psi$ to any order-
invariant $\textsc{FO}^{2}$-formula $\varphi$ on $\mathdutchcal{C}$, we will
pick $f(k)$ large enough so that for any two structures
$\mathcal{A}_{0},\mathcal{A}_{1}\in\mathdutchcal{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}$. In other word, we show that the
equivalence relation $\equiv^{{\textsc{FO}}}_{f(k)}$ is more fine-grained than
the equivalence relation $\equiv^{{<\\!\textup{-inv }\textsc{FO}^{2}}}_{k}$.
Let us show that this indeed guarantees the existence of $\psi$. By definition
of $\equiv^{{<\\!\textup{-inv }\textsc{FO}^{2}}}_{k}$, the class of structures
satisfying a formula $\varphi$ of $<\\!\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 $\mathdutchcal{C}$ is consequently the intersection of
$\mathdutchcal{C}$ with a union of equivalence classes $c_{1},\ldots,c_{l}$
for $\equiv^{{\textsc{FO}}}_{f(k)}$. It is folklore (see, , [Lib04, Cor.
3.16]) that there are only a finite number of equivalence classes for
$\equiv^{{\textsc{FO}}}_{f(k)}$, each of which being definable by an FO-
sentence of quantifier rank $f(k)$. Then the disjunction $\psi$ of the
sentences defining $c_{1},\ldots,c_{l}$ (which is again an FO-sentence of
quantifier rank $f(k)$) is indeed equivalent to $\varphi$ on
$\mathdutchcal{C}$, thus showing that the addition of a built-in order does
not allow to express more first-order properties on $\mathdutchcal{C}$,
although it may allow more concise descriptions of these properties.

In order to show that $\mathcal{A}_{0}\equiv^{{<\\!\textup{-inv
}\textsc{FO}^{2}}}_{k}\mathcal{A}_{1}$ for any structures $\mathcal{A}_{0}$
and $\mathcal{A}_{1}$ of $\mathdutchcal{C}$ such that
$\mathcal{A}_{0}\equiv^{{\textsc{FO}}}_{f(k)}\mathcal{A}_{1}$, we will
construct in Section 5.3 two particular orders $<_{0}$, $<_{1}$ on these
respective structures, and we will prove in Section 5.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}$.

In the process of constructing the linear orders $<_{0}$ and $<_{1}$ on
$\mathcal{A}_{0}$ and $\mathcal{A}_{1}$, it will be convenient to sort the
elements of these structures based on the isomorphism type of their
_neighbourhood_ (for $k\in\mathbb{N}$, the $k$-neighbourhood of some element
$a$ is the substructure induced by the set of elements that are at distance at
most $k$ from $a$). This notion is central in finite model theory, and is the
basic tool of the locality methods to prove inexpressibility results. For an
introduction on the subject, see, , [Lib04, Chapter 4].

Section 5.2 is devoted to the notion of neighbourhood: it is defined in
Section 5.2.1, where we recall that, when the degree is bounded, first-order
logic is precisely able to express properties that depend on the number (up to
some threshold) of each isomorphism type of neighbourhood. In Section 5.2.2,
we establish a dichotomy between neighbourhood types that appear frequently in
a structure, and those that have only a few occurrences. This distinction will
highlight which elements play a particular role in the structures
$\mathcal{A}_{0}$ and $\mathcal{A}_{1}$, and should thus be treated with
special care when constructing the linear orders. On the other hand, we can be
much more liberal with the way we treat elements with a frequent neighbourhood
type; in particular, we will use them as padding between critical parts of the
orders.

Lastly, we show in Section 5.5 that when the degree is bounded, the inclusion
of $<\\!\textup{-inv }\textsc{FO}^{2}$ in FO still holds when one adds
counting quantifiers to $\textsc{FO}^{2}$.

###  5.2. Neighbourhoods

####  5.2.1. Definition and properties of neighbourhoods

Let us start by defining the notion of neighbourhood of an element in a
structure.

Let $c$ be a new constant symbol, and let $\mathcal{A}\in\mathdutchcal{C}$.
For $k\in\mathbb{N}$ and $a\in A$, the (pointed) _$k$ -neighbourhood_
$\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$-neighbourhood 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$ -neighbourhood type_ $\tau=\text{neigh-tp}_{\mathcal{A}}^{k}(a)$ of $a$
in $\mathcal{A}$ is the isomorphism class of its $k$-neighbourhood. We say
that $\tau$ is a $k$-neighbourhood 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}$ (the number of elements with
$k$-neighbourhood $\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$-neighbourhood 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$-neighbourhood 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
neighbourhood types up to some threshold [FSV95]. We will only use one
direction of this characterization, namely:

######  Proposition 13.

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
$\mathdutchcal{C}$) such that for all structures
$\mathcal{A}_{0},\mathcal{A}_{1}\in\mathdutchcal{C}$,
$\mathcal{A}_{0}\equiv^{{\textsc{FO}}}_{\hat{f}(k,t)}\mathcal{A}_{1}$ implies
$\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 13 then
ensures that $f:k\mapsto\hat{f}(k,\Theta(k))$ fits the bill. Let us now
explain how the function $\Theta$ is chosen.

####  5.2.2. Frequency of a neighbourhood type

Let us write $N_{k}^{d}:=|\textsc{NeighType}_{k}^{d}|$, the number of types of
$k$-neighbourhoods possibly appearing in structures of $\mathdutchcal{C}$
(which have degree at most $d$).

In this section, we show that if we consider the set
$\textsc{Freq}[\mathcal{A}]_{k}$ of $k$-neighbourhood types that have enough
occurrences in some $\mathcal{A}\in\mathdutchcal{C}$ (where “enough” will be
given a precise meaning later on), each type in
$\textsc{Freq}[\mathcal{A}]_{k}$ must 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 $k$-neighbourhood type
not in $\textsc{Freq}[\mathcal{A}]_{k}$, which by definition have few
occurrences in $\mathcal{A}$. At first sight, such a distinction (which will
be formalized later on) between rare neighbourhood types and frequent
neighbourhood types appears to be circular. However, because the degree is
bounded, $N_{k}^{d}$ is bounded too, which allows this definition to be well-
founded.

Such a dichotomy was introduced in [Gra21]; we simply accommodate this
construction to our needs. In the remainder of this section, we recall and
adapt this construction.

The following lemma, which heavily relies on the degree boundedness
assumption, states that, when given a small set $B$ and a bounded number of
large enough sets $C_{1},\ldots,C_{n}$, it is always possible to find many
elements in each $C_{j}$ which are far apart from one another, as well as far
from $B$. It is a strengthening of [NDM10, Lemma 3.2]).

######  Lemma 14.

Given three integers $m$, $\delta$, $s$, there exists a threshold
$g(m,\delta,s)\in\mathbb{N}$ such that for all
$\mathcal{A}\in\mathdutchcal{C}$, all $B\subseteq A$ of size at most $s$, and
all subsets $C_{1},\ldots,C_{n}\subseteq A$ (with $n\leq N_{k}^{d}$) of size
at least $g(m,\delta,s)$, it is possible to find elements
$c_{j}^{1},\ldots,c_{j}^{m}\in C_{j}$ for all $j\in\\{1,\ldots,n\\}$, such
that for all $j,j^{\prime}\in\\{1,\ldots,n\\}$ and
$i,i^{\prime}\in\\{1,\ldots,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})$.

Furthermore, such a function $g$ can be chosen such that

  * •

for all integers $m,\delta,s$, $g(m,\delta,s)\geq s$, and

  * •

$g$ is non-decreasing in its third argument, i.e. for every integers
$m,\delta,s,s^{\prime}$ such that $s\leq s^{\prime}$, $g(m,\delta,s)\leq
g(m,\delta,s^{\prime})$.

######  Proof 5.1.

Let us fix $m,\delta,s\in\mathbb{N}$ and $\mathcal{A}\in\mathdutchcal{C}$,
which has degree at most $d$ by assumption.

Let us start by proving that for any $p\in\mathbb{N}$ and sets of elements
$X,Y\subseteq A$ such that $|X|\leq p$ and $|Y|\geq(p+m)(d^{\delta}+1)$, there
exists elements $y^{1},\ldots,y^{m}\in Y$ such that for all
$i,i^{\prime}\in\\{1,\ldots,m\\}$, $\text{dist}_{\mathcal{A}}(y^{i},Y)>\delta$
and $\text{dist}_{\mathcal{A}}(y^{i},y^{i^{\prime}})>\delta$ if $i\neq
i^{\prime}$.

Let us consider the $\delta$-th power $\mathcal{G}_{\mathcal{A}}^{\delta}$ of
the Gaifman graph of $\mathcal{A}$, where there is an edge between two
elements if their distance in $\mathcal{G}_{\mathcal{A}}$ is at most $\delta$.
The degree of $\mathcal{G}_{\mathcal{A}}^{\delta}$ can be coarsely bounded by
$d^{\delta}$. Thus, there are at most $p(d^{\delta}+1)$ elements in or
adjacent to $X$ in $\mathcal{G}_{\mathcal{A}}^{\delta}$, and at least
$m(d^{\delta}+1)$ elements in $Y\setminus(X\cup
N_{\mathcal{G}_{\mathcal{A}}^{\delta}}(X))$. Consider an arbitrary
$(d^{\delta}+1)$-coloring of $\mathcal{G}_{\mathcal{A}}^{\delta}$, which is
guaranteed to exist since the degree of $\mathcal{G}_{\mathcal{A}}^{\delta}$
is at most $d^{\delta}$. By the pigeonhole principle, one can find $m$
elements $y^{1},\ldots,y^{m}$ in $Y\setminus(X\cup
N_{\mathcal{G}_{\mathcal{A}}^{\delta}}(X))$ with the same color. Since these
elements do not belong to $X\cup N_{\mathcal{G}_{\mathcal{A}}^{\delta}}(X)$,
they are at distance at least $\delta+1$ from $X$ in
$\mathcal{G}_{\mathcal{A}}$. Furthermore, they form an independent set in
$\mathcal{G}_{\mathcal{A}}^{\delta}$ (by definition of a coloring), and are
thus at distance at least $(\delta+1)$ from one another in
$\mathcal{G}_{\mathcal{A}}$. This proves the claim.

We are now ready to prove the lemma: let $B$ be a subset of $A$ of size at
most $s$. Define $g_{n}(m,\delta,s):=(s+nm)(d^{\delta}+1)$. We show by
induction on $n$ that for every $C_{1},\ldots,C_{n}\subseteq A$ of size at
least $g_{n}(m,\delta,s)$, one can find elements $c_{j}^{i}\in C_{j}$, for
$j\in\\{1,\ldots,n\\}$ and $i\in\\{1,\ldots,m\\}$, which are at distance at
least $\delta+1$ from each other and from $B$ in $\mathcal{G}_{\mathcal{A}}$.
For $n=0$, there is nothing to show. For the inductive step from $n$ to $n+1$:
since $g_{n+1}(m,\delta,s)\geq g_{n}(m,\delta,s)$, we start by using the
induction hypothesis to get suiting elements $c_{j}^{i}\in C_{j}$ for
$j\in\\{1,\ldots,n\\}$ and $i\in\\{1,\ldots,m\\}$. We can then rely on the
previous claim with
$X:=B\cup\bigcup_{j=1}^{n}\\{c_{j}^{1},\ldots,c_{j}^{m}\\}$ ($p=s+nm$) and
$Y:=C_{n+1}$ (which, by choice of $g_{n+1}(m,\delta,s)$, satisfy the
cardinality condition of the claim), and pick the $y^{1},\ldots,y^{m}$ as our
$c^{1}_{n+1},\ldots,c^{m}_{n+1}$.

Setting $g(m,\delta,s):=g_{N_{k}^{d}}(m,\delta,s)$ concludes the proof: it is
routine to check that such a function $g$ satisfies the last two properties of
the lemma.

We now explain how to use the Lemma 14 in order to define the notion of
$k$-neighborhood frequency in a structure $\mathcal{A}$. For that, let us fix
$k\in\mathbb{N}$, and define

$M_{k}^{d}:=\max\\{|\tau|:\tau\in\textsc{NeighType}_{k}^{d}\\}\,.$ (2)

Note that $M_{k}^{d}$ can be bounded by a function of $k$ (recall that the
signature $\Sigma$ and the degree $d$ are fixed). Let us consider

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

Our goal is, given a structure $\mathcal{A}\in\mathdutchcal{C}$, to partition
the $k$-neighbourhood types into two categories: the frequent types, and the
rare types. The property we wish to enforce is that there exist in
$\mathcal{A}$ at least $m$ of occurrences of each one of the frequent
$k$-neighbourhood types which are both

  * •

at distance greater than $\delta$ from one another, and

  * •

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

To establish this property, we would like to use Lemma 14, with $s$ being the
total number of occurrences of all the rare $k$-neighbourhood types, and
$C_{1},\ldots,C_{n}$ being the sets of occurrences of the $n$ distinct
frequent $k$-neighbourhood types (obviously satisfying $n\leq N_{k}^{d}$).

The number $N_{k}^{d}$ of different $k$-neighbourhood 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$-neighbourhood 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 14) where $s$ is the total number of occurrences of all the
$k$-neighbourhood 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$-neighbourhood type.

Notice that we can go at most $N_{k}^{d}$ times through step 2, where
$N_{k}^{d}$ depends only on $k$. Furthermore, each time we add a type to the
set of rare $k$-neighbourhood types, we have the guarantee that this type has
few occurrences (namely, less than $g(m,\delta,s)$, where $s$ is the number of
occurrences of the $k$-neighbourhood types that were previously marked as
rare, and thus can be bounded by a function of $k$).

One of two things must occur: either the algorithm stops before all
neighbourhood types are marked as rare, or it doesn’t. In both cases, the
number of occurrences of all rare types can be controlled by a function of
$k$: the threshold $t$ such that a $k$-neighbourhood type $\tau$ is frequent
in $\mathcal{A}$ iff $|\mathcal{A}|_{\tau}\geq t$ can be bounded by some
$\Theta(k)$ depending only on $k$ (on top of $\Sigma$ and $d$) – importantly,
$\Theta(k)$ is the same for all structures of $\mathdutchcal{C}$.

Let us now make the above more formal. For $t\in\mathbb{N}$ and
$\mathcal{A}\in\mathdutchcal{C}$, let $\textsc{Freq}[\mathcal{A}]_{k}^{\geq
t}\subseteq\textsc{NeighType}_{k}^{d}$ denote the set of $k$-neighbourhood
types which have at least $t$ occurrences in $\mathcal{A}$. By applying the
procedure presented above, we derive the following lemma:

######  Lemma 15.

Let $k\in\mathbb{N}$ and define $m$ and $\delta$ as in Equation (3). There
exists $\Theta(k)\in\mathbb{N}$ such that for every
$\mathcal{A}\in\mathdutchcal{C}$, there exists some $t\leq\Theta(k)$ such that

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

######  Proof 5.2.

Define by induction $h_{1}(k):=0$ and
$h_{i+1}(k):=h_{i}(k)+g(m,\delta,h_{i}(k))$. This is well defined, as $m$ and
$\delta$ depend only on $k$. We now show that the lemma holds for

$\Theta(k):=g(m,\delta,h_{N_{k}^{d}+1}(k))+1\,.$

Fix some structure $\mathcal{A}\in\mathdutchcal{C}$ and let
$\tau_{1},\ldots,\tau_{N_{k}^{d}}$ be an enumeration of
$\textsc{NeighType}_{k}^{d}$ such that for $i<j$,
$|\mathcal{A}|_{\tau_{i}}\leq|\mathcal{A}|_{\tau_{j}}$.

Consider the algorithm described in Procedure 2. The set $X$, which is empty
at first, will eventually contain all types that will be declared rare.

1

2$X\leftarrow\emptyset$

3$i\leftarrow 1$

4while $i\leq N_{k}^{d}$ and $|\mathcal{A}|_{\tau_{i}}\leq
g(m,\delta,\sum_{\tau\in X}|\mathcal{A}|_{\tau})$

5 $X\leftarrow X\cup\\{\tau_{i}\\}$

6 $i$++

end

Procedure 2 Separation between rare and frequent neighborhood types

Let us establish the following invariant for the “while” loop:

$\sum_{\tau\in X}|\mathcal{A}|_{\tau}\leq h_{i}(k)$ (4)

Before the first execution of the body of the loop, both sides of Equation (4)
are zero. Suppose now that Equation (4) is true for some $i\leq N_{k}^{d}$ at
the start of the loop, and let us prove that Equation (4) still holds after
executing the body of the loop. We went from $i$ to $i+1$. Let $X_{i}$ denote
the old value of $X$, and $X_{i+1}$ its new value; in other words,
$X_{i+1}=X_{i}\cup\\{\tau_{i}\\}$. The left part of Equation (4) has been
augmented by $|\mathcal{A}|_{\tau_{i}}$, which, because the “while” condition
was satisfied, is less than $g(m,\delta,\sum_{\tau\in
X_{i}}|\mathcal{A}|_{\tau})$. Thus,

$\sum_{\tau\in X_{i+1}}|\mathcal{A}|_{\tau}\leq\sum_{\tau\in
X_{i}}|\mathcal{A}|_{\tau}+g\Bigg{(}m,\delta,\sum_{\tau\in
X_{i}}|\mathcal{A}|_{\tau}\Bigg{)}\,.$

By assumption, $\sum_{\tau\in X_{i}}|\mathcal{A}|_{\tau}\leq h_{i}(k)$, and
since $g$ is non-decreasing in its third variable, we get $\sum_{\tau\in
X_{i+1}}|\mathcal{A}|_{\tau}\leq h_{i+1}(k)$, which means that Equation (4) is
preserved by the body of the loop.

Let us now look at the two ways we can exit the “while” loop, and prove that
the statement of the lemma holds whichever the case:

  * •

If we exit the loop because the condition “$i\leq N_{k}^{d}$” is false, then
we have $i=N_{k}^{d}+1$ and $X=\textsc{NeighType}_{k}^{d}$. By Equation (4),
$\sum_{\tau\in\textsc{NeighType}_{k}^{d}}|\mathcal{A}|_{\tau}\leq
h_{N_{k}^{d}+1}(k)$, and we can choose $t:=g(m,\delta,h_{N_{k}^{d}+1}(k))$. We
then indeed get $t\leq\Theta(k)$ and, because $g$ is non-decreasing in its
third argument,

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

  * •

Otherwise, $i\leq N_{k}^{d}$ and it is “$|\mathcal{A}|_{\tau_{i}}\leq
g(m,\delta,\sum_{\tau\in X}|\mathcal{A}|_{\tau})$” which fails. We can then
choose $t:=g(m,\delta,\sum_{\tau\in X}|\mathcal{A}|_{\tau})+1$ (which is,
again, smaller than $\Theta(k)$). Let us prove that $X$ is exactly the set of
$k$-neighbourhood types that have less than $t$ occurrences in $\mathcal{A}$.
For $\tau\in X$, we have $|\mathcal{A}|_{\tau}\leq\sum_{\tau^{\prime}\in
X}|\mathcal{A}|_{\tau^{\prime}}\leq g(m,\delta,\sum_{\tau^{\prime}\in
X}|\mathcal{A}|_{\tau^{\prime}})<t$ (the second inequality follows from the
good properties of $g$). Conversely, if $\tau\notin X$, it means that
$|\mathcal{A}|_{\tau}\geq|\mathcal{A}|_{\tau_{i}}$ (recall that the $\tau_{i}$
are examined in number of occurrences in $\mathcal{A}$), which in turn is at
least $t$.

Then we have

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

We are now ready to formally establish the notion of frequent type:

Fix an integer $k$ and a structure $\mathcal{A}\in\mathdutchcal{C}$, and let
$\textsc{Freq}[\mathcal{A}]_{k}:=\textsc{Freq}[\mathcal{A}]_{k}^{\geq t}$ for
the smallest threshold $t\leq\Theta(k)$ such that

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

whose existence is guaranteed by Lemma 15. Some $k$-neighbourhood type
$\tau\in\textsc{NeighType}_{k}^{d}$ is said to be _frequent in $\mathcal{A}$_
if it belongs to $\textsc{Freq}[\mathcal{A}]_{k}$; that is, if
$|\mathcal{A}|_{\tau}\geq t$. Otherwise, $\tau$ is said to be _rare in
$\mathcal{A}$_.

Recall how $m$ and $\delta$ were defined in Equation (3). Combining Lemmas
14–15, we get:

######  Proposition 16.

Let $k\in\mathbb{N}$. In every structure $\mathcal{A}\in\mathdutchcal{C}$, one
can find $2(k+1)\cdot M_{k}^{d}!$ occurrences of each frequent
$k$-neighbourhood type in $\mathcal{A}$ which are at distance at least $4k+1$
from one another and from the set of occurrences of every rare
$k$-neighbourhood type in $\mathcal{A}$.

With these notions of frequent and rare neighbourhood types established, we
now turn to the construction of the two linear orders.

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

Recall that our goal is to find a function $f$ such that, given two structures
$\mathcal{A}_{0}$, $\mathcal{A}_{1}$ in $\mathdutchcal{C}$ such that
$\mathcal{A}_{0}\equiv^{{\textsc{FO}}}_{f(k)}\mathcal{A}_{1}$, 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 define $f$ and we detail the construction of such orders.
The proof of FO-similarity between $(\mathcal{A}_{0},<_{0})$ and
$(\mathcal{A}_{1},<_{1})$ will be the focus of Section 5.4.

For every integer $k$, we choose an $f(k)$ large enough so that

  * •

for every structures $\mathcal{A}_{0},\mathcal{A}_{1}\in\mathdutchcal{C}$,
$\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}$,
where $\Theta(k)$ is defined in Lemma 15 (see the discussion after Proposition
13),

  * •

$f(k)\geq\Theta(k)\cdot N_{k}^{d}+1$,

  * •

$f$ satisfies an additional lower bound made explicit later in this section,
in the paragraph _Transfer on $\mathcal{A}_{1}$_ below.

In what follows, we fix an integer $k\in\mathbb{N}$, as well as two structures
$\mathcal{A}_{0}$ and $\mathcal{A}_{1}$ of $\mathdutchcal{C}$ such that

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

for such a choice of $f$.

Let us remark already that by choice of $f$, we get
$\llbracket\mathcal{A}_{0}\rrbracket_{k}=^{\Theta(k)}\llbracket\mathcal{A}_{1}\rrbracket_{k}$
and Lemma 15 ensures that
$\textsc{Freq}[\mathcal{A}_{0}]_{k}=\textsc{Freq}[\mathcal{A}_{1}]_{k}$. In
other words, the notion of frequent and rare $k$-neighbourhood types coincide
on $\mathcal{A}_{0}$ and $\mathcal{A}_{1}$. From this point on, we thus refer
to _frequent_ and _rare_ $k$-neighbourhood types without mentioning the
structure involved.

Furthermore, if $\textsc{Freq}[\mathcal{A}_{0}]_{k}$ (and thus
$\textsc{Freq}[\mathcal{A}_{1}]_{k}$) is empty, then by Definition 5.2.2, each
$\tau\in\textsc{NeighType}_{k}^{d}$ has at most $\Theta(k)$ occurrences, and
$|\mathcal{A}_{0}|\leq\Theta(k)\cdot N_{k}^{d}$. As we chose
$f(k)\geq\Theta(k)\cdot N_{k}^{d}+1$, (5) entails 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 thus suppose that
there is at least one frequent $k$-neighbourhood type.

To construct the two linear orders, we need to define the notion of
$k$-environment: given $\mathcal{A}\in\mathdutchcal{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$-neighbourhood 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$-neighbourhood type is
$\tau$.

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

$A_{i}=X_{i}\uplus\biguplus_{j=0}^{2k}(L_{i}^{j}\uplus R_{i}^{j})\uplus
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}\,.$

Formally, we define the auxiliary order $\prec_{i}$ on the segments by

$X_{i}\prec_{i}L_{i}^{0}\prec_{i}L_{i}^{1}\prec_{i}\cdots\prec_{i}L_{i}^{2k}\prec_{i}M_{i}\prec_{i}R_{i}^{2k}\prec_{i}\cdots\prec_{i}R_{i}^{1}\prec_{i}R_{i}^{0}\,,$

and for $x,y\in A_{i}$, we let $x<_{i}y$ either if $x$’s segment is smaller
than $y$’s segment according to $\prec_{i}$, or if both belong to the same
segment and $x$ is less than $y$ according to the order for this segment.

Each segment $L_{i}^{j}$, for $j\in\\{0,\ldots,2k\\}$, is itself decomposed
into two segments $N\\!L_{i}^{j}$ and $U\\!L_{i}^{j}$, and the order on
$L_{i}^{j}$ will be defined as the concatenation of the order on
$N\\!L_{i}^{j}$ with the order on $U\\!L_{i}^{j}$ (meaning that all elements
from $N\\!L_{i}^{j}$ will be smaller than all elements from $U\\!L_{i}^{j}$).
The $U\\!L_{i}^{j}$ for $j\in\\{k+1,\ldots,2k\\}$ will be empty; they are
defined solely in order to keep the notations uniform. The ’N’ stands for
“neighbour” 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}$ (and thus all elements of $U\\!R_{i}^{j}$
will be smaller than all elements of $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,\ldots,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. Elements from two distinct segments can only be adjacent if there is
a black curvy edge between those segments. The order $<_{0}$ grows from the
left to the right.

For every $\tau\in\textsc{Freq}[\mathcal{A}_{0}]_{k}$, let
$\tau_{1},\ldots,\tau_{|\textsc{Env}(\tau)|}$ be an enumeration of
$\textsc{Env}(\tau)$. Recall the definition of $M_{k}^{d}$ in Equation (2): we
have $|\textsc{Env}(\tau)|\leq M_{k}^{d}!$ for every
$\tau\in\textsc{NeighType}_{k}^{d}$.

In particular, Proposition 16 ensures that we are able to pick, for every
$\tau\in\textsc{Freq}[\mathcal{A}_{0}]_{k}$, every
$l\in\\{1,\ldots,|\textsc{Env}(\tau)|\\}$ and every $j\in\\{0,\ldots,k\\}$,
two elements $a[\tau_{l}]_{L}^{j}$ and $a[\tau_{l}]_{R}^{j}$ which have $\tau$
as $k$-neighbourhood 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$-neighbourhood 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$-neighbourhood types, together with their $k$-neighbourhoods. 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 neighbours 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,\ldots,k\\}$, once we have constructed
$L_{0}^{0},\ldots,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}$. 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$-neighbourhood 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,\ldots,2k\\}$, suppose that we have constructed
$L_{0}^{0},\ldots,L_{0}^{j-1}$. The domain of $N\\!L_{0}^{j}$ consists of all
the neighbours (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,\ldots,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$-neighbourhood 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$-neighbourhood in
$\mathcal{A}_{0}$ as we see fit.

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

Let $M_{0}$ contain 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 (5) is large enough so that there
exists a set $S\subseteq A_{1}$ so that
$\mathcal{A}_{0}\mathord{\upharpoonright}_{S_{0}^{2k}\cup
N_{\mathcal{A}_{0}}(S_{0}^{2k})}\simeq\mathcal{A}_{1}\mathord{\upharpoonright}_{S}$.
This is ensured as long as $f(k)\geq|S_{0}^{2k}\cup
N_{\mathcal{A}_{0}}(S_{0}^{2k})|+1$, whose right side can be bounded by a
function of $k$, independent of $\mathcal{A}_{0}$ and $\mathcal{A}_{1}$.
Indeed, all elements of $S_{0}^{2k}\cup N_{\mathcal{A}_{0}}(S_{0}^{2k})$ are
at distance at most $3k+2$ from $X_{0}$ or one of the $a[\tau_{l}]_{*}^{j}$.
Since the number of such elements is bounded by a function of $k$ (remember
that, by Definition 5.2.2, the number of occurrences of each rare neihbourhood
types is at most $\Theta(k)$) and since the degree is at most $d$ (which is
fixed), $|S_{0}^{2k}\cup N_{\mathcal{A}_{0}}(S_{0}^{2k})|$ can be bounded by a
function of $k$.

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

We transfer alongside $\varphi_{0}$ all the segments besides $M_{0}$, with
their order, from $(\mathcal{A}_{0},<_{0})$ to $\mathcal{A}_{1}$, thus
defining $X_{1},N\\!L_{1}^{j},U\\!L_{1}^{j},\ldots$ as the respective images
by $\varphi_{0}$ of $X_{0},N\\!L_{0}^{j},U\\!L_{0}^{j},\ldots$, and we define
$M_{1}$ as the set of remaining elements of $A_{1}$. It remains to define the
restriction of $<_{1}$ on $M_{1}$: this is done in an arbitrary way. Note that
the properties concerning neighbourhood are transferred; all the neighbours 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 17.

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 17 has two immediate consequences:

  * •

The set $X_{1}$ contains the occurrences in $\mathcal{A}_{1}$ of all the rare
$k$-neighbourhood 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$-neighbourhood 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}$.

By virtue of $\varphi_{0}$ being an isomorphism, and because the order $<_{1}$
was constructed on $S^{\prime}$ as the image by $\varphi_{0}$ of $<_{0}$, we
get:

######  Lemma 18.

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))\,.$

###  5.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 19.

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

Recall Theorem 1: in order to prove Proposition 19, we show that the
duplicator wins the $k$-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,\ldots,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})$ ($\mathcal{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})$ ($\mathcal{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})$
($\mathcal{T}_{r}$)

Let us stress that in this context, $p_{0}^{x}$, $p_{0}^{y}$, $p_{1}^{x}$ and
$p_{1}^{y}$ denote the elements of $\mathcal{A}_{0}$ and $\mathcal{A}_{1}$ on
which the pebbles have been played after $k-r$ rounds, and thus depend on $r$.

The first property, $(\mathcal{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 $(\mathcal{E}_{r})$, it states that two corresponding pebbles are
always placed on elements sharing the same $r$-environment type. Once again,
the safety distance decreases with each round that goes.

Finally, $(\mathcal{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
$(\mathcal{T}_{r})$ is satisfied at the beginning of the game, and after each
of the $k$ rounds of the game.

####  5.4.1. Base case: proofs of $(\mathcal{S}_{k})$, $(\mathcal{E}_{k})$ and
$(\mathcal{T}_{k})$

We start by proving $(\mathcal{S}_{k})$, $(\mathcal{E}_{k})$ and
$(\mathcal{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 $(\mathcal{S}_{k})$ holds, while $(\mathcal{E}_{k})$ and
$(\mathcal{T}_{k})$ respectively follow from Lemma 17 and Lemma 18.

####  5.4.2. Strategy for the duplicator

We now describe the duplicator’s strategy to ensure that $(\mathcal{S}_{r})$,
$(\mathcal{E}_{r})$ and $(\mathcal{T}_{r})$ hold no matter how the spoiler
plays.

Suppose that we have $(\mathcal{S}_{r+1})$, $(\mathcal{E}_{r+1})$ and
$(\mathcal{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, to respond to the placement of $p_{i}^{\alpha}$ near the
endpoints by moving $p_{1-i}^{\alpha}$ on $\varphi_{i}(p_{i}^{\alpha})$.

If the duplicator does not respond this way, then the spoiler will be able to
expose the difference between $(\mathcal{A}_{0},<_{0})$ and
$(\mathcal{A}_{1},<_{1})$ in the subsequent moves, by forcing the duplicator
to play closer and closer to the endpoint, which will prove to be impossible
at some point.

On top of that, the occurrences of rare neighbourhood 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 1
below, and is detailed in Section 5.4.3.

  2. (2)

Next, suppose that the spoiler places a pebble, say $p_{0}^{x}$, next (in
$\mathcal{A}_{0}$) to $p_{0}^{y}$, 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 2, and is treated in Section 5.4.4.

  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}$ (such that
$(\mathcal{A}_{0},<_{0})\models p_{0}^{x}<p_{0}^{y}$).

In order to play according to the remarks from items 1 and 2 above, 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$-neighbourhood 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$-neighbourhood 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 3 and 5 (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 4 and 6
below.

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

  1. (1)

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 item 1 above.

  2. (2)

Else, if $p_{0}^{x}\notin S_{0}^{r}$, and $p_{0}^{x}\in
N_{\mathcal{A}_{0}}^{1}(p_{0}^{y})$, then $(\mathcal{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 item 2 above.

  3. (3)

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. (4)

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 $(\mathcal{S}_{r+1})$, $p_{0}^{x}$ indeed belongs
to the domain of $\varphi_{0}$).

  5. (5)

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 3.

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. (6)

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 4.

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

It remains to show that this strategy satisfies our invariants: under the
inductive assumption that $(\mathcal{S}_{r+1})$, $(\mathcal{E}_{r+1})$ and
$(\mathcal{T}_{r+1})$ hold, for some $0\leq r<k$, we need to show that this
strategy ensures that $(\mathcal{S}_{r})$, $(\mathcal{E}_{r})$ and
$(\mathcal{T}_{r})$ hold.

We treat each case in its own section: Section 5.4.3 is devoted to Case 1
while Section 5.4.4 covers Case 2. Both Cases 3 and 4 are treated in Section
5.4.5. Cases 5 and 6, being their exact symmetric counterparts, are left to
the reader.

######  Remark 20.

Note that some properties need no verification. Since $p_{0}^{y}$ and
$p_{1}^{y}$ are left untouched by the players, $(\mathcal{S}_{r+1})$ ensures
that half of $(\mathcal{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 $(\mathcal{E}_{r})$ concerning $p_{0}^{y}$ and
$p_{1}^{y}$ follows from $(\mathcal{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 $(\mathcal{E}_{r})$ holds, it
follows that
$\text{tp}_{\mathcal{A}_{0}}^{0}(p_{0}^{x})=\text{tp}_{\mathcal{A}_{1}}^{0}(p_{1}^{x})$
and
$\text{tp}_{\mathcal{A}_{0}}^{0}(p_{0}^{y})=\text{tp}_{\mathcal{A}_{1}}^{0}(p_{1}^{y})$.
This remark will help us prove $(\mathcal{T}_{r})$.

####  5.4.3. When the spoiler plays near the endpoints: Case 1

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 1, 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 $(\mathcal{S}_{r})$,
$(\mathcal{E}_{r})$ and $(\mathcal{T}_{r})$ hold. Recall from Remark 20 that
part of the task is already taken care of.

##### Proof of $(\mathcal{S}_{r})$ in Case 1

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 $(\mathcal{E}_{r})$ in Case 1

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 17 given that $p_{1}^{x}=\varphi_{0}(p_{0}^{x})$ and $r<k$.

##### Proof of $(\mathcal{T}_{r})$ in Case 1

First, suppose that $p_{0}^{y}\in S_{0}^{r+1}$. By $(\mathcal{S}_{r+1})$, we
know that $p_{1}^{y}=\varphi_{0}(p_{0}^{y})$. Thus, Lemma 18 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 $(\mathcal{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})$
(6)
$\displaystyle\text{tp}_{<_{0}}^{0}(p_{0}^{x},p_{0}^{y})=\text{tp}_{<_{1}}^{0}(p_{1}^{x},p_{1}^{y})$
(7)

By construction, the neighbours in $\mathcal{A}_{i}$ of an element of
$S_{i}^{r}$ all belong to $S_{i}^{r+1}$, thus $p_{0}^{x}$ and $p_{0}^{y}$
never appear in the same tuple of some relation, and neither do $p_{1}^{x}$
and $p_{1}^{y}$. In other words, the only (positive) atoms that hold in
$\mathcal{A}_{0}$ (resp. $\mathcal{A}_{1}$) about $p_{0}^{x}$ and $p_{1}^{y}$
(resp. $p_{1}^{x}$ and $p_{1}^{y}$) concern independently $p_{0}^{x}$ (resp.
$p_{1}^{x}$) and $p_{0}^{y}$ (resp. $p_{1}^{y}$). Equation (6) follows from
this fact together with
$\text{tp}_{\mathcal{A}_{0}}^{0}(p_{0}^{x})=\text{tp}_{\mathcal{A}_{1}}^{0}(p_{1}^{x})$
and
$\text{tp}_{\mathcal{A}_{0}}^{0}(p_{0}^{y})=\text{tp}_{\mathcal{A}_{1}}^{0}(p_{1}^{y})$
(Remark 20).

As for Equation (7), 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})$ and
$\text{tp}_{<_{1}}^{0}(p_{1}^{x},p_{1}^{y})$ both contain the atom “$x<y$” (as
$p_{0}^{x}$ and $p_{1}^{x}$ appear in segments to the left of the segments
containing $p_{0}^{y}$ and $p_{1}^{y}$, respectively) and are thus equal, 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})$ and
$\text{tp}_{<_{1}}^{0}(p_{1}^{x},p_{1}^{y})$ both contain the atom “$x>y$”,
and are still equal.

####  5.4.4. When the spoiler plays next to the other pebble: Case 2

Suppose now that the spoiler places $p_{0}^{x}$ next to the other pebble in
$\mathcal{A}_{0}$ ($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 1). 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 $(\mathcal{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
$(\mathcal{S}_{r})$, $(\mathcal{E}_{r})$ and $(\mathcal{T}_{r})$.

##### Proof of $(\mathcal{S}_{r})$ in Case 2

Because the spoiler’s move does not fall under Case 1, we know that
$p_{0}^{x}\notin S_{0}^{r}$. Let us now show that $p_{1}^{x}$ is not near the
endpoints either, that $p_{1}^{x}\notin S_{1}^{r}$.

We consider two cases, depending on whether $p_{1}^{y}\in S_{1}^{r+1}$. Since
$p_{1}^{x}$ and $p_{1}^{y}$ are neighbours in $\mathcal{A}_{1}$, if
$p_{1}^{y}\notin S_{1}^{r+1}$, then by construction $p_{1}^{x}\notin
S_{1}^{r}$. Otherwise, $p_{1}^{y}\in S_{1}^{r+1}$ and we know by
$(\mathcal{S}_{r+1})$ that $p_{0}^{y}=\varphi_{1}(p_{1}^{y})$. 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_{0}^{x}\notin S_{0}^{r}$ then entails $p_{1}^{x}\notin
S_{1}^{r}$.

Since we neither have $p_{0}^{x}\in S_{0}^{r}$ nor $p_{1}^{x}\in S_{1}^{r}$,
$(\mathcal{S}_{r})$ holds – recall from Remark 20 that the part concerning
$p_{0}^{y}$ and $p_{1}^{y}$ is always satisfied.

##### Proof of $(\mathcal{E}_{r})$ in Case 2

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
$(\mathcal{E}_{r})$.

##### Proof of $(\mathcal{T}_{r})$ in Case 2

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.

####  5.4.5. When the spoiler plays to the left: Cases 3 and 4

We now treat our last case, which covers both Cases 3 and 4, 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 1 and 2.

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$-neighbourhood 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 (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 neighbours in $\mathcal{A}_{1}$,
which, together with the fact that $p_{0}^{x}$ and $p_{0}^{y}$ are not
neighbours in $\mathcal{A}_{0}$, would break $(\mathcal{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 3.

  * •

if $p_{1}^{y}\in L_{1}^{r+1}$, then $(\mathcal{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 4.

Let us prove that $(\mathcal{S}_{r})$, $(\mathcal{E}_{r})$ and
$(\mathcal{T}_{r})$ hold in both of these instances.

##### Proof of $(\mathcal{S}_{r})$ in Case 3

Since the spoiler’s move does not fall under Case 1, 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 $(\mathcal{E}_{r})$ in Case 3

It follows from $\text{env-
tp}_{(\mathcal{A}_{0},<_{0})}^{k}(a[\tau_{l}]_{L}^{r+1})=\tau_{l}$ together
with Lemma 17 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 $(\mathcal{T}_{r})$ in Case 3

Because the spoiler’s move does not fall under Case 2, $p_{0}^{x}\notin
N_{\mathcal{A}_{0}}^{1}(p_{0}^{y})$. In other words, the (positive) atoms
occurring in $\text{tp}_{\mathcal{A}_{0}}^{0}(p_{0}^{x},p_{0}^{y})$ are
exactly those appearing in $\text{tp}_{\mathcal{A}_{0}}^{0}(p_{0}^{x})$ and
$\text{tp}_{\mathcal{A}_{0}}^{0}(p_{0}^{y})$, as no atom involving both
$p_{0}^{x}$ and $p_{0}^{y}$ holds.

Recall the construction of $U\\!L_{0}^{r+1}$: the whole $k$-neighbourhood 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 the atoms in
$\text{tp}_{\mathcal{A}_{1}}^{0}(p_{1}^{x},p_{1}^{y})$ are those occurring in
$\text{tp}_{\mathcal{A}_{1}}^{0}(p_{1}^{x})$ and
$\text{tp}_{\mathcal{A}_{1}}^{0}(p_{1}^{y})$. It then follows from the last
observation of Remark 20 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})$ contains
the atom “$x<y$”. We claim that $p_{1}^{y}\notin X_{1}\cup\bigcup_{0\leq j\leq
r+1}L_{1}^{j}$. Suppose otherwise: $(\mathcal{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 assumption $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. Both
$\text{tp}_{<_{1}}^{0}(p_{1}^{x},p_{1}^{y})$ and
$\text{tp}_{<_{0}}^{0}(p_{0}^{x},p_{0}^{y})$ contain the atom “$x<y$” and thus
must be equal, which concludes the proof of $(\mathcal{T}_{r})$.

##### Proof of $(\mathcal{S}_{r})$, $(\mathcal{E}_{r})$ and
$(\mathcal{T}_{r})$ in Case 4

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 $(\mathcal{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
$(\mathcal{E}_{r})$ and $(\mathcal{T}_{r})$, they follow readily from Lemmas
17 and 18 and the fact that $p_{1}^{x}=\varphi_{0}(p_{0}^{x})$ and
$p_{1}^{y}=\varphi_{0}(p_{0}^{y})$.

###  5.5. Counting quantifiers

We now consider the natural 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 (meaning that
contrary to $\textsc{FO}^{2}$, there exist satisfiable
$\textsc{C}^{2}$-sentences which do not have small, or even finite, models).
However, the satisfiability problem for $\textsc{C}^{2}$ is still decidable
[GOR97, Pra07, Pra10]. 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 12 can be adapted to show the following stronger
version:

######  Theorem 21.

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

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

######  Proof 5.3.

The proof is very similar as to that of Theorem 12. 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}$ [IL90]. 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 game 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 cardinality of the set chosen by the spoiler
(which is at most $k$) indeed corresponds to the fact that the counting
indexes of the formulae 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 [IL90], and is left to the reader.

Let us now explain how to modify the construction of $<_{0}$ and $<_{1}$
presented in Section 5.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$-neighbourhood
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$-neighbourhood 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 Equation (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 5.4.2. 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 5.4.2, they will
never answer two moves by the spoiler falling under different cases among
Cases 1-6 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 aforementioned strategy.

  * •

For Case 1, this is straightforward, since the strategy is based on the
isomorphism between the borders of the linear orders. The same goes for Cases
2, 4 and 6, 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 3.
Recall that our new construction guarantees, for each $k$-environment type
extending a frequent $k$-neighbourhood 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 5 is obviously symmetric.

This concludes the proof of Theorem 21.

##  6\. Conclusion

In this paper, we made significant progress towards a better understanding of
the two-variable fragment of order-invariant first-order logic:

  * •

From a complexity point of view, we established the coNExpTime-completeness of
the problem of deciding if a given $\textsc{FO}^{2}$-sentence is order-
invariant (Theorem 7), significantly simplifying and improving the result by
Zeume and Harwath [ZH16, Thm. 12].

  * •

From an expressivity point of view, we addressed the question of whether every
property definable in order-invariant $\textsc{FO}^{2}$ can also be expressed
in plain FO. We failed short of fully answering the question, but provided two
interesting results. The first one (namely, Theorem 11) establishes that under
a more relaxed notion of order-invariance, the answer to the above question is
“no”. While this does not bring a fully-satisfactory answer to the problem,
this leads us to believe that order-invariant $\textsc{FO}^{2}$ can indeed
express properties beyond the scope of FO. The second one (Theorem 12) states
that when the degree is bounded, every property expressible in order-invariant
$\textsc{FO}^{2}$ is definable in FO without the use of the order. This is an
important step towards resolving the conjecture that order-invariant FO over
classes of structures of bounded degree cannot express properties beyond the
reach of FO.

Results of Section 5 also apply to the case of the two-variable logic with
counting, $\textsc{C}^{2}$. While order-invariant $\textsc{C}^{2}$ has
decidable satisfiability and validity problems [CW16, Theorem 6.20], it is
open if it has a decidable syntax (whether the problem of determining if a
given $\textsc{C}^{2}$-sentence is order-invariant is decidable).
Unfortunately the techniques introduced in Section 3 are of no use here, as
$\textsc{C}^{2}$ lacks the finite model property. Finally, it might be a good
idea to study order-invariant $\textsc{FO}^{2}$ over graph classes beyond
classes of bounded-degree, planar graphs or nowhere-dense classes of graphs.

## Acknowledgements

Bartosz Bednarczyk was supported by the ERC Consolidator Grant No. 771779
(DeciGUT). He would like to thank Antti Kuusisto and Anna Karykowska for many
insightful discussions on the problem.

## References

  * [Bed22] Bartosz Bednarczyk.  Order-invariance of two-variable logic is conexptime-complete.  CoRR, 2022.
  * [BL16] Pablo Barceló and Leonid Libkin.  Order-Invariant Types and Their Applications.  Log. Methods Comput. Sci., 12(1), 2016.
  * [CW16] Witold Charatonik and Piotr Witkowski.  Two-variable logic with counting and a linear order.  Log. Methods Comput. Sci., 12(2), 2016.
  * [FSV95] Ronald Fagin, Larry J. Stockmeyer, and Moshe Y. Vardi.  On monadic NP vs. monadic co-NP.  Inf. Comput., 1995.
  * [Für83] Martin Fürer.  The Computational Complexity of the Unconstrained Limited Domino Problem (with Implications for Logical Decision Problems).  Logic and Machines: Decision Problems and Complexity, 1983.
  * [GKV97] Erich Grädel, Phokion G. Kolaitis, and Moshe Y. Vardi.  On the Decision Problem for Two-Variable First-Order Logic.  Bull. Symb. Log., 1997.
  * [GO99] Erich Grädel and Martin Otto.  On Logics with Two Variables.  Theor. Comput. Sci., 224(1-2):73–113, 1999.
  * [GOR97] Erich Grädel, Martin Otto, and Eric Rosen.  Two-variable logic with counting is decidable.  In LICS, 1997.
  * [Gra21] Julien Grange.  Successor-invariant first-order logic on classes of bounded degree.  Log. Methods Comput. Sci., 2021.
  * [Gra23] Julien Grange.  Order-invariance in the two-variable fragment of first-order logic.  In Bartek Klin and Elaine Pimentel, editors, 31st EACSL Annual Conference on Computer Science Logic, CSL 2023, February 13-16, 2023, Warsaw, Poland, volume 252 of LIPIcs, pages 23:1–23:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.
  * [GS00] Martin Grohe and Thomas Schwentick.  Locality of order-invariant first-order formulas.  ACM Trans. Comput. Log., 1(1):112–130, 2000.
  * [IK89] Neil Immerman and Dexter Kozen.  Definability with bounded number of bound variables.  Inf. Comput., 1989.
  * [IL90] Neil Immerman and Eric Lander.  Describing graphs: A first-order approach to graph canonization.  In Complexity theory retrospective. Springer, 1990.
  * [Lib04] Leonid Libkin.  Elements of Finite Model Theory.  Springer, 2004.
  * [NDM10] Jaroslav Nešetřil and Patrice Ossona De Mendez.  First order properties on nowhere dense structures.  The Journal of Symbolic Logic, 2010.
  * [Ott01] Martin Otto.  Two Variable First-Order Logic over Ordered Domains.  J. Symb. Log., 66(2):685–702, 2001.
  * [Pot94] Andreas Potthoff.  Logische Klassifizierung regulärer Baumsprachen.  PhD thesis, Christian-Albrechts-Universität Kiel, 1994.
  * [Pra07] Ian Pratt-Hartmann.  Complexity of the guarded two-variable fragment with counting quantifiers.  J. Log. Comput., 2007.
  * [Pra10] Ian Pratt-Hartmann.  The two-variable fragment with counting revisited.  In WoLLIC, 2010.
  * [Sch13] Nicole Schweikardt.  A Tutorial on Order- and Arb-Invariant Logics.  https://www.irif.fr/~steiner/jifp/schweikardt.pdf, 2013.
  * [Tra50] Boris A Trakhtenbrot.  Impossibility of an Algorithm for the Decision Problem for Finite Classes.  In Doklady Akademiia Nauk SSSR, volume 70, page 569, 1950.
  * [Tur38] Alan Mathison Turing.  On computable numbers, with an application to the Entscheidungsproblem. A correction.  Proceedings of the London Mathematical Society, 2(1):544–546, 1938\.
  * [ZH16] Thomas Zeume and Frederik Harwath.  Order-Invariance of Two-Variable Logic is Decidable.  LICS, 2016.