# On the relative power of linear algebraic approximations of graph
isomorphism

Anuj Dawar  Danny Vagnozzi

###### Abstract

We compare the capabilities of two approaches to approximating graph
isomorphism using linear algebraic methods: the _invertible map tests_
(introduced by Dawar and Holm in [DH12]) and proof systems with algebraic
rules, namely _polynomial calculus_ , _monomial calculus_ and _Nullstellensatz
calculus_. In the case of fields of characteristic zero, these variants are
all essentially equivalent to the the Weisfeiler-Leman algorithms. In positive
characteristic we show that the invertible map method can simulate the
monomial calculus and identify a potential way to extend this to the monomial
calculus.

##  1 Introduction

The _graph isomorphism problem_ consists in deciding whether there is an edge-
preserving bijection between the vertex sets of two given graphs.
Computationally, this problem is polynomial-time equivalent to finding the
partition into orbits of the induced action of the automorphism group of a
given graph on a fixed power $k$ of its vertex set [Mat79] (we shall refer to
this partition as the $k$-_orbit partitions_ for a graph). The complexity of
these problems is notoriously unresolved: while there are reasons to believe
that they are not NP-complete, it is still an open problem as to whether they
are in P. The best known upper bound to their computational time is quasi-
polynomial, which follows from a breakthrough by Babai [Bab16].

There has been a surge of interest recently in linear-algebraic approaches to
the graph isomorphism problem. This is partly because the examples which give
hard instances to standard graph isomorphism algorithms code systems of linear
equations over finite fields and partly because linear-algebraic groups seem
to be the barrier to improving Babai’s algorithm. In this paper, we consider
two distinct methods for incorporating algorithms for solving linear systems
into graph isomorphism solvers and compare them. The first is based based on
the use of algebraic proofs systems, such as the polynomial calculus and the
second are generalizations of the Weisfeiler-Leman method, based on stability
conditions and coherent algebras. We next look at these two approaches more
closely.

Let $\Gamma$ and $\Gamma^{\prime}$ be graphs with vertex set $V$ and adjacency
matrices $A$ and $A^{\prime}$ respectively. Then, $\Gamma$ and
$\Gamma^{\prime}$ are isomorphic if, and only if, there is a $V\times V$
permutation matrix $X$ such that $AX=XA^{\prime}$. The latter matrix equation
can be viewed as a system of linear equations in the variables $x_{vw}$ which
are the entries of $X$ for $v,w\in V$. If we add the conditions that all rows
and columns of $X$ must sum to one, and all variables must be non-negative
integers, then such a linear program has an integer solution if, and only if,
$\Gamma$ and $\Gamma^{\prime}$ are isomorphic. The feasibility of a linear
program over the integers is, however, not known to be decidable in polynomial
time, so it is natural to investigate what happens when one searches for
rational solutions. It has been shown by Tinhofer [Tin86] that such a solution
exists if, and only if, $\Gamma$ and $\Gamma^{\prime}$ are not distinguished
by _naïve colour refinement_. The latter is a method consisting of iteratively
refining a partition of the set of vertices of a graph until reaching a stable
labelled partition, which can be seen as a _canonical colouring_ of said
graph, approximating the orbits of the action of its automorphism group.

For every $k\in\mathbb{N}$, the $k$-_Weisfeiler-Leman_ algorithm is a
generalization of the naïve colour refinement, giving an approximation of the
$k$-orbit partition. For a graph with vertex set $V$, each of these algorithms
outputs in time $|V|^{O(k)}$ a canonical labelled partition of $V^{k}$
satisfying a stability condition and respecting local isomorphism. Informally,
they can be seen as forming a family of algorithms, each defining a notion of
equivalence on both graphs and tuples of vertices of graphs. A result by Cai,
Fürer and Immerman [CFI92] shows how to construct graphs $\Gamma_{k}$ of size
$O(k)$ for which the $k$-Weisfeiler-Leman algorithm fails to produce the
$k$-orbit partition. In the same paper, it is shown that the equivalence
classes of the output partition of the $k$-Weisfeiler-Leman algorithm coincide
with the equivalence classes of $k$-tuples of vertices distinguished by
_counting logic_ formulae with at most $k+1$ variables. Thus, one deduces from
the tight connection made by Immerman and Lander (see Theorem 2.3 in [Daw15]),
that the equivalence notions defined by the Weisfeiler-Leman family of
algorithms delimit the expressive power of _fixed point logic with counting_
(FPC). Intuitively, one such limitation is the expressibility of solvability
of systems of linear equations over finite fields, since the above mentioned
constructions by Cai, Fürer and Immerman are essentially graph encodings of
systems of linear equations over $\mathbb{Z}_{2}$ [ABD09]. This has therefore
prompted research into families of algorithms graded by the natural numbers,
whose notion of equivalence on tuples of vertices of graphs is conceptually a
linear algebraic invariance over some field $\mathbb{F}$. One such family is
that of the _invertible map tests_ over $\mathbb{F}$, first defined in [DH12].
For any graph, the $k^{th}$ algorithm of this family also produces a canonical
labelled partition of $k$-tuples of its vertices, satisfying a stability
condition and respecting local isomorphism, thus giving another notion of
equivalence on both graphs and $k$-tuples of vertices thereof. Furthermore,
such equivalences delimit the expressive power of the extension of fixed-point
logic with quantifiers over linear algebraic operators as shown in [DGP19].

For a fixed characteristic, the output of the $k$-invertible map tests is
independent of the field; as such, $\mathbb{F}$ will hereafter be taken to be
a prime field without loss of generality. Informally, one can claim that the
family of equivalences on tuples defined by the Weisfeiler-Leman algorithms
and that defined by the invertible map tests over $\mathbb{Q}$ _simulate_ each
other in the following sense. For every $k\in\mathbb{N}$, there is some
$k^{\prime}\in\mathbb{N}$ such that for any graph, any pair of $k$-tuples of
its vertices distinguished by the $k$-Weisfeiler-Leman algorithm are
distinguished by the $k^{\prime}$-invertible map test over $\mathbb{Q}$.
Conversely, for every $k\in\mathbb{N}$ there is a $k^{\prime}\in\mathbb{N}$
such that for any graph, any pair of $k$-tuples of vertices distinguished by
the $k$-invertible map test over $\mathbb{Q}$ is distinguished by the
$k^{\prime}$-Weisfeiler-Leman algorithm. If the characteristic of $\mathbb{F}$
is positive the former statement holds, but not the latter; indeed, it is
shown in [Hol10] and [DGP19] how one can construct graphs $\Gamma_{k,p}$ for
each $k\in\mathbb{N}$ and prime number $p$, for which the $3$-invertible map
test over $\mathbb{Z}_{p}$ outputs the $3$-orbit partition, but the output of
the $k$-invertible map test over $\mathbb{Z}_{q}$ with $q\neq p$ is strictly
coarser than the $k$-orbit partition.

The second approach to approximating the orbit partition, relying on linear
algebraic operations that we consider is that of algebraic proof systems
[BIK+94, CEI00]. These systems are the subject of very active study in the
area of proof complexity. They have been studied specifically in the context
of graph isomorphism in [BG15] and [GGPP19]. In particular, the proof systems
studied are the _polynomial calculus_ (PC), and the weaker _Nullstellensatz
calculus_ (NC) and _monomial calculus_ (MC). Each of these gives, for a fixed
field $\mathbb{F}$ a set of rules $\mathcal{R}$ dictating how new polynomials,
with coefficients in $\mathbb{F}$, may be derived from an initial set of
polynomials, which we shall refer to as _axioms_. For a graph $\Gamma$ on $V$,
we say that the corresponding calculus distinguishes $\vec{u},\vec{v}\in
V^{k}$ if there is a $\mathcal{R}$-derivation of
$x_{u_{1}v_{1}}x_{u_{2}v_{2}}\ldots x_{u_{k}v_{k}}$ from
$\mathrm{Ax}(\Gamma)\subset\mathbb{F}[\\{x_{uv}|u,v\in V\\}]$, a set of axioms
encoding the atomic types of the input graph $\Gamma$. Say that a derivation
has _degree_ $d$ if all polynomials occurring in the derivation have degree at
most $d$. For each of the calculi, fixing the degree $d$ gives us a
polynomial-time algorithm for checking the existence of a derivation and hence
a polynomial-time approximation of the orbit partition on graphs. Again, we
may restrict $\mathbb{F}$ to a prime field without loss of generality—this
will become clear once we define properly the set $\mathrm{Ax}(\Gamma)$ and
the derivation rules in Section 3.4.

The question we address in this paper is how the approximations of the orbit
partition obtained by these algebraic proof systems for a given field
$\mathbb{F}$ compare with those we get from the invertible map test. In the
case of fields of characteristic zero, the answer is quite clear, as both
approaches yield algorithms that are (up to constant factors) equivalent to
the Weisfeiler-Leman algorithms. This is shown for the invertible maps in
[DV20] and for the polynomial calculus in [GGPP19], giving the following
statement.

######  Theorem 1.1.

For any $k\in\mathbb{N}$ and $\vec{u},\vec{v}\in V^{k}$, there is a
$k^{\prime}\in\mathbb{N}$ such that if $x_{u_{1}v_{1}}\ldots x_{u_{k}v_{k}}$
has a degree $k$ PC derivation over $\mathbb{Q}$ from $\mathrm{Ax}(\Gamma)$,
then $\vec{u}$ and $\vec{v}$ are distinguished by the $k^{\prime}$-invertible
map test over $\mathbb{Q}$. Conversely, for any $k\in\mathbb{N}$ and
$\vec{u},\vec{v}\in V^{k}$, there is a $k^{\prime}\in\mathbb{N}$ such that if
$\vec{u}$ and $\vec{v}$ are distinguished by the $k$-invertible map test over
$\mathbb{Q}$, then $x_{u_{1}v_{1}}\ldots x_{u_{k}v_{k}}$ has a degree
$k^{\prime}$ PC derivation over $\mathbb{Q}$ from $\mathrm{Ax}(\Gamma)$.

In the case of positive characteristic, we show (in Section 4) the
definability of derivations of MC in FPS$(p)$, an extension of fixed-point
logic with quantifiers for the solvability of systems of linear equations over
fields of characteristic $p$. This implies, in particular, that the
approximation of the orbit partition obtained by MC in characteristic $p$ is
no finer than that obtained by the invertible map test in characteristic $p$.

######  Theorem 1.2.

For any prime number $p$, $k\in\mathbb{N}$ and $\vec{u},\vec{v}\in V^{k}$,
there is a $k^{\prime}\in\mathbb{N}$ such that if $x_{u_{1}v_{1}}\ldots
x_{u_{k}v_{k}}$ has a degree $k$ MC derivation over $\mathbb{Z}_{p}$ from
$\mathrm{Ax}(\Gamma)$, then $\vec{u}$ and $\vec{v}$ are distinguished by the
$k^{\prime}$-invertible map test over $\mathbb{Z}_{p}$.

In the other direction, we are able to show that the distinguishing power of
FPS$(p)$ can be simulated by NC. Thus, this apparently weaker proof system is
able to simulate (as far as the graph isomorphism problem is concerned) PC in
characteristic zero and at least MC in positive characteristic.

######  Theorem 1.3.

  1. 1.

For any $k\in\mathbb{N}$ and $\vec{u},\vec{v}\in V^{k}$, there is a
$k^{\prime}\in\mathbb{N}$ such that if $x_{u_{1}v_{1}}\ldots x_{u_{k}v_{k}}$
has a degree $k$ PC derivation of over $\mathbb{Q}$ from
$\mathrm{Ax}(\Gamma)$, then there is also a degree $k^{\prime}$ NC derivation
over $\mathbb{Q}$ from $\mathrm{Ax}(\Gamma)$.

  2. 2.

For any prime number $p$, $k\in\mathbb{N}$ and $\vec{u},\vec{v}\in V^{k}$,
there is a $k^{\prime}\in\mathbb{N}$ such that if $x_{u_{1}v_{1}}\ldots
x_{u_{k}v_{k}}$ has a degree $k$ MC derivation over $\mathbb{Z}_{p}$ from
$\mathrm{Ax}^{(k)}(\Gamma)$, then it also has a degree $k^{\prime}$ NC
derivation over $\mathbb{Z}_{p}$ from $\mathrm{Ax}(\Gamma)$.

From this, a strengthening of Theorem 6.3 in [BG15] also follows. Let $V$ be
the vertex set of $\Gamma_{k,p}$ as above.

######  Theorem 1.4.

If $\vec{u},\vec{v}\in V^{3}$ are not in the same equivalence class of the
$3$-orbit partition of $\Gamma_{k,p}$, then
$x_{u_{1}v_{1}}x_{u_{2}v_{2}}x_{u_{3}v_{3}}$ has a degree $3$ NC derivation
over $\mathbb{Z}_{p}$ from $\mathrm{Ax}(\Gamma_{k,p})$.

#### Structure of the paper.

We first give an overview of the relevant background (Sections 2 and 3).
Section 4 is mostly concerned with the definability of monomial calculus
refutations over $\mathbb{Z}_{p}$ in FPS$(p)$ and contains the proof of
Theorem 1.2. Theorems 1.3 and 1.4 are proven in Section 5. We conclude by
discussing related open problems and ways to approach them.

##  2 Preliminaries

In this section, after introducing some notational conventions, we recall some
notions on partitions introduced in Sections 3 and 4 of [DV20] and briefly
describe the logics of interest.

#### Notational conventions.

All sets are finite unless stated otherwise. Given two sets $V$ and $I$, a
tuple in $V^{I}$ is denoted by $\vec{v}$, and its $i^{th}$ entry by $v_{i}$,
for each $i\in I$. We use the notation $(v_{i})$ for $i\in I$ to denote the
element of $V^{I}$ with $i^{th}$ element equal to $v_{i}$. For a field
$\mathbb{F}$, the element of $\mathbb{F}^{V}$ with all its entries equal to
$1$ is denoted by $\mathbf{1}_{V}$. We set
$[k]=\\{1,2,\ldots,k\\}\subset\mathbb{N}$ and define
$[k]^{(r)}=\\{\vec{x}\in[k]^{r}\mid x_{i}\neq x_{j}\;\forall i,j\in[r],\;i\neq
j\\}$ for $r\leq k$.

For any $\vec{v}\in V^{k}$, $\vec{u}\in V^{r}$, and $\vec{i}\in[k]^{(r)}$ we
define $\vec{v}\langle\vec{i},\vec{u}\rangle\in V^{k}$ to be the tuple with
entries

$(\vec{v}\langle\vec{i},\vec{u}\rangle)_{j}=\begin{cases}u_{i_{s}}\;\,\text{if
$j=i_{s}$ for some $s\in[r]$}\\\ v_{j}\;\,\text{otherwise.}\\\ \end{cases}$

