17320 LABEL:LastPageSep. 25, 2020Aug. 13, 2021

# Successor-Invariant First-Order Logic on Classes of Bounded Degree

Julien Grange  ENS Paris, PSL, INRIA, CNRS<EMAIL_ADDRESS>
###### Abstract.

We study the expressive power of successor-invariant first-order logic, which
is an extension of first-order logic where the usage of an additional
successor relation on the structure is allowed, as long as the validity of
formulas is independent of the choice of a particular successor on finite
structures.

We show that when the degree is bounded, successor-invariant first-order logic
is no more expressive than first-order logic.

##  1\. Introduction

First-order logic, FO, is the standard formalism to express properties of
finite structures. Its expressive power is well known, and very restrained, as
it can only express properties that are local, which roughly means that it can
only talk about the immediate surroundings of a small number of elements, and
it is unable to count.

A number of logics with higher expressivity can be defined with FO as a
building block, such as MSO, in which quantification over sets is allowed, and
LFP, which adds a fixpoint operator to FO. These additions break the local
character of the logic.

Another way to define logics from FO is through the addition, in an invariant
way, of arithmetic predicates on the structure that are exterior to the
vocabulary. This amounts to arbitrarily identifying the universe of the
structure with an initial segment of the integers, and allowing some
arithmetic on them. However, we want these extensions to define properties of
the structures, and not to depend on a particular ordering on their elements:
thus we focus on invariant extensions of FO.

If the only predicate allowed is the order, we get order-invariant first-order
logic, $<\\!\textup{-inv }$FO. Restricting a bit the additional relation, we
get successor-invariant first-order, Succ-inv FO. In this formalism, we only
grant access to the successor relation derived from the order, provided that
the evaluation of a sentence using this successor relation is independent of
the choice of a particular successor.

The problem of determining whether an FO-sentence using an order or a
successor relation is invariant wrt. this relation is undecidable, by
reduction from the finite satisfiability problem (cf. Trakhtenbrot’s theorem
[Tra50]). In fact, it is shown in [BS09] that this problem in undecidable even
on strings. Hence we use here the term “logic” somewhat liberally, since
having a recursively enumerable syntax is a usual requirement for a logic.

The study of these two formalisms finds its motivation, among other topics
such as descriptive complexity, in database theory. As databases are commonly
stored on disk that implicitly order their memory segments, when one wishes to
express a query in FO, one has access to an additional order on the elements
of the database. However, making use of this order without care could result
in queries that evaluate differently on two implementations of the same
database, which is clearly an undesirable behavior. We want to use this order
only in an invariant fashion; this way, the result of a query depends only on
the database it is run on, and not on the way the data is stored on disk. This
amounts exactly to the definition of $<\\!\textup{-inv }$FO, or Succ-inv FO if
we restrict the way this order can be accessed.

It is straightforward that $<\\!\textup{-inv }$FO is at least as expressive as
Succ-inv FO, which in turn can express any FO-definable property. Gurevich
constructed a class of finite structures that can be defined by an
$<\\!\textup{-inv }$FO sentence, but which is not FO-definable. Though this
construction was not published by Gurevich, it can be found, e.g., in Section
5.2 of [Lib04]. Rossman extended this result, and proved in [Ros07] that on
finite structures, Succ-inv FO is strictly more expressive than FO.

Grohe and Schwentick [GS00] proved that these logics were Gaifman-local,
giving an upper bound to their expressive power. Other upper bounds were given
by Benedikt and Segoufin [BS09], who proved that $<\\!\textup{-inv }$FO, and
hence Succ-inv FO, are included in MSO on classes of bounded treewidth and on
classes of bounded degree. Elberfeld, Frickenschmidt and Grohe [EFG16]
extended the first inclusion to a broader setting, that of decomposable
structures. Whether these logics are included in MSO in general is still an
open question.

The classes of structures involved in the separating examples by Gurevich and
Rossman are dense, and no other example is known on classes that are sparse.
Far from it, $<\\!\textup{-inv }$FO and _a fortiori_ Succ-inv FO are known to
collapse to FO on several sparse classes. Benedikt and Segoufin [BS09] proved
the collapse on trees; Eickmeyer, Elberfeld and Harwarth [EEH14] obtained an
analogous result on graphs of bounded tree-depth; Grange and Segoufin [GS20]
proved the collapse on hollow trees.

Whether $<\\!\textup{-inv }$FO or Succ-inv FO collapse to FO on classes of
graphs of bounded treewidth (or even bounded pathwidth) are still open
questions. We go in another direction in this paper, and prove that Succ-inv
FO collapses to FO on classes of structures of bounded degree. To do this, we
show how to construct successors on two FO-similar structures of bounded
degree, such that the two structures remain FO-similar when considering the
additional successor relation.

#### Related work:

The general method used in [EEH14] to prove that $<\\!\textup{-inv }$FO
collapses to FO when the tree-depth is bounded is the same as ours: starting
from two FO-similar structures, they show how to construct orders that
maintain the similarity. However, the techniques we use to construct our
successors are nothing like the ones used in [EEH14], as the assumptions on
the classes at hand (bounded tree-depth versus bounded degree) are very
different.

Instead of directly constructing similar orders on two similar structures,
[BS09] and [GS20] exhibit a chain of intermediate structures and intermediate
orders that are pairwise similar, in order to prove the collapse on trees and
hollow trees. Although all these constructions, as well as ours, rely on a
careful manipulation of the neighborhoods, our construction differs widely
from these ones. Indeed, instead of chaining local modifications of the
structures, we construct all at once our successor relations, without
intermediate steps.

The classes of graphs on which the model checking problem for FO (denoted
MC(FO)) is fixed-parameter tractable has been widely studied. It has
originally been proven by Seese [See96] that MC(FO) is fixed-parameter linear
on any class of bounded degree. After a series of improvements on this result,
Grohe, Kreutzer and Siebertz [GKS17] showed that this problem is fixed-
parameter tractable on any nowhere dense class of graphs.

Concerning the model checking problem for Succ-inv FO, Van den Heuvel,
Kreutzer, Pilipczuk, Quiroz, Rabinovich and Siebertz [vdHKP+17] proved that
MC(Succ-inv FO) is fixed-parameter tractable on any class of bounded expansion
(which is less general than the nowhere dense setting, but also includes any
class of bounded degree). Since there is no indication that Succ-inv FO is
more expressive than FO on classes of bounded expansion, this could possibly
be due to a collapse of Succ-inv FO to FO on those classes. Our result showing
that Succ-inv FO collapses to FO on classes of bounded degree, together with
the aforementioned result from [See96], gives an alternative proof of the fact
that MC(Succ-inv FO) is non-uniform fixed-parameter linear when the degree is
bounded.

##  2\. Preliminaries

The remainder in the division of $n\in\mathbb{N}$ by $m>0$ is denoted $n[m]$.

A binary relation on a finite set $X$ is a successor relation on $X$ if it is
the graph of a circular permutation of $X$, i.e. a bijective function from $X$
to $X$ with a single orbit. This differs from the standard notion of successor
in that there is neither minimal nor maximal element. However, this does not
have any impact on our result, as discussed at the end of the present section.

We use the standard definition of first-order logic $\textsc{FO}(\Sigma)$ over
a signature $\Sigma$ composed of relation and constant symbols. We only
consider finite $\Sigma$-structures, which are denoted by calligraphic upper-
case letters, while their universes are denoted by the corresponding standard
upper-case letters; for instance, $A$ is the universe of the structure
$\mathcal{A}$.

[Succ-inv FO ] A sentence $\varphi\in\textsc{FO}(\Sigma\cup\\{S\\})$, where
$S$ is a binary relation symbol, is said to be successor-invariant if for
every $\Sigma$-structure $\mathcal{A}$, and every successor relations $S_{1}$
and $S_{2}$ on $A$, $(\mathcal{A},S_{1})\models\varphi$ iff
$(\mathcal{A},S_{2})\models\varphi$. We can then omit the interpretation for
the symbol $S$, and if $(\mathcal{A},S_{1})\models\varphi$ for any (every)
successor $S_{1}$, we write $\mathcal{A}\models\varphi$.

The set of successor-invariant sentences on $\Sigma$ is denoted $\textup{Succ-
inv }\textsc{FO}(\Sigma)$.

[$\mathcal{L}$-similarity] Given two $\Sigma$-structures $\mathcal{A}$ and
$\mathcal{B}$, and $\mathcal{L}$ being either $\textsc{FO}(\Sigma)$ or
$\textup{Succ-inv }\textsc{FO}(\Sigma)$, we write
$\mathcal{A}\equiv^{\mathcal{L}}_{k}\mathcal{B}$, and say that that
$\mathcal{A}$ and $\mathcal{B}$ are $\mathcal{L}$-similar at depth $k$, if
$\mathcal{A}$ and $\mathcal{B}$ satisfy the same $\mathcal{L}$-sentences of
quantifier rank at most $k$. For $\textsc{FO}(\Sigma)$ as well as for
$\textup{Succ-inv }\textsc{FO}(\Sigma)$, we omit $\Sigma$ when it is clear
from the context.

We write $\mathcal{A}\simeq\mathcal{B}$ if $\mathcal{A}$ and $\mathcal{B}$ are
isomorphic.

[Gaifman graph] The Gaifman graph $\mathcal{G}_{\mathcal{A}}$ of a
$\Sigma$-structure $\mathcal{A}$ is defined as $(A,V)$ where $(x,y)\in V$ iff
$x$ and $y$ are distinct and appear in the same tuple of a relation of
$\mathcal{A}$. In particular, if a graph is seen as a relational structure on
the vocabulary $\\{E\\}$, its Gaifman graph is the unoriented version of
itself. By $\text{dist}_{\mathcal{A}}(x,y)$, we denote the distance between
$x$ and $y$ in $\mathcal{G}_{\mathcal{A}}$. The degree of $\mathcal{A}$ is the
degree of its Gaifman graph, and a class $\mathcal{C}$ of $\Sigma$-structures
is said to be of bounded degree if there exists some $d\in\mathbb{N}$ such
that the degree of every $\mathcal{A}\in\mathcal{C}$ is at most $d$.

[Neighborhood types] Let $c$ be a constant symbol that does not appear in
$\Sigma$.

For $k\in\mathbb{N}$ and $x\in A$, the $k$-neighborhood
$\mathcal{N}_{\mathcal{A}}^{k}(x)$ of $x$ is the
$(\Sigma\cup\\{c\\})$-structure whose $\Sigma$-restriction is the substructure
of $\mathcal{A}$ induced by $\\{y\in A:\text{dist}_{\mathcal{A}}(x,y)\leq
k\\}$, and where $c$ is interpreted as $x$.

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

[Path and cycles] A cycle of length $l\geq 3$ in the
$\Sigma\cup\\{S\\}$-structure $\mathcal{A}$ is a sequence
$(x_{0},\dots,x_{l-1})$ of distinct vertices of $A$ such that for every $0\leq
i<l$, $x_{i}$ and $x_{i+1[l]}$ appear in the same tuple of some relation of
$\mathcal{A}$ (in other words, it is a cycle in $\mathcal{G}_{\mathcal{A}}$).
If furthermore $(x_{i},x_{i+1[l]})\in S$ for every $i$, then we say that it is
an $S$-cycle. If for some $i$, $(x_{i},x_{i+1[l]})\in S$ or
$(x_{i+1[l]},x_{i})\in S$, then we say that the cycle goes through an
$S$-edge. A path is defined similarly, without the requirement on $x_{l-1}$
and $x_{0}$, and its length is $l-1$ instead of $l$.

From now on, we assume that $\Sigma$ is purely relational (i.e. contains only
relation symbols) and does not contain the binary symbol $S$.

For a class $\mathcal{C}$ of $\Sigma$-structures, we say that

$\textup{Succ-inv }\textsc{FO}=\textsc{FO}\text{ on }\mathcal{C}$

if the properties of $\mathcal{C}$ definable in Succ-inv FO and in FO are the
same. In other words, if for every $\varphi\in\textup{Succ-inv }\textsc{FO}$,
there exists some $\bar{\varphi}\in\textsc{FO}$ such that

$\forall\mathcal{A}\in\mathcal{C},\quad\mathcal{A}\models\varphi\quad\text{iff}\quad\mathcal{A}\models\bar{\varphi}\,.$

