has to occur

A Finite-Model-Theoretic View on Propositional Proof Complexity
*This article is an extended version  of the
conference paper [27].

E. Grädel]Erich Grädel1
1RWTH Aachen University, Germany

M. Grohe]Martin Grohe1

B. Pago]Benedikt Pago1

W. Pakusa]Wied Pakusa2
2University of Oxford, England
The fourth author was supported by a DFG grant (PA 2962/1-1).

We establish new, and surprisingly tight, connections
between propositional proof complexity and finite model
Specifically, we show that the power of several propositional proof
such as Horn resolution, bounded-width resolution, and the polynomial
calculus of bounded degree, can be characterised in a precise sense by
variants of fixed-point logics that are
of fundamental importance in descriptive
complexity theory.
Our main results are that Horn resolution has the
same expressive power as least fixed-point logic, that
bounded-width resolution captures existential least
fixed-point logic, and that
the polynomial calculus with bounded degree over the rationals
solves precisely
the problems definable in fixed-point logic with
By exploring these connections further, we establish
tools for proving lower bounds for the polynomial calculus over
the rationals and over finite fields.

§ INTRODUCTION

The question whether there exists an efficient proof system
by means of which the validity of arbitrary propositional formulas
can be verified via proofs of polynomial
size is equivalent to the closure of NP under complementation.
Since Cook and Reckhow [15] made the notion of an efficient
propositional proof system precise,
a huge body of research on the power of various propositional proof
system has been established. In particular, we now have super-polynomial
bounds on the proof complexity for quite strong proof systems, see
[9, 40] for surveys on propositional proof

In this paper we study polynomial-time variants of propositional
proof systems,
which admit efficient proof search, resulting in proofs of polynomial size,
such as restricted variants of resolution and the polynomial calculus.
Recall that the resolution proof system
$\Res$  takes as input a propositional
formula $\phi$ in conjunctive normal form (CNF), and it
refutes the satisfiability of $\phi$ if there is a derivation of the empty
clause from $\phi$.
It is well-known that shortest resolution proofs can be of exponential
size, so in general, we provably cannot search for resolution proofs in
polynomial time.
However, there are interesting restrictions  of $\Res$, such as
$\HRes$ (resolution restricted to Horn clauses) and bounded-width
$\kRes$ (resolution restricted to clauses of size
$\leq k$) that do admit efficient proof search, that is the existence of
refutations can be verified in polynomial time.
Of course, unless P = NP, any proof system that admits efficient proof
search is necessarily incomplete for full propositional logic.
Nevertheless we can still prove interesting statements
in such systems, and usually have completeness for relevant fragments of
propositional logic,
such as Horn-logic or 2-CNF.
We can now try to solve algorithmic problems by reducing them to
provability (or refutability) in some specific polynomial-time proof
which, if it works successfully for all inputs, would give us a
polynomial-time algorithm for the problem.
Our goal is to understand how powerful this approach can be, depending on
the specific proof system that we use.

Let us illustrate this by two concrete problems.
First we consider graph isomorphism,
a problem which is not known to be solvable in
polynomial time although there is strong evidence that it is not
Given two graphs $G=(V,E)$ and $H = (W, F)$ we ask
whether there is a bijection $\pi\colon V \to W$ such that $\pi(E) = F$.
Of course, this can easily be encoded as the satisfiability
problem of a propositional CNF-formula.
First, for each pair of vertices $v \in V$ and $w \in W$ we introduce a
variable $X_{vw}$ with the intended meaning that $X_{vw} = 1$ if $\pi(v) =
We add clauses $\bigvee_{w \in W} X_{vw}$ for every $v \in V$ and
$\bigvee_{v \in V} X_{vw}$ for every $w \in W$  to ensure that
every $v \in V$ has an image and every $w \in W$ has a preimage.
Additionally we add for all $v_1, v_2 \in V$ and $w_1, w_2 \in W$ a
clause $\neg (X_{v_1w_1} \wedge X_{v_2w_2})$ in case that $\{ v_1 \mapsto
w_1, v_2 \mapsto w_2\}$ is not a partial isomorphism.
The resulting CNF-formula, denoted by
$\text{Iso}(G,H)$, is satisfiable if, and only if, the two graphs $G$ and
$H$ are isomorphic.
Following our reasoning from above, we can now use an efficient
variant of resolution, or of a stronger proof system, and try to refute
the satisfiability of the
formula $\text{Iso}(G,H)$. If this is possible, then $G$ and $H$ are not
Unfortunately, if we do not find a proof, then we are stuck, because it
might still be the case that $G$ and $H$ are not isomorphic, but our
proof system is just not strong enough to show this.
Hence, we get an efficient, sound, but not necessarily complete
graph isomorphism test.
The question of how successful this approach is  when based on resolution
studied by Toran in [41]. Unfortunately, he proved that shortest
resolution proofs for graph non-isomorphism can be of exponential size
(even for graphs with colour class size four).
More recently, Grohe and Berkholz showed that also in the stronger system
polynomial calculus (PC) one cannot obtain small proofs for graph
non-isomorphism [10, 11] in the general case.

Our second example is directed graph reachability: Given a directed graph
$G = (V,E)$ with two distinguished vertices $s, t \in V$,
we want to know whether there is a path from $s$ to $t$ in $G$. Again, it
is easy to encode this as a satisfiability problem in
propositional logic, by taking the conjunction of all
implication clauses $X_v \to X_w$, for all edges $(v,w)\in E$,
together with the two clauses $1 \to X_s$ and $X_t
\to 0$. Clearly the resulting formula $\text{NonReach}(G,s,t)$ is
unsatisfiable if, and only if, $t$ is reachable from $s$ in $G$.
However, in clear contrast to the formulas $\text{Iso}(G,H)$ from above,
we can easily prove unsatisfiability for the formulas
$\text{NonReach}(G,s,t)$ in efficient variants of resolution
such as $\HRes$ and $\kRes$ for $k\geq 2$.

Our two examples demonstrate the following: while certain problems, such
as  directed graph reachability, allow for small and efficient resolution
proofs, other problems, such as the graph isomorphism problem, provably
require proofs of super-polynomial size even in quite strong proof
This leads to the main question that we want to address in this paper: is
there a classification for those problems which can be solved in
fundamental polynomial-time propositional proof systems such
$\HRes$, $\kRes$  and $\PCx k$ (the degree-$k$ restriction of the
polynomial calculus)?
It came as a surprise to us that there is, indeed, a very clear and
tight classification of the power of all of these proof systems in terms
of definability in important fixed-point logics which are well-studied in
the area of descriptive complexity theory.

Before we can state our results in detail, we have to explain what
we mean by saying that a problem, such as directed graph reachability, can
be solved by a propositional proof system $\Prop$.
As usual, each decision problem can be identified with a membership
“$\mfA \in \mcK$?” for some class of structures $\mcK$.
For instance, the graph reachability problem from above is identified with
the class $\mcK_{\text{Reach}} = \{ (V, E, s, t) : \text{there is a path
from } s \text{ to } t \text{ in } G=(V,E)\}$.
Then we naturally want to say that a problem $\mcK$ can be solved by the
proof system $\Prop$ if we can find a reduction function $f$ which
maps structures $\mfA$ to inputs $f(\mfA)$ for $\Prop$
such that $\mfA \in \mcK$ if, and only if, $\Prop$ can prove that
$f(\mfA)$ is not satisfiable.
It is clear that we only want to allow simple
reduction functions $f$, because otherwise the computation of the encoding
could already contain part of the work to solve the problem.
Coming from the area of finite model theory the obvious and natural
formalisation for “$f$ being simple” is to say that $f$ is
definable in first-order logic ().
We introduce the precise technical definition of such reductions, which
is the notion of  a first-order interpretation, in
Section <ref>.
Note that for the two examples we discussed above the encoding
functions are clearly $\FO$-definable.

Having established this definition it turns out that our
classification problem is really about understanding the expressive power
of the Lindström extensions of first-order logic by
generalised quantifiers for propositional proof systems $\Prop$.
We denote these logics by $\FO(\Prop)$. The basic idea of the logic
$\FO(\Prop)$ is to extend first-order logic by new quantifiers
$\mcQ_{\Prop}$ which are capable of simulating  $\Prop$.
In other words, we just incorporate into first-order logic the power to
simulate $\Prop$ in an explicit way, that is the logics
$\FO(\Prop)$ are a formalisation of the concept
oracle Turing-machines with access to $\Prop$ in the world of first-order
logic (the oracle calls to the proof system $\Prop$ correspond to
applications of the new generalised quantifiers). Again, the precise
technical definitions of the Lindström extensions $\FO(\Prop)$ can be
found in Section <ref>.
We can now  say that a problem $\mcK$ can be
solved in a proof system $\Prop$ if, and only if, it is definable in
For instance, we saw that $\mcK_{\text{Reach}}$ is definable in
the logics $\FO(\HRes)$ and $\FO(\kResx 2)$.

We proceed to describe our main results and give a rough sketch of the
structure of this article.
This work is based on our conference paper [27].
However, the present article also contains some new results and substantial
generalisations of our results from [27] on the polynomial calculus.

In Section <ref>, we study the resolution
proof system and its aforementioned restrictions Horn-Resolution
($\HRes$) and Bounded-width-$k$ Resolution
($\kRes$), for $k \geq 2$.
It turns out that $\HRes$ can express precisely the problems that
are definable in least-fixed point logic (), that is $\FO(\HRes) =
\LFP$. This readily follows by the well-known fact
that the problem of computing winning positions in reachability games
(known as GAME or  alternating reachability)  is complete for $\LFP$ with
respect to
More interestingly, we proceed to show that $\kRes$, for every $k \geq 2$,
is less powerful than $\HRes$. In fact, $\FO(\kResx 2)
= \FOTC$, where $\FOTC$ is the extension of first-order logic by a
transitive closure operator. Moreover, we prove that, for every $k \geq
$\FO(\kRes) = \EFP$, where $\EFP$ is the existential fragment of
least fixed-point logic which is known to be a strict fragment of full
least fixed-point logic.
We can also show that the Lindström extensions for Horn resolution and
width-$k$ resolution have different structural properties. While for
$\FO(\HRes)$ a single application of a $\mcQ_{\HRes}$ quantifier suffices
to obtain the full expressive power, nesting of
$\mcQ_{\kRes}$ quantifiers is needed for the logics $\FO(\kRes)$.

In Section <ref>, we then turn our attention to the polynomial
calculus (),  a propositional proof system which is based on algebraic
reasoning techniques. The polynomial calculus manipulates polynomial
equations over an underlying field $\field F$. A $\PC$-refutation is a
derivation of the equation $0 = 1$.
As in the case of bounded-width resolution, if one restricts the
degree of the polynomials in all equations to some constant $k \geq 1$,
then one can search for PC-proofs in polynomial time.
Besides restricting the degree, one can also vary the underlying
field $\field F$. Specifically, we consider the cases where $\field F$ is
field of rationals (or reals) or a finite field. Moreover, the polynomial
calculus can also be restricted by weakening its proof rule for
multiplication, which defines a variant known as the monomial-PC ().
We denote its corresponding restriction to degree $k$ by $\monPCx k$.

For the case of the polynomial calculus over $\mbQ$ we
show the following.
First of all, if we consider the monomial-PC restricted to some degree $k
\geq 2$, then this proof system $\monPCx k$ has precisely the same
expressive power as fixed-point logic with counting (), which is a
very expressive logic
well-studied in descriptive complexity theory [17, 38]; formally,
we show that $\FOnum(\monPCx k) = \FPC$ for $k \geq 2$ where $\FOnum$
denotes the extension of $\FO$ by a numeric sort to match
the setting of $\FPC$.
In particular, this separates the (monomial-)PC from the resolution proof
system since $\FPC$ is known to be much stronger than $\EFP$ and $\LFP$.
In a second step, we generalise this characterisation for the monomial-PC
to the full polynomial calculus (PC) by showing that degree-$k$
refutations can be defined in $\FPC$ as well.
On our way we prove a result which is of independent interest,
namely that $\FPC$ can define solution spaces of linear equation systems
over the rationals.
One consequence is that bounded-degree monomial-PC and bounded-degree PC
have the same expressive power with respect to $\FOnum$-reductions. This
allows us to answer an open question by Grohe and Berkholz
from [10] about the relative power of these two proof
systems with respect to the graph isomorphism problem.

In Section <ref>, we turn our attention to the
polynomial calculus over finite
fields. It is easy to see that the connection between $\FPC$ and the
(monomial-)PC breaks down. We set out to establish
criteria on the characteristic of the underlying finite field and certain
finite-model-theoretic properties of polynomial equation systems that
allow us to retain
$\FPC$-definability of bounded-degree PC-refutations.
This result proves to be very useful in
order to derive lower bounds for the polynomial calculus over finite
There are also technical results in this section which should be
of independent interest. For example, we show that classes of
CFI-structures over expander graphs are homogeneous with respect to

Finally, in Section <ref>, we discuss how we
can apply our $\FPC$-definability results in order to prove
lower bounds for the polynomial calculus.
We give examples including the graph isomorphism problem and constraint
satisfaction problems.
Although most (but not all) of the lower bounds have been known before, we
present new proofs which only use finite-model-theoretic arguments.
Our novel, uniform approach to these lower bounds, also suggests a way to
capture a common weakness of many propositional proof systems:
whenever a proof system has a stratification which allows for
symmetric refutations that can be described and verified in counting
logic with a bounded number of variables, our lower bounds techniques can be
applied. For illustration, we discuss the example of the Positivstellensatz
proof system in Section <ref>.

§.§ Related work

Let us discuss some related work.
The most relevant result to mention here is the
characterisation by Atserias and Dalmau of resolution width in
terms of the number of pebbles required to win an existential pebble
game played on a given CNF-formula and a
structural encoding of truth assignments [2, 4]. This
resembles our result that bounded-width resolution corresponds to
existential least fixed-point logic.
Using their game-theoretic characterisation, Atserias
and Dalmau can reprove many of the known lower bounds on
resolution width. Again, this is similar to the applications we give in
Section <ref>.

However, what makes our setting different from the approach of
Atserias and Dalmau is that we always consider the power of proof
systems only up to logical reductions. This reflects, for
example, in our result saying that $\FO(\kResx 3) = \FO(\kResx 4)$,
i.e. that $\kResx 3$ has the same expressive power as $\kResx 4$. But,
this only holds if we allow first-order reductions to transform inputs
between $\kResx 4$ and $\kResx 3$.
Hence our characterisation of resolution width is “coarser” than that of
Atserias and Dalmau. But it has the advantage of being more robust.
For instance,
in the situation of lower bound proofs, we can avoid playing
pebble games directly on the inputs to proof systems, such as
but instead it suffices to play suitable games on pairs of structures in
these inputs interpret. This can make the
description of winning strategies much simpler. Furthermore, our setting
allows us to prove lower bound results not depending on specific encodings
of a problem, since our logics are closed under interpretations, see
Section <ref>.

Besides this, we want to mention the
series of
papers [5, 10, 37, 29] which establish
surprisingly tight connections between the equivalence of graphs in
counting logic and their indistinguishability by linear programming
techniques (Sherali-Adams relaxiations of graph isomorphism
polytopes) and algebraic propositional proof system. Similar to our
applications, these results also allow the transfer of
lower bounds from finite model theory to get lower
bounds on proof complexity.
In particular, we use notions and ideas of [10] in
Section <ref>.
Let us also point to the excellent work of Dawar and
Wang [20, 21] which connect finite model theory with
semi-algebraic proof systems.

This work, and our own, has certainly also interesting connections
to the very recent work by Atserias and Ochremiak [7]
showing by means of finite-model-theoretic arguments that the Sums-of-Squares
proof system can be simulated in $\Cinf$.
Surely these connections deserve to be explored further.

§ PRELIMINARIES

This is a paper in finite model theory. All structures are
relational and finite if not explicitly stated otherwise.
We assume that the reader has a solid background in logic. To fully
and appreciate our results, familiarity with the ideas and techniques of
model theory will be necessary
(see [22, 33, 36, 25]).
In particular, a good knowledge of fixed-point logic with counting
is needed in order to understand our definability results for the
polynomial calculus in
Sections <ref>,<ref>,<ref>,
see the above references plus [38, 17].

§.§ Finite Relational Structures.

Given a (finite, relational) vocabulary
(or signature) $\tau$, a $\tau$-structure $\mfA$ consists of a
universe $A$ and a
relation $R^A\subseteq A^k$ for each $k$-ary relation symbol $R$ in
If we consider (undirected) graphs, that is structures
over the vocabulary $\tau = \{ E \}$, then we usually use a different
notation and denote graphs by $G = (V,E)$. In particular, we denote the
vertex set of a graph $G$ by $V = V(G)$ and the set of edges $E$ by $E =
The class of all (finite)
$\tau$-structures is denoted by $\Str(\tau)$.
Sometimes we want to distinguish certain constants in $\tau$-structures
$\mfA$. For a tuple of parameters $\tup z$ we denote by $\Str(\tau, \tup
z)$ the class of all pairs $(\mfA, \tup z \mapsto \tup a)$ where $\mfA\in
\Str(\tau)$.
For our applications in Section <ref> and
Section <ref>, we also fix an encoding of
ordered pairs $(\mathfrak A,\mathfrak B)$ of $\tau$-structures as
$(\mathfrak A,\mathfrak B)$ of
some vocabulary $\tau_{\textup{pair}}$.

§.§ Logics without Counting.