In other words, $\vec{v}\langle\vec{i},\vec{u}\rangle$ is the tuple obtained
from $\vec{v}$ by substituting the elements of $\vec{u}$ in the positions
specified by $\vec{i}$.

Given two tuples $\vec{v}\in V^{r}$ and $\vec{w}\in V^{s}$, their
_concatenation_ is denoted by $\vec{v}\cdot\vec{w}\in V^{r+s}$. More
precisely, $\vec{v}\cdot\vec{w}$ is the tuple with entries

$(\vec{v}\cdot\vec{w})_{i}=\begin{cases}v_{i}\;\,&\textrm{if $i\in[r]$}\\\
w_{j}\;\,&\textrm{if $i=j+r$}.\end{cases}$

For a relation $R\subseteq V^{2}$ we define the _adjacency matrix_ of $R$ to
be the $V\times V$ matrix whose $(u,v)$ entry is $1$ if $(u,v)\in R$ and $0$
otherwise.

###  2.1 Labelled partitions and refinement operators

A _labelled partition_ of a set $A$ is a map $\gamma:A\rightarrow X$, where
the elements of $X$ are sometimes referred to as _colours_ , and $\gamma(a)$
as the colour of $a$ in $\gamma$. Denote the class of labelled partitions of
$A$ by $\mathcal{P}(A)$. For equivalence relations $\mathfrak{R}$ and
$\mathfrak{S}$ on $A$ we write $\mathfrak{R}\preceq_{A}\mathfrak{S}$ and say
that $\mathfrak{S}$ _refines_ $\mathfrak{R}$ if, whenever $a,b\in A$ are in
the same equivalence class of $\mathfrak{S}$, they are also in the same
equivalence class of $\mathfrak{R}$. We extend the partial order $\preceq_{A}$
to labelled paritions by writing $\gamma\preceq_{A}\rho$ to mean that the
equivalence relation $\\{(a,b)\mid\ \rho(a)=\rho(b)\\}$ refines the relation
$\\{(a,b)\mid\gamma(a)=\gamma(b)\\}$. Note that this does not require that the
co-domains of $\gamma$ and $\rho$ are the same or indeed related in any way.
We omit the subscript $A$ where the set is clear from the context.

Define an action of $\mathrm{Sym}(k)$ on $V^{k}$ by setting $\vec{v}^{\pi}$ to
be the element of $V^{k}$ with $i^{th}$ entry $v_{\pi^{-1}(i)}$.
$\gamma\in\mathcal{P}(V^{k})$ is said to be _invariant_ if
$\gamma(\vec{u})=\gamma(\vec{v})$ implies
$\gamma(\vec{u}^{\pi})=\gamma(\vec{v}^{\pi})$ for all $\pi\in\mathrm{Sym}(k)$
and $\vec{u},\vec{v}\in V^{k}$. For $t\in[k]$, the $t$-_projection_ of
$\gamma$ is defined to be the labelled partition
$\mathrm{pr}_{t}\gamma\in\mathcal{P}(V^{t})$ such that for all $\vec{u}\in
V^{t}$

$\mathrm{pr}_{t}\gamma(\vec{u})=\gamma(u_{1},u_{2},\ldots,u_{t},\ldots,u_{t}).$

For $\vec{v}\in V^{k}$, with $t,k$ as above, we similarly define
$\mathrm{pr}_{t}\vec{v}$ to be the $t$-tuple $(v_{1},v_{2},\ldots,v_{t})$.

For a labelled partition $\gamma\in\mathcal{P}(V^{k})$ and $t\in[k]$, we say
that $\vec{u},\vec{v}\in V^{t}$ are _distinguished_ by $\gamma$ if
$\mathrm{pr}_{t}\gamma(\vec{u})\neq\mathrm{pr}_{t}\gamma(\vec{v})$.

######  Definition 2.1 (Graph-like partition111The definition of a graph-like
partition in [DV20] has an additional assumption (that of $k$-_consistency_).
One can show, however, that the results in said paper still hold true without
the $k$-consistency assumption.).

$\gamma$ is said to be _graph-like_ if it is invariant and for all $i,j\in[k]$

$\gamma(\vec{u})=\gamma(\vec{v})\implies(u_{i}=u_{j}\implies v_{i}=v_{j}).$

In other words, a partition of $V^{k}$ is graph-like if it refines the
partition into equality types.

For $\vec{i}\in[k]^{(2r)}$ and $\vec{v}\in V^{k}$, define the
$(\vec{i},\vec{v})$-_character vector_ of $\gamma\in\mathcal{P}(V^{k})$ to be
the tuple $\vec{\chi}=(\chi_{\sigma})_{\sigma\in\mathrm{Im}(\gamma)}$ where
$\chi_{\sigma}$ is the adjacency matrix of the relation
$\\{(\vec{x},\vec{y})\in(V^{r})^{2}\mid\gamma(\vec{v}\langle\vec{i},\vec{x}\cdot\vec{y}\rangle)=\sigma\\}$.

######  Definition 2.2 (Refinement operator).

A $k$-_refinement operator_ is a map $R$ which, for any set $V$, assigns to
each $\gamma\in\mathcal{P}(V^{k})$ a partition
$R\circ\gamma\in\mathcal{P}(V^{k})$ that satisfies the following properties:

  * (R1).

Refinement: $\gamma\preceq R\circ\gamma$.

  * (R2).

Monotonicity: $\gamma\preceq\rho\implies R\circ\gamma\preceq R\circ\rho$.

We say that a partition $\gamma\in\mathcal{P}(V^{k})$ is _$R$ -stable_ if
$R\circ\gamma=\gamma$. Given an $X\in\mathcal{P}(V^{k})$, define a sequence of
labelled partitions by $X^{0}=X$ and $X^{i+1}=R\circ X^{i}$. Then, there is
some $s$ such that for all $i$, $i\geq s$ implies that $X^{i}$ is $R$-stable.
For the minimal such $s$ we denote $X^{s}$ by $[X]^{R}$. By the monotonocity
property of $R$, it follows that up to re-labelling of its equivalence
classes, $[X]^{R}$ is the unique minimal $R$-stable partition refining $X$.

A $k$-refinement operator $R$ is said to be _graph-like_ if $R\circ\gamma$ is
graph-like for any graph-like $\gamma$.

###  2.2 Extensions of first order and inflationary fixed point logics

We assume the reader has some familiarity with first-order and fixed-point
logics, whose details can be found, for instance in [EF99]. Throughout the
paper, for a logic $\mathcal{L}$, we denote by $\mathcal{L}_{k}$ the class of
all $\mathcal{L}$-formulae (over some pre-specified vocabulary) with at most
$k$ variables. Let $\mathfrak{A}$ be a structure with universe $V$ and fix
$\vec{u},\vec{v}\in V^{k}$. We say that some $\mathcal{L}_{k}$ formula
$\phi(\vec{z})$ _distinguishes_ $(\mathfrak{A},\vec{z}\mapsto\vec{u})$ from
$(\mathfrak{A},\vec{z}\mapsto\vec{v})$ if either
$\mathfrak{A}\models\phi(\vec{u})$ and $\mathfrak{A}\not\models\phi(\vec{v})$
or $\mathfrak{A}\not\models\phi(\vec{u})$ and
$\mathfrak{A}\models\phi(\vec{v})$ .

#### A language for graphs.

We may view any graph as an _edge-coloured complete digraph_ and hence, as a
labelled partition of the set of ordered pairs of its vertices. For example, a
loop-free uncoloured graph on $V$ is a partition of $V^{2}$ whose colour set
is $\\{\texttt{vertex, edge, non-edge}\\}$. From a logical view-point, we may
thus define a graph $\Gamma$ on $V$ to be a finite relational structure
$\mathfrak{A}_{\Gamma}$ with universe $V$, over a vocabulary consisting of
binary relation symbols.

#### Counting logic.

_Counting logic_ $\mathcal{C}$ is the extension of first-order logic with
_counting quantifiers_ $\exists^{m}$, for each positive integer $m$. A
structure satisfies the formula $\exists^{m}x.\phi(x)$ if, and only if, there
are at least $m$ elements in the universe for which the formula $\phi(x)$ is
satisfied. Note that $\exists^{m}x.\phi(x)$ can be written as an equivalent
first-order formula by using $m$ quantifiers $\exists$ and $m$ auxiliary
variables. This, however, inconveniently increases the number of variables
required.

#### Solvability quantifiers.

For a logic $\mathcal{L}$ we denote its extension via _solvability
quantifiers_ $\mathrm{slv}_{p}$ over a finite field of characteristic $p$ by
$\mathcal{L}+$S$(p)$. Let $\phi(\vec{x},\vec{y},\vec{z})$ be a formula of such
a logic, where $\vec{x},\vec{y},\vec{z}$ are $i,j,k$-tuples of variables
respectively. Then
$\mathrm{slv}_{p}(\vec{x}\vec{y}.\phi(\vec{x},\vec{y},\vec{z}))$ is also a
$\mathcal{L}+$S$(p)$ formula. See [DGH+12, GGPP19] for more about these
quantifiers.

The semantics of this quantifier is as follows. To each structure with
universe $V$ and $k$-tuple $\vec{v}\in V^{k}$, we associate the $V^{i}\times
V^{j}$ matrix $S_{\phi}^{\vec{v}}$ over $\\{0,1\\}\subseteq\mathbb{Z}_{p}$
with $(\vec{r},\vec{s})$-entry equal to $1$ if, and only if,
$\mathfrak{A}\models\phi(\vec{r},\vec{s},\vec{v})$. Then,
$(\mathfrak{A},\vec{z}\mapsto\vec{v})\models\mathrm{slv}_{p}(\vec{x}\vec{y}.\phi(\vec{x},\vec{y},\vec{z}))$
if, and only if, there is some $\vec{a}\in\mathbb{Z}_{p}^{V^{i}}$ such that
$S^{\vec{v}}_{\phi}\vec{a}=\mathbf{1}$.

Note that the fact that the linear equations encoded by the solvability
quantifier may seem to have a restricted form does not entail any loss of
generality, as is explained in Section 4.1. Furthermore, we may take $i=j$ in
the above (and hence, assume that $S_{\phi}^{\vec{v}}$ is a square matrix), by
simply adding auxiliary rows or columns. For a more detailed explanation see
Section 3.2 of [DGP19], which deals with quantifiers over linear algebraic
operators, of which the solvability quantifier is a special case.

When $\mathcal{L}$ is fixed-point logic or first order logic, we denote
$\mathcal{L}+$S$(p)$ by FPS$(p)$ or FOS$(p)$ respectively, and FOS${}_{k}(p)$
denotes the corresponding logic with formulae with at most $k$ variables.

#### Embedding fixed-points in finite variable logics.

Fixed point logics provide a compact framework for describing sets which are
defined recursively. For the purpose of establishing limits on their
expressive power, it is easier to study them in terms of finite variable
logics. which provide bounds for their expressive power. For example, it is
well known that if $\phi$ is a first-order formula in $m$ variables, then
$\mathrm{ifp}_{R,\vec{x}}\phi$ is equivalent, on structures with at most $n$
elements (for arbitrary $n$) to a first-order formula with $2m$ variables; see
Section 11.1 in [Lib04] for a detailed argument. It follows that
$\mathrm{ifp}_{R,\vec{x}}\phi$ cannot distinguish between two structures which
are indistinguishable by any first-order formula with at most $2m$ variables.
It is easy to see that a similar argument yields an analogous result for
FPS$(p)$. That is if $\phi$ is an FPS$(p)$ formula with at most $m$ variables,
it cannot distinguish any pair of structures which agree on all FOS$(p)$
formulas with at most $2m$ variables.

#### Logical interpretations.

A logical interpretation $\mathcal{I}$ maps a structure $\mathfrak{A}$ to a
structure $\mathcal{I}(\mathfrak{A})$ according to a rule dictated by a tuple
of formulae from a certain logic $\mathcal{L}$. They can be seen as the
logical counterpart of an algorithmic reduction. Formally, let $\mathtt{S}$
and $\mathtt{S}^{\prime}$ be relational vocabularies, and let
$\mathtt{T}_{1}\ldots\mathtt{T}_{l}$ be the symbols of $\mathtt{S}^{\prime}$,
with $t_{i}$ indicating the arity of $\mathtt{T}_{i}$. An
$\mathcal{L}[\mathtt{S},\mathtt{S}^{\prime}]$-_interpretation_ is a tuple

$\mathcal{I}(\vec{z})=(\phi_{\delta}(\vec{x},\vec{z}),\phi_{\equiv}(\vec{x},\vec{y},\vec{z}),\phi_{\mathtt{T}_{1}}(\vec{x}_{1},\ldots,\vec{x}_{t_{1}},\vec{z}),\ldots,\phi_{\mathtt{T}_{l}}(\vec{x}_{1},\ldots,\vec{x}_{t_{l}},\vec{z}))$

where
$\phi_{\delta},\phi_{\equiv},\phi_{\mathtt{T}_{1}},\ldots,\phi_{\mathtt{T}_{l}}$
are $\mathcal{L}$-formulae over $\mathtt{S}$,
$\vec{x},\vec{y},\vec{x}_{1},\ldots,\vec{x}_{t_{l}}$ are tuples of pairwise
distinct variables of length $d$ and $\vec{z}$ is a tuple of variables
pairwise distinct from the previous ones. We refer to $d$ and $\vec{z}$ as the
_arity_ and the _parameters_ of the interpretation respectively, and to
$\phi_{\equiv}$ as the _equivalence formula_.

With $\mathcal{I}(\vec{z})$ a $d$-ary interpretation as above, let
$\mathfrak{A}$ be a $\mathtt{S}$-structure with universe $V$, and $\vec{a}$ a
tuple of elements of $V$ with same length as $\vec{z}$. Define a
$\mathtt{S}^{\prime}$-structure $\mathfrak{B}$ with universe $\\{\vec{b}\in
V^{d}\mid\mathfrak{A}\models\phi_{\delta}(\vec{b},\vec{z})\\}$, and set
$\mathfrak{B}\models\mathtt{T}_{i}(\vec{b}_{1},\ldots,\vec{b}_{t_{i}})$ if,
and only if,
$\mathfrak{A}\models\phi_{\mathtt{T}_{i}}(\vec{b}_{1},\ldots,\vec{b}_{t_{i}},\vec{a})$.
Moreover, let $\mathcal{E}=\\{(\vec{b}_{1},\vec{b}_{2})\in V^{d}\times
V^{d}\mid\mathfrak{A}\models\phi_{\equiv}(\vec{b}_{1},\vec{b}_{2},\vec{a})\\}$.
We then define

$\mathcal{I}(\mathfrak{A},\vec{z}\mapsto\vec{a})=\begin{cases}\mathfrak{B}/\mathcal{E}\;\;\textrm{
if $\mathcal{E}$ is a congruence relation on $\mathfrak{B}$}\\\
\textrm{undefined otherwise}.\end{cases}$