The reverse inclusion, i.e. $\textsc{FO}\subseteq\textup{Succ-inv
}\textsc{FO}$, always holds and needs no verification.

We are now ready to state our main result:

######  Theorem 1.

For every vocabulary $\Sigma$ and for every class $\mathcal{C}$ of
$\Sigma$-structures of bounded degree,

$\textup{Succ-inv }\textsc{FO}=\textsc{FO}\text{ on }\mathcal{C}\,.$

The proof of Theorem 1 is given in Section 4, and constitutes the core of this
paper. We give here a sketch of this proof; this will motivate the definitions
given in Section 3.

######  Proof 2.1 (Proof overview).

Our goal is, given two structures $\mathcal{G}_{1}$ and $\mathcal{G}_{2}$ of
degree at most $d$ that are FO-similar (that is, such that
$\mathcal{G}_{1}\equiv^{\textsc{FO}}_{n}\mathcal{G}_{2}$ for a large enough
$n$), to construct a successor relation $S_{1}$ on $\mathcal{G}_{1}$ and
$S_{2}$ on $\mathcal{G}_{2}$ such that $(\mathcal{G}_{1},S_{1})$ and
$(\mathcal{G}_{2},S_{2})$ stay FO-similar. We will see that this entails that
$\equiv^{\textsc{FO}}$ refines $\equiv^{{\textup{Succ-inv }\textsc{FO}}}$ when
the degree is bounded. From there, a standard finite-model-theoretic argument
(namely, that $\equiv^{\textsc{FO}}_{n}$ has finite index and that each one of
its classes is FO-definable) gives the inclusion $\textup{Succ-inv
}\textsc{FO}\subseteq\textsc{FO}$ on classes of bounded degree.

It thus remains to construct suitable successor relations $S_{1}$ and $S_{2}$.
First, we separate the neighborhood types occurring in $\mathcal{G}_{1}$ and
$\mathcal{G}_{2}$ into two categories:

  * •

on the one hand, the rare neighborhood types, which have few occurrences in
$\mathcal{G}_{1}$ and $\mathcal{G}_{2}$ (and thus, that have the same number
of occurrences in both structures, by FO-similarity)

  * •

on the other hand, the frequent neighborhood types, which have many
occurrences both in $\mathcal{G}_{1}$ and $\mathcal{G}_{2}$.

In order to make the proof of FO-similarity of $(\mathcal{G}_{1},S_{1})$ and
$(\mathcal{G}_{2},S_{2})$ as simple as possible, we want an element of
$\mathcal{G}_{1}$ and its successor by $S_{1}$ (and similarly for
$\mathcal{G}_{2}$ and $S_{2}$) to have the same neighborhood type in
$\mathcal{G}_{1}$ as much as possible, and to be far away in
$\mathcal{G}_{1}$, in order for the neighborhood types occurring in
$(\mathcal{G}_{1},S_{1})$ to be as “regular” as possible. As long as there are
at least two different neighborhood types, the first constraint obviously
cannot be satisfied, but we will construct $S_{1}$ as close as possible to
satisfying it.

For instance, suppose that $\mathcal{G}_{1}$ contains three frequent
neighborhood types $\tau_{0},\tau_{1}$ and $\tau_{2}$, and one rare
neighborhood type $\chi$ with two occurrences. At the end of the construction,
$S_{1}$ will (mostly) look like in Figure 1, where the relations of
$\mathcal{G}_{1}$ have been omitted and the arrows represent $S_{1}$, which is
indeed a circular successor.

Note that all the elements of neighborhood type $\tau_{1}$ form a segment wrt.
$S_{1}$, as well as all the elements of neighborhood type $\tau_{2}$. The
first frequent neighborhood type, $\tau_{0}$, has a special role in that it is
used to embed all the elements of rare neighborhood type (here, $\chi$).
Furthermore, and this is not apparent in the figure, two successive elements
for $S_{1}$ are always distant in $\mathcal{G}_{1}$.

$\tau_{0}$$\tau_{0}$$\tau_{0}$$\chi$$\chi$$\tau_{1}$$\tau_{2}$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\circledcirc$$\circledcirc$$\circledcirc$$\circledcirc$$\circledcirc$$\circledcirc$
Figure 1. Illustration of $S_{1}$ when there are three frequent neighborhood
types ($\tau_{0}$, $\tau_{1}$, $\tau_{2}$) and one rare neighborhood type
($\chi$) in $\mathcal{G}_{1}$. The elements of rare neighborhood type are
surrounded by occurrences of the first frequent neighborhood type, $\tau_{0}$.
Junction elements are circled.

Keeping this idea in mind, $S_{1}$ (and similarly, $S_{2}$) is constructed
iteratively, by adding $S$-edges to the initial structures one at a time. For
practical reasons, we will start the construction of $S_{1}$ around
occurrences of rare neighborhood types: for each element $x$ of rare
neighborhood type, we find two elements of neighborhood type $\tau_{0}$ that
are far apart in $\mathcal{G}_{1}$, and far from $x$. Then we add two
$S$-edges in order for those two elements to become the $S_{1}$-predecessor
and the $S_{1}$-successor of $x$. We repeat this process for every element of
rare neighborhood type (and actually, for every element that belongs to the
neighborhood of a rare element) until each one is protected by a ball of
elements of frequent neighborhood type. This is possible because there are few
elements of rare neighborhood type, and many elements of any frequent
neighborhood type; since the degree is bounded, those elements of frequent
neighborhood type are spread across the structure, and can be found far from
the current construction.

Once this is done, we apply a similar construction around elements of frequent
neighborhood types that will, in the end, be the $S_{1}$-predecessor or
$S_{1}$-successor of an element of another frequent neighborhood type - that
is, elements that will be at the border of the segments (for $S_{1}$) of a
given frequent neighborhood type. Such elements are circled in Figure 1. We
must choose only a small number of such elements (two for each frequent
neighborhood type, of which there are few due to the degree boundedness
hypothesis), hence we can find enough far-apart elements of frequent
neighborhood type to embed them. Once again, degree boundedness is crucial.

After these two steps, $S_{1}$ has been constructed around all the singular
points. It only remains to complete $S_{1}$ by adding edges between the
remaining elements (all of which are occurrences of frequent neighborhood
types), in such a way that elements of a same frequent neighborhood type end
up forming a segment for $S_{1}$, and such that $S_{1}$ brings together
elements that were far apart in the initial structure $\mathcal{G}_{1}$. Once
again, the high number of occurrences of each frequent neighborhood type
allows us to do so.

Applying the same construction to $\mathcal{G}_{2}$, we end up with two
structures $(\mathcal{G}_{1},S_{1})$ and $(\mathcal{G}_{2},S_{2})$ that cannot
be distinguished by FO-formulas of small (wrt. the initial FO-similarity index
between $\mathcal{G}_{1}$ and $\mathcal{G}_{2}$) quantifier rank, which
concludes the proof.

We have given a global overview of the construction process of $S_{1}$;
however, there are technical difficulties to take care of, which are dealt
with in Section 4. For that, we need the definitions given in Section 3, which
formalize the notion of regularity of a neighborhood type in
$(\mathcal{G}_{1},S_{1})$ and $(\mathcal{G}_{2},S_{2})$.

Let us now prove that our decision to consider circular successors instead of
the more traditional linear ones (with a minimal and a maximal element) bears
no consequence on this result. If we define LinSucc-inv FO in the same way as
Succ-inv FO, but where the invariant relation is a linear successor $\bar{S}$,
we get:

######  Lemma 2.

For every vocabulary $\Sigma$, LinSucc-inv FO and Succ-inv FO define the same
properties of $\Sigma$-structures.

######  Proof 2.2.

Given $\varphi\in\textup{Succ-inv }\textsc{FO}$, let us prove that there
exists a formula $\psi\in\textup{LinSucc-inv }\textsc{FO}$ such that $\psi$ is
equivalent to $\varphi$ (i.e. for every $\Sigma$-structure $\mathcal{A}$,
$\mathcal{A}\models\varphi$ iff $\mathcal{A}\models\psi$).

Let $\psi$ be defined as $\varphi$ in which every atom $S(x,y)$ has been
replaced with the formula $\bar{S}(x,y)\vee\neg\exists
z(\bar{S}(x,z)\vee\bar{S}(z,y))$.

Let $\mathcal{A}$ be a $\Sigma$-structure and $\bar{S}$ be a linear successor
on $A$. Then $(\mathcal{A},\bar{S})\models\psi$ iff
$(\mathcal{A},S)\models\varphi$, where $S$ is the circular successor obtained
from $\bar{S}$ by adding an edge from the maximal element to the minimal one.

This guarantees that $\psi\in\textup{LinSucc-inv }\textsc{FO}$, and that
$\psi$ and $\varphi$ are equivalent.

Conversely, let $\psi\in\textup{LinSucc-inv }\textsc{FO}$ and let $\varphi$ be
the formula $\exists\min\,\text{Cut}(\psi)$, where $\text{Cut}(\psi)$ is
obtained by replacing in $\psi$ every $\bar{S}(x,y)$ with $S(x,y)\wedge\neg
y=\min$.

Let $\mathcal{A}$ be a $\Sigma$-structure, let $S$ be a circular successor on
$A$, and let $\min\in A$. Then $(\mathcal{A},S,\min)\models\text{Cut}(\psi)$
iff $(\mathcal{A},\bar{S})\models\psi$, where $\bar{S}$ is the linear
successor obtained from $S$ by removing the edge pointing to $\min$. Hence
$(\mathcal{A},S)\models\varphi$ iff there exists a linear successor $\bar{S}$
obtained from $S$ by an edge removal such that
$(\mathcal{A},\bar{S})\models\psi$, that is iff $\mathcal{A}\models\psi$.

This ensures that $\varphi\in\textup{Succ-inv }\textsc{FO}$ and that $\varphi$
and $\psi$ are equivalent.

##  3\. Fractal types and layering

To prove Theorem 1, we will start from two structures $\mathcal{G}_{1}$ and
$\mathcal{G}_{2}$ that are FO-similar, and construct successor relations
$S_{1}$ and $S_{2}$ on their universes so that the structures remain FO-
similar when we take into account these additional successor relations.

We want to construct $S_{\epsilon}$, for $\epsilon\in\\{1,2\\}$, in a way that
makes $\text{tp}_{(\mathcal{G}_{\epsilon},S_{\epsilon})}^{k}(a)$ as regular as
possible for every $a\in G_{\epsilon}$, in order to ease the proof of FO-
similarity of $(\mathcal{G}_{1},S_{1})$ and $(\mathcal{G}_{2},S_{2})$.

Ideally, the $S_{\epsilon}$-successors and $S_{\epsilon}$-predecessors of any
element should have the same $k$-neighborhood type in $\mathcal{G}_{\epsilon}$
as this element. On top of that, there should not be any overlap between the
$k$-neighborhoods in $\mathcal{G}_{\epsilon}$ of elements that are brought
closer by $S_{\epsilon}$ (this “independence” is captured by the layering
property, introduced in Definition 2).

Let us now try to visualize what
$\text{tp}_{(\mathcal{G}_{\epsilon},S_{\epsilon})}^{k}(a)$ would look like in
those perfect conditions, for some $a$ of $k$-neighborhood type $\tau$ in
$\mathcal{G}_{\epsilon}$, with Figure 2 as a visual aid.

Let $a^{+}$ be the successor of $a$ by $S_{\epsilon}$: in the $k$-neighborhood
of $a$ in $(\mathcal{G}_{\epsilon},S_{\epsilon})$ appears the
$(k-1)$-neighborhood of $a^{+}$ in $\mathcal{G}_{\epsilon}$. But in these
ideal conditions, we have that
$\text{tp}_{\mathcal{G}_{\epsilon}}^{k}(a^{+})=\text{tp}_{\mathcal{G}_{\epsilon}}^{k}(a)$,
hence in $\text{tp}_{(\mathcal{G}_{\epsilon},S_{\epsilon})}^{k}(a)$, we see
that the pattern $\text{tp}_{\mathcal{G}_{\epsilon}}^{k}(a)$ is repeated
around the $S_{\epsilon}$-successor of $a$, with a radius shrunk by one. If we
follow again $S_{\epsilon}$, the same neighborhood type will appear once more,
this time with radius $k-2$, and so on.

