Group Order Logic

Anatole Dahan

University of Cambridge

Université Paris-Cité

Inria, ENS-Paris

*Abstract*—We introduce an extension of fixed-point logic (FP) with a group-order operator (ord), that computes the size of a group generated by a definable set of permutations. This operation is a generalization of the rank operator (rk). We show that FP + ord constitutes a new candidate logic for the class of polynomial-time computable queries (P). As was the case for FP + rk, the model-checking of FP + ord formulae is polynomial-time computable. Moreover, the query separating FP + rk from P exhibited by Lichter in his recent breakthrough is definable in FP + ord. Precisely, we show that FP + ord canonizes structures with Abelian colors, a class of structures which contains Lichter's counter-example. This proof involves expressing a fragment of the group-theoretic approach to graph canonization in the logic FP + ord.

*Index Terms*—Descriptive Complexity, Logic for P, Finite Model Theory, Computational Group Theory, Fixed-point logic, Schreier-Sims algorithm

# I. INTRODUCTION

The quest to identify a logic that precisely characterizes the class of problems solvable in polynomial time (P) is a central challenge in descriptive complexity. This question can be traced back to [1], and its modern formulation was stated by Gurevich [2]. While fixed-point logic (FP) captures P on ordered structures, no logic is currently known to capture P in the general case. FP and its natural extensions, such as fixed-point logic with counting (FPC), fail to capture P [3]. This limitation of FPC was demonstrated using the CFI-construction, a class of structures encoding the satisfiability of systems of equations over the finite field $F_2$ [3].

To address these limitations, extensions of FP incorporating linear-algebraic operations, such as the rank operator (rk), have been proposed [4]–[7]. However, even FP + rk falls short of capturing P, as recently shown by Lichter [8] through a generalized class of CFI-structures.

On the other hand, a lot of work has been devoted to *partial capture results*, showing that on restricted classes of structures, extensions of FP are able to define all P queries. For instance, Grohe showed that FPC captures P on any class of structures which excludes a minor [9]. Those results usually rely on the definition within the logic at hand of a canonization of the structures under consideration. Indeed, for any logic extending FP, the Immerman-Vardi theorem implies that the definability

of a canonization on a class of structures yields the capture of P on that class. This motivates the study of canonization algorithms, and their definability in candidate logics for P.

Parallel to this investigation, significant progress has been made in the development of efficient algorithms for graph isomorphism and canonization through a group-theoretic approach. This line of research has yielded polynomial-time isomorphism and canonization algorithms for various classes of structures [10]–[12], as well as Babai’s recent breakthrough that general graph isomorphism is solvable in quasi-polynomial time [13]. Notably, an early result in this area demonstrates the polynomial-time canonization of CFI-structures. This result generalizes seamlessly to the broader classes of CFI-constructions used in [7], or even in [8] to separate FP + rk from P. These findings underscore the potential of integrating group-theoretic operators into FP to extend its expressive power.

The most fundamental polynomial-time permutation group algorithm is probably Schreier-Sims algorithm [14], [15], which enables, given a set of permutations, to compute the order, and recognize elements of the group generated by that set. However, this procedure relies on stabilizing one by one the elements of the domain on which the permutations act. This process thus depends on an ordering of the domain of the permutation group at hand, and cannot be defined in an isomorphism-invariant way, while its output is isomorphism-invariant.

This situation is quite similar to the one which motivated the introduction of the rk operator: Gaussian elimination is inherently dependent on an ordering of the rows and columns of the matrix at hand, yet the rank of the matrix is not. Note that, the fact that FP + rk is strictly more expressive than FPC implies that FPC indeed cannot define Gaussian elimination, nor can it define the rank of a matrix by any other means.

In this article, we introduce a novel group-theoretic operator, ord, which computes the order of a group generated by a definable set of permutations. Because the Schreier-Sims algorithm enables the computation of this operation in polynomial-time, whether a structure satisfies a formula in FP + ord can be decided in polynomial-time (in the size of the structure). Thus, like rk, the ord operator defines the isomorphism-invariant result of a polynomial-time algorithm whose computation inherently depends on an ordering of the structure at hand.

The ord operator fills an interesting space within the alge-

Funded in part by UK Research and Innovation (UKRI) under the UK government's Horizon Europe funding guarantee: grant number EP/X028259/1.

Funded in part by ANR - project QUID

Funded in part by ANR - project δifference
braic extensions of fixed-point logics that have been studied. In [16], the authors consider various solvability quantifiers — expressing the satisfiability of definable systems of equations over different algebraic structures, as abelian groups, fields, or commutative rings. In this work, the authors suggest a new *permutation group membership* (GM) quantifier, that subsumes all the quantifiers considered in this article. The ord operator defines this quantifier. Actually, the ord operator can be thought of as being to the GM quantifier what the rk operator is to the field solvability quantifier. This should be contrasted with the apparent absence of such a matrix rank operator in the context of rings.

Even with this operator available, simulating group-theoretic algorithms within FP + ord presents significant challenges due to the reliance of those algorithms on an implicit ordering of the domain. This difficulty is particularly pronounced in graph canonization. In this context, the group-theoretic approach consists in the computation of a canonical labeling coset. A labeling coset is a set of permutations of the domain of a structure which behaves *almost* like a group. Building a canonical labeling coset rather than a mere encoding of the canonical structure enables exploiting the structure of underlying permutation groups, but depends on the existence of an ordering of the domain. Indeed, in the ordered setting, a labeling is a reordering, and thus a permutation; while in the unordered setting, it is a bijection from the domain to an initial segment of the integers, and those bijections cannot be composed. Schweitzer et al. [17] provide such a definition of labeling cosets that accounts for the distinct nature of the structure's domain and its canonical numerical representation. However, their contributions remain algorithmic and do not provide an isomorphism-invariant representation of labeling cosets.

Our main result is that FP + ord strictly extends the expressive power of FP + rk. Precisely, we show that the rank of a definable matrix is definable in FP + ord, and that FP + ord captures P on the class of structures used by Lichter to separate FP + rk from P. This result has the direct implication that FP + rk cannot define the order of a group given by a generating set, in the same way that FPC < FP + rk implies that FPC cannot define the rank of a matrix.

We obtain this canonization result by showing that, on CFI-structures, FP + ord can simulate the graph canonization algorithm defined in [12], using an isomorphism-invariant representation of labeling cosets. This representation of labeling cosets relies on a notion of *definable group morphisms* that we will define in Section III.

A similar approach to the canonization of CFI-structures was taken in [18], where the same algorithm is simulated in the context of CPT, another candidate logic for P. However, the two results differ in the way labeling cosets are represented. In CPT, labeling cosets are represented as systems of equations over a finite ring. In the case of FP + ord, our representation of labeling cosets remains purely theoretic. While this does not seem to directly allow generalization of the classes of structures canonized, this opens the door to new representation

schemes for labeling cosets.

While we do not expect FP + ord to capture P, our results suggest that FP + ord represents a meaningful advancement in the landscape of logics for polynomial-time computation. Moreover, many other operations on permutation groups are known to be polynomial-time computable, many of them playing an important role in polynomial-time Graph Isomorphism algorithms for broader classes of graphs. This first group-theoretic logic for P sets the stage to study the relationship of those different problems in an isomorphism-invariant context.