Hence, intrepretations can be seen to induce maps from $\mathtt{S}$-structures
to $\mathtt{S}^{\prime}$-structures. Their crucial property is that, in terms
of $\mathcal{L}$-formulae, they can be reversed to give a map from
$\mathcal{L}$-formulae over $\mathtt{S}^{\prime}$ to $\mathcal{L}$-formulae
over $\mathtt{S}$ as the next result illustrates. A proof can be found in most
standard textbooks (see, for example [EFT94]) with $\mathcal{L}$ being first
order logic. Using induction on the structure of $\psi$, it is easy to adapt
the proof to $\mathcal{L}$ being fixed point logics and/or its extension with
solvability quantifiers.

######  Lemma 2.3 (Interpretation Lemma).

Let $\mathcal{I}(\vec{z})$ be a $d$-ary
$\mathcal{L}[\mathtt{S},\mathtt{S}^{\prime}]$ interpretation. Then, for every
$\mathcal{L}$-formula $\psi(x_{1},\ldots x_{m})$ over $\mathtt{S}^{\prime}$,
there is a $\mathcal{L}$-formula
$\psi^{-\mathcal{I}}(\vec{y}_{1},\ldots,\vec{y}_{m},\vec{z})$ over
$\mathtt{S}$ (where $\vec{y}_{i}$ are $d$-tuples of pairwise distinct
variables) such that for all $(\mathfrak{A},\vec{z}\mapsto\vec{a})$ with
$\mathcal{I}(\mathfrak{A},\vec{z}\mapsto\vec{a})$ well defined, and for all
$d$-tuples $\vec{q}_{1},\ldots,\vec{q}_{m}$ of elements from the universe of
$\mathfrak{A}$ such that $\vec{q}_{1}/_{\equiv},\ldots,\vec{q}_{m}/_{\equiv}$
are elements of the universe of
$\mathcal{I}(\mathfrak{A},\vec{z}\mapsto\vec{a})$

$\mathfrak{A}\models\psi^{-\mathcal{I}}(\vec{q}_{1},\ldots,\vec{q}_{m},\vec{a})\iff\mathcal{I}(\mathfrak{A},\vec{z}\mapsto\vec{a})\models\psi(\vec{q}_{1}/_{\equiv},\ldots,\vec{q}_{m}/_{\equiv}).$

##  3 Refinement operators and proof systems with algebraic rules

In this section we give an overview of the refinement operators of interest
and briefly describe the proof systems mentioned in the introduction. In
particular, we recall the invertible map and counting logics operators and
introduce the solvability operators.

###  3.1 The invertible map tests

The equivalence relations on tuples of vertices induced by the invertible map
tests have been originally introduced in [DH12], under the guise of a pebble
game with algebraic rules on a pair of graphs. In [DGP19], it was shown that
these equivalences correspond to indistinguishability in an extension of first
order logic with linear algebraic operators (Theorem 2). Algorithmically, one
can find these equivalence classes by computing a fixed point of the
_invertible map operators_ $\mathrm{IM}_{k,r}^{\mathbb{F}}$, as defined in
Sections 8 of [DV20]. Each of these is a $k$-refinement operator such that for
$\gamma\in\mathcal{P}(V^{k})$, the colour of $\vec{v}\in V^{k}$ in the
partition $\mathrm{IM}_{k,r}^{\mathbb{F}}\circ\gamma$ is given by a tuple
whose entries are $\gamma(\vec{v})$ and the equivalence classes under matrix
conjugation of the $(\vec{i},\vec{v})$-character vectors of $\gamma$, for all
$\vec{i}\in[k]^{(2r)}$. We shall not need the definitions of these operators,
as their _stability conditions_ are simpler to state and more useful for our
purpose. That is, $\gamma$ is $\mathrm{IM}_{k,r}^{\mathbb{F}}$-stable if for
all $\vec{u},\vec{v}\in V^{k}$ and $\vec{i}\in[k]^{(2r)}$

$\gamma(\vec{u})=\gamma(\vec{v})\implies\exists
M\in\mathrm{GL}_{V^{r}}(\mathbb{F}),M\chi_{\sigma}M^{-1}=\xi_{\sigma}\,\,\forall\sigma\in\mathrm{Im}(\gamma)$

where $(\chi_{\sigma})_{\sigma\in\mathrm{Im}(\gamma)}$ and
$(\xi_{\sigma})_{\sigma\in\mathrm{Im}(\gamma)}$ are the $(\vec{i},\vec{v})$
and $(\vec{i},\vec{u})$-character vectors of $\gamma$ respectively.

For a graph $\Gamma$ on $V$, let $\alpha_{k,\Gamma}$ be a canonical labelled
partition of $V^{k}$ into atomic types of $\Gamma$.222By _canonical_ we mean
_invariant under isomorphism_. That is, if $\Gamma$ and $\Gamma^{\prime}$ are
graphs on $V$ and $V^{\prime}$ respectively and $\vec{u}\in V^{k}$ and
$\vec{v}\in(V^{\prime})^{k}$, then
$\alpha_{k,\Gamma}(\vec{u})=\alpha_{k,\Gamma^{\prime}}(\vec{v})$ if, and only
if, the mapping $u_{i}\rightarrow v_{i}$ is an isomorphism of the subgraphs
induced by the vertices in $\vec{u}$ and $\vec{v}$. Define the $k$-refinement
operator $\mathrm{IM}_{k}^{\mathbb{F}}$ so that for
$\gamma\in\mathcal{P}(V^{k})$, the colour of $\vec{v}\in V^{k}$ in
$\mathrm{IM}_{k}^{\mathbb{F}}\circ\gamma$ is given by a tuple whose entries
are the colours of $\vec{v}$ in $\mathrm{IM}_{k,r}^{\mathbb{F}}\circ\gamma$,
for all $r<k/2$. Formally,

$\mathrm{IM}_{k}^{\mathbb{F}}\circ\gamma(\vec{v})=(\mathrm{IM}_{k,1}^{\mathbb{F}}\circ\gamma(\vec{v}),\mathrm{IM}_{k,2}^{\mathbb{F}}\circ\gamma(\vec{v}),\ldots,\mathrm{IM}_{k,\lfloor
k/2\rfloor}^{\mathbb{F}}\circ\gamma(\vec{v})).$

Then, the output of the $k$-invertible map test over $\mathbb{F}$ is the
labelled partition $[\alpha_{k,\Gamma}]^{\mathrm{IM}_{k}^{\mathbb{F}}}$. It is
explained in Proposition $4.6$ in [DV20] how one can obtain this partition in
time $|V|^{O(k)}$ by iteratively applying $\mathrm{IM}_{k}^{\mathbb{F}}$ to
$\alpha_{k,\Gamma}$. For $\vec{u},\vec{v}\in V^{l}$ and $l\leq k$, we say that
the $k$-invertible map over $\mathbb{F}$ _distinguishes_ $\vec{u}$ and
$\vec{v}$ if they are in different equivalence classes of the partition
$\mathrm{pr}_{l}[\alpha_{k,\Gamma}]^{\mathrm{IM}_{k}^{\mathbb{F}}}$.

Finally, we note that for a fixed characteristic, the choice of $\mathbb{F}$
is irrelevant: indeed the matrices
$A_{1},\ldots,A_{m}\in\mathrm{Mat}_{V}(\mathbb{F})$ and
$B_{1},\ldots,B_{m}\in\mathrm{Mat}_{V}(\mathbb{F})$ are simultaneously similar
over $\mathbb{F}$ if, and only if, they are simultaneously similar over any
extension of $\mathbb{F}$ [dSP09]. Since the entries of the character vectors
are $01$-matrices, we may assume, without loss of generality, that
$\mathbb{F}$ is a prime field. Hereafter, we shall then indicate the operators
$\mathrm{IM}_{k,r}^{\mathbb{F}}$ and $\mathrm{IM}_{k}^{\mathbb{F}}$ by
$\mathrm{IM}_{k,r}^{c}$ and $\mathrm{IM}_{k}^{c}$ respectively, where $c$ is
the characteristic of $\mathbb{F}$.

###  3.2 Counting logics operators

It is useful to express the partition of $k$-tuples into equivalence classes
under finite variable counting logics as the fixed point of a refinement
operator. For this purpose, the $k$-refinement operators $\mathrm{C}_{k,r}$,
for $r<k$, have been defined so that for any $\gamma\in\mathcal{P}(V^{k})$,
the colour of $\vec{v}\in V^{k}$ in $\mathrm{C}_{k,r}\circ\gamma$ is given by
a tuple whose entries are $\gamma(\vec{v})$ and the multisets of colours in
$\gamma$ of the tuples which can be obtained by substituting an $r$-tuple into
$\vec{v}$ (see Section 4 of [DV20]). In particular, $\gamma$ is
$\mathrm{C}_{k,r}$-stable if, and only if, for all $\vec{i}\in[k]^{(r)}$ and
$\sigma\in\mathrm{Im}(\gamma)$, the size of the set $\\{\vec{x}\in
V^{r}\mid\gamma(\vec{v}\langle\vec{i},\vec{x}\rangle)=\sigma\\}$ is
independent of the choice of $\vec{v}$ from within its equivalence class in
$\gamma$. As such, for a graph $\Gamma$ on $V$, $\vec{u},\vec{v}\in V^{k}$ are
in the same equivalence class of $[\alpha_{k,\Gamma}]^{\mathrm{C}_{k,1}}$ if,
and only if, there are no $\mathcal{C}_{k}$ formulae distinguishing
$(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{u})$ from
$(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{v})$. The combinatorial properties
of $\mathrm{C}_{k,r}$-stable partitions can be used to show the relation
between the distinguishing powers of finite variable fragments of counting
logics and the invertible map tests. In short, the invertible map test over
fields of characteristic zero is not more distinguishing than counting logic,
but over fields of positive characteristic it is. To be precise, with
$\Gamma,\vec{u},\vec{v}$ as above, the following holds:

> For any field $\mathbb{F}$, if the $k$-invertible map test over $\mathbb{F}$
> does not distinguish $\vec{u}$ and $\vec{v}$ in $\Gamma$, then there are no
> $\mathcal{C}_{k-1}$-formulae distinguishing
> $(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{u})$ from
> $(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{v})$. If the $k$-invertible map
> test over $\mathbb{Q}$ distinguishes $\vec{u}$ from $\vec{v}$ in $\Gamma$,
> then there is some $\mathcal{C}_{2k-1}$-formula distinguishing
> $(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{u})$ from
> $(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{v})$. 333This is a direct
> consequence of the following generalizations of Lemmata 7.1 and 7.3 in
> [DV20] respectively: for all $k,r\in\mathbb{N}$ with $2r<k$,  1. The
> $k$-projection of a graph-like $\mathrm{IM}_{k+r,r}^{c}$-stable partition is
> $\mathrm{C}_{k,r}$-stable for any characteristic $c$. 2. The $k$-projection
> of a graph-like $\mathrm{C}_{k+r,r}$-stable partition is
> $\mathrm{IM}_{k,r}^{0}$-stable. The authors prove it only for the case
> $r=1$, but a similar argument holds for any $r\in\mathbb{N}$.

###  3.3 Solvability operators

Central to this paper are finite variable fragments of the extension of first
order logic with solvability quantifiers over a fixed field. In order to
construct a refinement operator whose stable points reflect the properties of
this logic, we consider a weakened version of the invertible map operators,
whose action on labelled partitions can be computed solely by solving systems
of linear equations. To achieve this, we proceed by defining an equivalence
relation $\sim_{\mathrm{sol}}$ on the character vectors, which can be seen as
a relaxation of the conjugation relation $\sim$.

Let
$\mathfrak{P}_{V}(\mathbb{F})=\\{A\in\mathrm{Mat}_{V}(\mathbb{F})\mid\sum_{w\in
V}A_{wv}=\sum_{w\in V}A_{uw}=1,\forall u,v\in V\\}$. Or, equivalently,
$\mathfrak{P}_{V}(\mathbb{F})$ is the set of matrices
$A\in\mathrm{Mat}_{V}(\mathbb{F})$ such that $\mathbf{1}_{V}$ is an
eigenvector of both $A$ and $A^{t}$, with corresponding eigenvalue $1$. For a
set $I$, let

$\mathcal{X}_{V}^{I}(\mathbb{F})=\\{\vec{A}\in\mathrm{Mat}_{V}(\mathbb{F})^{I}\mid\sum_{s\in
I}A_{s}=\mathbb{J}_{V}\;\mathrm{and}\;\forall i\in I,\exists
j,A_{i}^{t}=A_{j}\\}.$

Note that if $\gamma$ is invariant and $\vec{i}\in[k]^{(2r)}$, then any
$(\vec{i},\vec{v})$\- character $\vec{\chi}$ of $\gamma$ is an element of
$\mathcal{X}_{V}^{\mathrm{Im}(\gamma)}(\mathbb{F})$, since

$\sum_{\sigma\in\mathrm{Im}(\gamma)}\chi_{\sigma}=\mathbb{J}_{V^{r}}$ (1)

and by invariance of $\gamma$, for any $\sigma\in\mathrm{Im}(\gamma)$ there is
some $\sigma^{\prime}$ such that $(\chi_{\sigma})^{t}=\chi_{\sigma^{\prime}}$.

Define the relation $\sim_{\mathrm{sol}}$ on $\mathcal{X}_{V}^{I}(\mathbb{F})$
as follows: $\vec{A}\sim_{\mathrm{sol}}\vec{B}$ if there is some
$S\in\mathfrak{P}_{V}(\mathbb{F})$ such that $A_{i}S=SB_{i}$ for all $i\in I$.

######  Lemma 3.1.

$\sim_{\mathrm{sol}}$ is an equivalence relation on
$\mathcal{X}_{V}^{I}(\mathbb{F})$.

###### Proof.

Clearly, $\vec{A}\sim_{\mathrm{sol}}\vec{A}$, since
$\mathbb{I}_{V}\in\mathfrak{P}_{V}(\mathbb{F})$ and
$A_{i}\mathbb{I}_{V}=\mathbb{I}_{V}A_{i}$ for all $i\in I$. Suppose
$\vec{A}\sim_{\mathrm{sol}}\vec{B}$. Let $S\in\mathfrak{P}_{V}(\mathbb{F})$
satisfy $A_{i}S=SB_{i}$ for all $i\in I$. Then $B_{i}^{t}S^{t}=S^{t}A_{i}^{t}$
and thus, from the definition of $\mathcal{X}_{V}^{I}$,
$B_{i}S^{t}=S^{t}A_{i}$ for all $i\in I$. Since
$S^{t}\in\mathfrak{P}_{V}(\mathbb{F})$, $\vec{B}\sim_{\mathrm{sol}}\vec{A}$.
Finally, suppose $\vec{A}\sim_{\mathrm{sol}}\vec{B}$ and
$\vec{B}\sim_{\mathrm{sol}}\vec{C}$. Let $S,T\in\mathfrak{P}_{V}(\mathbb{F})$
satisfy $A_{i}S=SB_{i}$ an $B_{i}T=TC_{i}$ for all $i\in I$. Then
$A_{i}ST=SB_{i}T=STC_{i}$. Since $S,T,S^{t}$ and $T^{t}$ must all have
$\mathbf{1}_{V^{r}}$ as eigenvector, with corresponding eigenvalue $1$, so
must $ST$ and $(ST)^{t}$. Hence, $ST\in\mathfrak{P}_{V}(\mathbb{F})$ and
$\vec{A}\sim_{\mathrm{sol}}\vec{C}$. ∎