Let us now take a step sideways in the $k$-neighborhood of $a$ in
$\mathcal{G}_{\epsilon}$ (i.e. in the horizontal plane in the figure), and
consider some element $x$ at distance $d$ from $a$ in
$\mathcal{G}_{\epsilon}$. In these perfect conditions, $x$ and its
$S_{\epsilon}$-successor have the same $k$-neighborhood type in
$\mathcal{G}_{\epsilon}$. Of course, only a part of these neighborhoods will
appear in the $k$ neighborhood of $a$ in
$(\mathcal{G}_{\epsilon},S_{\epsilon})$; namely, the $(k-d)$-neighborhood of
$x$ in $\mathcal{G}_{\epsilon}$ and the $(k-d-1)$-neighborhood of $x^{+}$ in
$\mathcal{G}_{\epsilon}$. If we move to the $S_{\epsilon}$-successor of
$x^{+}$, we will find that the visible part in
$\text{tp}_{(\mathcal{G}_{\epsilon},S_{\epsilon})}^{k}(a)$ of its neighborhood
in $\mathcal{G}_{\epsilon}$ will have the same $(k-d-2)$-radius type as
$x^{+}$.

Of course, everything we have said about $S_{\epsilon}$-successors also holds
for $S_{\epsilon}$-predecessors, and for any iteration of upward/downward
(i.e. along $S_{\epsilon}$-edges) and sideways (i.e. in
$\mathcal{G}_{\epsilon}$) steps, thus encapsulating $a$ in a very regular
neighborhood of radius $k$ in $(\mathcal{G}_{\epsilon},S_{\epsilon})$.

It should now be visible that this construction is reminiscent of a fractal,
in that some patterns - here, the neighborhood types - are repeated each time
we follow the successor relation, their size shrinking time after time
(although in our setting, the patterns are obviously repeated only a finite
number of times).

This is why we introduce in Definition 3 the fractal type $[\tau]_{k}$.

Aside from a small number of exceptions (namely, for neighborhood types that
do not occur frequently enough, and around the transitions between frequent
neighborhood types), every element of $k$-neighborhood type $\tau$ in
$\mathcal{G}_{\epsilon}$ will have the fractal neighborhood type $[\tau]_{k}$
in $(\mathcal{G}_{\epsilon},S_{\epsilon})$.

If $\mathcal{N}$ is a representative of a neighborhood type $\tau$,
$c^{\mathcal{N}}$ is called the center of $\mathcal{N}$. Recall from
Definition 2 that $c$ is the constant symbol added to $\Sigma$ when
considering neighborhood types to pinpoint the central element of a
neighborhood.

[Fractal types] We define by induction on $k\in\mathbb{N}$, for every
$k$-neighborhood type $\tau$ over $\Sigma$, the $k$-neighborhood types
$[\tau]_{k}$, $[\tau]^{+}_{k}$ and $[\tau]^{-}_{k}$ over $\Sigma\cup\\{S\\}$.

For $k=0$, $[\tau]_{0}=[\tau]^{+}_{0}=[\tau]^{-}_{0}=\tau$ (meaning that $S$
is interpreted as the empty relation in $[\tau]_{0}$, $[\tau]^{+}_{0}$ and
$[\tau]^{-}_{0}$).

Starting from a representative $\mathcal{N}$ of center $a$ of the isomorphism
class $\tau$, we construct $\mathcal{N}^{\prime}$, whose role is to serve as
an intermediate step in the construction of the full fractal neighborhood, as
follows.

For every $x\in N$ at distance $d\leq k-1$ from $a$, let $\mathcal{M}^{+}_{x}$
and $\mathcal{M}^{-}_{x}$ be structures of respective isomorphism type
$[\chi]^{+}_{k-d-1}$ and $[\chi]^{-}_{k-d-1}$, where $\chi$ is the
$(k-d-1)$-neighborhood type of $x$ in $\mathcal{N}$, and of respective center
$x^{+}$ and $x^{-}$.

$\mathcal{N}^{\prime}$ is defined as the disjoint union of $\mathcal{N}$ and
all the $\mathcal{M}^{+}_{x}$ and the $\mathcal{M}^{-}_{x}$, for $x\neq a$,
together with all the edges $S(x,x^{+})$ and $S(x^{-},x)$.

From there, $\mathcal{N}^{+}$ (resp. $\mathcal{N}^{-}$) is defined as the the
disjoint union of $\mathcal{N}^{\prime}$ and $\mathcal{M}^{+}_{a}$ (resp.
$\mathcal{M}^{-}_{a}$) together with the edge $S(a,a^{+})$ (resp.
$S(a^{-},a)$). Likewise, $\mathcal{N}^{+/-}$ is defined as the disjoint union
of $\mathcal{N}^{\prime}$, $\mathcal{M}^{+}_{a}$ and $\mathcal{M}^{-}_{a}$
together with the edges $S(a,a^{+})$ and $S(a^{-},a)$. In each case, $a$ is
taken as the center.

Now, $[\tau]_{k}$, $[\tau]^{+}_{k}$ and $[\tau]^{-}_{k}$ are defined
respectively as the isomorphism type of $\mathcal{N}^{+/-}$, $\mathcal{N}^{+}$
and $\mathcal{N}^{-}$.

An illustration of this definition is given in Figure 2.

$a$$\bullet$$a^{+}$$\bullet$$a^{-}$$\bullet$$x$$\bullet$$x^{+}$$\bullet$$\tau$$\tau_{|k-1}$$\tau_{|k-1}$$\chi_{|k-d-1}$$d$
Figure 2. Partial representation of $\mathcal{N}^{+/-}$, of type $[\tau]_{k}$.
Here, $\chi$ is the $(k-d)$-neighborhood type of the element $x$, at distance
$d$ from $a$ in $\tau$. The dashed arrows represent $S$-edges.

[Layering] We say that an $r$-neighborhood $\mathcal{N}$ over
$\Sigma\cup\\{S,c\\}$ is layered if it does not contain any cycle going
through an $S$-edge. Every $[\tau]_{r}$ is obviously layered by construction.

We say that a structure over $\Sigma\cup\\{S\\}$ satisfies the property
(Layer[$r$]) iff all the $r$-neighborhoods of this structure are layered.

It turns out (Layer[$r$]) can be reformulated in a way that does not involve
the $r$-neighborhoods of the structure.

######  Lemma 3.

A structure $\mathcal{G}$ over $\Sigma\cup\\{S\\}$ satisfies (Layer[$r$]) if
and only if it contains no cycle of length at most $2r+1$ going through an
$S$-edge.

######  Proof 3.1.

If $\mathcal{G}$ contains a cycle of length at most $2r+1$ going through an
$S$-edge, then the $r$-neighborhood of any vertex of this cycle contains the
whole cycle, thus (Layer[$r$]) does not hold in $\mathcal{G}$.

Conversely, we show that if some $r$-neighborhood contains a cycle going
through an $S$-edge, then it must also contain a small (i.e. of length at most
$2r+1$) such cycle.

Suppose that there exists $x\in G$ such that
$\mathcal{N}_{\mathcal{G}}^{r}(x)$ contains a cycle going through an $S$-edge,
and let $S(y,z)$ be such an edge.

For any $u\in\mathcal{N}_{\mathcal{G}}^{r}(x)$, we define the cone $C_{u}$ at
$u$ as the set of elements $v\in\mathcal{N}_{\mathcal{G}}^{r}(x)$ such that
every shortest path from $x$ to $v$ in $\mathcal{N}_{\mathcal{G}}^{r}(x)$ goes
through $u$.

There are two cases, depending on the relative position of $y$, $z$ and their
cones:

  * •

If $z\notin C_{y}$ and $y\notin C_{z}$, let $p_{y\rightarrow x}$ (resp.
$p_{x\rightarrow z}$) be a path of minimal length from $y$ to $x$, not going
through $z$ (resp. from $x$ to $z$, not going through $y$).

Let $X$ be the set of nodes appearing both in $p_{y\rightarrow x}$ and
$p_{x\rightarrow z}$. $X$ is not empty, as $x\in X$, and $y,z\notin X$. Let
$v\in X$ such that $\text{dist}_{\mathcal{G}}(x,v)$ is maximal among the nodes
of $X$, and let $p_{y\rightarrow v}$ (resp. $p_{v\rightarrow z}$) be the
segment of $p_{y\rightarrow x}$ (resp. of $p_{x\rightarrow z}$) from $y$ to
$v$ (resp. from $v$ to $z$).

Then $p_{v\rightarrow z}\cdot(z,y)\cdot p_{y\rightarrow v}$ is a cycle going
through an $S$-edge, and is of length $\leq 2r+1$. This is illustrated in
Figure 3.

$x$$\bullet$$y$$\bullet$$z$$\bullet$$v$$\bullet$$C_{y}$$C_{z}$$S$ Figure 3.
Existence of a short cycle joining $y$, $z$ and $v$

  * •

Otherwise, suppose without loss of generality that $z\in C_{y}$. This entails
that $y\notin C_{z}$ and $\text{dist}_{\mathcal{G}}(x,z)=d+1$ where
$d:=\text{dist}_{\mathcal{G}}(x,y)$.

Let the initial cycle be $(z,v_{1},\cdots,v_{m-1},y)$, with the notation
$v_{0}=z$ and $v_{m}=y$.

Let $i$ be the minimal integer such that $v_{i}\notin C_{z}$. Let
$p_{x\rightarrow v_{i}}$ be a shortest path from $x$ to $v_{i}$: by
definition, it does not intersect $C_{z}$, and has length at most $r$. Thus,
there exists a path $p_{y\rightarrow v_{i}}=p_{y\rightarrow x}\cdot
p_{x\rightarrow v_{i}}$ from $y$ to $v_{i}$ of length at most $r+d$ going only
through nodes outside of $C_{z}$.

Since $v_{i-1}\in C_{z}$, there exists a path $p_{v_{i-1}\rightarrow z}$ from
$v_{i-1}$ to $z$ of length at most $r-(d+1)$ going only through nodes of
$C_{z}$.

Hence $p_{y\rightarrow v_{i}}\cdot(v_{i},v_{i-1})\cdot p_{v_{i-1}\rightarrow
z}\cdot(z,y)$ is a cycle going though an $S$-edge, and its length is at most
$2r+1$. This is depicted in Figure 4.

$x$$\bullet$$y$$\bullet$$z$$\bullet$$v_{i-1}$$\bullet$$v_{i}$$\bullet$$C_{z}$$S$
Figure 4. Existence of a short cycle joining $y$, $z$, $v_{i-1}$ and $v_{i}$

This characterization of (Layer[$r$]) allows us to state the following lemma,
which is now straightforward. It provides a method to add an $S$-edge without
breaking the property (Layer[$r$]).

######  Lemma 4.

Let $r\in\mathbb{N}$, and $(\mathcal{G},S)$ be a structure satisfying
(Layer[$r$]).

If $x,y\in G$ are such that $\text{dist}_{(\mathcal{G},S)}(x,y)>2r$, then
(Layer[$r$]) holds in $(\mathcal{G},S\cup\\{(x,y)\\})$

##  4\. Proof of Theorem 1

We are now ready to prove Theorem 1. Recall the sketch of proof from Section
2. We proceed in several steps:

Section 4.1 details the general framework of the proof. In Section 4.2, we
divide the neighborhood types into rare ones and frequent ones.

We then begin the construction of $S_{1}$: Section 4.3 is dedicated to the
construction of $S_{1}$ around the occurrences in $\mathcal{G}_{1}$ of rare
neighborhood types. Then, in Section 4.4, we keep constructing $S_{1}$ around
the occurrences (two for each neighborhood type) of frequent neighborhood
types that are designed to make, when the construction is complete, the
$S_{1}$-junction between two frequent neighborhood types.

At this point, $S_{1}$ will be fully built around the singular points of
$\mathcal{G}_{1}$. Section 4.5 deals with the transfer of this partial
successor relation $S_{1}$ over to $\mathcal{G}_{2}$: this will result in a
partial $S_{2}$, built in a similar way around the singular points of
$\mathcal{G}_{2}$.

