15414 LABEL:LastPageFeb. 27, 2018Dec. 11, 2019

# Definable isomorphism problem

Khadijeh Keshvardoosta  aDepartment of Mathematics, Velayat University,
Iranshahr, Iran  ,  Bartek Klinb  bUniversity of Warsaw  ,  Sławomir Lasotab
cCNRS, LaBRI, Université de Bordeaux  ,  Joanna Ochremiakc  and  Szymon
Toruńczykb

###### Abstract.

We investigate the isomorphism problem in the setting of definable sets
(equivalent to sets with atoms): given two definable relational structures,
are they related by a definable isomorphism? Under mild assumptions on the
underlying structure of atoms, we prove decidability of the problem. The core
result is parameter-elimination: existence of an isomorphism definable with
parameters implies existence of an isomorphism definable without parameters.

###### Key words and phrases:

isomorphism problem, definable sets, $\omega$-categoricity

This work has been partially supported by the ERC project ‘Lipa’ within the EU
Horizon 2020 research and innovation programme, No. 683080 (the second
author), the NCN grant 2016/21/B/ST6/01505 (the third author) and the NCN
grant 2016/21/D/ST6/01485 (the fifth author).

##  1\. Introduction

We consider _hereditarily first-order definable sets_ , which are usually
infinite, but can be finitely described and are therefore amenable to
algorithmic manipulation. We drop the qualifiers _herediatarily first-order_ ,
and simply call them definable sets in what follows. They are parametrized by
a fixed underlying relational structure $\mathsf{Atoms}$ whose elements are
called _atoms_.

######  Example .

Let $\mathsf{Atoms}$ be a countable set $\\{\underline{1\mkern-1.0mu}\mkern
1.0mu,\underline{2\mkern-1.0mu}\mkern 1.0mu,\underline{3\mkern-1.0mu}\mkern
1.0mu,\ldots\\}$ equipped with the equality relation only; we shall call this
structure the pure set. Let

$\displaystyle V$
$\displaystyle=\left\\{\,\\{a,b\\}\,|\,a,b\in\mathsf{Atoms},a\neq
b\,\right\\},$ $\displaystyle E$
$\displaystyle=\left\\{\,(\\{a,b\\},\\{c,d\\})\,|\,a,b,c,d\in\mathsf{Atoms},a\neq
b\wedge a\neq c\wedge a\neq d\wedge b\neq c\wedge b\neq d\wedge c\neq
d\,\right\\}.$

Both $V$ and $E$ are definable sets (over $\mathsf{Atoms}$), as they are
constructed from $\mathsf{Atoms}$ using (possibly nested) set-builder
expressions with first-order guards ranging over $\mathsf{Atoms}$. In general,
we allow finite unions in the definitions, and finite tuples (as above) are
allowed for notational convenience. Precise definitions are given in Section
2. The pair $G=(V,E)$ is also a definable set, in fact, a definable graph. It
is an infinite Kneser graph (a generalization of the famous Petersen graph):
its vertices are all two-element subsets of $\mathsf{Atoms}$, and two such
subsets are adjacent iff they are disjoint.

The graph $G$ is $\emptyset$-definable: its definition does not refer to any
particular elements of $\mathsf{Atoms}$. In general, one may refer to a finite
set of parameters $S\subseteq\mathsf{Atoms}$ to describe an _$S$ -definable_
set. For instance, the set
$\left\\{\,a\,|\,a\in\mathsf{Atoms},a\neq\underline{1\mkern-1.0mu}\mkern
1.0mu\land a\neq\underline{2\mkern-1.0mu}\mkern 1.0mu\,\right\\}$ is
$\\{\underline{1\mkern-1.0mu}\mkern 1.0mu,\underline{2\mkern-1.0mu}\mkern
1.0mu\\}$-definable. Definable sets are those which are $S$-definable for some
finite $S\subseteq\mathsf{Atoms}$. ∎

We remark that in the pure set $\mathsf{Atoms}$, every first-order formula is
effectively equivalent to a quantifier-free formula, via a simple quantifier-
elimination procedure. Thus, as long as complexity issues are ignored and
decidability is the only concern, in the case of the pure set, we can safely
restrict to quantifier-free formulas, however, in general, definable sets may
include arbitrary first-order formulas.

A definable function $f:X\to Y$ is simply a function whose domain $X$,
codomain $Y$, and graph $\Gamma(f)\subseteq X\times Y$ are definable sets. A
relational structure is definable if its signature, universe, and
interpretation function that maps each relation symbol to a relation on the
universe, are definable111A structure over a finite signature is definable in
$\mathsf{Atoms}$ if and only if it is interpretable in $\mathsf{Atoms}$, in
the model-theoretic sense.. Finally, a definable isomorphism between definable
structures over the same signature is a definable bijective mapping between
their universes that preserves and reflects every relation in the signature.
Likewise one introduces, e.g., definable homomorphisms. All hereditarily
finite sets (finite sets, whose elements are finite, and so on, recursively)
are definable, and every finite relational structure over a finite signature
is (isomorphic to) a definable one.

### Contribution

The classical isomorphism problem asks whether two given _finite_ structures
are isomorphic. In this paper, we consider its counterpart in the setting of
definable sets (the problem is called _definable isomorphism problem_ in the
sequel): given two definable structures ${\mathbb{A}},{\mathbb{B}}$ over the
same definable signature $\Sigma$, all over the same fixed structure
$\mathsf{Atoms}$, are they related by a definable isomorphism? Note that
definable structures can be meaningfully considered as input to a
computational problem since they are finitely described using the set-builder
notation and first-order formulas in the language of $\mathsf{Atoms}$. The
structure $\mathsf{Atoms}$ is considered here in a parametric manner, not as a
part of input: every structure $\mathsf{Atoms}$ induces a different decision
problem.

As our main result we prove, under a certain assumptions on the structure
$\mathsf{Atoms}$, that the definable isomorphism problem is decidable. The key
technical difficulty is to show that every two $S$-definable structures
related by a definable isomorphism are also related by an $S$-definable one.
(When $S=\emptyset$ this is parameter elimination: existence of an isomorphism
defined with parameters enforces existence of one defined without parameters.)
Having this, the problem reduces to testing whether two $S$-definable
structures are related by an $S$-definable isomorphism, which in turn reduces
to the first-order satisfiability problem in $\mathsf{Atoms}$.

As witnessed by Example 2 below, existence of an isomorphism does not
guarantee existence of a definable one. Therefore we do not solve the
_isomorphism problem_ for definable structures, which asks whether two given
definable structures (over the same signature) are isomorphic. In fact, the
decidability status of the latter problem remains an intriguing open question,
even for $\mathsf{Atoms}$ being the pure set.

### Motivation and related work

This paper is part of a programme aimed at generalizing classical decision
problems (for instance the homomorphism problem, studied recently in [KKOT15,
KLOT16]), and computation models such as automata [BKL14], Turing machines
[BKLT13, KLOT14] and programming languages [BBKL12, BT12, KS16, KT16], to sets
with atoms. For other applications of sets with atoms (called there nominal
sets) in computing, see [Pit13].

Isomorphism testing is at the core of many decision problems in combinatorics
and logic. In case of finite graphs it is well known to be solvable in NP, and
since recently in quasi-polynomial time [Bab16]. Whether it can be solved in P
is still an extremely challenging open question, and only special cases are
shown so by now, e.g. [Luk82].

### Acknowledgement

We are grateful to Pierre Simon for valuable discussions.

##  2\. Preliminaries

Throughout the paper, fix a countable relational structure $\mathsf{Atoms}$,
whose elements are called _atoms_. We overload the notation and use the symbol
$\mathsf{Atoms}$ both for the relational structure and for the set of its
elements, hoping that this does not lead to confusion. We assume that the
vocabulary of $\mathsf{Atoms}$ is finite. We shall now formally introduce the
notion of definable sets over $\mathsf{Atoms}$, following [KT17, KKOT15,
KLOT16].

### Definable sets

An _expression_ is either a variable (from some fixed infinite set or
variables), or a formal finite union (including the empty union $\emptyset$)
of set-builder expressions of the form

$\displaystyle\left\\{\,e\,|\,a_{1},\ldots,a_{n}\in\mathsf{Atoms},\phi\,\right\\},$
(1)

where $e$ is an expression, $a_{1},\ldots,a_{n}$ are pairwise different
variables, and $\phi$ is a first-order formula over the signature of
$\mathsf{Atoms}$. The variables $a_{1},\ldots,a_{n}$ are considered bound in
$e$ and $\phi$. The free variables in (1) are those free variables of $e$ and
of $\phi$ which are not among $a_{1},\ldots,a_{n}$.

For an expression $e$ with free variables $V$, any valuation
$\mathrm{val}:V\to\mathsf{Atoms}$ defines in an obvious way a value
$X=e[\mathrm{val}]$, which is either an atom or a set, formally defined by
induction on the structure of $e$. We then say that $X$ is a _definable set
over $\mathsf{Atoms}$_, and that it is _defined_ by $e$ with $\mathrm{val}$.
When the structure $\mathsf{Atoms}$ is obvious from the context, we simply
speak of _definable sets_ without explicitly specifying $\mathsf{Atoms}$. Note
that one set $X$ can be defined by many different expressions. Finally,
observe that the family of definable sets is hereditary: every element of a
definable set is a definable set (or an atom).

Sometimes we want to emphasize those atoms that appear in the image of the
valuation $\mathrm{val}:V\to\mathsf{Atoms}$. For any finite set
$S\subseteq\mathsf{Atoms}$ of atoms with $\mathrm{val}(V)\subseteq S$ we say
that $X$ is _$S$ -definable_. Clearly, an $S$-definable set is also
$T$-definable whenever $S\subseteq T$.