For $k,r\in\mathbb{N}$ with $2r<k$, a field $\mathbb{F}$, and an invariant
$\gamma\in\mathcal{P}(V^{k})$, we define the _solvability operators_
$\mathrm{S}_{k,r}^{\mathbb{F}}$ by setting
$\mathrm{S}_{k,r}^{\mathbb{F}}\circ\gamma$ to be the labelled partition for
which the colour of $\vec{v}\in V^{k}$ is a tuple whose entries are
$\gamma(\vec{v})$ and the equivalence classes under the relation
$\sim_{\mathrm{sol}}$ of the $(\vec{i},\vec{v})$-character vectors of
$\gamma$, for all $\vec{i}\in[k]^{(2r)}$. Formally:

$\begin{matrix}\mathrm{S}_{k,r}^{\mathbb{F}}\circ\gamma:&V^{k}&\rightarrow&\mathrm{Im}(\gamma)\times(\mathcal{X}_{V^{r}}^{\mathrm{Im}(\gamma)}(\mathbb{F})/\sim_{\mathrm{sol}})^{[k]^{(2r)}}\\\
&\vec{v}&\mapsto&(\gamma(\vec{v}),(\vec{\chi}_{\vec{i}})_{\vec{i}\in[k]^{(2r)}}),\end{matrix}$

where $\vec{\chi}_{\vec{i}}$ is the $(\vec{i},\vec{v})$-character vector of
$\gamma$.

As before, since the entries of the matrices in the character vector are all
$0$ and $1$, we may restrict $\mathbb{F}$ to being a prime field without loss
of generality, and denote $\mathrm{S}_{k,r}^{\mathbb{F}}$ by
$\mathrm{S}_{k,r}^{c}$, where $c=\mathrm{char}(\mathbb{F})$.

Observe that $\mathrm{S}_{k,r}^{c}$ is monotone on the class of invariant
partitions of $V^{k}$ and is thus a $k$-refinement operator when considered
with this domain restriction. Indeed, if $\gamma,\rho\in\mathcal{P}(V^{k})$
are invariant and $\gamma\preceq\rho$, then for every
$\alpha\in\mathrm{Im}(\gamma)$ there is some
$I_{\alpha}\subseteq\mathrm{Im}(\rho)$ such that
$\gamma^{-1}(\sigma)=\bigcup_{\beta\in I_{\sigma}}\rho^{-1}(\beta)$. Fix
$\vec{i}\in[k]^{(2r)}$ and $\vec{v}\in V^{k}$, and let $\vec{\chi}$ and
$\vec{\xi}$ be the $(\vec{i},\vec{v})$-character vectors of $\gamma$ and
$\rho$ respectively. Then

$\chi_{\alpha}=\sum_{\beta\in I_{\alpha}}\xi_{\beta}.$

It readily follows that if
$\mathrm{S}_{k,r}^{c}\circ\rho(\vec{u})=\mathrm{S}_{k,r}^{c}\circ\rho(\vec{v})$,
then
$\mathrm{S}_{k,r}^{c}\circ\gamma(\vec{u})=\mathrm{S}_{k,r}^{c}\circ\gamma(\vec{v})$
and thus,
$\mathrm{S}_{k,r}^{c}\circ\gamma\preceq\mathrm{S}_{k,r}^{c}\circ\rho$.

In a similar fashion to Proposition $4.6$ in [DV20], one can show that
$\mathrm{S}_{k,r}^{c}$ are graph-like refinement operators. Thus, for any
invariant $\gamma\in\mathcal{P}(V^{k})$, $[\gamma]^{\mathrm{S}_{k,r}^{c}}$ is
the unique coarsest $\mathrm{S}_{k,r}^{c}$-stable partition refining $\gamma$,
up to relabelling of its equivalence classes.

For the remainder of this section, we assume that
$\gamma\in\mathcal{P}(V^{k})$ is invariant and that $\vec{\chi}$ and
$\vec{\xi}$ are the $(\vec{i},\vec{v})$ and $(\vec{i},\vec{u})$-character
vectors of $\gamma$ respectively, for some fixed $\vec{i}\in[k]^{(2r)}$. The
following is a direct consequence of the definition of $\mathrm{S}_{k,r}^{c}$.

######  Proposition 3.2.

Let $\mathbb{F}$ be the prime field of characteristic $c$. For all
$k,r\in\mathbb{N}$, with $2r\leq k$,
$\mathrm{S}_{k,r}^{c}\circ\gamma(\vec{u})=\mathrm{S}_{k,r}^{c}\circ\gamma(\vec{v})$
if, and only if, $\gamma(\vec{u})=\gamma(\vec{v})$ and for each
$\vec{i}\in[k]^{(2r)}$ there exist some $M\in\mathfrak{P}_{V^{r}}(\mathbb{F})$
such that for all $\sigma\in\mathrm{Im}(\gamma)$

$\chi_{\sigma}M=M\xi_{\sigma}.$

In particular, $\gamma$ is $\mathrm{S}_{k,r}^{c}$-stable if, and only if, for
all $\vec{u},\vec{v}\in V^{k}$ and $\vec{i}\in[k]^{(2r)}$

$\gamma(\vec{u})=\gamma(\vec{v})\implies\exists
M\in\mathfrak{P}_{V^{r}}(\mathbb{F}),\chi_{\sigma}M=M\xi_{\sigma}\,\,\forall\sigma\in\mathrm{Im}(\gamma).$

We now show some properties of the operator $\mathrm{S}_{k,r}^{c}$ in order to
establish the link between the above and finite variable fragments of the
extension of first-order logic with solvability quantifiers.

######  Lemma 3.3.

An $\mathrm{IM}_{k,r}^{c}$-stable partition is $\mathrm{S}_{k,r}^{c}$-stable.

###### Proof.

Let $\mathbb{F}$ be the prime field of characteristic $c$. Suppose $\gamma$ is
$\mathrm{IM}_{k,r}^{c}$-stable and let $\gamma(\vec{u})=\gamma(\vec{v})$.
Then, for all $\vec{i}\in[k]^{(2r)}$, there is some $M\in
GL_{V^{r}}(\mathbb{F})$ such that $M^{-1}\chi_{\sigma}M=\xi_{\sigma}$ for all
$\sigma\in\mathrm{Im}(\gamma)$. By equation 1,
$M\mathbb{J}_{V^{r}}=\mathbb{J}_{V^{r}}M$ and thus, both $M$ and $M^{t}$ have
$\mathbf{1}_{V^{r}}$ as eigenvector with corresponding non-zero eigenvalue
$\lambda\in\mathbb{F}$. Since,
$\frac{1}{\lambda}M\in\mathfrak{P}_{V^{r}}(\mathbb{F})$, the result follows. ∎

######  Lemma 3.4.

If $\gamma$ is $\mathrm{S}_{k,r}^{c}$-stable the following hold:

  1. 1.

If $\gamma(\vec{u})=\gamma(\vec{v})$, and $\gamma$ is graph-like, then for all
$\vec{i}\in[k]^{(2r)}$ and $\sigma\in\mathrm{Im}(\gamma)$, $\\{\vec{w}\in
V^{r}\mid\gamma(\vec{u}\langle\vec{i},\vec{w}\cdot\vec{w}\rangle)=\sigma\\}$
is non-empty if, and only if, $\\{\vec{w}\in
V^{r}\mid\gamma(\vec{v}\langle\vec{i},\vec{w}\cdot\vec{w}\rangle)=\sigma\\}$
is non-empty.

  2. 2.

If $c=0$, then $\gamma$ is $\mathrm{C}_{k,2r}$-stable.

Note that if $c=0$, the second statement implies the first (refer to Section
$4$ and $5$ of [DV20] for more details on properties of
$\mathrm{C}_{k,r}$-stability).

###### Proof.

Suppose $\\{\vec{w}\in
V^{r}\mid\gamma(\vec{u}\langle\vec{i},(\vec{w}\cdot\vec{w})\rangle)=\sigma\\}$
is non-empty. Since $\gamma$ is graph-like, $\chi_{\sigma}$ must have all the
non-zero entries on the diagonal. Hence, for any
$M\in\mathfrak{P}_{V^{r}}(\mathbb{F})$, $\chi_{\sigma}M$ and, consequently
$M\xi_{\sigma}$ must be non-zero. As such, $\\{\vec{w}\in
V^{r}\mid\gamma(\vec{v}\langle\vec{i},(\vec{w}\cdot\vec{w})\rangle)=\sigma\\}$
is non-empty. The converse can be argued by symmetry, thus showing $(1)$.

For $(2)$, it suffices to show that: if $A,B\in\mathrm{Mat}_{V}(\mathbb{F})$
are $01$-matrices and $AM=MB$ for some $M\in\mathfrak{P}_{V}(\mathbb{F})$ then
$A$ and $B$ have the same number of non-zero entries if
$\mathrm{char}(\mathbb{F})=0$. Indeed, note that if $\alpha$ and $\beta$ are
the number of non-zero entries of $A$ and $B$ respectively, then
$\alpha\mathbb{J}_{V}=\mathbb{J}_{V}A\mathbb{J}_{V}$ and
$\beta\mathbb{J}_{V}=\mathbb{J}_{V}B\mathbb{J}_{V}$. Since
$M\mathbb{J}_{V}=\mathbb{J}_{V}M=\mathbb{J}_{V}$,

$\alpha\mathbb{J}_{V}=\mathbb{J}_{V}A\mathbb{J}_{V}=\mathbb{J}_{V}AM\mathbb{J}_{V}=\mathbb{J}_{V}MB\mathbb{J}_{V}=\mathbb{J}_{V}B\mathbb{J}_{V}=\beta\mathbb{J}_{V},$

whence $\alpha=\beta$. ∎

In particular, if $r=1$, statement $(1)$ above implies that there is some
$x\in V$ such that $\mathrm{pr}_{k-1}\gamma(\mathrm{pr}_{k-1}\vec{u}\langle
i,x\rangle)=\sigma$ if, and only if, there is some $y\in V$, such that
$\mathrm{pr}_{k-1}\gamma(\mathrm{pr}_{k-1}\vec{v}\langle i,y\rangle)=\sigma$.
Furthermore, from $(2)$ and Lemma $5.7$ in [DV20], $\mathrm{pr}_{k-1}\gamma$
is $\mathrm{C}_{k-1}$ stable.

######  Corollary 3.5.

Let $\gamma=[\alpha_{k,\Gamma}]^{\mathrm{S}_{k,1}^{c}}$ for some graph
$\Gamma$ on $V$. If
$\mathrm{pr}_{k-1}\gamma(\vec{u})=\mathrm{pr}_{k-1}\gamma(\vec{v})$, there are
no first-order formulae distinguishing
$(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{u})$ from
$(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{v})$. In addition, if $c=0$, there
are no $\mathcal{C}_{k-1}$-formulae distinguishing
$(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{u})$ from
$(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{v})$.

Similarly to the invertible map operators, we define the $k$-refinement
operator $\mathrm{S}_{k}^{c}$ so that for $\gamma\in\mathcal{P}(V^{k})$, the
colour of $\vec{v}\in V^{k}$ in $\mathrm{S}_{k}^{c}\circ\gamma$ is given by a
tuple whose entries are the colours of $\vec{v}$ in
$\mathrm{S}_{k,r}^{c}\circ\gamma$, for all $r<k/2$; that is,

$\mathrm{S}_{k}^{c}\circ\gamma(\vec{v})=(\mathrm{S}_{k,1}^{c}\circ\gamma(\vec{v}),\mathrm{S}_{k,2}^{c}\circ\gamma(\vec{v}),\ldots,\mathrm{S}_{k,\lfloor
k/2\rfloor}^{c}\circ\gamma(\vec{v})).$

The next statement will be the crux of our main results.

######  Theorem 3.6.

For any prime number $p$, if $\gamma=[\alpha_{k,\Gamma}]^{\mathrm{S}_{k}^{p}}$
and $\gamma(\vec{u})=\gamma(\vec{v})$, there are no FOS${}_{k-1}(p)$ formulae
distinguishing $(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{u})$ from
$(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{v})$.

###### Proof.

We proceed by induction on the structure of FOS$(p)$ formulae $\phi(\vec{z})$,
where $\vec{z}$ is a $k$-tuple of pairwise distinct variables. If
$\phi(\vec{z})$ contains only atomic formulae, boolean connectives and first
order quantifiers, the statement holds by Corollary 3.5. Assume that for some
$\phi(\vec{z})\in\text{FOS}_{k}(p)$,
$\mathfrak{A}_{\Gamma}\models\phi(\vec{u})\iff\mathfrak{A}_{\Gamma}\models\phi(\vec{v})$,
and suppose
$(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{v})\models\mathrm{slv}_{p}[\vec{x}\vec{y}.\phi(\vec{z}\langle\vec{i},\vec{x}\cdot\vec{y}\rangle)]$,
where $\vec{i}\in[k]^{(2r)}$ and $\vec{x},\vec{y}$ are $r$-tuples of distinct
variables (distinct from variables in the tuple $\vec{z}$). Let $S^{\vec{v}}$
be the adjacency matrix of the relation $\\{(\vec{a},\vec{b})\in V^{r}\times
V^{r}\mid(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{v})\models\phi(\vec{v}\langle\vec{i},\vec{a}\cdot\vec{b}\rangle)\\}$,
and similarly define $S^{\vec{u}}$. Then, there is some
$\vec{a}\in\mathbb{Z}_{p}^{V^{r}}$ such that
$S^{\vec{v}}\vec{a}=\mathbf{1}_{V^{r}}$. By the induction hypothesis,
$S^{\vec{u}}=\sum_{\sigma\in I}\chi_{\sigma}$ and $S^{\vec{v}}=\sum_{\sigma\in
I}\xi_{\sigma}$ for some $I\subseteq\mathrm{Im}(\gamma)$. Since there exists
$M\in\mathfrak{P}_{V^{r}}(\mathbb{Z}_{p})$ such that
$\chi_{\sigma}M=M\xi_{\sigma}$ for all $\sigma\in\mathrm{Im}(\gamma)$, we have

$S^{\vec{v}}\vec{a}=\mathbf{1}_{V^{r}}\implies
MS^{\vec{v}}\vec{a}=\mathbf{1}_{V^{r}}\implies
S^{\vec{u}}(M\vec{a})=\mathbf{1}_{V^{r}},$