In Section 4.6, $S_{1}$ and $S_{2}$ are completed independently, to cover
$G_{1}$ and $G_{2}$. These expansions do not need to be coordinated, since at
this point, the elements that are not already covered by $S_{1}$ and $S_{2}$
are occurrences of frequent neighborhood types and their resulting
neighborhood types will be regular (i.e. fractal) both in
$(\mathcal{G}_{1},S_{1})$ and $(\mathcal{G}_{2},S_{2})$.

We then give some simple examples in Section 4.7, before establishing
properties of $S_{1}$ and $S_{2}$ in Section 4.8, and concluding the proof in
Section 4.9.

###  4.1. General method

Let $\mathcal{C}$ be a class of $\Sigma$-structures of degree at most $d$. We
show the following: for every $\alpha\in\mathbb{N}$, there exists some
$f(\alpha)\in\mathbb{N}$ such that, given
$\mathcal{G}_{1},\mathcal{G}_{2}\in\mathcal{C}$, if
$\mathcal{G}_{1}\equiv^{\textsc{FO}}_{f(\alpha)}\mathcal{G}_{2}$ then
$\mathcal{G}_{1}\equiv^{{\textup{Succ-inv
}\textsc{FO}}}_{\alpha}\mathcal{G}_{2}$. For that, we will exhibit successor
relations $S_{1}$ and $S_{2}$ such that
$(\mathcal{G}_{1},S_{1})\equiv^{\textsc{FO}}_{\alpha}(\mathcal{G}_{2},S_{2})$.

More precisely, using the notations from Definition 2, we will show that
$[\\![(\mathcal{G}_{1},S_{1})]\\!]_{r}=^{t}[\\![(\mathcal{G}_{2},S_{2})]\\!]_{r}$
where $r$ and $t$ depend on $\alpha$ and are large enough to ensure that
$(\mathcal{G}_{1},S_{1})\equiv^{\textsc{FO}}_{\alpha}(\mathcal{G}_{2},S_{2})$.
The existence of such $r$ and $t$ follows from the well-known Hanf threshold
theorem, whose finite version is given in [FSV95], and stated as Theorem 4.24
in [Lib04].

We will construct $S_{1}$ and $S_{2}$ iteratively in a way that ensures, at
each step, that the property (Layer[$r$]) holds in $(\mathcal{G}_{1},S_{1})$
and in $(\mathcal{G}_{2},S_{2})$. The property (Layer[$r$]) is obviously
satisfied in $(\mathcal{G}_{1},\emptyset)$. Each time we add an $S_{1}$-edge
or an $S_{2}$-edge, we will make sure that we are in the right conditions to
call upon Lemma 4, so that (Layer[$r$]) is preserved.

Let us define the two-variable function $N$ by
$N(d,r):=d\cdot\frac{(d-1)^{r}-1}{d-2}+1$ if $d\neq 2$, and by $N(2,r):=2r+1$.

Note that the size of any $r$-neighborhood of degree at most $d$ is bounded by
$N(d,r)$.

###  4.2. Separation between rare and frequent neighborhood types

Knowing the values of $r$ and $t$ as defined in Section 4.1, we are now able
to divide the $r$-neighborhood types into two categories: the rare
neighborhood types and the frequent neighborhood types. The intent is that the
two structures have the same number of occurrences of every rare neighborhood
type, and that frequent neighborhood types have many occurrences (wrt. the
total number of occurrences of rare neighborhood types) in both structures.
This “many occurrences wrt.” is formalized through a function $g$ which is to
be specified later on.

More precisely,

######  Lemma 5.

Given $d,r\in\mathbb{N}$ and an increasing function
$g:\mathbb{N}\rightarrow\mathbb{N}$, there exists $p\in\mathbb{N}$ such that
for every $\Sigma$-structures
$\mathcal{G}_{1},\mathcal{G}_{2}\in\mathcal{C}_{d}$ satisfying
$\mathcal{G}_{1}\equiv^{\textsc{FO}}_{p}\mathcal{G}_{2}$, we can divide the
$r$-neighborhood types over $\Sigma$ of degree at most $d$ into rare
neighborhood types and frequent neighborhood types, such that

  * •

every rare neighborhood type has the same number of occurrences in
$\mathcal{G}_{1}$ and in $\mathcal{G}_{2}$

  * •

both in $\mathcal{G}_{1}$ and in $\mathcal{G}_{2}$, every frequent
neighborhood type has at least $g(\beta)$ occurrences, where $\beta$ is the
number of occurrences of all the rare neighborhood types in the structure

  * •

if there is no frequent neighborhood type, then $\mathcal{G}_{1}$ and
$\mathcal{G}_{2}$ are isomorphic.

######  Proof 4.1.

Let $\mathcal{G}_{1}$ and $\mathcal{G}_{2}$ be such that
$\mathcal{G}_{1}\equiv^{\textsc{FO}}_{p}\mathcal{G}_{2}$, for an integer $p$
whose value will become apparent later in the proof.

Let $\chi_{1},\cdots,\chi_{n}$ be an enumeration of all the $r$-neighborhood
types over $\Sigma$ of degree at most $d$, ordered in such a way that $\forall
i<j,|\mathcal{G}_{1}|_{\chi_{i}}\leq|\mathcal{G}_{1}|_{\chi_{j}}$. Note that
$n$ is a function of $d$ and $r$.

The classification of neighborhood types between rare ones and frequent ones
is done through Algorithm 1. The idea is to go through the $r$-neighborhood
types in increasing order of occurrences in $\mathcal{G}_{1}$; if at some
point we reach a neighborhood type with at least $g(\beta)$ occurrences in
$\mathcal{G}_{1}$, where $\beta$ is the total number of occurrences of the
previously visited neighborhood types, then we have found a separation between
rare and frequent types. Otherwise, it means that there are few (wrt. $g$)
occurrences of each neighborhood type, hence $\mathcal{G}_{1}$ is small and,
as long as $p$ is large enough, $\mathcal{G}_{2}$ must be isomorphic to
$\mathcal{G}_{1}$.

Algorithm 1 Separation between rare and frequent neighborhood types

1:$\beta\leftarrow 0$

2:$i\leftarrow 1$

3:while $i\leq n$ and $|\mathcal{G}_{1}|_{\chi_{i}}<g(\beta)$ do

4: $\beta\leftarrow\beta+|\mathcal{G}_{1}|_{\chi_{i}}$

5: $i$++

6:end while$\triangleright$ If $i\leq n$, $\chi_{i}$ is the frequent
neighborhood type with the least occurrences in $\mathcal{G}_{1}$. If $i=n+1$,
all the neighborhood types are rare.

At the end of Algorithm 1, we call $\chi_{1},\cdots,\chi_{i-1}$ the rare
neighborhood types, and $\chi_{i},\cdots,\chi_{n}$ the frequent ones.

Note that $\beta$ indeed counts the total number of occurrences of rare
neighborhood types in $\mathcal{G}_{1}$.

We now define the integers $(a_{i})_{1\leq i\leq n}$ as $a_{1}:=g(0)$ and
$a_{i+1}:=g(ia_{i})$.

As $g$ is monotone, it is easy to show by induction that for each rare
neighborhood type $\chi_{j}$ with $j<i$, $|\mathcal{G}_{1}|_{\chi_{j}}<a_{j}$.

As long as $p$ is chosen large enough so that
$\mathcal{G}_{1}\equiv^{\textsc{FO}}_{p}\mathcal{G}_{2}$ entails
$[\\![\mathcal{G}_{1}]\\!]_{r}=^{a_{n}}[\\![\mathcal{G}_{2}]\\!]_{r}$, we have
by construction that every rare neighborhood type has the same number of
occurrences (which is smaller that $a_{n}$) in $\mathcal{G}_{1}$ and in
$\mathcal{G}_{2}$. Furthermore, in $\mathcal{G}_{1}$ as in $\mathcal{G}_{2}$,
if $\beta$ denotes the total number of occurrences of rare neighborhood types,
every frequent neighborhood type has at least $g(\beta)$ occurrences.

We just need to make sure that the two structures are isomorphic when all the
neighborhood types are rare. If this is the case, then
$|\mathcal{G}_{1}|=|\mathcal{G}_{2}|\leq n(a_{n}-1)$. Hence, as long as $p\geq
n(a_{n}-1)$, $\mathcal{G}_{1}\equiv^{\textsc{FO}}_{p}\mathcal{G}_{2}$ implies
$\mathcal{G}_{1}\simeq\mathcal{G}_{2}$ when all the neighborhood types are
rare.

Let $\tau_{0},\cdots,\tau_{m-1}$ be the frequent neighborhood types. From now
on, we suppose that $m\geq 1$: there is nothing to do if $m=0$, since
$\mathcal{G}_{1}$ and $\mathcal{G}_{2}$ are isomorphic. Let $\beta$ be the
total number of occurrences of rare neighborhood types in $\mathcal{G}_{1}$.

###  4.3. Construction of $S_{1}$ around elements of rare neighborhood type

To begin with, let us focus on $\mathcal{G}_{1}$, and start the construction
of $S_{1}$ around occurrences of rare neighborhood types. Algorithm 2 deals
with this construction. In the following, $R_{\leq k}$ will denote
$\bigcup\limits_{0\leq j\leq k}R_{j}$.

For a given occurrence $x$ of some rare neighborhood type, we choose as its
$S_{1}$-successor and $S_{1}$-predecessor two occurrences of neighborhood type
$\tau_{0}$ (the first frequent neighborhood type), far apart from one another
and from $x$. The existence of those elements relies on the bounded degree
hypothesis. This is done on lines 8 and 11.

When line 14 is reached, every occurrence of rare neighborhood type has an
$S_{1}$-predecessor and an $S_{1}$-successor of neighborhood type $\tau_{0}$.

It is not enough, however, only to deal with the occurrences of rare
neighborhood types. We need to “protect” them up to distance $r$ in
$(\mathcal{G}_{1},S_{1})$. For that purpose, we construct the subsets $R_{k}$
of $G_{1}$, for $0\leq k\leq r$.

For each $k$, the subset $R_{k}$ is the set of elements at distance exactly
$k$ in $(\mathcal{G}_{1},S_{1})$ from the set of occurrences of rare
neighborhood types. Until we have reached $k=r$ (that is, distance $r$ from
occurrences of rare neighborhood types), every element of $R_{k}$ is given an
$S_{1}$-successor (line 21) and/or an $S_{1}$-predecessor (line 26) of its
neighborhood type, if it does not already have one. Once again, those elements
are required to be far (i.e. at distance greater than $2r$) from what already
has been constructed.

Provided that $g$ is large enough, it is always possible to find $x^{+}$ and
$x^{-}$ on lines 8, 11, 21 and 26. Indeed, all the neighborhood types
considered are frequent ones, and the size of the $2r$-neighborhood of
$R_{\leq k+1}$ is bounded by a function of $d$, $r$ and $\beta$ (the total
number of occurrences of rare neighborhood types in $\mathcal{G}_{1}$). More
precisely, at any point of the construction, $(\mathcal{G}_{1},S_{1})$ has
degree at most $d+2$. Hence, the $2r$-neighborhood of $R_{r}$ has size at most

$\beta N(d+2,3r)$

(recall the definition of $N$ from Definition 4.1), and it is enough to make
sure that

$g(\beta)\geq\beta N(d+2,3r)+1\,.$

Algorithm 2 Construction of $S_{1}$ around elements of rare neighborhood type

1:$S_{1}\leftarrow\emptyset$

2:$R_{0}\leftarrow\\{x\in G_{1}:\text{tp}_{\mathcal{G}_{1}}^{r}(x)\text{ is
rare}\\}$

3:$R_{1},\cdots,R_{r}\leftarrow\emptyset$

4:for all $x\in R_{0}$ do

5: for all neighbors $y\notin R_{\leq 1}$ of $x$ in $\mathcal{G}_{1}$ do

6: $R_{1}\leftarrow R_{1}\cup\\{y\\}$

7: end for

8: find  $x^{+}$ such that $\text{tp}_{\mathcal{G}_{1}}^{r}(x^{+})=\tau_{0}$
and $\text{dist}_{(\mathcal{G}_{1},S_{1})}(x^{+},R_{\leq 1})>2r$
$\triangleright$ We pick a node at distance greater than $2r$ in compliance
with Lemma 4, so that neighborhoods stay layered. Recall that $\tau_{0}$ is
the first frequent neighborhood type.