As syntactic sugar, we allow atoms to occur directly in set expressions (these
atoms are called _parameters_). For example, what we write as the
$\\{\underline{1\mkern-1.0mu}\mkern 1.0mu\\}$-definable set $\\{a\ |\
a\in\mathsf{Atoms},a\neq\underline{1\mkern-1.0mu}\mkern 1.0mu\\}$ is formally
defined by the expression $\\{a\ |\ a\in\mathsf{Atoms},a\neq b\\}$, together
with a valuation mapping $b$ to $\underline{1\mkern-1.0mu}\mkern 1.0mu$. With
this syntactic sugar, a definable set is determined by a sole expression $e$
with parameters, but without valuation.

As a notational convention, when writing set-builder expressions (1) we omit
the formula $\phi$ when it is trivially true, and omit the enumeration
$a_{1},\ldots,a_{n}\in\mathsf{Atoms}$ when $n=0$. This allows us, in
particular, to write singletons, like $\\{\underline{1\mkern-1.0mu}\mkern
1.0mu\\}$.

######  Remark .

To improve readability, it will be convenient to use standard set-theoretic
encodings to allow a more flexible syntax. In particular, ordered pairs and
tuples can be encoded e.g. by Kuratowski pairs,
$(x,y)=\\{\\{x,y\\},\\{x\\}\\}$. We will also consider definable infinite
families of symbols, such as $\\{R_{x}:x\in X\\}$, where $R$ is a symbol and
$X$ is a definable set. Formally, such a family can be encoded as the set of
ordered pairs $\\{R\\}\times X$, where the symbol $R$ is represented by some
$\emptyset$-definable set, e.g. $\emptyset$ or $\\{\emptyset\\}$. Here we use
the fact that definable sets (over any fixed atoms) are closed under Cartesian
products.

### Definable relational structures

Any object in the set-theoretic universe (a relation, a function, a relational
structure, etc.) may be definable. For example, a definable relation on $X,Y$
is a relation $R\subseteq X\times Y$ which is a definable set of pairs, and a
definable function $X\to Y$ is a function whose graph is definable. Along the
same lines, a definable relational signature is a definable set of _symbols_
$\Sigma$, partitioned into definable sets
$\Sigma=\Sigma_{1}\uplus\Sigma_{2}\uplus\ldots\uplus\Sigma_{l}$ according to
the arity of symbols. We say that $\sigma$ has _arity_ $r$ if
$\sigma\in\Sigma_{r}$, and $l\in\mathbb{N}$ is thus the maximal arity of a
symbol in $\Sigma$.

For a signature $\Sigma$, a definable $\Sigma$-structure ${\mathbb{A}}$
consists of a definable universe $A$ and a definable interpretation function
which assigns a relation $\sigma^{{\mathbb{A}}}\subseteq A^{r}$ to each
relation symbol $\sigma\in\Sigma$ of arity $r$. (We denote structures using
blackboard font, and their universes using the corresponding symbol in
italics). More explicitly, such a structure can be represented by the tuple
${\mathbb{A}}=(A,I_{1},\ldots,I_{l})$ where
$I_{r}=\\{(\sigma,a_{1},\ldots,a_{r})\ |\
\sigma\in\Sigma_{r},(a_{1},\ldots,a_{r})\in\sigma^{{\mathbb{A}}}\\}$ is a
definable set for $r=1,\ldots,l$. It is not difficult to see that the
interpretation $\sigma^{{\mathbb{A}}}$ of every fixed symbol $\sigma\in\Sigma$
is definable.

######  Remark .

As argued in [KLOT16], definable structures over finite signatures coincide,
up to definable isomorphism, with _first-order interpretations with
parameters_ in $\mathsf{Atoms}$, in the sense of model theory [Hod93]. ∎

######  Example .

The graph $G$ from Example 1 is a definable (over $\mathsf{Atoms}$ being the
pure set) structure over a finite signature $\Sigma$ containing a single
binary relation symbol. To give an example of a definable structure over an
infinite definable signature, extend $G$ to a structure ${\mathbb{A}}$ by
infinitely many unary predicates representing the neighborhoods of each vertex
of $G$. To this end, define the signature
$\Sigma=\\{E\\}\cup\left\\{\,N_{v}\,|\,v\in V\,\right\\}$, where
$V=\left\\{\,\\{a,b\\}\,|\,a,b\in\mathsf{Atoms},a\neq b\,\right\\}$ is the
vertex set of $G$ and $N$ is a symbol (cf. Remark 2). The interpretation of
$N_{v}$ is specified by the set $I_{1}=\left\\{\,(N_{v},w)\,|\,(v,w)\in
E\,\right\\}$ (where $E$ is defined by the expression from Example 1). ∎

### Representing the input

Definable relational structures can be input to algorithms, as they are
finitely presented by expressions defining the signature, the universe, and
the interpretation function. If the input is an $S$-definable set $X$ defined
by an expression $e$ with parameters $a_{1},\ldots,a_{n}\in S$, then we also
need to represent the tuple $a_{1},\ldots,a_{n}$ of atoms. For example, in the
case of pure set $\mathsf{Atoms}$ these elements can be represented as
arbitrary pairwise distinct numbers.

### Definable isomorphism problem

Let the structure of atoms be fixed and denoted by $\mathsf{Atoms}$. Recall
that a definable function $f:X\to Y$ is a function whose graph
$\Gamma(f)\subseteq X\times Y$ is a definable set. A definable isomorphism
between definable structures ${\mathbb{A}}$, ${\mathbb{B}}$ over the same
signature $\Sigma$ is a definable bijective function $h:A\to B$ between their
universes that preserves and reflects every relation in the signature: for
every $\sigma\in\Sigma$ of arity $r$ and every $r$-tuple
$a_{1},\ldots,a_{r}\in A$ of elements of ${\mathbb{A}}$,
$(a_{1},\ldots,a_{r})\in\sigma^{{\mathbb{A}}}$ if, and only if
$(h(a_{1}),\ldots,h(a_{r}))\in\sigma^{{\mathbb{B}}}$. Likewise one can also
introduce definable homomorphisms, embeddings, etc.

We focus in this paper on the following family of decision problems (note that
the structure $\mathsf{Atoms}$ is fixed, and not part of input, and hence
every choice of $\mathsf{Atoms}$ yields a different decision problem):

Problem: Definable-isomorphism($\mathsf{Atoms}$)
Input: A definable signature $\Sigma$ and two definable $\Sigma$-structures
${\mathbb{A}}$ and ${\mathbb{B}}$.
Decide: Is there a definable isomorphism from ${\mathbb{A}}$ to
${\mathbb{B}}$?

######  Example .

Imposing the definability requirement on isomorphisms clearly does matter. Let
$\mathsf{Atoms}$ be the pure set again, and consider the following two
$\emptyset$-definable graphs, each of them being an infinite, edgeless graph:

$\displaystyle V_{1}$
$\displaystyle=\left\\{\,a\,|\,a\in\mathsf{Atoms}\,\right\\}=\mathsf{Atoms}$
$\displaystyle V_{2}$
$\displaystyle=\left\\{\,\\{a,b\\}\,|\,a,b\in\mathsf{Atoms},a\neq
b\,\right\\},$ $\displaystyle E_{1}$ $\displaystyle=\emptyset$ $\displaystyle
E_{2}$ $\displaystyle=\emptyset.$

The two graphs are clearly isomorphic. On the other hand there is no
_definable_ isomorphism between them, simply because there is no definable
bijection between $V_{1}$ and $V_{2}$, as we will argue in Example 5 in
Section 5. ∎

In this paper, we will always assume that the structure $\mathsf{Atoms}$ is
$\omega$-categorical. We will also make assumptions regarding computability
properties, least supports and denseness, as introduced below.

###  $\omega$-categoricity

We say that a countable structure $\mathsf{Atoms}$ is _$\omega$ -categorical_
if any countable structure $\mathsf{Atoms}^{\prime}$ which satisfies the same
first-order sentences as $\mathsf{Atoms}$ is isomorphic to $\mathsf{Atoms}$.
The following fundmanental theorem, due to Ryll-Nardzewski, Engeler and
Svenonius [Eng59, RN59, Sve59], gives a useful characterization of
$\omega$-categorical structures in terms of their automorphism groups. Below,
automorphisms act on the set $\mathsf{Atoms}^{n}$ of all $n$-tuples of
elements of $\mathsf{Atoms}$ in a coordinatewise fashion. For each $n\geq 1$,
the set $\mathsf{Atoms}^{n}$ is partitioned into the orbits of this action.

######  Theorem .

A structure $\mathsf{Atoms}$ is $\omega$-categorical if, and only if for each
$n$, the automorphism group of $\mathsf{Atoms}$ induces finitely many orbits
on the set $\mathsf{Atoms}^{n}$. Moreover, if $\mathsf{Atoms}$ is
$\omega$-categorical, then each orbit of this action can be defined by a
first-order formula with $n$ free variables.

Examples of $\omega$-categorical structures include:

  * •

the pure set;

  * •

the dense total order $(\mathbb{Q},\leq)$ of rational numbers;

  * •

the universal (random) graph (the Fraïssé limit of all finite graphs [Fra53]);

  * •

the universal partial order (the Fraïssé limit of all finite partial orders);

  * •

a countable vector space over a finite field.

All the structures considered in this paper as atoms are assumed to be
$\omega$-categorical.

### Effectivity