from which it follows that
$(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{u})\models\mathrm{slv}_{p}[\vec{x}\vec{y}.\phi(\vec{z}\langle\vec{i},\vec{x}\cdot\vec{y}\rangle)]$.
Using a symmetric argument, we conclude that
$\mathrm{slv}_{p}[\vec{x}\vec{y}.\phi(\vec{z}\langle\vec{i},\vec{x}\cdot\vec{y}\rangle)]$
does not distinguish $(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{u})$ from
$(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{v})$ and the result follows by
induction. ∎

###  3.4 Polynomial, monomial and Nullstellensatz calculi

The idea behind the proof systems we are concerned with is that of encoding
Boolean formulae by multivariate polynomials over a field and determining, via
inference rules, if these do not have a common root. In such cases, we
conclude that the formulae are inconsistent. The _polynomial calculus_ (PC),
_monomial calculus_ (MC) and _Nullstellensatz calculus_ (NC) are proof systems
of this kind that have been studied in the literature. The PC inference rules
for a set of axioms $A\subset\mathbb{F}[x_{1},...,x_{n}]$ are as follows:

  1. 1.

$\frac{}{f}$ for all $f\in A$.

  2. 2.

_Multiplication rule_ : $\frac{f}{xf}$ for all derived polynomials $f$, and
variables $x\in\\{x_{1},...,x_{n}\\}$.

  3. 3.

_Linearity rule_ : $\frac{f,g}{\lambda f+\mu g}$ for all derived polynomials
$f,g$ and $\lambda,\mu\in\mathbb{F}$.

The inference rules for MC are obtained by restricting $f$ in the
multiplication rule to be an axiom times a monomial or a monomial. By further
restricting $f$ to be an axiom times a monomial, one obtains the NC inference
rules. The _degree_ of a PC (or MC or NC) derivation is the maximum degree of
all polynomials involved in the derivation, and a PC (or MC or NC,
respectively) _refutation_ of $A$ is a derivation of $1$ from $A$ using PC (or
MC or NC, respectively) rules. We are really interested in roots where the
variables are assigned $01$-values, so as to encode the Boolean framework. To
enforce this, we tacitly assume that the set of axioms always includes the
polynomials $x^{2}-x$ for all $x\in\\{x_{1},\ldots,x_{n}\\}$. As such, we may
restrict our focus to multilinear polynomials exclusively: indeed, if, for
distinct variables $x$ and $y$, we may derive $x^{2}y$, we can also derive
$x^{2}y-y(x^{2}-x)=xy$.

It is easy to check that all three proof systems are sound and, by Hilbert’s
weak Nullstellensatz Theorem444This is a fundamental result in algebra which
states that the polynomials of an ideal in $\mathbb{F}[x_{1},...x_{n}]$ have a
common root in the algebraic closure of $\mathbb{F}$ if, and only if, $1$ is
not in the ideal., complete. That is, there is a refutation in each of the
proof systems if, and only if, the polynomials in the axioms do not have a
common root. In general, the degree of refutations can be unbounded, which
suggests that such a quantity is a reasonable complexity parameter to study.
We denote by PCk the proof system using the same inference rules as PC with
the added constraint that all derivations must have degree at most $k$, and we
use the same convention for MCk and NCk. Though these proof systems with
bounded degree are not complete, their refutations can be decided in
polynomial time in the number of variables.

For a graph $\Gamma$ on $V$ we define
$\mathrm{Ax}(\Gamma)\subseteq\mathbb{F}[\\{x_{uv}|u,v\in V\\}]$ to be the set
of axioms containing the following polynomials:

  * A1.

$\sum_{u\in V}x_{uv}-1\;\,\textrm{ for all $v\in V$.}$

  * A2.

$\sum_{u\in V}x_{vu}-1\;\,\textrm{ for all $v\in V$.}$

  * A3.

$x_{uv}x_{u^{\prime}v^{\prime}}\;\,\textrm{ if the map $u\mapsto
u^{\prime},v\mapsto v^{\prime}$ is not a local isomorphism in $\Gamma$.}$

  * A4.

$x_{uv}^{2}-x_{uv}\;\,\textrm{for all $u,v\in V$.}$

For $\vec{u},\vec{v}\in V^{k}$, we further define
$\mathrm{Ax}(\Gamma_{\vec{u}\rightarrow\vec{v}})$ to contain the above plus
the following:

  * A5.

$x_{v_{i}u_{i}}-1\;\,\textrm{for all $i\in[k]$.}$

Note that any of these proof systems has a refutation of
$\mathrm{Ax}(\Gamma_{\vec{u}\rightarrow\vec{v}})$ if, and only if, $\vec{u}$
and $\vec{v}$ are in different equivalence classes of the $k$-orbit partition
for $\Gamma$ . Furthermore, any of the proof systems has a degree $d$
refutation of $\mathrm{Ax}(\Gamma_{\vec{u}\rightarrow\vec{v}})$ if, and only
if, it allows a degree $d$ derivation from $\mathrm{Ax}(\Gamma)$ of the
monomial $\prod_{i\in J}x_{v_{i}u_{i}}$ for some subset $J\subseteq[k]$ of
size at most $d$. Since all coefficients of the elements of
$\mathrm{Ax}(\Gamma_{\vec{u}\rightarrow\vec{v}})$ are $0$ and $\pm 1$,
refutations can be decided by restricting the use of the linearity rule with
$\lambda,\mu$ belonging to the prime subfield of $\mathbb{F}$. When
considering these axioms, we may then assume, without loss of generality, that
$\mathbb{F}$ is a prime field.

Let $\equiv_{\mathrm{PC}_{k}}^{c}$ be the relation on $V^{k}$, where
$\vec{u}\equiv_{\mathrm{PC}_{k}}^{c}\vec{v}$ if there is no degree $k$ PC
refutation of $\mathrm{Ax}(\Gamma_{\vec{u}\rightarrow\vec{v}})$ over the prime
field of characteristic $c$, and similarly define
$\equiv_{\mathrm{MC}_{k}}^{c}$ and $\equiv_{\mathrm{NC}_{k}}^{c}$.

######  Lemma 3.7.

$\equiv_{\mathrm{PC}_{k}}^{c}$, $\equiv_{\mathrm{MC}_{k}}^{c}$ and
$\equiv_{\mathrm{NC}_{k}}^{c}$ are equivalence relations on $V^{k}$.

We prove this statement only for $\equiv_{\mathrm{PC}_{k}}^{c}$, since a
similar argument applies in the other two cases. As remarked above, we may
restrict our focus to multilinear polynomials exclusively and denote the
multilinear monomial $x_{a_{1}}x_{a_{2}}\ldots x_{a_{m}}$ by $X_{A}$ where
$A=\\{a_{1},a_{2},\ldots a_{m}\\}$.

###### Proof.

Clearly, $\vec{u}\equiv_{\mathrm{PC}_{k}}^{c}\vec{u}$. Indeed, the polynomials
in the ideal generated by $\mathrm{Ax}(\Gamma_{\vec{u}\rightarrow\vec{u}})$
have the common root $x_{rs}=\delta_{rs}$, where $\delta_{rs}$ is the
Kronecker delta. Hence, the ideal generated by
$\mathrm{Ax}(\Gamma_{\vec{u}\rightarrow\vec{u}})$ is non-trivial. The set
$\mathrm{Ax}(\Gamma)$ is invariant under the transformation $x_{rs}\rightarrow
x_{sr}$ for all $r,s\in V$. Thus,
$\vec{u}\equiv_{\mathrm{PC}_{k}}^{c}\vec{v}\implies\vec{v}\equiv_{\mathrm{PC}_{k}}^{c}\vec{u}$.

Suppose $\vec{u}\equiv_{\mathrm{PC}_{k}}^{c}\vec{v}$ and
$\vec{v}\equiv_{\mathrm{PC}_{k}}^{c}\vec{w}$. Let $\pi$ be the map
$v_{i}\rightarrow w_{i}$ for $i\in[k]$. Note that $\pi$ is well defined, for
if $v_{i}=v_{j}$ for some $i\neq j$ and $\pi(v_{i})\neq\pi(v_{j})$, then
$x_{v_{i}w_{i}}x_{v_{j}w_{j}}\in\mathrm{Ax}(\Gamma)$ \- a contradiction. For
$A\subseteq V^{2}$, define $A^{\pi}$ as follows:

$A^{\pi}=\begin{cases}\\{(r,\pi(s))\mid(r,s)\in A\\}\;\;\textrm{ if for all
$(r,s)\in A$ there is some $j$ such that $s=v_{j}$;}\\\
\\{(r,\pi^{-1}(s))\mid(r,s\in A)\\}\;\,\textrm{ if for all $(r,s)\in A$ there
is some $j$ such that $s=w_{j}$; and}\\\ A\;\;\textrm{otherwise.}\end{cases}$

For a multilinear polynomial $f=\sum a_{A}X_{A}$, let $p^{\pi}=\sum
a_{A}X_{A^{\pi}}$. We show by induction on the $\mathrm{PC}$ inference rules
that there is a $\mathrm{PC}_{k}$ derivation of $p$ if, and only if, there is
$\mathrm{PC}_{k}$ derivation of $f^{\pi}$. Indeed, if $f$ is in
$\mathrm{Ax}(\Gamma)$, then so is $f^{\pi}$. Suppose there is a
$\mathrm{PC}_{k}$ derivation of $f,g,f^{\pi}$ and $g^{\pi}$. Then there is a
$\mathrm{PC}_{k}$ derivation of $(\lambda f+\mu g)^{\pi}=\lambda f^{\pi}+\mu
g^{\pi}$. Finally, suppose the degree of $f$ is less than $k$, and suppose,
without loss of generality that $f=X_{A}$ for some $A\subseteq V^{2}$. Then,
there is a $\mathrm{PC}_{k}$ derivation of $X_{A\cup\\{(r,s)\\}}$ for any
$r,s\in V$. By checking case by case, it follows that there is a
$\mathrm{PC}_{k}$ derivation of $(X_{A\cup\\{(r,s)\\}})^{\pi}$. Since
$(A^{\pi})^{\pi}=A$ and hence, $(f^{\pi})^{\pi}=f$, there is a
$\mathrm{PC}_{k}$ derivation of $f$ if, and only if, there is a
$\mathrm{PC}_{k}$ derivation of $f^{\pi}$. In particular, since there is no
$\mathrm{PC}_{k}$ derivation of $X_{\\{(v_{i},w_{i})\mid i\in[k]\\}}$, there
is no derivation of $(X_{\\{(u_{i},v_{i})\mid
i\in[k]\\}})^{\pi}=X_{\\{(u_{i},w_{i})\mid i\in[k]\\}}$. Whence,
$\vec{u}\equiv_{\mathrm{PC}_{k}}^{c}\vec{w}$. ∎

It is easy to see that the relation $\equiv_{\mathrm{PC}_{k}}^{c}$ refines
$\equiv_{\mathrm{MC}_{k}}^{c}$ which, in turn, is a refinement of
$\equiv_{\mathrm{NC}_{k}}^{c}$, since any $\mathrm{NC}_{k}$ refutation is a
$\mathrm{MC}_{k}$ refutation which is also a $\mathrm{PC}_{k}$ refutation.
More precisely:

######  Lemma 3.8.

For any graph on $V$ and $\vec{u},\vec{v}\in V^{k}$,
$\vec{u}\equiv_{\mathrm{PC}_{k}}^{c}\vec{v}\implies\vec{u}\equiv_{\mathrm{MC}_{k}}^{c}\vec{v}\implies\vec{u}\equiv_{\mathrm{NC}_{k}}^{c}\vec{v}$.

For $c=0$, Grohe et. al. have characterized these equivalence relations in
terms of counting logics. More precisely:

> Let $\Gamma$ be a graph on $V$ and $\vec{u},\vec{v}\in V^{k}$. Then
> $\vec{u}\equiv_{\mathrm{MC}_{k}}^{0}\vec{v}$ if, and only if, no
> $\mathcal{C}_{k}$ formula distinguishes
> $(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{u})$ from
> $(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{v})$ (Theorem $4.4$ in [BG15]).
> Furthermore, if $\vec{u}\not\equiv_{\mathrm{PC}_{k}}^{0}\vec{v}$, there a
> $k^{\prime}=O(k)$, such that some $\mathcal{C}_{k^{\prime}}$ formula
> distinguishes $(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{u})$ from
> $(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{v})$ (Theorem 6.6 in [GGPP19]).

In this paper, we aim at a similar characterization for the equivalence
relations induced by the proof systems in fields of positive characteristic.
The corresponding logic we consider are the finite variable fragments of the
extension of first-order logic with solvability quantifiers. This allows us to
relate the distinguishing power of these relations to that of the equivalence
relations defined by the invertible map tests.

##  4 Definability of monomial calculus refutations over finite fields

At the core of the proof of Theorem 1.2 is the definability of monomial
calculus refutations in FPS$(p)$. More precisely, the main objective of this
section is to prove the following statement.

######  Lemma 4.1.

Let $\mathfrak{A}$ be a structural encoding of a finite set of polynomials $P$
of degree at most $d$, over a finite field $\mathbb{F}$ of positive
characteristic $p$. For any $d,k\in\mathbb{N}$ there is a $\mathrm{FPS}(p)$
formula $\phi_{d,k}$ such that $\mathfrak{A}\models\phi_{d,k}$ if, and only
if, there is an $\mathrm{MC}_{k}$ refutation of $P$ over $\mathbb{F}$. 555Note
that it is possible to drop the dependence on $d$, but this would involve a
more cumbersome definition of $\mathfrak{A}$ and subsequent interpretations.
Since elements of $\mathrm{Ax}(\Gamma)$ have degree at most $2$, this
statement is sufficient for our purpose.

For the sake of argument, we assume that $\mathbb{F}=\mathbb{Z}_{p}$. We first
recall how to express the solvability of linear equations with coefficients
other than $0$ and $1$ and explain the meaning of _structural encoding_ of a
set of polynomials.

###  4.1 Defining solvability of linear equations over finite fields

For each prime number $p$, let $\mathtt{LIN}_{p}$ be a relational vocabulary
with the following symbols:

  1. 1.

A binary relational symbol $\texttt{A}_{q}$ for each $q\in\mathbb{Z}_{p}$.

  2. 2.

A unary relational symbol $\texttt{b}_{q}$ for each $q\in\mathbb{Z}_{p}$.

Let $A\in\mathrm{Mat}_{E\times V}(\mathbb{Z}_{p})$ and
$\vec{b}\in\mathbb{Z}_{p}^{E}$. A $\mathtt{LIN}_{p}$-structure $\mathfrak{A}$
with universe $V\cup E$ ($V$ for variables and $E$ for equations) encodes the
system of linear equations $A\vec{x}=\vec{b}$ if, for all $e\in E,v\in V$,
$\mathfrak{A}\models\texttt{A}_{q}(e,v)$ if $A_{ev}=q$ and
$\mathfrak{A}\models\texttt{b}_{q}(e)$ if $b_{e}=q$.

