In particular, there is $\ell \geq 1$ such that the classes
$\CFIclass{\mcF}{p}$ are
$\cyclp$ for all $p \in \Primes$.

We already analysed the automorphism groups of CFI-structures
$\mfA \in \CFIclass{\mcF}{p}$ in Section <ref>. In
particular, we saw that these groups are elementary Abelian $p$-groups, so
property <ref> holds for CFI-structures in
Moreover, Corollary <ref> tells us that classes of
CFI-structures are homogeneous.

Now, let $\ell \geq 1$ and let $\mfA$ be $\ell$-homogeneous with
automorphism group $\Gamma$.
Then, by Theorem <ref>, we know that for every $k \geq
1, r \geq 0$ the formula $\Typk{\ell \cdot (r+k)}{(r+k)}(\tup x_1 \tup
\tup y_1 \tup y_2)$ defines in $\mfA$ a total preorder on $A^{r+k}$ which
order $(r +k)$-tuples up to $\Gamma$-orbits.

\[\Typk{\ell \cdot (r+k)}{k}[\tup z](\tup x, \tup y) = \Typk{\ell \cdot
(r+k)}{(r+k)}(\tup z \tup x, \tup z \tup y),\]

we know that for every $\tup c \in A^r$ it holds that the total preorder
$\Typk{\ell \cdot (r+k)}{k}[\tup c]$ distinguishes $k$-tuples $\tup a,
\tup b \in A^k$ if, and only if, $\Gamma(\tup c \tup a) \neq \Gamma(\tup c
\tup b)$. But this last condition is indeed equivalent to
$\Gamma_{\tup c}(\tup a) \neq \Gamma_{\tup c}(\tup b)$, which completes
the proof.

Our next aim is to show that the class of $\cyclp$ structures is
closed under $\FPC$-transformations.
Unfortunately, stated in this very general form, this claim is clearly wrong.
example, $\FPC$-transformations can easily generate each fixed finite
structure (starting from any structure), and so the resulting structures
will not have Abelian automorphism groups for instance (which is one of
the requirements for being ). However, as we
will show next, one can extend each -interpretation $\mcI$ to
an $\FPC$-interpretation $\Norm(\mcI)$ in such a way that the original
input structure is preserved as a
substructure. This will enable us to maintain the property of being .

Let us be a bit more precise. As said, instead of only interpreting
$\mcI(\mfA)$ in $\mfA$ we want to
interpret the structure $\Norm(\mcI)(\mfA) = \mcI(\mfA) \uplus \mfA$ in
$\mfA$, that is the disjoint union of the original structure $\mfA$ and the
interpreted structure $\mcI(\mfA)$. However, as such, this is not sufficient
since we can
still get new automorphisms due to the new substructure $\mcI(\mfA)$.
To overcome this problem, we create additional relations that
indicate from which elements in
$\mfA$ the newly created elements in $\mcI(\mfA)$ originate. Note that the
elements in $\mcI(\mfA)$  are equivalence classes of tuples of elements
from $\mfA$ and we will encode this information in $\Norm(\mcI)(\mfA)$.
Formally, our result is as follows.

Let $\mcI(\tup z) \in \FPC[\sigma \to \tau, \tup z]$ be an
$\FPC$-interpretation of dimension $d$ and with $r \geq 0$ parameters
$\tup z$, $| \tup z | = r$, that
maps $\sigma$-structures to $\tau$-structures.
Let $\hat \tau = \sigma \uplus \tau \uplus \{ \in \}$ (where $\in$ is a
fresh binary relation symbol).
Then there exists an $\FPC$-interpretation $\mcJ(\tup z)  \in
\FPC[\sigma \to \hat \tau, \tup z]$ such that for every structure $\mfA$
and every $\tup a \in \dom(\mfA, \tup z)$ the following holds
for $\mfB = \mcI(\mfA, \tup a)$ and $\mfC = \mcJ(\mfA, \tup a)$:

* the dimension of $\mcJ(\tup z)$ is at most $d+3$, and

* $\mfB \subseteq_{\FO} \mfC|_{\tau}$, that is $\mfB$ is an
$\FO$-definable substructure of the reduct of $\mfC$
to $\tau$, and

* if $\Gamma = \Aut(\mfA, \tup a)$ and $\Delta = \Aut(\mfC)$, then
$\Gamma \cong \Delta$ (that is, up to isomorphism, the automorphism group
of the input structure $(\mfA, \tup a)$ is preserved), and

* if $\mfA$ is $\ell$-homogeneous (for $\ell \geq 3$), then the
structure $\mfC$ is
$\ell \cdot (d+r)$-homogeneous.