9: $R_{1}\leftarrow R_{1}\cup\\{x^{+}\\}$

10: $S_{1}\leftarrow S_{1}\cup\\{(x,x^{+})\\}$

11: find  $x^{-}$ such that $\text{tp}_{\mathcal{G}_{1}}^{r}(x^{-})=\tau_{0}$
and $\text{dist}_{(\mathcal{G}_{1},S_{1})}(x^{-},R_{\leq 1})>2r$

12: $R_{1}\leftarrow R_{1}\cup\\{x^{-}\\}$

13: $S_{1}\leftarrow S_{1}\cup\\{(x^{-},x)\\}$

14:end for $\triangleright$ At this point, every element of rare neighborhood
type has an $S_{1}$-predecessor and an $S_{1}$-successor of neighborhood type
$\tau_{0}$

15:for $k$ from $1$ to $r-1$ do

16: for all $x\in R_{k}$ do $\triangleright$
$\text{tp}_{\mathcal{G}_{1}}^{k}(x)$ is a frequent neighborhood type

17: for all neighbors $y\notin R_{\leq k+1}$ of $x$ in $\mathcal{G}_{1}$ do

18: $R_{k+1}\leftarrow R_{k+1}\cup\\{y\\}$

19: end for

20: if $x$ does not have a successor by $S_{1}$ then

21: find  $x^{+}$ such that
$\text{tp}_{\mathcal{G}_{1}}^{r}(x^{+})=\text{tp}_{\mathcal{G}_{1}}^{r}(x)$
and $\text{dist}_{(\mathcal{G}_{1},S_{1})}(x^{+},R_{\leq k+1})>2r$

22: $R_{k+1}\leftarrow R_{k+1}\cup\\{x^{+}\\}$

23: $S_{1}\leftarrow S_{1}\cup\\{(x,x^{+})\\}$

24: end if

25: if $x$ does not have a predecessor by $S_{1}$ then

26: find  $x^{-}$ such that
$\text{tp}_{\mathcal{G}_{1}}^{r}(x^{-})=\text{tp}_{\mathcal{G}_{1}}^{r}(x)$
and $\text{dist}_{(\mathcal{G}_{1},S_{1})}(x^{-},R_{\leq k+1})>2r$

27: $R_{k+1}\leftarrow R_{k+1}\cup\\{x^{-}\\}$

28: $S_{1}\leftarrow S_{1}\cup\\{(x^{-},x)\\}$

29: end if

30: end for

31:end for

###  4.4. Construction of $S_{1}$ around the junctions between two frequent
neighborhood types

Recall that there is a second kind of singular elements: those which will be
at the junction between two successive frequent neighborhood types. That is,
elements of neighborhood type $\tau_{i}$ that will, in the final structure
$(\mathcal{G}_{1},S_{1})$, have an $S_{1}$-successor of neighborhood type
$\tau_{i+1[m]}$, or an $S_{1}$-predecessor of neighborhood type
$\tau_{i-1[m]}$.

Those junction elements need to be treated in a similar way as the occurrences
of rare neighborhood types in Section 4.3. This construction is done following
Algorithm 3.

The idea of Algorithm 3 is very similar to that of Algorithm 2. We start by
picking two elements $x_{i}^{\text{min}}$ and $x_{i}^{\text{max}}$ for every
frequent neighborhood type $\tau_{i}$ (for loop line 2), that are far from
each other and from the previous construction. Once the construction is done,
$x_{i}^{\text{min}}$ will be the first (wrt. $S_{1}$) element of the sequence
of occurrences of type $\tau_{i}$, and $x_{i}^{\text{max}}$ the last one. The
elements that will appear between (in the sense of $S_{1}$)
$x_{i}^{\text{min}}$ and $x_{i}^{\text{max}}$ will exactly be those of
neighrborhood type $\tau_{i}$, except possibly for $i=0$, where all the
occurrences of the rare neighborhood types will also appear between
$x_{0}^{\text{min}}$ and $x_{0}^{\text{max}}$.

Once these $2m$ elements are chosen, we add an $S_{1}$-edge between each
$x_{i}^{\text{max}}$ and the corresponding $x_{i+1[m]}^{\text{min}}$ on line
9: in the final structure, these edges will mark the transition (in the sense
of $S_{1}$) between the range of elements of neighborhood type $\tau_{i}$ and
those of neighborhood type $\tau_{i+1[m]}$.

The set $P_{0}$ of those $2m$ elements will have the same role as the set
$R_{0}$ of occurrences of rare neighborhood types for Algorithm 2: we build
$S_{1}$-edges at depth $r$ around it. This is done through the subsets $P_{k}$
of $G_{1}$, for $0\leq k\leq r$, $P_{k}$ being the set of elements at distance
$k$ from $P_{0}$ in $(\mathcal{G}_{1},S_{1})$. Once again, $P_{\leq k}$
denotes $\bigcup\limits_{0\leq j\leq k}P_{j}$.

For the same reason as for Algorithm 2, it is always possible to find elements
$x^{+}$ and $x^{-}$ on lines 17 and 22.

Note that if $m=1$, there is obviously no transition elements: we simply
construct an $S_{1}$-edge between $x_{0}^{\text{max}}$ and
$x_{0}^{\text{min}}$.

Algorithm 3 Construction of $S_{1}$ around the junctions between two frequent
neighborhood types

1:$P_{0},\cdots,P_{r}\leftarrow\emptyset$

2:for $i$ from $0$ to $m-1$ do

3: find  $x_{i}^{\text{min}}$ such that
$\text{tp}_{\mathcal{G}_{1}}^{r}(x_{i}^{\text{min}})=\tau_{i}$ and
$\text{dist}_{(\mathcal{G}_{1},S_{1})}(x_{i}^{\text{min}},R_{\leq r}\cup
P_{0})>2r$

4: $P_{0}\leftarrow P_{0}\cup\\{x_{i}^{\text{min}}\\}$

5: find  $x_{i}^{\text{max}}$ such that
$\text{tp}_{\mathcal{G}_{1}}^{r}(x_{i}^{\text{max}})=\tau_{i}$ and
$\text{dist}_{(\mathcal{G}_{1},S_{1})}(x_{i}^{\text{max}},R_{\leq r}\cup
P_{0})>2r$

6: $P_{0}\leftarrow P_{0}\cup\\{x_{i}^{\text{max}}\\}$

7:end for

8:for $i$ from $0$ to $m-1$ do

9: $S_{1}\leftarrow
S_{1}\cup\\{(x_{i}^{\text{max}},x_{i+1[m]}^{\text{min}})\\}$

10:end for

11:for $k$ from $0$ to $r-1$ do

12: for all $x\in P_{k}$ do

13: for all neighbors $y\notin P_{\leq k+1}$ of $x$ in $\mathcal{G}_{1}$ do

14: $P_{k+1}\leftarrow P_{k+1}\cup\\{y\\}$

15: end for

16: if $x$ does not have a successor by $S_{1}$ then

17: find  $x^{+}$ such that
$\text{tp}_{\mathcal{G}_{1}}^{r}(x^{+})=\text{tp}_{\mathcal{G}_{1}}^{r}(x)$
and $\text{dist}_{(\mathcal{G}_{1},S_{1})}(x^{+},R_{\leq r}\cup P_{\leq
k+1})>2r$

18: $P_{k+1}\leftarrow P_{k+1}\cup\\{x^{+}\\}$

19: $S_{1}\leftarrow S_{1}\cup\\{(x,x^{+})\\}$

20: end if

21: if $x$ does not have a predecessor by $S_{1}$ then

22: find  $x^{-}$ such that
$\text{tp}_{\mathcal{G}_{1}}^{r}(x^{-})=\text{tp}_{\mathcal{G}_{1}}^{r}(x)$
and $\text{dist}_{(\mathcal{G}_{1},S_{1})}(x^{-},R_{\leq r}\cup P_{\leq
k+1})>2r$

23: $P_{k+1}\leftarrow P_{k+1}\cup\\{x^{-}\\}$

24: $S_{1}\leftarrow S_{1}\cup\\{(x^{-},x)\\}$

25: end if

26: end for

27:end for

###  4.5. Carrying $S_{1}$ over to $\mathcal{G}_{2}$

In Sections 4.3 and 4.4, $S_{1}$ has been constructed around the singular
points of $\mathcal{G}_{1}$, i.e. occurrences of rare neighborhood types and
elements that are to make the junction between two $S_{1}$-segments of
frequent neighborhood types.

Before we extend $S_{1}$ to the remaining elements (all of them being
occurrences of frequent neighborhood types) of $\mathcal{G}_{1}$, we carry it
over to $\mathcal{G}_{2}$. This transfer is possible under the starting
hypothesis that $\mathcal{G}_{1}$ and $\mathcal{G}_{2}$ are FO-similar.

Indeed, we made the assumption that
$\mathcal{G}_{1}\equiv^{\textsc{FO}}_{f(\alpha)}\mathcal{G}_{2}$; now,
provided that $f(\alpha)$ is large enough, this ensures that there exists a
substructure of $\mathcal{G}_{2}$ which is isomorphic to the part of
$\mathcal{G}_{1}$ around which we have already constructed $S_{1}$. This
isomorphism will make it possible to carry this partial successor relation
over to $\mathcal{G}_{2}$. We make this precise in the following.

Let

$A_{1}:=R_{\leq r}\cup P_{\leq r}$

and

$B:=\\{x\in G_{1}:\text{dist}_{(\mathcal{G}_{1},S_{1})}(x,A_{1})\leq r\\}\,.$

If we let $t_{r}^{d}$ be the number of $r$-neighborhood types of degree at
most $d$ over $\Sigma$, we must have that $m\leq n$ thus $|A_{1}|$ can be
bounded by

$(\beta+2t_{r}^{d})N(d+2,r)\,.$

Similarly, the size of $B$ can be bounded by

$(\beta+2t_{r}^{d})N(d+2,2r)\,,$

which is a function of $\beta$, $r$ and $d$. Hence as long as $f(\alpha)$ is
larger than that number, the Duplicator has a winning strategy in the
Ehrenfeucht-Fraïssé game between $\mathcal{G}_{1}$ and $\mathcal{G}_{2}$ in
which the Spoiler chooses every element of $B$. Let $h:B\rightarrow G_{2}$ be
the function resulting from such a strategy.

The mapping $h$ defines an isomorphism from $\mathcal{G}_{1}|_{B}$ to
$\mathcal{G}_{2}|_{\operatorname{Im}(h)}$. Let $A_{2}:=h(A_{1})$. By making
$f(\alpha)$ large enough, we can make sure that $\operatorname{Im}(h)$ covers
the $r$-neighborhood in $\mathcal{G}_{2}$ of every element of $A_{2}$. We then
have that for every $x\in A_{1}$,
$\text{tp}_{\mathcal{G}_{2}}^{r}(h(x))=\text{tp}_{\mathcal{G}_{1}}^{r}(x)$.

We set $S_{2}:=\\{(h(x),h(y)):(x,y)\in S_{1}\\}$. $h$ now defines an
isomorphism from $(\mathcal{G}_{1},S_{1})|_{B}$ to
$(\mathcal{G}_{2},S_{2})|_{\operatorname{Im}(h)}$, and for every $x\in A_{1}$,
$\text{tp}_{(\mathcal{G}_{2},S_{2})}^{r}(h(x))=\text{tp}_{(\mathcal{G}_{1},S_{1})}^{r}(x)$.

Note that since $\mathcal{G}_{1}$ and $\mathcal{G}_{2}$ have the same number
of occurrences of each rare neighborhood type, every element lying outside of
$A_{2}$ must have a frequent neighrbohood type.

###  4.6. Completion of $S_{1}$ and $S_{2}$

Now that $S_{1}$ and $S_{2}$ are constructed around all the singular points in
$\mathcal{G}_{1}$ and $\mathcal{G}_{2}$, it remains to extend their
construction to all the other elements of the structures. Recall that all the
remaining elements are occurrences of frequent neighborhood types.