In the following section, we define the ord operator. In Section III, we provide a set of group-theoretic operations which are definable in FP + ord, including the morphism-definability results mentioned above. Section IV is devoted to the proof that FP + ord defines the rk operator. Finally, in Section V, we show that FP + ord canonizes CFI-structures, thus separating FP + rk from FP + ord (relying on Lichter's result [8]).

## II. THE GROUP ORDER OPERATOR

In this section, we introduce the ord operator. We first introduce some notations and known facts concerning logic and the capture of P that will be useful throughout the article. In a second time, we introduce our representation of permutations and sets of permutations, together with the formal definition of the ord operator.

### A. Preliminaries

We denote signatures by upper-case Greek letters, structures by Fraktur symbols (e.g., $\mathfrak{A}, \mathfrak{B}, \mathfrak{C}$), and their respective domains by the corresponding Roman symbols (e.g., $A, B, C$). We assume all structures to be finite, and all signatures to be relational.

Tuples of the form $(v_1, \dots, v_l)$ are denoted by $\vec{v}$. For a set $X$, we write $|X|$ to indicate its cardinality, and for a tuple $\vec{x} = (x_1, \dots, x_k)$, we write $|\vec{x}|$ to denote its length $k$. Given $n \in \mathbb{N}$, we denote $[n]$ the set $\{1, 2, \dots, n\}$.

The graph of a function $f: A \to B$ is the set $\{(a, b) \in A \times B \mid f(a) = b\}$, denoted graph($f$). Given a function $f: Y \to Z$ and $X \subseteq Y$, we denote $f|_X$ the restriction of $f$ to $X$.

To keep the horizontal length of formulae reasonable, we occasionally denote large disjunctions of the form $A \lor B \lor C$ as

$$ \begin{cases} A \\ \circled{B} \\ C \end{cases} $$

We use a similar notation for large conjunctions.

Given a logic $\mathcal{L}$ and a signature $\Sigma$, we denote by $\mathcal{L}[\Sigma]$ the set of formulae in $\mathcal{L}$ over $\Sigma$. For a formula $\varphi \in \mathcal{L}[\Sigma]$ and a $\Sigma$-structure $\mathfrak{A}$, we denote by $\varphi(\mathfrak{A})$ the set of assignments $v: \text{free}(\varphi) \to A$ such that $(\mathfrak{A}, v) \models \varphi$. By imposing an ordering on the free variables of $\varphi$, we can view $\varphi(\mathfrak{A})$ as a $|\text{free}(\varphi)|$-ary relation over $A$. Usually, this ordering will be explicitly specified when defining formulae. For instance, if
a formula $\varphi(x, y, z)$ is defined, we order the components of $\varphi(\mathfrak{A})$, starting with the $x$-component, followed by $y$, and then $z$. The function that maps $\mathfrak{A}$ to $\varphi(\mathfrak{A})$ is the query defined by $\varphi$. Given two logics $\mathcal{L}, \mathcal{L}'$, we write $\mathcal{L} \leq \mathcal{L}'$ if any query definable in $\mathcal{L}$ is definable in $\mathcal{L}'$.

All logics considered in this article are extensions of FPC, whose definition relies on the notion of numerical sort. We use the definition of the numerical sort from [19], that we introduce now. Given a signature $\Sigma$ such that $(\leq) \notin \Sigma$, and a $\Sigma$-structure $\mathfrak{A}$, we denote $\mathfrak{A}^+$ the $\Sigma \cup \{\leq\}$-structure $(A \cup A^\leq, (R^\mathfrak{A})_{R \in \Sigma}, \leq^{A^\leq})$ where $A^\leq = \{0, 1, \dots, |A|\}$ and $\leq^{A^\leq}$ is the natural linear order over the set of integers $A^\leq$. Note that $|A^\leq| = |A| + 1$. It will be useful later to have a notation for the prefix of the natural numbers of cardinality $|A|$. We denote $A^< = \{0, 1, \dots, |A| - 1\}$.

Intuitively, FP is the extension of first-order logic with an operator enabling the computation of the inflationary fixed-point of definable second-order functions (i.e. functions mapping relations to relations). A formal definition of FP can be found in, e.g. [9] or [19].

We can add to any $\Sigma$-structure $\mathfrak{A}$ its numerical domain, and consider formulae of FP[$\Sigma \cup \{\leq\}$], evaluating them over $\mathfrak{A}^+$. Since any isomorphic structures $\mathfrak{A}$ and $\mathfrak{B}$ share the same numerical domain, this extension preserves the isomorphism invariance of the logic. This is the gist of FPC, whose formal definition can once again be found in [9] or [19]. Moreover, the Immerman-Vardi theorem [20] ensures that all P computable arithmetic functions can be defined by FP on $A^\leq$.

Note that, with this definition, arithmetic functions involving integers larger than $|A|$ require the encoding of those integers as tuples of numerical values. It is easy to see that for any $k$, one can encode integers up to $|A|^k$ as $k$-tuples of numerical values. Given a tuple of numerical variables $\vec{\mu}$ and an integer $m \leq |A|^{|\vec{\mu}|}$, we write $\vec{\mu} \leftarrow m$ for the assignment mapping $\vec{\mu}$ to the unique tuple of numerical values which encodes $m$ in $\mathfrak{A}$.

We follow usual conventions when writing and handling formulae. In particular, we separate domain variables, which range over $\mathfrak{A}$, composed of domain elements, and numerical variables, which range over $A^\leq$, the set of numerical elements. This distinction constitutes the type of a variable.

When reasonable, we keep distinct names for domain variables (for instance $x, y, z$) and numerical variables (for instance $i, j, \mu, \nu, \lambda$). However, for reasons to become clear in the following chapters, the strong separation of variable symbols can often bear a cost on readability. In particular, it is often convenient to consider tuples containing variables of different types. In the same way, we usually keep distinct names for variables, and their values. When this seems to hinder readability, we may break this rule.

The type of a tuple $\vec{x}$ of variables, denoted $\text{type}(\vec{x})$ is the unique word $w \in \{\text{element}, \text{number}\}^*$ such that $x_i$ is a domain variable iff $w_i$ = element. We often need to consider the set underlying all potential valuations of a tuple $\vec{x}$, and therefore denote $A^{\vec{x}}$ (or $A^{\text{type}(\vec{x})}$) the set $\prod_{i=1}^{|\vec{x}|} A^{\text{type}(\vec{x})_i}$, where $A^{\text{element}} := A$ and $A^{\text{number}} := A^\leq$.

We also allow types instead of arity in the definition of signatures. For instance, if a relation symbol $R$ has type (number, number, element), an interpretation of $R$ on $A$ is a subset of $A^\leq \times A^\leq \times A$. Finally, we overload this notation to relations themselves, so that if $X$ is a relation over $A$, $\text{type}(X)$ is the unique type-word such that $X \subseteq A^{\text{type}(X)}$.

An isomorphism between two $\Sigma$-structures $\mathfrak{A}, \mathfrak{B}$ is a function $f: A \to B$ such that, for any relation $R \in \Sigma$ and any tuple $\vec{a} \in A^{\text{type}(R)}$,

$$ \vec{a} \in R(\mathfrak{A}) \iff f^*(\vec{a}) \in R(\mathfrak{B}) $$

where $f^*(\vec{a})$ is the vector $\vec{b}$ defined by

$$ b_i := \begin{cases} f(a_i) & \text{if } a_i \in A \\ a_i & \text{if } a_i \in A^\leq \end{cases} $$

Given a logic $\mathcal{L}$ and a class $\mathcal{C}$ of $\Sigma$-structures, $\mathcal{L}$ canonizes structures in $\mathcal{C}$, if there are formulae $(\varphi_R)_{R \in \Sigma}$, each with $|\text{type}(R)|$ free numerical variables, such that, for any structure $\mathfrak{A} \in \mathcal{C}$,

$$ (A^<, (\varphi_R(\mathfrak{A})_{R \in \Sigma})) \cong \mathfrak{A} $$

If $\mathcal{C}$ consists of structures over several signatures, $\mathcal{L}$ canonizes $\mathcal{C}$ if for any signature $\Sigma$, $\mathcal{L}$ canonizes the class of all $\Sigma$-structures in $\mathcal{C}$. This definition of canonization is quite restrictive, compared for instance to [9, Definition 3.3.2]. This choice is made purely to enhance clarity.

Given a logic $\mathcal{L}$ and a class of structures $\mathcal{C}$, $\mathcal{L}$ is said to capture P on $\mathcal{C}$ if, for any polynomial-time query $Q$ over the signature $\Sigma$, there is a formula $\varphi \in \mathcal{L}$ such that, for any $\Sigma$-structure $\mathfrak{A} \in \mathcal{C}$, $Q(\mathfrak{A}) = \varphi(\mathfrak{A})$. It is a direct consequence of the Immerman-Vardi theorem that, if $\mathcal{L} \supseteq \text{FP}$ canonizes structures in $\mathcal{C}$, then $\mathcal{L}$ captures P on $\mathcal{C}$.

## B. Representation of sets of permutations in first-order logic

Given a set $X$, we denote $\text{Sym}(X)$ the group of permutations over $X$, i.e. the set of all bijections $f: X \to X$. Given $S \subseteq \text{Sym}(X)$, we denote $\langle S \rangle$ the minimal group $G \leq \text{Sym}(X)$ which contains $S$. If $G$ is a group, we write $H \leq G$ when $H$ is a subgroup of $G$ (i.e. it is a group contained in $G$). In such a case, a (left) coset of $H$ in $G$ is a set of the form $gH := \{g \cdot h \mid h \in H\}$, for some $g \in G$. The set of cosets of $H$ in $G$ forms a partition of $G$ into $|G|/|H|$ classes, of $|H|$ elements each.

As outlined in the introduction, we aim to define an operator which enables the computation of $|\langle S \rangle|$, when given a representation of $S$ as input. We first introduce such a representation of permutations and sets of permutations in first-order logic.

**Definition II.1.** A formula $\varphi(\vec{s}, \vec{t})$ defines a permutation $\sigma \in \text{Sym}(A^{\vec{s}})$ on $\mathfrak{A}$ if $\varphi(\mathfrak{A}) = \text{graph}(\sigma)$.

Conversely, given a relation $R \subseteq X \times X$ which is the graph of a permutation on $X$, we denote $\text{perm}(R)$ this unique permutation.
Because FP does not provide a seamless way to represent
sets, we represent sets of permutations as enumerations of
graphs of permutations:

**Definition II.2.** A formula $\varphi(\vec{p}, \vec{s}, \vec{t})$ defines $S$ binding $\vec{p}$ in $\mathfrak{A}$ if

$$
S = \{ \sigma \in \operatorname{Sym}(A^{\vec{s}}) \mid \exists \vec{a} \in A^{\vec{p}}, \operatorname{graph}(\sigma) = \varphi(\mathfrak{A}, \vec{a}) \}.
$$

In such a case, we denote the group $\langle S \rangle$ as $\langle\varphi\rangle_{\vec{p},\vec{s},\vec{t}}(\mathfrak{A})$.

Note that we do not require that $\varphi$ defines a permutation on $\mathfrak{A}$ for all valuations of $\vec{p}$, but rather consider the set of permutations defined by $\varphi$ for some valuation of $\vec{p}$. This can be seen as a way to work around the fact that, given such a formula $\varphi$, it is undecidable whether on all structures $\mathfrak{A}$ and for all valuations of $\vec{p}$, $\varphi$ defines a permutation. Notice also that we have used dots in the definition of $\langle\varphi\rangle_{\vec{p},\vec{s},\vec{t}}(\mathfrak{A})$ as to separate the three “blocks” of variables bound by this operator: the parameters of the enumeration, the pre-image of the permutation, and its image. When clear from context, we may omit the two last blocks in the subscript.

There is one last obstacle to the definition of the ord
operator. Recall that, given a formula $\varphi(\vec{p}, \vec{s}, \vec{t})$, we expect
($\mathrm{ord}_{\vec{p}, \vec{s}, \vec{t}}\varphi$) to represent $|\langle\varphi\rangle_{\vec{p}, \vec{s}, \vec{t}}(\mathfrak{A})|$. However, this value may
exceed any polynomial bound on $|A|$:

**Example II.3.** Consider the formula

$$
\varphi(p_1, p_2, s, t) := \begin{cases} s = p_1 \wedge t = p_2 \\ t = p_1 \wedge s = p_2 \\ s \neq p_1 \wedge s \neq p_2 \wedge s = t \end{cases}
$$

For any $\mathfrak{A}$ and $a, b \in A$, $\varphi(\mathfrak{A}, a, b) = \text{graph}((a \ b))$, where
$(a \ b)$ is the permutation fixing all points in $A \setminus \{a, b\}$ and
mapping $a$ to $b$ and $b$ to $a$. Such a permutation is called
a transposition, and it is a well known fact that all finite
permutations on a set can be written as a finite product of
transpositions.

$\varphi$ binding $p_1, p_2$ defines the set of all transposition $(a \ b)$ on the domain of the structure. Therefore, $|\langle\varphi\rangle_{p_1, p_2, s, t}(\mathfrak{A})| = |\text{Sym}(A)| = |A|!$.

On the other hand, this example is maximal: for any type $T$, $|\text{Sym}(A^T)| = |A|^{|T|}$, and as such, the binary representation of $|G|$ for any group $G \le \text{Sym}(A^T)$ requires at most $\log(|A|^{|T|}) \le |A|^{|T|} \log(|A|^{|T|}) \le |A|^{2|T|}$.

We are limited by the usual representation of integers in
fixed-point logic as numerical values, which equates to unary
encoding of integers: we can only consider integers bounded
by a polynomial, while, with binary encoding, it is expected
that the length of the numbers at hand be polynomially
bounded. However, there is a straight-forward representation
of the binary encoding of integers in fixed-point: as numerical
relations. That is, the number $N = \sum_{i=1}^{\ell} w_i 2^{\ell-i}$ is repre
sented as a numerical relation $R$ such that $R(x)$ holds iff
$w_x = 1$. If $\ell$ is bounded by $|A|^k$ for some constant $k$, it
suffices to consider a $k$-ary relation $R$ to encode $N$.

Therefore, for any $T$, and any formula $\varphi(\vec{p}, \vec{s}, \vec{t})$ with
$\mathrm{type}(\vec{s}) = \mathrm{type}(\vec{t}) = T$, $N := |\langle\varphi\rangle_{\vec{p},\vec{s},\vec{t}}(\mathfrak{A})|$ can be rep
resented as a relation of type number$2^{|T|}$, representing the
binary encoding of $N$. This yields the following definition of
the ord operator:

**Definition II.4.** Given a $\Sigma$-formula $\varphi(\vec{p}, \vec{s}, \vec{t})$, with $\mathrm{type}(\vec{s}) = \mathrm{type}(\vec{t}) = T$, and a $\Sigma$-structure $\mathfrak{A}$, $(\mathrm{ord}_{\vec{p}, \vec{s}, \vec{t}}\varphi)$ is a $2^{|T|}$-ary numeric relation that encodes $|\langle\varphi\rangle_{\vec{p}, \vec{s}, \vec{t}}(\mathfrak{A})|$, that is, for any $\vec{\mu} \in (A^{\le})^{2^{|T|}}$, $(\mathrm{ord}_{\vec{p}, \vec{s}, \vec{t}}\varphi)$ holds on $(\mathfrak{A}, \vec{\mu})$ iff the $(\sum_{i=1}^{2^{|T|}} |A|^{2^{|T|}-i} \mu_i)$-th bit of the binary decomposition of $|\langle\varphi\rangle_{\vec{p}, \vec{s}, \vec{t}}(\mathfrak{A})|$ is a 1.

Notice once again the use of dots in variables bound by
the ord operator. We sometimes omit $\vec{s}$ and $\vec{t}$ to improve
readability.

Note that, because FP captures P over ordered structures, all polynomial-time computable arithmetic properties and operations over integers in binary representation can also be defined in FP with this representation of binary integers.

III. FIRST PROPERTIES OF FP + ord

We begin the study of FP + ord. This section is divided as
follows: first, we present some basic facts about FP + ord. In
a second subsection, we introduce the *morphism formalism*,
which is a key part of our labeling coset representation in
Section V. Finally, we show that FP + ord can express any
FP + rk query.

A. Model-checking, membership, union

First, remark that the Schreier-Sims algorithm, introduced
in [14], [15], precisely enables the computation in polynomial-
time of the function $S \mapsto |\langle S \rangle|$. As such, it is quite easy to
show that

**Lemma III.1.** For any fixed formula $\varphi \in (\mathrm{FP} + \mathrm{ord})(\Sigma)$,

$$
\mathrm{Mod}(\varphi) := \{\mathfrak{A} \mid \mathfrak{A} \models \varphi\}
$$

constitutes a polynomial-time decidable class of structures

This constitutes one of the two conditions for a logic to
capture P in the sense of Gurevich [2]. The second one is for
all P-queries to be definable in FP + ord. While we do not
believe this to hold, it remains unknown whether that is the
case.

We now turn to the definition of group-related operations
in FP + ord. First, we show that the composition and inverse
of permutations are definable:

**Lemma III.2.** For any $\mathcal{L} \ge \mathrm{FP}$, given $\mathcal{L}$-formulae $\varphi_\sigma(\vec{s}, \vec{t})$ and $\varphi_\tau(\vec{s}, \vec{t})$, there are formulae $\varphi_{\sigma\tau}(\vec{s}, \vec{t})$ and $\varphi_{\sigma^{-1}}(\vec{s}, \vec{t})$, such that, for any structure $\mathfrak{A}$ on which $\varphi_\sigma$ and $\varphi_\tau$ define permutations,

• $\mathrm{perm}(\varphi_{\sigma\tau}(\mathfrak{A})) = \mathrm{perm}(\varphi_\sigma(\mathfrak{A})) \cdot \mathrm{perm}(\varphi_\tau(\mathfrak{A}))$

• $\mathrm{perm}(\varphi_{\sigma^{-1}}) = \mathrm{perm}(\varphi_\sigma)^{-1}$
### Proof.

$$ \varphi_{\sigma\tau}(\vec{s}, \vec{t}) := \exists \vec{u}, \bigwedge \begin{cases} \varphi_{\tau}(\vec{s}, \vec{u}) \\ \varphi_{\sigma}(\vec{u}, \vec{t}) \end{cases} \\ \varphi_{\sigma^{-1}}(\vec{s}, \vec{t}) := \varphi_{\sigma}(\vec{t}, \vec{s}) \quad \square $$

Besides order computation, the Schreier-Sims algorithm enables another fundamental operation on sets of permutations: given $S \subseteq \text{Sym}(X)$ and $\sigma \in \text{Sym}(X)$, decide if $\sigma \in \langle S \rangle$. We now show that this operation is also definable in FP + ord:

**Lemma III.3.** *Consider a pair of (FP + ord)[Σ] formulae $\varphi(\vec{p}, \vec{s}, \vec{t})$ and $\psi(\vec{s}, \vec{t})$. There is a (FP + ord)[Σ]-sentence $\langle \psi \in \langle \varphi \rangle \rangle_{\vec{p}, \vec{s}, \vec{t}}$ that holds on $\mathfrak{A}$ iff the permutation defined by $\psi$ on $\mathfrak{A}$ belongs to $\langle \varphi \rangle_{\vec{p}, \vec{s}, \vec{t}}(\mathfrak{A})$.*

**Proof.** Fix a structure $\mathfrak{A}$, and let $\tau := \text{perm}(\psi(\mathfrak{A}))$ and $S := \{\text{perm}(\varphi(\mathfrak{A}, \vec{a})) \mid \vec{a} \in A^{\vec{p}}\}$. We rely on the fact that $\tau \in \langle S \rangle$ iff $|\langle S \rangle| = |\langle S \cup \{\tau\} \rangle|$. Consider

$$ \chi(\vec{p}, b, \vec{s}, \vec{t}) := \bigwedge \begin{cases} b = 0 \land \varphi(\vec{p}, \vec{s}, \vec{t}) \\ b = 1 \land \psi(\vec{s}, \vec{t}) \end{cases} \quad (1) $$

$b$ is a fresh numerical variable which enables the definition of the union of $S$ and $\{\tau\}$: for any $\vec{a} \in A^{\vec{p}}$, $\chi(\mathfrak{A}, \vec{a}, 0) = \varphi(\mathfrak{A}, \vec{a})$, and $\chi(\mathfrak{A}, \vec{a}, 1) = \psi(\mathfrak{A})$ (for any other value of $b$, $\chi$ never holds). As such, the set of permutations defined by $\chi$ binding $\vec{p}, b$ is exactly $S \cup \{\tau\}$. Therefore, $\langle \chi \rangle_{\vec{p}, b, \vec{s}, \vec{t}}(\mathfrak{A}) = \langle S \cup \{\tau\} \rangle$. Thus, the formula

$$ (\psi \in \langle \varphi \rangle)_{\vec{p}, \vec{s}, \vec{t}} := (\text{ord}_{\vec{p}, \vec{s}, \vec{t}} \varphi) \hat{=} (\text{ord}_{\vec{p}, b, \vec{s}, \vec{t}} \chi) $$

fulfills the conditions of the lemma. Note that, in this definition, $\hat{=} \text{ denotes the equality of relations, i.e.}$

$$ R \hat{=} R' := \forall \vec{x}, R(\vec{x}) \iff R'(\vec{x}) $$

which, in this context, defines the equality of integers encoded in binary. We use such operations seamlessly, relying on the fact already mentioned below Definition II.4, that all arithmetic polynomial-time computable operations are FP definable. $\square$

Note that we have just shown the definability of the permutation group membership quantifier from [16], mentioned in the introduction.

Using the same technique as in the proof of Eq. (1), we can actually construct arbitrary unions of generating sets: given two formulae $\varphi(\vec{p}, \vec{s}, \vec{t})$ and $\psi(\vec{q}, \vec{s}, \vec{t})$,

$$ \chi(b, \vec{p}, \vec{q}, \vec{s}, \vec{t}) := \bigwedge \begin{cases} b = 0 \land \varphi(\vec{p}, \vec{s}, \vec{t}) \\ b = 1 \land \psi(\vec{q}, \vec{s}, \vec{t}) \end{cases} $$

is such that $\langle \chi \rangle_{b \vec{p} \vec{q} \vec{s} \vec{t}}(\mathfrak{A}) = \langle \langle \varphi \rangle_{\vec{p}, \vec{s}, \vec{t}}(\mathfrak{A}) \cup \langle \psi \rangle_{\vec{q}, \vec{s}, \vec{t}}(\mathfrak{A}) \rangle$. This definition can be iterated for any constant number of definable generating sets. However, to define unions of $O(|A|)$ generating sets, we rely on a different representation:

**Lemma III.4.** *Given a formula $\varphi(\vec{\mu}, \vec{p}, \vec{s}, \vec{t})$, let $G_m := \langle \varphi \rangle_{\vec{p}, \vec{s}, \vec{t}}(\mathfrak{A}, \vec{\mu})$, where $\vec{\mu}$ is the unique tuple of numerical values encoding integer $m$. Then, $\langle \varphi \rangle_{\vec{p}, \vec{p}, \vec{s}, \vec{t}}(\mathfrak{A}) = \langle \bigcup_{m < |A| |\vec{\mu}|} G_m \rangle$.*

With those basic tools at our disposal, we can motivate and present the morphism framework mentioned in the introduction.

## B. Morphism-definability

In the previous subsection, we have seen that if a group $G$ admits a FP + ord definable generating set, FP + ord defines the order of $G$ (by definition of ord), and the membership test on $G$ (by Lemma III.3).

However, an important kind of group-theoretic primitives remains unexplored: operations that allow for the definition of subgroups. The ability to construct representations of subgroups is central to many group-theoretic algorithms for graph isomorphism and canonization. Indeed, these algorithms often rely on gradually refining a large group until a generating set for the automorphism group of the graph in question has been computed.<fnref n="1" />

In the most general case — given a generating set for $G$ and a membership test for $H \le G$, output a generating set for $H$ — this operation is known to be at least as hard as Graph Isomorphism, and as such, most probably out of reach of a logic for P.

On the other hand, when we additionally assume $|G|/|H|$ to be polynomially bounded, the Schreier-Sims algorithm enables a polynomial-time procedure to obtain a generating set for $H$, given a generating set for $G$ and a membership test for $H$. This fact is central to the polynomial-time Graph Isomorphism (and Canonization) algorithms for restricted classes of graphs introduced in [10]–[12]. Yet, this approach also appears incompatible with FP + ord due to the need for selecting coset representatives, a process at odds with the isomorphism-invariance of FP + ord.

In this subsection, we introduce yet another restriction on $H$ which ensures that its cosets in $G$ can be represented in FP + ord: when FP + ord can define a morphism $m: G \to K$, for some permutation group $K$, such that the kernel of $m$ equals $H$ (all morphisms related notions are defined below). We call such a subgroup $H$ morphism-definable from $G$. Such subgroups constitute a tractable scenario where cosets and intersections of subgroups can be defined within FP + ord. However, it does not seem possible, given a morphism-definable subgroup $H$ of $G$, to define a generating set for $H$. As such, all our results on morphism-definable subgroups rely on a shift of representation of groups: in this new context, a group is represented by a pair $(S, m)$, where $m: \langle S \rangle \to K$ for some $K$, such that $H = \{g \in \langle S \rangle \mid m(g) = 1\}$. For this representation of groups to be useful, we must also show that the order and membership tests of morphism-definable subgroups can be defined in FP + ord.

Recall that $H$ is a normal subgroup of $G$, denoted $H \le G$, if $H \le G$ and, for all $g \in G$, $gH = Hg$. A group morphism

<footnote n="1">¹While this process is critical to graph canonization, it also involves the problem of defining labeling cosets at each restriction step — a topic we defer to later discussions.</footnote>
is a function $m: G \to K$, for $G, K$ two groups, which is compatible with the operations of $G$ and $K$, i.e. $\forall g, g' \in G$,

$$m(g \cdot g') = m(g) \cdot m(g')$$

We denote $\ker(m) := \{g \in G \mid m(g) = \text{Id}\}$ and $\text{im}(m) := \{m(g) \mid g \in G\}$. The first isomorphism theorem states that, for any such morphism $m$,

$$|\text{im}(m)| = \frac{|G|}{|\ker(m)|}.$$

Finally, recall that $\ker(m) \trianglelefteq G$, and each normal subgroup of $G$ is realized this way: $H \trianglelefteq G$ iff there is a morphism $m: G \to K$ for some group $K$ such that $\ker(m) = H$.

**Definition III.5.** For $T, T'$ two types, and $\varphi_m(R, \vec{x}, \vec{y})$ a formula with $R$ a relational variable of type $T \cdot T$, and type $(\vec{x}) = \text{type}(\vec{y}) = T'$, $\varphi_m$ is said to define a morphism $m: G \to \text{Sym}(A^{T'})$ on $\mathfrak{A}$, where $G \leq \text{Sym}(A^T)$ if, for all $\sigma \in G$,

$$\varphi_m(\mathfrak{A}, \text{graph}(\sigma)) = \text{graph}(m(\sigma))$$

$H \trianglelefteq G$ is $\mathcal{L}$-morphism-definable from $G$ in $\mathfrak{A}$ if $\mathcal{L}$ defines a generating set for $G$ in $\mathfrak{A}$, and there is a $\mathcal{L}$-formula $\varphi_m$ which defines a morphism $m: G \to \text{Sym}(A^{T'})$ on $\mathfrak{A}$ such that $\ker(m) = H$.

In this section, we will show that, if $H \trianglelefteq G$ is morphism-definable from $G$, then:

* The order of $H$ is FP + ord definable (Lemma III.7 i)

* Membership to $H$ is FP + ord definable (Lemma III.7 ii)

* Given a second subgroup $H' \trianglelefteq G$ morphism-definable from $G$, their intersection $H \cap H'$ is also a morphism-definable subgroup of $G$. (Corollary III.11)

The first two results ensure that morphism-definability constitutes a reasonable representation of groups, while the third is the motivation for the introduction of this new representation of groups. That is, if we shift our representation of groups from the definability of a generating set of permutations to morphism-definability, an intersection operation on groups morphism-definable from a common group $G$ becomes definable within FP + ord.

As a first intermediate result, we show that, given a definable morphism $m: G \to K$ and a definable generating set for $G$, $\text{im}(m)$ admits a definable generating set.

**Lemma III.6.** Let $\mathfrak{A}$ be a structure. Let $\varphi(\vec{p}, \vec{s}, \vec{t})$ be a formula that defines a permutation on $(\mathfrak{A}, \vec{a})$ for all $\vec{a} \in A^{\vec{p}}$, and let $\varphi_m(R, \vec{x}, \vec{y})$ be a formula defining a morphism $m: G \to \text{Sym}(A^{\vec{x}})$, where $G := \langle\varphi\rangle_{\vec{p}, \vec{s}, \vec{t}}(\mathfrak{A})$. Then, $\text{im}(m)$ admits a definable generating set.

*Proof.*

$$\varphi_{\text{im}(m)}(\vec{p}, \vec{x}, \vec{y}) := \varphi_m(R, \vec{x}, \vec{y})[R(\vec{s}, \vec{t})/\varphi(\vec{p}, \vec{s}, \vec{t})]$$

that is, the formula $\varphi_m$ where all occurences of $R(\vec{s}, \vec{t})$ (for any tuples of variables $\vec{s}$ and $\vec{t}$) are substituted by $\varphi(\vec{p}, \vec{s}, \vec{t})$ with variables suitably renamed to avoid capture. $\square$

Moreover, given such a $v \in \text{im}(m)$,

$$m^{-1}(v) = \{\sigma \in G, m(\sigma) = v\}$$

is a coset of $\ker(m)$, equal to $\sigma \ker(m)$ for any $\sigma \in m^{-1}(v)$. Recall that we have argued at the beginning of this section that, unlike in the computational framework, the isomorphism-invariance of FP + ord prohibits the representation of a coset through the choice of a witness. In the case of a subgroup $H$ defined by a morphism $m$, the unique $v$ such that $m(\sigma H) = \{v\}$ constitutes a definable representative of $\sigma H$.

**Lemma III.7.** Let $\varphi_G(\vec{p}, \vec{s}, \vec{t})$, $\varphi_m(R, \vec{x}, \vec{y})$ be two formulae. There are formulae $\varphi \in (R)$, $\varphi_{\text{ord}}(\vec{\mu})$ such that, on any structure $\mathfrak{A}$ on which $\varphi_m$ defines a morphism $m$ from $G := \langle\varphi_G\rangle_{\vec{p}, \vec{s}, \vec{t}}(\mathfrak{A})$ to $\text{Sym}(A^{\vec{x}})$,

(i) $\varphi_{\text{ord}}(\mathfrak{A})$ is a $2|\vec{s}|$-ary numerical predicate encoding $|\ker(m)|$

(ii) for any $\tau \in \text{Sym}(A^{\vec{s}})$, $(\mathfrak{A}, \text{graph}(\tau)) \models \varphi \text{ iff } \tau \in \ker(m)$.

*Proof.* Given $\tau \in \text{Sym}(A^{\vec{s}})$, it is in $\ker(m)$ iff it is in $G$ and $m(\tau) = \text{Id}$. Using Lemma III.3, this is easily definable in FP + ord:

$$\varphi \in (R) := (R(\vec{s}, \vec{t}) \in \langle\varphi_G\rangle)_{\vec{p}, \vec{s}, \vec{t}} \wedge \forall \vec{x}, \varphi_m(R, \vec{x}, \vec{x})$$

To compute the order of $\ker(m)$, we use the fact that $|\ker(m)| = \frac{|G|}{|\text{im}(m)|}$:

$$\varphi_{\text{ord}}(\vec{\mu}) := \left( \frac{(\text{ord}_{\vec{p}, \vec{s}, \vec{t}}\varphi_G)}{(\text{ord}_{\vec{p}, \vec{s}, \vec{t}}\varphi_{\text{im}(m)})} \right) (\vec{\mu})$$

where $(\frac{P}{Q})$ denotes the result of the euclidean division of $P$ by $Q$, where $P$ and $Q$, and $(\frac{P}{Q})$ are $2|\vec{s}|$-ary numerical relations encoding integers bounded by $2^{n^2|\vec{s}|}$. Note that, since euclidean division of integers (encoded in binary) is a polynomial-time computable arithmetic function, the Immerman-Vardi theorem ensures once again that the above expression is definable in FP + ord. $\square$

As mentioned above, the interest of morphism-definable subgroups stems from the ability to consider their intersection:

**Definition III.8.** For $m_1: G \to X$ and $m_2: G \to Y$ two group morphisms, let

$$m_1 \otimes m_2: G \to X \times Y \\ g \mapsto (m_1(g), m_2(g))$$

It is quite clear that $\ker(m_1 \otimes m_2) = \ker(m_1) \cap \ker(m_2)$, and as such, $m_1 \otimes m_2$ defines (from $G$) the intersection of the subgroups defined by $m_1$ and $m_2$ from $G$. It remains to show that, under a suitable permutation representation of direct products of groups, the $\otimes$ operation on morphisms is definable in FPC. Indeed, Definition III.8 relies on direct product of groups, thus we must first provide a representation of direct products of groups in fixed-point logics.
Intuitively, if $X, Y \le \text{Sym}(A)$, we can represent $X \times Y$ as a subgroup of $\text{Sym}(A \times \{0, 1\})$ with

$$ (x, y) \cdot (a, i) := \begin{cases} (x(a), i) & \text{if } i = 0 \\ (y(a), i) & \text{if } i = 1. \end{cases} $$

However, in Section V, we will need to construct the intersection of $O(|A|)$ different subgroups, and as such, we need a representation of polynomially large product of groups $\le \text{Sym}(A^T)$, while keeping the type of tuples on which this representation acts constant. Although the operation at hand is different, this situation is similar to that of Lemma III.4. In the following, we suppose that a family of groups is defined by $\varphi_G(\vec{\mu}, \vec{p}, \vec{s}, \vec{t})$ over $\mathfrak{A}$ binding $\vec{\mu}$, that is, there is a family of groups ($G_k$) where, for $k \le |A|^{\vec{\mu}}$, $G_k := \langle \varphi_G \rangle_{\vec{p}, \vec{s}, \vec{t}}(\mathfrak{A}, \vec{\mu}(k))$, where $\vec{\mu}(k)$ is the unique tuple of numerical values encoding $k$ over $\mathfrak{A}$.

**Lemma III.9.** Let $\varphi_G(\vec{\mu}, \vec{p}, \vec{s}, \vec{t})$ be a FP + ord[$\Sigma$]-formula defining a family of groups binding $\vec{\mu}$, and let $\Omega := A^{\vec{\mu}} \times A^{\vec{s}}$. Then, $\prod_{\vec{n} \in (A \le |\vec{\mu}|)} G_{\vec{n}}$ is isomorphic to a subgroup of $\text{Sym}(\Omega)$. Moreover, there is a FP + ord formula $\varphi_{\Pi G}$ that defines a generating set for this permutation group isomorphic to $\prod G_k$.

*Proof.* Consider the function $\iota : \prod_k G_k$ on $\Omega$:

$$ \iota : \prod_k G_k \to \text{Sym}(\Omega) \\ (\vec{g}) \mapsto (\langle \vec{\lambda}, \vec{a} \rangle \mapsto (\vec{\lambda}, g_{\vec{\lambda}}(\vec{a}))) $$

It is quite clear that $\iota$ is an injective group morphism. As such, $\iota(\prod_k G_k)$ is a permutation group representing $\prod G_k$

Let us now show that it is definable in FPC. As $\prod G_k$ is generated by $\cup S_k$, where $S_k$ is a generating set for $G_k$, it is sufficient to show that, for any permutation defined by $\varphi_G$, we can define its action on $\Omega$ in FPC:

$$ \varphi_{\Pi G}(\vec{\mu}, \vec{p}, \vec{v}_s, \vec{v}_t, \vec{t}) := \bigwedge \left\{ \begin{array}{l} \vec{v}_s = \vec{v}_t \\ \bigvee \left\{ \begin{array}{l} \vec{\mu} = \vec{v}_s \wedge \varphi_G(\vec{\mu}, \vec{p}, \vec{s}, \vec{t}) \\ \vec{\mu} \neq \vec{v}_s \wedge \vec{s} = \vec{t} \end{array} \right. \end{array} \right\} $$

For any $k < |A|^{\vec{\mu}}$ and any $\vec{c} \in A^{\vec{p}}$, $\varphi_{\Pi G}(\mathfrak{A}, \vec{\mu}(k), \vec{c})$ defines the action of the permutation in $G_k$ whose graph is $\varphi_G(\mathfrak{A}, \vec{\mu}(k), \vec{c})$ on $\Omega$. As such, $\langle \varphi_{\Pi G} \rangle_{\vec{\mu}, \vec{p}}(\mathfrak{A}) \simeq \prod_k G_k$. $\square$

**Lemma III.10.** Consider two formulae $\varphi_G(\vec{p}, \vec{s}, \vec{t})$ and $\varphi_m(\vec{\mu}, R, \vec{x}, \vec{y})$ such that, for all structure $\mathfrak{A}$ and $k < |A|^{\vec{\mu}}$, $\varphi_m(\mathfrak{A}, \vec{\mu}(k))$ defines a morphism $m_k : \langle \varphi_G \rangle_{\vec{p}}(\mathfrak{A}) \to \text{Sym}(A^{\vec{s}})$. There is a formula $\varphi_{\otimes m}(R, \vec{v}_x \vec{x}, \vec{v}_y, \vec{y})$ that defines the morphism

$$ \bigotimes_{k \le |A|^{\vec{\mu}}} m_k : G \mapsto \prod_{k \le |A|^{\vec{\mu}}} \text{im}(m_k) $$

*Proof.*

$$ \varphi_{\otimes m}(R, \vec{v}_s, \vec{s}, \vec{v}_t, \vec{t}) := \bigwedge \left\{ \begin{array}{l} \vec{v}_s = \vec{v}_t \\ \varphi_m(\vec{v}_s, R, \vec{s}, \vec{t}) \end{array} \right\} \quad \square $$

As such, if $m_k$ morphism-defines a group $H_k \le G$, $\otimes_k m_k$ morphism-defines $\cap H_k$. Thus,

**Corollary III.11.** If $(H_i)$ is a FP + ord definable sequence of morphism-definable subgroups of $G$, $\cap H_i$ is morphism-definable in $G$.

Note that we expect the sequence of subgroups to be definable in the sense that the sequence of morphisms defining the groups should be given as a formula $\varphi_m$ as in Lemma III.10.

## IV. DEFINING THE RANK OF A MATRIX

The remainder of this article is devoted to the comparison of FP + rk and FP + ord. In this section, we show that FP + ord is at least as expressive as FP + rk, and we will show in the following section that FP + ord expresses the query shown by Lichter to separate FP + rk from P. Together, those results imply that FP + rk < FP + ord.

To show that FP + rk $\le$ FP + ord, we show that any instance of the rk operator can be defined by a formula in FP + ord. Let us first introduce the rank operator. We denote $\mathbb{F}_p$ the unique finite field with $p$ elements, for $p$ a prime number.

**Definition IV.1.** A relation $R \subseteq X \times Y \times \mathbb{N}$ is said to define a matrix over $(X, Y)$ if, for all $x \in X, y \in Y$, there is a unique $m_{x,y} \in \mathbb{N}$ such that $(x, y, m_{x,y}) \in R$. In such a case, $M_R := (m_{x,y})_{x \in X, y \in Y}$ is the matrix defined by $R$.

In such a case, and for $p$ a prime number, $M_R$ defines a linear map $f_{R,p} : \mathbb{F}_p^X \to \mathbb{F}_p^Y$, that maps $\vec{u} \in \mathbb{F}_p^X$ to $\vec{v} \in \mathbb{F}_p^Y$, where $v_y = (\sum_{x \in X} m_{x,y} u_x)$ mod $p$. The rank of this linear map, denoted $\text{rank}_p(M_R)$ is the dimension of the vector space $f_{R,p}(\mathbb{F}_p^X)$. Recall that, on input $M_R$, $\text{rank}_p(M_R)$ is computable in polynomial-time through Gaussian elimination.

**Definition IV.2.** For any formula $\varphi(\vec{x}, \vec{y}, \vec{\mu})$ on signature $\Sigma$ with $\vec{\mu}$ and $\vec{\pi}$ tuples of numerical variables of same length,

$$ \psi := (\text{rk}_{\vec{x}, \vec{y}, \vec{\pi}} \varphi \cdot \vec{\pi}) $$

is a relation of type number $\min\{|\vec{x}|, |\vec{y}|\}$ and free variables $\{\vec{\pi}\} \cup \text{free}(\varphi) \setminus \{\vec{x}, \vec{y}, \vec{\pi}\}$.

For any $\Sigma$-structure $\mathfrak{A}$, any $p < |A|^{\vec{\pi}}$, and any valuation $v$ of the free variables of $\psi$:

* if $\varphi(\mathfrak{A}, v)$ defines a matrix $M_{\varphi}^{\mathfrak{A}, v}$ over $(A^{\vec{x}}, A^{\vec{y}})$, $\psi(\mathfrak{A}, v, \vec{\pi} \leftarrow p)$ consists of the unique tuple of numerical values which encodes $\text{rank}_p(M_{\varphi}^{\mathfrak{A}, v})$.

* otherwise, $\psi(\mathfrak{A}, v) = \emptyset$

This definition of the rk operator is very close to [6, Definition 3.3.1], the main distinction being that, to avoid the handling of numerical terms, we define $(\text{rk}\varphi)$ as a numerical relation. Note that the way its semantics are defined, there is at most one value in this relation. Contrary to [6], we only consider the uniform variant of the rk operator — when the size of the field is a variable of the operator. This is the most expressive variant of the rk operator.

We now show that FP + ord $\ge$ FP + rk:

**Theorem IV.3.** Let $\varphi \in (\text{FP} + \text{ord})(\Sigma]$, $\vec{x}, \vec{s}$ be tuples of variables and $\vec{\mu}, \vec{\pi}$ be tuples of numerical variables of the same
length. There is a formula $\psi(\pi) \in (\text{FP} + \text{ord})[\Sigma]$ such that,
for any $p < |A|^{\lvert\pi\rvert}$, $\psi(\mathfrak{A}, \pi \leftarrow p) = (\text{rk}_{\mathfrak{A}, \pi, \vec{\pi}} \varphi(\pi))(\mathfrak{A}, \pi \leftarrow p)$.

Sketch of proof. Fix a structure $\mathfrak{A}$, and let $\mathcal{M}$ be the matrix defined by $\varphi(\mathfrak{A}, v)$ over $(A^{\vec{x}}, A^{\vec{s}})$. To ease notations, let $I := A^{\vec{x}}$ and $J := A^{\vec{s}}$. Recall that $\mathrm{rank}_p(\mathcal{M})$ is the dimension of the image of $\mathcal{M}$, i.e. $\mathrm{im}_{\mathrm{F}_p}(\mathcal{M}) := \{\mathcal{M} \cdot \vec{X}, \vec{X} \in \mathrm{F}_p^I\}$, and

$$
\mathrm{rank}_p(\mathcal{M}) = \log_p |\mathrm{im}_{\mathrm{F}_p}(\mathcal{M})|
$$

Since the base $p$ logarithm is a P-computable arithmetic function, it can be defined in FPC, and it is only left to show that $|\mathrm{im}_{\mathrm{F}_p}(\mathcal{M})|$ can be defined in FP + ord.

$\mathrm{im}_{\mathrm{F}_p}(\mathcal{M})$ is a subgroup of the additive group of $\mathbb{F}_p^J$, and it is the image of the group-morphism $f_{\mathcal{M},p} : \mathbb{F}_p^I \to \mathbb{F}_p^J$ as defined below Definition IV.1. Thus, the theorem reduces to the definability of a generating set $\mathcal{E}$ for $\mathbb{F}_p^I$ and of the morphism $f_{\mathcal{M},p}$, using Lemma III.6. However, because the general definition within FP + ord of the morphism $f_{\mathcal{M},p}$ is quite convoluted, we will instead provide directly a formula enumerating $f_{\mathcal{M},p}(\mathcal{E})$. The formulae defining $f_{\mathcal{M},p}(\mathcal{E})$ are provided in appendix, Section A.
$\square$

<figure><img src="image_1.png" /></figure>

Let us mention that this proof actually generalises to broader
algebraic structures than fields: for instance, for any ring<fnref n="2" />
$\mathcal{R}$, a set of linear equations over $\mathcal{R}$ can be represented as
a matrix $\mathcal{M} \subseteq \mathcal{R}^{I \times J}$ for some index-sets $I, J$. As long as
$|\mathcal{R}| \le |A^k|$ for some $k$, and the addition and multiplication
in $\mathcal{R}$ are provided, we can construct a generating set for the
additive group $\mathrm{im}_{\mathcal{R}}(\mathcal{M}) := \{\mathcal{M} \cdot X, X \in \mathcal{R}^I\}$.

This bears some importance as further candidate logics for P
have been considered [6], [16], introducing operators allowing
to check, given such a matrix M and a tuple Y ∈ R<sup>J</sup>, whether
there is a tuple X ∈ R<sup>I</sup> such that M · X = Y. This is the
Ring Equation Satisfiability operator (RES).

Since a generating set for $\mathrm{im}_{\mathcal{R}}(\mathcal{M})$ can, under the assumptions given above, be defined in FP + ord, we can check whether $Y \in \mathrm{im}_{\mathcal{R}}(\mathcal{M})$ using the membership operator defined in Lemma III.3, which shows that FP + ord is also at least as expressive as FP + RES.

V. SEPARATION OF RANK AND GROUP ORDER LOGICS

In this section, we show that the ord operator is strictly more
expressive than the rk operator (in the context of fixed-point
logics). We have just shown that FP + rk ≤ FP + ord, so that
it is only left to exhibit a property inexpressible in FP + rk
that is definable in FP + ord.

Recently, Lichter [8] provided such a property separating
FP + rk from CPT (although whether FP + rk ≤ CPT
remains unknown). More precisely, Lichter exhibits a class
of structures $\mathcal{K}$ and a property $\mathcal{P} \subseteq \mathcal{K}$ such that no FP + rk
formula expresses $\mathcal{P}$, while $\mathcal{P}$ is CPT-definable.

The CPT-definability of $\mathcal{P}$ stems from the fact that $\mathcal{P}$
is P-computable, and that CPT canonizes structures in $\mathcal{K}$.

The ability of CPT to canonize structures in $\mathcal{K}$ is a direct consequence of the fact that those structures have *definable abelian colors*, a notion that we will make precise in the second section of this chapter. The fact that structures with abelian colors can be canonized in CPT was proved in [18].

We will show that FP + ord also canonizes structures with abelian colors. First, we review the notion of abelian colors and the method used in [18] to canonize those structures in CPT. Subsequently, we adapt this method in the context of FP + ord.

A. Canonizing structures with abelian colors

A coloring of a structure $\mathfrak{A}$ is a function $c : A \to [m]$ for some $m$. For $i \le m$, the $i$-th color-class of $\mathfrak{A}$ is the set $c^{-1}(i) \subseteq A$, denoted $A_i$. A coloring is usually represented within a structure as a total pre-order $\leq$ (i.e. a total, transitive, reflexive binary relation), such that $c^{-1}(i)$ is the set of elements which admit a maximal $\prec$-increasing sequence of length $i$ (where $x \prec y$ iff $x \leq y \land \neg y \leq x$).

An abelian group is a commutative group. A group $G$ is said to act on a set $X$ if we are given a morphism $m : G \to \text{Sym}(X)$. A group action is faithful if $m$ is injective ; it is transitive if $\{m(g)(x), g \in G\} = X$ for some (and thus all) $x \in X$. When $G \leq \text{Sym}(X)$ we say that $G$ is transitive if its action through the identity morphism is transitive.

**Definition V.1.** A $\Sigma$-structure with *Abelian colors* is a $\Sigma \cup \{\leq, \Phi\}$-structure $\mathfrak{A}$, where type($\leq$) = element<fnref n="2" /> and type($\Phi$) = number²element<fnref n="2" />, such that:

* $\leq$ is a total pre-order on $A$. From now on, let $m$ be the number of equivalence classes of $\leq$; and $A_i$ be the $i$-th equivalence class.

* for any $i < m$, $j < |A_i|$, $\Phi(\mathfrak{A}, i, j)$ is the graph of a permutation $\gamma_j^i \in \text{Sym}(A_i)$ (recall that $\Phi(\mathfrak{A}, i, j) = \{(s, t) \mid (i, j, s, t) \in \Phi^{\mathfrak{A}}\}$);

* for any $i < m$, $\Gamma_i := \{\gamma_j^i \mid j < |A_i|\}$ is an abelian, transitive permutation group over $A_i$.<fnref n="3" />

That is, $\mathfrak{A}$ has abelian colors if it is equipped with a total pre-order $\leq$ and a relation $\Phi$ that explicitly enumerates a family of abelian transitive groups acting on each of the color-classes defined by $\leq$. Even more so, the type of $\Phi$ implies that each of those groups is linearly ordered. Given a $\Sigma$-structure $\mathfrak{A}$, we call such an interpretation of $\leq$ and $\Phi$ on $\mathfrak{A}$ an *abelian coloring* of $\mathfrak{A}$. Note that we require that $|\Gamma_i| \le |A_i|$. This always holds because a transitive abelian group $G \le \text{Sym}(X)$ has exactly $|X|$ elements:

**Lemma V.2.** Let $G$ be an abelian group acting faithfully and transitively on a set $X$. Then, the action of $G$ on $X$ is regular, i.e. for any $x \in X$ and $g \in G$, $g \cdot x = x \iff g = 1$. As such, for any fixed $y \in X$, the map $g \mapsto g \cdot y$ is a bijection between $G$ and $X$.

*Proof.* Consider $g \in G$ such that $g \cdot x = x$. We will show that $g = 1_G$. Because the action of $G$ on $X$ is faithful, this

<footnote n="2">²Let us recall that a ring has the same properties as a field, except for the existence of multiplicative inverses. That is, we only consider commutative rings with a multiplicative identity.</footnote>

<footnote n="3">³Note that as a subgroup of $\text{Sym}(A_i)$, $\Gamma_i$ acts faithfully on $A_i$.</footnote>
amounts to show that, for any $y, g \cdot y = y$. Consider such a $y \in X$, and by transitivity, let $h \in G$ such that $h \cdot x = y$. Then,

$$ g \cdot y = (hh^{-1}g) \cdot y = (hgh^{-1}) \cdot y \quad \text{since } G \text{ is abelian} \\ = (hg) \cdot x = h \cdot x = y \quad \square $$

The structures defined by Lichter to separate FP+rk from P have abelian colors [8], [18]. Moreover, a direct adaptation of [21, Theorem 5.5.1] implies that the canonization of structures with abelian colors reduces to the canonization of graphs with abelian colors. Together, those results reduce the separation between FP + rk and FP + ord to the canonization of graphs with abelian colors in FP + ord.

**Theorem V.3.** FP+ord canonizes graphs with abelian colors.

**Corollary V.4.** FP + rk < FP + ord.

The remainder of this section is devoted to the proof of Theorem V.3. In [18], the author introduces an algorithm to canonize structures with abelian colors. We will follow the same procedure. Before we present this algorithm, a few introductory definitions are in order. Fix a colored graph $\mathfrak{A}$ and let $c$ be its coloring. We denote $A_i$ the $i$-th color-class of $\mathfrak{A}$, and $E_{i,j}$ the edges between $A_i$ and $A_j$, i.e. $E_{i,j} := E \cap (A_i \times A_j \cup A_j \times A_i)$. An ordering of $A$ consistent with $c$ is a bijection $\sigma : A \to A^<$ such that for any $a, b \in A$, $c(a) < c(b) \implies \sigma(a) < \sigma(b)$. Let $A_i^< := \sigma(A_i)$ for some ordering $\sigma$ consistent with $c$. Note that this definition of $A_i^<$ does not depend on the choice of $\sigma$. An ordering of $A_i$ consistent with $c$ is a bijection $\sigma : A_i \to A_i^<$. It is clear that any ordering of $A$ consistent with $c$ can be decomposed in a product $\prod_{i \le m} \sigma_i$, where $\sigma_i$ is an ordering of $A_i$ consistent with $c$. Given a relation $R$ over $A$ and $\sigma$ an ordering of $A$, we can define the encoding of $R$ relative to $\sigma$, denoted $R^\sigma$: $R^\sigma$ has type number$^{|type(R)|}$, and $R^\sigma := \{(\sigma^*(v_1), \sigma^*(v_2), \dots, \sigma^*(v_l)) \mid (v_1, \dots, v_l) \in R\}$, where

$$ \sigma^*(v) := \begin{cases} \sigma(v) & \text{if } v \in A \\ v & \text{if } v \in A^< \end{cases} $$

A set of orderings $C$ is said to canonize $R$ if, for any $\sigma, \tau \in C$, $R^\sigma = R^\tau$. From now on, we only consider orderings consistent with the coloring of the structure at hand. Moreover, an ordering $\sigma$ is definable in $\mathcal{L}$ if there is a $\mathcal{L}$-formula such that $\varphi(\mathfrak{A}) = \text{graph}(\sigma)$. It is easy to show that, if $R$ and $\sigma$ are definable in $\mathcal{L}$, $R^\sigma$ is definable as well (for any logic $\mathcal{L}$ extending FPC).

Algorithm 1 presents the canonization procedure used in the context of CPT in [18]. As a first remark, note that for this canonization procedure to be complete, we should also provide relations ($\preceq$) and $\Phi^<$$. We will actually see in Lemma V.7 that the initial value of $C$ already canonizes $\Phi$, and because by construction, all orderings in $C$ are consistent with $c$, $C$ canonizes $\preceq$ as well.

The structure of this algorithm in and of itself is easily definable in FPC: the only control-flow mechanism is a

**Input** : $\mathfrak{A} = (A, E, \preceq, \Phi)$ a structure with Abelian colors

**Output:** A numerical relation $E^<$ isomorphic to $E$

1. Find, for each $i \le m$, a canonical set $O(A_i)$ of orderings of $A_i$;

2. $C := \prod_{i=1}^m O(A_i)$;

3. **for** $(i, j) \in [m]^2$ **do**

4. &nbsp;&nbsp;&nbsp;&nbsp; $E_{i,j}^<$, the smallest lexicographical encoding of $E_{i,j}$ which is compatible with $C$, i.e.

$$ \exists \sigma \in C, E_{i,j}^{\sigma} = E_{i,j}^{<}; $$

5. &nbsp;&nbsp;&nbsp;&nbsp; $C \leftarrow \{\sigma \in C, E_{i,j}^{\sigma} = E_{i,j}^{<}\}$;

6. **end**

7. **return** $E^< := \bigcup_{i,j} E_{i,j}^<$

**Algorithm 1:** canonisation procedure

for-loop over an ordered domain, which can obviously be implemented in FPC. On the other hand, it is not obvious how to represent sets of orderings, and it is precisely in how this is achieved that we depart from [18]. Before delving into this question, we show that the construction of sets $O(A_i)$ on line 1 of Algorithm 1 is FPC-definable. To ease reading, throughout this section, we fix a graph $\mathfrak{A}$ with abelian colors.

**Lemma V.5.** There is an FPC-formula $\text{map}(\lambda, x, y, \mu)$ such that, for $i \le m$ and $a \in A_i$, $\text{map}(\mathfrak{A}, i, a)$ defines an ordering of $A_i$ (that is, a bijection between $A_i$ and $A_i^<$)

*Proof.* First, Lemma V.2 ensures that the action of $\Gamma_i$ on $A_i$ is regular. Thus, for any fixed $a \in A_i$,

$$ \gamma_1^i(a) < \gamma_2^i(a) < \dots < \gamma_{|A_i|}^i(a) \quad (2) $$

defines a linear ordering on $A_i$. This ordering corresponds to a bijection between $A_i$ and $A_i^<$ whose graph is easily definable in FPC, using $\Phi$ and some basic arithmetic. The formal definition of the formula map is provided in Section B-A. $\square$

We denote $\text{map}_a^i$ the ordering defined by $\text{map}(\mathfrak{A}, i, a)$. By definition of map, with the notations introduced above, we have, for any $a, b \in A_i$ and $\mu \in A_i^<$,

$$ \text{map}_a^i(b) = \mu \iff \gamma_\mu^i(a) = b. \quad (3) $$

We follow Pakusa's notation and denote $O(A_i)$ the set of all $\text{map}_a^i$, for $a \in A_i$. $O(A_i)$ is not an arbitrary set of orderings:

**Lemma V.6.** For any $i \le m$ and $a \in A_i$, $O(A_i) = \text{map}_a^i \Gamma_i$.

*Proof.* Let $a \in A_i$, and $\gamma_j^i \in \Gamma_i$. Then, for any $b \in A_i$,

$$ \text{map}_a^i \gamma_j^i \cdot b = \mu \iff \gamma_\mu^i \cdot a = \gamma_j^i \cdot b \quad \text{by Eq. (3)} $$

$$ \iff ((\gamma_j^i)^{-1} \gamma_\mu^i) \cdot a = b $$

$$ \iff \gamma_\mu^i \cdot ((\gamma_j^i)^{-1} \cdot a) = b \quad (\Gamma_i \text{ is abelian}) $$

$$ \iff \text{map}_{(\gamma_j^i)^{-1} \cdot a}^i \cdot b = \mu $$

Therefore, $O(A_i)$ is closed by multiplication on the right (i.e. precomposition) by elements of $\Gamma_i$, or, said differently,
$map_a^i \Gamma_i \subseteq \mathcal{O}(A_i)$. The transitivity of $\Gamma_i$ yields the other inclusion: for $a, b \in A_i$, let $\gamma_j^i$ be the element<fnref n="4" /> such that $\gamma_j^i \cdot b = a$. Then, $map_a^i \gamma_j^i = \mathit{map}_{(\gamma_j^i)^{-1} \cdot a}^i = \mathit{map}_b^i$. □

We now show that $\mathcal{O}(A_i)$ canonizes $\Phi(\mathfrak{A}, i)$:

**Lemma V.7.** For any $a, b \in A_i$, the encodings of $\Phi(\mathfrak{A}, i)$ relative to $map_a^i$ and $map_b^i$ are equal.

*Proof.* Fix $i \le m, j \in [A_i], a \in A_i$. Then, the following holds:

$$ \begin{aligned} \Phi^{\mathit{map}_a^i}(i, j) &= \{(\mathit{map}_a^i \cdot b, \mathit{map}_a^i \gamma_j^i \cdot b), b \in A_i\} \\ &= \{(\alpha, \mathit{map}_a^i \gamma_j^i (\mathit{map}_a^i)^{-1} \cdot \alpha), \alpha \in A_i^<\} \end{aligned} $$

In words, encoding $\Gamma_i$ relative to $map_a^i$ entails to enumerate the elements of $\Gamma_i$ conjugated by $map_a^i$. It happens that the conjugation actions of $map_a^i$ and $map_b^i$ on $\Gamma_i$ coincide:

$$ \begin{aligned} (\gamma_j^i)^{\mathit{map}_a^i} &= \mathit{map}_a^i \gamma_j^i (\mathit{map}_a^i)^{-1} \\ &= \mathit{map}_a^i \gamma_j^i (\mathit{map}_a^i)^{-1} \mathit{map}_b^i (\mathit{map}_b^i)^{-1} \end{aligned} $$

$$ \begin{aligned} \text{Since } \Gamma_i \text{ is abelian, } \quad &= \mathit{map}_a^i (\mathit{map}_a^i)^{-1} \mathit{map}_b^i \gamma_j^i (\mathit{map}_b^i)^{-1} \\ &= \mathit{map}_b^i \gamma_j^i (\mathit{map}_b^i)^{-1} \\ &= (\gamma_j^i)^{\mathit{map}_b^i} \end{aligned} $$

Note that we have used the fact that $(\mathit{map}_a^i)^{-1} \mathit{map}_b^i \in \Gamma_i$, which is a direct consequence of Lemma V.6. □

It is now time to discuss the representation of sets of orderings. Indeed, Algorithm 1 shows that the proof of Theorem V.3 reduces to the existence of a FP + ord-definable representation of sets of orderings which enables the four following operations:

* The definition of $C_0 := \prod_{i=1}^m \mathcal{O}(A_i)$, as on line 2 of Algorithm 1.

* Given $i, a$ and $j, b$, the definition of the set $C_{a,b}^{i,j}$ of orderings in $C_0$ which yield the same encoding of $E_{i,j}$ as $\mathit{map}_a^i \oplus \mathit{map}_b^j$.

* Given $C, C'$, the definition of $C \cap C'$.

* Given $C$, checking if $C = \emptyset$.

Let us show how these operations enable the definition of line 4 of Algorithm 1. Given $C$, define a binary relation $\mathrm{Comp}_C$ which holds on $(a, b)$ iff $\mathit{map}_a^i \oplus \mathit{map}_b^j = \sigma_{\upharpoonright A_i \cup A_j}$ for some $\sigma \in C$:

$$ \mathrm{Comp}_C(x, y) := (C_{x,y}^{i,j} \cap C) \neq \emptyset $$

Then, find a pair $(a, b) \in \mathrm{Comp}_C$ which yields the minimal encoding of $E_{i,j}$:

$$ \min_C(x, y) := \bigcirc \left\{ \begin{array}{l} \mathrm{Comp}_C(x, y) \\ \forall x', y' \bigcirc \left( \begin{array}{l} \neg \mathrm{Comp}_C(x', y') \\ (E_{i,j})^{\mathit{map}_x^i \oplus \mathit{map}_y^j} \le (E_{i,j})^{\mathit{map}_{x',}^i \oplus \mathit{map}_{y',}^j} \end{array} \right) \end{array} \right\} $$

(where $\le$ denotes the lexicographical comparison of numerical relations, which is obviously FPC-definable). Because all pairs

$(a, b) \in \min_C(\mathfrak{A})$ yield the same encoding of $E_{i,j}$, we can define

$$ E_{i,j}^{<}(\mu, \nu) := \exists x, y, s, t, \bigcirc \mathit{map}(i, x, s, \mu) \wedge \mathit{map}(j, y, t, \nu) \quad \begin{cases} \min_C(x, y) \\ E(s, t) \end{cases} $$

The new set of orderings $C'$ defined on line 5 is then $C \cap C_{a,b}^{i,j}$ for any $(a, b) \in \min_C(\mathfrak{A})$. The definition of line 2 is a direct application of the definability of $C_0$.

In order to define such a representation of sets of orderings, let us first remark that the sets under consideration along the run of Algorithm 1 have a strong structural property: they are of the form $\sigma\Lambda$, for some $\sigma \in C_0$, and $\Lambda$ a subgroup of $\Gamma := \prod_{i=1}^m \Gamma_i$. We call such sets *labeling cosets*. The fact that those sets are all labeling cosets is a direct consequence of the three following lemmas:

**Lemma V.8.** For any $\pi \in C_0$, we have $C_0 = \pi\Gamma$.

*Proof.* This is a direct consequence of Lemma V.6 □

**Lemma V.9.** For any $i, j$, there is a group $\bar{\Delta}_{i,j} \le \Gamma$ such that $C_{a,b}^{i,j} = \sigma\bar{\Delta}_{i,j}$ for any $\sigma \in C_0$ s.t. $\sigma_{\upharpoonright A_i \cup A_j} = \mathit{map}_a^i \oplus \mathit{map}_b^j$.

*Proof.* Let $\bar{\Delta}_{i,j} = (\Gamma_i \Gamma_j \cap \mathrm{Aut}(E_{i,j})) \cdot \prod_{\lambda \in [m] \setminus \{i,j\}} \Gamma_\lambda$, where $\mathrm{Aut}(E_{i,j})$ is the group of permutations of $A_i \cup A_j$ which stabilize $E_{i,j}$. The proof is straight-forward. □

**Lemma V.10.** Given two labeling cosets $\sigma\Lambda, \tau\Lambda'$, $\sigma\Lambda \cap \tau\Lambda'$ is either empty, or a labeling coset of $\Lambda \cap \Lambda'$.

*Proof.* Suppose $C := \sigma\Lambda \cap \tau\Lambda' \neq \emptyset$ and let $\rho \in C$. Then, $\sigma\Lambda = \rho\Lambda$, $\tau\Lambda' = \rho\Lambda'$ and $C = \rho\Lambda \cap \rho\Lambda' = \rho(\Lambda \cap \Lambda')$. □

At this point, let us point out that the algorithm we are aiming to define is a special case of the canonical placement-coset algorithm defined by Babai and Luks in [12, Section 3.2]. However, in the algorithmic context, a labeling coset $\sigma\Lambda$ can be represented by an arbitrary witness $\tau \in \sigma\Lambda$ and a generating set for $\Lambda$. Such an arbitrary choice is not isomorphism-invariant. Here, the fact that $\Gamma$ is abelian comes at play: in this context, any labeling coset $\sigma\Lambda$ is such that $\Lambda \le \Gamma$, and thus there is a morphism $m_\Lambda : \Gamma \to X_\Lambda$ for some group $X_\Lambda$, such that $\ker(m_\Lambda) = \Lambda$. In such a case, $m_\Lambda$ defines a bijection between cosets of $\Lambda$ and $\mathrm{im}(m_\Lambda)$.

This leads to a second issue with the unordered domain: while in the algorithmic context, a labeling coset $\sigma\Lambda$ is a coset of $\Lambda$ in a group $\mathcal{G}$ that contains $\Lambda$ as a subgroup, this is not the case here, as orderings (i.e. bijections from $A$ to $A^<$), unlike *reorderings* (i.e. bijections from $A^<$ to $A^<$) cannot be composed with one another.

To overcome this, we now show that we can define in FPC a representation $\varphi$ of orderings as permutations over a fixed domain ($A^T$ for some fixed type $T$). Then, setting $\mathcal{G} := \langle\varphi(\pi\Gamma)\rangle$, we will show that for any labeling coset $\sigma\Lambda$ considered during the run of Algorithm 1, $\varphi(\sigma\Lambda)$ is a coset of a morphism-definable subgroup of $\mathcal{G}$. With a few encoding details, this will conclude our proof of Theorem V.3, as Corollary III.11 and Lemma III.6 ensure that FP + ord

<footnote n="4">⁴Recall that $\Gamma_i$ is regular, and thus this element is unique</footnote>

<footnote n="5">⁵Where, $f \oplus g$ is the minimal common extension of $f$ and $g$ (if such an extension exists).</footnote>
defines the intersection operation and checks the emptiness of
morphism-definable labeling cosets, respectively.

B. Orderings as permutations

Fix some $\pi \in \prod_i O(A_i)$, and let $\pi_i := \pi_{\upharpoonright A_i}$. Recall that, by Lemma V.8, $\pi\Gamma = \prod_i O(A_i)$.

Let us first give an intuition of our construction: suppose we were given a “base” ordering $f: A \to A^<$. Then, there is a bijection mapping any $g: A \to A^<$ to the permutation of $A$ that maps $f$ to $g$ through composition, that is, $f^{-1}g$. Here, while we obviously do not have access to such a fixed single ordering, for each color class $A_i$, we have a canonical family $\pi_i\Gamma_i$ of $|A_i|$ “base” orderings$^6$, and therefore any $\sigma \in \pi_i\Gamma_i$ can be mapped injectively to $\Gamma_i^{A_i}$:

$$
\varphi_i : \pi_i \Gamma_i \to \Gamma^A \\
\sigma \mapsto \left( b \mapsto \begin{cases} (\mathrm{map}_b^i)^{-1} \sigma & \text{if } b \in A_i \\ \mathrm{Id} & \text{otherwise} \end{cases} \right)
$$

This encoding is compatible with the morphism

$$
\psi_i : \Gamma_i \to \Gamma^A \\
\gamma \mapsto \left( b \mapsto \begin{cases} \gamma & \text{if } b \in A_i \\ \mathrm{Id} & \text{otherwise} \end{cases} \right)
$$

in the sense that $\forall \sigma \in \pi_i \Gamma_i, \gamma \in \Gamma_i, \varphi_i(\sigma\gamma) = \varphi_i(\sigma)\psi_i(\gamma)$.
Note that this implies that, for any $\sigma, \tau \in \pi_i \Gamma_i$,

$$
\varphi_i(\sigma)^{-1} \varphi_i(\tau) = \psi_i(\sigma^{-1}\tau) \quad (4)
$$

For any $\sigma \in \pi_i \Gamma_i$ and $\gamma \in \Gamma_i$, $\varphi_i(\sigma)$ and $\psi_i(\gamma)$ are families of
elements of $\Gamma$ indexed by $A$, and given $a \in A$, we denote the
$a$-component of $\varphi_i(\sigma)$ (resp. $\psi_i(\gamma)$) by $\varphi_i(\sigma)_a$ (resp. $\psi_i(\gamma)_a$).
Note that, while we have defined $\varphi_i$ and $\psi_i$ to range over $\Gamma^A$,
their image is actually quite restricted: first, for any $a \in A$, $\varphi_i(\sigma)_a$ and $\psi_i(\gamma)_a$ are in $\Gamma_i$. Moreover, all the non-trivial
values of $\varphi_i(\sigma)_a$ and $\psi_i(\gamma)_a$ are reached for $a \in A_i$. That is, morally, $\varphi_i$ and $\psi_i$ take values in $\Gamma_i^{A_i}$. However, providing
a uniform codomain to all those functions is convenient, as it
allows us to combine them easily into a “global” representation
of $\pi\Gamma$ within $\Gamma^A$:

$$
\varphi : \pi\Gamma \to \Gamma^A \\
\sigma \mapsto \prod_{i=1}^{m} \varphi_i(\sigma_{\upharpoonright A_i})
$$

$$
\psi : \Gamma \to \Gamma^A \\
\gamma \mapsto \prod_{i=1}^{m} \psi_i(\gamma_{\upharpoonright A_i})
$$

$\varphi$ is compatible with $\psi$, hence $\varphi(\pi\Gamma) = \varphi(\pi)\psi(\Gamma)$ is a coset of $\psi(\Gamma)$. Moreover, as was the case for $\varphi_i$ and $\psi_i$:

$$
\varphi(\sigma)^{-1} \varphi(\tau) = \psi(\sigma^{-1} \tau) \quad (5)
$$

One can also easily check that $\varphi_i, \psi_i$ are injective for all $i \le m$, and thus so are $\varphi$ and $\psi$. As a side note, $\Gamma^A$ is

not exactly a permutation group, but a product of permutation
groups. However, we can use Lemma III.9 to represent $\Gamma^A$
as a subgroup of $\text{Sym}(A \times A)$. We will mostly keep this
encoding nuance implicit. $\varphi(\pi\Gamma)$ is a coset of $\psi(\Gamma)$, and
we will show that $\psi(\Gamma)$ is morphism-definable (as defined
in Definition III.5), which will enable the representation of its
coset $\varphi(\pi\Gamma)$ by defining, in FPC:

* A generating set for a group $\mathcal{G}$ that contains both $\varphi(\pi\Gamma)$ and $\psi(\Gamma)$ (as subsets)

* A morphism $m_{init} : \mathcal{G} \to \text{Sym}(\Omega)$ such that $\ker(m_{init}) = \psi(\Gamma)$

* A value $v_{init} \in \text{Sym}(\Omega)$ such that $m_{init}^{-1}(v_{init}) = \varphi(\pi\Gamma)$. Because $\varphi(\sigma) = \prod_{i=1}^{m} \varphi_i(\sigma_{\upharpoonright A_i})$, and for each $\sigma \in \pi\Gamma$, $\sigma_{\upharpoonright A_i} \in \Gamma_i$, we have

$$
\varphi(\pi\Gamma) \subseteq \prod_{i=1}^{m} \varphi_i(\pi_i\Gamma_i) \leq \langle \bigcup_{i=1}^{m} \varphi_i(\pi_i\Gamma_i) \rangle
$$

Therefore, we set $\mathcal{G} := \langle \bigcup_{i=1}^{m} \varphi_i(\pi_i \Gamma_i) \rangle$.

**Lemma V.11.** *There is a FPC formula genG which defines a generating set for $\iota(G)$.*

*Proof.* We remind the reader that we actually define a gener-
ating set for the group $\iota(G)$. By definition of $G$, it is enough
to build a formula genG such that, for any $i, a$,

$$
\operatorname{genG}(\mathfrak{A}, i, a) = \operatorname{graph}(\iota(\varphi_i(\operatorname{map}_a^i))).
$$

Consider the following formula:

$$
\operatorname{genG}(p_1 p_2, b_s x_s, b_t x_t) := \bigwedge \left\{ \begin{array}{l} (b_s = b_t) \\ \bigvee \left\{ \begin{array}{l} \bigwedge \left\{ i(x_s) = p_1 \right. \\ x_t = (\operatorname{map}_{b_s}^{p_1})^{-1} \operatorname{map}_{p_2}^{p_1}(x_s) \\ \left. i(x_s) \neq p_1 \wedge x_s = x_t \right. \end{array} \right. \\ \bigvee \left\{ \begin{array}{l} \bigwedge \left\{ i(x_s) = p_1 \right. \\ x_t = (\operatorname{map}_{b_s}^{p_1})^{-1} \operatorname{map}_{p_2}^{p_1}(x_s) \\ \left. i(x_s) \neq p_1 \wedge x_s = x_t \right. \end{array} \right. \end{array} \right\}
$$

In this formula, $p_1, p_2$ are the enumeration parameters of
this generating set. Note that $p_1$ is numerical (and ranges
over the indices of the color classes), while $p_2$ is a domain
variable. The pairs of variables $b_s x_s$ and $b_t x_t$ are used to
represent permutations in $\text{Sym}(A \times A)$ as in Definition II.4.
For any $i, a \in A \stackrel{\le}{\times} A$, $\mathfrak{A} = \text{genG}(i, a, \vec{s}, \vec{t})$ if $s_1 = t_1$ and
$t_2 = (\text{map}_{s_1}^i)^{-1} \cdot \text{map}_a^i(s_2)$, i.e., if $\vec{t} = \iota(\varphi_i(\text{map}_a^i))(\vec{s})$, which
yields the desired result. $\square$

**Theorem V.12.** *There is an FPC-definable morphism $m_{init}: \mathcal{G} \to \Gamma^{A \times A}$ and an FPC-definable value $v_{init} \in \Gamma^{A \times A}$, such that $\varphi(\pi\Gamma) = \varphi(\pi)\psi(\Gamma) = \{\lambda \in \mathcal{G}, m_{init}(\lambda) = v_{init}\}$.*

That is, we prove that $\psi(\Gamma)$ is morphism-definable from
$\mathcal{G}$ in FPC (by the morphism $m_{init}$), and provide a FPC-
definable value $(v_{init})$ which represent its coset $\varphi(\pi\Gamma)$ (w.r.t.
the morphism $m_{init}$).

*Sketch of proof.* We define $m_{init}$ and $v_{init}$ as follows:

$$
\begin{align*}
m_{init}(\lambda)_{a,b} &:= \begin{cases} \lambda_a \lambda_b^{-1} & \text{if } \exists i, \{a, b\} \subseteq A_i \\ \text{Id} & \text{otherwise} \end{cases} \\
(v_{init})_{a,b} &:= \begin{cases} (\text{map}_a^i)^{-1} \text{map}_b^i & \text{if } \exists i, \{a, b\} \subseteq A_i \\ \text{Id} & \text{otherwise} \end{cases}
\end{align*}
$$

<footnote>$^6$Recall that Lemma V.6 implies that $\pi_i \Gamma_i = O(A_i)$</footnote>
Lemmas B.1 to B.3 in appendix show, respectively, that $m_{init}$ is indeed a morphism, that $m_{init}^{-1}(v_{init}) = \varphi(\pi\Gamma)$, and that $m_{init}$ and $v_{init}$ are FPC-definable, which altogether proves the theorem. Note that Lemma B.1 requires $\Gamma$ to be abelian. $\square$

This concludes the morphism-definability of $C_0$. It is only left to show that $C_{a,b}^{i,j}$ is morphism-definable from $G$, since intersections can be defined using Corollary III.11, and whether a coset represented by $(m, v)$ is empty can be defined using Lemma III.6 (as this is equivalent to $v \notin \text{im}(m)$).

**Theorem V.13.** For each $i < j \le m$, there is a FPC-definable morphism

$$ \vartheta_{i,j} : G \to \text{Sym}(A \times A \times \Omega_{i,j}) $$

and a FPC definable function $v_{i,j} : A_i \times A_j \to \text{Sym}(A \times A \times \Omega_{i,j})$ such that, for any $(a, b) \in A_i \times A_j$ and $\sigma \in \pi\Gamma$,

$$ \vartheta_{i,j}(\varphi(\sigma)) = v_{i,j}(a, b) \iff E_{i,j}^{\sigma} = E_{i,j}^{\text{map}_a^i \oplus \text{map}_b^j} $$

The proof of this theorem relies on the existence of morphisms defining $\Delta_{i,j} := \Gamma_i \Gamma_j \cap \text{Aut}(E_{i,j})$:

**Theorem V.14.** For each $i < j \le m$, there is a FPC definable ordered set $\Omega_{i,j}$, and a FPC definable morphism

$$ m_{i,j} : \Gamma_i \Gamma_j \to \text{Sym}(\Omega_{i,j}) $$

such that $\ker(m_{i,j}) = \Delta_{i,j}$.

**Sketch of proof of Theorem V.14.** Because $\Gamma_i$ and $\Gamma_j$ are abelian, $\Delta_{i,j} \trianglelefteq \Gamma_i \Gamma_j$. Consider the canonical morphism

$$ \theta_{i,j} : \Gamma_i \Gamma_j \to (\Gamma_i \Gamma_j)/\Delta_{i,j} \\ \gamma \mapsto \gamma \Delta_{i,j} $$

Because $\Gamma_i$ and $\Gamma_j$ are ordered by $\Phi$, we can represent each coset by its minimal representative. Let $\Omega_{i,j}$ be the set of those minimal representatives. Note that $|\Omega_{i,j}|$ is polynomially bounded by $|A|$ because $|\Gamma_i \Gamma_j|$ is. The action of $\Gamma_i \Gamma_j$ by left multiplication on $(\Gamma_i \Gamma_j)/\Delta_{i,j}$ defines an action of $\Gamma_i \Gamma_j$ on $\Omega_{i,j}$, and the corresponding morphism is definable within FP+ord. To summarize, for $\gamma \in \Gamma_i \Gamma_j$ and $\omega \in \Omega_{i,j}$, $m_{i,j}(\gamma)(\omega)$ is the unique $\omega' \in \Omega_{i,j}$ such that $\gamma\omega\Delta_{i,j} = \omega'\Delta_{i,j}$. $\square$

**Sketch of proof of Theorem V.13.** We provide the definition of $\vartheta_{i,j}$ and $v_{i,j}$. For readability purposes, we present $\vartheta_{i,j}(\sigma)$ and $v_{i,j}(a, b)$ as elements of $\text{Sym}(\Omega_{i,j})^{A \times A}$ rather than $\text{Sym}(A \times A \times \Omega_{i,j})$, relying on Lemma III.9 as in the previous subsections.

$$ \vartheta_{i,j} : G \to \text{Sym}(\Omega_{i,j})^{A \times A} \\ \lambda \mapsto \left( (a, b) \mapsto \begin{cases} m_{i,j}(\lambda_a \lambda_b) & \text{if } a \in A_i, b \in A_j \\ \text{Id} & \text{otherwise} \end{cases} \right) $$

For $(a_i, a_j) \in A_i \times A_j$, let $v_{i,j}(a_i, a_j) \in \text{Sym}(\Omega_{i,j})^{A \times A}$ be defined, for any $(a, b) \in A_i \times A_j$, as

$$ v_{i,j}(a_i, a_j)(a, b) := m_{i,j}((\text{map}_a^i \oplus \text{map}_b^j)^{-1}\text{map}_{a_i}^i \oplus \text{map}_{a_j}^j) $$

When $(a, b) \notin A_i \times A_j$, we set $v_{i,j}(a_i, a_j)(a, b)$ to Id. In Lemmas C.1 to C.3 in appendix, we show, respectively, that

$\vartheta_{i,j}$ is a morphism, that it behaves as expected regarding to the encoding of $E_{i,j}$, and that both $\vartheta_{i,j}$ and $v_{i,j}$ are FPC-definable, which altogether yield the theorem. $\square$

This concludes the definition of our representation of labeling cosets. An important corollary of Theorem V.13 is that the value of $v_{i,j}$ does not depend on the choice of pair $(a, b)$ within its equivalence class:

**Corollary V.15.** For any two pairs $(a, b), (a', b') \in A_i \times A_j$, if $E_{i,j}^{\text{map}_a^i \oplus \text{map}_b^j} = E_{i,j}^{\text{map}_{a'}^i \oplus \text{map}_{b'}^j}$, then $v_{i,j}(a, b) = v_{i,j}(a', b')$.

This proves that our representation scheme is indeed isomorphism-invariant. Theorem V.3 follows, with its corollary Corollary V.4. We have left some technicalities out of this presentation. In particular, the precise way in which we define this procedure as a fix-point computation requires a few more steps: morphisms are defined by formulae with free second-order variables, not by relations. Indeed, as third order objects, they cannot be seen as variables within a fix-point computation. Instead, we define them syntactically, and only pass the value of $v$ in the representation $(m, v)$ of the current labeling coset. Another second-order variable is used to indicate which morphisms amongst $m_{init} \cup \{\vartheta_{i,j}\}$ are relevant at the current step of computation.

Another omission concerns the internal edges of a color-class: in the present proof, we have only treated the harder case of edges between two distinct color-classes. Indeed, the edges within $A_i$ can be treated in a simpler way: it happens that we can assume $O(A_i)$ to already canonize those edges. For if it does not, we can refine the ordering on $A_i$, by setting $a \prec a'$ if $E_i^{\text{map}_a^i} <_{lex} E_i^{\text{map}_{a'}^i}$. $\Phi$ can be adapted to this finer pre-ordering, since the natural action of $\Gamma_i \cap \text{Aut}(A_i)$ is transitive on each of the new color-classes induced by this refinement. We iterate this refinement process until a fix-point is reached.

# VI. CONCLUSION

We have introduced ord, an operator enabling the definition of permutation group properties within fixed-point logics. As expected, this operator generalizes the rank operator rk, as shown in Theorem IV.3. Perhaps more surprising is the fact that ord is strictly more expressive than rk (Section V). Indeed, this implies that the order of a group represented by a definable generating set is not definable with FP + rk. To prove that FP + ord is more expressive than FP + rk, we have shown that it canonizes structures with abelian colors, by defining the computation of the group-theoretic algorithm for the canonization of graphs defined in [12]. While this algorithm was already defined in a logical context (precisely, in the context of Choiceless Polynomial Time [18]), the use of a group-theoretic operator enabled a purely group-theoretic representation of labeling cosets. This opens the door to novel techniques towards canonization in fixed-point logics: if our representation of labeling cosets relied heavily on the underlying groups being abelian, ordered, and transitive, a more complex representation scheme might allow the relaxation of some of those assumptions.
REFERENCES

[1] A. Chandra and D. Harel, “Structure and complexity of relational queries,” *Journal of Computer and System Sciences*, vol. 25, no. 1, pp. 99–128, Aug. 1982.

[2] Y. Gurevich, “Logic and the Challenge of Computer Science,” *Current Trends in Theoretical Computer Science ed. Egon Boerger*, Jul. 1988. [Online]. Available: https://www.microsoft.com/en-us/research/publication/logic-challenge-computer-science/

[3] J.-Y. Cai, M. Fürer, and N. Immerman, “An optimal lower bound on the number of variables for graph identification,” *Combinatorica*, vol. 12, no. 4, pp. 389–410, Dec. 1992.

[4] A. Dawar, M. Grohe, B. Holm, and B. Laubner, “Logics with Rank Operators,” in *2009 24th Annual IEEE Symposium on Logic In Computer Science*, Aug. 2009, pp. 113–122.

[5] B. Holm, “Descriptive complexity of linear algebra,” Ph.D. dissertation, University of Cambridge, 2010. [Online]. Available: http://bjarkiholm.com/publications/Holm_2010_phd-thesis.pdf

[6] W. Pakusa, “Finite Model Theory with Operators from Linear Algebra,” 2010. [Online]. Available: https://wwwsemanticscholar.org/paper/Finite-Model-Theory-with-Operators-from-Linear-Pakusa/32bd5ab2fde31e3876621140f4a7df3893cb9e8e

[7] E. Grädel and W. Pakusa, “Rank logic is dead, long live rank logic!” *The Journal of Symbolic Logic*, vol. 84, no. 1, pp. 54–87, Mar. 2019.

[8] M. Lichter, “Separating Rank Logic from Polynomial Time,” *J. ACM*, vol. 70, no. 2, pp. 14:1–14:53, Mar. 2023.

[9] M. Grohe, *Descriptive Complexity, Canonisation, and Definable Graph Structure Theory*, 1st ed. Cambridge University Press, Aug. 2017.

[10] L. Babai, “Monte-Carlo algorithms in graph isomorphism testing,” *Université de Montréal Technical Report*, DMS, no. 79-10, 1979. [Online]. Available: https://people.cs.uchicago.edu/~laci/lasvegas79.pdf

[11] E. M. Luks, “Isomorphism of graphs of bounded valence can be tested in polynomial time,” *Journal of Computer and System Sciences*, vol. 25, no. 1, pp. 42–65, Aug. 1982.

[12] L. Babai and E. M. Luks, “Canonical labeling of graphs,” in *Proceedings of the Fifteenth Annual ACM Symposium on Theory of Computing - STOC '83*. ACM Press, 1983, pp. 171–183.

[13] L. Babai, “Graph Isomorphism in Quasipolynomial Time,” Jan. 2016.

[14] C. C. Sims, “Computational methods in the study of permutation groups,” in *Computational Problems in Abstract Algebra*, J. Leech, Ed. Pergamon, Jan. 1970, pp. 169–183.

[15] ——, “Computation with permutation groups,” in *Proceedings of the Second ACM Symposium on Symbolic and Algebraic Manipulation*, ser. SYMSAC '71. New York, NY, USA: Association for Computing Machinery, Mar. 1971, pp. 23–28.

[16] A. Dawar, E. Kopczynski, B. Holm, E. Grädel, and W. Pakusa, “Definability of linear equation systems over groups and rings,” *Logical Methods in Computer Science*, vol. Volume 9, Issue 4, p. 725, Nov. 2013.

[17] P. Schweitzer and D. Wiebking, “A unifying method for the design of algorithms canonizing combinatorial objects,” in *Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing*. Phoenix AZ USA: ACM, Jun. 2019, pp. 1247–1258.

[18] W. Pakusa, “Linear equation systems and the search for a logical characterisation of polynomial time,” Ph.D. dissertation, RWTH Aachen University, 2015. [Online]. Available: http://publications.rwth-aachen.de/record/567588/files/567588.pdf?subformat=pdfa

[19] M. Otto, *Bounded Variable Logics and Counting: A Study in Finite Models*, ser. Lecture Notes in Logic. Cambridge: Cambridge University Press, 2017.

[20] N. Immerman, “Relational queries computable in polynomial time,” *Information and Control*, vol. 68, no. 1, pp. 86–104, Jan. 1986.

[21] W. Hodges, *Model Theory*, 1st ed. Cambridge University Press, Mar. 1993.

APPENDIX A
PROOF OF THEOREM IV.3

Consider the set $\mathcal{E} := \{E_{\vec{a}}^v | \vec{a} \in I, v \in \mathbb{F}_p\}$ of vectors of $\mathbb{F}_p^I$ defined by:

$$E_{\vec{a}}^{v}(\vec{b}) := \begin{cases} 0_{\mathbb{F}_p} & \text{if } \vec{a} \neq \vec{b} \\ v & \text{otherwise} \end{cases}$$

Obviously, any vector $\vec{X} \in \mathbb{F}_p^I$ is of the form $\sum_{\vec{a} \in I} E_{\vec{a}}^{X_{\vec{a}}}$. As such, this constitutes a generating set for $\mathbb{F}_p^I$. We now show how to represent $\mathbb{F}_p^I$ as a permutation group in FPC. First, we represent $v \in \mathbb{F}_p$ as the numerical permutation

$$f_v(w) : w \mapsto \begin{cases} w & \text{if } w \ge p \\ w + v \mod p & \text{otherwise} \end{cases}$$

Let $K := \mathbb{A}^\pi$. $v \mapsto f_v$ defines a morphism from $\mathbb{F}_p$ to $\text{Sym}(K)$, and can obviously be defined in FPC. In the same way, we define a morphism from $\mathbb{F}_p^I$ to $\text{Sym}(I \times K)$:

$$\iota_I(\vec{X})(\vec{a}, w) := (\vec{a}, f_{X_{\vec{a}}}(w))$$

We can define a similar representation $\iota_J$ of $\mathbb{F}_p^J$ in $\text{Sym}(J \times A^\le)$ (note that those representations of products are defined in the same way as in Lemma III.9). We can now define an enumeration of $\iota_I(\mathcal{E})$:

$$\varphi_I(\vec{p}^{\lambda}, \vec{x}^{\mu}, \vec{y}^{\nu}) := \bigcirc \begin{cases} \vec{p} = \vec{x} = \vec{y} \wedge \vec{\mu} < \vec{\pi} \wedge (\vec{\nu} = \vec{\mu} + \vec{\lambda} \mod \vec{\pi}) \\ \vec{p} = \vec{x} = \vec{y} \wedge \vec{\mu} \ge \vec{\pi} \wedge \vec{\nu} = \vec{\mu} \\ \vec{p} \ne \vec{x} = \vec{y} \wedge \vec{\nu} = \vec{\mu} \end{cases}$$

Note that the tuple $\vec{\pi}$ is free in $\varphi_I$. For any $\vec{a}, v, \varphi_I(\mathfrak{A}, \vec{a}, \vec{\lambda} \leftarrow v)$ defines the graph of $\iota_I(E_{\vec{a}}^v)$. We can now define in the same way $\iota_I(f_{\mathcal{M},p}(E_{\vec{a}}^v))$:

$$\varphi_{\text{im}_p}(\mathcal{M})(\vec{p}^{\lambda}, \vec{s}^{\mu}, \vec{t}^{\nu}) := \bigcirc \begin{cases} \vec{\mu} \ge \vec{\pi} \wedge \vec{\mu} = \vec{\nu} \wedge \vec{s} = \vec{t} \\ \exists \vec{m}, \begin{tikzpicture}[baseline=(current bounding box.center)] \draw (-0.5,0) -- (0.5,0); \node at (0,0.5) {$\vec{s} = \vec{t}$}; \node at (0,-0.5) {$\vec{m} = \vec{t}$}; \node at (0.5,0.5) {$\vec{\mu} < \vec{\pi} \wedge \vec{\nu} < \vec{\pi}$}; \node at (0.5,-0.5) {$\vec{\nu} = (\vec{\mu} + \vec{\lambda} \cdot \vec{m}) \mod \vec{\pi}$}; \end{tikzpicture} \\ \varphi_M(\vec{p}, \vec{s}, \vec{m}) \\ \vec{\nu} = (\vec{\mu} + \vec{\lambda} \cdot \vec{m}) \mod \vec{\pi} \end{cases}$$

Let us walk through all variables appearing in this formula. $\vec{p}$ tracks the $I$-component $\vec{a}$ of the unit vector $E_{\vec{a}}^v$ under consideration. The value of $v$ is tracked by $\vec{\lambda}$. $\vec{s}$ and $\vec{t}$ range over $J$, and represent the component of the vector $\mathcal{M} \cdot E_{\vec{a}}^v$ we are currently defining. Per our representation of group products, $\varphi_{\text{im}_p}(\mathcal{M})$ holds only if $\vec{s} = \vec{t}$. $\vec{m}$ tracks the value of the matrix $\mathcal{M}$ at coordinates $\vec{a}, \vec{b}$ where $\vec{a}$ is the current value of $\vec{p}$ and $\vec{b}$ the current value of both $\vec{s}$ and $\vec{t}$.

Therefore, $\langle \varphi_{\text{im}_p}(\mathcal{M}) \rangle_{\vec{p}^{\lambda}, \vec{s}^{\mu}, \vec{t}^{\nu}}(\mathfrak{A}) = \text{im}_{\mathbb{F}_p}(\mathcal{M})$, and our reasoning at the beginning of this proof yields the desired result. $\square$
APPENDIX B
PROOFS OMITTED IN SECTION V

A. *Proof of Lemma V.5*

Consider the formula $\Psi$ defined as follows:

$$
\Psi(\lambda, x, y, \mu) := \Phi(\lambda, \mu, x, y)
$$

(A, i, a, b, k) |=$ \Psi$ iff b is the k-th element in the ordering
of A<sub>i</sub> defined by Eq. (2). However, this defines a bijection
between A<sub>i</sub> and [|A<sub>i</sub>|]. In order to build a bijection whose
image is A<sub>i</sub><sup>&lt;</sup> instead of [A<sub>i</sub>], we add an adequate offset:

$$
\mathrm{map}(\lambda, x, y, \mu) := \exists \nu, \left( \mu = \nu + \sum_{\lambda < \lambda} |A_{\lambda}| \right) \wedge \Phi(\lambda, \nu, x, y)
$$

The definability of those arithmetic operations in FPC is
straight-forward. We have successfully built a formula map
such that, for all $i \le m$ and $a \in A_i$, $map(A, i, a)$ is the graph
of a bijection between $A_i$ and $A_i^<$, and thus defines a partial
ordering over $A_i$.

B. *Proof of Theorem V.12*

**Lemma B.1.** $m_{init} : \mathcal{G} \to \Gamma^{A \times A}$ is a morphism

Proof. Consider $\lambda, \lambda' \in \mathcal{G}$. For any $i \neq j$, $a \in A_i$ and $b \in A_j$,
$m_{init}(\lambda\lambda')_{a,b} = \text{Id} = (m_{init}(\lambda)_{a,b})(m_{init}(\lambda')_{a,b})$.

For $a, b \in A_i$,

$$
\begin{align*}
m_{init}(\lambda\lambda')_{a,b} &= (\lambda\lambda')_a(\lambda\lambda')_b^{-1} \\
&= \lambda_a\lambda'_a\lambda'_b^{-1}\lambda_b^{-1}
\end{align*}
$$

$$
\begin{align*}
\text{Since } \Gamma_i \text{ is abelian, } & = \lambda_a \lambda_b^{-1} \lambda'_a \lambda'_b^{-1} \\
& = m_{\text{init}}(\lambda)_{a,b} \cdot m_{\text{init}}(\lambda')_{a,b}
\end{align*}
$$

<figure><img src="image_2.png" /></figure>

**Lemma B.2.** $\varphi(\pi\Gamma) = \{\lambda \in \mathcal{G}, m_{init}(\lambda) = v_{init}\}$

Proof. For $\sigma \in \pi\Gamma$ and $a, b \in A_i$, we have:

$$
\begin{align*}
m_{init}(\varphi(\sigma))_{a,b} &= \varphi(\sigma)_a \varphi(\sigma)_b^{-1} \\
&= (\mathrm{map}_a^i)^{-1} \sigma \sigma^{-1} \mathrm{map}_b^i \\
&= (v_{init})_{a,b}
\end{align*}
$$

We now show the other inclusion. Let $\lambda \in \mathcal{G}$ such that $m_{init}(\lambda) = v_{init}$. Fix, for all $i$, some $a_i \in A_i$, and let $\sigma_i := \text{map}_{a_i}^i \lambda_{a_i}$. Then, for any $b \in A_i$,

$$
\begin{align*}
\mathrm{map}_b^i \lambda_b &= \mathrm{map}_b^i \lambda_b \lambda_{a_i}^{-1} \lambda_{a_i} \\
&= \mathrm{map}_b^i m_{init}(\lambda)_{b,a_i} \lambda_{a_i} \\
&= \mathrm{map}_b^i (\mathrm{map}_b^i)^{-1} \mathrm{map}_{a_i}^i \lambda_{a_i} \\
&= \sigma_i
\end{align*}
$$

Thus, for any $b$, $\lambda_b = (\mathrm{map}_b^{i(b)})^{-1} \sigma_{i(b)} = \varphi_{i(b)}(\sigma_{i(b)})_b$, which in turn implies that $\lambda = \varphi(\sigma_1 \dots \sigma_m)$. $\square$

<figure><img src="image_3.png" /></figure>

In order to state Lemma B.3, we need a representation of
Sym($A$)$^{A \times A}$ as a permutation group:

$$
\begin{align*}
\iota_2 : \operatorname{Sym}(A)^{A \times A} &\to \operatorname{Sym}(A \times A \times A) \\
(\sigma_{(a,b)})(a,b) \in A \times A &\mapsto ((a, b, c) \mapsto (a, b, \sigma_{(a,b)}(c)))
\end{align*}
$$

**Lemma B.3.**

* There is a formula_ initMorph(R, a_s, b_s, x_s, a_t, b_t, x_t), such that, for any $\lambda \in \mathcal{G}$, initMorph(A, graph(ι(λ))) = graph(ι₂(m_init(λ))).

* There is a formula initValue(a_s, b_s, x_s, a_t, b_t, x_t) that defines in A the graph of ι₂(v_init).

Proof.

$$
\begin{align*}
\text{initMorph}(R, a_s, b_s, x_s, a_t, b_t, x_t) &:= \exists \nu, \sigma \begin{cases}
a_s = a_t \\
b_s = b_t \\
R(b_s, x_t, y) \\
R(a_s, x_s, y)
\end{cases} \\
\text{initValue}(a_s, b_s, x_s, a_t, b_t, x_t) &:= \exists i, \mu, \sigma \begin{cases}
a_s = a_t \\
b_s = b_t \\
\text{map}(i, a_s, x_t, \mu) \\
\text{map}(i, b_s, x_s, \mu)
\end{cases} \quad \square
\end{align*}
$$

C. *Proof of Theorem V.14*

We introduce two intermediate lemmas. First, we show that
the membership to Δ<sub>i,j</sub> is definable in FPC:

**Lemma B.4.** There is a FPC formula aut$(i, j, \mu, \nu)$ such that
$\mathfrak{A} \models \text{aut}(i, j, \alpha, \beta)$ iff $\gamma_{\alpha}^{i} \gamma_{\beta}^{j} \in \Delta_{i,j}$.

Proof. :

$$
\begin{align*}
\text{aut}(i, j, \mu, \nu) &:= \forall a_i \in A_i, a_j \in A_j, \exists b_i, b_j, \sigma \\
&\qquad \begin{cases}
\Phi(i, \mu, a_i, b_i) \\
\Phi(j, \nu, a_j, b_j) \\
\Xi(a_i, a_j, b_i, b_j)
\end{cases}
\end{align*}
$$

where

$$
\Xi(a_i, a_j, b_i, b_j) := E(a_i, a_j) \iff E(b_i, b_j) \quad \square
$$

This in turn enables us to check if two elements of $\Gamma_i \Gamma_j$
belong to the same coset of $\Delta_{i,j}$:

**Lemma B.5.** There is a FPC formula coset$(i, j, \mu, \nu, \mu', \nu')$ such that

$$
\mathfrak{A} \models \text{coset}(i, j, \alpha, \beta, \alpha', \beta') \iff \gamma_{\alpha}^{i} \gamma_{\beta}^{j} \Delta_{i,j} = \gamma_{\alpha'}^{i} \gamma_{\beta'}^{j} \Delta_{i,j}
$$

Proof. For α, β, α', β', γ_α^i γ_β^j Δ_{i,j} = γ_α^i γ_β^j Δ_{i,j} iff χ := (γ_α^i γ_β^j)^-1 γ_α^i γ_β^j Δ_{i,j}. Because Γ_i and Γ_j act on disjoint sets, they commute, thus χ ∈ Γ_iΓ_j and there is a pair (α'', β'') such that χ = γ_α'' γ_β''^j. Because χ ∈ Γ_iΓ_j, χ ∈ Δ_{i,j} is equivalent to χ ∈ Aut(E_{i,j}), which yields the following formula:

$$
\operatorname{coset}(i, j, \mu, \nu, \mu', \nu') := \exists \mu'', \nu'', \sigma \begin{cases} \gamma_{\mu''}^{i} = (\gamma_{\mu'}^{i})^{-1} \gamma_{\mu}^{i} \\ \gamma_{\nu''}^{j} = (\gamma_{\nu'}^{j})^{-1} \gamma_{\nu}^{j} \\ \text{aut}(i, j, \mu'', \nu'') \end{cases}
$$

To ease reading, we have included two clauses of the form
$\sigma = \tau^{-1}\rho$ which are not FPC formulae per se. However,
when the graphs of $\sigma$, $\tau$ and $\rho$ are defined by $R_\sigma$, $R_\tau$ and $R_\rho$, respectively, this equality can easily be defined in FPC. $\square$

We are now ready to prove Theorem V.14:

**Proof of Theorem V.14.** We can choose as a representative of the coset $\sigma\Delta_{i,j}$ the lexicographically smallest pair $(\alpha, \beta)$ such that $\gamma_{\alpha}^{i}\gamma_{\beta}^{j} \in \sigma\Delta_{i,j}$. The following formula holds for $(i, j, \alpha, \beta)$ iff $(\alpha, \beta)$ is such a pair for some coset:

$$ \text{witness}(i, j, \mu, \nu) := \forall \mu', \nu', \bigcirc \begin{cases} \mu\nu \le_{lex} \mu'\nu' \\ -\coset(i, j, \mu, \nu, \mu', \nu') \end{cases} $$

This shows that $\Omega_{i,j} := \text{witness}(\mathfrak{A}, i, j)$ is definable in FPC.

We aim to define $m_{i,j}(\gamma)(\alpha, \beta)$ as the unique $(\alpha', \beta') \in \Omega_{i,j}$ such that $\gamma\gamma_{\alpha}^{i}\gamma_{\beta}^{j} \in (\gamma_{\alpha'}^{i}\gamma_{\beta'}^{j})\Delta_{i,j}$, that is, such that $(\gamma_{\alpha'}^{i}\gamma_{\beta'}^{j})^{-1}\gamma\gamma_{\alpha}^{i}\gamma_{\beta}^{j} \in \Delta_{i,j}$. Note that, rather than keeping $m_{i,j}$ undefined on $(A^\leq)^2 \setminus \Omega_{i,j}$, we simply set it to act trivially. This indeed defines a morphism, as the action of $m_{i,j}(\gamma)$ on $\Omega_{i,j}$ is, by construction, isomorphic to the action of $\gamma$ on the set of cosets of $\Delta_{i,j}$ in $\Gamma_i\Gamma_j$ by left multiplication. For the same reason, $\ker(m_{i,j}) = \Delta_{i,j}$.

$$ \text{slMorph}(i, j, R_{\gamma}, \mu_s \nu_s, \mu_t \nu_t) := \bigcirc \left\{ \begin{array}{@{}l@{}} \neg witness(i, j, \mu_s, \nu_s) \\ \qquad \bigcirc \mu_s = \mu_t \\ \qquad \nu_s = \nu_t \\ witness(i, j, \mu_s, \nu_s) \\ \qquad \neg witness(i, j, \mu_t, \nu_t) \\ \qquad \Xi \end{array} \right. $$

where

$$ \Xi := \exists \mu', \nu', \bigcirc \begin{cases} \gamma_{\mu'}^{i} \gamma_{\nu'}^{j} = (\gamma_{\mu_t}^{i} \gamma_{\nu_t}^{j})^{-1} \gamma \gamma_{\mu}^{i} \gamma_{\nu}^{j} \\ \text{aut}(i, j, \mu', \nu') \end{cases} $$

This corresponds exactly to our definition of a definable morphism, in the sense that for any $\gamma \in \Gamma_i\Gamma_j$,

$$ \text{slMorph}(\mathfrak{A}, i, j, \text{graph}(\gamma)) = \text{graph}(m_{i,j}(\gamma)) $$

Note that, while we usually prefer to keep second order variables on the left-most side, we did not do so this time to underline the fact that slMorph actually defines a family of morphisms, one for each pair of colors.

Finally, let us justify our use of permutations equalities in the definition of $\Xi$. As the graph $R_\gamma$ of $\gamma$ is a parameter of slMorph, and for all $i, \mu$, the graph of $\gamma_\mu^i$ is given by $\Phi(i, \mu)$, the subformula $\gamma_{\mu'}^i \gamma_{\nu'}^j = (\gamma_{\mu_t}^i \gamma_{\nu_t}^j)^{-1}$ is in FPC, following the same idea as in Lemma III.2. $\square$

# APPENDIX C

## PROOF OF THEOREM V.13

**Lemma C.1.** For all $i < j \le m$, $\vartheta_{i,j}$ is a morphism.

**Proof.** Consider $\lambda, \lambda' \in \mathcal{G}$ and $(a, b) \in A \times A$. We aim to show that

$$ (\vartheta_{i,j}(\lambda)\vartheta_{i,j}(\lambda'))_{(a,b)} = \vartheta_{i,j}(\lambda\lambda')_{(a,b)} $$

If $(a, b) \notin A_i \times A_j$, both sides of this equation evaluate to $\text{Id}$. Otherwise,

$$ \begin{align*} (\vartheta_{i,j}(\lambda)\vartheta_{i,j}(\lambda'))_{(a,b)} &= m_{i,j}(\lambda_a \lambda_b) m_{i,j}(\lambda'_a \lambda'_b) \\ &= m_{i,j}(\lambda_a \lambda_b \lambda'_a \lambda'_b) \quad \text{m}_{i,j} \text{ morph.} \\ &= m_{i,j}(\lambda_a \lambda'_a \lambda_b \lambda'_b) \quad \Gamma_i \Gamma_j \text{ ab.} \\ &= \vartheta_{i,j}(\lambda\lambda')_{(a,b)} \quad \square \end{align*} $$

**Lemma C.2.** For any $i < j$, $(a_i, a_j) \in A_i \times A_j$, and $\sigma \in \pi\Gamma$,

$$ \vartheta_{i,j}(\varphi(\sigma)) = v_{i,j}(a_i, a_j) \iff E_{i,j}^{\sigma} = E_{i,j}^{\text{map}_{a_i}^{i} \oplus \text{map}_{a_j}^{j}} $$

**Proof.** First, notice that, for any $i < j$ and $a_i \in A_i$, $a_j \in A_j$, $v_{i,j}(a_i, a_j) = \vartheta_{i,j}(\varphi(\sigma))$, where $\sigma$ is any element of $\pi\Gamma$ such that $\sigma|_{A_i \cup A_j} = \text{map}_{a_i}^i \oplus \text{map}_{a_j}^j$.

It is thus only left to prove that, for two labellings $\sigma, \tau \in \pi\Gamma$, $\vartheta_{i,j}(\varphi(\sigma)) = \vartheta_{i,j}(\varphi(\tau))$ iff $\sigma$ and $\tau$ yield the same encoding of $E_{i,j}$. Equation (5) implies that

$$ \vartheta_{i,j}(\varphi(\sigma)) = \vartheta_{i,j}(\varphi(\tau)) \iff \vartheta_{i,j}(\psi(\sigma^{-1}\tau)) = 1 $$

so that it is only left to show that, $\psi(\gamma) \in \ker(\vartheta_{i,j}) \iff \gamma \in \text{Aut}(E_{i,j})$. And indeed:

$$ \begin{align*} \vartheta_{i,j}(\psi(\gamma)) = 1 &\iff \forall a \in A_i, b \in A_j, m_{i,j}(\psi(\gamma)_a \psi(\gamma)_b) = 1 \\ \text{by def. of } \psi, \iff \forall a \in A_i, b \in A_j, m_{i,j}(\gamma|_{A_i} \gamma|_{A_j}) = 1 \\ &\iff \gamma|_{A_i \cup A_j} \in \ker(m_{i,j}) \\ \text{by def. of } m_{i,j}, \iff \gamma|_{A_i \cup A_j} \in \text{Aut}(m_{i,j}) \end{align*} $$

To prove Theorem V.13, it remains to show that $\vartheta_{i,j}$ and $v_{i,j}$ are FPC-definable. Once again, we use a representation of $\text{Sym}(\Omega_{i,j})^{A \times A}$ as a permutation group. Recall that for each $i, j, \Omega_{i,j} \subseteq (A^<)^2$.

$$ \begin{align*} \iota_3 : \text{Sym}((A^<)^2)^{A \times A} \to \text{Sym}(A \times A \times ((A^<)^2)) \\ (\sigma_{(a,b)}_{(a,b)} \in A \times A) \mapsto ((a, b, (\mu, \nu)) \mapsto (a, b, \sigma_{(a,b)}(\mu, \nu))) \end{align*} $$

**Lemma C.3.** There is a FPC formula $\vartheta(\mu, \nu, x, y, \vec{s}, \vec{t})$ with type$(\vec{s}) = \text{type}(\vec{t}) = \text{element}^2\text{number}^2$ and type$(R) = \text{element}^2$ such that, for any $\sigma \in \varphi(\pi\Gamma)$ and $i \ne j \le m$,

$$ \vartheta(\mathfrak{A}, i, j, \text{graph}(\iota(\sigma))) = \text{graph}(\iota_3(\vartheta_{i,j}(\sigma))). $$

There is a FPC formula $\mathfrak{v}(\mu, \nu, x, y, \vec{s}, \vec{t})$ with type$(\vec{s}) = \text{type}(\vec{t}) = \text{element}^2\text{number}^2$ such that, for any $i \ne j \le m$,

$$ \mathfrak{v}(\mathfrak{A}, i, j, a, b) = \text{graph}(\iota_3(v_{i,j}(a, b))). $$

**Proof.** Let us first define $v_{i,j}$ as a formula $\mathfrak{v}(\mu, \nu, x, y, \vec{s}, \vec{t})$. The variables $\mu, \nu$ track the pair of color-classes we are currently handling and $x, y$ track the component of $v_{i,j}$ we are defining, i.e. we aim to obtain $\mathfrak{v}(\mathfrak{A}, i, j, a_i, a_j) = \text{graph}(v_{i,j}(a_i, a_j))$. Note that $v_{i,j}(a_i, a_j)$ is represented as acting on $A \times A \times \Omega_{i,j}$. Thus, the tuples of variables $\vec{s}$ and $\vec{t}$ are meant to represent individual elements of this set, and for readability purposes, we name those variables in accordance with our definition of $v_{i,j}$ above: $\vec{s} = (a_s, b_s, \mu_s, \nu_s)$ and
$\vec{t} = (a_t, b_t, \mu_t, \nu_t)$ ; with $(\mu_s, \nu_s)$ and $(\mu_t, \nu_t)$ representing elements of $\Omega_{i,j}$.

$$
\nu(\mu, \nu, x, y, \vec{s}, \vec{t}) := \bigcirc \left\{
\begin{array}{@{}l@{}}
  (x \notin A_{\mu} \lor y \notin A_{\nu}) \land \vec{s} = \vec{t} \\
  (a_s \notin A_{\mu} \lor b_s \notin A_{\nu}) \land \vec{s} = \vec{t} \\
  \quad \begin{array}{@{}l@{}}
    x \in A_{\mu} \land y \in A_{\nu} \\
    a_s \in A_{\mu} \land b_s \in A_{\nu}
  \end{array} \\
  \otimes \quad a_s = a_t \land b_s = b_t \\
  \quad \mathrm{slMorph}(\mu, \nu, R_g, \mu_s \nu_s, \mu_t \nu_t) \\
  \quad \qquad [R_g(\alpha, \beta)/\xi(\alpha, \beta)]
\end{array}
\right\}
$$

where

$$
\xi(\alpha, \beta) := \bigcirc \left\{
\begin{array}{@{}l@{}}
  \alpha \in A_{\mu} \\
  \beta \in A_{\mu} \\
  \quad \exists \lambda, \mathit{map}(\mu, x, \alpha, \lambda) \\
  \quad \mathit{map}(\mu, a_s, \beta, \lambda) \\
  \alpha \in A_{\nu} \\
  \beta \in A_{\nu} \\
  \quad \exists \lambda, \mathit{map}(\nu, y, \alpha, \lambda) \\
  \quad (\mathit{map}(\nu, b_s, \beta, \lambda))
\end{array}
\right\}
$$

Recall that map is the formula defining the local-labellings $\mathrm{map}_a^i$ as shown in Lemma V.5, that $\mathrm{slMorph}$ is the formula defining the morphisms $m_{i,j}$, as shown in Lemma B.5, and that $F[G/H]$ denotes substitution, as explained in the proof of Lemma III.6. Thus, for any suitable $\vec{a} = (i, j, a_i, a_j, a, b)$, an assignment of the free variables $(\mu, \nu, x, y, a_s, b_s)$ of $\xi, \xi(\mathfrak{A}, \vec{a})$ defines the graph of $(\mathrm{map}_a^i \mathrm{map}_b^j)^{-1} \mathrm{map}_{a_i}^i \mathrm{map}_{a_j}^j \in \Gamma_i \Gamma_j$. As such, the last clause in the definition of $\nu$ correctly defines the graph (on the variables $\mu_s \nu_s, \mu_t \nu_t$) of $m_{i,j}((\mathrm{map}_a^i \oplus \mathrm{map}_b^j)^{-1}(\mathrm{map}_{a_i}^i \oplus \mathrm{map}_{a_j}^j))$.

We now turn to the definition of the morphisms $\vartheta_{i,j}$. We provide a formula $\vartheta(\mu, \nu, R, \vec{s}, \vec{t})$, where once again, $(\mu, \nu)$ tracks the pair of color-classes at hand, and now, $R$ should be the graph of an element $g \in \iota(\mathcal{G})$.

As in the definition of $\nu$, $\vec{s}$ and $\vec{t}$ represent the domain $A \times A \times \Omega_{i,j}$ of the permutational image of the morphism $\vartheta_{i,j}$, and we name each individual variable $a_s, b_s, \mu_s, \nu_s$ (resp. $a_t, b_t, \mu_t, \nu_t$) to improve readability.

$$
\vartheta(\mu, \nu, R, \vec{s}, \vec{t}) := \bigcirc \left\{
\begin{array}{@{}l@{}}
  a_s = a_t \\
  b_s = b_t \\
  \quad \mathrm{slMorph}(\mu, \nu, R_g, \mu_s \nu_s, \mu_t \nu_t) \\
  \quad \qquad [R_g(x, y)/\theta(x, y)]
\end{array}
\right\}
$$

where

$$
\theta(x, y) := \exists w, R(a_s, x, a_s, w) \wedge R(b_s, w, b_s, y)
$$

One should be careful not to confuse $R_g$, which is the
second-order variable in $\mathrm{slMorph}$ that should take as value
the graph of a permutation in $\Gamma_i \Gamma_j$, and $R$, which is used
in $\vartheta$ as a place-holder for the graph of a permutation in $\mathcal{G}$,
so that $\vartheta(\mu, \nu, R, \vec{s}, \vec{t})$ defines a morphism as explained in
Definition III.5.
$\square$