Let $\mcI(\tup z)$ be $d$-dimensional with domain formula
$\lintdom{\phi}(\tup x, \tup z)$ and congruence formula
$\lintcong{\phi}(\tup x_1, \tup x_2, \tup z)$.
Let $\mfA$ be a $\sigma$-structure and let $\tup a \in \dom(\mfA, \tup z)$.
The elements of the interpreted structure $\mfB = \mcI(\mfA, \tup a)$ are
equivalence classes of tuples in $\dom(\mfA, \tup x)$.
The idea of the construction of $\mfC$ is as follows.
The universe of $\mfC$ consists of four different sorts $U_A, U_T, U_B,
The first sort $U_A$ contains elements that represent the elements in the
universe of the original structure $\mfA$.
The second sort contains elements to represent all elements in
$\dom(\mfA, \tup x)$ that are selected by $\lintdom{\phi}$ and,
furthermore, a unique element that is used in order to encode the
parameter tuple $\tup a$. Also $U_T$ contains auxiliary elements to encode
the structure of tuples, that is the individual entries.
The third sort $U_B$ contains elements to represent the elements
of the structure $\mfB$, that is the equivalence classes $[\tup b] = \{
\tup c \in \dom(\mfA, \tup x) : \mfA \models \lintdom{\phi}(\tup c, \tup
\wedge \lintcong{\phi}(\tup b, \tup c, \tup a)\}$ for $\tup b \in
\dom(\mfA, \tup x)$ with $\mfA \models \lintdom{\phi}(\tup b, \tup a)$.
The last sort $U_N$ is an auxiliary sort which holds a sufficient amount
of numbers (that is a linearly ordered set) to represent the different
sorts, their relations, the indices for tuples, and so on.
The binary relation symbol $\in$ is used to relate the different sorts and
to encode the tuple structure. Relations in $\sigma$ and $\tau$ are
interpreted on the respective sorts $U_A$ and $U_B$ as in $\mfA$ and
$\mfB$, respectively.

Let us elaborate more on some technical details (we remark that, as
usual, there are many different ways to formalise an appropriate encoding;
in order to verify the properties of $\mcJ$, we describe one of them).
First of all, we extend the dimension of $\mcI$ by three additional
components $(\mu, \nu, x)$ where the first two variables $\mu, \nu$ range
over the number sort and where $x$ ranges over the vertex sort (we
remark that it would be sufficient to increase the dimension by at most
one numeric component, but this would unnecessarily make the following
description more complicated).
In general, we will use the first component $\mu$ to address different
sorts. For instance, let us start with the number sort $U_N$. We can use
congruence formula to merge all tuples $(0, \mu, d, \tup b)$ and
$(0, \mu, d', \tup c)$ (for $d,d' \in A$ and $\tup b, \tup c \in
\dom(\mfA,
\tup x)$) and then use the resulting set $\{ (0, 0, \star), (0,1, \star),
(0, 2, \star), \dots \}$ to encode the elements in $U_N$. Hereby, we
choose the
range of the numeric variable $\nu$ larger than the range of any other
numeric variable which occurs in the interpretation $\mcI$.
To identify the numeric sort $U_N$ in the resulting structure we define a
linear order on $U_N$ using the new relation symbol $\in$.
As a second step, we encode elements $a \in A$ of the original
$\mfA$ in $\mfC$ by using elements of the form $(1, \star, a, \star)$ (as
before, the $\star$'s
in this notation indicate that we use the congruence formula to merge all
elements with different $\star$-components).
To identify the first sort $U_A$ in the resulting structure $\mfC$, we
draw an
$\in$-edge from the first element in the number sort $U_N$ to all elements
the first sort $U_A$.
Of course, we define all the relation symbols in $\sigma$ on $U_A$ by
copying their definition from $\mfA$.

Thirdly, to encode the elements in $\dom(\mfA, \tup x)$ and the parameter
$\tup a$ we proceed in two steps.
First of all, for every index $1 \leq i \leq \max(k,r)$, we introduce
component elements $(i, a)$, $a \in A$, and
$(i, m)$, $m < \dom(\nu)$, to represent all possible components of
tuples in $\dom(\mfA, \tup x)$.
Formally, we encode them in $\mfC$ by using elements of the form
$(2+i,\star,a,\star)$ and $(2+i,m,\star)$.
To identify them in $\mfC$, we mark them in a similar way as
before, i.e. we introduce $\in$-edges from position $2+i$ in the number
sort to all component elements $(i, a)$ and $(i,m)$. We also connect
all component elements $(i,a)$ and $(i,m)$ to their respective values
$a$ and $m$ via $\in$-edges (which point from component elements to the
sorts $U_A$ and $U_N$).
We proceed to represent all tuples in $\dom(\mfA, \tup x)$
using the original components of the interpretation $\mcI$, that is we use
elements $(2+\max(k,r)+1, \star, \star, \tup b)$ where $\tup b \in
\dom(\mfA, \tup x)$
and mark them appropriately.
We additionally connect tuples $(2+\max(k,r)+1, \star, \star, \tup b)$
with their
matching component elements, that is with $(i, b_i)$. We then use
$\lintdom{\phi}$ to select those
tuples in $\dom(\mfA, \tup x)$ that are in the domain of $\mcI$.
Also, we add one further special tuple element, say encoded as
$(2+\max(k,r)+1,0, \star)$, which is meant to encode the parameter tuple
$\tup a$. This
special element is thus connected to all component elements $(i,a_i)$.
Finally, we make an additional copy of all tuple elements $(2+\max(k,r)+2,
\star,
\star, \tup b)$ that we added, and use $\lintdom{\phi}$ to merge them
according to $\mcI$. This will give us the sort of elements $U_B$
that we use in order to represent the elements of $\mfB$. We mark them
appropriately in the same way as we did for the other sorts.
Recall that these elements are equivalence classes of elements in
$\dom(\mfA, \tup x)$, hence we additionally connect them, with
$\in$-edges, to their representatives in the tuple sort $U_T$.
We define the relations in $\tau$ on $U_B$ according to $\mcI$, that is
we copy them from $\mfB = \mcI(\mfA, \tup a)$.

From this description it is easy to see that all of the
required transformations can be expressed by an $\FPC$-interpretation
with dimension at most $d + 3$ (and while we increase the number of
variables by a constant number only).
Also, it should be clear that item <ref> holds as we can
very easily define the different sorts in the resulting structure $\mfC$
(in particular, the sort $U_B$ is the maximal sort according to
our linear order on $U_N$).
Let us now consider item <ref>.
The main observation is that each automorphism $\pi \in \Delta$ of $\mfC$
is uniquely defined by its projection on the sort $U_A$.
Indeed, this directly follows from the way in which we constructed $\mfC$
using the
new relation symbol $\in$. First note that no automorphism of $\mfC$ can
elements in the numeric sort $U_N$, since $\in$ defines a linear order on
$U_N$. In particular it follows that all sorts $U_N, U_A, U_B, U_T$ are
preserved. Secondly, assume that we have a permutation $\pi$ on $U_A$ that
can be
extended to an automorphism of $\mfC$. Since the $\sigma$-relations on
$U_A$ in $\mfC$ coincide with the relations in $\mfA$, we know
that $\pi$ is an automorphism of $\mfA$.
Moreover, to obtain an automorphism of $\mfC$, there is only one unique
way in which we can extend $\pi$ to the tuple sort $U_T$ and the sort
$U_B$ encoding the universe of $\mfB$.
Indeed, the $\in$-edges enforce that tuple components $(i,a)$ are moved
to $(i, \pi(a))$ (and tuple components $(i,m)$ cannot be moved) and,
accordingly, that tuples $\tup b$ in $U_T$ are moved
to $\pi(\tup b)$. In particular, for the special tuple $\tup a$ this
means that we have $\pi(\tup a) = \tup a$.
Finally, since $\pi$ extends uniquely to the tuple sort $U_T$, it also
uniquely extends to the sort $U_B$ of elements of the interpreted
structure $\mfB = \mcI(\mfA, \tup a)$. Indeed, the elements in $U_B$ are
sets $[\tup b]$ of tuples $\tup b \in U_T$, and we have connected these
sets with the elements they contain using $\in$-edges in $\mfC$. Hence,
for each
equivalence class $[\tup b] \in U_B$ for $\tup b \in U_T$ we have
$\pi([\tup b]) = [ \pi(\tup b) ]$.
So altogether, we can conclude that the extension of $\pi$ from $U_A$ to
the other sorts $U_N, U_T, U_B$ is unique. On the other hand, note that if
$\pi$ is an automorphism of $\mfA$ satisfying
$\pi(\tup a) = \tup a$, then the resulting extended $\pi$ is indeed an
automorphism of
$\mfC$. To see this, note that all relations in $\tau$ and
$\sigma$ are preserved under automorphisms of $(\mfA, \tup a)$: for the
$\sigma$-relations this follows from the
assumption that $\pi$ is an automorphism of $\mfA$, and for the
$\tau$-relation it follows from the fact that they are defined by the
$\FPC$-interpretation $\mcI$ in $(\mfA, \tup a)$.
This shows that $\Aut(\mfA, \tup a) \cong \Aut(\mfC)$.

Finally, let us consider consider item <ref>. Assume
that $\mfA$ is $\ell$-homogeneous, for $\ell \geq 3$, and let $k \geq 1$.
Let $\tup c = (c_1, \dots, c_k)$ and $\tup d = (d_1, \dots, d_k)$ be two
$k$-tuples of elements in $\mfC$.
We have to show that if $(\mfC, \tup c) \equiv^{\ell \cdot (d+r) \cdot
k} (\mfC, \tup d)$, then there exists an automorphism $\pi$ of $\mfC$ such
that $\pi(\tup c) = \tup d$.
The main observation is that each element in $\mfC$ is $d$-supported
by elements of $\mfA$, that is the element can be defined in
$\FPC$ in $\mfC$ using at most $d$ parameters from $U_A$. More precisely,
for every element $c$ of $\mfC$ there
exist at most $d$-many elements $s_1, \dots, s_d \in A = U_A$ for which
there exists an $\FPC$-formula $\psi(x,y_1, \dots, y_d)$ with at most
$(d+3)$ many variables such that $\psi(x,s_1, \dots, s_d)$ defines $c$ in
the structure $\mfC$. For instance, for tuples $c = (b_1, \dots, b_d)$ in
$U_T$, we can choose $s_1,
\dots, s_d$ to be the components $b_1, \dots, b_d$ of the tuple, and for
elements $c = [\tup b] \in U_B$ we can choose the components of some
Hence, if $(\mfC, \tup c) \equiv^{\ell
\cdot (d+r) \cdot k} (\mfC, \tup d)$, then in particular we can find two
supports $s(\tup c) \in U_A^{d \cdot k}$ for $\tup c$ and $s(\tup d) \in
U_A^{d \cdot k}$ for $\tup d$ such that
$(\mfC, s(\tup c)) \equiv^{\ell \cdot (d+r) \cdot k} (\mfC, s(\tup d))$.
Moreover, since $\tup a$ is -definable in $\mfC$ (each component of
the tuple $\tup a$ is definable using at most three variables), we can
conclude that
$(\mfC, s(\tup c), \tup a) \equiv^{\ell \cdot (d+r) \cdot k} (\mfC, s(\tup
d), \tup a)$.
Since $\mfA$ is $\ell$-homogeneous, we know that
$\Typk{\ell \cdot (d \cdot k + r)}{d \cdot k}[\tup a]$ defines a
total preorder on $(d \cdot k)$-tuples in $\mfA$ which orders tuples up
to orbits with respect to $\Aut(\mfA, \tup a) \cong \Aut(\mfC)$.
Since $\mfA$ is a definable substructure of $\mfC$ we know that
$(\mfA, s(\tup c), \tup a) \equiv^{\ell \cdot (d+r) \cdot k} (\mfA, s(\tup
d), \tup a)$.
It follows that we can find a $\pi \in \Aut(\mfC)$ such that $\pi(s(\tup
c)) =
s(\tup d)$. Since supports uniquely describe elements, we conclude that
$\pi(\tup c) = \tup d$, as claimed.

In what follows, for a given $\FPC$-interpretation $\mcI(\tup z) \in
\FPC[\sigma \to \tau, \tup z]$, we denote the interpretation $\mcJ(\tup
z)$ as constructed in Theorem <ref> by $\Norm(\mcI)(\tup z)$.

For every $\FPC$-interpretation $\mcI(\tup z)$, there exists $\ell \geq
1$ such that the class of structures $\{ \Norm(\mcI)(\mfA, \tup a) : \mfA
\in
\CFIclass{\mcF}{p}, \tup a \in A^r \}$ is $(\ell, p)$-cyclic.

Intuitively we showed that the class of $\cyclp$ is closed under
$\FPC$-interpretations (which, if stated precisely, means that we have
to rewrite the interpretations in normal form and we have to increase the
homogeneity constant by a factor depending on the dimension and parameter
length of the specific interpretation).
We end this section by stating a much simpler observation.
Assume that we have two $\cyclp$-structures $\mfA$ and $\mfB$ of the same
vocabulary $\tau$.
Then the ordered pair $(\mfA, \mfB)$ is a $\cyclp$-structure as
Of course, to some extent this depends on the technical details on how we
implement ordered pairs as relational structure.
The most important property is that, in the ordered pair
$(\mfA, \mfB)$, we have a simple means to identify the two
substructures $\mfA$ and $\mfB$, for instance by using additional
predicate symbols to identify the two universes $A$ and $B$.
In this article, we agree to understand ordered pairs in this way.
consequence is that the automorphism group of $(\mfA, \mfB)$ is just
the direct product of the automorphism groups of $\mfA$ and $\mfB$. In
particular, orbits of (mixed) tuples in $(\mfA, \mfB)$ can be
in terms of the respective subtuples in $\mfA$ and $\mfB$. Having this, we
can easily see that the following holds.

Let $\mfA$ and $\mfB$ be two $\cyclp$ structures of vocabulary $\tau$.
Then the ordered pair $(\mfA, \mfB)$ is an $\cyclp$ structure as

§.§ Solving Cocyclic Linear Equation Systems

If we want to express $k$-dimensional -refutations over a
$\mbF$ in $\FPC$, then we need to be able to define solution spaces of
equation systems over that field $\mbF$ in $\FPC$, see
Figure <ref>.
In Section <ref> we proved that $\FPC$ can
define solution spaces of linear equation systems over $\mbQ$, and this
was the key to showing
that $\FPC$ can express $k$-dimensional
$\PC$-refutations over $\mbQ$, cf. Theorem <ref>.
Hence, in order to prepare our main result of this section
(Theorem <ref>), we
are now going to show that $\FPC$ can define solution spaces of linear
equation systems over a finite field $\mbF$ of characteristic $q$ under
the assumption that these
systems are interpreted in a class of $\cyclp$-structures with $q \neq p$.
Moreover, we show that the number of required variables is
bounded linearly in $\ell$ (with a constant factor that only depends on
the initial interpretation).
Note that our assumption $q \neq p$ is crucial: the CFI-problem over
$\field F_p$ cannot be expressed in $\FPC$,
but it can be reduced (in first-order logic) to the solvability
problem of linear equation systems over $\field F_p$.

For our proof we make use of a key idea from [28]: in the
special situation that we consider here, it turns out that
(solvable) linear  equation system always have symmetric solutions, that
is solutions which are invariant under all automorphisms of the underlying
linear equation systems. Together with the property of homogeneity this
observation allows us to show that $\FPC$ can define such symmetric
solutions, see [28].
In this article, we go one important step further.
We not only show that, in this particular setting, we can define the
Boolean solvability problem for
linear equation systems in $\FPC$, but that we can also define the more
functional problem of expressing solution spaces of given linear

Let us remark that our results here extend our approach
from [28] in another crucial way. In [28] we
considered the CFI-construction with respect to underlying graphs of
unbounded degree. The reason is that, if we work with such underlying
graphs, then this considerably simplifies the proof
of the homogeneity property for CFI-structures. Here, in contrast, we
consider the “full” power of the
CFI-construction, that is with respect to a family of underlying
expander graphs.  This has the effect that we get much better lower
bounds on the number of variables, and this makes our separation results
even stronger. That is to say that the techniques that we develop here can
readily be used in order to strengthen our separation
results from [28] to formulas with a sublinear number of
variables (rather than a constant number as we considered
in [28]).

As usual, in order to talk about systems of linear
equations over finite fields in the context of logical definability, we
first have to agree on an encoding of such systems as finite relational
Again, the concrete choice does not matter, so we do not specify
such an encoding explicitly. Let us rather go through some notation  that
we use in this section.
We consider (unordered) matrices $M$ over a finite field
$\field F$ as mappings
$M \colon I \times J \to \field F$ for two (non-empty) index sets $I$
and $J$.
An (unordered) vector $v$ over a finite field $\field F$ is a
mapping $v\colon I \to \field F$.
A linear equation system $M \cdot x = b$ over a finite field $\field F$ is
specified by an $I \times J$-coefficient matrix $M$ over $\field F$ and an
$I$-constants vector $b\colon I \to \mbF$.
We usually think of the finite field $\field F$ as being part of the
We are primarily interested in the setting where the
characteristic $q = \characteristic(\mbF)$ of this field $\field F$ and
the prime $p$ for
CFI-class $\CFIclass{\mcF}{p}$ are distinct:

Let $\ell \geq 1$.
We say that a $\tau$-structure $\mfA$ contains an
vector, (or matrix, or linear equation system) over a finite field $\field
F$ if

* the structure $\mfA$ is $\cyclp$ for some prime $p \in \Primes$, and

* for some distinguished relation symbol $S \in \tau$, the
substructure of $\mfA$ induced on $S$ is (the structural encoding of) a
vector $v\colon I \times \mbF$ (or
matrix $M \colon I\times J \to \mbF$, or linear equation system $M \cdot x
= b$) over the finite field $\mbF$ with characteristic different
from $p$, that is $\characteristic(\mbF) = q$ for some $q \in \Primes$,
$p \neq q$.

We proceed to show that $\FPC$ can express solution spaces of
$\ell$-cocyclic linear equation systems using $\mcO(\ell)$ many
variables only.
The proof consists of two steps. First of all, we show that $\FPC$
can define a single solution of a (solvable) linear equation
system (Theorem <ref>).
In a second step we then show that $\FPC$ can also define (small)
sets for kernels of matrices (Theorem <ref>). By
putting these two results together, we obtain the desired result.
The main idea for this second step is to repeatedly make use of the
$\FPC$-formula from Theorem <ref> for solving linear
equation systems and the fact
that structures can be linearly ordered locally in $\FPC$.

For every $\ell \geq 1$ there exists an $\FPC$-formula $\phi$ with
$\mcO(\ell)$ many variables such that $\phi$ defines in every structure
$\mfA$ that contains
a solvable linear equation system $M \cdot x
= b$ over a finite field $\mbF$, where $M \colon I \times J \to \mbF$ and
$b\colon I \to \mbF$, a solution to $M \cdot x = b$, that is $\phi$
defines a vector $v\colon J \to \mbF$ such that $M \cdot v = b$ (and, if
\cdot x = b$ is not solvable, then, by convention, $\phi$ defines the
all-$0$-vector in $\mfA$).

Let $\mfA$ be an $\cyclp$ structure which contains a linear equation
system $M \cdot x  = b$ for a matrix $M \colon I \times J \to \mbF$ and a
constants vector $b\colon I \to \mbF$ over a finite field $\mbF$ of
characteristic $\characteristic(\mbF) = q$, $p \neq q$.
Let $\Gamma = \Aut(\mfA)$ denote the automorphism group of $\mfA$.
Then $\Gamma$ acts on the solution space of $M\cdot x = b$.
We know that this space (in case that it is non-empty) has size $q^i$ for
some $i \geq 0$, since we are
dealing with a linear equation system over a field of characteristic $q
\in \Primes$.
On the other hand, recall that $\Gamma$ is a $p$-group which means that
each orbit of the action of $\Gamma$ on the solution space of $M \cdot x =
b$ has size $p^j$ for some $j \geq 0$.
We conclude that there has to be at least one orbit of size one.
This, however, means that there is a solution $v\colon J \to \field F$
$\pi(v) = v$ for all $\pi \in \Gamma$.
We call a vector $v\colon J \to \field F$ which satisfies this property
symmetric. Note that a symmetric vector $v\colon J \to \field F$ is
constant on
the orbits induced by $\Gamma$ on the set $J$ since $\pi(v)(j) =
By our assumption that $\mfA$ is $\cyclp$, we know that the formula
$\Typk{\ell}{1}(x,y)$ defines a linear preorder $\preceq$ on $J$ which
linearly orders $J$ up to $\Gamma$-orbits.
Moreover, recall that this $\FPC$-formula $\Typk{\ell}{1}$ only uses
$\mcO(\ell)$ variables.
Let $J = J_0 \preceq J_1 \preceq \cdots \preceq J_{n-1}$ denote the
$\Gamma$-orbit partition of $J$.

For $0 \leq i < n$ let $t_i\colon J \to \field F$ denote the $J$-vector
is the identity on the $i$-th $J$-orbit, that is $t_i(j) = 1$ for $j \in
J_i$ and $t_i(j) = 0$ for $j \not\in J_i$.
Let $T$ denote the $J \times \{0, \dots, n-1\}$-matrix which has $t_i$ as
its $i$-th column.
Then for every symmetric $v\colon J \to \field F$ we can find a vector
$w \colon \{ 0, \dots, n-1 \} \to \field F$ such that $Tw = v$. Indeed,
choose $w(i) = v(j)$ for (some) $j \in J_i$.
We conclude, that the linear equation system $M\cdot x = b$ is solvable
if, and only if, the system $M \cdot T \cdot x = b$ is solvable.
Clearly, every solution of $M \cdot T \cdot x = b$ gives rise to a
solution of $M \cdot x = b$.
Hence, it suffices to define a solution of $M \cdot T \cdot x = b$ in
fixed-point logic with counting.
However, this is very easy because $M \cdot T$ is an $I\times \{0, \dots,
n-1\}$-matrix which has a linearly ordered set of columns.
Moreover, if we drop duplicates of rows, then the order on the columns
also induces a (first-order definable) linear order on the rows, namely
the lexicographical ordering (note that there exists an $\FO$-definable
order on the finite field $\field F$).
It follows by the Immerman-Vardi Theorem that fixed-point logic can
define a solution of the system $M \cdot T \cdot x = b$ or determine that
the original system was not solvable. This solution
can be lifted to a solution of $M \cdot x = b$ by multiplying
by $T$. Finally, observe that the number of variables in the resulting
formula is independent of $\ell$ except for the subformula
which defines the linear order on the orbit-partition of $J$. Hence, the
required number of variables is indeed $\mcO(\ell)$.

For every $\ell \geq 1$ there exists an $\FPC$-formula $\phi$
with $\mcO(\ell)$ variables which defines in every structure $\mfA$
that contains an matrix $M\colon I \times J \to \field F$ over a
finite field $\field F$, a
matrix $\phi^\mfA\colon J \times (J \times |J|) \to \field F$ such that
$\im(\phi^\mfA) = \kernel(M)$.

Let $\mfA$ be an $\cyclp$ structure with automorphism group
$\Gamma=\Aut(\mfA)$, and assume that $\mfA$ contains a matrix $M\colon I
\times J
\to \field F$ over a finite field $\field F$ of characteristic
$\characteristic(\field F) = q \neq p$.
First of all, we again use the formula $\Typk{\ell}{1}(x,y)$ to define a
preorder $\preceq$ on $J$ which orders the indexing elements in $J$ up to
Let $J = J_0 \preceq J_1 \preceq \cdots \preceq J_{n-1}$.
Recall that $\Typk{\ell}{1}$ is an $\FPC$-formula with $\mcO(\ell)$
Our plan is as follows. We aim to define a generating set for $\kernel(M)$
which consists of $i$-homogeneous vectors for $0 \leq i < n-1$.
Here we say that a vector $v\colon J \to \field F$ is $i$-homogeneous if
= 0$ for all $j \in J_{i'}$ for $i' < i$. That is an $i$-homogeneous
vector is zero on all $\Gamma$-orbits on $J$ which precede the $i$-th
orbit $J_i$.
Our plan is to define in $\FPC$, for every $0 \leq i < n$,  sets
$K_i$ consisting of $i$-homogeneous vectors $v\colon J \to \field F$, $v \in
\kernel(M)$, such that the
projections of $K_i$ to $J_i$ yield generating sets for the projections
of $\kernel(M)$ to $J_i$, which means that $\bigcup_{i < n-1} K_i$ is a
generating set for $\kernel(M)$.

We will index the elements in $K_i$ by elements in $J_i
\times |J|$. The crucial insight is that $\cyclp$ structures satisfy the
additional property that for each fixed parameter $j \in J_i$  the
formula $\Typk{\ell \cdot 2}{1}[j](x,y)$ defines a linear order $<_j$ on
Hence, if we have a fixed $j \in J_i$, then it makes sense to speak of
an $m$-th echelon vector $(0, \dots, 0, 1, \star, \star)$ of the
projection of $\kernel(M)$ to $J_i$. Here an $m$-th echelon vector has
$1$ in the $m$-th component and is zero at all preceding components (and
its length is $|J_i|$). Clearly, for some $0 \leq m \leq |J_i|$ such a
vector may not exist, but if we collect a set of (existing) $m$-th echelon
vectors for $0 \leq m \leq |J_i|$, then we obtain a generating set for
the projection of $\kernel(M)$ to $J_i$.
With this preparation, we can describe our strategy more
precisely. The intention is that the $J$-vector $v \in K_i$ that is
by $(j, m)$, $j \in J_i$, $m < |J|$, represents an $i$-homogeneous vector
$v \in \kernel(M)$ with the additional property that the projection of $v$
$J_i$ is the $m$-th echelon vector of the projection of $\kernel(M)$ to
(if it exists, otherwise we agree to let $v = 0$).
Note that in this way we actually include too many vectors in $K_i$.
Indeed, it would be sufficient to consider all such vectors indexed by $j
\times |J_i|$ for a single $j \in J_i$. However, since we cannot choose a
particular $j \in J_i$ we just add all of these vectors for any $j
\in J_i$. This
does not cause any problems, since we do not aim at defining a basis for
$\kernel(M)$, but just at defining a generating set.

It remains to see how we can define such a vector $v\colon J \to \field F$
$\FPC$ given parameters $(j, m) \in J_i \times |J|$.
To this end we make use of Theorem <ref> and the formulas
$\Typk{\ell}{1}$ and $\Typk{\ell \cdot 2}{1}[j]$ (both with $\mcO(\ell)$
many variables only).
Let us start with the homogeneous linear equation system $M \cdot x = 0$
which defines $\kernel(M)$. Given the parameters $(j,m)$, we now add
extra constraints for the variables
$x = (x_j)_{j \in J}$ as follows:

* for $j' \in \bigcup_{i' < i} J_{i'}$ we set $x_{j'} = 0$,

* for $J_i = j_1 <_j \cdots <_j j_s$, we set $x_j = 0$ for $j \in \{
j_1, \dots, j_{m-1} \}$ and $x_{j_m} = 1$.

It is clear that the solution space of this linear equation system
consists precisely of the $i$-homogeneous vectors $v \colon J \to \field
$\kernel(M)$ whose projections to $J_i$ are $m$-th echelon vectors (with
respect to the order $<_j$ defined by $\Typk{\ell \cdot 2}{1}[j]$ on
Moreover, this system can easily be defined in $\mfA$ using an
$\FPC$-formula which uses $\Typk{\ell \cdot 2}{1}[j]$ and $\Typk{\ell}{1}$
as subformulas and parameters $(j,m)$.
We can now make use of Theorem <ref> to define a solution
$v\colon J \to \field F$ of this system (if a solution exists) in $\FPC$
again $\mcO(\ell)$ many variables only. This yields the desired vector in
$K_i$, that is indexed by $(j,m)$, and it concludes our proof.

By putting Theorem <ref> and Theorem <ref>
together we arrive at our desired result, namely that $\FPC$ is able to express
solution spaces
of linear equation systems $M \cdot x = b$ where $M\colon I
\times J \to \field F$ and $b \colon I \to \field F$ using $\mcO(\ell)$
many variables only.
Unfortunately, there is still a small problem:
according to Theorem <ref>, the index set for the solution
space that we get is $(J \times |J|)$. However, in general, $|J|$ can be
much larger than $|I|$, and we would like to get small generating
sets for expressing $\PC$-refutations when we think of our procedure from
Figure <ref>. In fact, when we express $k$-dimensional
-refutations in $\FPC$, then for the
linear equation systems that we need to solve there, we only have a global
polynomial bound on the size of the index $I$ (the set of $k$-dimensional
monomials), but not on
the size of the index $J$ (which indexes the generating set for $\PCx
k(\mcP)$ that we have computed up to a certain
stage, cf. Figure <ref>).
Fortunately, we can use the same strategy that we used in order to prove
Theorem <ref> in order to convert a (potentially large)
generating set for a given linear space into a small one within $\FPC$.

For every $\ell \geq 1$ there exists an $\FPC$-formula
$\phi$ with $\mcO(\ell)$ variables such that for every structure $\mfA$
which contains an matrix $M\colon I \times J \to \field F$ over a
finite field $\field F$, the formula $\phi$ defines in $\mfA$ a
matrix $\phi^\mfA\colon I \times (I \times |I|) \to \field F$ such that
$\im(\phi^\mfA) = \im(M)$.

The proof is analogous to our proof of Theorem <ref>.

For every $\ell \geq 1$ there exist $\FPC$-formulas
with $\mcO(\ell)$ variables such that for every structure $\mfA$
which contains an linear equation system $M \cdot x = b$ for
$M \colon I \times J \to \field F$ and $b\colon I \to \field F$ over a
finite field $\field F$, the formulas either define a
matrix $N\colon J \times K \to \field F$ and a $J$-vector $v\colon J \to
\field F$ such that $\im(N) + v$ is the solution space of $M \cdot x = b$
$K \in \{ I \times |I|, J \times |J| \}$ and $|K| = \min(|I|^2, |J|^2)$,
or, in case that the solution space is empty, they define $v = \emptyset$.

§.§ Cocyclic PC-Refutations over Finite Fields in FPC

We can finally come to our main result of this section. We show that
can express $k$-dimensional -refutations over finite fields $\field F$
of characteristic $q$ if the inputs are polynomial equation systems
that are interpreted in a class of $(\ell,p)$-cyclic structures, where $q
\neq p$,
using only $\mcO(\ell)$ variables.
As the prototype example, this situation occurs whenever we interpret
polynomial equation systems over a field $\field F$ of characteristic
$\characteristic(\field F) = q$ in (disjoint unions) of CFI-structures
$\mfA \in \CFIclass{\mcF}{p}$ over $\field F_p$.
For the proof, recall that for an $\FPC$-interpretation $\mcI$, we denote
$\Norm(\mcI)$ its normal form according to Theorem <ref>.

Let $Q \subsetneq \Primes$ be a (non-trivial) set of primes.
Let  $\mcI(\tup x)$ be an $\FPC$-interpretation which
$\tau$-structures to polynomial equation systems over finite
fields $\field F$ of characteristic $q \in Q$.
Then for every $\ell \geq 1$, $k \geq 2$, and $p \in \Primes, p \not\in
Q$, there exists an $\FPC$-formula $\phi$ with $\mcO(k\cdot \ell)$ many
variables such that for every $\cyclp$ $\tau$-structure $\mfA$ and $\tup a
\in \dom(\mfA,\tup x)$ we have that $\mfA \models \phi(\tup a)$ if, and
only if, the polynomial equation system $\mcI(\mfA, \tup a)$ has a
$\PC$-refutation (over the respective finite field $\field F$) of degree
at most $k$.

Let $d \geq 1$ denote the dimension of $\mcI(\tup x)$ and $r \geq 0$ the
number of parameters, $r = |\tup x|$.
We use Theorem <ref> to transform $\mcI(\tup x)$ into normal
form $\Norm(\mcI)(\tup x)$.
Then, if $\mfA$ is an $\cyclp$ $\tau$-structure and $\tup a \in \dom(\mfA,
\tup x)$, then we know that $\Norm(\mcI)(\mfA, \tup a)$ is $(\ell \cdot (d
+r))$-homogeneous and that the automorphism group of $\Norm(\mcI)(\mfA,
\tup a)$ is an Abelian $p$-group.
We conclude, using Theorem <ref>, that
$\Norm(\mcI)(\mfA,\tup a)$ is $(\ell \cdot (d+r),p)$-cyclic. Note that $d,
r$ are
constants which only depend on the fixed interpretation $\mcI$.

Now, assume that we want to express in $\FPC$, given $\Norm(\mcI)(\mfA,
\tup a)$, whether the contained polynomial equation system
$\mcP$ over the finite field $\mbF$ of characteristic $q \neq p$
has a $k$-dimensional -refutation.
In order to do this, we want to express the procedure from
Figure <ref> in $\FPC$. Recall that the main (and only)
is to (iteratively) define solution spaces of linear equation system over
$\field F$ in $\FPC$.
However, since $\mcP$ is part of an $(\mcO(\ell),p)$-cyclic structure, all
linear equation systems that we have to solve are $\mcO(\ell)$-cocyclic
Since we can define the index sets for these systems using $\mcO(k)$ many
variables in $\FPC$ (because we basically have to index all degree-$k$
multilinear monomials) it follows from
Corollary <ref> that solution sets can
be defined in $\FPC$ using at most $\mcO(k \cdot \ell)$ many variables.
We can now translate the resulting formulas back via $\Norm(\mcI)$ which
adds another constant factor to the number required variables that only
depends on $\mcI$. This concludes our proof.

As we said, in particular, we can apply this result for polynomial
equation systems
interpreted in CFI-structures. This
will allow us to  derive lower bounds for the polynomial calculus
just by using finite-model-theoretic arguments in
Section <ref>.

§ APPLICATIONS IN PROOF COMPLEXITY

Our model-theoretic characterisations  of (bounded-width) resolution
and the polynomial calculus via $\EFP$- and $\FPC$-definability allow us
uniformly (re-)prove many lower bounds on the complexity of proofs (size
and/or width/degree) for families of propositional formulas using
arguments from finite model theory.
The basic idea is very simple. We saw that the amount of certain logical
resources that are required to express refutations (that is the number of
variables) matches the
complexity of refutations (width of clauses or degree of polynomials) up
to linear factors.
It follows that if we exhibit families of propositional
formulas $\Phi_n, \Psi_n$ that cannot be distinguished in $\EFP$ (or in
$\FPC$) using $\mcO(k)$ variables, then also the corresponding
propositional proof systems cannot distinguish between these
formulas using refutations of width $k$ or degree $k$, respectively. In
particular, if one of the formulas in our family
$(\Phi_n, \Psi_n)$, say $\Phi_n$, is satisfiable, then there cannot be a
refutation for the indistinguishable formula $\Psi_n$ (of a certain

In the conference version of this article [27] we discussed
these applications with respect to the resolution proof system.
However, given that we extended our definability results for the
polynomial calculus in this article, we can basically derive the same
bounds directly for the full polynomial calculus over the rationals and
over finite fields (with the Pigeonhole principle being the only
exception). Clearly, this makes the lower bounds more interesting
and, for conciseness, we therefore restrict our attention to the
polynomial calculus here.

§.§ Lower Bounds on Degree and Size of Refutations

In this section we establish our main tool for proving lower bounds for
the polynomial calculus.
Recall the notion of $(\ell, p)$-cyclic structures from
Section <ref>.

Let $\field F$ be a finite field or the field of rationals. Moreover, let
$(\mcP_n)$ and $(\mcQ_n)$ be two families of
polynomial equation systems over $\mbF$ and let
$\mcI$ be an $\FPC$-interpretation that maps $\tau$-structures to
polynomial equation systems over $\field F$.
In addition, let $\ell \geq 1$ and let $p \in \Primes$ be such that
$\characteristic(\field F) \neq p$ and let $(\mfA_n)$ and $(\mfB_n)$ be
two families of $(\ell,p)$-cyclic $\tau$-structures such that for all $n
\geq 1$:

* $\mcI(\mfA_n) = \mcP_n$ and $\mcI(\mfB_n) = \mcQ_n$,

* $\mcP_n$ is satisfiable and $\mcQ_n$ is not satisfiable,

* $\mfA_n \equiv^{\Omega(n)} \mfB_n$.

Then the following holds:

* Let $\PCdegree(n)$ denote the minimal degree required to
refute the system $\mcQ_n$ using the polynomial calculus over $\field F$.
Then $\PCdegree(n) \in \Omega(n)$.

Moreover, as a consequence of this, the following holds:

* Let $\PCsize(n)$ denote the
size of a minimal PC-refutation
for $\mcQ_n$ over $\field F$. If the systems $\mcQ_n$, for $n \geq 1$,
only contain $\mcO(n)$ many variables, then $\PCsize(n)$ is bounded from below
by $2^{\Omega(n)}$.

For any degree $k \geq 1$, we know that by Theorem <ref> (if
$\field = \mbQ$) or Theorem <ref> (if $\field F$
is finite and of characteristic $q \neq p$) there exists an $\FPC$-formula
$\phi_k$ with $\mcO(k)$ many variables (note that $\ell$ is fixed) which
expresses whether the polynomial equation systems $(\mcP_n)$, $(\mcQ_n)$
have a $\PC$-refutation over $\field F$ of degree at most $k$.
By translating these formulas back via the fixed $\FPC$-interpretation
$\mcI$ (where we use $\Norm(\mcI)$ in case of finite fields) we obtain
$\FPC$-formulas $\psi_k$ with $\mcO(k)$ such that $\mfA_n
\models \psi_k$ if, and only if, $\mcP_n$ has a degree $k$ PC-refutation
over $\field F$, and likewise for $\mfB_n$ and $\mcQ_n$.
However, since $\mcP_n$ is satisfiable it has no such refutation for any
degree $k \geq 1$. Since $\mfA_n \equiv^{\Omega(n)} \mfB_n$, it thus
follows that for $k \in \Omega(n)$, also $\mcQ_n$ has no such degree
$k$-refutation. This proves our first claim.
The second claim follows from the size-degree trade-off for the
polynomial calculus, see <cit.>.

§.§ Lower Bounds for the Graph Isomorphism Problem

We now discuss the prototype example for the lower bound technique on
$\PC$-refutations (Theorem <ref>). Specifically, we show
the graph
isomorphism problem does not allow small PC-refutations neither over
$\mbQ$ nor over finite fields.
This result has already been established by Berkholz and Grohe
in [10, 11] by using known lower bounds for the
polynomial calculus. Here, we present an alternative proof of (a
generalisation of) their result using only arguments from finite model

Given two graphs $G=(V,E)$ and $H=(W,F)$ it is easy to express the graph
isomorphism problem for $G$ and $H$ as a polynomial equation system
$\IsoForm(G,H)$ over any field $\mbF$ as follows.
We use variables $X[v \mapsto w]$, for $v \in V$ and $w \in W$, to
indicate whether $v$ is mapped to $w$ by an isomorphism (that we are going
to guess as a solution). We include the Boolean constraints $X^2 -
X = 0$ as usual, i.e. $X[v \mapsto w] \in \{0 , 1\}$ for every solution.
Then we just have to express that every vertex $v \in V$ is mapped to
precisely one $w \in W$: $\sum_w X[v \mapsto w] = 1$, and, dually, that
every $w \in W$ has precisely one preimage $v \in V$: $\sum_v X[v \mapsto
w] = 1$.
Finally we want that edges are preserved. We can achieve this by including
for each $v_1, v_2 \in V$ and $ w_1, w_2 \in W$ such that $(v_1, v_2) \in
E$ if, and only if, $(w_1,w_2) \not\in F$ the equation $X[v_1 \mapsto
w_1]\cdot X[v_2 \mapsto w_2] = 0$.
It is this (fixed) encoding that Berkholz and Grohe considered
in [10, 11] in order to prove their
lower bounds.
Interestingly, we can easily lift their result to a more general
setting, namely we can
allow arbitrary encodings of the graph isomorphism problem that are
definable in $\FPC$ and still obtain the same lower bounds.

Let $\field F$ be the field of rationals or a finite field.
Let $\mcI$ be an $\FPC$-interpretation that maps pairs of graphs $(G, H)$
to polynomial equation systems over $\field F$ such that $\mcI(G,H)$ is
solvable if, and only if, $G$ and $H$ are isomorphic.
Then there exists a sequence $(G_n, H_n)$ of pairs of non-isomorphic
graphs $G_n, H_n$ with bounded degree and of size $\mcO(n)$ such that
$\PC$-refutations for the systems $\mcI(G_n, H_n)$ over $\field F$ require

Choose $p \in \{ 2, 3 \}$ such that $\characteristic(\field F) \neq p$.
We consider the class of CFI-structures $\CFIclass{\mcF}{p}$ over $\field
F_p$. Recall that $\mcF = \{ F_n : n \geq 1\}$ is a family of $3$-regular,
connected expander graphs where $F_n$ has $\mcO(n)$ many vertices.
In Lemma <ref> we observed that we can encode
such CFI-structures as undirected graphs via $\FPC$-interpretations $\mcJ$
(with a corresponding inverse interpretation $\mcJ^{-1}$).
Moreover, for a CFI-structure $\mfA=\CFIgraph{F_n}{p}{\lambda} \in
\CFIclass{\mcF}{p}$, the graph $\mcJ(\mfA)$ encoding $\mfA$ has degree
$\mcO(p^2)$ and contains $\mcO(p^2 \cdot n)$ vertices. Since $p \in \{ 2,
3\}$, it follows that the graphs $\mcJ(\mfA)$ have bounded degree and
contain $\mcO(n)$ vertices only.

For $n \geq 1$ we fix two non-isomorphic CFI-structures $\mfA_n, \mfB_n
\in \CFIclass{\mcF}{p}$ with underlying graph $F_n$ over $\field F_p$.
We let $G_n = \mcJ(\mfA_n)$ and $H_n = \mcJ(\mfB_n)$. We claim that
the resulting sequence $(G_n, H_n)$ satisfies the above claim.
To show this we use Theorem <ref>.
Let $\mcP_n = \mcI(G_n, G_n)$ and $\mcQ_n = \mcI(G_n, H_n)$.
Then we observe that $\mcP_n$ and $\mcQ_n$ can be interpreted in the
structures $(\mfA_n, \mfA_n)$ and $(\mfA_n, \mfB_n)$ via $(\mcI \circ
\mcJ)$ (where, formally, we need to slightly modify $\mcJ$ to encode
ordered pairs of CFI-structures as ordered pairs of graphs).
By the CFI-Theorem <ref> we know that $(\mfA_n, \mfA_n)
\equiv^{\Omega(n)} (\mfA_n, \mfB_n)$.
By Theorem <ref> and Theorem <ref>,
we know that the structures $(\mfA_n, \mfA_n)$ and $(\mfA_n, \mfB_n)$ are
$\cyclp$ for some fixed $\ell \geq 1$.
Moreover, by our assumption on $\mcI$, the systems $\mcP_n$ are
satisfiable and the systems $\mcQ_n$ are not satisfiable.
Thus, all preconditions of Theorem <ref> are met, and the
lower bound follows.

Although Theorem <ref> gives us the desired linear lower bound
on the degree of PC-refutations for the graph isomorphism problem, we can
not readily infer the exponential size lower bound from
Theorem <ref>.
The reason is that the polynomial equation systems which encode the graph
isomorphism problem might contain more than a linear number of
variables. In fact, the number of variables in the system
$\IsoForm(G,H)$ that we defined above contains a quadratic number of
variables. This means that the size-degree trade-off results for the $\PC$
cannot be applied.

However we can fix this as follows. In our proof we used CFI-graphs
and these are graphs of bounded colour class size.
Formally, a graph with colour class size $k\geq 1$ is a structure
$G=(V,E, \preceq)$ where $(V,E)$ is a graph and where $\preceq$ is a
linear preorder on $V$ such that every class of $\preceq$-incomparable
vertices, that is every colour class, is of size at most $k$.
In other words, one can think of the vertices of the graph $G$ to be
coloured while we only allow that at most $k$ vertices get the same
We write $V = V_0 \preceq \cdots \preceq V_{n-1}$ to denote that $V$ is
linearly ordered by $\preceq$ into $n$ colour classes $V_i$ in the
indicated way. We have that $|V_i| \leq k$ for every $i < n$.

For CFI-graphs (that is graphs $\mcJ(\mfA)$ for $\mfA \in
\CFIclass{\mcF}{p}$ and where $\mcJ$ is the graph encoding of
CFI-structures from Lemma <ref>) the colour classes
are basically given as the edge classes of the underlying graph plus the
additional classes of inner nodes which encode the CFI-constraints, see
our discussion preceding Lemma <ref>. The size of
these classes is at most $\mcO(p^2)$. Since in our proof we can restrict
to CFI-graphs over the field $\field F_p$ with $p \in \{ 2, 3 \}$, these
edge classes are indeed of constant size.
Hence, it follows from our proof above that we can require the family
of graphs $(G_n, H_n)$ in Theorem <ref> to consist of graphs
of bounded colour class size.

Now, restricted to graphs of bounded colour class size, our encoding
$\IsoForm(G,H)$ for the graph isomorphism problem that we introduced above
can naturally be simplified resulting in a polynomial equation system
that uses linearly many variables only. To see this, we consider pairs of
graphs $G=(V,E,\preceq_V)$ and $H=(W,F,\preceq_W)$ of
colour class size $k\geq 1$ with the same number of colour classes, that is

\begin{align*}
V &= V_0 \preceq_V  V_1 \preceq_V \cdots \preceq_V V_{n-1} \\
W &= W_0 \preceq_W W_1 \preceq_W \cdots \preceq_W  W_{n-1}.
\end{align*}

Then each isomorphism is restricted to map vertices in the $i$-th
colour class $V_i$ in $G$ to the $i$-th colour class $W_i$ in $H$. That
means that in our system $\IsoForm(G,H)$ we only need to
include variables $X[v \mapsto w]$ for all $v \in V_i, w \in W_i$, $i <
Since the colour classes are of constant size, this means that the
resulting system only contains a linear number of variables.
Hence, we obtain the following strengthening of
Theorem <ref> for this setting.

Let $\field F$ be the field of rationals or a finite field.
Let $\mcI$ be an $\FPC$-interpretation that maps pairs of  graphs $(G,
H)$ of bounded colour class size to polynomial equation systems
over $\field F$ such that $\mcI(G,H)$ is
solvable if, and only if, $G$ and $H$ are isomorphic, and, moreover
$\mcI(G,H)$ contains a linear number of variables only (linear with
respect to the number of vertices of $G$ and $H$).
Then there exists a sequence $(G_n, H_n)$ of pairs of non-isomorphic
graphs $G_n, H_n$ with bounded degree, of size $\mcO(n)$, and of bounded
colour class size such that
$\PC$-refutations for the systems $\mcI(G_n, H_n)$ over $\field F$ require
$\Omega(n)$ and size $2^{\Omega(n)}$.

§.§ Monomial-PC versus (Full-)PC over the Field of Rationals

As mentioned above, in [10] Grohe and Berkholz studied
the power
of the polynomial
calculus with respect to the graph isomorphism problem.
One of their main results is that the monomial-PC over $\mbQ$ has
precisely the same expressive power as the well-known Weisfeiler-Leman
graph isomorphism test which, in turn, has the same expressive power as
counting logic (with respect to isomorphism testing).
However, they left open the question of whether the full polynomial
calculus is more expressive than its restricted variant the monomial-PC
over $\mbQ$ with respect to the graph isomorphism problem.

For all $k \geq 2$ and graphs $G,H$ we have that

\[ G \not\equiv^k H \text{ if, and only if, } G \not\equiv^{\monPCx k} H\]

In the above theorem, $G \not\equiv^{\monPCx k} H$ means that the
monomial-PC (over $\mbQ$) can refute the system $\IsoForm(G,H)$ using
degree at most $k$.
Obviously, this also implies that if $G \not\equiv^k H$, then $G
\not\equiv^{\PCx k} H$, that is $\IsoForm(G,H)$ can be refuted in the
full-PC with degree at most $k$. However, it remained open whether the
converse holds as well (in particular, it remained open if the converse
holds if we allow to increase the dimension for the Weisfeiler-Leman
algorithm by a constant factor).

Is there a function $f\colon \mbN \to \mbN$ such that for all $k \geq 2$
we have

\[ G \not\equiv^{\PCx k} H \,\, \Longrightarrow \,\, G \not\equiv^{f(k)}

It immediately follows from Theorem <ref> that the answer is
affirmative and that we can choose $f$ to be linear.

There is a linear function $f\colon \mbN \to \mbN$ such that for all $k
\geq 2$ we have

\[ G \not\equiv^{\PCx k} H \,\, \Longrightarrow \,\, G \not\equiv^{f(k)}
H. \]

Let $\mcI$ be an $\FO$-interpretation which interprets the
$\IsoForm(G,H)$-formulas as polynomial systems over $\mbQ$ in pairs of
graphs $(G,H)$.
Let $r \geq 1$ be the number of variables in $\mcI$ and let $c\geq 1$ be a
constant such that the number of variables in the $\FPC$-formulas $\phi_k$,
that express the existence of $k$-dimensional PC-proofs according to
Theorem <ref>, is bounded by $c \cdot k$.

We claim that $G \equiv^{r \cdot c \cdot k} H \,\, \Longrightarrow
\,\, G \equiv^{\PCx k} H$.
So let us assume that $G \equiv^{r \cdot c \cdot k} H$.
First of all it holds that $G \equiv^{r \cdot c \cdot k} H$ if, and only
if, $(G,G) \equiv^{r\cdot c \cdot k} (G,H)$.
By the closure of $\FPC$ under $\FO$-interpretations, it then follows that
$\IsoForm(G,G) \equiv^{c\cdot k} \IsoForm(G,H)$. Since $\IsoForm(G,G)$ is
clearly satisfiable and since $\phi_k$ cannot distinguish between
$\IsoForm(G,G)$ and $\IsoForm(G,H)$ it follows that there does not exist a
$k$-dimensional $\PC$-refutation of $\IsoForm(G,H)$. Hence $G \equiv^{\PCx
H$ as claimed.

§.§ Constraint Satisfaction Problems

In this section we derive a dichotomy result for constraint
satisfaction problems (CSPs) with respect to refutations in the polynomial
calculus and the (weaker) resolution proof system.
Intuitively, what we are going to show is that each CSP either allows
simple proofs of inconsistency, namely such proofs that can be derived in
bounded-width resolution, or it requires proofs of very high complexity,
that is of linear degree and exponential size, even in the much stronger
polynomial calculus proof system.

Let us recall the definition of CSPs.
We present the formulation as a homomorphism problem.
Let $\mfT$ be a fixed relational $\tau$-structure (the template).
Then the constraint satisfaction problem associated with $\mfT$ is
the class $\Hom(\mfT)$ consisting of all $\tau$-structures $\mfA$ for
which there exists an homomorphism $h\colon \mfA \to \mfT$.
Many combinatorial problems can be posed as CSPs. On the other hand, the
class of all CSPs is limited in a certain sense: a famous conjecture
by Feder and Vardi [23], which was recently confirmed
independently by
Bulatov [12] and Zhuk [42],
says that for each template $\mfT$ the problem
$\Hom(\mfT)$ is either decidable in polynomial time () or complete
for non-deterministic polynomial time (-complete).
We will make use of a similar definability dichotomy for $\FPC$ soon.

But before we do this, let us describe a simple algorithm to
(approximately) solve constraint satisfaction problems.
This algorithm is known as the $k$-consistency test
and it can be phrased as follows.
Fix a template $\mfT$ and consider an input structure $\mfA$.
Let us denote by $\Part^k(\mfA, \mfT)$ the set of all partial
homomorphisms $p$ from $\mfA$ to $\mfT$ whose domain $\dom(p)$ is of size
at most $k$ (we include the empty homomorphism $\emptyset$).
The idea is to iteratively compute restrictions $T_i \subseteq
\Part^k(\mfA, \mfT)$ of $\Part^k(\mfA, \mfT)$ with respect to the
following closure properties. We set $T_0 = \Part^k(\mfA, \mfT)$.
For $i \geq 1$ we set

\begin{align*}
T_i &= \{ p \in T_{i-1} : \text{for all} \dom(p) \subseteq S
\subseteq A \text{, } |S| \leq k \text{ th. ex. } q \in T_{i-1} \text{
s.th. } p \subseteq q, \dom(q) = S, \\
&\qquad\text{ and for all } q \subseteq p \text{ we have } q \in T_{i-1}\}
\end{align*}

We output the final set $T_\infty$. In other words we iteratively
eliminate all partial homomorphisms which cannot be extended to partial
homomorphisms of size at most $k$ with respect to all possible
(consistent) domains, and such partial homomorphisms for which we
eliminated a restriction in the iteration before.
The first observation is that if there exists a homomorphism $h\colon \mfA
\to \mfT$, then $T_\infty \neq \emptyset$, because the set of all
restrictions of $h$ to partial homomorphisms in $\Part^k(\mfA, \mfT)$ will
be contained in each $T_i$.
Hence, if $T_\infty = \emptyset$, then we can correctly conclude that
\not\in \Hom(\mfT)$.
If, on the other hand, $T_\infty \neq \emptyset$, then in the general case
we must output “we don't know”.
However, in many cases, depending on the template $\mfT$, this naive
algorithm will work correctly on all inputs, which means that we have
an efficient and simple way to decide the problem $\Hom(\mfT)$.

Before we come to this, let us observe that it is very easy to express the
$k$-consistency test using bounded-width resolution.
For every $p \in \Part^k(\mfA, \mfT)$ consider a Boolean variable $X_p$
with the intended meaning that $X_p$ is true if $p \in T_\infty$.
According to the $k$-consistency test, we consider the following set of

* For every $p \in \Part^k(\mfA, \mfT)$, every $\dom(p) \subseteq S
\subseteq A$ with $|S| \leq k$:

\[ X_p \rightarrow \bigvee_{\begin{array}{c} \footnotesize
p \subseteq q \in \Part^k(\mfA,
\mfT),  \\\dom(q) = S                            \end{array}
} X_q.\]

* For every $p \in \Part^k(\mfA, \mfT)$ and every $q \subseteq p$:

\[ X_p \rightarrow X_q.\]

We obtain a (dual-)Horn-formula which always has the trivial model where
we set every variable to false. Moreover, every non-trivial model is a
witness that $T_\infty \neq \emptyset$. Since in this case $\emptyset \in
T_\infty$, this means that if we add the single clause $X_{\emptyset}$ to
the above formula, then we obtain a (dual-)Horn-formula which is not
satisfiable if, and only if, $T_\infty = \emptyset$.
Moreover, note that since $\mfT$ is a fixed template, the above
formula is of constant width. We conclude that $T_\infty = \emptyset$ if,
and only if, bounded-width resolution can refute the above formula.
It is obvious that this formula is also interpretable in $\mfA$ using a
first-order interpretation.

For every $k \geq 1$, the $k$-consistency test can be
expressed in  $\FO(\Res_{\mcO(k)})$.

Now, what happens if we have a template $\mfT$ for which the
$k$-consistency test is incomplete for any fixed value of $k \geq 1$?
In this case the (descriptive) complexity of the problem $\Hom(\mfT)$
is much higher. In fact, it follows from [3]
and [8] that in this case, the problem cannot be defined in
$\FPC$. This  “definability dichotomy”  was first explicitly noted, and
refined, by Dawar and Wang in [19] and in [21]:

For every template $\mfT$ one of the following is true.

* Either there is a $k \geq 1$ such that the $k$-consistency
test correctly decides $\Hom(\mfT)$, or

* there exists a (non-trivial) finite Abelian group $G$ such that
the problem of deciding the solvability of linear equation systems over
$G$ with at most three variables per equation, $\text{3LIN}(G)$, reduces
to $\Hom(\mfT)$ via an $\FPC$-interpretation of linear size (that is the
interpretation only increases the sizes of structures by a constant

Moreover, it is known that the problem of deciding whether two
CFI-structures $\mfA, \mfB \in \CFIclass{\mcF}{p}$ over the same
underlying graphs are isomorphic reduces to $\text{3LIN}(\field F_p)$ via
an $\FPC$-reduction of linear size. Hence, by applying
Theorem <ref> (and using the same arguments as in the
Section <ref>) we get the following dichotomy for
the proof systems resolution and polynomial calculus.
For every template $\mfT$ one of the following holds.

* Either $\Hom(\mfT)$ can be decided using bounded-width resolution,

* there exists a finite set of primes $P \subseteq
\Primes$ such that for every linear-size $\FPC$-definable encoding of
$\Hom(\mfT)$ as a system of polynomial equations $\mcP(\mfT)$ over a field
$\field F$, which is either $\mbQ$ or a finite field with
$\characteristic(\field F) \not\in P$, refutations of $\mcP(\mfT)$ in the
polynomial calculus over $\field F$ require width $\Omega(n)$ and size
$2^{\Omega(n)}$ (where $n$ refers to the size of the input structures

For the case of $\mbQ$, this dichotomy result has been
established in [6] via a different proof strategy. Let us remark
that, as a result of our approach, we can
formulate our dichotomy result with respect to every $\FPC$-definable
encoding (of linear size if we want to maintain exponential size lower
bounds). Also, to the best of our knowledge, this dichotomy was not known
for the case of the polynomial calculus over finite fields.

§ DISCUSSION: THE POWER OF THE POLYNOMIAL CALCULUS AND BEYOND

The resolution proof system and the polynomial calculus are two
important and well-studied propositional proof systems.
In this article we characterised their power from the viewpoint of
finite model theory. We proved that bounded-width resolution ($\kRes$,
$k\geq 3$) is complete for existential fixed-point logic
($\EFP$), that Horn-Resolution ($\HRes$) is complete for least
fixed-point logic ($\LFP$), and that the bounded-degree (monomial)-PC
($\monPCx{k}, \PCx k, k \geq 2$) over $\mbQ$ are complete for fixed-point
logic with counting ($\FPC$) under (numerical) first-order reductions.

On the one hand, by considering definability as our measure for
expressive power, the classification that we obtain is much finer compared
to the one that we get by using standard complexity-theoretic
Indeed, it is well-known that already $\kResx 3$ is $\PTIME$-complete,
which means that all (fragments of) proof systems that we
considered here are
equivalent from the viewpoint of (algorithmic) complexity theory.
In contrast, as we saw, we obtain a more interesting landscape
if we measure their descriptive complexity instead.

On the other hand, compared to the view of proof complexity, our
analysis is much coarser. For instance, in our framework there is no
explicit difference between width-$3$ and width-$k$ resolution for any $k
\geq 4$, while, from the viewpoint of proof complexity, clearly these
systems have different power.
The reason for this mismatch is that we allow more powerful logical
reductions (which are still weak from the
viewpoint of finite model theory).
We believe that this more general perspective, though not as
precise, makes it easier to pin down fundamental differences between, and
weaknesses of, the different (fragments) of proof systems.
For instance, our results show that the resolution proof system cannot
refute the Pigeonhole Principle for any -definable encoding,
see [27], while the polynomial calculus over $\mbQ$ allows
simple refutations (with respect to a natural encoding). Our results
explain this
“counting dichotomy” very clearly: resolution corresponds to $\EFP$, a
logic which lacks counting, and the polynomial calculus over $\mbQ$ to
$\FPC$, a logic
which explicitly includes a counting ability.
Moreover, our results highlight that the polynomial calculus has a
severe weakness: it is not able to go beyond $\FPC$ (with respect to its
bounded-degree $\PTIME$-stratification).
Since it is known that $\FPC$ fails to express all
$\PTIME$-properties, this implies that there are certain
$\PTIME$-properties which do not have small
refutations in the polynomial calculus. The prototype example is solving
linear equation systems over finite fields.
We can exploit this connection between $\FPC$ and the polynomial calculus
over $\mbQ$ even further to derive yet another characterisation. Indeed,
we can show that linear programming is complete for $\FPC$ under
(numerical) first-order reductions. This means that the power of the
polynomial calculus over $\mbQ$ corresponds precisely to the power
of linear programming under numerical $\FO$-reductions. This connects the
polynomial calculus with a very natural and significant algorithmic
in the setting of finite model theory.

Another interesting outcome of our work are the new finite-model theoretic
proofs for lower bounds on the complexity of refutations in the polynomial
We saw that, using a uniform finite-model theoretic approach, one can show
that many families of propositional formulas require refutations of
exponential size.
Remarkably, we could obtain these lower bounds not only for the polynomial
calculus over $\mbQ$, but also for the polynomial calculus over
finite fields.
Also, as a result of our approach, our lower bounds are very robust
in the sense that they do not rely on any specific encoding of
a problem as a propositional formula, but they hold with respect to any
($\FPC$-)definable encoding of the problem.
For the case of the polynomial calculus this implies, for example, that
all of the aforementioned lower bounds also hold for the polynomial
calculus with resolution (PCR). This proof system is nothing more than
the polynomial calculus, but we include for any variable $X$ a syntactic
dual variable $\bar X$ together with the axiom $1 - X = \bar X$. Clearly
these additional axioms can be defined in $\FPC$, and so, our results do
change in any way by considering the PCR instead of the standard PC.

Let us finally take a look at some future work.
We observe that in our lower bound proofs for the
polynomial calculus over finite fields we do not require a precise
connection with $\FPC$-definability (in fact, as we saw, such a precise
match between $\FPC$ and the polynomial calculus over finite fields does
not exist).
Indeed, for proving lower bounds it was sufficient to establish
$\FPC$-definability of refutations for families of propositional formulas
that are defined in CFI-structures. We then made use of the fact that
the CFI-problem is hard for $\FPC$ which gave us the lower bounds on the
proof complexity.
Even more general, we do not need to obtain $\FPC$-definability, but,
because of the fact that the CFI-problem is hard already for
finite-variable counting logic $\Cinf$,
it is sufficient to show
$\Cinf$-definability (recall that $\Cinf$ is a more powerful logic
than $\FPC$, so showing definability is easier).
We followed these lines for the case of the polynomial calculus
over finite fields in
Section <ref>. Therefore, we strongly made use of our
key technical results which says that CFI-structures over expander graphs
Recall that this means that we can order orbits of $k$-tuples in
CFI-structures using $\FPC$-formulas with a linear number of
variables only.

In fact, we can use this homogeneity result to develop a much more general
strategy for proving lower bounds for certain propositional proof system
As we explain in the following, in certain situations this result
allows us to quantify over refutations in $\Cinf$.
More precisely, assume that $\Prop$ has a stratification $\Prop=(\Prop_k)$
along a
parameter $k \geq 1$.
Moreover, assume that whenever a family of propositional formulas
that is defined (via a fixed $\FPC$-interpretation) in (pairs of)
CFI-structures, has a refutation in $\Prop_k$, then
it also has a refutation $\mfp$ such that:

* $\mfp$ is symmetric, that is invariant under all automorphisms of
the underlying CFI-structures, and

* $\mfp$ can be encoded as an object that is definable in the logic
$C^{\omega}_{\infty\omega}$ over the underlying CFI-structures with
$\mcO(k)$ variables,

* given a description of $\mfp$ as above, it can be
verified using a $\Cinf$-formula with $\mcO(k)$ many variables, that
$\mfp$ refutes $\mcF$.

If these (vaguely formulated) conditions are satisfied, then we can
basically apply our techniques in order to show that certain families of
propositional formulas, namely such formulas
which encode the CFI-isomorphism problem, cannot be refuted in $\Prop_k$
for any sublinear $k$.
At the moment, we work out the details and study to what extent these
conditions can be relaxed.

For now, let us illustrate the usefulness of this approach by
means of a simple example.
If we take another look at the paper by Grohe and
Berkholz [10], then we observe that they do, in fact, not
only derive lower bounds on the complexity of refutations for the graph
isomorphism problem for the polynomial calculus over $\mbQ$, but also for
stronger proof system which is known as the Positivstellensatz (or
Sums-of-Squares Proof System).
Let us briefly introduce this system. The setting is the same as for the
polynomial calculus over $\mbQ$, that is our input is a set $\mcP$
consisting of multivariate polynomials $p \in \mbR[\mcX]$, and our aim is
to show that the polynomials in $\mcP$ do not have a common zero. As
before we implicitly assume that the Boolean constraints $X^2 - X = 0$ are
contained in $\mcP$ for every variable $X \in \mcX$.

Let us fix a degree $k \geq 2$ which is even. A degree-$k$
Positivstellensatz refutation of a polynomial equation system $\mcP$ over
variables $\mcX$ consists of polynomials $f_p
\in \mbR[\mcX]$ such that

\[ \sum_{p \in \mcP} f_p \cdot p = 1 + s, \]

where $s$ is a sum-of-squares (sos) polynomial, that is $s = \sum_{i \in
I} q_i^2$ for some polynomials $q_i \in \mbR[\mcX]$, and such that all
polynomials in the above equation have degree at most $k$. Since $s(a)
\geq 0$ for every evaluation $a\colon \mcX \to \mbR$, the existence of
a refutation clearly proves that $\mcP$ is inconsistent.
Now, as in our description above, assume that we have interpreted this
system in a (pair) of CFI-structures, and let $\Gamma$ be the
corresponding CFI-automorphism group. Every $\pi \in \Gamma$ extends
(uniquely) to a permutation on $\mcX$ and so it defines a unique
automorphism of $\mbR[\mcX]$. Moreover, this automorphism of $\mbR[\mcX]$
$\mcP$. It follows that if we have a refutation as above, also

\[ \sum_{p \in \mcP} \pi(f_p) \cdot \pi(p) = 1 + \pi(s),\]

is a refutation. Here we are just saying that refutations are mapped
to refutations if we permute the variables in such a way that the set of
given polynomials remains stable. Clearly, this holds for any
reasonable proof system. In particular, note that $\pi(s)$ is also a
sum-of-squares polynomial (because $\pi$ is an automorphism of

However, in the case of the Positivstellensatz we can go one important
step further by summing up over all refutations that we obtain in this way:

\begin{align*}
\sum_{\pi \in \Gamma} \left(\sum_{p \in \mcP} \pi(f_p) \cdot \pi(p)\right)
= |\Gamma| + \sum_{\pi \in \Gamma} \pi(s).
\end{align*}

The importance of this equation follows from the fact that the sos
polynomial on the right-hand side is symmetric with respect to $\Gamma$.
The simple consequence is that whenever we can derive from
$\mcP$, via a degree-$k$ combination of polynomials, a polynomial $1 + s$,
where $s$ is an sos polynomial, then we can also derive from $\mcP$ a
polynomial $1 + \hat s$ where $\hat s$ is a symmetric sos
polynomial (note that sos polynomials are closed under addition).

This already brings us very close to our proof strategy from above: we saw
that whenever there is a degree-$k$ refutation, there is also a symmetric
Let us now complete our argument for the case of the Positivstellensatz
more explicitly.
The most important question is how we can obtain the symmetric
polynomial $1 + \hat{s}$ in $\Cinf$.
The key insight is that we don't have to bother too much about this,
because $1 + \hat{s}$ is symmetric.
Clearly, we can describe $r= 1 + \hat{s}$ as a mapping $r\colon M_k \to
\mbR$ where $M_k$ denotes the set of all monomials of degree at most $k$.
Since $r$ is symmetric, $r$ is a vector with the same entries on all
$\Gamma$-orbits on $M_k$. We now make use of the fact that CFI-structures
are $\FPC$-homogeneous. This allows us to order the $\Gamma$-orbits on
$M_k$ in $\FPC$ using only $\mcO(k)$ many variables.
Using this we can see that we can describe the vector $r$ by using a
mapping from an ordered set to $\mbR$. This is a quite simple object
from the viewpoint of $\Cinf$ as it has nothing to do with the
underlying structure. In particular, we can explicitly quantify
over all such mappings, since we have infinite conjunctions and
disjunctions available in $\Cinf$.
The final step is to verify that, having guessed such a vector $r\colon M_k
\to \mbR$ in $\Cinf$, this vector is indeed a refutation, that is $r = 1 +
\hat{s}$ for a symmetric sos-polynomial $\hat s$, and that $r$ can be
derived from $\mcP$ using a degree-$k$ polynomial combination.
The latter problem is about solving a linear equation system over $\mbR$
which can be done $\Cinf$ by what we saw in Section <ref>
(it is not hard to see that dealing with real numbers in this
context is easy: since we are working in $\Cinf$ and not in $\FPC$, we
can quantify explicitly over (sets of) real numbers that we can use for
our definitions).

The former problem can be reformulated as follows.
Let $M_{k/2}$ denote the set of monomials over $\mcX$ of degree at most
Let $S$ be the $M_{k/2} \times M_{k/2}$-matrix over $\mbR$ which is
defined by letting $S(m,n)$ be the leading coefficient of the monomial
$m \cdot n$, $m,n \in M_{k/2}$, in $\hat s$ that we get when we
syntactically expand the sos polynomial $\hat s$. Then $S$ is symmetric
and, as a consequence of
the syntactic form of $\hat s$ ($\hat s$ is an sos polynomial), $S$ can
be written as a sum of matrices $vv^T$ where the $v\colon M_{k/2} \to
\mbR$ correspond to the summands in $\hat{s}$. Vice versa, assume
that $S$ can be written in this form. Let $z$ be the $M_{k/2}$-vector
whose entries are the monomials $m \in M_{k/2}$, i.e. $z(m) = m$. Then it
is easy to see that $z^T S z$ is an sos polynomial. Hence, $\hat{s}$ is an
sos polynomial if, and only if, the corresponding matrix $S$ can be
written as a sum of matrices $vv^T$ for $v\colon M_{k/2} \to \mbR$.
This condition is equivalent to saying that $S$ is positive semi-definite,
which, in turn, is equivalent to saying that $S$ has only non-negative
It is known that the eigenvalues of matrices over $\mbQ$ are definable in
$\FPC$, see [18]. It is easy to adapt this definability
result to our setting which shows that the positive semi-definiteness of
$S$ can be certified in $\Cinf$ (using $\mcO(k)$ many variables) as well.

This proof (sketch) shows that all lower bounds for the
polynomial calculus that we obtained in
Section <ref>,
that is for graph isomorphism refutations and for the CSP dichotomy,
remain valid for the Positivstellensatz. These lower bounds have
been known before, but it is nice to see how easily they can be derived by
using our newly developed finite-model-theoretic tools.
Again, let us stress that what makes our arguments particularly simple
is the $\FPC$-homogeneity of CFI-structures.
As we saw, this result allows us to quantify over refutations in
$\Cinf$ (assuming that symmetric refutations with certain syntactic
properties exist), so we are only left with the usually much simpler task
of verifying such refutations in $\Cinf$.
As indicated above, this line of research is part of on ongoing project
where we explore the power of symmetric proof systems from the viewpoint
of finite model theory more thoroughly, so we defer the details to this
upcoming work.

[1]
M. Anderson and A. Dawar.
On symmetric circuits and fixed-point logics.
Theory Comput. Syst., 60(3):521–551, 2017.

[2]
A. Atserias.
On sufficient conditions for unsatisfiability of random formulas.
J. ACM, 51(2):281–311, 2004.

[3]
A. Atserias, A. Bulatov, and A. Dawar.
Affine systems of equations and counting infinitary logic.
Theoretical Computer Science, 410:1666–1683, 2009.

[4]
A. Atserias and V. Dalmau.
A combinatorial characterization of resolution width.
Journal of Computer and System Sciences, 74(3):323–334, 2008.

[5]
A. Atserias and E. N. Maneva.
Sherali-adams relaxations and indistinguishability in counting
In Innovations in Theoretical Computer Science 2012, Cambridge,
MA, USA, January 8-10, 2012, pages 367–379. ACM, 2012.

[6]
A. Atserias and J. Ochremiak.
Proof complexity meets algebra.
In 44th International Colloquium on Automata, Languages, and
Programming, ICALP 2017, volume 80 of LIPIcs, pages 110:1–110:14.
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017.

[7]
A. Atserias and J. Ochremiak.
Definable ellipsoid method, sums-of-squares proofs, and the
isomorphism problem.
In Proceedings of LICS 2018, 2018.

[8]
L. Barto and M. Kozik.
Constraint satisfaction problems solvable by local consistency
J. ACM, 61(1):3:1–3:19, 2014.

[9]
P. Beame and T. Pitassi.
Propositional proof complexity: Past, present, and future.
Current Trends in TCS: Entering the 21st Century, pages 42–70,

[10]
C. Berkholz and M. Grohe.
Limitations of algebraic approaches to graph isomorphism testing.
In Proceedings of ICALP 2015, pages 155–166, 2015.

[11]
C. Berkholz and M. Grohe.
Linear diophantine equations, group CSPs, and graph isomorphism.
In Proceedings of SODA 2017, pages 327–339, 2017.

[12]
A. A. Bulatov.
A dichotomy theorem for nonuniform CSPs.
In Proceedings of FOCS 2017, pages 319–330. IEEE Computer
Society, 2017.

[13]
J. Cai, M. Fürer, and N. Immerman.
An optimal lower bound on the number of variables for graph
Combinatorica, 12(4):389–410, 1992.

[14]
M. Clegg, J. Edmonds, and R. Impagliazzo.
Using the Groebner Basis Algorithm to find Proofs of
In STOC 1996, pages 174–183, 1996.

[15]
S. Cook and R. Reckhow.
The relative efficiency of propositional proof systems.
J. Symbolic Logic, 44:36–50, 1979.

[16]
E. Dahlhaus.
Skolem normal forms concerning the least fixpoint.
In Computation Theory and Logic, In Memory of Dieter
Rödding, volume 270 of Lecture Notes in Computer Science, pages
101–106. Springer, 1987.

[17]
A. Dawar.
The nature and power of fixed-point logic with counting.
ACM SIGLOG News, 2(1):8–21, 2015.

[18]
A. Dawar, M. Grohe, B. Holm, and B. Laubner.
Logics with rank operators.
In Proceedings of LICS 2009, pages 113–122, 2009.

[19]
A. Dawar and P. Wang.
A definability dichotomy for finite valued CSPs.
In Proceedings of CSL 2015, volume 41 of LIPIcs, pages
60–77. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015.

[20]
A. Dawar and P. Wang.
Lasserre lower bounds and definability of semidefinite programming.
CoRR, abs/1602.05409, 2016.

[21]
A. Dawar and P. Wang.
Definability of semidefinite programming and lasserre lower bounds
for CSPs.
In Proceedings of LICS 2017, pages 1–12. IEEE Computer
Society, 2017.

[22]
H.-D. Ebbinghaus and J. Flum.
Finite Model Theory.
2nd edition, 1999.

[23]
T. Feder and M. Y. Vardi.
The computational structure of monotone monadic SNP and constraint
satisfaction: A study through datalog and group theory.
SIAM J. Comput., 28(1):57–104, 1998.

[24]
E. Grädel and S. Hegselmann.
Counting in Team Semantics.
In Proceedings of CSL 2016, 2016.

[25]
E. Grädel, P. Kolaitis, L. Libkin, M. Marx, J. Spencer, M. Vardi,
Y. Venema, and S. Weinstein.
Finite Model Theory and Its Applications.

[26]
E. Grädel and G. McColm.
Hierarchies in Transitive Closure Logic, Stratified Datalog and
Infinitary Logic.
Annals of Pure and Applied Logic, 77:166–199, 1996.

[27]
E. Grädel, B. Pago, and W. Pakusa.
The model-theoretic expressiveness of propositional proof systems.
In Proceedings of CSL 2017, volume 82 of LIPIcs, pages
27:1–27:18. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017.

[28]
E. Grädel and W. Pakusa.
Rank logic is dead, long live rank logic!
In Proceedings of CSL 2015, Leibniz International Proceedings
in Informatics (LIPIcs), 2015.

[29]
M. Grohe and M. Otto.
Pebble games and linear equations.
J. Symb. Log., 80(3):797–844, 2015.

[30]
M. Grohe and W. Pakusa.
Descriptive complexity of linear equation systems and applications to
propositional proof complexity.
In Proceedings of LICS 2017, pages 1–12. IEEE Computer
Society, 2017.

[31]
B. Holm.
Descriptive Complexity of Linear Algebra.
PhD thesis, University of Cambridge, 2010.

[32]
S. Hoory, N. Linial, and A. Wigderson.
Expander graphs and their applications.
Bulletin of the American Mathematical Society, 43(4):439–561,

[33]
N. Immerman.
Descriptive complexity.
Graduate texts in computer science. Springer, 1999.

[34]
R. Impagliazzo, P. Pudlák, and J. Sgall.
Lower bounds for the polynomial calculus and the gröbner basis
Computational Complexity, 8(2):127–144, 1999.

[35]
P. G. Kolaitis.
The expressive power of stratified programs.
Inf. Comput., 90(1):50–66, 1991.

[36]
L. Libkin.
Elements of Finite Model Theory.

[37]
P. N. Malkin.
Sherali-adams relaxations of graph isomorphism polytopes.
Discrete Optimization, 12:73–97, 2014.

[38]
M. Otto.
Bounded Variable Logics and Counting.
Springer, 1997.

[39]
W. Pakusa.
Linear Equation Systems and the Search for a Logical
Characterisation of Polynomial Time.
PhD thesis, RWTH Aachen University, 2016.

[40]
N. Segerlind.
The Complexity of Propositional Proofs.
Bulletin of Symbolic Logic, 13(04):417–481, 2007.

[41]
J. Torán.
On the resolution complexity of graph non-isomorphism.
In Proceedings of SAT 2013, volume 7962 of LNCS, pages
52–66, 2013.

[42]
D. Zhuk.
A proof of CSP dichotomy conjecture.
In Proceedings of FOCS 2017, pages 331–342. IEEE Computer
Society, 2017.