Recall Lemma 4.1 in [DGH+12].

######  Lemma 4.2.

There is a quantifier free interpretation $\mathcal{I}$ of $\mathtt{LIN}_{p}$
into $\mathtt{LIN}_{p}$ such that if $\mathfrak{A}$ encodes the system of
linear equations $A\vec{x}=\vec{b}$, then:

  1. 1.

$\mathcal{I}(\mathfrak{A})$ encodes a system of linear equations
$A^{\prime}\vec{y}=\mathbf{1}$, where $\mathbf{1}$ is the all $1$s vector of
appropriate length and $A^{\prime}$ is a $01$-matrix.

  2. 2.

$A^{\prime}\vec{y}=\mathbf{1}$ has a solution if, and only if,
$A\vec{x}=\vec{b}$ has a solution.

Thus,
$\mathcal{I}(\mathfrak{A})\models\mathrm{slv}_{p}(xy.\mathtt{A}_{1}(x,y))$ if,
and only if, $A\vec{x}=\vec{b}$ has a solution and hence, from the
Interpretation Lemma, there is a FOS$(p)$ formula $\Phi$ such that
$\mathfrak{A}\models\Phi$ if, and only if, the system of linear equations
encoded by $\mathfrak{A}$ has a solution.

###  4.2 Proof of Lemma 4.1

Monomial calculus refutations of bounded degree can be understood as the
following procedure, where the input is a finite set of multilinear
polynomials $P$ from the ring $\mathbb{F}[x_{1},\ldots,x_{r}]$, and the output
is REFUTE or NOREFUTE. We denote the multilinear monomial
$x_{a_{1}}x_{a_{2}}\ldots x_{a_{r}}$ by $X_{A}$ where
$A=\\{a_{1},a_{2}\ldots,a_{r}\\}$, so that for a polynomial $f$,
$X_{A}f=x_{a_{1}}x_{a_{2}}\ldots x_{a_{r}}f$. In this form, $X_{\emptyset}$
denotes $1$.

  1. INPUT.

$P\subset\mathbb{F}[x_{1},\ldots,x_{r}]$

  2. OUTPUT.

REFUTE or NOREFUTE.

  3. 1.

Initialize $\mathcal{S}=\\{X_{A}f\mid f\in P,\mathrm{deg}(X_{A}f)\leq k\\}$.

  4. 2.

while $\mathrm{span}_{\mathbb{F}}\mathcal{S}$ has changed since last round or
$1\notin\mathrm{span}_{\mathbb{F}}\mathcal{S}$ do lines 3-4

  5. 3.

$\mathcal{M}\leftarrow\\{A\subseteq[r]\mid|A|<k,X_{A}\in\mathrm{span}_{\mathbb{F}}\mathcal{S}\\}.$

  6. 4.

$\mathcal{S}\leftarrow\mathcal{S}\cup\\{X_{B}\mid|B|\leq k,\exists
A\in\mathcal{M},A\subseteq B\\}.$

  7. 5.

If $1\in\mathrm{span}_{\mathbb{F}}\mathcal{S}$ output REFUTE

  8. 6.

else output NOREFUTE.

Put otherwise, the procedure computes the inflationary fixed point of the set
of monomials within the $\mathbb{F}$-span of $\mathcal{S}$ and checks whether
it contains the constant $1$ or its dimension has increased. This does not
require to store in memory the set $\mathrm{span}_{\mathbb{F}}\mathcal{S}$
(whose size is exponential in the input), but can be done by checking the
solvability of linear equations. The number of iterations of the while loop is
at most the number of multilinear monomials of degree at most $k$, thus
ensuring that the procedure runs, overall, in polynomial time. Crucially, at
each iteration of the while loop, the $\mathbb{F}$-span of $\mathcal{S}$ has a
_canonical_ generating set. As illustrated below, this property is really what
allows definability of the above procedure in FPS$(p)$.

Recall that we are assuming that $\mathbb{F}=\mathbb{Z}_{p}$. By viewing
polynomials over $\mathbb{Z}_{p}$ as vectors in the standard basis given by
monomials, we encode $P$ as a structure $\mathfrak{A}$ with universe $V$ over
the vocabulary
$\mathtt{POLY}_{p}=(\mathtt{Var},\mathtt{U},\mathtt{C}_{0},\mathtt{C}_{1},\ldots,\mathtt{C}_{p-1})$,
where:

  1. 1.

$V=P\cup\\{x_{i}\mid i\in[r]\\}\cup\\{1\\}$.

  2. 2.

$\mathtt{Var}$ and $\mathtt{U}$ are unary relational symbol with
$\mathfrak{A}\models\mathtt{Var}(v)$ if, and only if $v\in\\{x_{i}\mid
i\in[r]\\}$, and $\mathfrak{A}\models\mathtt{U}(v)$ if, and only if, $v=1$.

  3. 3.

$\mathtt{C}_{q}$ for $q\in\mathbb{Z}_{p}$ are $(d+1)$-ary relations, where $d$
is the maximal degree of the polynomials in $P$. These encode $P$ in matrix
form; that is, $\mathfrak{A}\models\mathtt{C}_{q}(u,v_{1},\ldots,v_{d})$ if,
and only if, $u\in P$, each $v_{i}$ is equal to a variable or $1$, and the
coefficient of the monomial $v_{1}v_{2}\ldots v_{d}$ in $u$ is equal to $q$.

Note that there is a formula $\delta_{m}$ identifying the polynomials in $P$
of degree $m$. Indeed, let $\kappa_{m,t}(v_{1},\ldots,v_{t})$ for each $t\geq
m$ be a formula satisfied by $\mathfrak{A}$ if, and only if,
$v_{1},\ldots,v_{t}$ assume exactly $m$ distinct values from $\\{x_{i}\mid
i\in[r]\\}$, and define

$\hat{\delta}_{m}(u)=\bigvee_{q\in\mathbb{Z}_{p}^{*}}\exists z_{1}\ldots
z_{d}.\mathtt{C}_{q}(u,z_{1},\ldots,z_{d})\land\kappa_{m,d}(z_{1},\ldots,z_{d})$

Then $\delta_{m}(u)=\hat{\delta}_{m}(u)\land\lnot\hat{\delta}_{m+1}(u)$ is
satisfied by $\mathfrak{A}$ if, and only if, $u\in P$ has degree $m$.

Next, we use a $k$-ary interpretation to obtain a structure whose universe is
the set of multilinear polynomials of degree at most $k$. Formally, let
$\mathtt{POLY}_{p}^{*}=(\mathtt{A}_{0},\mathtt{A}_{1},\ldots,\mathtt{A}_{p-1},\mathtt{U}^{*},\mathtt{Mon},\mathtt{Sub})$
be a vocabulary where $\mathtt{Mon}$ and $\mathtt{U}^{*}$ are unary relational
symbols, $\mathtt{Sub}$ is a binary relational symbol, and $\mathtt{A}_{q}$
are as in the vocabulary $\mathtt{LIN}_{p}$. One can then define an
interpretation $\mathcal{J}$ from $\mathtt{POLY}_{p}$ into
$\mathtt{POLY}^{*}_{p}$ such that:

  1. 1.

The universe of $\mathcal{J}(\mathfrak{A})$ are elements $\vec{v}\in V^{k}$
such that

$\mathfrak{A}\models\bigwedge_{i\in[k]}\mathtt{U}(v_{i})\lor\bigwedge_{i\in[k]}\mathtt{Mon}(v_{i})\lor\bigvee_{m\in[k]}\delta_{m}(v_{1})\land\kappa_{k-m,k}(v_{2},\ldots,v_{k}),$
(2)

and the equivalence relation $\equiv_{\mathcal{J}}$ on $V^{k}$ defined by the
equivalence formula of $\mathcal{J}$ is as follows:
$\vec{u}\equiv_{\mathcal{J}}\vec{v}$ if, and only if, the set of entries of
$\vec{u}$ is the same as that of $\vec{v}$. Put otherwise, formula (2) ensures
that the elements of the universe of $\mathcal{J}(\mathfrak{A})$ are tuples
$\vec{v}$ where either all $v_{i}$ are equal to $1$, all $v_{i}$ are
variables, or $v_{1}$ is a polynomial in $P$ and $v_{2},\ldots,v_{k}$ are
either all equal to $1$ or are variables such that $|\\{v_{i}\mid 2\leq i\leq
k\\}|\leq k-\mathrm{deg}(v_{1})$. The relation $\equiv_{\mathcal{J}}$
partitions the universe into equivalence classes uniquely determined by the
set of entries of each tuple. If the entries of $\vec{v}$ are all equal to
$1$, we indicate its class by $X_{\emptyset}$, and similarly, if
$v_{i}=x_{a_{i}}$ for all $i\in[k]$, we indicate its class by $X_{A}$ where
$A=\\{a_{i}\mid i\in[k]\\}$. If $v_{1}=f$ for some $f\in P$ and
$v_{2},\ldots,v_{k}$ are all equal to $1$, we indicate the class of $\vec{v}$
by $f$ and if $v_{i}=a_{i}$ for $2\leq i\leq k$, we indicate its class by the
pair $(X_{A},f)$ where $A=\\{a_{i}\mid 2\leq i\leq k\\}$.

  2. 2.

$\mathfrak{A}\models\mathtt{U}(\vec{v})$ and
$\mathfrak{A}\models\mathtt{Mon}(\vec{v})$ if, and only if, the equivalence
class of $\vec{v}$ is $X_{\emptyset}$ and $X_{A}$ with $|A|\geq 1$
respectively.

  3. 3.

$\mathfrak{A}\models\mathtt{A}_{q}(\vec{u},\vec{v})$ if, and only if, the
equivalence class of $\vec{u}$ and $\vec{v}$ are $X_{A}$ and $(X_{B},f)$ for
some $f\in P$ respectively, and the coefficient of $X_{A}$ in $X_{B}f$ equals
$q$.

  4. 4.

$\mathfrak{A}\models\mathtt{Sub}(\vec{u},\vec{v})$ if, and only if, the
equivalence classes of $\vec{u}$ and $\vec{v}$ are $X_{A}$ and $X_{B}$
respectively and $A\subseteq B$.

We leave the details to the reader to check that the above relations on
$V^{k}$ can be defined by first-order formulae.

Thus far, we have shown that the INPUT of the monomial calculus procedure and
the initial set $\mathcal{S}$ in line $1$ can be defined in first-order logic.
The last thing required for proving Lemma 4.1 is showing the definability of
monomials in the set $\mathcal{S}$ _after_ each iteration of the while loop,
which is where the solvability quatifier and fixed-point operator come into
play. In what follows, set $\mathcal{T}=\\{X_{A}f\mid f\in
P,A\subseteq[r],\textrm{deg}(X_{A}f)\leq k\\}$.

###### Proof of Lemma 4.1.

Let $\psi(z)$ be some FPS$(p)$ formula over the vocabulary POLY*p. There is an
interpretation $\mathcal{K}(t)$ of $\mathtt{POLY}_{p}^{*}$ into
$\mathtt{LIN}_{p}$ such that $\mathcal{K}(\mathcal{J}(\mathfrak{A}),t\mapsto
X_{A})$ encodes the system of linear equations determining whether $X_{A}$ is
in the $\mathbb{Z}_{p}$-span of the set

$\mathcal{T}_{\psi}=\mathcal{T}\cup\\{X_{B}\mid(\mathfrak{A},z\mapsto
X_{B})\models\psi(z)\land\mathtt{Mon}(z)\\}.$

By Lemma 4.2, there is a FPS$(p)$ formula $\theta_{\psi}(z)$, depending on
$\psi$, such that $(\mathcal{J}(\mathfrak{A}),z\mapsto
X_{A})\models\theta_{\psi}(z)$ if, and only if, the monomial $X_{A}$ is in the
$\mathbb{Z}_{p}$-span of $\mathcal{T}_{\psi}$.

In particular, replacing $\psi$ with some unary relational variable $Z$, then

$(\mathcal{J}(\mathfrak{A}),z\mapsto X_{A})\models\exists
y.\theta_{Z}(y)\land\mathtt{Sub}(y,z)$

holds if, and only if, there is some $B\subseteq A$ such that $X_{B}$ is in
the $\mathbb{Z}_{p}$-span of $\mathcal{T}_{Z}$. Whence,

$(\mathcal{J}(\mathfrak{A}),z^{\prime}\mapsto
X_{\emptyset})\models\mathrm{ifp}_{Z,z}(\exists
y.\theta_{Z}(y)\land\mathtt{Sub}(y,z))(z^{\prime})$ (3)

if, and only if, there is an $\mathrm{MC}_{k}$ refutation of $P$ over
$\mathbb{Z}_{p}$. By applying the Interpretation Lemma to the above formula
and the interpretation $\mathcal{J}$, the desired result follows. ∎

Note that in formula 3, the solvability quantifier is included in the formula
$\theta_{Z}(y)$.

######  Corollary 4.3.

For any $k\in\mathbb{N}$, there is some $k^{\prime}$ such that for any graph
$\Gamma$ on $V$ and $\vec{u},\vec{v}\in V^{k}$, if there is a
$\mathrm{MC}_{k}$ refutation of
$\mathrm{Ax}(\Gamma_{\vec{u}\rightarrow\vec{v}})$ over $\mathbb{Z}_{p}$, then
there is some FOS${}_{k^{\prime}}(p)$ formula $\phi(\vec{z})$ distinguishing
$(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{u})$ from
$(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{v})$.

###### Proof.

By Lemma 4.1 the equivalence classes of $\equiv_{\mathrm{MC}_{k}}^{p}$ are
definable in FPS$(p)$ and hence, by the embedding of FPS$(p)$ in infinitary
FOS$(p)$, the statement follows. ∎

Theorem 1.2 readily follows.

###### Proof of Theorem 1.2.

Statement $(1)$ follows directly from the relation between the distinguishing
power of counting logics, polynomial calculus and the invertible map tests
highlighted in Section $3$.

Let $\vec{u},\vec{v}\in V^{k}$ and suppose
$\mathrm{Ax}(\Gamma_{\vec{v}\rightarrow\vec{u}})$ has a $\mathrm{MC}_{k}$
refutation over $\mathbb{Z}_{p}$. By Corollary 4.3 there is a FOS${}_{k}(p)$
formula $\phi(\vec{z})$ distinguishing the structures
$(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{u})$ and
$(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{v})$. Then, by Theorem 3.6,
$\vec{u},\vec{v}$ are in different equivalence classes of
$\mathrm{pr}_{k}[\alpha_{k^{\prime},\Gamma}]^{\mathrm{S}_{k^{\prime}}^{p}}$.
Since
$[\alpha_{k^{\prime},\Gamma}]^{\mathrm{IM}_{k^{\prime}}^{p}}\succeq[\alpha_{k^{\prime},\Gamma}]^{\mathrm{S}_{k^{\prime}}^{p}}$
(by Lemma 3.3), statement $(2)$ is implied. ∎