We will additionally impose certain computability assumptions on
$\mathsf{Atoms}$. First, we fix an encoding of elements of $\mathsf{Atoms}$ as
strings, i.e., a surjection from $\\{0,1\\}^{*}$ to $\mathsf{Atoms}$.
Similarly, we fix an encoding of the symbols in the signature of
$\mathsf{Atoms}$ as strings. This allows us to represent first-order formulas,
together with valuations of their free variables, as strings. We then assume
that $\mathsf{Atoms}$ has a decidable first-order theory, i.e., there is an
algorithm which inputs a first-order formula, together with a valuation of its
free variables in $\mathsf{Atoms}$, and determines whether the valuation
satisfies the formula in $\mathsf{Atoms}$. We remark that decidability of the
first-order theory of $\mathsf{Atoms}$ implies (and is equivalent to) the
existence of an algorithm which inputs two expressions describing definable
sets $x$ and $y$, and decides whether $x=y$. Lastly, we assume _computability
of the Ryll-Nardzewski function_ , which maps a given number $n$ to the number
of orbits of $\mathsf{Atoms}^{n}$. We say that a structure $\mathsf{Atoms}$ is
_effectively $\omega$-categorical_ if it is $\omega$-categorical, has a
decidable first-order theory, and its Ryll-Nardzewski function is computable.
Note that effective $\omega$-categoricity implies that there is an algorithm
which inputs a number $n$ and outputs the orbits of $\mathsf{Atoms}^{n}$, each
defined by a first-order formula with $n$ free variables.

### Automorphisms, partial automorphisms, and self-embeddings

Automorphisms of $\mathsf{Atoms}$ will be called _atom automorphisms_. For a
finite $S\subseteq\mathsf{Atoms}$, _atom $S$-automorphisms_ are those atom
automorphisms $\pi$ which fix all elements of $S$, i.e., $\pi(a)=a$ for every
$a\in S$. If $\pi$ is an atom automorphism and $x$ is a definable set, defined
by an expression $e$ with parameters $a_{1},\ldots,a_{n}$, then we define the
set $\pi x$ as the set defined by the same expression, and the parameters
$\pi(a_{1}),\ldots,\pi(a_{n})$.

A _partial automorphism_ 222also called a _partial elementary map_. of
$\mathsf{Atoms}$ is a partial bijection $f$ between two subsets of
$\mathsf{Atoms}$, such that for every first-order formula
$\phi(x_{1},\ldots,x_{k})$ and every tuple $a_{1},\ldots,a_{k}\in\text{Dom}f$,
$\phi(a_{1},\ldots,a_{k})$ holds in $\mathsf{Atoms}$ if, and only if
$\phi(f(a_{1}),\ldots,f(a_{k}))$ holds in $\mathsf{Atoms}$. In particular, an
automorphism is a partial automorphism whose domain and codomain are
$\mathsf{Atoms}$. A _self-embedding_ of $\mathsf{Atoms}$ is a partial
automorphism whose domain is $\mathsf{Atoms}$.

A partial automorphism is _finite_ if its domain is finite. The following
lemma is a consequence of the theorem of Ryll-Nardzewski, Engeler, and
Svenonius, specifically of the fact that two $n$-tuples of atoms are in the
same orbit if and only if they satisfy the same first-order formulas.

######  Lemma .

Every finite partial automorphism of an $\omega$-categorical structure extends
to an automorphism of that structure.

### Least supports

We say that a finite set $S\subseteq\mathsf{Atoms}$ _supports_ $x$ if every
$S$-automorphism $\pi$ fixes $x$, i.e., $\pi x=x$. Note that any $S$-definable
set $x$ is supported by $S$. We say that $\mathsf{Atoms}$ has _least supports_
if every definable set $x$ has a least (under inclusion) support. On the face
of it, admitting least supports is a rather complex condition333It can be
shown to be equivalent to the conjunction of _weak elimination of imaginaries_
and _trivial algebraic closure_ , which are well-studied notions in model
theory., in that its formulation relies on the notion of definable sets.
However, for $\omega$-categorical structures the existence of least supports
has an equivalent structural characterization in terms of $\mathsf{Atoms}$
itself, see in [BKL14, Thm. 9.3]. Examples of atoms with least supports
include:

  * •

the pure set,

  * •

the dense total order $(\mathbb{Q},\leq)$,

  * •

the random graph,

  * •

the universal homogeneous partial order.

######  Example .

An example which does not have least supports is an infinite-dimensional
vector space over a finite field. The idea is that any basis of a finite-
dimensional subspace is a support of that subspace, but there is no least
support.

More precisely, fix a finite field $\mathbb{K}$, e.g. the two-element field.
Let $V$ be a countable vector space over $\mathbb{K}$. A concrete example is
obtained by considering the set of all infinite sequences of elements of
$\mathbb{K}$, with finitely many non-zero elements, with coordinatewise
addition and multiplication by scalars.

We treat $V$ as a logical structure ${\mathbb{V}}$ equipped with the binary
addition operation $x,y\mapsto x+y$ and unary operations $x\mapsto c\cdot x$,
for each scalar $c\in\mathbb{K}$. Then, automorphisms of ${\mathbb{V}}$
correspond precisely to invertible linear maps of $V$. Clearly, the vector
space $V$ has countable dimension. By basic results of linear algebra, any two
countable-dimensional vector spaces over $\mathbb{K}$ are isomorphic. Hence,
${\mathbb{V}}$ is an $\omega$-categorical structure.

We argue that the structure ${\mathbb{V}}$, treated as atoms, does not have
least supports. Fix $k\geq 0$ and fix a $k$-dimensional subspace $W$ of $V$.
Then $W$ is a definable set, as it is finite (of cardinality
$|\mathbb{K}|^{k}$).

We claim that a finite set $S\subseteq\mathsf{Atoms}$ is a support of $W$ if,
and only if, $W$ is contained in the linear span of $S$. In one direction,
suppose that $W$ is contained in the linear span of $S$. In particular, every
element $w$ of $W$ can be expressed as a linear combination of elements of
$S$. Then, every linear automorphism of $V$ which fixes $S$ pointwise must fix
$w$. Since this applies to all $w\in W$, $W$ is fixed by all $S$-automorphisms
of ${\mathbb{V}}$.

Conversely, suppose that $W$ is not contained in the linear span of $S$, i.e.,
there is some element $w\in W$ which is not a linear combination of the
elements of $S$. Then there is a linear automorphism of $V$ which is the
identity on $S$ and maps $w$ to some element $w^{\prime}$ not in $W$ (we use
the fact that $V$ has infinite dimension and $S\cup W$ is finite).

In particular, a set $S\subseteq{\mathbb{V}}$ is a minimal support of $W$ if
and only if $S$ is a basis of $W$. Now, if $k>1$ then every space $W$ of
dimension $k$ has more than one basis444If $e_{1},e_{2},\ldots,e_{k}$ is a
basis then so is $e_{1}+e_{2},e_{2},\ldots,e_{k}$. If $k=1$ then $e_{1}$ and
$-e_{1}$ are distinct bases, unless $\mathbb{K}=2$. . In particular, $W$ has
multiple minimal supports, and hence has no least support.

### Denseness

We call the structure $\mathsf{Atoms}$ _dense_ if for all finite sets $T$ and
$S$, where $T\subseteq S\subseteq\mathsf{Atoms}$, there is a self-embedding
$H$ which fixes $T$ pointwise, such that every automorphism of
$H(\mathsf{Atoms})$ extends to an atom $S$-automorphism. All the structures
mentioned above are dense.

##  3\. Parameter elimination

The main property that will ensure the decidability of the definable
isomorphism problem is the following _parameter elimination property_ :

> If two $T$-definable relational structures ${\mathbb{A}}$ and ${\mathbb{B}}$
> are related by a definable isomorphism, then they are also related by a
> $T$-definable one.

Roughly speaking, the lemma says that in a definition of an isomorphism
between $T$-definable structures, one can eliminate parameters outside of $T$,
possibly at the price of modifying the isomorphism. The following example
shows that even in very simple situations, constructing a $T$-definable
isomorphism from a given definable one may be nontrivial.

######  Example .

Let $\mathsf{Atoms}$ be the pure set, put $T=\emptyset$, and consider sets
(qua relational structures over the empty vocabulary):

${\mathbb{A}}={\mathbb{B}}=\mathsf{Atoms}^{2}+\mathsf{Atoms}.$

Fix an atom $c\in\mathsf{Atoms}$, and define $f:{\mathbb{A}}\to{\mathbb{B}}$
by:

$f(a)=(a,c),\qquad f(a,c)=a,\qquad f(a,b)=(a,b)$

for every $a\in\mathsf{Atoms}$ and $b\in\mathsf{Atoms}-\\{c\\}$. This is a
$\\{c\\}$-definable bijection between ${\mathbb{A}}$ and ${\mathbb{B}}$ which
needs to be “smoothed out” to yield a $\emptyset$-definable one (in this case,
e.g. the identity function). Note that this requires altering $f$ even at some
arguments that do not contain $c$ in their supports.

To prove parameter elimination, even for atoms being the pure set, in Section
6 we will provide an iterative procedure for “smoothing out isomorphisms” by
gradual elimination of parameters. This is the main technical result of this
paper. More precisely, we prove:

######  Theorem .

Any dense, $\omega$-categorical structure $\mathsf{Atoms}$ with least supports
has the parameter elimination property.

Theorem 3 is proved in Section 6. We now show how the parameter elimination
property yields decidability:

######  Lemma .

Suppose that $\mathsf{Atoms}$ is effectively $\omega$-categorical and has the
parameter elimination property. Then Definable-isomorphism($\mathsf{Atoms}$)
is decidable.

###### Proof.

By the parameter elimination property, Definable-isomorphism($\mathsf{Atoms}$)
reduces to testing whether given $T$-definable $\Sigma$-structures
${\mathbb{A}}$, ${\mathbb{B}}$ are related by a $T$-definable isomorphism. In
turn, as we show now, testing of the latter condition reduces to evaluation of
first-order formulas in $\mathsf{Atoms}$. Let the given structures be
${\mathbb{A}}=(A,I_{1},\ldots,I_{l})$ and
${\mathbb{B}}=(B,J_{1},\ldots,J_{l})$. We follow the lines of the proof of
Thm. 12 in [KKOT15]; in particular, we build on the following fact, which
follows from effective $\omega$-categoricity of $\mathsf{Atoms}$ (cf. [Boj,
Lemma 5.27]):