We assume that the reader is familiar with first-order logic ()
and least and inflationary fixed-point logic ($\LFP$ and $\IFP$).
Infinitary finite variable logic $\Linf$ extends $\FO$ by
infinite conjunctions and disjunctions in formulas, but with the
additional requirement that formulas only contain a finite number of
More precisely, if we denote by $\Linfx k$ the $k$-variable
fragment of $\Linf$, then we have $\Linf = \bigcup_k \Linfx k$.
Formulas of $\LFP$ with $k$ variables can be translated
into equivalent formulas of $\Linfx{k}$. In particular, $\LFP \leq
\Linf$ (in this article we use the notation $\Ll_1 \leq \Ll_2$ to say that
every class of structures that is $\Ll_1$-definable is also
$\Ll_2$-definable, that is $\leq$ refers to semantic inclusion of
logics wrt. sentences).

§.§ Logics with Counting.

(Infinitary) counting logic $\Cinf$ is the extension of $\Linf$ that
allows counting
quantifiers $\exists^{\ge m}x$ (“there exist at least $m$ values for
$x$”) for each $m$ (with the same restriction on the number of variables
as before, that is each $\Cinf$-formula only contains a finite number of
Note that each individual quantifier $\exists^{\ge m}x$ can be expressed
using $m$ first-order quantifiers and
$m$ distinct variables for $x$. However, the translation leads to formulas
with a higher quantifier rank and, moreover, it increases the number of
required variables. Analogous to the above, we denote by $\Cinfx k$ the
fragment of $\Cinf$ consisting of all formulas with at most $k$ (free or
bound) variables. Then $\Cinf = \bigcup_k \Cinfx k$.
For two structures $\mfA, \mfB$ (of the same vocabulary) we write $\mfA
\equiv^k \mfB$ if the structures cannot be distinguished by any formula of
$\Cinfx k$.

We now recall the definition of fixed-point logic
with counting ($\FPC$). In a nutshell, $\FPC$ is the
extension of inflationary fixed-point logic ($\IFP$) by counting
Formulas of $\FPC$ are evaluated over the two-sorted extension of
input structure $\mfA$ by a copy of the natural numbers.
Following [18] we denote by  $\mfA^{\#}$ the two-sorted
of a $\tau$-structure $\mfA=(A,R_1,\dots,R_k)$ by $\mfN=(\N,+,\cdot,0,1)$,
that is the two-sorted structure $\mfA^{\#} = ( A, R_1,\dots , R_k , \N, +,
\cdot, 0, 1)$ where the universe of the first sort (also referred to as
vertex sort) is $A$ and the universe of the second sort (also
referred to as number sort or counting sort) is $\N$.
For both, the vertex and the number sort, we have a collection of
typed first-order variables, that is the domain of any variable $x$
(over the input structure $\mfA$) is either $A$ or $\N$.
Similarly, for second-order variables $R$ we allow mixed types, that is a
relation symbol $R$ of type $(k , \ell) \in \N \times \N$ stands for a
$R \subseteq A^k \times \N^\ell$.

Of course, already $\FO$ is undecidable over the class of two-sorted
structures $\mfA^{\#}$. To obtain a logic with polynomial-time data
complexity, we have to restrict the range of
quantifiers over the numeric sort by fixed polynomials.
More precisely, $\FPC$-formulas can use quantifiers over the numeric sort
only in the form $Qx \leq n^q . \phi$ where $Q \in \{ \exists, \forall
\}$ and where $q \geq 1$ is a fixed constant.
The range of the quantifier $Q$ is $\{0, \dots, n^q\}$ where $n$ denotes
size of the input structure $\mfA$. To simplify notation, we henceforth
assume that each numeric variable $x$ comes with a built-in restricted
polynomial, that is $x = (x \leq n^q)$. For better readability, we
usually omit this range polynomial in our notation.
By this convention, each variable $x$ has a
predefined range in any input structure $\mfA^{\#}$ of polynomial size
(which is either $A$ or $\{0, \dots, n^q\}$ for a fixed $q \geq 1$).
We denote this range by $\dom(\mfA,x)$ (or just by $\dom(x)$ if
$\mfA$ is clear from the context). Analogously, for a tuple of variables
$\tup x=(x_1, \dots, x_k)$ we set $\dom(\tup x) = \dom(x_1) \times \cdots
\times \dom(x_k)$.
By this, we also obtain polynomial bounds for numeric components in
fixed-point definitions $\left[ \ifp \, R\bx \,.\, \phi(R,\bx)
\right](\bx)$.
Indeed, the inflationary fixed-point defined by this formula is of the
form $R \subseteq \dom(\tup x)$.

The crucial elements of $\FPC$ are counting terms which
allow to define cardinalities of sets. Starting with an arbitrary
$\FPC$-formula $\phi(x)$ one can form a new counting term $s = [\#
x \,.\, \phi]$ whose value in $\mfA$ is just the size of the set defined
by $\phi$ in $\mfA$.
In particular, the term $s$ is a numeric term, that is $s$ takes
value in the number sort. More precisely, for an input structure $\mfA$,
the  value $s^\mfA \in \N$ of $s$ in $\mfA$ is the number of elements
$a \in A $ such that $\mfA \models \phi(a)$.
One can allow counting terms of a more general form
without increasing the expressive power of . In particular, counting
terms $[\# \bx \,.\, \phi]$
over mixed tuples of variables can be simulated with unary counting
terms  and fixed-point operators; we refer to [38] for more
and background on fixed-point logic with counting.

An important fact that we are going to use frequently is that formulas of
$\FPC$ with $k$ variables can be rewritten as equivalent
$\Cinfx k$-formulas. In particular, we have that $\FPC \leq \Cinf$.
In Section <ref>, we also make use of the fact that
for every $k \geq 1$, there exists an $\FPC$-formula $\phi$ with $\mcO(k)$
many variables such that $(\mfA, \mfB) \models \phi$ if, and only if,
$\mfA \equiv^k \mfB$, see e.g. [38].

In Section <ref>, we also make use of the numeric
extension of first-order logic, denoted by $\FOnum$, which is defined
as $\FPC$, but without the rule for forming (inflationary) fixed points.

§.§ Logical Interpretations and Lindström Quantifiers

The logical counterpart of the notion of an (algorithmic) reduction is
of a logical interpretation. A logical interpretation $\mcI$
transforms an input structure $\mfA$ into a new structure $\mfB =
\mcI(\mfA)$
this transformation is defined by formulas of some logic $\Ll$.
In this article we consider $\Ll$-interpretations with respect to
different underlying logics $\Ll$, such as $\FO, \FOnum, \LFP, \FPC,
\Cinf$. Basically, the definition of an $\Ll$-interpretation is uniform for
all of these logics. However, there is one exception for the case of
$\FOnum$ and $\FPC$ where we have the special situation that formulas
can use numeric variables. As a consequence, the interpreted
structures $\mcI(\mfA)$ can contain such numeric elements.
In this section, we further introduce Lindström
quantifiers, also known as generalised quantifiers, which capture
the notion of oracles in the realm of finite model theory.

Let us start with the case of single-sorted logics
$\Ll$, such as $\FO, \LFP$, or $\Cinf$. Let $\sigma, \tau$ be signatures
with $\tau =
\{S_1,...,S_{\ell}\}$. Let $s_i$ denote the arity of $S_i$. An
$\Ll[\sigma,\tau]$-interpretation is a tuple

\[ I(\tup{z}) =
\tup{z}),\varphi_{S_1}(\tup{x}_1,...,\tup{x}_{s_1},\tup{z}),...,\varphi_{S_

\in \Ll[\sigma]$ and $\tup{x},\tup{x}_1,...,\tup{x}_{s_{\ell}}$ are tuples
of pairwise distinct variables of the same length $d$ and $\tup{z}$ is a
tuple of variables pairwise distinct from the $x$-variables. We call $d$
the dimension and $\tup{z}$ the parameters of $\I(\tup{z})$.

A $d$-dimensional $\Ll[\sigma,\tau]$-interpretation $\I(\tup{z})$  defines
a partial mapping $\I \colon \Str(\sigma,\tup{z}) \rightarrow \Str(\tau)$
in the
following way:  For $(\AA,\tup{z} \mapsto \tup{a}) \in
\Str(\sigma,\tup{z})$ we obtain a $\tau$-structure $\BB$ over the universe
$\{\tup{b} \in A^d \ | \ \AA \models \varphi_{\delta}(\tup{b},\tup{a})\}$,
setting $S_i^{\BB} = \{(\tup{b}_1,..,\tup{b}_{s_i}) \in B^{s_i} \ | \ \AA
\models \varphi_{S_i}(\tup{b}_1,...,\tup{b}_{s_i},\tup{a})\}$ for each
\in \tau$.
Moreover let $\Ee = \{(\tup{b}_1,\tup{b}_2) \in A^d \times A^d \ | \ \AA
\models \varphi_{\approx}(\tup{b}_1,\tup{b}_2,\tup{a})\}$. Now we define

\begin{equation*}
\I(\AA,\tup{z} \mapsto \tup{a}) :=
\begin{cases}
\BB/ \Ee &\text{if $\Ee$ is a congruence relation on } \BB\\
\text{undefined} & \text{otherwise.}
\end{cases}
\end{equation*}

We say that $\I$ interprets $\BB/\Ee$ in $\AA$.

Let us briefly discuss the case of two-sorted logics. If $\Ll$ is
$\FPC$ or $\FOnum$, then we have the same definition of an
$\Ll$-interpretation as above. However, note that now the variable tuples
$\tup x, \tup z, \dots$ may contain numeric variables. Recall that each
numeric variable $x$ has an explicit polynomial range bound $\dom(\mfA,
x)$ which is either $A$ or $\{0, \dots, n^q\}$ for a fixed $q \geq 1$. As
a consequence, the domain of the structure $\mcI(\mfA, \tup z \mapsto \tup
a)$ does not longer consist of equivalence classes of tuples in $A^d$ but,
more generally, it consists of equivalence classes of elements in
$\dom(\mfA, \tup x)$ (and note that these tuples may contain numeric

Next, we introduce Lindström quantifiers. Let $\Ll$ be a logic and $\Kk
\subseteq Str(\tau)$ a class of
$\tau$-structures with $\tau = \{S_1,...,S_{\ell}\}$. The Lindström
extension $\Ll(\Qq_{\Kk})$ of $\Ll$ by Lindström quantifiers for
the class $\Kk$ is obtained by extending the syntax of $\Ll$ by the
following formula creation rule:

be formulas in $\Ll(\Qq_{\Kk})$ that form an
$\Ll[\sigma,\tau]$-interpretation $\I(\tup{z})$. Then $\psi(\tup{z}) =
\Qq_{\Kk}\I(\tup{z})$
is a formula in $\Ll(\Qq_{\Kk})$ over the signature $\sigma$, with
$(\AA,\tup{z} \mapsto \tup{a}) \models \Qq_{\Kk}\I(\tup{z})$, if, and only
if,  $\BB :=
\I(\AA,\tup{z} \mapsto \tup{a})$ is defined and $\BB \in \Kk$.

As we see, adding the Lindström quantifier $\Qq$ to the logic $\Ll$ is
the most direct way to make the class $\mcK$ definable in $\Ll$.
We use this key notion to capture the power of propositional proof systems
up to first-order definable transformations.

§.§ Representing Propositional Formulas as Relational

As always when we are dealing with logics in algorithmic contexts,
we have to agree on encodings of (non-structural) inputs as
relational structures.
In this article such inputs are, for instance, propositional formulas,
polynomial equation systems, matrices and vectors over fields.
In all of these cases, it is straightforward to come up with natural
structural representations. Most
often, we refrain from describing such encodings explicitly. For it is
rather tedious, and, more importantly, the concrete details do not matter
too much: all (natural) encodings will be interdefinable in first-order

To get a better intuition, let's go through one encoding explicitly. Let
us briefly discuss two ways to represent propositional formulas (in CNF)
as finite relational structures.
Perhaps the most obvious representation of a CNF-formula $\psi$
as a structure $\AA(\psi)$ is based on the vocabulary
the universe of $\AA(\psi)$ consists of the variables and the clauses of
$\psi$, the monadic relations
$V$ and $C$ identify the variables and clauses, respectively, and the
binary relations
$P$ and $N$ specify which variables appear positively and negatively in
which clauses;
so $Pvc$ is true in $\AA(\psi)$ if the variable $v$ appears positively in
the clause $c$,
and analogously for $N$.
A different representation, that sometimes leads to more elegant logical
descriptions works
with the set $L$ of literals and with a self-inverse bijection $\neg: L \ra
L$, so that $\psi$ would be
represented by $\AA(\psi)=(A,C,L,\neg,\in)$ where $A$ is the set of
clauses and literals, $\neg(x)$ is the complementary literal to $x$, and
$x\in c$ means
that the literal $x$ occurs in the clause $c$ (note that, formally, we do
not allow function symbols in our vocabularies, but, of course, we can
substitute function symbols by their graph relations).

§ RESOLUTION AND (EXISTENTIAL) LEAST FIXED-POINT LOGIC

In this section we study the resolution proof system.
We start by showing that Horn-Resolution ($\HRes$) is complete for least
fixed-point logic ($\LFP$) wrt. (many-to-one) first-order
interpretations, see Theorem <ref>.
In a second step, we consider bounded-width resolution ($\kRes$, for $k
\geq 2$). We show that bounded-width resolution is strictly weaker than
Horn-Resolution from the viewpoint of finite model theory. Specifically,
we prove that $\kResx 2$ is complete for transitive closure logic
$\FOTC$ (Theorem <ref>) and that for every $k \geq 3$, $\kRes$
is complete for the existential fragment of least fixed-point logic
($\EFP$), see Theorem <ref>. Since it is known that $\FOTC <
\EFP < \LFP$, this separates the power of these polynomial-time
restrictions of the resolution proof system.

§.§ Horn Resolution Captures Least Fixed-Point Logic

Let $\posLFP$ be the fragment of -formulas that are in
negation normal form (i.e. negation is applied only to
input atoms), in which each fixed-point variable is bound only once, and
that do not make use of greatest fixed points.
Further, let $\EFP_0$ be the basic existential fragment of LFP;
it consists of those formulas in $\posLFP$ whose quantifiers are all

It is known that, on finite structures (but not in general), every
LFP-formula can be effectively
translated into an equivalent one in $\posLFP$. On the other side $\EFP_0$
is strictly weaker;
it has the same expressive power as Datalog with negation of input atoms.

For every $\phi\in\posLFP[\tau]$
there is a
first-order interpretation $I_\phi$ that maps  finite $\tau$-structures
to propositional Horn formulas  $\psi_{\AA,\phi}$ such that
$\AA\models\phi$ if, and only if, $\psi_{\AA,\phi}$ is unsatisfiable.
Further, if $\phi$ is in $\EFP_0$ then
all clauses in $\psi_{\AA,\phi}$ have width at most three.

Fix a formula $\phi\in \posLFP[\tau]$. For every finite
$\tau$-structure $\AA$, with universe $A$,
we construct the propositional Horn formula   $\psi_{\AA,\phi}$ as follows.
An instantiated subformula of $\phi$ is an expression $\beta(\bar
which is obtained by taking some subformula $\beta(\bar x)$ of $\phi$ and
by instantiating every free variable $x$ by some element $a\in A$.
We now take for every instantiated subformula $\beta$ of $\phi$ a
propositional variable $X_\beta$, and inductively define a set
$C(\AA,\phi)$ of clauses as follows.

* If $\beta$ is a $\tau$-literal, then we add $1\ra X_\beta$
in case that
$\AA\models\beta$ and $X_\beta\ra 0$ in case $\AA\not\models \beta$.

* If $\beta=\eta\lor\theta$, then we add the clauses $X_\eta\ra
X_\beta$ and
$X_\theta\ra X_\beta$.

* If $\beta=\eta\land\theta$, then we add the clause $X_\eta\land

* If $\beta=\E x\eta(x)$, then we add all clauses $X_{\eta(a)}\ra
X_\beta$ for $a\in A$.

* If $\beta=\A x\eta(x)$, then we add the clause $(\bigwedge_{a\in
A}X_{\eta(a)})\ra X_\beta$.

* If $\beta=[\lfp R\bar x \,.\, \eta ](\bar a)$ or $\beta=R\bar a$, then we
add the clause $X_{\eta(\bar a)}\ra X_\beta$.

By induction, it readily follows that the minimal model of all these
clauses sets the variable
$X_\beta$ to true if, and only if,  $\AA\models\beta$
(with fixed-point variables interpreted by their least fixed-point on
Let now $\psi_{\AA,\phi}$ be defined as the conjunction of all clauses in
together with  $X_\phi\ra 0$.
Then $\psi_{\AA,\phi}$ is unsatisfiable if, and only if, $\AA\models\phi$.

We observe that the only clauses of size larger than three are those
from universal quantifiers. Hence, if there are no universal quantifiers,
formula only has clauses of size at most three.
Finally it is clear that, for every fixed $\phi\in \posLFP[\tau]$,  we can
interpret  (a representation of) the formula $\psi_{\AA,\phi}$ inside
$\AA$,  by using an $\FO$-interpretation $I_\phi$.

This shows that $\LFP \leq \FO(\HRes)$. Actually we
established a stronger result.

For every formula $\phi \in \LFP$ there exists a first-order
such that $\Q{\HRes}( J_\phi)$ is equivalent to $\phi$ on
finite structures. In particular, each
$\LFP$-formula can be translated into an equivalent  $\FO(\HRes)$-formula
with a single
application of the generalised quantifier $\Q{\HRes}$.

We are ready to prove that $\FO(\HRes)$ has the same expressive
power as $\LFP$.

On finite structures,  $\LFP=\FO(\HRes)$.

It remains to  show that $\FO(\HRes) \leq \LFP$, that is we have to express
Horn resolution in . Recall that a propositional
Horn formula $\psi$  admits a derivation of the empty clause if,
and only if, $\psi$ contains a clause in which
all variables appear negatively, written $X_1 \wedge \dots \wedge X_k\ra
such that all unit clauses $\{X_i\}$ for $i=1,\dots, k$
can be derived from $\psi$ by Horn resolution.

Let $\psi$ be presented as a structure $\AA(\psi)$ with universe
$C\cup V$ and vocabulary $\{C,V,P,N\}$.
Let $D$ be the set of variables $v\in V$ such that
the clause $\{v\}$ can be derived from $\psi$ by
Horn resolution. Then $\psi$ is unsatisfiable if, and only if,
$\AA(\psi)\models  \E c (Cc\land \neg\E x Pxc \land \A x(Nxc\ra Dx))$.
The set $D$ is definable by the -formula
$ [  \lfp   Dx\,.\,  \E c (Pxc  \land \A y (Nyc \ra Dy))](x)$.

§.§ Bounded-Width Resolution and Existential Least Fixed-Point

Intuitively, existential least fixed-point logic (EFP) extends
$\EFP_0$ by stratified negation.
This means that it permits fixed-point formulas over existential formulas
which may depend on
closed fixed-point relations, defined in a lower stratum, and these can be
used also in negated form.
Thus, negation (and hence, implicitly, also universal quantifiers) are
present in a limited form, but
least fixed-point recursions may never go through negation or universal
In fact, EFP is equivalent to Stratified
Datalog and is weaker than full  [16, 35].

Existential fixed-point logic
$\EFP:=  \bigcup_{\ell \geq 0} \EFP_{\ell}$
generalises $\EFP_0$ as follows.  The stratum $\EFP_{\ell+1}$ is the
closure under disjunction, conjunction and existential quantification
of formulas of the form $[\lfp \ R\bar{x}. \E \bar y
\varphi(R,\bar{x},\bar
where $\phi(R,\bar x,\bar y)$ is obtained from a quantifier-free formula,
that may contain positive and
negative occurrences of additional relations $S_1,\dots,S_m$, by
substituting these relations by
formulas from $\EFP_\ell$.

Let us remark that the logic $\EFP$ is known under different names
(we stick to the term $\EFP$ which was used
in [16, 35]). For instance, in [22], the
term bounded fixed-point logic (BFP) is used to refer to the same
logic. Another common name for this logic  is stratified fixed-point
logic (SFP) in reference to its equivalence with Stratified Datalog.

Notice that first-order logic $\FO$ is contained in $\EFP$, but not in any
bounded level $\EFP_\ell$, because every quantifier alternation in $\FO$
must be simulated by an additional level of stratified
negation, again see [16, 35].
For the same reason $\EFP$, but none of its levels $\EFP_\ell$, is closed
under first-order operations. As a consequence of Theorem <ref> we
can infer

On finite structures, $\EFP \leq \FO(\kResx 3)$.

Theorem <ref> directly establishes this for $\EFP_0$.
So assume that the claim is established for $\EFP_\ell$.
Every formula in $\EFP_{\ell +1}$ can be written as an
$\EFP_0$-formula over predicates that are $\EFP_\ell$-definable.
Hence, by applying Theorem <ref> once more, it can be rewritten
as an $\FO(\kResx 3)$-formula over predicates that are themselves
definable in $\FO(\kResx 3)$.
Since Lindström extensions of $\FO$ are closed under nesting of
quantifiers, it follows that also $\EFP_{\ell+1}\leq  \FO(\kResx 3)$.

We require clauses of width 3 for translating $\EFP$-formulas into Horn
In fact, if we restrict to clauses of width 2, then we obtain the power of
first-order logic with a transitive closure operator $\FOTC$. This
immediately follows from the fact that satisfiability of $2$-CNF formulas
reduces to graph reachability, and from the reduction of graph
to the non-satisfiability problem for a $2$-CNF formula that we described
in the introduction.

On finite structures, $\FO(\kResx{2}) = \FOTC$.

§.§ Simulating Bounded-Width Resolution in EFP

To express width-$k$ resolution, for fixed $k \geq 1$, in
, we
shall use
the representation of a CNF-formula $\psi$ by structures
where $C$ is the set of clauses and $L$ is the set of literals, and the
is $A=C\cup L\cup\{0\}$.
Further we shall describe the set of all derivable clauses
of size at most $k$ as a $k$-ary relation $D\subseteq (L\cup\{0\})^k$,
that contains those $k$-tuples $(x_1,\dots,x_k)$ for which $\{ x_i: i\leq
k, x_i\neq 0\}$ is
a clause that is derivable from $\psi$.
This relation $D$ is defined by a fixed-point formula  $[\lfp D\tup x\,.\,
\phi(D,\tup x)](\tup x)$
where $\phi(D,\tup x)$ expresses the following. Either

* there exists a clause $c\in C$ such that $c=
\{x_1,\dots,x_k\}\setminus\{0\}$, or

* there exist tuples $\tup y, \tup z\in D$ such that, for some $i,j$,
the literal $z_j$ is the
negated literal to $y_i$, and $(\{

When spelling out these equations in first-order logic, we can express
$\phi(\tup x,D)$ by an existential $\FO$-formula
$\E \tup y \,  \alpha(\tup x,\tup y,D,Q)$ where $Q$ is $\FO$-definable
by a formula (with quantifier prefix $\E^*\A$) that does not depend
on $D$. This yields a formula in $\EFP_1$.
Since $\EFP$ is closed under $\FO$-operations, this proves

On finite structures, $\FO(\kRes) = \EFP$ for all $k \geq 3$.

Another interesting observation is that if we restrict the nesting depth
of $\kRes$-quantifiers in $\FO(\kRes)$-formulas to some constant $d
\geq 1$, then we obtain a fragment $\FO(\kRes)^{\leq d}$ of $\FO(\kRes)$
which is strictly
less expressive.
This follows from the results of Grädel and McColm [26] and the
observation that formulas in $\FO(\kRes)^{\leq d}$ can be written as
$\Linf$-formulas with at most $d$ many nested unbounded quantifier
However, as Grädel and McColm show there are formulas of transitive
closure logic $\FOTC$ which require more than $d$ many such blocks when
expressed as equivalent $\Linf$-formulas.
Since $\FOTC \leq \FO(\kRes)$, it follows that for every $d \geq 1$ we
have $\FO(\kRes)^{\leq d} < \FO(\kRes)$.
Note that this is different from the case of Horn-Resolution
where nesting of $\HRes$-quantifiers was not necessary.
In other words, while Horn-Resolution $\HRes$ is many-to-one complete for
$\LFP$ wrt. first-order interpretations, $\kRes$ is only complete wrt.
first-order Turing reductions for $\FOTC$ and $\EFP$, respectively.

§ THE POLYNOMIAL CALCULUS OVER THE FIELD OF RATIONALS AND
FIXED-POINT LOGIC WITH COUNTING

We now turn our attention to the polynomial calculus (). The
polynomial calculus is an important and well-studied propositional proof
system that is based
on algebraic reasoning techniques. The idea is to represent Boolean
formulas by polynomial equation systems over some field $\field F$ and to
show that, by
manipulating these polynomial equations, one can derive an inconsistent
equation such as $0 = 1$.
Analogous to the case of bounded-width resolution $\kRes$, it
possible to stratify the polynomial calculus along a parameter $k \geq
2$ to obtain polynomial-time fragments. More precisely, if we restrict the
degree of all polynomials in $\PC$-refutations to some constant $k \geq
2$, then we obtain (incomplete) fragments $\PCx k$ of the full $\PC$ in
which proofs can be found in polynomial time (more precisely, in time
One can define the polynomial calculus with respect to any underlying
field $\field F$. Throughout this section, this underlying field $\field
F$ will always be the field of rationals $\mbQ$. In the following
Section <ref>, we turn our attention to the case of finite

Another important fragment of the polynomial calculus is the so-called
monomial-PC (). This restricted variant of the full PC
was introduced by Berkholz and Grohe in [10]. Their
intention was to precisely characterise the power of a
combinatorial graph isomorphism test, the so-called Weisfeiler-Leman
algorithm [13],
in terms of propositional proof complexity.
Specifically, they proved that two graphs $G$ and $H$ can be distinguished
by the $k$-dimensional Weisfeiler-Leman algorithm if, and only
if, the $k$-dimensional monomial-PC ($\monPCx k$) can refute the
solvability of a certain system of polynomial equations $\IsoForm(G,H)$
over $\mbQ$ which encode the graph isomorphism problem for $G$ and $H$.
In this section, we analyse the power of the monomial-PC and the (full) PC
from the perspective of finite model theory.
In our main result we are going to show that both proof systems, the
monomial-PC and the full PC, have precisely the same expressive power as
fixed-point logic with counting (), which is a
natural and powerful logic of great importance in the area of descriptive
complexity theory (see Theorem <ref>).
As a consequence, the correspondence between the Weisfeiler-Leman
and the monomial-PC can be generalised to the full PC (though we have to
sacrifice the
tightness of the connection between the degree of polynomials
and the dimension of the Weisfeiler-Leman algorithm), see
Theorem <ref>.

Our proof consists of three parts.
First of all, we show that proofs in the monomial-PC can be expressed in
$\FPC$, see Subsection <ref>. This shows that
$\FOnum(\monPCx k) \leq \FPC$.
After that, we show in Subsection <ref> that
$\FPC$-iterations can be simulated using the monomial-PC. Taken together
this shows that $\FOnum(\monPCx k) = \FPC$.
As the final step, in Subsection <ref>, we show that
$\FPC$ can also express $k$-dimensional refutations in the (full)
polynomial calculus over $\mbQ$.

§.§ The Polynomial Calculus

We start with some background on the polynomial calculus and its
restricted variant, the monomial-PC.
Both systems refute the solvability of a given set of (multivariate)
polynomial equations over some  field $\mbF$ using proof rules
that manipulate such equations.
In this paper, $\mbF$ will either be the field of rationals $\mbQ$ or a
finite field $\mbF_{p^n}$ of size $p^n$ for $p \in \Primes$, where $\Primes$
denotes the set of primes and where $n \geq 1$.
We denote by $\field F[\mcX]$ the ring of polynomials in
variables $\mcX = \{ X_j : j \in J\}$, for some
index set $J$ and with
coefficients in $\mbF$.
For an “exponent”  $\alpha: J \to \mbN$ we let the monomial
$X^\alpha$ be defined as $X^\alpha = \Pi_{j \in J} X_j^{\alpha(j)}$.
Then polynomials $f \in \field F[\mcX]$ can be written as $f =
\sum_{\alpha} f_\alpha \cdot X^\alpha$ where the $f_\alpha \in \mbF$ are
coefficients from the field $\mbF$ and such that $f_\alpha \neq 0$ for
finitely many $\alpha$ only.
The degree $\deg(X^\alpha)$ of a monomial $X^\alpha$ is defined as
$|\alpha| = \sum_{j \in J}
\alpha(j)$, and the degree  of a polynomial is defined as the maximal
degree of its monomials.
A polynomial equation is an equation of the form $f = 0$ for a
polynomial $f \in \field F[\mcX]$. For better readability, we usually omit
equality “$= 0$” when we specify polynomial equations, that
is we identify polynomials $f \in \field F[\mcX]$ with the corresponding
normalised polynomial equations $f = 0$.
A system of polynomial equations is a set $\mcP = \{ f_i : i \in I
\}$
consisting of polynomials $f_i \in \field F[\mcX]$ for all $i \in I$ where
$I$ is an (unordered) index set.
A solution of $\mcP$ is a common zero $a \in \mbF^J$ of all
polynomials in $\mcP$.
In what follows, we only consider systems $\mcP = \{ f_i : i \in I
\}$ which
contain for every variable $X = X_j$, $j \in J$, the polynomial equation
$(X^2 - X) = 0$.
The axioms $(X^2 - X) = 0$ enforce that each variable $X=X_j$,
\in J$, can only take values $0$ or $1$.
These equations encode the Boolean setting (truth values) that we are
interested in.

The polynomial calculus is based on the following result from algebra
which is known as Hilbert's Nullstellensatz.
It says that the non-solvability of the system $\mcP=\{f_i:i\in I\}$ of
polynomial equations is equivalent to the existence of polynomials $g_i
\in
\field F[\mcX], i \in
I$, such that $\sum_{i \in I} g_i \cdot f_i = 1.$
The polynomials $g_i$ are called a Nullstellensatz
refutation for the system $\mcP$.
The idea of the polynomial calculus is to search for such polynomials
$g_i$ in a sequential way.

The inference rules of the polynomial calculus ($\PC$)
over the ring of polynomials $\field F[\mcX]$ are as follows:

\begin{align*}
&\text{(Multiplication)}\qquad &&\quad\frac{\, f \,}{Xf}
&&\text{ where } X \in \mcX \\
&\text{(Linear Combination)}\qquad
&& \frac{g , \, f}{ag+bf}
&& \text{ where } a, b \in \mbF
\end{align*}

The goal of the polynomial calculus is to derive with these rules,
from a collection $\mcP$ of axioms $p \in \mcP$,
the constant polynomial $1 \in \mbF[\mcX]$,  in order to prove that the
polynomials in $\mcP$ have no common zero.

The monomial-PC  ($\monPC$) is the restriction of the (full)
$\PC$ that permits the use of the multiplication rule only in the cases
where $f$ is either a
monomial or the product of a monomial and an axiom.
A polynomial equation system $\mcP$ has a refutation of
degree $k \geq 1$
in the $\PC$ (or $\monPC$)  if the constant
polynomial $1 \in \field F[\mcX]$ can be derived from $\mcP$ using only
polynomials of degree at most $k$.

The polynomial calculus, and the monomial-PC, are clearly sound and, by
Nullstellensatz, also complete proof systems. However, completeness
requires unbounded degree in refutations. In fact, as we
indicated before, the “degree of polynomials” for
the $\PC$ ($\monPC$) is a complexity measure with very similar properties
as the
“width of clauses” measure for the resolution proof system.
If we restrict the $\PC$ ($\monPC$) to polynomials of degree at most $k$,
for some fixed $k\geq 1$,
then the systems become incomplete, but admit proof search in polynomial
In what follows, whenever we speak of the monomial-PC or the (full) PC,
then we usually refer to a variant with restricted degree $k \geq 1$. If
we want to make
this constant $k$ explicit, then we
denote the corresponding proof system by $\monPCx k$ and $\PCx k$,
Another fact which we use implicitly throughout this section is
that the axioms $(X^2 - X)$ guarantee that in (monomial-)PC
proofs we can restrict ourselves to multilinear
To see this, say that we were able to derive the polynomial
$p = X^2 Y + Z$ within some (monomial)-PC proof. Of course, $p$ is not
However, we can use the axiom $(X^2- X)$ together with the “linear
combination”-rule to reduce this polynomial to the corresponding
multilinear polynomial $p' = X Y + Z$. Indeed, $p' = p - Y(X^2-X)$.
Hence, restricting to multilinear polynomials, and modifying the
multiplication rule accordingly with implicit linearisation, does not
change the power of the corresponding proof systems.
For a polynomial $p \in \field F[\mcX]$ we denote its
multilinearisation by $\ML(p)$.
So, from now on we stick to the setting of implicitly multilinearising all
polynomials which precisely captures the semantics of the polynomial
equations $(X^2 - X) =0$.

We remind the reader that in this section the underlying
field $\field F$ for the (monomial-)PC is always the field of rationals

§.§ Monomial-PC in Fixed-Point Logic with Counting

Our first aim is to show that $\FPC$ can express $\monPCx k$-refutations
over the rationals using only $\mcO(k)$ many variables.
Of course, in order to obtain such a definability result, we have to agree
on an encoding of sets $\mcP$ of
rational, multilinear polynomials
as finite relational structures.
Similar to our representation of CNF-formulas described in
Section <ref>, a natural encoding
can be based on a many-sorted structure $\mfA_\mcP$ whose universe is
partitioned into sets
of polynomials, (multilinear) monomials, variables, and rational
coefficients that occur in $\mcP$.
As usual, we represent rationals as fractions of integers using
binary encoding. Hence, $\mfA_\mcP$  provides a linear order of
sufficient length to encode these binary strings.
Again, the exact technical details  are not important, as long as the
encoding has some natural properties, such as $\FO$-definability of the
class of valid encodings.
By a slight abuse of notation, we also denote by $\monPCx k$ the class of
structures $\mfA_\mcP$ which encode a system $\mcP$ of polynomials over
$\mbQ$ which can be refuted in  $\monPC_k$.

For every $k \geq 1$, $\monPC_k \in \FPC$.

Given a set of multilinear polynomials $\mcP$ of degree at most $k$, we
consider the set $V_\mcP = \monPCx k(\mcP)$
of multilinear polynomials
which can be derived
from $\mcP$ using $\monPCx{k}$.
The first observation is that $V_\mcP$ is a $\mbQ$-linear space.
This easily follows since we can take $\mbQ$-linear combinations of
polynomials that we derived.
Now, since this vector space $V_\mcP$ only contains multilinear
polynomials of degree at
most $k$,
we can naturally associate polynomials $p \in V_\mcP$ with vectors $p \in
\mbQ^{M_k}$ where the index set $M_k$ denotes the set of all multilinear
monomials of degree at most $k$.
For fixed $k \geq 1$, this set $M_k$ is of polynomial size $n^{\mcO(k)}$.

To prove Theorem <ref> we are going to express in $\FPC$
an inductive algorithm,  that is based on a similar algorithm for
the full
polynomial calculus from [14],
for computing a generating set for the $\mbQ$-linear space
$V_\mcP$. Then, in order to see whether $\monPCx{k}$ can refute the
system $\mcP$, we simply check whether the constant polynomial $1$
is contained in $V_\mcP$, see Figure <ref>.

Set of multilinear polynomials $\mcP \subseteq \mbQ^{M_k}$

$\mcB \subseteq \mbQ^{M_k}$ such that $\langle \mcB \rangle =
\monPCx k(\mcP)$
where $\langle \mcB \rangle$ denotes the $\mbQ$-linear
subspace generated by $\mcB$

$\mcB := \{\ML(m \cdot p) \ | \ p \in \mcP, m \text{ a monomial
such that} \,\deg(\ML(m \cdot p)) \leq k\}$
Initialisation (lift all axioms in $\mcP$ up to degree $k$)

monomials $m  \in \langle \mcB \rangle$,
$\deg(m) < k$
$\mcB := \mcB \cup \{ \ML(X \cdot m) : \text{for some variable
$X$} \}$
$\mcB$ remains unchanged

$\FPC$-procedure to define generating set for $V_\mcP =
\monPCx{k}(\mcP)$

During the run of the algorithm we iteratively construct a set $\mcB
\subseteq V_\mcP$ of polynomials such that $\langle \mcB \rangle \leq
V_\mcP$. Here, $\langle \mcB \rangle$ denotes the $\mbQ$-linear subspace
generated by the polynomials in $\mcB$ (considered as $M_k$-vectors over
$\mbQ$). Moreover, we ensure that at termination we have $\langle
\mcB \rangle = V_\mcP$, see Figure <ref>.
One important point to observe is that after the initialisation step we
only add
monomials to the set $\mcB$. This closure operation is sufficient
for the monomial-PC, since, except for the given axioms in $\mcP$ of which
we take care at initialisation, we can only use the multiplication (or
lifting) rule for monomials.
Since there are only polynomially many
different monomials of degree at most $k$, for a fixed $k$, this means
the algorithm is guaranteed to terminate after a polynomial number of

It is not obvious how to express this algorithm in $\FPC$. Most
steps, such as
the representation of the set $\mcB$ and the multilinearisation of
polynomials, are easy to formalise, but there is a severe obstacle
hidden in the condition for the main loop. Here, we want to iterate, in
parallel, through all monomials $m \in \langle \mcB \rangle$. This
condition “$m \in \langle \mcB \rangle$”  translates to solving a linear
equation system over $\mbQ$.
Although it is provably impossible to express the method of Gaussian
elimination in
$\FPC$, since it requires arbitrary choices during its computation, and
$\FPC$ cannot define
the solvability of linear equation systems over finite
fields [3], it is known [18]
that $\FPC$ can indeed express solvability of
linear equation systems over the rationals, see also
Subsection <ref>.

The solvability of linear equation systems over $\mbQ$ is definable in

Using this result we can express the algorithm from Figure <ref>
in $\FPC$. In order to
complete our proof of
Theorem <ref> we just need to recall that $\monPCx k$ can
if, and only if, $1 \in \langle \mcB \rangle = V_\mcP$.
This last assertion, again, reduces to deciding the solvability of a
linear equation system over $\mbQ$ and it can thus, by
Theorem <ref>, be defined in $\FPC$.

§.§ Monomial-PC captures Fixed-Point Logic with Counting

Next we show that the monomial-PC can simulate fixed-point logic with
We first observe, however, that the logic $\FO(\monPCx k)$ does
not suffice for this purpose. This is due to the fact that $\FPC$
has access to the
second (numeric) sort, on which it can perform arbitrary polynomial-time
computations, whereas $\FO(\monPCx k)$ is
evaluated over standard single sorted input structures.
To overcome this mismatch we have to extend the logic $\FO(\monPCx k)$
to the second-sorted framework as well.
We denote this extension of $\FO(\monPCx k)$ by
$\FOnum(\monPCx k)$.
As in the case of $\FPC$, this means that formulas are evaluated over
extensions $\mfA^+$ of relational
structures $\mfA$ by a numeric sort, as defined in
Section <ref>. In particular, interpretations for the Lindström
quantifiers can make use of the second numeric sort, and we require this
capability in the proof of our following result.

For every $k \geq 2$, $\FPC \leq \FOnum(\monPCx k)$.

An elegant way to prove Theorem <ref> is to use  a
game-theoretic characterisation of $\FPC$ which was recently established
in [24].
It is based on the notion of so-called threshold games.
A threshold game is a two-player game  played on a
directed graph $G = (V,E)$ that is equipped with a
threshold function $\theta \colon V \to \mathbb{N}$.
This function satisfies that $\theta(v)\leq \delta(v)+1$ for
all $v \in V$, where $\delta(v)$ denotes the out-degree of $v$ in $G$.
Moreover, there is a designated vertex $s \in V$ at which each play
A play is a sequence of $G$-nodes that arises
according to the following rules. At the current position $v \in
V$, Player 0 first selects a set $X \subseteq vE = \{ w : (v,w) \in E\}$
with $|X| \geq \theta(v)$. Then Player 1 chooses a node $w \in
X$ and the play moves on to $w$. A player who cannot move loses. Hence
Player 0 wins at all nodes in $T_0 := \{v \in V \ | \ \theta(v) = 0\}$ and
Player 1 at all nodes in $T_1 := \{v \in V \ | \ \delta(v) <
\theta(v)\}$.

In [24] it is shown that threshold games provide
appropriate model-checking games $\Tt(\AA,\phi)$
for any finite structure $\AA$ and any formula $\phi\in \FPC$.
Since fixed-point evaluations on finite structures can be
uniformly unraveled to first-order evaluations, we can in fact assume that
the game graphs
of these threshold games are acyclic.
For any fixed -formula $\phi$, these model checking games
are polynomially bounded in the size of the input structure and can, in
be interpreted in (two-sorted) input structures using a first-order
This is related to the transformation of $\FPC$-formulas into
uniform families of polynomial-size threshold circuits, as used
for instance in [38] and [1].

For every $\FPC$-formula $\phi$ there is a
first-order interpretation $I_\phi$ which, for every finite structure
interprets in $\AA^+$ an acyclic threshold game
$\Gg(\AA,\phi)$ such that
$\mfA \models \phi$ if, and only if, Player 0 has a winning strategy for

It remains to show that the monomial-PC can define winning regions in
acyclic threshold games.
Given an acyclic threshold game $\mcG = (G = (V,E),\theta)$, we
construct an axiom system $\mcP(\mcG)$ which consists of polynomial
equations of degree at most two.
For every node $v \in V$ in the threshold  game $\mcG$, the
system $\mcP(\mcG)$ contains a variable $X_v$.
Let us denote by $W_\sigma^\mcG$ the winning region of Player $\sigma$ in
$\mcG$. Then $\mcP(\mcG)$ satisfies the following:

* if $v \in W^\mcG_0$, then $X_v = 1$ is derivable from $\mcP(\mcG)$
in $\monPCx 2$;

* if $v \in W^\mcG_1$, then $X_v = 0$ is derivable from $\mcP(\mcG)$
$\monPCx 2$;

* $\mcP(\mcG)$ is consistent; in particular, either $X_v = 1$ or
$X_v = 0$ is derivable for every $v \in V$;

If we can construct such a system $\mcP(\mcG)$ via an
$\FO$-interpretation in $\mcG$, then this completes
our proof of Theorem <ref>. In fact, it then
follows that $\FOnum(\monPCx 2)$ can define winning regions in acyclic
threshold  games: a node $v \in V$ is in the winning
region of Player 0 if, and only if, the system $\mcP(\mcG) \cup \{X_v =
0\}$ can be refuted in $\monPCx 2$.

Recall that $vE = \{ w \in V: (v,w) \in E\}$, for $v \in V$, denotes
the set of successors of $v$. Further, we let $\ns(v)$ denote the number
successors of $v$, and we let $\nws(v)$ denote the number of successors of
$v$ which
are in the winning region of Player 0, that is
$\ns(v) = | vE |$ and
$\nws(v) = | vE \cap W_0^\mcG |$.
We denote the set of non-terminal positions by $\NT = \{ v \in V : \ns(v)
The system $\mcP(\mcG)$ uses the following set of variables:

* a variable $X_v$, for every $v \in V$,

* a variable $Y_{v}^{m}$ for every $v \in \NT$,
and $0 \leq m \leq \ns(v)$,

* a variable $Z_{v}^{m}[u \mapsto j]$ for every $v \in \NT$, $1 \leq
m \leq \ns(v)$, $1 \leq j \leq m$, $u \in vE$.

The intuition is that the variables $X_v$ encode the winning regions of
both players, as described above. Moreover, the variables $Y_v^{m}$
should indicate whether $\nws(v) = m$, in the following way: if $\nws(v)
\neq m$, then $Y_v^{m} = 0$ is derivable, and if $\nws(v) = m$, then
$Y_v^{m} = 1$ is derivable.
The variables $Z_{v}^{m}[u \mapsto j]$ are auxiliary variables used to
encode this last condition, cf. [10].
The system $\mcP(\mcG)$ consists of the following axioms:

\begin{align*}
\text{(T)}\qquad &\text{For } v \in T_0:  X_v = 1  \text{ and for  } v
\in T_1:  X_v = 0 && \\
\text{(C)}\qquad
& \text{For } v \in \NT, 1 \leq m \leq \ns(v), u \in vE :
&&\sum_{j = 1}^{m} Z^m_{v}[u \mapsto j] - Y_{v}^m = 0 \\
& \text{For } v \in \NT , 1 \leq m \leq \ns(v), 1 \leq j
\leq m:
&&\sum_{u \in vE} X_u Z^m_{v}[u \mapsto j] - Y_{v}^m = 0 \\
&\text{For } v \in \NT:
&&\sum_{u \in vE} X_u \cdot Y_{v}^0 = 0 \\
\text{(E)}\qquad &
\text{For } v \in V:
(1 - X_v) - \sum_{m = 0}^{\theta(v)-1} Y_{v}^{m} = 0  \,  \text{
and  } \,
X_v \hspace{-3pt}  && \hspace{-3pt}-   \sum_{m = \theta(v)}^{\ns(v)}
Y_{v}^{m} = 0
\end{align*}

We also add for each variable $X=X_v$, $v \in V$, a syntactic dual
variable $\bar X$ together with the axiom

\[ \text{(N)}\,\, 1 - X - \bar{X} = 0.\]

These axioms enforce that each dual variable $\bar X$ takes as value $1 -
Note that the system $\mcP(\mcG)$ only contains axioms of degree at most

The system $\mcP(\mcG)$ is consistent.

We define an intended model of $\mcP(\mcG)$.
For   $X$-variables, we set $X_v := 1$, if $v \in W_0^\mcG$, and $X_v :=
if $v \in W_1^\mcG$.
For   $Y$-variables, we set $Y_{v}^{m} := 1$, if $\nws(v) = m$, and
$Y_{v}^{m} := 0$ if $m \neq \nws(v)$.
For   $Z$-variables, we set $Z_{v}^{m}[u \mapsto j] :=
0$ for all non-terminal positions $v \in V$, $u \in vE$, and $j \in \{1,
\dots, m \}$, if $m \neq \nws(v)$.
For $m = \nws(v) > 0$, we let $vE \cap W_0^\mcG = \{u_1, \dots, u_m\}$.
We then set $Z_v^{m}[u_i \mapsto j] = 1$ if $j = i$, and $Z_v^{m}[u_i
\mapsto j] = 0$ for $j \neq i$. Moreover, for $u \in vE \setminus
W_0^\mcG$, we set $Z_v^{m}[u \mapsto 1] = 1$, and $Z_v^{m}[u \mapsto j] =
0$ for $j \in \{2, \dots, m\}$.

If $v \in W_0^\mcG$, then we can derive the polynomial $X_v - 1$ (that is
the equation $X_v = 1$) from $\mcP(\mcG)$ in
$\monPCx 2$; and if $v \in W_1^\mcG$, then the polynomial
$X_v$ (that is the equation $X_v = 0$) can be derived from $\mcP(\mcG)$
in $\monPCx 2$.

We start with a small remark. Assume that we can derive $(1 - X)$   for a
variable $X = X_v$, $v \in V$. We show how to derive $W(1 - X)$
for any variable $W$.
This is clearly possible in the full polynomial calculus: we just have to
multiply by $W$. In the monomial-PC, however,
we cannot multiply $(1 - X)$ by $W$, since $(1-X)$ is neither a monomial
nor an axiom. Instead, we use our negation axioms.
Starting from $1 - X$, we can derive $\bar{X}$ by subtracting (N) from
Since (N)
is an axiom, we can multiply it by $W$; also, $\bar{X}$ is a
monomial and so we can multiply it by $W$. Thus, $W(1 - X -
\bar{X}) + W \bar{X} = W(1 - X)$ can be derived, as claimed. We make use
of this trick in the following.

Our proof is by induction on the height of the subgame rooted
at $v \in V$ (recall that $\mcG$ is acyclic).
For terminal positions $v \in V$, the assertion is immediate from
axioms (T).

Assume $v \in V$ is a non-terminal position.
Let $W_0(v) = vE \cap W_0^\mcG$ and $W_1(v) = vE \cap W_1^\mcG$.
By the induction hypothesis we know that we can derive in $\monPCx{2}$ for
every $u \in W_0(v)$ the equation $X_u = 1$ and for every $u \in W_1(v)$
the equation $X_u = 0$.

Let $m > 0$.
Consider an equation of the form
$\sum_{u \in vE} X_u Z^m_{v}[u \mapsto j] - Y_{v}^m = 0$ for $j \in \{1,
\dots, m\}$ of type (C).
We have $vE = W_0(v) \uplus W_1(v)$. For every $Z$-variable and for every
$u\in W_0(v)$ we can derive $ZX_u = Z$ in
$\monPCx 2$, and for every $u \in W_1(v)$ we can derive $ZX_u = 0$ in
$\monPCx 2$.
Hence, we can simplify these equations of type (C) as
$\sum_{u \in W_0(v)} Z^m_{v}[u \mapsto j] - Y_{v}^m = 0$ for $j \in
\{1, \dots, m\}$ in $\monPCx{2}$.

Next, we consider for every $u \in W_0(v)$ the equations
$\sum_{j = 1}^{m} Z^m_{v}[u \mapsto
j] - Y_{v}^m = 0$, again of type (C). We combine these two sets of
equations as follows:

\[ \sum_{j =1}^m \left(\sum_{u \in W_0(v)} Z^m_{v}[u
\mapsto j] - Y_{v}^m \right )
- \sum_{u \in W_0(v)} \left( \sum_{j = 1}^{m} Z^m_{v}[u \mapsto
j] - Y_{v}^m
\right) = 0.
\]

We can further simplify this equation (the variables $Z_v^m[u \mapsto
j]$ cancel out) and we get

\[ (m - \nws(v)) Y_v^m = 0.\]

Hence, for every $m > 0$, $m \neq \nws(v)$, we can derive $Y_v^m = 0$ in
Indeed, also in the case where $m = 0 < \nws(v)$ we can derive $Y_v^m = 0$.
In this case we just use the equation
$\sum_{u \in vE} X_u Y_v^0 = 0$.
Using the same arguments as above, this equation simplifies to $\nws(v)
\cdot Y_v^0 = 0$. Hence, if $\nws(v) > 0$, we can also derive $Y_v^0=0$.
Note that the two equations of type (E) can be combined to the equation
$\sum_{m=0}^{s(v)} Y_v^m = 1$.
Hence, altogether we showed the following. For all $0 \leq m \leq s(v)$ it
holds that:

* if $m = \nws(v)$, then we can derive $Y_v^m = 1$ in $\monPCx 2$;

* if $m \neq \nws(v)$, then we can derive $Y_v^m = 0$ in $\monPCx 2$.

Having this, the claim follows immediately by using the equations
of type $(E)$.

In summary, we have seen that defining the winning regions in acyclic
threshold games is an $\FPC$-complete problem, with respect
to $\FOnum$-reductions, and that the winning regions in
such games can be defined in $\FOnum(\monPCx{2})$.
Furthermore, it is easy to see that the system $\mcP(\mcG)$ can be
obtained from the game $\mcG$ by means of an $\FO$-interpretation.
This completes the proof of Theorem <ref> and, together
with Theorem <ref>, establishes our first main theorem of
this section.

For every $k \geq 2$, $\FPC = \FOnum(\monPCx{k})$.

§.§ $\FPC$-Definability of Refutations in the (Full) Polynomial

Next, we are going to show that the restriction to the monomial-PC is
not essential: in fact, $\FPC$ can also express the existence of
degree-$k$ refutations in the full polynomial calculus over $\mbQ$.
In particular, it follows that the $k$-dimensional variants $\monPCx k$
and $\PCx k$ of the
monomial-PC and the full polynomial calculus have the same
expressive (with respect to $\FOnum$-interpretations), that is for all
$k\geq 2$ we have

\[ \FOnum({\monPCx k}) = \FPC = \FOnum(\PCx{k}).\]

Our result provides an interesting new characterisation of the power of
the (full)
polynomial calculus from the perspective of finite model theory. In
particular, it allows us to use techniques from finite model theory
to answer open questions about the (relative) power of the two
variants of the polynomial calculus.
As indicated before, one example is given in Section <ref> where we
our new characterisation of the polynomial calculus to answer an open
question posed by Grohe and Berkholz in [10], see
Question <ref> and Theorem <ref>.

To prove the equivalence of $\FPC$ and $\FOnum(\PCx k)$, the first
important step is to understand why it is more difficult to
express $k$-dimensional refutations in the (full) polynomial calculus in
$\FPC$ rather than
in its restricted variant $\monPC$.
Basically, this comes down to the following problem: in order to find
proofs in the monomial-PC it suffices to decide the solvability
problem for linear equation systems over $\mbQ$ (this is a Boolean
decision problem; the output is either solvable or not
solvable). However, in order to search for proofs in the full PC we need
to express the functional problem of computing solution
spaces of linear equation system over $\mbQ$ in $\FPC$.
However, while it was known that
$\FPC$ can define the (Boolean) solvability problem over $\mbQ$, it was
not known whether solution spaces of linear equation systems over
$\mbQ$ can be expressed in $\FPC$. Luckily, as we show in
Theorem <ref>, this is indeed the case.

Let us now elaborate more on how to find refutations in the full PC.
To this end, we recall the procedure from Figure <ref> to find
$k$-dimensional proofs in the monomial-PC.
Given a set of multilinear polynomials $\mcP \subseteq \mbQ^{M_k}$ of
degree at most $k$, the idea is to construct a set $\mcB \subseteq
\mbQ^{M_k}$ of (multilinear) polynomials of degree at most $k$ which
generate (as $\mbQ$-linear combinations) the set of all polynomials
$\DeriveMonPCx k(\mcP)$ that can be derived
in the $k$-dimensional $\monPC$ (starting from the given set of
polynomials $\mcP$).
At the beginning, $\mcB$ is set to contain
all (linearised and) lifted versions $\ML(m \cdot p)$ of the given
polynomials $p \in \mcP$ up to degree $k$.
Subsequently, the set $\mcB$ is  closed under liftings by variables $X$.
More precisely, in each iteration, the set $\mcB$ is extended by
all possible
(linearised) liftings $X \cdot m$ of monomials $m$ of degree at
most $k-1$
that can be derived up to this stage, i.e. for which $m \in \langle \mcB
\rangle$ holds (here, $\langle \mcB \rangle$ denotes the set of all
polynomials that can be derived from polynomials in $\mcB$ using
$\mbQ$-linear combinations).
The crucial observation is that this simple inductive lifting step is
sufficient for the monomial-PC,  because, indeed, by its rules we are only
allowed to lift monomials and the initial polynomials $p \in \mcP$.
The set $\mcB$ is extended in this way until $\langle \mcB
\rangle$ remains stable.

In order to adapt this algorithm to the (full) PC, we need to make the
following changes.
Most importantly, instead of lifting all monomials $m  \in \langle
\mcB
\rangle$, $\deg(m) < k$, during the iteration, for the full PC we have to
take all (multilinear) polynomials $p  \in
\langle \mcB \rangle$, $\deg(p) < k$ into account, and make sure that
their liftings $X \cdot p$ are contained in $\langle \mcB \rangle$.
This is more difficult for the following two reasons.
First of all, we cannot go through all such polynomials
$p$, simply because their number is exponential in the number of
variables. To overcome this obstacle, we have to use linear-algebraic
preprocessing which enables us to lift a generating set for the set of
polynomials $p \in \langle \mcB \rangle, \deg(p) < k$, instead. Note
that this was not necessary in the setting of the monomial-PC:
here, the number of possible $k$-dimensional monomials is bounded
polynomially in
the number of variables (for fixed $k\geq 2$).
There is a second problem. During the iteration, for the monomial-PC we
could repeatedly add all lifted variants $X \cdot m$ of all
monomials $m
\in \langle \mcB \rangle, \deg(m) < k$ to our partial generating set
$\langle \mcB \rangle$. This is because the (linearised)
version of a lifted monomial remains a monomial and we just said that the
number of all $k$-dimensional monomials is polynomially bounded. Hence, we
never obtain generating sets $\mcB$ of super-polynomial
size in this way.
In contrast, for the setting of the (full) PC, assume that at some stage
during the iteration we have a small generating set $\mcC$ for the set of
polynomials $p \in \langle \mcB \rangle$ of degree at most $k-1$. If
we now lift all polynomials $p \in \mcC$ in all possible ways $X
\cdot p$, then clearly the size of the resulting set $\mcC'$
by a factor which corresponds to the number of variables (and there is no
global polynomial upper bound for $\mcC'$ as in the case of the
Hence, before each lifting step, we have to ensure that the size of the
generating set $\mcC$ of polynomials that we lift is (globally) bounded by
a polynomial. We can invoke standard linear-algebraic algorithms to
achieve this. More specifically, we construct $\mcC$ in such a way that
does not exceed $|M_k|$, that is the number of different multilinear
monomials of degree at most $k$. Note that a generating set of this size
exists, since each $\mbQ$-linear subspace of $\mbQ^{M_k}$ is of
dimension at most $|M_k|$. Moreover, as we mentioned before, $|M_k|$ is of
polynomial size for any fixed $k$.
We summarise the adapted algorithm for finding $k$-dimensional refutations
the (full) polynomial calculus in Figure <ref>.

Set of multilinear polynomials $\mcP \subseteq \mbQ^{M_k}$

$\mcB \subseteq \mbQ^{M_k}$ such that $\langle \mcB \rangle =
\DerivePC(\mcP)$.

$\mcB := \{\ML(m \cdot p) \ | \ p \in \mcP, m \text{ a monomial
such that}\, \deg(\ML(m \cdot p)) \leq k\}$
Initialisation (lift all axioms in $\mcP$)

Construct set $\mcC \subseteq \mbQ^{M_k}$ of size at most
$|M_k|$ such   that
$ \langle \mcC \rangle = \{ p \in \langle \mcB \rangle : \deg(p) < k \}$

polynomials $p  \in \mcC$
$\mcB := \mcB \cup \{ \ML(X \cdot p) : \text{for some variable
$X$} \}$
$\langle \mcB \rangle$ remains unchanged

-procedure to construct generating set $\mcB$ for the set
$\DerivePC(\mcP)$ of all polynomials that can be derived in $\PCx k$
starting from the given set of polynomials $\mcP$

To see how we can implement the algorithm from Figure <ref> in
polynomial time, let us have a closer look at the construction of the set
$\mcC$ during the iteration.
First of all note that the set $\{ p \in \langle \mcB \rangle : \deg(p) <
k \}$ is indeed a $\mbQ$-linear subspace of $\langle \mcB \rangle$ which,
in turn, is a $\mbQ$-linear subspace of $\mbQ^{M_k}$.
Hence, it is clear that a generating set $\mcC$ of size at most $|M_k|$
Moreover, we can easily obtain $\mcC$ as the solution space of a linear
equation system.
Indeed, let $M$ be the $M_k \times \mcB$-matrix over $\mbQ$ whose columns
correspond to the polynomials in $\mcB$. Then $\im(M) = \langle \mcB
\rangle$.
Hence, if we let $x$ and $p$ denote a $\mcB$-vector and an $M_k$-vector
of variables ranging over $\mbQ$, respectively, then the solution space of
the linear
equation system determined by the equation $Mx = p$ is
$\langle \mcB \rangle$ when we project it to the variables $p$.
Hence, by adding extra constraints $p(m) = 0$ for all monomials $m \in
M_k$ with $\deg(m) = k$, we obtain a linear equation system whose
solution space, projected to variables in $p$, is a generating set
for $\{ p \in \langle \mcB \rangle : \deg(p) < k \}$.
Clearly, solution spaces for such systems can be computed in polynomial

Before we discuss the $\FPC$-definability of this procedure, let us observe
that there is a small caveat with the approach above. So far, the
generating set for $\{ p \in \langle \mcB \rangle : \deg(p) < k \}$ that we
obtain is not of size at most $|M_k|$. Indeed,
by our construction, which relies on the final projection step,
the size of the generating set depends on $|\mcB|$ (because
the vector of variables $x$ is indexed by $\mcB$).
Hence, we need to make a second important observation.
Say we were able to construct an $M_k \times J$-matrix $N$ over $\mbQ$
with the property that $\im(N) = \{ p \in \langle \mcB \rangle : \deg(p) <
k \}$ (that is the columns of $N$ form a generating
set for the solution space of the above linear equation system projected to
We would like to transform this matrix $N$ into a “smaller” $M_k \times
M_k$-matrix $\hat N$ such that $\im(\hat N) = \im(N)$. This is clearly
possible simply because the dimension of the space $\im(N)$ is at most $|M_k|$.
However, the question is about how difficult it is to obtain such a
“more compact” version $\hat N$ of $N$. Specifically, for our
$\FPC$-definability proof, we need to express this “compression
transformation” in $\FPC$ as well.

Fortunately, the step from $N$ to $\hat N$ is surprisingly easy to realise.
As we will see in the following subsection, it holds that the
$(M_k \times M_k)$-matrix $\hat N  := N \cdot N^T$ has the same
image as the matrix $N$, see
Lemma <ref>. Hence, we obtain a small generating set for
$\im(N)$ by
the columns of $\hat N = N \cdot N^T$.
This shows that we can, in general, quite easily transform an arbitrary
generating set for a $\mbQ$-linear subspace of $\mbQ^{M_k}$ into a
small generating set of size at most $|M_k|$. Moreover, this
transformation only relies on simple matrix operations, such as
transposition and matrix multiplication. As such operations are well-known
to be definable in $\FPC$, see e.g.
[31], this transformation is $\FPC$-definable.

Altogether, this means that the only difficulty we face is to define
solution spaces of linear equation system over $\mbQ$ in $\FPC$.
Recall that by the result of Dawar, Grohe, Holm, and Laubner we know
that $\FPC$ can express the Boolean solvability problem of linear
systems over $\mbQ$, see Theorem <ref>.
However, this does not give direct evidence for
$\FPC$ begin able to express the more general functional problem of
defining solution spaces over $\mbQ$.
To illustrates this, consider the case of Rank
Logic () [18, 28]. It is well-known
that Rank Logic can express the
(Boolean) solvability problem for linear equation systems over finite
fields. However, using the CFI-construction (see Section <ref>), it
is not hard to show that it is impossible to define solutions of solvable
linear equation systems over finite fields in Rank Logic. This means that while
Rank Logic can define the Boolean solvability problem, it provably fails to
express the functional solvability problem for linear equation systems over
finite fields.

In contrast, as we will show in the following
Subsection <ref>, the situation for linear equation
systems over $\mbQ$ and $\FPC$ is much nicer. Indeed, we prove that $\FPC$ can
define solution spaces of linear equation systems over $\mbQ$, see
Theorem <ref>.
From this result and our preceding discussion it easily follows that the
algorithm in Figure <ref> is definable in $\FPC$. Beyond this
application, we believe that
Theorem <ref> is interesting in its own right and
might prove useful in other contexts.
Let us conclude by stating our main result of this subsection (where we rely on
the yet to be proven
Theorem <ref>).

For every $k \geq 2$, there exists an $\FPC$-formula $\phi$ with
$\mcO(k)$ many variables such that given (a structural encoding of) a
system $\mcP$ of polynomials  over $\mbQ$ as input for
the $k$-dimensional polynomial calculus of degree $k$, $\phi$ expresses
whether $\mcP$ can be refuted in $\PC_k$, that is $\phi$
defines whether $1 \in \PCx{k}(\mcP)$.

For all $k \geq 2$:

\[ \FPC = \FOnum(\monPCx k) = \FOnum(\PCx k).\]

§.§ Definability of Solution Spaces of Linear Equation Systems
over $\mbQ$

To complete our proof of Theorem <ref>, we proceed to show
that $\FPC$ can define solution spaces of linear equation systems
over $\mbQ$.
Formally, our main result in this subsection reads as follows.

There exist $\FPC$-formulas which define the following:
given (a structural encoding of) a linear equation system $M\cdot x = b$
over $\mbQ$, for $M\colon I \times J \to \mbQ$ and $b\colon I \to \mbQ$,
they express whether $M \cdot x = b$ is solvable, and in this
define (structural encodings of) a matrix $S\colon J \times J \to \mbQ$
and a vector $c: J \to \mbQ$ such that $\im(S) = \kernel(M)$ and $M \cdot
= b$, i.e. such that
$\im(S) +c $ is the solution space of $M \cdot x = b$.

In order to prove Theorem <ref>, we make use of
the following linear-algebraic properties of matrices over the
For completeness, and since it is central for our application, we
present short proofs to recall the underlying algebraic arguments.
From now on, let us fix a linear equation system $M \cdot x = b$ with
$M\colon I \times J \to \mbQ$ and $b\colon I \to \mbQ$.
The key is to consider the following matrices over $\mbQ$:

\begin{align*}
B &:= M \cdot M^T \in \mbQ^{I \times I} \\
C &:= M^T \cdot M \in \mbQ^{J \times J}.
\end{align*}

In Figure <ref> we summarise what we are going to show.

[font=] (rj) at (-3.5,0) $\mbQ^J$;
[below of=rj, node distance=0.7cm] 90$=$;
[below of=rj, node distance=1.3cm] (kerm) $\kernel(M)$;
[below of=rj, node distance=2cm] (oplusrj) $\oplus$;
[below of=rj, node distance=2.7cm] (immt) $\im(M^T)$;

[left of=kerm, node distance=1.2cm] (kerme) $=$;
[left of=immt, node distance=1.2cm] (immte) $=$;

[left of=kerm, node distance=2.4cm] (kerme) $\kernel(C)$;
[left of=immt, node distance=2.4cm] (imc) $\im(C)$;
[left of=oplusrj, node distance=2.4cm] (oplusrj2) $\oplus$;

[font=] (ri) at (3.5,0) $\mbQ^I$;
[below of=ri, node distance=0.7cm] 90$=$;
[below of=ri, node distance=1.3cm] (kermt) $\kernel(M^T)$;
[below of=ri, node distance=2cm] (oplusri) $\oplus$;
[below of=ri, node distance=2.7cm] (imm) $\im(M)$;

[right of=kermt, node distance=1.2cm] (kermte) $=$;
[right of=imm, node distance=1.2cm] (imme) $=$;

[right of=kermt, node distance=2.4cm] (kerme) $\kernel(B)$;
[right of=imm, node distance=2.4cm] (imb) $\im(B)$;
[right of=oplusri, node distance=2.4cm] (oplusrj2) $\oplus$;

[->=stealth, bend left=10] (immt) edge node[ fill=white,
anchor=center, pos=0.5,font=] $\cong$ (imm);
[->=stealth, bend left=10] (imm) edge node[ fill=white,
anchor=center, pos=0.5,font=] $\cong$ (immt);

[font=] (m) at (0.1,-1.6) $M$;
[font=] (m) at (0.1,-3.7) $M^T$;

(imc) edge [->=stealth, loop below, out=310, in=230,looseness=5]
node[ fill=white,
anchor=center, pos=0.5,font=] $\cong$ (imc);

(imb) edge [->=stealth, loop below, out=310, in=230,looseness=5]
node[ fill=white,
anchor=center, pos=0.5,font=] $\cong$ (imb);

at (-6.7,-3.5) $C$;
at (6.7,-3.5) $B$;

Linear-algebraic structure induced by the matrix $M\colon I
\times J \to \mbQ$ where $B = M \cdot M^T \colon I \times I \to \mbQ$ and
$C = M^T \cdot M\colon J \times J \to \mbQ$

* $B^T = B$ and $C^T = C$, that is $B$ and $C$ are symmetric.

* $\kernel(B) = \kernel(B^i)$ and $\kernel(C) = \kernel(C^i)$ for all
$i \geq 1$.

* $\im(B) = \im(B^i)$ and $\im(C) = \im(C^i)$ for all $i \geq 1$.

* $\mbQ^I = \kernel(B) \oplus \im(B)$ and $\mbQ^J = \kernel(C) \oplus
\im(C)$.

* $B$ is an automorphism of $\im(B)$ and $C$ is an automorphism of

The arguments for $B$ and $C$ are completely symmetric, so let us
consider the case of $B\colon I \times I \to \mbQ$.
First of all, $B^T = (M \cdot M^T)^T = M \cdot M^T = B$.
For the second claim, we proceed by induction on $i$. It is clear that
$\kernel(B) \subseteq \kernel(B^i)$ for all $i \geq 1$, so it suffices to
$\kernel(B^i) \subseteq \kernel(B)$.
For $i= 1$, the claim is trivial, so assume that $i \geq 2$ and for some
$x \in \mbQ^I$ we have $B^i x = 0$.
Then also  $B^{i-1} \cdot B^{i-1} x = 0$. Since $B^T = B$, this means that
also $x^T \cdot (B^{i-1})^T \cdot B^{i-1} x = 0$.
Hence, $|B^{i-1} x|^2 = 0$, which implies that $B^{i-1}x = 0$. We get $x
\in \kernel(B^{i-1})$ and by the induction hypothesis $x \in \kernel(B)$.

Let's consider (<ref>). Again, it is easy to see that
$\im(B^i) \subseteq \im(B)$ for all $i \geq 1$.
Now let's choose a basis $Be_1, \dots, B{e_\ell}$ for $\im(B)$ and let $i
\geq 2$. Then $B^ie_1, \dots, B^ie_\ell$ is a generating set for
We claim that $B^ie_1, \dots, B^ie_\ell$ is a basis for $\im(B^i)$ which
would prove our claim.
Indeed, assume that for some non-zero $(a_j) \in \mbQ^\ell$ we had
$\sum_j a_j \cdot B^i e_j = 0$.
Since $\kernel(B^i) = \kernel(B)$ it follows that $\sum_j a_j B e_j = 0$,
We turn our attention to (<ref>).
We have to show two things, namely that every vector in $\mbQ^I$ can be
written as a linear combination of elements in $\kernel(B)$ and $\im(B)$
that this expression is unique.
Let us start with the latter claim. Assume that $Bx +  y = 0$ for $x, y
\in
\mbQ^I$, $y \in \kernel(B)$. We have to show that $Bx = y = 0$.
From $Bx + y = 0$ we can conclude that $B^2x = 0$ since $By = 0$. Since
$\kernel(B^2) = \kernel(B)$ it follows
that $Bx = 0$ which yields $y = 0$.
To complete the proof, let $x \in \mbQ^I$.
Consider the cyclic space generated by $B$, that is $\langle \{ x, Bx,
B^2x, \cdots, B^nx \} \rangle$ where $n=|I|$. Note that $\{ x, Bx,
B^2x, \cdots, B^nx \}$ is linearly dependent.
If $x \in \im(B)$, then there is nothing to show.
Otherwise, we know that $x \not\in \langle \{ Bx, B^2x, \cdots, B^nx \}
\rangle$.
We choose a non-zero vector $(a_j) \in \mbQ^n$ such that
$\sum_{j=1}^n a_j B^jx = 0$. Let $k \geq 1$ be minimal such that $a_k \neq
Then $B^k (a_k x + \sum_{j=k+1}^n a_j B^{j-k} x) = 0$, hence $a_k x + z
\in \kernel(B^k) = \kernel(B)$ for some $z \in \im(B)$. This is what we
to show.
Finally,  (<ref>) follows from (<ref>).

* $\kernel(B) = \kernel(M^T)$ and $\kernel(C) = \kernel(M)$.

* $\im(B) = \im(M)$ and $\im(C) = \im(M^T)$.

* $M$ is an isomorphism from $\im(M^T)$ to $\im(M)$ and $M^T$ an
isomorphism from $\im(M)$ to $\im(M^T)$. In particular, $\rank(C) =
\rank(M^T) = \rank(M) = \rank(B)$.

Again, as the arguments are symmetric, we only consider the case of $B$.
For (<ref>), note that $\kernel(M^T) \subseteq \kernel(M\cdot
= \kernel(B)$ for trivial reasons.
Moreover, if $M\cdot M^T x = 0$ for some $x \in \mbQ^I$, then also $x^T M
M^T x = 0$, that is $| M^T x |^2 = 0$ which implies $M^Tx = 0$. Hence,
$\kernel(B) \subseteq \kernel(M^T)$.
For (<ref>), note that $\im(B) = \im(M \cdot M^T) \subseteq
\im(M)$, again for trivial reasons. To verify the other direction, let $x
\in \mbQ^J$ and consider the element $Mx \in \im(M)$.
By Lemma <ref>, we can write $Mx$ as $Mx = By + z$ for some
$y,z \in \mbQ^I$ and $z \in \kernel(B)=\kernel(M^T)$.
Hence $M^TMx = (M^TM)M^Ty$, that is $Cx = CM^Ty$. From this we get that
$C(x - M^Ty) = 0$. Using $\kernel(C) = \kernel(M)$, we get $M(x-M^Ty) = 0$.
This implies that $Mx = MM^Ty = By$ which proves our claim.
Finally, (<ref>) follows immediately
from (<ref>),(<ref>) and Lemma <ref>.

We are ready to establish the following central criterion for the
solvability of linear equation systems over $\mbQ$.

Let $M \cdot x = b$  be a linear equation system over $\mbQ$ where with
$M\colon I \times J \to \mbQ$ and $b \colon I
\to \mbQ$.
Let $B = M \cdot M^T$ as above. Let $n = \minimum\{|I|, |J|\}$.
Then the linear equation system $M \cdot x = b$ is solvable if, and only
if, $b$ can be written as a $\mbQ$-linear combination of vectors in
$\Gamma = \{ Bb, B^2b,
\dots, B^{n+1}b \}$, that is if $b \in \langle \Gamma \rangle$.

First, note that $\langle \Gamma \rangle \subseteq \im(B)$. Hence, if
$b \in \langle \Gamma \rangle$, then clearly the linear equation system
$M \cdot x = b$ is solvable.
For the other direction, assume that $b \in \im(M) = \im(B)$. Then for
some $c \in \mbQ^I$ we have $Bc = b$.
Let $\Delta = \{Bc, B^2c, \dots, B^{n+1}c \} = \{ b, Bb, \dots, B^nb \}$.
This set $\Delta$ is linearly dependent, because it is a subset of
and we have established before that
the dimension of $\im(B)$ coincides with $\rank(M)$ which is at most $n =
\minimum\{ |I|, |J| \}$.
It easily follows that $\langle \Delta
\rangle$ is $B$-invariant, that is $\langle B\Delta \rangle \subseteq
\langle \Delta \rangle$.
Moreover, by Lemma <ref>, $B$ is an automorphism of $\im(B)$
which implies that $\langle B\Delta \rangle = \langle \Delta
\rangle$. However, this shows that $b \in \Delta$ can be written as a
linear combination of elements in $B\Delta = \Gamma$ which proves our

Using  Lemma <ref>, it is easy to show that $\FPC$ can
define the solvability problem for linear equation systems over

Given a linear equation system $M \cdot x = b$ over $\mbQ$ for $M\colon I
\times J \to \mbQ$ and $b\colon I \to \mbQ$, we first define $B = M M^T$
as above and the ordered set of vectors
$\Gamma = \{ Bb, \dots, B^{n+1}\}$ as in  Lemma <ref>.
This can be done in $\FPC$, since matrix multiplication over $\mbQ$ is
well-known to be definable in $\FPC$, see e.g. [31].

Since $\Gamma$ is an ordered set we can use the Immerman-Vardi Theorem to
define the problem $b \in \langle \Gamma \rangle$ in $\FPC$. More
precisely, let $N$ be the $I \times \{1, \dots, n+1\}$-matrix over
$\mbQ$ whose $i$-th column is the vector $B^ib\colon I \to \mbQ$.
Then $b \in \langle \Gamma \rangle$ if, and only if, $N \cdot x = b$ is
Note that $N$ can be written as $N = B \cdot \hat N$ where $\hat N$ is
the $I \times \{1, \dots, n+1\}$ matrix whose $i$-th column is $B^{i-1}b$.
Moreover, since $B = M \cdot M^T$, we have transformed our
original system $M \cdot x = b$ into the system $M \cdot (M^T \cdot \hat
N) \cdot x = b$ which is solvable if, and only if, $M \cdot x = b$ is
Furthermore, a solution $c\colon \{ 1, \dots, n+1 \} \to \mbQ$ for $M
\cdot (M^T \cdot \hat N) \cdot x = b$ readily defines the solution $(M^T
\cdot \hat N \cdot c)\colon J \to \mbQ$ for $M \cdot x = b$

To solve the system $N \cdot x = b$ in $\FPC$, first note that $N$ has an
ordered set of columns. However, the set of rows $I$ is not ordered. To
obtain an ordered linear equation system, we can consider the
lexicographical ordering on the set of rows of $N$ induced by the linear
order on the set of columns and on $\mbQ$. This results in a linear
preorder which merges columns that are identical (such columns correspond
to repeated linear equations). By merging identical columns we obtain a
fully ordered system. By the Immerman-Vardi Theorem such systems can
be solved in $\FPC$.

We are left with the second claim of
Theorem <ref>,
namely that, given $M \cdot x = b$ with $M\colon I \times J \to \mbQ$ and
$b \colon I \to Q$, we can define in $\FPC$ a matrix $S\colon J \times
J \to \mbQ$ whose columns form a generating set for $\kernel(M)$, that is
$\im(S) = \kernel(M)$.
For this we make use of the structure induced by the linear transformation
$C = M^T M\colon J \times J \to \mbQ$ on $\mbQ^J$.

We established in Lemma <ref> that $\mbQ^J = \kernel(C) \oplus
\im(C)$ and in Lemma <ref> that $\kernel(M) = \kernel(C)$.
Hence, we can equivalently define a generating set for $\kernel(C)$ in
Let us denote by $e_j$ the $j$-th standard basis vector on $\mbQ^J$.
We can clearly define the vector $e_j\colon J \to \mbQ$ in $\FPC$ using $j
\in J$ as a parameter.
Since $\mbQ^J = \kernel(C) \oplus \im(C)$ we can write each $e_j$ uniquely
$e_j = k_j + c_j$ for $k_j \in \kernel(C)$ and $c_j \in \im(C)$.
It is easy to see that the set $\{k_j : j \in J\}$ forms a generating set
for $\kernel(C)$.
Hence, our aim is to define this set in $\FPC$.

To obtain the projections $k_j$ of $e_j$ onto $\kernel(C)$, we make use of
the fact that $\FPC$ can solve linear equation systems over $\mbQ$ and
define single solutions.
Indeed, $k_j$ is the unique vector $k_j \in \mbQ^J$ such that
$e_j = k_j + c_j$ and $Ck_j = 0$ and $Cz = c_j$ for some $c_j,z \in
\mbQ^J$ (where we treat $k_j, z, c_j$ here as $J$-vectors of variables
ranging over $\mbQ$).
Since in each solution of this system the projection onto $k_j$ is unique,
we can define $k_j$ in $\FPC$ as we saw before.
Note that in order to define these linear equation systems we use $j \in
J$ as a parameter, so we really solve $|J|$-many linear equation systems
in parallel.
Given the vectors $k_j\colon J \to \mbQ$, we can define the matrix
$S\colon J \times J \to \mbQ$ as the matrix whose $j$-th column is the
vector $k_j$. Then $\im(S) = \ker(C) = \ker(M)$.
This completes our proof of Theorem <ref>.

In fact, by going through our proof once again, one can show that
Theorem <ref> can be strengthened to the
extent that the $\FPC$-formulas only use fixed-point operators that
converge after a polylogarithmic number of steps, cf. [30].

§ DEFINABILITY OF POLYNOMIAL CALCULUS REFUTATIONS OVER FINITE

In Section <ref> we proved that fixed-point logic with counting
and the ($k$-dimensional)
polynomial calculus over $\mbQ$ have the same expressive power.
In this section we study to what extent this characterisation remains
intact if we consider the polynomial calculus not over $\mbQ$, but over
finite fields. Unfortunately, in the general
case, this
connection breaks down: it is easy to show that the problem of
solving linear equation systems
over a field $\mbF$ can be reduced (in first-order logic) to finding
in the ($k$-dimensional) $\PC$ over $\mbF$. However, $\FPC$ cannot
define the
solvability problem for linear equation systems over finite fields $\mbF$,
see [3].

Instead of giving up completely, we set out to explore
certain (interesting)
situations in which we can establish the same strong connections between
and the polynomial calculus that we discovered over $\mbQ$ also over
To identify these, we take a closer look at typical settings where
the connection breaks down, that is where we encounter linear equation
systems over finite fields that cannot be solved by $\FPC$.
To generate such hard linear equation systems, a common approach is to
use the Cai-Fürer-Immerman (CFI) construction [13].
Specifically, the CFI-construction yields for every prime $p \in
\Primes$ a family of structures $(\mfA^p_n)_{n \geq 1}$
of size $\mcO(n)$ such that the solvability problem for linear equation
systems over finite fields $\mbF$ of characteristic $p$ that are
defined in CFI-structures $\mfA^p_n$ (via $\FO$-interpretations)
cannot be expressed in $\FPC$.
Clearly, over these families of -structures $(\mfA^p_n)_{n \geq 1}$
there is no hope to
express $\PCx k$-proofs in $\FPC$ over fields $\mbF$ of characteristic $p$.

However, what happens if we consider the following slightly more
asymmetric situation. As before, we consider equation systems over a
field $\mbF$ that are interpreted
in CFI-structures $\mfA^p_n$. But, in contrast to the above, we make the
additional assumption that the characteristic $q = \characteristic(\mbF)$
of the
finite field $\mbF$ does not match the prime $p$ that was
used for the -construction, that is we assume that $q \neq p$.
In this case, as we show in our main result of this section
(Theorem <ref>), we can
express $\PCx k$-refutations in fixed-point logic with counting.
Although this result only gives limited insight into the logical
expressiveness of the polynomial calculus over finite fields, it turns out
to be extremely useful to prove lower bounds for the polynomial calculus,
as we demonstrate in Section <ref>.

This section is structured as follows.
First of all, we recall (a generalised version of) the Cai-Fürer-Immerman
construction in Subsection <ref> and we analyse automorphism
groups of -structures in Subsection <ref>.
To unfold its full power, the -construction relies on an underlying
family of highly connected graphs of bounded degree. To this end, we
recall the notion of expander graphs in Subsection <ref>.
We prove our first main technical result in
Subsection <ref> where we show that -structures over expander
graphs are homogeneous wrt. $\FPC$, which means that $\FPC$ can
describe elements (and tuples of elements) in -structures up to
automorphisms. An important consequence is that $\FPC$ can linearly order
orbits of elements (and tuples of elements) with a bounded number of
In Subsection <ref> we establish another important property
of -structures which extends homogeneity: we show that -structures
are cyclic (wrt. to $\FPC$) which means that $\FPC$ can linearly
order orbits of elements (and tuples of elements) by fixing a single
parameter in this orbit. We also show that this property is closed under
taking $\FPC$-interpretations and ordered pairs.
Building on this, we establish our key technical result in
Subsection <ref>: we show that $\FPC$ can define
solution spaces of linear equation systems over finite fields $\mbF$ that
are interpreted in cyclic background structures with the additional
assumption that the characteristic of the field $\mbF$ does not divide the
size of the (Abelian) automorphism group of the cyclic structure (we say
that such linear equation systems are cocyclic).
Finally, in Subsection <ref> we use this result in
order to prove our main Theorem <ref>: $\FPC$
express $k$-dimensional -refutations for polynomial equation systems
that are
defined in cyclic structures over finite fields $\mbF$ if this same
condition on the characteristic for $\mbF$ holds.

§.§ Cai-Fürer-Immerman Construction

For notational convenience, we introduce the -construction
only for connected (undirected) graphs $G$ which are 3-regular and
ordered. The assumption that $G$ is ordered means that additional
to the set of vertices $V = V(G)$ and the (symmetric) edge relation $E =
E(G) \subseteq V(G) \times V(G)$ we assume that $G$ contains a
linear order $\Ord \,\,\,=\, \Ord(G)$ on its set of vertices $V$.
In fact, this is the original setting as it was introduced by Cai, Fürer,
and Immerman in [13].

Let $p \in \Primes$ be a prime. For every vector $\lambda \in \mbF_p^V$ we
construct the CFI-structure $\CFIgraph{G}{p}{\lambda}$ over the
(connected and ordered) graph $G$, the finite field $\field F_p$, and
with load $\lambda$ as the following relational structure with
signature $\taucfi = \{ \preceq, R, C, I \}$ where $R$ is a ternary
relation symbol and where $\preceq, I, C$ are binary relation symbols.
The universe $A$ of the CFI-structure $\mfA = \CFIgraph{G}{p}{\lambda}$ is
$A = E(G) \times \mbF_p$.
The linear order $\Ord(G)$ on the vertex set $V(G)$ of $G$
extends to a linear order on the edge set $E(G)$.
We use this linear order on $E(G)$ to define the following
total preorder $\preceq$ on $A$: $(e,x) \preceq (f,y)$ if $e \leq
f$. Note that $\preceq$ induces a linear order on the corresponding
equivalence classes $e^p = e \times \mbF_p$. Clearly, each of these
classes $e^p$ is of size $p$.
Since $G$ is undirected every edge $e=(v,w) \in E$ comes with its
corresponding dual edge $f=(w,v)\in E$. In what follows, we use
the notation $e^{-1} = f$ to denote the dual of the edge $e \in E$.
The relations $I$ and $C$ are defined follows.

* The cycle relation $C$ defines the cyclic structure
of the additive group of $\field  F_p$ on each of the equivalence classes
More precisely,

\[ C = \bigcup_{e \in E} \{ ((e,x), (e, x+1 \text{ mod } p) )
: x \in \field F_p\}.\]

* The inverse relation $I$ relates additive inverses for
dual edges. Formally,

\[ I = \bigcup_{e \in E} \{ ( (e,x), (e^{-1}, -x) : x \in \field F_p
\}.\]

Note that while the cycle relation $C$ defines a directed cycle, the
inverse relation $I$ is symmetric. Furthermore, observe that the
relations $\preceq, C$ and $I$ are defined independently of the load
vector $\lambda$ and so do only depend on the underlying graph $G$ and
the prime field $\field F_p$.
In contrast, the CFI-relation $R=R^\lambda$ is defined using the
load vector $\lambda$ as follows.
For each $v \in V$, we let $vE \subseteq V$ denote the set of neighbours
of $v$ in $G$, that is $E(v) = \{ v \} \times vE \subseteq E$ is the set
of edges outgoing from $v$.
Since $G$ is $3$-regular we have that $|vE| = 3$ for each $v \in V$.
For $v \in V$ let $E(v) = \{ w_1, w_2, w_3 \}$ where $w_1 < w_2 < w_3$. The
CFI-relation $R^\lambda(v)$ at vertex $v$ is defined as follows:

\[ R^\lambda(v) = \{ ((w_1, x_1), (w_2, x_2), (w_3,x_3)) : x_1 + x_2 + x_3
= \lambda(v)  \}. \]

The full CFI-relation $R^\lambda$ of the structure
$\CFIgraph{G}{p}{\lambda}$ is given as $R^\lambda = \bigcup_{v \in
V} R^\lambda(v)$.

§.§ Symmetries of -Structures

It turns out that the automorphism group $\Gamma$ of a CFI-structure
$\CFIgraph{G}{p}{\lambda}$ only depends on $G$ and $p$, but not on
$\lambda$. To see this, first observe that every automorphism $\pi \in
\Gamma$ has to maintain the linear preorder $\preceq$ which means that
$\pi(e^p) = e^p$ for all $e \in E$. Moreover, $\pi$ has to maintain the
cycle relation $C$. This means that the action of $\pi$ on an
edge class $e^p$ is a cyclic shift in $\field F_p$. Let us write $\pi(e)
\in \field F_p$ to denote this cyclic shift of $\pi$ on $e^p$ for $e \in
Then, because of the inverse relation $I$, we have $\pi(e) + \pi(e^{-1}) =
Altogether this shows that

\[ \Gamma \leq \{ \pi \in \field F^E_p : \pi(e) +
\pi(e^{-1}) = 0 \text{ for } e \in E \} \leq \field F^E_p.\]

However, so far we have not taken the CFI-relation $R^\lambda$ into
Again, because of the linear preorder $\preceq$, for each $\pi \in \Gamma$
we have $\pi(R^\lambda(v)) = R^\lambda(v)$ for all $v \in V$.
Let  $v \in V$ and $vE = \{ w_1, w_2, w_3 \}$ and let
$((w_1, x_1), (w_2, x_2) , (w_3, x_3)) \in R^\lambda(v)$, that is
$x_1 + x_2 + x_3 = \lambda(v)$.
From our earlier observations we know that

\[\pi( (w_i, x_i)) =(w_i,

Hence, the condition $\pi(R^\lambda(v))=R^\lambda(v)$ implies that

\[ x_1 + \pi(v,w_1) +  x_2 + \pi(v, w_2) + x_3 + \pi(v,w_3) = \lambda(v).\]

This implies that $\pi(v,w_1) + \pi(v,w_2) + \pi(v,w_3) =
\sum_{e \in E(v)} \pi(e) = 0$. In fact, this condition is not only
necessary but also sufficient for $\pi$ to preserve
$R^\lambda(v)$. Moreover, note that all of this holds independent of what
$\lambda$ is.
Altogether this gives us a characterisation of the automorphism group
$\Gamma$ of $\CFIgraph{G}{p}{\lambda}$ as a subgroup of the vector space
$\field F_p^E$ that is determined by the following set of linear equations
in variables $\pi(e)$ for $e \in E$:

\begin{align*}
\tag{\text{Inv}}\pi(e) + \pi(e^{-1}) &=0 && \text{ for } e \in
E \label{aut-constr-inv}
\\
\tag{\text{CFI}}\pi(v) := \sum_{e \in E(v)} \pi(e)
&=0 && \text{ for
} v \in V.\label{aut-constr-CFI}
\end{align*}

More generally, we can apply each vector $\pi \in \field F_p^E$, that
satisfies the constraints (Inv), to a CFI-structure
$\CFIgraph{G}{p}{\lambda}$ and obtain a new CFI-structure over the same
underlying graph $G$.
As it turns out the resulting structure is $\CFIgraph{G}{p}{\lambda+\pi}$
where $(\lambda + \pi) (v) = \lambda(v) + \pi(v)$ for all $v \in V$.
Let us denote by $\Inv(\field F_p^E) \leq \field F_p^E$ the set of all
vectors $\pi$ that satisfy the $(\Inv)$-constraints.

For every $G=(V,E,\leq)$ (connected, ordered, $3$-regular) and each
prime $p \in \Primes$, the group $\Delta = \Inv(\field F_p^{E}) \leq
\field F_p^{E}$ acts on the set of CFI-structures over
that is on $\CFIgraph{G}{p}{\star} = \{ \CFIgraph{G}{p}{\lambda} : \lambda
\in\field F_p^V\}$, and this action partitions the set into precisely $p$
orbits (see below).

Clearly, the set $\CFIgraph{G}{p}{\star}$ has size $p^n$ where $n =
|V(G)|$. However, if we consider this set up to isomorphism, there are
only $p$ different -structures over a fixed graph $G$:

Two CFI-structures $\CFIgraph{G}{p}{\lambda}, \CFIgraph{G}{p}{\sigma} \in
\CFIgraph{G}{p}{\star}$ are isomorphic if, and only if,

\[\sum \lambda = \sum_{v \in V} \lambda (v) = \sum_{v \in V} \sigma(v) =
\sum \sigma.\]

Let us remark that, for technical convenience, we have introduced
CFI-structures as relational
structures. However, it is easy to encode them as usual (unordered)
graphs, and, in fact, this is the way in which they were originally
defined in [13]. The main step is to introduce for each
CFI-constraint $i = ((e_1, x_1), (e_2, x_2), (e_3,x_3)) \in
R^{\lambda(v)}$, $e_i \in E(v)$, $x_i \in \field F_p$, a new node
$i^{\lambda(v)}$ and to connect it to the edge nodes $(e_i,x_i) \in E(v)
\times \field F_p$
(these additional constraint nodes $i^{\lambda(v)}$ are called inner
nodes in
the original
construction of Cai, Fürer, and Immerman).
Furthermore, we can replace the linear preorder by a path of the
appropriate length and connect vertices in the edge classes to positions
on this path accordingly.
All of these simple transformation steps are clearly definable in .

There exist -interpretations
$\mcJ$ and $\mcJ^{-1}$
such that $\mcJ$ maps CFI-structures $\mfA = \CFIgraph{G}{p}{\lambda}
\in \CFIclass{\mcF}{p}$ to  graphs $\mcJ(\mfA)$ of degree $\mcO(p^2)$ and
with $\mcO(p^2 \cdot n)$ many  vertices, where $n = |V(G)|$, and such that
$\mcJ^{-1}$, which maps graphs to CFI-structures, is the inverse of $\mcJ$
in the sense that for all $\mfA \in \CFIgraph{G}{p}{\lambda}$ we have that
$\mcJ^{-1} ( \mcJ(\mfA) )$ is isomorphic to $\mfA$, that is $ \mcJ^{-1}
( \mcJ(\mfA) ) \cong \mfA$.

§.§ Expander Graphs and CFI-Classes

Let us briefly recall the definition of expander graphs based on
the exposition in [32].
In the following $G=(V,E)$ denotes an undirected $d$-regular
graph (in this paper we only consider the case $d = 3$).
For two subsets of vertices $S, T \subseteq V$ in $G$ we denote the set of
(directed) edges from $S$ to $T$ by  $E[S;T] = E \cap (S \times T)$.
The edge boundary of a set $S \subseteq V$ is $\partial S = E[S;V
\setminus S]$ and the expansion ratio $h(G)$ is defined as:

\[ h(G) = \min\limits_{\{ S : |S| \leq |V|/2 \}} \frac{|\partial S|}{|S|}.
\]

[Expander graphs]
A sequence $\mcF = \{ G_n : n \in \mathbb N\}$ of undirected $d$-regular
graphs is called a family of $d$-regular expander graphs if

* $\mcF$ is increasing, that is $|V(G_n)|$ is monotone and
unbounded, and

* $\mcF$ is expanding, that is there exists $\varepsilon > 0$
such that $h(G_n) \geq \varepsilon$ for all $n \in \mathbb N$.

For our applications in this paper we make use of the existence of a
family of
$3$-regular connected expander graphs.

There exists a family of 3-regular expander graphs $\mcF = \{ G_n : n \in
\mathbb N\}$ such that each graph $G_n$, $n \in \mathbb N$, is connected
and has $\mcO(n)$ vertices.

For the rest of this paper let us fix a family $\mcF = \{ G_n : n \in
\mathbb N\}$ of expander graphs as in the previous theorem.
Of course, we can also assume that the graphs in $\mcF$ are
ordered just by adding to each graph $G_n \in \mcF$ an arbitrary
linear order on $V(G_n)$.
From this family $\mcF$ of $3$-regular, connected, ordered expander graphs
$G_n$ with $\mcO(n)$ many vertices we construct, for every $p \in
\Primes$, the CFI-class $\CFIclass{\mcF}{p}$ consisting of
all CFI-structures over graphs from $\mcF$ that is

\[ \CFIclass{\mcF}{p} = \bigcup_{n \in \mathbb N}
\CFIgraph{G_n}{p}{\star}.\]

The CFI-problem (over $\mcF$ and $p \in \Primes$) is to
decide, given a structure
$\CFIgraph{G}{p}{\lambda} \in \CFIclass{\mcF}{p}$ whether $\sum\lambda =
0$. It was shown by Cai, Fürer, and Immerman that this problem is
undefinable in counting logic with sublinearly many variables.

For $\CFIgraph{G_n}{p}{\lambda}, \CFIgraph{G_n}{p}{\sigma}  \in
\CFIclass{\mcF}{p}$ we have

\[ \CFIgraph{G_n}{p}{\lambda} \equiv^{\Omega(n)}
\CFIgraph{G_n}{p}{\sigma}.\]

§.§ Homogeneity of -Structures

In this section we establish a key technical result:
We show that
CFI-structures (over ordered expander graphs) are
($\FPC$-)homogeneous. This means that the orbits of $k$-tuples in
CFI-structures can be uniquely described in $\FPC$ by using only $\mcO(k)$
many variables.
This is extremely useful as it implies that we can actually order the set
of orbits on $k$-tuples in $\FPC$ using only $\mcO(k)$ many variables.
To put it differently, we show that in CFI-structures over
expander graphs, $\FPC$
can describe tuples up to their automorphism type without using too many
resources (variables).
We believe that this result is of independent interest and should prove
useful in
other applications (one example is discussed in
Section <ref>).

There is a constant $\ell \geq 1$ such that for every $k \geq 1$, $p \in
\Primes$, and every $\mfA = \CFIgraph{G}{p}{\lambda} \in
\CFIclass{\mcF}{p}$ with
automorphism group $\Gamma \leq \field F_p^{E(G)}$ and every $\tup a, \tup
b \in A^k$ we have that
$(\mfA, \tup a) \equiv^{\ell \cdot k} (\mfA, \tup b)$ if, and only if,
$\Gamma(\tup a) = \Gamma(\tup b)$.

Let $1 > \varepsilon > 0$ be the expander constant corresponding to the
class $\mcF$, that is for all $G \in \mcF$ we have that $h(G) \geq
\epsilon$.
We will prove Theorem <ref> for

\[ \ell \geq \frac{12}{\epsilon}. \]

To this end, we inductively show the following for all $k \geq 0$:
For  $\mfA = \CFIgraph{G}{p}{\lambda} \in \CFIclass{\mcF}{p}$ with
automorphism group $\Gamma \leq \field F_p^{E(G)}$, every $\tup a \in
and every $a, b \in A$ such that $(\mfA, \tup a, a) \equiv^{\ell \cdot
(k+1)} (\mfA, \tup a, b)$ we can find an automorphism $\pi \in \Gamma$
such that $\pi(\tup a, a) = (\tup a, b)$.

If we have shown this, then the above theorem easily follows.
Indeed, let $\tup a, \tup b \in A^k$ such that $(\mfA, \tup a)
\equiv^{\ell \cdot k} (\mfA, \tup b)$.
We have to show that in this case $\tup a$ and $\tup b$ are in the same
orbit, i.e. $\Gamma(\tup a) = \Gamma(\tup b)$. In other words, we have to
show that every $\equiv^{\ell \cdot k}$-class on $A^k$ is a single
$\Gamma$-orbit (clearly, each such class is a union of orbits).
For the sake of contradiction, assume that $\Gamma(\tup a) \neq
\Gamma(\tup b)$.
Let $r \geq 0$, $r < k$ be maximal with respect to the following property:
there exists $\tup c \in \Gamma(\tup a)$ such that $\tup b$ and
$\tup c$ share a prefix of length $r$, that is $\tup b =(b_1, \dots,
b_r, b_{r+1}, \cdots b_k)$, and $\tup c = (b_1, \dots, b_r, c_{r+1}, \dots
c_k)$, and $b_{r+1} \neq c_{r+1}$.
But then $(\mfA, a_1, \dots, a_{r}, a_{r+1}) \equiv^{\ell \cdot k} (\mfA,
b_1, \dots, b_r, c_{r+1})$ (since $\tup a$ and $\tup c$ are in the same
orbit) and $(\mfA, a_1, \dots, a_{r}, a_{r+1}) \equiv^{\ell \cdot k}
(\mfA, b_1, \dots, b_{r}, b_{r+1})$ (by the assumption).
\[ (\mfA, b_1, \dots, b_{r}, b_{r+1}) \equiv^{\ell \cdot k}
(\mfA, b_1, \dots, b_{r}, c_{r+1}).\]

By the above proposition, we can find $\pi \in
\Gamma$ such that $\pi(b_1, \dots, b_r, c_{r+1}) = (b_1, \dots, b_r,
b_{r+1})$. This means that $\pi(\tup c) \in \Gamma(\tup a)$ is a tuple in
$\Gamma(\tup a)$ sharing a longer prefix with $\tup b$ than $\tup c$ which
leads to the desired contradiction.

Hence, let us now focus on proving the above proposition.
For this let $k \geq 0$, $\tup a \in A^k$, and $a, b \in A$ such
that $(\mfA, \tup a, a) \equiv^{\ell \cdot
(k+1)} (\mfA, \tup a, b)$ where $\mfA = \CFIgraph{G}{p}{\lambda} \in
\CFIclass{\mcF}{p}$. Recall that $\Gamma \leq \Inv(\field F_p^{E(G)})
\leq \field F_p^{E(G)}$ denotes the automorphism group of $\mfA$.
We have to show the existence of some $\pi \in \Gamma$ such that
$\pi(\tup a, a) = (\tup a, b)$.
To do this, we establish two key properties of the elements $a, b \in A$
using the fact that $(\mfA, \tup a, a) \equiv^{\ell \cdot
(k+1)} (\mfA, \tup a, b)$. Clearly, we can assume that $a \neq b$, because
the claim is trivial otherwise.

* The elements $a, b$ are in the same edge class in $\mfA$, i.e.
there exists
$e \in E(G)$ such that $a, b \in e^p = e \times \field F_p \subseteq A$.

This easily follows from the fact that each edge class $e^p$ can
be identified in counting logic by using the preorder $\preceq$ and at most
three variables (which we use to enumerate the edge classes
starting from the minimal one). Moreover, this formula does not require
access to any of the parameters from $\tup a$. Hence, a counting
logic formula with three variables could distinguish between $a$ and $b$
in $\mfA$ if they were in different edge classes. Note that $\ell \geq 12$,
so we clearly have enough variables available.

The next simple observation is that this edge class $e^p$ is
free, a property that we are going to define now.
Let $\Blocked \subseteq E(G)$ be the smallest set such that

* if $a_i \in f^p$, for some $1 \leq i \leq k$ and for $f \in E(G)$, then
$f \in \Blocked$, and

* if $f \in \Blocked$, then $f^{-1} \in \Blocked$,

We say that the edges in $\Blocked$ are blocked and the edges $E(G)
\setminus \Blocked$ are free.
For blocked edges it is straightforward to define the individual elements in
the corresponding blocked edge classes.

For every blocked edge $f \in \Blocked$ and every $c \in f^p = f \times
\field
F_p \subseteq A$, there exists a formula of counting logic $\phi(x_1,
\dots, x_k, y)$ with at most $k+2$  many
variables which defines
$c$ in $(\mfA, a_1, \dots, a_k)$, i.e. such that for every $d \in A$ we
have that $\mfA \models \phi(a_1, \dots, a_k, d)$ if, and only if, $c = d$.

First of all, assume that an edge $f \in \Blocked$ is marked
blocked because for some $1 \leq i \leq k$ we
have that $a_i \in f^p = f \times \field F_p$, i.e. we are in case
<ref>. Recall that the cycle relation $C$ defines a
directed cycle on $f^p$. Hence, using $C$ and $a_i$ as a parameter we
can define every other element $c \in f^p$ in counting logic using
the parameter $a_i$ and one additional auxiliary variable.

Secondly, assume that $f \in \Blocked$ is blocked, because $g = f^{-1} \in
\Blocked$, i.e. we are in case <ref>.
By the induction hypothesis we know that we can define in counting logic
each element in $g^p$ using $k+2$ many variables (and the
parameters in $\tup a$). Let $\phi(\tup x, y)$ be a formula defining such an
element $c \in g^p$.
Then $\psi(\tup x, y) = \exists z ( I(z,y) \wedge \phi(\tup x, z))$
is a formula of counting logic with at most $k+2$ many variables which
defines an element in $f^p$. Since $I$ is a bijection between $f^p$ and
$g^p$ we can define each element in $f^p$ in this way.

For obvious reasons, the number of blocked edges is linearly bounded
in $k$:

The number of blocked edges is linear in $k$: we have $|\Blocked|
\leq 2 k$ (or $|\Blocked| \leq k$ if we count edges as undirected).

Let us come back to our original goal.
Recall that we have to show the existence of some $\pi \in \Gamma$ such
$\pi(\tup a, a) = (\tup a, b)$ where $(\mfA, \tup a, a) \equiv^{\ell \cdot
(k+1)} (\mfA, \tup a, b)$, $a \neq b$.
With the above preparation it is now easy to see that $a$ and $b$ satisfy
the following property.

* The edge class $e^p$, $e \in E(G)$, that contains the elements
$a, b$ (see <ref>), is free, that is $e \in E(G)\setminus
\Blocked$.

This immediately follows from Lemma <ref> (note that
$k+2 \leq \ell \cdot (k+1)$).

Let us fix a free edge class $e^p$, $e \in E(G)\setminus \Blocked$.
We are going to construct an automorphism $\pi \in \Gamma$ such that
$\pi(\tup a) = \tup a$ and such that $\pi(e) = 1$, that is $\pi$ acts as
a cyclic shift by one on the edge class $e^p$.
If we can show this, then our original claim follows.
To this end, we distinguish between the following two cases.
We say that the edge $e$ lies on a free cycle, if there exist
edges $e_0=(v_0,v_1), e_1=(v_1,v_2), \dots,
e_r=(v_r,v_0)$, $r \geq 2$, such that all $v_i$, $0 \leq i \leq r$, are
distinct and such that $e = e_0$ and $e_i \in E(G) \setminus \Blocked$, $0
\leq i
\leq r$.
Indeed, if $e$ lies on such a free cycle, then we can construct an
automorphism $\pi \in \Gamma$ with the desired properties as follows:
we simply set $\pi(e_i) = 1$ and $\pi(e_i^{-1}) = -1$ for all
$0 \leq i \leq r$. Note that each of the moved
edge classes $e_i^p$ is free, so none of the elements in the tuple $\vec
a$ will occur
in any of the edge classes moved by $\pi$, that is $\pi(\tup a) = \tup a$.

Hence, the interesting case is that $e$ does not lie on a free cycle.
We show that in this case each element in the edge class
$e^p$ can be defined in counting logic by fixing elements in a
bounded number of additional edge classes (more precisely, by using at
most $\ell \cdot (k+1)$ many variables). Hence, for our original setting
this would mean that the assumption $(\mfA, \tup a, a) \equiv^{\ell \cdot
(k+1)} (\mfA, \tup a, b)$ would already imply that $a = b$.
To prove this, we strongly make use of the fact that the family $\mcF$ of
graphs from which we constructed the CFI-class $\CFIclass{\mcF}{p}$ is
an expander family. Let us formulate our claim precisely.

As above, let $\mfA = \CFIgraph{G}{p}{\lambda} \in \CFIclass{\mcF}{p}$,
$\tup a \in A^k$, $\ell \geq 12 / \varepsilon$, and let $e \in
E(G)\setminus B$ be a free edge which does not lie on a free cycle.
Then for every $b \in e^p$ there exists a formula $\phi(\tup x, y)$ of
counting logic with at most $\ell \cdot (k+1)$ many variables that
defines $b$ in $(\mfA, \tup a)$, that is for every $c \in A$ we have that
$\mfA \models \phi(\tup a, c)$ if, and only if, $c = b$.

Let us consider the subgraph $H=(W,F)$ of $G$ that is induced by the free
edges $E(G) \setminus \Blocked$. Note that since $\Blocked$ is symmetric,
$H$ is an
undirected graph.
Let $e = (v,w) \in E(G)\setminus \Blocked$ be the free edge that we
consider and let $X \subseteq
V(H)$ and $Y \subseteq V(H)$ denote
the connected components of $v$ and $w$ in the graph
\setminus e$, that is in the graph that results from $H$ by removing the
(undirected) edge $e$.
Since $e$ does not lie on a free cycle we know that $X$ and $Y$ are
Using the expander property of $G$, we now aim to bound the size of $X$
or $Y$.
Clearly, at least one of the two sets contains at most $|V(G)| / 2$ many
vertices. Without loss of generality, let us assume that $|X| \leq |V(G)|
/ 2$.
Then $|\partial X| \geq |X| \cdot \varepsilon$ since $h(G) \geq
\varepsilon$.
The important observation is that we can bound $|\partial X|$ in terms
of $k$.
Indeed, in $G$ every edge leaving the set $X$ (different from $e$) has to
be blocked, since $X$ is a connected component in $H$. Hence $|\partial X|
\leq k$.
This yields the bound of $|X| \leq k/\varepsilon$ on the size of $X$.

In conclusion, the set $X \subseteq V(G)$ in $G$ is a set of vertices of
size at most $k/\varepsilon$ such that each edge leaving $X$ is blocked
except for the single free edge $e$.
We now consider the CFI-substructure $\mfB$ of the input CFI-structure
$\mfA$ induced on the edge classes incident with vertices in $X$ where in
every blocked edge class $f^p$ we arbitrarily mark an element $c \in
f^p$ to be $c = (f,0) \in f^p$ (this choice depends on the
parameters $\tup a$).
More precisely, let $E_X = \{ e \in E(v): v \in X, e \not\in \Blocked \}$,
then the universe $B$ of $\mfB$ is the set $B= \bigcup_{e \in E_X} e^p$,
and the linear preorder $\preceq$, the cycle
relation $C$, and the inverse relation $I$ in $\mfB$ are just the
restrictions of the corresponding relations in $\mfA$ to the
subuniverse $B$.
To define the CFI-relation $R_\mfB^\lambda$ on $\mfB$ we distinguish
between the following cases. Recall that $R^\lambda = \bigcup_{v \in
V(G)} R^\lambda(v)$.
First, let us consider vertices $v \in X$ whose neighbours are all
contained in $X$. In this case we simply set $R_\mfB^\lambda(v) =
For vertices $v \in X$ for which some incident edge (classes) are blocked we
define $R_\mfB^\lambda(v)$ as follows.
Let $F\subseteq E(v)$ denote the set of blocked edges incident with $v$.
Note that $|F| \leq 2$. We fix $x^f \in f^p$ for every $f \in F$ (we
can make this choice using the parameters $\tup a$,
see Lemma <ref>).
Then we define $R_\mfB^\lambda(v)$ to be the restriction of $R^\lambda(v)$
to those tuples that contain $x^f$ for every $f \in F$.
If we recall the definition of $R^\lambda(v)$, then this intuitively
corresponds to declaring $x^f = (f,0)$. In particular, note
that the arity of $R_\mfB^\lambda(v)$ is $3-|F|\geq 1$.
Finally, the CFI-relation $R_\mfB^\lambda$ in $\mfB$ is defined as
$R_\mfB^\lambda = \bigcup_{v \in X}{R^\lambda(v)}$.

If follows from our preparations that $\mfB$ can be defined in
$\mfA$ by using a parametrised, one-dimensional interpretation $\mcI(\bar
x)$ in counting logic, i.e. $\mcI(\mfA, \tup a) = \mfB$.
Moreover, $\mcI$ can be constructed by using, as a rough estimate, at most
$k + 6$ many variables. The most important thing to observe is that we
can use Lemma <ref> in order to fix elements in all
blocked edge classes as required.

We now want to argue that every possible automorphism $\pi \in \field
F_p^{E_X}$ of $\mfB$ will fix the edge class $e^p$ (recall that $e$
the single free edge $e$ that leaves the set $X$).
Recall that the inverse constraints (<ref>) enforce that
for each pair of dual edges $f, g \in E_X$ we have $\pi(f) + \pi(g) = 0$.
Note that for each edge $f \in E_X$ we have $f^{-1} \in E_X$ except for
the single
edge $e$ for which $e^{-1} \not\in E_X$. Hence $\sum_{f \in E_X} \pi(f) =
\pi(e)$.
Moreover, recall that the CFI-constraints (<ref>) enforce
that for each $v \in X$ we have $\sum_{f \in E_X(v)} \pi(f) = 0$.
Hence, $\sum_{v \in X} \sum_{f \in E_X(v)} \pi(f) = 0$.
Since $\sum_{f \in E_X} \pi(f) = \sum_{v \in X} \sum_{f \in E_X(v)}
\pi(f)$ we
conclude that $\pi(e) = 0$, that is $\pi$ fixes the edge class $e^p$, as

It follows that in $\mfB$ every element $x \in e^p$ can be defined
in counting logic by using roughly $|E_X| + 6$ many variables. Indeed, for
some $c \in e^p$, we can use $|E_X|$ many variables to fix elements in all
other edge class and then describe the isomorphism type of the structure
$(\mfB,c)$. Since each $c \in e^p$ is in a singleton orbit, these
isomorphism types will be different for all elements $c \in e^p$.
Note that $|E_X| + 6 \leq 3k / \varepsilon + 6$.
If we translate the resulting formulas back to $\mfA$ via $\mcI(\tup x)$,
then we obtain a formula in counting logic that defines $c \in e^p$ in
$\mfA$ and which uses at most $3k / \varepsilon + 6 + k + 6 \leq 4k /
\varepsilon + 12 \leq (12k + 12) / \varepsilon \leq \ell \cdot (k+1)$ many

This completes the proof of Theorem <ref>.

For $\ell \geq 1$, we say that a structure $\mfA$ with automorphism group
$\Gamma$ is $\ell$-homogeneous if for all $k \geq 1$ and all
$k$-tuples $\tup a, \tup b \in A^k$ we have that

\[ (\mfA, \tup a) \equiv^{\ell \cdot k} (\mfA, \tup b) \text{ if, and only
if, } \Gamma(\tup a) = \Gamma(\tup b).\]

Moreover, we say that a class $\mcK$ of structures is homogeneous
there is an $\ell \geq 1$ such that each structure $\mfA \in \mcK$ is

The class of CFI-structures $\CFIclass{\mcF}{p}$ is homogeneous.

As mentioned before, an important consequence of homogeneity is that
$\FPC$ can (uniformly)
define a total preorder on the set $A^k$, for each $k \geq 1$, which
orders $k$-tuples up to orbits. Moreover, the number of variables
required by such an $\FPC$-formula is linear in $k$.
To see this, we make use of the well-known fact that for every $\ell \geq
there exists an $\FPC$-formula $\Typ{\ell}(\tup x, \tup y)$ with
$\mcO(\ell)$ many variables which defines on each input structure $\mfA$ a
linear preorder on $A^\ell$ which distinguishes between all pairs of tuples
$\tup a, \tup b \in A^\ell$ for which $(\mfA, \tup a) \not\equiv^\ell (\mfA,
\tup b)$ holds, see e.g. [38]. That is $\Typ \ell(\tup x, \tup y)$
defines in each input structure
$\mfA$ a linear order on the set $\{ [\tup a]_{\equiv^\ell} : \tup a
\in A^\ell\}$ consisting of $\equiv^\ell$-equivalence classes
$[\tup a]_{\equiv^\ell} = \{ \tup b \in A^\ell: (\mfA, \tup a)
\equiv^\ell (\mfA,\tup b) \}$ for $\tup a \in A^\ell$.
Of course, we can also use the formula $\Typ {\ell}(\tup x, \tup y)$
to define the corresponding preorder on $k$-tuples for lengths $1
\leq k < \ell$ (a common approach is to extend $k$-tuples to $\ell$-tuples
by repeating the last component).
We denote the corresponding -formula by $\Typk{\ell}{k}(\tup x, \tup
y) = \Typk{\ell}{k}(x_1, \dots, x_k, y_1, \dots, y_k)$.

Let $\mfA$ be $\ell$-homogeneous with automorphism group $\Gamma$. Then
the -formula $\Typk{\ell\cdot
k}{k}(\tup x, \tup y)$ defines a total preorder $\preceq$ on $A^k$
that identifies $k$-tuples which are in the same orbit. In particular,
$\Typk{\ell\cdot k}{k}(\tup x, \tup y)$ induces a linear order on the set
of orbits of $k$-tuples $\{ \Gamma(\tup a) : \tup a \in A^k\}$.

§.§ CFI-structures are Cyclic

In Section <ref> we proved that the CFI-classes
$\CFIclass{\mcF}{p}$ are homogeneous, which by Theorem <ref>
implies that $\FPC$ can order
$k$-tuples in structures $\mfA \in \CFIclass{\mcF}{p}$ up to orbits using
only $\mcO(k)$ many variables.
In this subsection we go one step further and show that, as a result of
the algebraic properties of the automorphism groups of CFI-structures,
each individual orbit of $k$-tuples can be linearly ordered in fixed-point
logic with counting
by fixing a single $k$-tuple from this orbit as a parameter (and, again, by
using $\mcO(k)$ many variables only).
Furthermore, we are going to show that this key property of CFI-structures
remains intact if we apply logical transformations.
Intuitively, our results show that CFI-structures come quite close to
structures: in $\FPC$, one can preorder the elements of
CFI-structures up to orbits,and, secondly,
each individual orbit can be totally ordered by fixing a
single element as a parameter. Note, however, that this does not
mean that we can order the full CFI-structure,
since this would require to
fix a parameter in each of the orbits at the same time. Indeed,
Theorem <ref> implies that CFI-structures can not be
ordered in $\FPC$ if we restrict ourselves to formulas with a sublinear
number of variables.

Recall that, for $1 \leq k \leq \ell$, the formulas
$\Typk{\ell}{k} = \Typk{\ell}{k}(\tup x,
\tup y)$ define a total preorder that distinguishes $k$-tuples up to
In what follows we make use of parametrised versions of these
More precisely, for a parameter tuple $\tup z$ of length $r \geq 0$ we
$\Typk{\ell}{k}[\tup z](\tup x, \tup y)$ to denote the formula
$\Typk{\ell}{r + k}(\tup z \tup x, \tup z \tup y)$ (of course this only
makes sense if $r+k \leq \ell$).
Note that, again, this formula orders $k$-tuples up to
$\equiv^\ell$-equivalence, but now we consider $\equiv^\ell$-equivalence
with respect to the additional parameter tuple $\tup z$.
Hence for every structure $\mfA$ and every $\tup c \in A^r$ we have that
the linear preorder defined by $\Typk{\ell}{k}[\tup c]$ in $\mfA$ refines
the linear preorder defined by $\Typk{\ell}{k}$ in $\mfA$.
Note that, in particular, the tuple $\tup c$ will always be in a singleton
class according to the preorder $\Typk{\ell}{k}[\tup c]$.
Note further that for the special case $r = 0$ we just obtain the formula

Given a structure $\mfA$ with automorphism $\Gamma$, we denote for
a parameter $\tup c \in A^r$ by $\Gamma_{\tup c} \leq \Gamma$ the
stabiliser subgroup of the tuple $\tup c$, i.e. the
group of all $\pi \in \Gamma$ such that $\pi(\tup c) = \tup c$.

A structure $\mfA$ with automorphism group $\Gamma$ is called
$\cyc{\ell}{p}$, for $\ell \geq 1$ and $p \in \Primes$, if the
following holds for every $k \geq 1$:

* $\Gamma$ is an Abelian $p$-group. In particular, for every
$k$-tuple $\tup
a \in A^k$, the size of the
orbit $\Gamma(\tup a)$ of $\tup a$ is a $p$-power, that is $|\Gamma(\tup
a)| = p^n$
for some $n \geq 0$.

* For every $\tup c \in A^r$, $r \geq 0$, the
$\Typk{\ell \cdot (k+r)}{k}[\tup c]$ defines a total preorder on
$A^k$ such that two tuples $\tup a, \tup b \in A^k$ are incomparable if,
and only if, $\Gamma_{\tup c}(\tup a) = \Gamma_{\tup c}(\tup b)$.
Note that for  $r = 0$ we obtain $\ell$-homogeneity as a special case.

We say that a class $\mcK$ of structures is $\cyclp$ if every
structure $\mfA \in \mcK$ is $\cyclp$.

Actually, if in the above definition, we would only include
item <ref>, then the resulting notion of
$\cyclp$ structures would not be very interesting: it would collapse to
notion of $\ell$-homogeneity, see Theorem <ref> below.
However, in combination with condition <ref>, we get a
remarkable effect:

In Definition <ref>, we can add the following to
item <ref> without changing the resulting notion:
Assume that $r \leq k$. Then the preorder defined by $\Typk{\ell \cdot
(k+r)}{k}[\tup c]$ induces a
linear order on the orbit $\Gamma(\tup c)$ of the parameter $\tup c$.

This follows from the fact that,
by <ref>,  $\Gamma$ is an Abelian group (and so the
induced group action on the orbit is regular).
More explicitly, assume that for some $\pi \in \Gamma$ and
$(\tup c, \tup a) \in \{ \tup c \} \times \Gamma(\tup c)$ it holds that
$\pi(\tup c, \tup a) = (\tup c, \tup b)$.
Choose $\sigma \in \Gamma$ such that $\sigma(\tup a) = \tup c$.
Then $\pi(\sigma(\tup a)) = \tup c$. Since $\Gamma$ is Abelian, it follows
that $\sigma(\pi(\tup a)) = \tup c$. Hence $\pi(\tup a) = \tup a$, which
yields $\tup a = \tup b$.
Hence, it follows that for every $\tup a \in \Gamma(\tup c)$ we have
$|\Gamma_{\tup c}(\tup a)| = 1$.
Having this, item <ref> implies that $\Typk{\ell
\cdot (k+r)}{k}[\tup c]$ defines a
linear order on $\{ \tup c \} \times \Gamma(\tup c)$, as claimed.

Let $\mfA$ be $\ell$-homogeneous and assume that the automorphism group
$\Gamma$ of $\mfA$ is an Abelian $p$-group. Then $\mfA$ is $\cyclp$.