##  5 Nullstellensatz refutations and $\mathrm{S}_{k}^{p}$-stability

The focus of this section is the proof of the following statement.

######  Lemma 5.1.

Let $\Gamma$ be a graph on $V$ and let $\gamma\in\mathcal{P}(V^{k})$. If for
all $\vec{u},\vec{v}\in V^{k}$, $\gamma(\vec{u})=\gamma(\vec{v})$ if, and only
if, $\vec{u}\equiv_{\mathrm{NC}_{k}}^{p}\vec{v}$, then $\gamma$ is
$\mathrm{S}_{k}^{p}$-stable.

Theorems 1.3 and 1.4 are its direct consequences.

###  5.1 Proof of Lemma 5.1

In what follows, $\gamma\in\mathcal{P}(V^{k})$ satisfies the assumptions of
Lemma 5.1, $\vec{u},\vec{v}\in V^{k}$ and $\vec{\chi}$ and $\vec{\xi}$ are the
$(\vec{i},\vec{u})$ and $(\vec{i},\vec{v})$-character vectors of $\gamma$
respectively, where we may assume without loss of generality that
$\vec{i}=(k,k-1,\ldots,k-2r+1)\in[k]^{(2r)}$, for some $r$ with $2r<k$. For
$\vec{w},\vec{z}\in V^{l}$, denote by $X_{\vec{w}\vec{z}}$ the monomial
$x_{w_{1}z_{1}}x_{w_{2}z_{2}}\ldots x_{w_{l}z_{l}}$ (which need not be
multilinear).

Recall that $\gamma$ is $\mathrm{S}_{k,r}^{p}$-stable, if, and only if, for
every $\vec{u},\vec{v}$ there is some matrix
$T\in\mathfrak{P}_{V^{r}}(\mathbb{Z}_{p})$ such that
$\chi_{\sigma}T=T\xi_{\sigma}$, for all $\sigma\in\mathrm{Im}(\gamma)$. That
is, the following system of equations is solvable in the variables
$T_{\vec{w}\vec{z}}$:

$\sum_{\vec{a}\in
V^{r}}(\chi_{\sigma})_{\vec{w}\vec{a}}T_{\vec{a}\vec{z}}-\sum_{\vec{a}\in
V^{r}}T_{\vec{w}\vec{a}}(\xi_{\sigma})_{\vec{a}\vec{z}}=0\;\;\textrm{for
$\sigma\in\mathrm{Im}(\gamma)$, $\vec{w},\vec{z}\in V^{r}$}$ $\sum_{\vec{a}\in
V^{r}}T_{\vec{w}\vec{a}}-1=0\;\;\textrm{and}\;\;\sum_{\vec{a}\in
V^{r}}T_{\vec{a}\vec{z}}-1=0\;\;\textrm{for $\vec{w},\vec{z}\in V^{r}$},$

where $(\chi_{\sigma})_{\vec{w}\vec{a}}$ is equal to $1$ if
$\gamma(\vec{u}\langle\vec{i},\vec{w}\cdot\vec{a}\rangle)=\sigma$ and $0$
otherwise (similarly for $\xi_{\sigma}$).

We show that there is a $\mathrm{NC}_{k}$ derivation from
$\mathrm{Ax}(\Gamma_{\vec{v}\rightarrow\vec{u}})$ over $\mathbb{Z}_{p}$ of the
following multilinear polynomials (Lemma 5.4):

$\sum_{\vec{a}\mid\gamma(\vec{u}\langle\vec{i},\vec{w}\cdot\vec{a}\rangle)=\sigma}X_{\vec{a}\vec{z}}-\sum_{\vec{a}\mid\gamma(\vec{v}\langle\vec{i},\vec{a}\cdot\vec{z}\rangle)=\sigma}X_{\vec{w}\vec{a}}\;\;\textrm{for
$\sigma\in\mathrm{Im}(\gamma)$, $\vec{w},\vec{z}\in V^{r}$}$ (4)
$\sum_{\vec{a}\in
V^{r}}X_{\vec{w}\vec{a}}-1\;\;\textrm{and}\;\;\sum_{\vec{a}\in
V^{r}}X_{\vec{a}\vec{z}}-1\;\;\textrm{for $\vec{w},\vec{z}\in V^{r}$}.$ (5)

We may view each monomial (apart from the constant term) as a distinct linear
variable, so that all of the above are linear polynomials. Since
$\gamma(\vec{u})=\gamma(\vec{v})$, there is no $\mathrm{NC}_{k}$ refutation of
$\mathrm{Ax}(\Gamma_{\vec{v}\rightarrow\vec{u}})$ and hence, no linear
combination of 4 and 5 gives the constant polynomial $1$. It follows that if
viewed as linear polynomials, 4 and 5 have a common root, thus showing Lemma
5.1.

######  Lemma 5.2.

If
$\gamma(\vec{u}\langle\vec{i},\vec{w}\cdot\vec{z}\rangle)\neq\gamma(\vec{v}\langle\vec{i},\vec{w}^{\prime}\cdot\vec{z^{\prime}}\rangle)$,
then there is a $\mathrm{NC}_{k}$ derivation over $\mathbb{Z}_{p}$ from
$\mathrm{Ax}(\Gamma_{\vec{v}\rightarrow\vec{u}})$ of
$X_{\vec{w}\vec{w}^{\prime}}X_{\vec{z}\vec{z}^{\prime}}$.

###### Proof.

Set $Y=X_{\vec{w}\vec{w}^{\prime}}X_{\vec{z}\vec{z}^{\prime}}$ and let
$X_{\vec{u}^{\prime}\vec{v}^{\prime}}$ be the degree $k-2r$ monomial where
$u^{\prime}_{j}=u_{j}$ and $v^{\prime}_{j}=v_{j}$ for $j\in[k-2r]$. Then,
there is a $\mathrm{NC}_{k}$ derivation of
$Y(X_{\vec{u}^{\prime}\vec{v}^{\prime}}-1)$, for indeed

$Y(X_{\vec{u}^{\prime}\vec{v}^{\prime}}-1)=Y(x_{u_{1}v_{1}}-1)+Yx_{u_{1}v_{1}}(x_{u_{2}v_{2}}-1)+\ldots+Y(x_{u_{1}v_{1}}\ldots
x_{u_{k-2r-1}v_{k-2r-1}})(x_{u_{k-2r}v_{k-2r}}-1).$

By assumption,
$\gamma(\vec{u}\langle\vec{i},\vec{w}\cdot\vec{z}\rangle)\neq\gamma(\vec{v}\langle\vec{i},\vec{w}^{\prime}\cdot\vec{z^{\prime}}\rangle)$
and hence, there is an $\mathrm{NC}_{k}$ derivation of
$YX_{\vec{u}^{\prime}\vec{v}^{\prime}}$. Subtracting the latter from
$Y(X_{\vec{u}^{\prime}\vec{v}^{\prime}}-1)$ yields the desired statement. ∎

######  Lemma 5.3.

For any $\vec{w},\vec{z}\in V^{r}$ and $\vec{s}\in V^{t}$ there is a
$\mathrm{NC}_{t+r}$ derivation over $\mathbb{Z}_{p}$ from
$\mathrm{Ax}(\Gamma_{\vec{v}\rightarrow\vec{u}})$ of

$X_{\vec{w}\vec{z}}\big{(}\sum_{\vec{a}\in
V^{t}}X_{\vec{s}\vec{a}}-1\big{)}\;\;\textrm{and}\;\;X_{\vec{w}\vec{z}}\big{(}\sum_{\vec{a}\in
V^{t}}X_{\vec{a}\vec{s}}-1\big{)}.$

###### Proof.

We proceed by induction on $t$. For $t=1$,
$X_{\vec{w}\vec{z}}\big{(}\sum_{a\in V}x_{sa}-1\big{)}$ is the product of a
monomial and an axiom, so has a $\mathrm{NC}_{r+1}$ derivation.

Assume $X_{\vec{w}\vec{z}}\big{(}\sum_{\vec{a}\in
V^{t}}X_{\vec{s}\vec{a}}-1\big{)}$ has a $\mathrm{NC}_{t+r}$ derivation. It
can be easily verified that if a polynomial $f$ has a $\mathrm{NC}_{r}$
derivation from some set of axioms, then $xf$ has a $\mathrm{NC}_{r+1}$
derivation for any variable $x$. Thus,
$x_{s^{\prime}a^{\prime}}X_{\vec{w}\vec{z}}\big{(}\sum_{\vec{a}\in
V^{t}}X_{\vec{s}\vec{a}}-1\big{)}$ has a $\mathrm{NC}_{t+r+1}$ derivation.
Finally

$\sum_{a^{\prime}\in
V}x_{s^{\prime}a^{\prime}}X_{\vec{w}\vec{z}}\big{(}\sum_{\vec{a}\in
V^{t}}X_{\vec{s}\vec{a}}-1\big{)}=X_{\vec{w}\vec{z}}\big{(}\sum_{\vec{a}\in
V^{t},a^{\prime}\in V}X_{(\vec{s}\cdot s^{\prime})(\vec{a}\cdot
a^{\prime})}-1\big{)}=X_{\vec{w}\vec{z}}\big{(}\sum_{\vec{a}\in
V^{t+1}}X_{(\vec{s}\cdot s^{\prime})\vec{a}}-1\big{)}$

as required. ∎

######  Lemma 5.4.

There is a $\mathrm{NC}_{k}$ derivation over $\mathbb{Z}_{p}$ from
$\mathrm{Ax}(\Gamma_{\vec{v}\rightarrow\vec{u}})$ of the polynomials in
formulae (4) and (5).

###### Proof.

For $\vec{a}\in V^{r}$, set $\mathcal{N}(\vec{u},\vec{w})=\\{\vec{a}\in
V^{r}\mid\gamma(\vec{u}\langle\vec{i},\vec{w}\cdot\vec{a}\rangle)=\sigma\\}$
and $\mathcal{N}(\vec{v},\vec{z})=\\{\vec{a}\in
V^{r}\mid\gamma(\vec{v}\langle\vec{i},\vec{a}\cdot\vec{z}\rangle)=\sigma\\}$
(note the slight asymmetry). By Lemma 5.3, there is a $\mathrm{NC}_{2r}$ (and
hence, $\mathrm{NC}_{k}$, since $2r<k$) derivation of

$X_{\vec{a}\vec{z}}\big{(}\sum_{\vec{a}^{\prime}\in
V^{r}}X_{\vec{s}\vec{a}^{\prime}}-1\big{)}$

for every $\vec{a},\vec{s},\vec{z}\in V^{r}$. By subtracting from the above
all monomials $X_{\vec{a}\vec{z}}X_{\vec{s}\vec{a}^{\prime}}$ for which
$\vec{a}^{\prime}\notin\mathcal{N}(\vec{v},\vec{z})$ (which have a
$\mathrm{NC}_{k}$ derivation by Lemma 5.2) one gets

$X_{\vec{a}\vec{z}}\big{(}\sum_{\vec{a}^{\prime}\in\mathcal{N}(\vec{v},\vec{z})}X_{\vec{s}\vec{a}^{\prime}}-1\big{)}.$

Adding these for all $\vec{a}\in\mathcal{N}(\vec{u},\vec{w})$ yields

$\sum_{\vec{a}\in\mathcal{N}(\vec{u},\vec{w})}X_{\vec{a}\vec{z}}\big{(}\sum_{\vec{a}^{\prime}\in\mathcal{N}(\vec{v},\vec{z})}X_{\vec{s}\vec{a}^{\prime}}-1\big{)}.$
(6)

A similar argument shows that there is a $\mathrm{NC}_{k}$ derivation of

$\sum_{\vec{a}\in\mathcal{N}(\vec{v},\vec{z})}X_{\vec{w}\vec{a}}\big{(}\sum_{\vec{a}^{\prime}\in\mathcal{N}(\vec{u},\vec{w})}X_{\vec{a}^{\prime}\vec{s}}-1\big{)}.$
(7)

Subtracting (6) from (7) yields (4).

The polynomials in (5) can be derived by setting $r=0$ in Lemma 5.3. ∎

###### Proof of Theorem 1.3.

If $\mathbb{F}=\mathbb{Q}$, and $X_{\vec{u}\vec{v}}$ has a $\mathrm{PC}_{k}$
derivation over $\mathbb{Q}$ from $\mathrm{Ax}(\Gamma)$, there is some
$k^{\prime}\in\mathbb{N}$ and a $\mathcal{C}_{k^{\prime}}$ formula
distinguishing $(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{u})$ from
$(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{v})$ by Theorem 6.6 in [GGPP19]. By
Corollary 3.5, $\vec{u}$ and $\vec{v}$ are distinguished by
$[\alpha_{k^{\prime}+1,\Gamma}]^{\mathrm{S}_{k^{\prime}+1}^{0}}$. It follows
from Theorem 3.6 and Lemma 5.1 that there is a $\mathrm{NC}_{k^{\prime}+2}$
derivation over $\mathbb{Q}$ from $\mathrm{Ax}(\Gamma)$ of
$X_{\vec{u}\vec{v}}$, as required by statement $(1)$.

If $\mathbb{F}=\mathbb{Z}_{p}$ and $X_{\vec{u}\vec{v}}$ has a
$\mathrm{MC}_{k}$ derivation over $\mathbb{Z}_{p}$ from $\mathrm{Ax}(\Gamma)$,
there is some $k^{\prime}$ and an $\mathrm{FOS}_{k^{\prime}}(p)$ formula
distinguishing $(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{u})$ from
$(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{v})$ (Lemma 4.1). Theorem 3.6 and
Lemma 5.1 imply that there is a $\mathrm{NC}_{k^{\prime}+1}$ derivation over
$\mathbb{Z}_{p}$ from $\mathrm{Ax}(\Gamma)$ of $X_{\vec{u}\vec{v}}$, thus
showing statement (2). ∎

###  5.2 Generalized Cai-Fürer-Immerman constructions

In 1992, Cai, Fürer and Immerman provided, for $k\geq 1$, a family of pairs of
non-isomorphic graphs $(\mathcal{G}_{k},\mathcal{H}_{k})$ which cannot be
distinguished by $\mathcal{C}_{k}$-formulae. Furthermore, the construction of
such graphs ensures that $\mathcal{G}_{k}$ and $\mathcal{H}_{k}$ only have
$O(k)$ vertices and require $\mathcal{C}$-formulae with $\Omega(k)$ variables
in order to be distinguished, thus showing an optimal lower bound (up to
constant factors) on the number of variables required to define such
structures in the logic.