######  Lemma .

Suppose that $\mathsf{Atoms}$ are effectively $\omega$-categorical. For any
finite set $T$ of atoms, a $T$-definable set $X$ has only finitely many
$T$-definable subsets, and expressions defining them can be computed
effectively from an expression defining $X$.

To verify existence of a $T$-definable isomorphism from ${\mathbb{A}}$ to
${\mathbb{B}}$, apply Lemma 3 to $X=A\times B$ and for every $T$-definable
subset $R\subseteq A\times B$, test the validity of the first-order formula

$\forall a\in A\ \exists!b\in B\ R(a,b)\ \wedge\ \forall b\in B\ \exists!a\in
A\ R(a,b)$

ensuring that $R$ is the graph of a bijection; and for every $i=1,\ldots,l$,
test the validity of the fomula

$\displaystyle\begin{array}[]{r}\forall\sigma\in\Sigma_{i}\ \forall
a_{1},\ldots,a_{i}\in A\\\ \forall b_{1},\ldots,b_{i}\in
B\end{array}\quad\bigwedge_{1\leq j\leq
i}R(a_{i},b_{i})\implies\big{(}I_{i}(\sigma,a_{1},\ldots,a_{i})\iff
J_{i}(\sigma,b_{1},\ldots,b_{i})\big{)}$

ensuring that the function is an isomorphism. Evaluation of first-order
formulas of the above form reduces to evaluation of first order formulas in
$\mathsf{Atoms}$, see [BT12, KKOT15] for further details. ∎

Theorem 3 and Lemma 3 together prove:

######  Theorem .

Definable-isomorphism($\mathsf{Atoms}$) is decidable whenever $\mathsf{Atoms}$
is an effective $\omega$-categorical structure which is dense and has least
supports.

######  Remark .

In this paper we consider purely relational signatures, but nothing changes if
function symbols are allowed: the proofs of Theorem 3 and Lemma 3 (and thus of
Theorem 3) are still valid when some signature symbols are enforced to be
interpreted as functions.

##  4\. On the necessity of the assumptions

Before proving Theorem 3, we review the assumptions it uses: denseness and
least supports. Note that effective $\omega$-categoricity is not used in
Theorem 3, but only in the proof of Theorem 3, i.e., in Lemma 3 (we do,
however, always assume $\omega$-categoricity).

An essential assumption that makes Theorem 3 go through is the denseness of
$\mathsf{Atoms}$. Dropping it would invalidate the lemma, in view of the
following counterexample:

######  Example .

Let $\mathsf{Atoms}$ be the set of rational numbers with the so-called cyclic
order relation, which is a ternary relation $R$ defined by:

$R(a,b,c)\quad\text{if and only if}\quad a<b<c\quad\text{or}\quad
b<c<a\quad\text{or}\quad c<a<b.$

(Note that the binary order relation itself is not in the vocabulary of
$\mathsf{Atoms}$.) These atoms can be visualized as densely distributed on an
oriented circle, so that one cannot say whether one atom is “smaller” or
“greater” than another, but one can say whether three atoms $a,b,c$ follow
each other in the clockwise direction:

$\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
41.16112pt\hbox{\ignorespaces\ignorespaces\hbox{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{{}{}}{{}{}{}{}\lx@xy@spline@}{}}}}\ignorespaces\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{{}{}}{{}{}{}{}\lx@xy@spline@}{}}}}\ignorespaces\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{{}{}}{{}{}{}{}\lx@xy@spline@}{}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{{}{}{{{}{}{}{}{{{{{}}}{{{}}{{{}}{{{}}{{{}}{{{}}{{{}}{{{}}{{{}}{{{}}{{{}}{{{}}{{{}}{{{}}{{{}}}}}}}}}}}}}}}}}}}}}{{}{}{}{}\lx@xy<EMAIL_ADDRESS>0.0pt\raise
0.0pt\hbox{\hbox{\lx<EMAIL_ADDRESS>3.0pt\raise-7.30554pt\hbox{$\textstyle{a}$}}}}}\ignorespaces{\hbox{\kern-17.07156pt\raise
24.18472pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\lx<EMAIL_ADDRESS>24.18472pt\hbox{\hbox{\kern 3.0pt\raise
3.0pt\hbox{$\textstyle{b}$}}}}}\ignorespaces{\hbox{\kern 26.46092pt\raise
12.80368pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\lx@xy@point}}}}}}{\hbox{\kern 26.46092pt\raise
12.80368pt\hbox{\hbox{\kern 3.0pt\raise
3.0pt\hbox{$\textstyle{c}$}}}}}\ignorespaces{\hbox{\kern
25.32285pt\raise-15.64893pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\lx@xy@point}}}}}}{\hbox{\kern
25.32285pt\raise-15.64893pt\hbox{\hbox{\kern
3.0pt\raise-9.94444pt\hbox{$\textstyle{d}$}}}}}}}}}\qquad\begin{array}[]{ll}\text{e.g.}\\\
&(a,b,c)\in R,(b,d,a)\in R\\\ &(a,c,b)\not\in R,(b,d,c)\not\in R\end{array}$
(2)

For example, in the drawing above, there is an atom automorphism that maps the
ordered pair $(a,b)$ to $(c,d)$ (that is, it maps $a$ to $b$ and $c$ to $d$),
there is also one that maps $(a,b)$ to $(d,c)$ and one that maps $(a,b,c)$ to
$(b,c,d)$, but there is no atom automorphism that maps $(a,b,c)$ to $(a,d,c)$.

This structure of atoms is effectively $\omega$-categorical (in fact, it is
definable in $(\mathbb{Q},\leq)$). It is also not difficult to check, using
the criterion of [BKL14, Thm. 9.3], that is admits least supports. However, it
is not dense. To see this, fix some $a\in\mathsf{Atoms}$ and put $T=\emptyset$
and $S=\\{a\\}$. Let $H$ be an embedding of $\mathsf{Atoms}$ into
$\mathsf{Atoms}$ that avoids $a$, and pick some $b\neq c$ in
$H(\mathsf{Atoms})$, i.e. the image of $H$. Since $H(\mathsf{Atoms})$ is
isomorphic to $\mathsf{Atoms}$, there is some automorphism of it that swaps
$b$ and $c$. This automorphism does not extend to any $\\{a\\}$-automorphism
of $\mathsf{Atoms}$, since no $\\{a\\}$-automorphism can swap $b$ and $c$.

We shall now show that parameter elimination fails for the structure
$\mathsf{Atoms}$. Put $T=\emptyset$, and define a directed graph
${\mathbb{A}}$ so that:

  * •

the set of vertices is the relation $R$; more explicitly, vertices are ordered
triples $(a,b,c)\in\mathsf{Atoms}^{3}$ such that $(a,b,c)\in R$,

  * •

from each vertex $(a,b,c)$ there is exactly one directed edge, ending in the
vertex $(b,c,a)$.

As a directed graph, ${\mathbb{A}}$ is an infinite disjoint family of directed
triangles.

Furthermore, define a graph ${\mathbb{B}}$ as obtained from ${\mathbb{A}}$ by
inverting all arrows; that is, from each vertex $(a,b,c)$ in ${\mathbb{B}}$
there is exactly one directed edge, ending in the vertex $(c,a,b)$.

Clearly, ${\mathbb{A}}$ and ${\mathbb{B}}$ are isomorphic as graphs. However,
no $\emptyset$-definable isomorphism between them exists. Indeed, such an
automorphism $\pi$ would have to map a vertex $(a,b,c)$ to one of three
candidates: $(a,b,c)$, $(b,c,a)$ or $(c,a,b)$. If the first is chosen then, by
$\emptyset$-definability, $\pi$ has to map $(b,c,a)$ to $(b,c,a)$, but on the
other hand, since $\pi$ must preserve edges, it must map $(b,c,a)$ to
$(c,a,b)$, which is a contradiction. The other two candidates for $\pi(a,b,c)$
are excluded by analogous arguments.

On the other hand, for any fixed atom $d\in\mathsf{Atoms}$, a
$\\{d\\}$-definable isomorphism $\pi:{\mathbb{A}}\to{\mathbb{B}}$ exists and
is defined as follows. For any set $\\{a,b,c\\}\subseteq\mathsf{Atoms}$, we
shall define a $\\{d\\}$-definable isomorphism between directed graphs