From $(\mathcal{G}_{\epsilon},S_{\epsilon})$, for $\epsilon\in\\{1,2\\}$, at
any point in the construction, let us define the partial function
$S_{\epsilon}^{*}:G_{\epsilon}\rightarrow G_{\epsilon}$ that maps $x\in
G_{\epsilon}$ to the (unique) $y$ that is $S_{\epsilon}$-reachable (while
taking the orientation into account) from $x$ and that does not have an
$S_{\epsilon}$-successor. This function is defined on every element that does
not belong to an $S_{\epsilon}$-cycle (and in particular, on every element
without an $S_{\epsilon}$-predecessor).

Likewise, we define $S_{\epsilon}^{-*}$ by reversing the arrows of
$S_{\epsilon}$.

At this point, for every $x\notin A_{1}$, $S_{1}^{*}(x)=S_{1}^{-*}(x)=x$, and
for every $x\notin A_{2}$,

$S_{2}^{*}(x)=S_{2}^{-*}(x)=x\,.$

We now run Algorithm 4. We first treat $\mathcal{G}_{1}$, and then apply a
similar method to $\mathcal{G}_{2}$, replacing $x_{i}^{\text{min}}$ and
$x_{i}^{\text{max}}$ by $h(x_{i}^{\text{min}})$ and $h(x_{i}^{\text{max}})$.
The idea is, for every frequent neighborhood type $\tau_{i}$, to insert all
its remaining occurrences between (in the sense of $S_{1}$)
$x_{i}^{\text{min}}$ and $x_{i}^{\text{max}}$.

The first approach (the loop at line 2) is greedy: while constructing
$S_{\epsilon}$ on nodes of neighborhood type $\tau_{i}$, we choose as the
successor of the current node any occurrence of $\tau_{i}$ that is at distance
greater than $2r$ from the current node $s$ and the closing node of
neighborhood type $\tau_{i}$, $S_{\epsilon}^{-*}(x_{i}^{\text{max}})$. This,
together with Lemma 4, ensures that (Layer[$r$]) holds after every addition.
The conditions line 11 also ensure that the final edge addition, line 15, does
not break (Layer[$r$]).

Once we cannot apply this greedy approach anymore, we know that only a small
number (which can be bounded by $2N(d+2,2r)$) of nodes of neighborhood type
$\tau_{i}$ remain without $S_{1}$-predecessor. The loop at line 17 considers
one such node $x$ at a time. As long as $g$ is large enough, we have
constructed $S_{1}$ around enough elements of neighborhood type $\tau_{i}$ in
the greedy approach to ensure the existence of some $S_{1}(y,z)$, with $y,z$
of neighborhood type $\tau_{i}$ and at distance greater than $2r$ from $x$;
$x$ is inserted between $y$ and $z$ (line 20). For that, it is enough to have
constructed at least

$2N(d+2,2r)+1$

$S_{1}$-edges in the greedy phase. This is the case in particular when there
are at least

$4N(d+2,2r)+1$

elements of neighborhood type $\tau_{i}$ without $S_{1}$-predecessor at the
beginning of Algorithm 4, which can be ensured by having

$g(\beta)\geq|A_{1}|+4N(d+2,2r)+1\,.$

This holds in particular when

$g(\beta)\geq(\beta+2t_{r}^{d})N(d+2,r)+4N(d+2,2r)+1\,.$

We will prove in Lemma 7 that all these insertions preserve (Layer[$r$]).

Algorithm 4 Completion of $S_{\epsilon}$

1:for $\epsilon$ from $1$ to $2$ do

2: for $i$ from $0$ to $m-1$ do

3: if $\epsilon=1$ then

4: $s\leftarrow S_{1}^{*}(x_{i}^{\text{min}})$

5: $t\leftarrow S_{1}^{-*}(x_{i}^{\text{max}})$

6: else

7: $s\leftarrow S_{2}^{*}(h(x_{i}^{\text{min}}))$

8: $t\leftarrow S_{2}^{-*}(h(x_{i}^{\text{max}}))$

9: end if

10: while such an $x$ exists do

11: find  $x$ with no $S_{\epsilon}$-predecessor, such that
$\text{tp}_{\mathcal{G}_{\epsilon}}^{r}(x)=\tau_{i}$,
$\text{dist}_{(\mathcal{G}_{\epsilon},S_{\epsilon})}(s,x)>2r$,
$\text{dist}_{(\mathcal{G}_{\epsilon},S_{\epsilon})}(x,t)>2r$ and
$\text{dist}_{(\mathcal{G}_{\epsilon},S_{\epsilon})}(S_{\epsilon}^{*}(x),t)>2r$

12: $S_{\epsilon}\leftarrow S_{\epsilon}\cup\\{(s,x)\\}$

13: $s\leftarrow S_{\epsilon}^{*}(x)$

14: end while$\triangleright$ At this point, only a bounded number of elements
of neighborhood type $\tau_{i}$ are left without an $S_{\epsilon}$-predecessor

15: $S_{\epsilon}\leftarrow S_{\epsilon}\cup\\{(s,t)\\}$

16: end for

17: for $i$ from $0$ to $m-1$ do

18: for all $x$ without $S_{\epsilon}$-predecessor, s.t.
$\text{tp}_{\mathcal{G}_{\epsilon}}^{r}(x)=\tau_{i}$ do

19: find  $y,z\notin A_{\epsilon}$ such that
$\text{tp}_{\mathcal{G}_{\epsilon}}^{r}(y)=\text{tp}_{\mathcal{G}_{\epsilon}}^{r}(z)=\tau_{i}$,
$(y,z)\in S_{\epsilon}$,
$\text{dist}_{(\mathcal{G}_{\epsilon},S_{\epsilon})}(y,x)>2r$ and
$\text{dist}_{(\mathcal{G}_{\epsilon},S_{\epsilon})}(S_{\epsilon}^{*}(x),z)>2r$

20: $S_{\epsilon}\leftarrow
S_{\epsilon}\setminus\\{(y,z)\\}\cup\\{(y,x),(S_{\epsilon}^{*}(x),z)\\}$

21: end for

22: end for

23:end for

###  4.7. Examples of construction

Before we give the proof of correctness of these algorithms, let us see how
they apply in some simple cases

Suppose that there are no occurrences of rare neighborhood types, and only one
frequent neighborhood type $\tau_{0}$, and assume $r=2$.

In this case, Algorithm 2 is irrelevant, and all Algorithm 3 does is pick
$x_{0}^{\text{max}}$ and $x_{0}^{\text{min}}$ far from each other, and start
building $S_{1}$ around those nodes in order to construct their complete
$r$-neighborhood in $(\mathcal{G}_{1},S_{1})$. In order to make the figure
more readable, let us consider that $x_{0}^{\text{max}}$ and
$x_{1}^{\text{min}}$ have only one neighbor. In Figure 5, the plain lines
represent edges in $\mathcal{G}_{1}$, and the dashed arrows represent $S_{1}$.

$x_{0}^{\text{max}}$$\bullet$$x_{0}^{\text{min}}$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$
Figure 5. After Algorithm 3, with one frequent neighborhood type

We now apply Algorithm 4. The first step is to add elements between (in the
sense of $S_{1}$) $S_{1}^{*}(x_{0}^{\text{min}})$ and
$S_{1}^{-*}(x_{0}^{\text{max}})$ in order to join them, in a greedy fashion.
Once this is done, there only remain a few elements that have not been
assigned an $S_{1}$-predecessor. This is depicted in Figure 6.

$x_{0}^{\text{max}}$$x_{0}^{\text{min}}$$x$$S_{1}^{*}(x)$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$
Figure 6. After the greedy part of Algorithm 4, with one frequent neighborhood
type

Now we consider one by one each of the elements that do not have an
$S_{1}$-predecessor: let us start with $x$ in Figure 6. Our goal is to insert
it in the $S_{1}$-cycle while still respecting (Layer[$r$]). For that, we find
two successive elements $y,z$ of the cycle that are far from $x$ and
$S_{1}^{*}(x)$, and we insert $x$ between them, as shown in Figure 7.

$x_{0}^{\text{max}}$$x_{0}^{\text{min}}$$y$$z$$x$$S_{1}^{*}(x)$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$
Figure 7. Inserting $x$ in the $S_{1}$-cycle, as in the second part of
Algorithm 4, with one frequent neighborhood type

We treat all the elements without an $S_{1}$-predecessor in the same way,
until $S_{1}$ is fully built.

Suppose now that there are two frequent neighborhood types $\tau_{0}$ and
$\tau_{1}$, and still no occurrences of rare neighborhood types.

The procedure is very similar: in Algorithm 3, we build the $r$-neighborhood
in $(\mathcal{G}_{1},S_{1})$ of the four nodes $x_{0}^{\text{max}}$,
$x_{0}^{\text{min}}$, $x_{1}^{\text{max}}$ and $x_{1}^{\text{min}}$.

After the greedy part of Algorithm 4, $S_{1}$ looks like in Figure 8, where
occurrences of $\tau_{0}$ are represented as $\bullet$ and occurrences of
$\tau_{1}$ as $\circ$. The remaining of Algorithm 4 is as unchanged.

$x_{0}^{\text{max}}$$x_{1}^{\text{min}}$$x_{1}^{\text{max}}$$x_{0}^{\text{min}}$$x$$S_{1}^{*}(x)$$\circ$$\circ$$\circ$$\circ$$\circ$$\circ$$\circ$$\circ$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$$\bullet$
Figure 8. After the greedy part of Algorithm 4, with two frequent neighborhood
types

Note that if there existed some occurrences of rare neighborhood types, they
would be embedded in the $\tau_{0}$ part of the $S_{1}$-cycle.

###  4.8. Properties of $S_{1}$ and $S_{2}$

We are now ready to show that, after the successive run of Algorithms 2, 3 and
4,

  * •

$S_{1}$ and $S_{2}$ are indeed successor relations (Lemma 6),

  * •

$(\mathcal{G}_{1},S_{1})$ and $(\mathcal{G}_{2},S_{2})$ satisfy (Layer[$r$])
(Lemma 7), and

  * •

a singular element (around a rare or a junction element) of
$(\mathcal{G}_{1},S_{1})$ and its corresponding element via $h$ in
$(\mathcal{G}_{2},S_{2})$ have the same $r$-neighborhood type (Lemma 10),
while any other element in both structures has a regular (i.e. fractal)
$r$-neighborhood type (Lemma 9).

These properties will allow us to prove in Section 4.9 that
$(\mathcal{G}_{1},S_{1})$ and $(\mathcal{G}_{2},S_{2})$ have the same number
of occurrences of every $r$-neighborhood type, up to a threshold $t$.

######  Lemma 6.

$S_{1}$ (resp. $S_{2}$) is a successor relation on $G_{1}$ (resp. $G_{2}$).

######  Proof 4.2.

This result is rather transparent, but a rigorous proof requires the usage of
a somewhat cumbersome invariant.

Let us focus on $\mathcal{G}_{1}$: the proof is the same for
$\mathcal{G}_{2}$, replacing every $x_{i}^{\text{min}}$ and
$x_{i}^{\text{max}}$ with $h(x_{i}^{\text{min}})$ and $h(x_{i}^{\text{max}})$.

Let $a\in G_{1}$ be defined as $S_{1}^{-*}(x_{m-1}^{\text{max}})$ at the
beginning of Algorithm 4. By construction,
$\text{tp}_{\mathcal{G}}^{r}(a)=\tau_{m-1}$ and $a$ has no $S_{1}$-predecessor
as of now.

We show that at any point before line 15 of the loop iteration $i=m-1$ of
Algorithm 4,

  1. (1)

$S_{1}^{-*}(s)=a$

  2. (2)

$S_{1}^{-*}(x_{m-1}^{\text{max}})=a$

  3. (3)

let $y,z\notin A_{1}$ such that $(y,z)\in S_{1}$ and

$\text{tp}_{\mathcal{G}_{1}}^{r}(y)=\text{tp}_{\mathcal{G}_{1}}^{r}(z)=\tau_{j}$

for some $j$; then $S_{1}^{-*}(y)=a$

  4. (4)

for every $i$, $(x_{i}^{\text{max}},x_{i+1[m]}^{\text{min}})\in S_{1}$

  5. (5)

there is no $S_{1}$-cycle

  6. (6)

for every $j>i$,
$\text{tp}_{\mathcal{G}_{1}}^{r}(S_{1}^{-*}(x_{j}^{\text{max}}))=\tau_{j}$