It is known, however, that $\mathcal{G}_{k}$ and $\mathcal{H}_{k}$ can be
distinguished in poly($k$)-time. On the one hand, the construction ensures
that both graphs, for any $k$, are $3$-regular, and isomorphism of graphs with
bounded valency can be decided in polynomial time (see [Luk82]).
Alternatively, the isomorphism problem between $\mathcal{G}_{k}$ and
$\mathcal{H}_{k}$ really encodes a system of linear equations over
$\mathbb{Z}_{2}$, the solvability of which can be decided in polynomial time.

These structures can be generalized to encode a systems of linear equations
over an arbitrary finite field (or, indeed, an arbitrary finite Abelian group
[Hol10]). Loosely speaking, the _generalized Cai-Fürer-Immerman_ construction
for the field $\mathbb{Z}_{p}$ provides, for each $k\in\mathbb{N}$, $p$ non-
isomorphic $3$-regular graphs
$\mathcal{G}_{k}^{(1)},\ldots,\mathcal{G}_{k}^{(p)}$. These delimit the power
of well known linear algebra based polynomial-time approximations of graph
isomorphism, as can be seen in the following known results, which we have
paraphrased in terms of the equivalent problem of computing the orbits of the
induced action of the automorphism group. Let $\Gamma_{k,p}$ be the disjoint
union of the graphs $\mathcal{G}_{k}^{(1)},\ldots,\mathcal{G}_{k}^{(p)}$ and
let $V$ denote its vertex set.

######  Theorem 5.5 (Theorems 8.1 and 8.2 in [DGP19]).

If $\Gamma=\Gamma_{k,p}$ and $q\neq p$, then the equivalence classes of
$[\alpha_{k,\Gamma}]^{\mathrm{IM}_{k}^{q}}$ do not coincide with those of the
$k$-orbit partition for $\Gamma$. If $q=p$, the equivalence classes of
$[\alpha_{3,\Gamma}]^{\mathrm{IM}_{3}^{q}}$ coincide with those of the
$3$-orbit partition for $\Gamma$.

The next statement can be deduced from the proof of Theorems 6.1 and 6.2 in
[GGPP19].

######  Theorem 5.6.

The equivalence classes of $\equiv_{\mathrm{PC}_{k}}^{p}$ on $V^{k}$ do not
coincide with those of the $k$-orbit partition for $\Gamma_{k,q}$ if $q\neq
p$.

Originally, the generalized Cai-Fürer-Immerman constructions were introduced
to delimit the expressive power of the extension of fixed point logics with
rank operators over a finite field FPR$(p)$ and, correspondingly, the
distinguishing power of the extension of first order logic by said operators,
FOR$(p)$ (see Chapter 7 of [Hol10]). The distinguishing power of the
invertible map test in characteristic $p$ is at least that of FOR$(p)$, so in
one direction Theorem 5.5 provides a lower bound for this logic. In the other
direction, we can show that the orbit partition on $\Gamma_{k,p}$ can already
be defined in FPR$(p)$. Indeed, it can be defined in the apparently weaker
logic FPS$(p)$, giving the following result.

######  Theorem 5.7.

Let $\Gamma=\Gamma_{k,p}$. If $p\neq q$, there exist $\vec{u},\vec{v}\in
V^{k}$ in different equivalence classes of the $k$-orbit partition of
$\Gamma$, such that there are no FOS${}_{k}(q)$-formulae distinguishing
$(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{u})$ from
$(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{v})$. If $q=p$ and
$\vec{u},\vec{v}\in V^{2}$, then
$(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{u})$ is distinguished from
$(\mathfrak{A}_{\Gamma},\vec{z}\mapsto\vec{v})$ by some FOS${}_{2}(q)$-formula
if, and only if, $\vec{u},\vec{v}$ are in different equivalence classes of the
$2$-orbit partition of $\Gamma$.

This allows us to show Theorem 1.4.

###### Proof of Theorem 1.4.

Let $\Gamma=\Gamma_{k,p}$ and $\vec{u},\vec{v}$ be as in the statement of the
Theorem. By Theorem 5.7 and Theorem 3.6, $\vec{u}$ and $\vec{v}$ belong to
different equivalence classes of $[\alpha_{3,\Gamma}]^{\mathrm{S}_{3}^{p}}$.
By Lemma 5.1 $\vec{u}\not\equiv_{\mathrm{NC}_{3}}^{p}\vec{v}$ as required. ∎

Theorem 1.4 generalizes Theorem 6.3 in [BG15] to aribitrary positive
characteristic. Combined with Theorem 5.6, it also shows that bounded degree
$\mathrm{PC},\mathrm{MC}$ and $\mathrm{NC}$ refutations have a similar
distinguishing power as the invertible map tests on the class of generalized
Cai-Fürer-Immerman constructions.

##  6 Conclusions: where does polynomial calculus lie?

The invertible map tests can be thought of a family of algorithms, each of
which distinguishes tuples of vertices of graphs according to the most general
linear algebraic invariants expressible with a bounded number of variables in
a logic. As bounded degree $\mathrm{PC},\mathrm{MC}$ and $\mathrm{NC}$
refutations can be decided solely by using basic field operations, one expects
that the equivalences defined by the invertible map tests simulate those
defined by the abovementioned proof systems. Theorem 1.2 gives a partial proof
of this conjecture, leaving it open as to whether the invertible map tests can
simulate bounded degree $\mathrm{PC}$ refutations, when taken over some finite
field.

Our approach to this question was to attempt to define the above proof systems
in the simplest logics which could express the solvability of systems of
linear equations. The proof of Lemma 4.1 hints at the flaws of this choice.
Deciding whether or not there is a $\mathrm{PC}_{k}$ refutation of
$P\subseteq\mathbb{F}[x_{1},\ldots,x_{r}]$ can be understood as the following
procedure, similar to that in Section 4.2.

  1. INPUT.

$P\subset\mathbb{F}[x_{1},\ldots,x_{r}]$

  2. OUTPUT.

REFUTE or NOREFUTE.

  3. 1.

Initialize $\mathcal{S}=\\{X_{A}f\mid f\in P,\mathrm{deg}(X_{A}f)\leq k\\}$.

  4. 2.

while $\mathrm{span}_{\mathbb{F}}\mathcal{S}$ has changed since last round or
$1\notin\mathrm{span}_{\mathbb{F}}\mathcal{S}$ do lines 3-4

  5. 3.

Find a set $\mathcal{B}$ generating the $\mathbb{F}$-space
$\\{f\in\mathrm{span}_{\mathbb{F}}\mathcal{S}\mid\mathrm{deg}(f)<k\\}$.

  6. 4.

$\mathcal{S}\leftarrow\mathcal{S}\cup\\{X_{A}f\mid
f\in\mathcal{B},\mathrm{deg}(X_{A}f)\leq k\\}$.

  7. 5.

If $1\in\mathrm{span}_{\mathbb{F}}\mathcal{S}$ output REFUTE

  8. 6.

else output NOREFUTE.

This procedure runs in polynomial time, as one can find $\mathcal{B}$ by using
Gaussian elimination (there is no need to store the set
$\mathrm{span}_{\mathbb{F}}\mathcal{S}$ as a generating set suffices), and the
number of iterations of the while loop is bounded by the number of monomials
of degree at most $k$ in the variables $\\{x_{1},\ldots,x_{r}\\}$. If
$\mathbb{F}$ is finite, this procedure is a priori _not_ definable in
FPS$(p)$, as it is not immediate whether there is a canonical choice for the
set $\mathcal{B}$ (its counterpart in the procedure for monomial calculus
refutations was the set $\mathcal{M}$ of monomials in the span of
$\mathcal{S}$). Put otherwise, defining the set $\mathcal{B}$ requires
defining the solution space of a system of linear equations over a field of
positive characteristic $p$, rather than just determining the solvability of
the system and this cannot be done in FPS$(p)$.666One can use the extended
Cai-Fürer-Immerman constructions to explain this. The FPC definability of
bounded degree polynomial calculus refutations over the field $\mathbb{Q}$
(Theorem 4.9 in [GGPP19]) relies in fact on the FPC definability of solution
spaces of linear equations over $\mathbb{Q}$ (Theorem 4.11 in [GGPP19]). It is
important to note, however, that we are only concerned with axioms of the form
$\mathrm{Ax}(\Gamma_{\vec{u}\rightarrow\vec{v}})$, and such a restriction
could potentially allow a canonical choice of $\mathcal{B}$.

Let us view the problem from the viewpoint of proof complexity. It follows
from Lemma 5.1, that if $\mathrm{PC}_{k}$ refutations over $\mathbb{Z}_{p}$
are definable in FPS$(p)$, then for every $k$, there is some $k^{\prime}$ such
that if $\mathrm{Ax}(\Gamma_{\vec{u}\rightarrow\vec{v}})$ has a
$\mathrm{PC}_{k}$ refutation over $\mathbb{Z}_{p}$, then it has a
$\mathrm{NC}_{k^{\prime}}$ refutation over $\mathbb{Z}_{p}$. It is known that
for all $n$ and for any field, there is a set of axioms on $n(n+1)$ variables
which can be refuted by $\mathrm{PC}_{3}$ but require degree $o(n)$ to be
refuted by $\mathrm{NC}$ (Theorem $6$ in [Bus98]). Furthermore, this lower
bound can be shown to be optimal. On the other hand, Buss et. al. have shown
that $\mathrm{NC}$ derivations can be used to simulate _tree-like_
$\mathrm{PC}$ derivations (see Theorems 5.3 and 5.4 in [BIK+97]) with only a
small increase in degree. For a set of axioms of the form
$\mathrm{Ax}(\Gamma_{\vec{u}\rightarrow\vec{v}})$, it is not known if any
$\mathrm{PC}_{k}$ refutation of such can be converted into a tree-like
refutation without incurring in an unbounded increase in degree.

Finally, let us justify our conjecture; namely, that for any field, the
equivalences on tuples of vertices of graphs defined by the invertible map
tests simulate those defined by bounded degree $\mathrm{PC}$ refutations.
First, Theorems 5.5, 5.6 and 1.4 show that the invertible map tests and
bounded degree $\mathrm{PC}$ refutations have a similar distinguishing power
on the class of generalized Cai-Fürer-Immerman graphs, thus suggesting that
there should be a tight connection between them. Moreover, the procedure we
have described above for deciding $\mathrm{PC}_{k}$ refutations of a set of
polynomials is _linear algebraic invariant_ in the sense that after each
iteration of the while loop, the $\mathbb{F}$-span of $\mathcal{S}$ is
independent of the choice of the set $\mathcal{B}$. This seems to be a strong
hint at the fact that extending fixed-point logic with a quantifier over some
linear algebraic operator over $\mathbb{Z}_{p}$ should suffice to define
$\mathrm{PC}_{k}$ refutations over the same field.

#### Acknowledgements.

We are grateful to Martin Grohe, Benedikt Pago and Gregory Wilsenach for many
helpful discussions and suggestions.

## References

  * [ABD09] A. Atserias, A. Bulatov, and A. Dawar.  Affine systems of equations and counting infinitary logic.  Theoretical Computer Science, 410(18):1666 – 1683, 2009.  Automata, Languages and Programming (ICALP 2007).
  * [Bab16] L. Babai.  Graph isomorphism in quasipolynomial time [extended abstract].  In Proc. 48th Annual ACM SIGACT Symp. Theory of Computing, STOC, pages 684–697, 2016.
  * [BG15] C. Berkholz and M. Grohe.  Limitations of algebraic approaches to graph isomorphism testing.  CoRR, abs/1502.05912, 2015.
  * [BIK+94] P. Beame, R. Impagliazzo, J. Krajicek, T. Pitassi, and P. Pudlak.  Lower bounds on Hilbert’s Nullstellensatz and propositional proofs.  volume 73, pages 794–806, 1994.
  * [BIK+97] Samuel Buss, Russell Impagliazzo, Jan Krajícek, Pavel Pudlak, Alexander Razborov, and Jiri Sgall.  Proof complexity in algebraic systems and bounded depth Frege systems with modular counting.  Computational Complexity, 6:256–298, 01 1997.
  * [Bus98] Samuel R. Buss.  Lower bounds on Nullstellensatz proofs via designs.  In in Proof Complexity and Feasible Arithmetics, P. Beame and S. Buss, eds., American Mathematical Society, pages 59–71. American Math. Soc, 1998\.
  * [CEI00] M. Clegg, J. Edmonds, and R. Impagliazzo.  Using the Gröbner basis algorithm to find proofs of unsatisfiability.  Proceedings of STOC’96, 03 2000.
  * [CFI92] J. Y. Cai, M. Fürer, and N. Immerman.  An optimal lower bound on the number of variables for graph identification.  Combinatorica, 12(4):389–410, 1992.
  * [Daw15] A. Dawar.  The nature and power of fixed-point logic with counting.  ACM SIGLOG News, 2:8–21, 2015.
  * [DGH+12] Anuj Dawar, Erich Graedel, Bjarki Holm, Eryk Kopczyński, and Wied Pakusa.  Definability of linear equation systems over groups and rings.  Logical Methods in Computer Science, 9, 04 2012.
  * [DGP19] A. Dawar, E. Grädel, and W. Pakusa.  Approximations of isomorphism and logics with linear algebraic operators.  In 46th International Colloquium on Automata, Languages, and Programming, ICALP, pages 112:1–112:14, 2019.
  * [DH12] A. Dawar and B. Holm.  Pebble games with algebraic rules.  In Artur Czumaj, Kurt Mehlhorn, Andrew Pitts, and Roger Wattenhofer, editors, Automata, Languages, and Programming, pages 251–262, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg.
  * [dSP09] C. de Seguins Pazzis.  Invariance of simultaneous similarity and equivalence of matrices under extension of the ground field.  Linear Algebra and its Applications, 433, 02 2009.
  * [DV20] A. Dawar and D. Vagnozzi.  Generalizations of $k$-Weisfeiler-Leman stabilization.  Moscow Journal of Number Theory and Combinatorics, 2020.
  * [EF99] H-D. Ebbinghaus and J. Flum.  Finite Model Theory.  Springer, 2nd edition, 1999.
  * [EFT94] H. Ebbinghaus, J. Flum, and W. Thomas.  Mathematical Logic.  1994\.
  * [GGPP19] E. Grädel, M. Grohe, B. Pago, and W. Pakusa.  A finite-model-theoretic view on propositional proof complexity.  Logical Methods in Computer Science, 15(1), 2019.
  * [Hol10] B. Holm.  Descriptive Complexity of Linear Algebra.  PhD thesis, University of Cambridge, 2010.
  * [Lib04] L. Libkin.  Elements of Finite Model Theory.  01 2004.
  * [Luk82] Eugene Luks.  Isomorphism of graphs of bounded valence can be tested in polynomial time.  Journal of Computer and System Sciences, 25(1):42 – 65, 1982.
  * [Mat79] R. Mathon.  A note on the graph isomorphism counting problem.  Information Processing Letters, 8:131–136, 1979.
  * [Tin86] G. Tinhofer.  Graph isomorphism and theorems of Birkhoff type.  Computing, 36:285–300, 1986.