$\textstyle{(a,b,c)}$$\textstyle{(c,a,b)}$$\textstyle{(b,c,a)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$
and
$\textstyle{(a,b,c)}$$\textstyle{(b,c,a)}$$\textstyle{(c,a,b),\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$

which are fragments of ${\mathbb{A}}$ and ${\mathbb{B}}$, respectively.

First, consider the case where $d\not\in\\{a,b,c\\}$. Then exactly one of the
triples

$(a,d,b),(b,d,c),(c,d,a)$

belongs to the relation $R$. (This becomes clear by looking at the drawing (2)
above, where $(c,d,a)\in R$.) One of the triples $(a,b,c)$, $(b,c,a)$ and
$(c,a,b)$ is thus singled out by $d$, and the isomorphism of the above
triangles that fixes that triple and swaps the other two, is
$\\{d\\}$-definable.

If on the other hand $d\in\\{a,b,c\\}$, then one of the triples $(a,b,c)$,
$(b,c,a)$ and $(c,a,b)$ is even more directly singled out by $d$, and a
$\\{d\\}$-definable automorphism is defined as before.

Altogether we have constructed $\emptyset$-definable graphs ${\mathbb{A}}$ and
${\mathbb{B}}$ that are related by a definable isomorphism, but not by a
$\emptyset$-definable one. ∎

We now discuss the necessity of the assumption on least supports. Removing
this assumption also causes Theorem 3 to fail, as witnessed below.

######  Example .

Fix a finite field $\mathbb{K}$. Let ${\mathbb{A}}$ be a countable affine
space over $\mathbb{K}$. This can be defined for example as follows.

Let $V$ be a countable vector space over $\mathbb{K}$, cf. Example 2.
Intuitively, ${\mathbb{A}}$ is the vector space $V$ with the origin point
forgotten. Formally, for each scalar $c\in\mathbb{K}$, let $R_{c}\subseteq
V^{4}$ consist of all tuples $(a_{1},a_{2},b_{1},b_{2})\in V^{4}$ with
$a_{1}-a_{2}=c\cdot(b_{1}-b_{2})$. We call the structure ${\mathbb{A}}$ with
domain $V$ and relations $R_{c}$, for $c\in\mathbb{K}$, the _affine space_
modelled on $V$. The fundamental property of ${\mathbb{A}}$ is that its
automorphisms are the _affine automorphisms_ , i.e., the permutations of $V$
which are of the form $a\mapsto b_{0}+\pi(a-a_{0})$, for some
$a_{0},b_{0}\in{\mathbb{A}}$ and some linear automorphism $\pi$ of $V$.

Since ${\mathbb{A}}$ is definable in terms of the $\omega$-categorical
structure ${\mathbb{V}}$, by Theorem 2, ${\mathbb{A}}$ itself is
$\omega$-categorical555Indeed, all automorphisms of ${\mathbb{V}}$ remain
automorphisms of ${\mathbb{A}}$, so ${\mathbb{A}}^{n}$ has at most as many
orbits under the action of affinie automorphisms as ${\mathbb{V}}^{n}$ has
under the action of linear automorphisms, i.e., finitely many.. It is also not
difficult to check that the structure ${\mathbb{A}}$ is dense.

By a similar argument as in Example 2, the structure ${\mathbb{A}}$ does not
have least supports. Indeed, any affine line contained in the affine space is
supported by any two of its points. (For the special case
$\mathbb{K}=\mathbb{Z}_{2}$ this is not a counterexample yet, as an affine
line in this case consists of only two points. In this case, a counterexample
is obtained by looking at planes: a two-dimensional plane is supported by any
three of its points.)

We now show that the structure ${\mathbb{A}}$, treated as atoms, does not have
parameter elimination. To this end, we show two $\emptyset$-definable sets
over ${\mathbb{A}}$ such that there is a definable bijection between them, but
no $\emptyset$-definable bijection.

The first set is the domain $A$ of ${\mathbb{A}}$ itself. The second set $B$
is essentially (an isomorphic copy of) the vector space $V$ underlying
${\mathbb{A}}$. Formally, it is defined as the set of equivalence classes of
pairs $(a,b)\in A^{2}$, where $(a,b)$ is equivalent to
$(a^{\prime},b^{\prime})$ iff $b-a=b^{\prime}-a^{\prime}$. This equivalence
relation is clearly definable. The set $B$ has a $\emptyset$-definable element
$0$, namely the equivalence class of a pair $(a,a)$. The set $A$ has no
$\emptyset$-definable point, since such a point would be invariant under all
automorphisms of ${\mathbb{A}}$, and affine automorphisms act transitively on
$A$. As any $\emptyset$-definable bijection $f\colon B\to A$ would map the
$\emptyset$-definable point $0\in B$ to a $\emptyset$-definable point $f(0)\in
A$, no such bijection can exist.

On the other hand, for any fixed $a\in A$, there is a $\\{a\\}$-definable
bijection between $A$ and $B$, namely the function mapping $b\in A$ to the
equivalence class of the pair $(a,b)$.∎

##  5\. Definable sets via the action of atom automorphisms

For the proof of Theorem 3 it will be more convenient to take a different
perspective on definable sets, namely via the action of atom automorphisms.
This view emphasises that definable sets are always _orbit-finite_ (cf. Lemma
5 below). In this section we provide the necessary definitions and properties
that will be useful in the proof of Theorem 3 in the next section. All further
missing details can be found in [Boj].

Definable sets contain, as elements, either other definable sets or atoms
$a\in\mathsf{Atoms}$. The group of atom automorphisms acts naturally on such
sets, by renaming all atoms appearing as elements, as elements of elements,
etc. The action preserves definable sets: a definable set is mapped to a
definable set. By $\pi x$ we denote the result of the action of an atom
automorphism $\pi$ on a definable set $x$. For instance, consider the pure set
$\mathsf{Atoms}$ as atoms and the atom automorphism $\pi$ that swaps
$\underline{0\mkern-1.0mu}\mkern 1.0mu$ with $\underline{1\mkern-1.0mu}\mkern
1.0mu$, and $\underline{3\mkern-1.0mu}\mkern 1.0mu$ with
$\underline{4\mkern-1.0mu}\mkern 1.0mu$, and preserves all other atoms. Then

$\pi\left\\{\,a\,|\,a\in\mathsf{Atoms},a\neq\underline{1\mkern-1.0mu}\mkern
1.0mu\land a\neq\underline{2\mkern-1.0mu}\mkern 1.0mu\,\right\\}\ =\
\left\\{\,a\,|\,a\in\mathsf{Atoms},a\neq\underline{0\mkern-1.0mu}\mkern
1.0mu\land a\neq\underline{2\mkern-1.0mu}\mkern
1.0mu\,\right\\}\quad\pi\\{\underline{0\mkern-1.0mu}\mkern
1.0mu,\underline{1\mkern-1.0mu}\mkern 1.0mu,\underline{2\mkern-1.0mu}\mkern
1.0mu\\}\ =\ \\{\underline{0\mkern-1.0mu}\mkern
1.0mu,\underline{1\mkern-1.0mu}\mkern 1.0mu,\underline{2\mkern-1.0mu}\mkern
1.0mu\\}.$

The action defines a partition of all definable sets into _orbits_ : $x$ and
$x^{\prime}$ are in the same orbit if $\pi x=x^{\prime}$ for some atom
automorphism $\pi$. In the same vein, for every finite set
$S\subseteq\mathsf{Atoms}$, the action of the subgroup of atom
$S$-automorphisms defines a finer partition of all definable sets into _$S$
-orbits_ ($\emptyset$-orbits are just orbits). In particular, the set
$\mathsf{Atoms}$ of atoms is itself also partitioned in $S$-orbits.

By inspecting the syntactic form of definable sets, one easily verifies the
following basic fact:

######  Lemma .

Every $S$-definable set is closed under the action of atom $S$-automorphisms
on its elements, i.e., is a union of $S$-orbits.

We will intensively use the following consequence of Lemma 5:

######  Lemma .

Every $S$-definable function $h$ commutes with atom $S$-automorphisms: for
every atom $S$-automorphism $\pi$, $h\pi=\pi h.$

It is not difficult to prove, by induction on the structure of set-builder
expressions, that $\omega$-categoricity of $\mathsf{Atoms}$ guarantees
finiteness in the statement of Lemma 5:

######  Lemma .

Assume that the structure of atoms is $\omega$-categorical. Then every
$S$-definable set is a finite union of $S$-orbits.

For an $S$-orbit $O$ and an $S$-definable set $X$, if $O\subseteq X$ we say
that $O$ is an $S$-orbit _inside_ $X$; on the other hand, whenever $x\in O$ we
say that $O$ is _the $S$-orbit of_ $x$, and write $O=\text{orbit}_{S}(x)$. The
converse of Lemma 5 is also true when $\mathsf{Atoms}$ is
$\omega$-categorical, as follows from Theorem 2:

######  Lemma .

Assume that the structure of atoms is $\omega$-categorical. Then every
function $h$ that commutes with atom $S$-automorphisms, with $\text{Dom}(h)$
and $\text{Codom}(h)$ being $S$-definable, is itself $S$-definable.

######  Example .

Lemma 5 can be used to prove the claim formulated in Example 2 in Section 2:
there is no definable bijection between the following two sets

$\displaystyle V_{1}$
$\displaystyle=\left\\{\,a\,|\,a\in\mathsf{Atoms}\,\right\\}=\mathsf{Atoms}$
$\displaystyle V_{2}$
$\displaystyle=\left\\{\,\\{a,b\\}\,|\,a,b\in\mathsf{Atoms},a\neq
b\,\right\\}.$

Suppose the contrary, and let $f:V_{1}\to V_{2}$ be an $S$-definable
bijection. Consider any $a,b,c\in\mathsf{Atoms}-S$ with $f(a)=\\{b,c\\}$, and
any atom $S$-automorphism $\pi$ that swaps $b$ and $c$ and does not preserve
$a$, say $\pi(a)=a^{\prime}$. Note that such $\pi$ always exists, e.g., when
$a=b$ then $a^{\prime}=c$. By Lemma 5 we obtain: $f(a^{\prime})=f\pi(a)=\pi
f(a)=\pi\\{b,c\\}=\\{b,c\\}=f(a),$ which is in contradiction with bijectivity
of $f$. ∎

We will also need some basic properties involving least supports. Recall that
we assume that the structure $\mathsf{Atoms}$ has least supports, and that
$\mathrm{sup}(x)\subseteq\mathsf{Atoms}$ denotes the least support of $x$.
First, we observe that the support function commutes with atom automorphisms.

######  Lemma .

For every definable set $x$ and atom automorphism $\pi$, we have
$\mathrm{sup}(\pi x)=\pi(\mathrm{sup}(x))$.

The cardinality of $\mathrm{sup}(x)$ will be called the _dimension_ of $x$.

######  Corollary .

Every two elements in the same $\emptyset$-orbit have supports of same
dimension.

Moreover, the action of an atom automorphism $\pi$ on $x$ depends only on the
restriction of $\pi$ to $\mathrm{sup}(x)$:

######  Lemma .

If atom automorphisms $\pi,\pi^{\prime}$ coincide on $\mathrm{sup}(x)$, then
$\pi x=\pi^{\prime}x$.

We observe the relationship between the least support of a function, its
argument and value:

######  Lemma .

Let $f$ be a definable function and let $a\in\text{Dom}(f)$. Then
$\mathrm{sup}(f(x))\subseteq\mathrm{sup}(f)\cup\mathrm{sup}(x)$.

##  6\. Proof of Theorem 3

In this section we prove Theorem 3. Consider two $T$-definable structures
${\mathbb{A}}$ and ${\mathbb{B}}$ related by an $S$-definable isomorphism $f$
and assume, w.l.o.g., that $S\supseteq T$. We are going to modify suitably the
isomorphism in order to obtain a possibly different one which will be
$T$-definable. For the sake of readability we elaborate the proof in a special
but crucial case, under the following assumptions:

  * •

$T=\emptyset$,

  * •

the signature contains just one binary symbol.

Thus we assume the structures ${\mathbb{A}}$, ${\mathbb{B}}$ to be
$\emptyset$-definable directed graphs. The proof adapts easily to the general
case, as discussed at the end of this section.

Consider therefore two $\emptyset$-definable directed graphs
${\mathbb{A}}=(A,E)$ and ${\mathbb{B}}=(B,F)$, where $A$ and $B$ are sets of
nodes, and $E\subseteq A\times A$ and $F\subseteq B\times B$ are sets of
directed edges, together with an $S$-definable isomorphism $f:A\to B$ of
graphs. Assume w.l.o.g. that the node sets $A$ and $B$ are disjoint. By Lemma
5, the set $A$ of nodes of ${\mathbb{A}}$, being itself $\emptyset$-definable,
splits into finitely many $\emptyset$-orbits. Likewise the set $B$ of nodes of
${\mathbb{B}}$ splits into finitely many $\emptyset$-orbits, but a priori it
is not clear whether the numbers of $\emptyset$-orbits inside $A$ and $B$ are
equal. As a side conclusion of our proof, it will be made clear that they
really are.

We apply denseness of $\mathsf{Atoms}$. Fix in the sequel an embedding
$H:\mathsf{Atoms}\to\mathsf{Atoms}$ such that every automorphism of
$H(\mathsf{Atoms})$ extends to an $S$-automorphism of $\mathsf{Atoms}$. Atoms
in $H(\mathsf{Atoms})$ will be called _$S$ -independent_. Along the same
lines, a node $x\in A\cup B$ will be called _$S$ -independent_ if
$\mathrm{sup}(x)\subseteq H(\mathsf{Atoms})$. By $\omega$-categoricity and
denseness of atoms we have:

######  Claim .

Every $\emptyset$-orbit inside $A\cup B$ contains an $S$-independent node.

(The claim, as well as few other claims formulated below, will be proved below
once the proof of Theorem 3 is outlined.)

We are going to construct an $\emptyset$-definable bijection $h:A\to B$ which
will be later shown to be an isomorphism; to this end we will define
inductively a sequence of $\emptyset$-definable partial bijections

$h_{i}:A\to B,$

for $i=0,1,\ldots,m$, where $m$ is the number of $\emptyset$-orbits inside $A$
(or $B$, as made explicit below), such that the domain $\text{Dom}(h_{i+1})$
of every $h_{i+1}$ extends the domain $\text{Dom}(h_{i})$ of $h_{i}$ by one
$\emptyset$-orbit inside $A$. The required bijection will be $h=h_{m}$. The
order of adding $\emptyset$-orbits to the domain of $h$ will be relevant for
showing that $h$ is an isomorphism.

We start easily by taking as $h_{0}$ the empty function. For the induction
step, suppose that $h_{n}$ is already defined. Among the remaining
$\emptyset$-orbits of $A$ and $B$, i.e., among those which are not included in
$\text{Dom}(h_{n})\cup\text{Codom}(h_{n})$, choose an orbit $O$ whose elements
have maximal dimension (cf. Corollary 5). W.l.o.g. assume that $O\subseteq A$
(if $O\subseteq B$, change the roles of ${\mathbb{A}}$ and ${\mathbb{B}}$, and
replace $f$ and all $h_{i}$ for $i\leq n$ by their inverses). Choose an
arbitrary $S$-independent node $x_{0}\in O$. We observe that the $S$-orbit of
$x_{0}$ does not depend on the choice of $x_{0}$:

######  Claim .

All $S$-independent nodes in $O$ belong to the same $S$-orbit.

We call this $S$-orbit $M\subseteq O$ the _starting_ $S$-orbit inside $O$, and
all its elements _starting nodes_.

Intuitively, an obvious idea would be to declare $h_{n+1}(x_{0})=f(x_{0})$ and
then to close under atom automorphisms to lift the definition of $h_{n+1}$ to
the full orbit $O$. However, it might be the case that $y_{0}=f(x_{0})\in B$
is already contained in $\text{Codom}(h_{n})$. In such case we return back to
$A$ using ${h_{n}}^{-1}$, which yields
$x_{1}:={h_{n}}^{-1}(y_{0})\in\text{Dom}(h_{n})$. Continuing in this way, we
define a sequence $x_{0},y_{0},x_{1},y_{1},x_{2},\ldots$ of nodes, alternating
between nodes of ${\mathbb{A}}$ and nodes of ${\mathbb{B}}$, by the following
equalities:

$\displaystyle h_{n}(x_{i+1})\quad=\quad y_{i}\quad$ $\displaystyle=\quad
f(x_{i}).$ (3)

In words, $y_{i}$ is obtained from $x_{i}$ by applying $f$, and $x_{i+1}$ is
obtained from $y_{i}$ by applying $(h_{n})^{-1}$. Clearly, the latter
application is well-defined only when $y_{i}\in\text{Codom}(h_{n})$. We thus
stop generating the sequence as soon as $y_{i}\notin\text{Codom}(h_{n})$. We
need however to prove that this will eventually happen, i.e., that the
sequence is finite:

######  Claim .

$y_{l}\notin\text{Codom}(h_{n})$, for some $l\geq 0$.

(In particular, when $n=0$ the claim necessarily holds for $l=0$.) The
$S$-orbit $M^{\prime}$ of $y_{l}$ will be called the starting $S$-orbit inside
the $\emptyset$-orbit $O^{\prime}$ of $y_{l}$ (${\mathbb{A}}$ and
${\mathbb{B}}$ are treated symmetrically here). The number $l$ will be called
the length of the starting orbit $M$, and $n+1$ will be called its order; we
write $\text{order}(M)=n+1$, and $\text{length}(M)=l$. By abuse of notation,
we will also assign the same order and length to the $\emptyset$-orbit $O$,
and to every element of $O$.

We are now ready to define the bijection $h_{n+1}$ with
$\text{Dom}(h_{n+1})=\text{Dom}(h_{n})\cup O$. It agrees with $h_{n}$ on
$\text{Dom}(h_{n})$; on the orbit $O$, we define $h_{n+1}$ by extending the
mapping $x_{0}\mapsto y_{l}$ to all of $O$. We claim that there is a (unique)
$\emptyset$-definable bijection between the $\emptyset$-orbit $O$ of $x_{0}$
and the $\emptyset$-orbit $O^{\prime}$ of $y_{l}$ that maps $x_{0}$ to
$y_{l}$:

######  Claim .

The set of pairs $\left\\{\,(\pi x_{0},\pi y_{l})\,|\,\pi\text{ is an atom
automorphism}\,\right\\}$ is an $\emptyset$-definable bijection between $O$
and $O^{\prime}$.

This completes the induction step of the definition of $h$.

Before proving that $h$ is an isomorphism, we formulate a concise equality
describing $h$; the equality will be useful later. The definition of $h_{n+1}$
in the induction step does not depend on the choice of the $S$-independent
node $x_{0}\in M$. To see this, observe that Claim 6 holds, with the same
value $l$, for every other choice of $x_{0}\in M$; indeed, both $f$ and
$(h_{n})^{-1}$ are $S$-definable, and hence by Lemma 5 they preserve the
relation of belonging to the same $S$-orbit; thus, no matter which
$S$-independent node $x_{0}\in M$ is chosen, it will always belong to the same
$S$-orbit (by Claim 6), hence the node $y_{l}$ will always belong to the same
$S$-orbit (and hence to the same $\emptyset$-orbit) inside $B$. Thus by Lemma
5 and by the definition of $h$ we have, for every starting node $x\in A$, the
following equality:

$\displaystyle h(x)=\Big{[}f\circ(h^{-1}\circ f)^{l}\Big{]}(x)$

where $l=\text{length}(x)$; or equivalently (as $f$ and $h$ are bijections)

$\displaystyle(h^{-1}\circ f)^{l+1}(x)=x.$ (4)

(In the special case of starting nodes $x$ of $\text{order}(x)=1$ (recall that
1 is the minimal possible order) we have $\text{length}(x)=0$, and thus the
above equality reduces to $h(x)=f(x)$. Thus $h$ agrees with $f$ on the
starting $S$-orbit of order 1.)

Now we shall prove that $h$ is an isomorphism, i.e., that for every two nodes
$x,x^{\prime}\in A$,

$\displaystyle(x,x^{\prime})\in E\quad\text{ if, and only if
}\quad(h(x),h(x^{\prime}))\in F.$ (5)

The proof is by induction on the orders of $x$ and $x^{\prime}$. Let
$n=\text{order}(x)$ and $n^{\prime}=\text{order}(x^{\prime})$. For the
induction step, suppose that (5) holds for all pairs $y,y^{\prime}$ of
starting nodes with $\langle
m,m^{\prime}\rangle=\langle\text{order}(y),\text{order}(y^{\prime})\rangle$
pointwise strictly smaller than $\langle n,n^{\prime}\rangle$. Thus we assume
that the claim holds for $y,y^{\prime}$ whenever $m\leq n$, $m^{\prime}\leq
n^{\prime}$, but either $m<n$ or $m^{\prime}<n^{\prime}$. Let
$l=\text{length}(x)$ and $l^{\prime}=\text{length}(x^{\prime})$.

We first prove (5) in the special case when both $x$ and $x^{\prime}$ are
starting nodes. (Recall that in the special case $n=n^{\prime}=1$ we have
$h(x)=f(x)$ and $h(x^{\prime})=f(x^{\prime})$, and the claim follows since $f$
is an isomorphism.) Consider two sequences of nodes,

$\displaystyle x_{0},y_{0},x_{1},y_{1},\ldots,\qquad\text{ and }\quad
x^{\prime}_{0},y^{\prime}_{0},x^{\prime}_{1},y^{\prime}_{1},\ldots$

where $x_{0}=x$ and $x^{\prime}_{0}=x^{\prime}$, alternating between nodes of
${\mathbb{A}}$ and ${\mathbb{B}}$, determined by the equalities analogous to
(3):

$\displaystyle h(x_{i+1})\quad=\quad y_{i}\quad$ $\displaystyle=\quad
f(x_{i})$ $\displaystyle h(x^{\prime}_{i+1})\quad=\quad y^{\prime}_{i}\quad$
$\displaystyle=\quad f(x^{\prime}_{i}).$

Analogously as before, the sequence is obtained by alternating applications of
$f$ and $h^{-1}$. In particular, $x_{i+1}=h^{-1}(f(x_{i}))$ and
$x^{\prime}_{i+1}=h^{-1}(f(x^{\prime}_{i}))$. Consider the smallest $k>0$ such
that $x_{k}=x$ and $x^{\prime}_{k}=x^{\prime}$. Observe that equality (4)
guarantees that such $k$ exists, for instance $k=(l+1)(l^{\prime}+1)$ works.
Note that the equality (4) implies also that

$\displaystyle h(x)=y_{k-1}\qquad\text{ and }\qquad
h(x^{\prime})=y^{\prime}_{k-1}.$ (6)

Since $f$ is an isomorphism, for every $i\geq 0$ we have:

$\displaystyle(x_{i},x^{\prime}_{i})\in E\quad\text{ if, and only if
}\quad(y_{i},y^{\prime}_{i})\in F.$ (7)

Using the inductive assumption we want to prove additionally

$\displaystyle(x_{i+1},x^{\prime}_{i+1})\in E\quad\text{ if, and only if
}\quad(y_{i},y^{\prime}_{i})\in F,$ (8)

for every $i$ such that $0<i+1<k$. By the definition of $h$ we know that
$\text{order}(x_{i})\leq n$ and $\text{order}(x^{\prime}_{i})\leq n^{\prime}$
for every $i\geq 0$. Furthermore, observe that for every $0<i<k$ we have
$\text{order}(x_{i})<n$ or $\text{order}(x^{\prime}_{i})<n^{\prime}$; indeed,
the equalities $\text{order}(x_{i})=n$ and
$\text{order}(x^{\prime}_{i})=n^{\prime}$, together with the bijectivity of
$(h^{-1}\circ f)^{i}$, would imply $x_{i}=x$ and $x^{\prime}_{i}=x^{\prime}$.
In consequence, the induction assumption (5) applies for every pair
$(x_{i+1},x^{\prime}_{i+1})$ where $0<i+1<k$, which proves the equivalences
(8). Combining (7) with (8) we get

$\displaystyle(x,x^{\prime})\in E\quad\text{ if, and only if
}\quad(y_{k-1},y^{\prime}_{k-1})\in F$

which, by (6), is exactly (5), as required.

Now we proceed to proving (5) for arbitrary nodes $x,x^{\prime}\in A$. To this
end we will use the following fact, easy to prove using $\omega$-categoricity
and denseness of $\mathsf{Atoms}$:

######  Claim .

For every two nodes $x,x^{\prime}\in A$ there is an atom automorphism $\pi$
such that both $\pi x$ and $\pi x^{\prime}$ are starting nodes.

For any $\pi$ in Claim 6 we have the following sequence of equivalences:

$\displaystyle\begin{aligned} (x,x^{\prime})\in E&\ \text{ iff }\\\ (\pi x,\pi
x^{\prime})\in E&\ \text{ iff }\\\ (h(\pi x),h(\pi x^{\prime}))\in F&\ \text{
iff }\\\ (\pi h(x),\pi h(x^{\prime}))\in F&\ \text{ iff }\\\
(h(x),h(x^{\prime}))\in F&.\end{aligned}$ (9)

The first and the last equivalence hold as the relations $E$ and $F$, being
$\emptyset$-definable, are closed under atom automorphisms (cf. Lemma 5); the
second equivalence has been treated previously as both $\pi x$ an $\pi
x^{\prime}$ are starting nodes; and the third equivalence holds as the
function $h$ is $\emptyset$-definable (cf. Lemma 5). Theorem 3 is thus proved,
once we prove the yet unproven Claims 6–6.

###### Proof of Claim 6.

Consider an $\emptyset$-orbit $O\subseteq A\cup B$. We will use the embedding
$H:\mathsf{Atoms}\to\mathsf{Atoms}$. Take any node $x\in O$ and consider the
restriction of $H$ to the finite set $\mathrm{sup}(x)\subseteq\mathsf{Atoms}$.
As $H$ is an embedding, the restriction is a finite partial isomorphism which
extends, by $\omega$-categoricity of $\mathsf{Atoms}$ (c.f. Lemma 2), to an
atom automorphism, say $\pi$. Then $\pi x$ is an $S$-independent node in $O$,
as $\mathrm{sup}(\pi x)=\pi\mathrm{sup}(x)\subseteq H(\mathsf{Atoms})$ (cf.
Lemma 5). ∎

###### Proof of Claim 6.

Let $x,x^{\prime}\in O$ be two $S$-independent nodes, thus
$\mathrm{sup}(x)\cup\mathrm{sup}(x^{\prime})\subseteq H(\mathsf{Atoms})$. Take
an atom automorphism $\pi$ such that $\pi x=x^{\prime}$. By Lemma 5 we have
$\pi\mathrm{sup}(x)=\mathrm{sup}(x^{\prime})$. The restriction of $\pi$ to
$\mathrm{sup}(x)$ is a finite partial isomorphism, and hence it extends to an
automorphism of $H(\mathsf{Atoms})$, which in turn extends to an atom
$S$-automorphism $\tau$, by denseness. Thus $\tau x=x^{\prime}$ (we use Lemma
5 here) and hence $x$ and $x^{\prime}$ are in the same $S$-orbit. ∎

###### Proof of Claim 6.

It is enough to prove that the nodes $y_{0},y_{1},\ldots$ belong to different
$S$-orbits inside $B$ (as $B$ has finitely many $S$-orbits, and so does
$\text{Codom}(h_{n})$, and the claim follows). With this aim consider the
sequence of $S$-orbits:

$\text{orbit}_{S}(x_{0}),\text{orbit}_{S}(y_{0}),\text{orbit}_{S}(x_{1}),\ldots$

and suppose, towards contradiction, that some $S$-orbit $O$ in $B$ repeats in
the sequence, say $\text{orbit}_{S}(y_{k})=\text{orbit}_{S}(y_{j})$ for some
indices $j<k$. Recall that $A$ and $B$ are disjoint, and that $y_{i}=f(x_{i})$
and $x_{i+1}=h_{n}^{-1}(y_{i})$, for every $i$. Since $f$ is $S$-definable,
and $h_{n}$, being $\emptyset$-definable, is also $S$-definable, by Lemma 5
they both (preserve and) reflect the relation of belonging to the same
$S$-orbit; therefore
$\text{orbit}_{S}(y_{k-\alpha})=\text{orbit}_{S}(y_{j-\alpha})$ for
$\alpha=1,\ldots,j$, and in consequence the first orbit $O$ necessarily
repeats in the sequence:

$\displaystyle\text{orbit}_{S}(x_{0})\ =\ \text{orbit}_{S}(x_{i})$ (10)

for $i=k-j>0$. Recall that $x_{i}=(h_{n}^{-1}\circ f)^{i}$ to observe that the
equality (10) is impossible: $x_{i}\in\text{Dom}(h_{n})$ while
$x_{0}\notin\text{Dom}(h_{n})$, and $\text{Dom}(h_{n})$, being the union of
$\emptyset$-orbits, is also the union of $S$-orbits. ∎

###### Proof of Claim 6.

Relying on Lemma 5 it is enough to demonstrate that the set of pairs

$\left\\{\,(\pi x_{0},\pi y_{l})\,|\,\pi\text{ is an atom
automorphism}\,\right\\}$

is (the graph of) a bijection. In other words, it is enough to prove that for
every two atom automorphism $\pi,\pi^{\prime}$, the equality $\pi
x_{0}=\pi^{\prime}x_{0}$ holds if, and only if the equality $\pi
y_{l}=\pi^{\prime}y_{l}$ holds. This is equivalent to the following condition:

$\displaystyle\text{for every atom automorphism }\pi,\ \pi x_{0}=x_{0}\text{
iff }\pi y_{l}=y_{l}.$ (11)

Recall that $y_{l}=g(x_{0})$, where $g=\Big{[}f\circ(h_{n}^{-1}\circ
f)^{l}\Big{]}$; as both $f$ and $h_{n}$ are $S$-definable (partial)
bijections, their composition $g$ is also an $S$-definable bijection, and
hence the condition (11) holds for all atom $S$-automorphisms $\pi$. Our aim
is to prove (11) for all atom automorphisms, using $S$-independence of
$x_{0}$.

Define the _$S$ -support_ as $\mathrm{supp}_{S}(x)\
\stackrel{{\scriptstyle\text{def}}}{{=}}\ \mathrm{sup}(x)-S$. Let
$U=\mathrm{sup}(x_{0})$. We claim that $\mathrm{sup}(y_{l})=U$ as well, i.e.,
$y_{l}$ is $S$-independent too. To demonstrate this, we first observe using
Lemma 5 that the mapping $g$, being $S$-definable, can only decrease the
$S$-support: $\mathrm{supp}_{S}(x_{0})\supseteq\mathrm{supp}_{S}(y_{l}).$ But
$g^{-1}$, being also $S$-definable, has the same property and hence
$\mathrm{supp}_{S}(x_{0})=\mathrm{supp}_{S}(y_{l}).$ Furthermore, $x_{0}$ is
$S$-independent and thus satisfies
$\mathrm{supp}_{S}(x_{0})=\mathrm{sup}(x_{0})$, which yields
$U=\mathrm{supp}_{S}(y_{l})\subseteq\mathrm{sup}(y_{l})$. Finally, the
dimension of $y_{l}$ is at most equal to the dimension of $x_{0}$ (because the
node $x_{0}$ has been chosen as one with the maximal dimension), i.e., to the
cardinality of $U$, therefore we deduce the equality $U=\mathrm{sup}(y_{l})$.

We are now ready to prove (11); we focus on the left-to-right implication, as
the other one is proved similarly. Consider any atom automorphism $\pi$
satisfying $\pi x_{0}=x_{0}$. By Lemma 5 we know that $\pi$ preserves the set
$U$, i.e., $\pi U=U$. We claim that some atom $S$-automorphism $\pi^{\prime}$
coincides with $\pi$ on $U$. Indeed, the restriction of $\pi$ to $U$ extends,
as a finite partial isomorphism inside $H(\mathsf{Atoms})$, to an automorphism
of $H(\mathsf{Atoms})$; and the latter extends to an atom $S$-automorphism
$\pi^{\prime}$, by denseness of $\mathsf{Atoms}$. As $\pi$ and $\pi^{\prime}$
coincide on $U=\mathrm{sup}(x_{0})$, by Lemma 5 we have $\pi^{\prime}x_{0}=\pi
x_{0}=x_{0}$. We can apply (11) to the atom $S$-automorphism $\pi^{\prime}$,
thus obtaining $\pi^{\prime}y_{l}=y_{l}$. Finally, again by Lemma 5 applied to
$\pi$ and $\pi^{\prime}$, coinciding on $U=\mathrm{sup}(y_{l})$, we deduce
$\pi y_{l}=\pi^{\prime}y_{l}$. This entails $\pi y_{l}=y_{l}$ as required. ∎

###### Proof of Claim 6.

Similarly as in the proof of Claim 6, we use the embedding
$H:\mathsf{Atoms}\to\mathsf{Atoms}$. The restriction of $H$ to the finite set
$\mathrm{sup}(x)\cup\mathrm{sup}(x^{\prime})\subseteq\mathsf{Atoms}$ is
necessarily a finite partial isomorphism which extends, by
$\omega$-categoricity of $\mathsf{Atoms}$, to an atom automorphism $\pi$, such
that the nodes $\pi x$ and $\pi x^{\prime}$ are both $S$-independent and
hence, by Claim 6, also starting. ∎

### The general case

The additional assumptions imposed in the proof are not essential, and the
proof easily adapts to the general case. To get rid of the assumption
$T=\emptyset$, one just needs to replace the atoms by the structure
$\mathsf{Atoms}^{\prime}$ obtained from $\mathsf{Atoms}$ by introducing
constant symbols for each element of $T$. Then, every set $x$ which is
$T$-definable in $\mathsf{Atoms}$ becomes $\emptyset$-definable in
$\mathsf{Atoms}^{\prime}$. Moreover, $\mathsf{Atoms}^{\prime}$ remains
effectively $\omega$-categorical, dense, and still has least supports.

One also easily gets rid of the assumption that the signature has just one
binary symbol. First, to deal with (possibly infinitely) many symbols, in the
inductive argument towards $h$ being an isomorphism one treats each symbol
separately. In case symbols of arity other than 2, say $r$, the induction is
with respect to the $r$-tuples of orders, instead of pairs thereof. The
inductive argument itself, as well as Claim 6, adapt easily to $r$-tuples.
Finally, in case of a (possibly infinite) $T$-definable signature, one needs
to modify the sequence of equalities (9) appropriately, in order to take into
account the action of atom automorphisms on signature symbols. For a signature
symbol $\sigma$, denote by $\sigma^{{\mathbb{A}}}$, $\sigma^{{\mathbb{B}}}$
the interpretation of $\sigma$ in ${\mathbb{A}}$, ${\mathbb{B}}$,
respectively. Then the sequence of equalities (9) is adapted as follows:

$\displaystyle(x_{1},\ldots,x_{r})\in\sigma^{{\mathbb{A}}}$ iff
$\displaystyle(\pi x_{1},\ldots,\pi x_{r})\in\pi(\sigma^{{\mathbb{A}}})$ iff
$\displaystyle(\pi x_{1},\ldots,\pi x_{r})\in(\pi\sigma)^{{\mathbb{A}}}$ iff
$\displaystyle(h(\pi x_{1}),\ldots,h(\pi x_{r}))\in(\pi\sigma)^{{\mathbb{B}}}$
iff $\displaystyle(h(\pi x_{1}),\ldots,h(\pi
x_{r}))\in\pi(\sigma^{{\mathbb{B}}})$ iff $\displaystyle(\pi
h(x_{1}),\ldots,\pi h(x_{r}))\in\pi(\sigma^{{\mathbb{B}}})$ iff
$\displaystyle(h(x_{1}),\ldots,h(x_{r}))\in\sigma^{{\mathbb{B}}}$ .

We consider here the action $\pi\sigma$ on the signature symbol $\sigma$, as
well as the action on the interpretation of the signature symbol,
$\pi(\sigma^{{\mathbb{A}}})$ or $\pi(\sigma^{{\mathbb{B}}})$. In particular,
$(\pi\sigma)^{{\mathbb{A}}}$ denotes the interpretation of the signature
symbol $\pi\sigma$ in ${\mathbb{A}}$. As $\pi$ is a $T$-automorphism, the
first, the second, the fourth and the last equivalence follow by
$T$-definability of ${\mathbb{A}}$ and ${\mathbb{B}}$ (cf. Lemma 5); the third
equivalence is proved previously, as $\pi x_{1},\ldots,\pi x_{r}$ are starting
nodes; and the fifth equivalence holds since the function $h$ is $T$-definable
(cf. Lemma 5).

## References

  * [Bab16] László Babai.  Graph isomorphism in quasipolynomial time [extended abstract].  In Procs. STOC 2016, pages 684–697, 2016.
  * [BBKL12] Mikołaj Bojańczyk, Laurent Braud, Bartek Klin, and Sławomir Lasota.  Towards nominal computation.  In Procs. POPL 2012, pages 401–412, 2012.
  * [BKL14] Mikołaj Bojańczyk, Bartek Klin, and Sławomir Lasota.  Automata theory in nominal sets.  Log. Meth. Comp. Sci., 10, 2014.
  * [BKLT13] Mikołaj Bojańczyk, Bartek Klin, Sławomir Lasota, and Szymon Toruńczyk.  Turing machines with atoms.  In Procs. LICS 2014, pages 183–192, 2013.
  * [Boj] Mikołaj Bojańczyk.  Slightly infinite sets.  A draft of a book available at https://www.mimuw.edu.pl/~bojan/paper/atom-book.
  * [BT12] M. Bojańczyk and S. Toruńczyk.  Imperative programming in sets with atoms.  In Procs. FSTTCS 2012, volume 18 of LIPIcs, 2012.
  * [Eng59] Erwin Engeler.  Äquivalenzklassen von n-tupeln.  Z. Math. Logic Grundl. Math., 5:340–345, 1959.
  * [Fra53] R. Fraïssé.  Theory of relations.  North-Holland, 1953.
  * [Hod93] Wilfrid Hodges.  Model Theory.  Number 42 in Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1993.
  * [KKOT15] Bartek Klin, Eryk Kopczyński, Joanna Ochremiak, and Szymon Toruńczyk.  Locally finite constraint satisfaction problems.  In Procs. LICS’15, pages 475–486, 2015.
  * [KLOT14] Bartek Klin, Sławomir Lasota, Joanna Ochremiak, and Szymon Toruńczyk.  Turing machines with atoms, constraint satisfaction problems, and descriptive complexity.  In Procs. CSL-LICS’14, pages 58:1–58:10, 2014.
  * [KLOT16] Bartek Klin, Slawomir Lasota, Joanna Ochremiak, and Szymon Toruńczyk.  Homomorphism problems for first-order definable structures.  In Procs. FSTTCS 2016, pages 14:1–14:15, 2016.
  * [KS16] Bartek Klin and Michal Szynwelski.  SMT solving for functional programming over infinite structures.  In Procs.of MSFP 2016, pages 57–75, 2016.
  * [KT16] Eryk Kopczyński and Szymon Toruńczyk.  LOIS: an application of SMT solvers.  In Procs. SMT Workshop, volume 1716 of CEUR Proceedings, pages 51–60, 2016.
  * [KT17] Eryk Kopczynski and Szymon Toruńczyk.  LOIS: syntax and semantics.  In Procs. POPL, pages 586–598, 2017.
  * [Luk82] Eugene M. Luks.  Isomorphism of graphs of bounded valence can be tested in polynomial time.  J. Comput. Syst. Sci., 25(1):42–65, 1982.
  * [Pit13] A. M. Pitts.  Nominal Sets: Names and Symmetry in Computer Science.  Cambridge University Press, 2013.
  * [RN59] Czesław Ryll-Nardzewski.  On category in power $\leq\aleph_{0}$.  Bull. Acad. Pol. Sci. Ser. Math. Astr. Phys., 7:545–548, 1959.
  * [Sve59] Lars Svenonius.  $\aleph_{0}$-categoricity in first-order predicate calculus.  Theoria, 25:82–94, 1959.