This is obviously satisfied at the beginning of Algorithm 4: there are not yet
such $y,z$ as in 3, and $s=S_{1}^{*}(x_{0}^{\text{min}})$ is $S_{1}$-reachable
from $x_{m-1}^{\text{max}}$ (since
$(x_{m+1}^{\text{max}},x_{0}^{\text{min}})\in S_{1}$) hence 1 holds.

Line 4 preserves the invariant. Indeed, the new value of $s$ is
$S_{1}$-reachable from its previous value (this is guaranteed by 4), which
means that they have the same image through $S_{1}^{-*}$, namely $a$.

Let us prove that line 12 preserves the invariant. 1 and 2 still hold since
$x\neq a$: indeed, for $i<m-1$, $x$ and $a$ do not share the same neighborhood
type, while for $i=m-1$, $a=t$ (because of 2) and the distance condition
prohibits $x=a$. 3 still holds, as the only new possibility for such a couple
$(y,z)$ is $(s,x)$, which is such that $S_{1}^{-*}(y)=a$ (because of 1). 4
obviously holds, as does 5, since the only way for an $S_{1}$-cycle to have
been created is if $x=S_{1}^{-*}(s)$, that is $x=a$. We have seen that this is
absurd. 6 is satisfied, as the only way for it to fail is for $x$ to be some
$S_{1}^{-*}(x_{j}^{\text{max}})$, for $j>i$, which is impossible due to
neighborhood type requirements.

Now, let us move to line 13. Only 1 needs verification, and the argument is
the same as for line 4.

Finally, let us look at line 15, for $i<m-1$. $t\neq a$ since their
neighborhood types are different, hence 1, 2 and 5 still hold. 3 still holds,
as the only new possibility for such a couple $(y,z)$ is $(s,t)$, which is
such that $S_{1}^{-*}(y)=a$ because of 1 (actually, $(s,t)$ does not even fit
the condition, since $t\in A_{1}$). 4 is still satisfied. 6 holds, as the only
way for it to fail is for $t$ to be some $S_{1}^{-*}(x_{j}^{\text{max}})$, for
$j>i$, which is impossible due to neighborhood type requirements.

We now prove that from line 17 until the end of Algorithm 4, there is exactly
one $S_{1}$-cycle, which contains every $y,z\notin A_{1}$ such that $(y,z)\in
S_{1}$ and
$\text{tp}_{\mathcal{G}_{1}}^{r}(y)=\text{tp}_{\mathcal{G}_{1}}^{r}(z)=\tau_{j}$
for some $j$.

This is true after line 15 of the loop iteration $m-1$, which creates the
first $S_{1}$-cycle, as 1 and 2 ensure $t=a=S_{1}^{-*}(s)$. 3 guarantees that
this newly created $S_{1}$-cycle contains all the couple $(y,z)$ satisfying
the condition.

It remains to show that line 20 preserves this property: by hypothesis, $y$
and $z$ belong to the $S_{1}$-cycle. After line 20, there is still exactly one
$S_{1}$-cycle, which corresponds to the previous one where the $S_{1}$-edge
has been replaced by the $S_{1}$-segment $[x,S_{1}^{*}(x)]$. The only
$S_{1}$-edges that have been added belong to the $S_{1}$-cycle, hence the
second part of the property still holds.

In the end, every element of $G_{1}$ has a predecessor by $S_{1}$, hence
$S_{1}$ is a permutation of $G_{1}$. We have shown that it has a single orbit.

######  Lemma 7.

(Layer[$r$]) holds in $(\mathcal{G}_{\epsilon},S_{\epsilon})$, for
$\epsilon\in\\{1,2\\}$

######  Proof 4.3.

This property is guaranteed by the distance conditions of the form

$\text{dist}_{(\mathcal{G}_{\epsilon},S_{\epsilon})}(.,.)>2r$

imposed throughout Algorithms 2, 3 and 4, and by Lemma 4.

One can very easily verify that (Layer[$r$]) is guaranteed by Lemma 4 to hold
in $(\mathcal{G}_{\epsilon},S_{\epsilon})$ prior to the run of Algorithm 4.

We focus on Algorithm 4, and we use Lemma 4 to prove that (Layer[$r$]) remains
valid in $(\mathcal{G}_{\epsilon},S_{\epsilon})$ throughout its run. There are
three edge additions we have to prove correct:

  * •

For the edge addition of line 12, this follows directly from Lemma 4.

  * •

For the edge addition of line 15, we show that the invariant

$\text{dist}_{(\mathcal{G}_{\epsilon},S_{\epsilon})}(s,t)>2r$

is satisfied at the beginning and at the end of the while at line 10. This
invariant, together with Lemma 4, will be enough to conclude.

The invariant holds before the first execution of the while loop.

Working towards a contradiction, suppose that the invariant is broken during
an execution of the loop. In the following, when mentioning a variable, we
refer to its value at the beginning of the loop. There must exists a path from
$S_{\epsilon}^{*}(x)$ (which is to become the new value of $s$ at the end of
the loop) to $t$ in $(\mathcal{G}_{\epsilon},S_{\epsilon}\cup\\{(s,x)\\})$ of
length at most $2r$; consider a shortest one. As is cannot be valid in
$(\mathcal{G}_{\epsilon},S_{\epsilon})$ by choice of $x$, it must go through
the newly added edge $(s,x)$. This means that in
$(\mathcal{G}_{\epsilon},S_{\epsilon})$, either there exist paths of length at
most $2r$ from $S_{\epsilon}^{*}(x)$ to $s$ and from $x$ to $t$, or paths of
length at most $2r$ from $S_{\epsilon}^{*}(x)$ to $x$ and from $s$ to $t$. The
former is absurd considering the way $x$ was chosen, and the latter
contradicts the previous invariant.

  * •

Let us prove that the addition of the two $S_{\epsilon}$-edges of line 20 does
not break (Layer[$r$]). By choice of $y$, we know that
$\text{dist}_{(\mathcal{G}_{\epsilon},S_{\epsilon})}(y,x)>2r$. _A fortiori_ ,
we must have

$\text{dist}_{(\mathcal{G}_{\epsilon},S_{\epsilon}\setminus\\{(y,z)\\})}(y,x)>2r\,,$

and Lemma 4 ensures that
$(\mathcal{G}_{\epsilon},S_{\epsilon}\setminus\\{(y,z)\\}\cup\\{(y,x)\\})$
satisfies the property (Layer[$r$]).

Now, to the second addition: let us prove that, at the beginning of line 20,

$\text{dist}_{(\mathcal{G}_{\epsilon},S_{\epsilon}\setminus\\{(y,z)\\}\cup\\{(y,x)\\})}(S_{\epsilon}^{*}(x),z)>2r\,.$

We then conclude with Lemma 4.

Suppose it is not the case and consider a shortest path from
$S_{\epsilon}^{*}(x)$ to $z$, which must be of length at most $2r$. This path
cannot be valid in $(\mathcal{G}_{\epsilon},S_{\epsilon})$, thus it has to go
through the new edge $(y,x)$. Since there cannot exist a path of length at
most $2r$ from $S_{\epsilon}^{*}(x)$ to $y$ in
$(\mathcal{G}_{\epsilon},S_{\epsilon})$ (as this would contradict
$\text{dist}_{(\mathcal{G}_{\epsilon},S_{\epsilon})}(S_{\epsilon}^{*}(x),z)>2r$),
it has to borrow the edge from $x$ to $y$.

Then in $(\mathcal{G}_{\epsilon},S_{\epsilon}\setminus\\{(y,z)\\})$, there is
a path of length at most $2r$ from $y$ to $z$, which contradicts (Layer[$r$])
in $(\mathcal{G}_{\epsilon},S_{\epsilon})$.

The following Lemma states that the only time $S_{\epsilon}$ joins two nodes
that have different $r$-neighborhood types in $\mathcal{G}_{\epsilon}$ is when
one of them is an occurrence of a rare neighborhood type (in which case its
$S_{\epsilon}$-predecessor and $S_{\epsilon}$-successor are of neighborhood
type $\tau_{0}$) or when they are the elements which make the transition
between two frequent neighborhood types (that is, one is $x_{i}^{\text{max}}$
and the other is $x_{i+1[m]}^{\text{min}}$, for some $i<m$):

######  Lemma 8.

We have the following:

  * •

$\forall x,y\in G_{1}$ such that $(x,y)\in S_{1}$ and ($x\notin R_{0}$ and
$y\notin R_{0}$) and ($x\notin P_{0}$ or $y\notin P_{0}$), then
$\text{tp}_{\mathcal{G}_{1}}^{r}(x)=\text{tp}_{\mathcal{G}_{1}}^{r}(y)$

  * •

$\forall x,y\in G_{2}$ such that $(x,y)\in S_{2}$ and ($x\notin h(R_{0})$ and
$y\notin h(R_{0})$) and ($x\notin h(P_{0})$ or $y\notin h(P_{0})$), then
$\text{tp}_{\mathcal{G}_{2}}^{r}(x)=\text{tp}_{\mathcal{G}_{2}}^{r}(y)$

######  Proof 4.4.

The property clearly holds at the end of Algorithm 2 and Algorithm 3.

For any $i$ from $0$ to $m-1$, the only $S_{1}$-edges (resp. $S_{2}$-edges)
that are added during the $i$-th loop are between two nodes of neighborhood
type $\tau_{i}$.

Recall the discussion at the beginning of Section 3. We now prove that, as
long as an element is far from any occurrence of a rare neighborhood type and
from the elements that make the transition between two frequent neighborhood
types, its neighborhood type in $(\mathcal{G}_{\epsilon},S_{\epsilon})$ is the
fractal of its neighborhood type in $\mathcal{G}_{\epsilon}$:

######  Lemma 9.

For $\epsilon\in\\{1,2\\}$ and for every $0\leq k\leq r$ and $x\notin R_{\leq
k}\cup P_{\leq k}$ (if $\epsilon=1$) or $x\notin h(R_{\leq k}\cup P_{\leq k})$
(if $\epsilon=2$),

$\text{tp}_{(\mathcal{G}_{\epsilon},S_{\epsilon})}^{k}(x)=[\text{tp}_{\mathcal{G}_{\epsilon}}^{k}(x)]_{k}\,.$

######  Proof 4.5.

We prove the result by induction on $k$. For $k=0$, there is nothing to do but
note that no edge $S_{\epsilon}(x,x)$ has been created.

Suppose that we have proven the result for some $k<r$, and let $x\notin
R_{\leq k+1}\cup P_{\leq k+1}$, or $x\notin h(R_{\leq k+1}\cup P_{\leq k+1})$.

Let $y$ be such that $\text{dist}_{\mathcal{G}_{\epsilon}}(x,y)=d$, for some
$1\leq d\leq k+1$. By construction of the $R_{i}$ and $P_{i}$, and of $h$, we
have that $y\notin R_{\leq k+1-d}\cup P_{\leq k+1-d}$, or $y\notin h(R_{\leq
k+1-d}\cup P_{\leq k+1-d})$ (this is easily shown by induction on $d$). Hence,
$\text{tp}_{(\mathcal{G}_{\epsilon},S_{\epsilon})}^{k+1-d}(y)=[\text{tp}_{\mathcal{G}_{\epsilon}}^{k+1-d}(y)]_{k+1-d}$.

Because Lemma 7 ensures that the $(k+1)$-neighborhood of $x$ in
$(\mathcal{G}_{\epsilon},S_{\epsilon})$ is layered, it only remains to show
that the $S_{\epsilon}$-successor $x^{+}$ and predecessor $x^{-}$ of $x$ are
such that
$\text{tp}_{(\mathcal{G}_{\epsilon},S_{\epsilon})}^{k}(x^{+})=\text{tp}_{(\mathcal{G}_{\epsilon},S_{\epsilon})}^{k}(x^{-})=[\text{tp}_{\mathcal{G}_{\epsilon}}^{k}(x)]_{k}$.
Let us show this for $x^{+}$.

Lemma 8 ensures
$\text{tp}_{\mathcal{G}_{\epsilon}}^{r}(x^{+})=\text{tp}_{\mathcal{G}_{\epsilon}}^{r}(x)$.
It only remains to note that $x^{+}\notin R_{\leq k}\cup P_{\leq k}$, or
$x^{+}\notin h(R_{\leq k}\cup P_{\leq k})$, and the induction hypothesis
allows us to conclude.

When we first defined $h$, it preserved $r$-neighborhood types by
construction. The last step before we are able to conclude the proof of
Theorem 1 is to make sure that $h$ still preserves $r$-neighborhood types,
taking into account the $S_{\epsilon}$-edges added during the run of Algorithm
4:

######  Lemma 10.

$\forall x\in
A_{1},\text{tp}_{(\mathcal{G}_{2},S_{2})}^{r}(h(x))=\text{tp}_{(\mathcal{G}_{1},S_{1})}^{r}(x)$

######  Proof 4.6.

We prove by induction on $0\leq k\leq r$ that $\forall x\in
A_{1},\text{tp}_{(\mathcal{G}_{2},S_{2})}^{k}(h(x))=\text{tp}_{(\mathcal{G}_{1},S_{1})}^{k}(x)$

There is nothing to prove for $k=0$.

Moving from $k$ to $k+1$, let $x\in A_{1}$ and let $y$ be such that
$\text{dist}_{\mathcal{G}_{1}}(x,y)=d$, for some $1\leq d\leq k+1$. Note that
$y\in B$, hence it has an image by $h$.

If $y\in A_{1}$, the induction hypothesis allows us to conclude that

$\text{tp}_{(\mathcal{G}_{2},S_{2})}^{k+1-d}(h(y))=\text{tp}_{(\mathcal{G}_{1},S_{1})}^{k+1-d}(y)\,.$

Else, Lemma 9 ensures that:

$\text{tp}_{(\mathcal{G}_{2},S_{2})}^{r}(h(y))=[\text{tp}_{\mathcal{G}_{2}}^{r}(h(y))]_{r}=[\text{tp}_{\mathcal{G}_{1}}^{r}(y)]_{r}=\text{tp}_{(\mathcal{G}_{1},S_{1})}^{r}(y)\,.$

In both cases,
$\text{tp}_{(\mathcal{G}_{2},S_{2})}^{k+1-d}(h(y))=\text{tp}_{(\mathcal{G}_{1},S_{1})}^{k+1-d}(y)$.

Because of (Layer[$r$]), it only remains to show that the
$S_{\epsilon}$-successors of $x$ and $h(x)$, as well as their
$S_{\epsilon}$-predecessors, have the same $k$-neighborhood type in
$(\mathcal{G}_{\epsilon},S_{\epsilon})$. Let us prove this for the successors,
respectively named $x^{+}$ and $h(x)^{+}$.

If $x^{+}\in A_{1}$, then by construction $h(x)^{+}=h(x^{+})$, and the
induction hypothesis allows us to conclude.

Otherwise, $x^{+}\notin A_{1}$ and $h(x)^{+}\notin A_{2}$. Under this
hypothesis, Lemma 8 ensures that

$\text{tp}_{\mathcal{G}_{2}}^{r}(h(x)^{+})=\text{tp}_{\mathcal{G}_{2}}^{r}(h(x))=\text{tp}_{\mathcal{G}_{1}}^{r}(x)=\text{tp}_{\mathcal{G}_{1}}^{r}(x^{+})\,.$

Now, Lemma 9 ensures that

$\text{tp}_{(\mathcal{G}_{2},S_{2})}^{r}(h(x)^{+})$ | $=$ | $[\text{tp}_{\mathcal{G}_{2}}^{r}(h(x)^{+})]_{r}$
---|---|---
| $=$ | $[\text{tp}_{\mathcal{G}_{1}}^{r}(x^{+})]_{r}$
| $=$ | $\text{tp}_{(\mathcal{G}_{1},S_{1})}^{r}(x^{+})\,.$

###  4.9. Conclusion of the proof

We recall Theorem 1, whose proof we are now able to conclude:

See 1

Let $\alpha\in\mathbb{N}$. We want to prove that there exists some
$f(\alpha)\in\mathbb{N}$ such that for any $\Sigma$-structures
$\mathcal{G}_{1},\mathcal{G}_{2}$ of degree at most $d$,

$\mathcal{G}_{1}\equiv^{\textsc{FO}}_{f(\alpha)}\mathcal{G}_{2}\quad\text{entails}\quad\mathcal{G}_{1}\equiv^{{\textup{Succ-
inv }\textsc{FO}}}_{\alpha}\mathcal{G}_{2}\,.$ (1)

Indeed, this means that on the class of $\Sigma$-structures of degree at most
$d$, any equivalence class $\mathcal{C}$ for $\equiv^{{\textup{Succ-inv
}\textsc{FO}}}_{\alpha}$ is a finite union of equivalence classes for
$\equiv^{\textsc{FO}}_{f(\alpha)}$, and is consequently definable by an FO-
sentence $\varphi_{\mathcal{C}}$ of quantifier rank $f(\alpha)$. Let now
$\mathcal{P}$ be a property of structures of degree at most $d$ definable by a
sentence of Succ-inv FO of quantifier rank at most $\alpha$. It is a finite
union $\bigcup_{i}\mathcal{C}_{i}$ of equivalence classes for
$\equiv^{{\textup{Succ-inv }\textsc{FO}}}_{\alpha}$. Hence, the
$\textsc{FO}[f(\alpha)]$-sentence $\bigvee_{i}\varphi_{\mathcal{C}_{i}}$
defines $\mathcal{P}$.

This proves the inclusion $\textup{Succ-inv }\textsc{FO}\subseteq\textsc{FO}$
on structures of degree at most $d$.

In order to prove (1), we need $f(\alpha)$ to be large enough so as to enable
us, given

$\mathcal{G}_{1}\equiv^{\textsc{FO}}_{f(\alpha)}\mathcal{G}_{2}\,,$

to construct two successor relations $S_{1}$ and $S_{2}$ such that

$(\mathcal{G}_{1},S_{1})\equiv^{\textsc{FO}}_{\alpha}(\mathcal{G}_{2},S_{2})\,,$
(2)

which in turn ensures that

$\quad\mathcal{G}_{1}\equiv^{{\textup{Succ-inv
}\textsc{FO}}}_{\alpha}\mathcal{G}_{2}\,.$

Now, the Hanf threshold theorem yields two integers $r$ and $t$, depending on
$\alpha$ and $d$, such that

$[\\![(\mathcal{G}_{1},S_{1})]\\!]_{r}=^{t}[\\![(\mathcal{G}_{2},S_{2})]\\!]_{r}$
(3)

entails (2).

We have seen throughout this section how to construct two successor relations
$S_{1}$ and $S_{2}$. All that remains is for us to show that, for the right
value of $g$ in Lemma 5, our construction guarantees (3).

Let $\tau$ be an $r$-neighborhood type over $\Sigma\cup\\{S\\}$ which occurs
in $(\mathcal{G}_{1},S_{1})$. There are two cases to consider:

  * •

if $\tau$ occurs outside of $A_{1}$, then Lemma 9 ensures that
$\tau=[\chi]_{r}$ for some frequent $r$-neighborhood type $\chi$. We can
choose $g$ so that $\chi$ is guaranteed to have at least $t$ occurrences in
$\mathcal{G}_{1}$ outside of $A_{1}$, and in $\mathcal{G}_{2}$ outside of
$A_{2}$. This is ensured as long as

$g(\beta)\geq|A_{1}|+t\,,$

and in particular when

$g(\beta)\geq(\beta+2t_{r}^{d})N(d+2,r)+t\,.$

Lemma 9 then ensures that $\tau$ occurs at least $t$ times both in
$(\mathcal{G}_{1},S_{1})$ and in $(\mathcal{G}_{2},S_{2})$.

  * •

if $\tau$ occurs only in $A_{1}$, then it cannot occur in
$(\mathcal{G}_{2},S_{2})$ outside of $A_{2}$ (for the same reasons as above).
Lemma 10 guarantees that $\tau$ has the same number of occurrences in $A_{1}$
and in $A_{2}$, hence in $(\mathcal{G}_{1},S_{1})$ and in
$(\mathcal{G}_{2},S_{2})$.

As long as $g$ satisfies these conditions, (3) holds. We are now able to fix
the value of $f(\alpha)$ as prescribed by Lemma 5 for this $g$. This concludes
the proof of Theorem 1.

##  5\. Conclusion

We have shown that Succ-inv FO collapses to FO on any class of bounded degree.
In other words, we have shown that there exists a translation from Succ-inv FO
to FO on classes of bounded degree. As given by our proof, the quantifier rank
of the translated sentence is triple-exponential in the quantifier rank of the
original formula. It is an easy exercise to prove that the blowup is at least
exponential, but we do not know if an exponential translation is at all
possible.

Similar considerations arise when we take into account the length of the
sentences instead of their quantifier rank - in this regard, our construction
is even non-elementary, and all we know is that the blowup is at least
exponential.

An interesting task would be (i) to give an effective translation and (ii) to
improve the succinctness of this translation, or to give tighter lower bounds
on such translations.

Apart from these considerations, there are two main directions in which one
could look to extend the present result. One possibility would be to keep
looking at classes of bounded degree while climbing up in the ladder of
expressivity, and ask whether $<\\!\textup{-inv }$FO collapses to FO as well
on these classes of structures. New techniques would be needed, as contrary to
what was the case with a successor, the addition of an order does not preserve
the bounded degree property. Furthermore, even if $<\\!\textup{-inv
}\textsc{FO}=\textsc{FO}$ in this setting, it is not clear whether such orders
can be directly constructed. It may be necessary to construct, as in [BS09], a
chain of intermediate structures and orders.

Alternatively, we could change the setting, and study the expressivity of
Succ-inv FO on other sparse classes of structures, e.g., on classes of bounded
treewidth. If showing the collapse of Succ-inv FO to FO on these classes
proved itself to be out of reach, a possibility would be to aim at proving
that Succ-inv FO is Hanf-local (which would be stronger than the known
Gaifman-locality). In that case, the starting hypothesis on the structures
$\mathcal{G}_{1}$ and $\mathcal{G}_{2}$ would be stronger, as the existence of
a $k$-neighborhood type-preserving bijection between the two structures would
be assumed.

These tasks are much harder without any bound on the degree, which was what
guaranteed that we could find elements of a given frequent neighborhood type
far from each other.

## Acknowledgment

The author wishes to thank Luc Segoufin as well as the anonymous referees for
their most appreciated feedback.

## References

  * [BS09] Michael Benedikt and Luc Segoufin.  Towards a characterization of order-invariant queries over tame graphs.  J. Symb. Log., 2009.
  * [EEH14] Kord Eickmeyer, Michael Elberfeld, and Frederik Harwath.  Expressivity and succinctness of order-invariant logics on depth-bounded structures.  In Mathematical Foundations of Computer Science (MFCS) - 39th International Symposium, 2014.
  * [EFG16] Michael Elberfeld, Marlin Frickenschmidt, and Martin Grohe.  Order invariance on decomposable structures.  In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS, 2016.
  * [FSV95] Ronald Fagin, Larry J. Stockmeyer, and Moshe Y. Vardi.  On monadic NP vs. monadic co-np.  Inf. Comput., 1995.
  * [GKS17] Martin Grohe, Stephan Kreutzer, and Sebastian Siebertz.  Deciding first-order properties of nowhere dense graphs.  J. ACM, 2017.
  * [GS00] Martin Grohe and Thomas Schwentick.  Locality of order-invariant first-order formulas.  ACM Trans. Comput. Log., 2000.
  * [GS20] Julien Grange and Luc Segoufin.  Order-Invariant First-Order Logic over Hollow Trees.  In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Schloss Dagstuhl, 2020.
  * [Lib04] Leonid Libkin.  Elements of Finite Model Theory.  Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004\.
  * [Ros07] Benjamin Rossman.  Successor-invariant first-order logic on finite structures.  J. Symb. Log., 2007.
  * [See96] Detlef Seese.  Linear time computable problems and first-order descriptions.  Math. Struct. Comput. Sci., 1996.
  * [Tra50] Boris A Trakhtenbrot.  Impossibility of an algorithm for the decision problem in finite classes.  Doklady Akademii Nauk SSSR, 1950.
  * [vdHKP+17] Jan van den Heuvel, Stephan Kreutzer, Michal Pilipczuk, Daniel A. Quiroz, Roman Rabinovich, and Sebastian Siebertz.  Model-checking for successor-invariant first-order formulas on graph classes of bounded expansion.  In LICS, 2017.