# Separating LREC from LFP††thanks: Research funded in part by EPSRC grant
EP/S03238X/1.

Anuj Dawar and Felipe Ferreira Santos
Department of Computer Science and Technology
University of Cambridge.
<EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract

$\textsf{LREC}_{=}$ is an extension of first-order logic with a logarithmic
recursion operator. It was introduced by Grohe et al. and shown to capture the
complexity class $\mathrm{L}$ over trees and interval graphs. It does not
capture $\mathrm{L}$ in general as it is contained in FPC—fixed-point logic
with counting. We show that this containment is strict. In particular, we show
that the path systems problem, a classic $\mathrm{P}$-complete problem which
is definable in LFP—fixed-point logic—is not definable in $\textsf{LREC}_{=}$.
This shows that the logarithmic recursion mechanism is provably weaker than
general least fixed points. The proof is based on a novel Spoiler-Duplicator
game tailored for this logic.

##  1 Introduction

The founding result of the subject of descriptive complexity is Fagin’s
characterization of $\mathrm{NP}$ as the class of properties definable in
existential second-order logic [6]. Similar characterizations for complexity
classes below $\mathrm{NP}$ are not known and remain an active area of
investigation. Much attention has been devoted to the question of whether
there is a logic for $\mathrm{P}$, and this is often said to be the central
open question of descriptive complexity. Perhaps less well known but still
wide open is the question of whether there is a logic giving a descriptive
characterization of $\mathrm{L}$—the class of properties of finite structures
decidable deterministically in logarithmic space.

Immerman established logical characterizations of $\mathrm{P}$ and
$\mathrm{L}$ on _ordered_ structures. The former is given by the properties
definable in LFP—the extension of first-order logic with a least fixed-point
operator (a result obtained independently by Vardi)—and the latter by DTC—the
extension of first-order logic with a deterministic transitive closure
operator. These logics are known to be strictly weaker than the corresponding
complexity classes in the absence of a built-in order (see [14] for details).
Moreover, on unordered structures, it is known that the expressive power of
DTC is strictly weaker than that of LFP [7], whereas the corresponding
question for ordered structures is equivalent to the separation of
$\mathrm{L}$ from $\mathrm{P}$.

Since the simplest properties separating LFP and DTC from the complexity
classes $\mathrm{P}$ and $\mathrm{L}$ respectively are counting properties,
there has also been much interest in the extensions of these logics with
counting mechanisms. The logic FPC—fixed-point logic with counting—is widely
studied (see [3] for a brief introduction). Though it is known to be strictly
weaker than $\mathrm{P}$ by a celebrated result of Cai, Fürer and Immerman
[2], it gives a robust definition of the class of problems in $\mathrm{P}$
which are symmetrically solvable [1] and captures $\mathrm{P}$ on a wide range
of graph classes. Most significantly, Grohe has proved that any polynomial-
time property of graphs that excludes a fixed graph as a minor is definable in
FPC [10]. Results showing that FPC captures $\mathrm{P}$ on a class of
structures $\mathcal{C}$ (including Grohe’s theorem) are typically established
by showing that a polynomial-time canonical labelling algorithm on the class
$\mathcal{C}$ can be implemented in FPC. Such results were established for
specific classes of graphs such as trees [15] and graphs of bounded tree-width
[9] before Grohe’s theorem which supersedes them all.

The situation for logics capturing $\mathrm{L}$ is less clear-cut, even for
classes of structures where it is known that logarithmic-space canonical
labelling algorithms are possible. For instance, Etessami and Immerman [5]
showed that the extension of DTC with counting fails to capture $\mathrm{L}$
even on trees. What this suggests is that the weakness of DTC is not just in
the lack of a means of counting but that the recursion mechanism embodied in
the deterministic transitive closure operator is too weak. An interesting
suggestion to remedy this is in the logic LREC introduced in [11], which
incorporates a rich recursion mechanism which can still be evaluated within
logarithmic space. To be precise, the paper introduces two versions of the
logic, one called LREC and the second $\textsf{LREC}_{=}$. While the first is
shown to be sufficient to capture the complexity class $\mathrm{L}$ on trees,
it is the latter that is the more robust logic. In particular,
$\textsf{LREC}_{=}$ properly extends LREC in expressive power, is closed under
first-order interpretations and (unlike LREC) can express undirected
reachability. Moreover, $\textsf{LREC}_{=}$ has also been shown to capture
$\mathrm{L}$ on other interesting classes of structures [13].

It is known that $\textsf{LREC}_{=}$ does not capture $\mathrm{L}$ on all
graphs. In particular, $\textsf{LREC}_{=}$ is included in FPC and the CFI
construction that separates FPC from $\mathrm{P}$ can be suitably padded to
give a separation of $\textsf{LREC}_{=}$ from $\mathrm{L}$ [8]. While Grohe et
al. proved that LREC is properly contained in FPC (for instance, it cannot
express reachability on undirected graphs), the question was left open for the
stronger logic $\textsf{LREC}_{=}$. We settle this question in the present
paper. That is, we prove that the expressive power of $\textsf{LREC}_{=}$ is
strictly weaker than FPC. Indeed, we show that the _path systems problem_
(PSP), a natural $\mathrm{P}$-complete problem that is expressible in LFP
(even without counting) is not expressible in $\textsf{LREC}_{=}$. The result
is established by first defining an Ehrenfeucht-style pebble game for the
$L$-recursion quantifier used in the logic $\textsf{LREC}_{=}$ and then
deploying it on an intricate class of instances of PSP. Describing the winning
Duplicator strategy in the game is challenging and takes up the bulk of the
paper.

##  2 Preliminaries

We assume that the reader is familiar with the definitions of the basic logics
used in finite model theory, in particular first-order logic FO, fixed-point
logic LFP and their extension swith coungint, FOC and FPC respectively. These
definitions can be found in standard textbooks [4, 16]. We consider
vocabularies with relation and constant symbols, which we call _relational
vocabularies_ for short. Formulas in a vocabulary $\sigma$ are interepreted in
finite $\sigma$-structures. We often use Fraktur letters
$\mathfrak{A},\mathfrak{B},\ldots$ for structures and the corresponding Roman
letter $A,B,\ldots$ to denote the universe of the structure.

In the case of logics with counting, such as FOC and FPC, the interpretation
also involves a _number domain_. The logic allows for two kinds of variables
(and more generally, two kinds of terms) which range over elements and numbers
respectively. Thus, we consider a $\sigma$-structure $\mathfrak{A}$ to be
extended with a domain of non-negative integers up to the cardinality of
$\mathfrak{A}$. Element variables are interpreted by elements of
$\mathfrak{A}$ and number variables by elements of the number domain. We write
$\mathcal{N}(A)$ to denote the number domain associated with the structure
$\mathfrak{A}$. This can be identified with the set $\\{0,\ldots,|A|\\}$ and
we assume this is disjoint from the set $A$. The logics include a counting
operator and we assume a normal form where every occurrence of the counting
operator is in a formula of the form $[\\#x\varphi]=\nu$ where $\nu$ is a
number variable. This formula is to be read as saying that the number of
elements $x$ satisfying $\varphi$ is $\nu$.

Any formula in any of the logics defines a _query_. If $\varphi$ is a formula
in vocabulary $\sigma$ and $\vec{x}$ is an $m$-tuple of element variables such
that all free variables of $\varphi$ are among $\vec{x}$, then $\varphi(x)$
defines an _$m$ -ary query_. This is a map taking each $\sigma$-structure
$\mathfrak{A}$ to an $m$-ary relation $\varphi^{\mathfrak{A}}$ on the universe
of $\mathfrak{A}$ containing the tuples $\vec{a}$ such that
$\mathfrak{A}\models\varphi[\vec{a}]$. If $m=0$ and so $\varphi$ is a
sentence, we call the query a _Boolean query_. A Boolean query is often
identified with a class of $\sigma$-structures. Note that the query is not
completely specified by the formula $\varphi$ alone, but rather by the formula
along with the tuple of variables $\vec{x}$. In particular the order on the
variables is given by the tuple.

To allow for formulas which may also have free number variables, we consider
_numerical queries_. An $m$-ary numerical query is a map $Q$ that takes any
$\sigma$-structures $\mathfrak{A}$ to a relation $Q(\mathfrak{A})\subseteq
A^{m}\times\mathbb{N}$ and is invariant under isomorphisms. The last condition
means that if $\eta:A\rightarrow B$ is an isomorphism from $\mathfrak{A}$ to
$\mathfrak{B}$, then $(\vec{a},n)\in Q(\mathfrak{A})$ if, and only if,
$(\eta(\vec{a}),n)\in Q(\mathfrak{B})$. Such queries arise quite naturally. As
an example, the function that takes a graph $G$ to the number of connected
components in $G$ is a $0$-ary numerical query. The function taking a graph
$G$ to the set of pairs $(a,n)$ where $a$ is a vertex in $G$ and $n$ the
number of vertices in the connected component of $a$ is a $1$-ary numerical
query.

Suppose $\varphi$ is a formula of a logic with counting, such as FOC or FPC,
with free variables among $\vec{x}$, where $\vec{x}$ contains $m_{1}$ element
variables and $m_{2}$ number variables. Without loss of generality we assume
all element variables appear in $\vec{x}$ before the number variables.
Interpreted in a structure $\mathfrak{A}$, the formula $\varphi$ defines a
relation of mixed type: a subset of $A^{m_{1}}\times\mathcal{N}(A)^{m_{2}}$.
We treat the tuples of numbers as coding positive integers in a natural way.
So, suppose $n=|A|$ and therefore $\mathcal{N}(A)=\\{0,\ldots,n\\}$. For a
tuple $\vec{r}=(r_{1},\ldots,r_{m_{2}})$ we write $\langle\vec{r}\rangle$
denote the number

$\sum\limits_{i=1}^{m_{2}}(n+1)^{i-1}r_{i}.$

In this way, we can see $\varphi$ as defining an $m_{1}$-ary numerical query
which takes $\mathfrak{A}$ to the set
$\\{(\vec{a},\langle\vec{r}\rangle)\mid\mathfrak{A}\models\varphi[\vec{a},\vec{r}]\\}$.

###  2.1 Generalized Quantifiers and Operators

In the next subsection we define the logics LREC and $\textsf{LREC}_{=}$ which
were introduced by Grohe et al. [12]. They were originally defined as an
extension of first-order logic with a new kind of recursion operator called
$L$-recursion, designed to be computable in logspace. We present an equivalent
formulation through a variation of generalized quantifiers in the style of
Lindström. To do this, we first briefly review interpretations and generalized
quantifiers. In what follows, fix a logic $\mathcal{L}$, which can be any of
the logics FO, FOC, LFP or FPC. Whenever we refer to formulas, this is to be
read as formulas of $\mathcal{L}$.

Given two relational vocabularies $\sigma$ and $\tau$ and a positive integer
$d$, where $\tau=(R_{1},\ldots,R_{s})$ contains no constant symbols, an
interpretation of $\tau$ in $\sigma$ of dimension $d$ is a sequence
$\mathcal{I}$ of formulas

$(\delta(\vec{x},\vec{w}),\varepsilon(\vec{x},\vec{y},\vec{w}),\varphi_{R_{1}}(\vec{z}_{1},\vec{w}),\ldots,\varphi_{R_{s}}(\vec{z}_{s},\vec{w})),$

where $\vec{x}$ and $\vec{y}$ are tuples of variables of length $d$, and each
$\vec{z}_{i}$ is a tuple of variables of length $dr_{i}$ where $r_{i}$ is the
arity of the relation symbol $R_{i}$. The variables $\vec{w}$ are the
_parameter variables_. Note that all tuples of variables may contain both
element variables and number variables.

Let $\mathfrak{A}$ be a $\sigma$ structure and $\vec{p}$ be an interpretation
for the parameter variables $\vec{w}$. The interpretation $\mathcal{I}$
associates a $\tau$-structure $\mathfrak{B}$ to $\mathfrak{A},\vec{p}$ if
there is a map $h$ from
$\\{\vec{a}\in(A\cup\mathcal{N}(A))^{d}\mid\mathfrak{A}\models\delta[\vec{a},\vec{p}]\\}$
to the universe $B$ of $\mathfrak{B}$ such that: (i) $h$ is surjective onto
$B$; (ii) $h(\vec{a}_{1})=h(\vec{a}_{2})$ if, and only if,
$\mathfrak{A}\models\varepsilon[\vec{a}_{1},\vec{a}_{2},\vec{p}]$; and (iii)
$R^{\mathfrak{B}}(h(\vec{a}_{1}),\dots,h(\vec{a}_{k}))$ if, and only if,
$\mathfrak{A}\models\varphi_{R}[\vec{a}_{1},\dots,\vec{a}_{k},\vec{p}]$. Note
that an interpretation $\mathcal{I}$ associates a $\tau$-structure with
$\mathfrak{A},\vec{p}$ only if $\varepsilon$ defines an equivalence relation
on $(A\cup\mathcal{N}(A))^{d}$ that is a congruence with respect to the
relations defined by the formulaa $\varphi_{R}$. In such cases, however,
$\mathfrak{B}$ is uniquely defined up to isomorphism and we write
$\mathcal{I}(\mathfrak{A},\vec{p})=\mathfrak{B}$.

There are many kinds of interpretation that are defined in the literature. The
ones we have defined here are fairly generous, in that they allow for
_relativization_ , _vectorization_ and _quotienting_. The first of these means
that the universe of $\mathcal{I}(\mathfrak{A})$ is defined as a subset of
$(A\cup\mathcal{N}(A))^{d}$ rather than the whole set. The formula $\delta$ is
the relativizing formula. Vecotorization refers to the fact that $d$ can be
greater than $1$ and so $\mathcal{I}$ can map $\sigma$-structures to
structures that are polynomially larger, and quotienting refers to the fact
that the universe is obtained by quotienting with the congruence relation
defined by $\varepsilon$.

Let $K$ be an isomorphism-closed class of $\tau$-structures (or equivalently a
Boolean query). A standard way of extending any logic $\mathcal{L}$ to obtain
a minimal extension $\mathcal{L}[K]$ in which the Boolean query $K$ can be
expressed is to adjoin to $\mathcal{L}$ the Lindström quantifier $Q_{K}$,
corresponding to $K$ (see [4, Chapt. 12]). This allows us to write formulas of
the form $Q_{K}\mathcal{I}$ where $\mathcal{I}$ is an interpretation as above.
The quantifier $Q_{K}$ binds the variables
$\vec{x},\vec{y},\vec{z}_{1},\ldots,\vec{z}_{s}$ appearing in $\mathcal{I}$ so
the free varialbles of $Q_{K}\mathcal{I}$ are $\vec{w}$. The formula
$Q_{K}\mathcal{I}$ is true in a $\sigma$-structure $\mathfrak{A}$ with an
intepretation $\vec{p}$ for the free variables if, and only if,
$\mathcal{I}(\mathfrak{A},\vec{p})$ is in $K$.

We generalize such quantifiers to queries that are not necessarily Boolean. In
general, consider an $m$-ary numerical query $K$ over $\tau$-structures. We
define $\mathcal{L}[K]$, the extension of the logic $\mathcal{L}$ with an
operator for $K$ as follows. Let
$\mathcal{I}=(\delta(\vec{x},\vec{w}),\varepsilon(\vec{x},\vec{y},\vec{w}),\varphi_{R_{1}}(\vec{z}_{1},\vec{w}),\ldots,\varphi_{R_{s}}(\vec{z}_{s},\vec{w}))$
be an interpretation of $\tau$ in $\sigma$ of dimension $d$. Let $\vec{u}$ be
a tuple of variables of length $md$ and $\vec{s}$ a tuple of number terms.
Then,

$[{Q_{K}}_{\vec{x},\vec{y},\vec{z}_{1},\ldots,\vec{z}_{s}}\mathcal{I}](\vec{u},\vec{s})$

is a formula with free variables $\vec{w},\vec{u},\vec{s}$. This formula is
true in a $\sigma$-structure $\mathfrak{A}$, with an interpretation of
$\vec{p}$ for $\vec{w}$, $\vec{a}$ for $\vec{u}$ and $\vec{r}$ for $\vec{s}$
if, and only if,

$([\vec{a}]_{\varepsilon},\langle\vec{r}\rangle)\in
K(\mathcal{I}(\mathfrak{A},\vec{p})).$

Here, $[\vec{a}]_{\varepsilon}$ denotes the $m$-tuple of elements of
$\mathcal{I}(\mathfrak{A},\vec{p})$ obtained by taking the equivalence classes
of the $m$ $d$-tuples that make up $\vec{a}$ under the equivalence relation
defined by $\varepsilon$.

###  2.2 LREC =

In this subsection we define $\textsf{LREC}_{=}$, the logic in which we prove
the inexpressibility result. We define the logic as an extension of FOC by
means of a generalized operator in the sense of Section 2.1 above. This
definition is superficially different from that of Grohe et al. [11] where it
is defined as a restricted fixed-point operator, but the two definitions are
easily seen to be equivalent.

We first define a unary numeric query $\chi$ on a class of _labelled_ graphs.
These are directed graphs $G=(V,E)$ together with a labelling $C$ that gives
for each vertex $v\in V$ a set of numbers $C(v)\subseteq\mathcal{N}(V)$. For
each such $(G,C)$ we define $\chi(G,C)\subseteq V\times\mathbb{N}$. To do
this, we first introduce some notation. For any binary relation $R\subseteq
A^{2}$, and $a\in A$, let $aR$ denote the set $\\{b\in A\mid(a,b)\in R\\}$ and
$Ra$ denote $\\{b\in A\mid(b,a)\in R\\}$. Then $\chi$ is defined by recursion
on $l$ by the following rule:

$(u,\ell)\in\chi(G,C):\iff\ell\geq 0\text{ and }|\\{v\in
uE\mid(v,\lfloor(\ell-1)/|Ev|\rfloor)\in\chi(G,C)\\}|\in C(u).$

The logic LREC is the closure of FOC with a generalized operator for computing
the numeric query $\chi$. Note that to get this formally, we have to extend
the idea of interpretation we had earlier to be able to produce a _labelled_
graph. In a logic with couting, this is easily achieved as the interpretation
will allow for formulas defining relations of mixed element and number type.

To define the logic $\textsf{LREC}_{=}$, we considered labelled _semi-graphs_.
A semi-graph is a structure $G=(V,E,\sim)$, where $V$ is a set of nodes, and
$E$ and $\sim$ are two binary relations on $V$. Again, we consider a semi-
graph together with a labelling $C$ such that for each $v\in V$,
$C(v)\subseteq\mathcal{N}(V)$. Let $\cong$ be the symmetric reflexive
transitive closure of $\sim$ and $[v]$ denote the equivalence class of $v$
under $\cong$. Write $V/_{\cong}$ for set of such equivalence classes, i.e.
the quotient of $V$ under this equivalence relation. We write $[G]$ for the
directed graph with vertex set $V/_{\cong}$ and edge set

$[E]:=\\{([a],[b])\mid(a^{\prime},b^{\prime})\in E\text{ for some
}a^{\prime}\in[a]\text{ and }b^{\prime}\in[b]\\}.$

Write $\hat{C}$ for the labelling of $[G]$ given by
$\hat{C}([v])=\bigcup_{u\in[v]}C(u)$. We can then define the numeric query
$\hat{\chi}$ on labelled semi-graphs by the condition:

$\hat{\chi}(G,C)=\chi([G],\hat{C}).$

The logic $\textsf{LREC}_{=}$ is then defined as the closure of FOC under a
generalized operator for the numeric query $\hat{\chi}$. For simplicity, we
only allow applications of the operator to interpretations without
relativization of quotienting. We explian below why this is no loss of
generality. Indeed, it is also easily checked that this restricted definition
corresponds exactly to the original definition of the logic
$\textsf{LREC}_{=}$ given by Grohe et al.

The syntax of the logic can then be defined as follows.

######  Definition 2.1.

For a vocabulary $\tau$, the set of formulas of $\textsf{LREC}_{=}[\tau]$ is
defined by extending $\textsf{FOC}[\tau]$ formula formation rules by the
following rule. Suppose
$\varphi_{\sim}(\vec{u},\vec{v}),\varphi_{F}(\vec{u},\vec{v})$, and
$\varphi_{C}(\vec{u},\vec{p})$ are $\textsf{LREC}_{=}$ formulas where
$\vec{u}$,$\vec{v}$ and $\vec{w}$ are tuples of variables all of length $c$;
$\vec{p}$ is a tuple of _number_ variables of length $d\leq c$ and $\vec{r}$
is a tuple of number variables of length $q$, then

$\varphi:=[\textsf{lrec}_{\vec{u},\vec{v},\vec{p}}\varphi_{E},\varphi_{\sim},\varphi_{C}](\vec{w},\vec{r})$

is an $\textsf{LREC}_{=}$ formula. The free variables of the formula are those
in $\vec{w}$ and $\vec{r}$, along with the free variables in $\varphi_{E}$ and
$\varphi_{\sim}$ that are not among $\vec{u}$ and $\vec{v}$ and those of
$\varphi_{C}$ that are not among $\vec{u}$ and $\vec{p}$.

To define the semantics of the logic, consider the formula
$\textsf{lrec}_{\vec{u},\vec{v},\vec{p}}\varphi_{E},\varphi_{\sim},\varphi_{C}](\vec{w},\vec{r})$
interpreted in a $\tau$-structure $\mathfrak{A}$. Let the semigraph
$G=(A^{c},E,\sim)$ be given by the interpretation $\varphi_{E},\varphi_{\sim}$
on $\mathfrak{A}$ and $C$ be the labelling defined by $\varphi_{C}$. Then the
formula is satisfied in $\mathfrak{A}$ with $\vec{a}$ and $\vec{s}$
interpreting $\vec{w}$ and $\vec{r}$ respectively if, and only if,
$(\vec{a},\langle\vec{s}\rangle)\in\hat{\chi}(G,C)$.

Note that this amounts to extending FOC with a generalized operator for the
numeric query $\hat{\chi}$. We have not allowed for relatavization or
quotienting in the interpretations in our definition and we now explain why
this involves no loss of generality. The definition of $\hat{\chi}$ over the
semi-graph $G$ is defined by taking $\chi$ over the quotient of $G$ with
respect to the reflexive, symmetric and transitive closure of $\sim$. Thus, we
can replace a definable congruence in an interpretation by combining it with
the definition of $\sim$ without changing the semantics. By the same token, we
can replace any relativizing formula $\delta$ by incorporating it in the
definition of the binary relation $E$ and ensuring that only tuples that
satisfy $\delta$ are involved in this binary relation. It is easily seen from
the definition of $\chi$ that for any vertex $v$ that has no $E$-neighbours,
either $0$ is in $C(v)$ and thus all pairs $(v,\ell)$ are in $\chi(G,C)$ for
all $\ell\in\mathbb{N}$, or 0 is not in $C(v)$ and thus no such pairs
$(v,\ell)$ are in $\chi(G,C)$.

We define two parameters by which we measure the size of an
$\textsf{LREC}_{=}$ formula, rank and iteration-degree. As a base case, the
rank and iteration-degree of any atomic formula $\varphi$ is 0. If $\varphi$
has rank $r$ and iteration-degree $d$, then $\exists x\varphi$, $\forall
x\varphi$ and $[\\#x\varphi]=\nu$ all have rank $r+1$ and iteration degree $d$
Finally, if we have the formula

$\varphi:=[\textsf{lrec}_{\vec{u},\vec{v},\vec{p}}\varphi_{E},\varphi_{\sim},\varphi_{C}](\vec{w},\vec{r})$

where the length of $\vec{u},\vec{v}$ is $c$ and $\vec{p}$ is $d$, then the
rank of $\varphi$, denoted $\operatorname{rank}(\varphi)$, is equal to

$\max[2c+\operatorname{rank}(\varphi_{\sim}),2c+\operatorname{rank}(\varphi_{E}),c+d+\operatorname{rank}(\varphi_{C})]$

and if $\vec{r}$ has length $q$ then the iteration-degree of $\varphi$,
denoted $\operatorname{deg}(\varphi)$, is equal to

$\max[q,\operatorname{deg}(\varphi_{\sim}),\operatorname{deg}(\varphi_{E}),\operatorname{deg}(\varphi_{C})].$

Note that the rank and iteration-degree values may be distinct from each
other, and the iteration-degree need not be larger than that of sub-formulas,
regardless of the form of $\varphi$. This will be important when we introduce
the game for the logic.

###  2.3 The Path Systems Problem

In this subsection we define the path systems problem ($\mathrm{PSP}$).
Moreover we will define a specific subclass of $\mathrm{PSP}$ instances which
we will be using to prove that $\mathrm{PSP}$ is inexpressible in
$\textsf{LREC}_{=}$.

The problem is defined as a class of structures in a vocabulary with a ternary
relation $R$, unary relation $S$, and constant $\mathtt{t}$. Given a universe
$U$ and a relation $R\subseteq U^{3}$, we define the upward closure of any set
$X\subseteq U$ as the smallest superset $Y$ of $X$ such that for $a,b,c\in U$,
if $a,b$ is in $Y$ and $(a,b,c)$ is in $R$, then $c$ is in $Y$.

The decision problem $\mathrm{PSP}$ then consists of those structures
$\mathfrak{A}$ for which $\mathtt{t}^{\mathfrak{A}}$ is in the upwards closure
of $S^{\mathfrak{A}}$.

As we will be using $\mathrm{PSP}$ to prove a separation between
$\textsf{LREC}_{=}$ and LFP, we verify that $\mathrm{PSP}$ is definable in
LFP. This is well known. For completeness, we give the defining sentence.

$\varphi:=[\textsf{lfp}_{X,u}S(u)\vee(\exists v,w.X(v)\wedge X(w)\wedge
R(v,w,u))](\mathtt{t}).$

##  3 LREC= Game

In order to prove the inexpressibility result for $\textsf{LREC}_{=}$, we
introduce a Spoiler-Duplicator game. This game does not exactly characterize
the expressive power of the logic, but it provides a sufficient condition for
indistinguishability of structures.

The game we define is an extension of the classic Ehrenfeucht-Fraïssé game for
first-order logic played on a pair of structures $\mathfrak{A}$ and
$\mathfrak{B}$, where Spoiler aims to demonstrate a difference between the two
structures and Duplicator aims to demonstrate that they are not
distinguishable. Before introducing it formally, we make some observations.
Because our logic includes counting, the games are based on bijection games,
which characterise first-order logic with counting. Thus, our games have two
kinds of moves—bijection moves, which account for counting and ordinary
quantifers, and what we call _graph moves_ which account for the lrec
operator.

In a graph move, Spoiler chooses an interpretation which defines a labelled
semi-graph from each of $\mathfrak{A}$ and $\mathfrak{B}$. An auxilliary game
is then played on the pair of semi-graphs in which Spoiler aims to show that
the two semi-graphs are distinguished by the query $\hat{\chi}$ while
Duplicator attempts to hide the difference between them. At any point in this
auxilliary game, Spoiler can choose to revert to the main game, for instance
if a position is reached from where Spoiler can win the ordinary bijection
game.

It should be noted that in requiring Spoiler to provide an explicit
interpretation in the graph game, we build in definability in the logic
$\textsf{LREC}_{=}$ into the rules of the game. In that sense, it does not
provide an independent characterization of definability. Nonetheless, it does
give a sufficient criterion for proving undefinability. Similarly, Theorem 3.2
below only gives one direction of the connection between the game and the
logic. That is, it shows that if there is a formula distinguishing
$\mathfrak{A}$ and $\mathfrak{B}$, it yields a winning strategy for Spoiler.
We do not claim, and do not need, the other direction.

A final remark is that we have, for simplicity, only defined the game for the
special case where $\mathfrak{A}$ and $\mathfrak{B}$ are structures over the
same universe. Again, this is sufficient for our purpose as the structures we
construct on which we play the game satisfy this condition.

The game is parameterized by the two measures of size of formulas we
introduced in Section 2.2: the rank and iteration degree. To define the game,
we first introduce some notation for partial maps.

For any sets $A,B,C$ and $D$ with $A\subseteq B$ and $C\subseteq D$, and
function $f:A\to C$, we say $f$ is a _partial function_ between $B$ and $D$,
which we can denote by $f:B\hookrightarrow D$. We say that a function
$f^{\prime}:B\hookrightarrow D$ _extends_ $f$ if $f^{\prime}|_{A}=f$. Let
$\operatorname{dom}{f}$ denote the set $A$ where $f$ is defined. For partial
function $g:B\hookrightarrow D$ with $g(a)=f(a)$ for
$a\in\operatorname{dom}{f}\cap\operatorname{dom}{g}$, let $f\cup
g:B\hookrightarrow D$ be the partial function defined on
$\operatorname{dom}{f}\cup\operatorname{dom}{g}$ with $[f\cup g](a)=f(a)$ if
$a$ is in $\operatorname{dom}{f}$ and $[f\cup g](a)=g(a)$ otherwise.

###  3.1 Games

We now give the formal definition of the game and prove its adequacy.

######  Definition 3.1.

The _$k$ -step, $q$-degree $\textsf{LREC}_{=}$ game_ over vocabulary $\tau$ is
played by two players, _Spoiler_ and _Duplicator_ on two $\tau$-structures
$\mathfrak{A}$ and $\mathfrak{B}$ of same universe $U$ of size $n$. At any
stage of the game, the game position consists of a partial injection
$f:U\hookrightarrow U$ where $f(e^{\mathfrak{A}})=f(e^{\mathfrak{B}})$ for all
constants $e$ in $\tau$, and the domain of $f$ has at most $k$ elements.

Let $\beta=\\{b_{1},b_{2},\ldots,b_{|\beta|}\\}$ be the domain of $f$, and fix
an ordering on it so that $\vec{b}$ is the tuple
$(b_{1},b_{2},\ldots,b_{|\beta|})$. As long as $|\beta|<k$, Spoiler can play
either an extension move or a graph move. These are defined as follows.

  * •

_Extension move_ : If Spoiler selects this move then the duplicator begins by
choosing a bijection $g:U\to U$ that extends $f$. The spoiler then picks some
$a\in U$. The resulting position is $f^{\prime}=f\cup g|_{\\{a\\}}$.

  * •

_Graph move_ : In this move Spoiler begins by selecting $c\leq(k-|\beta|)/2$,
and $\textsf{LREC}_{=}$ queries $\varphi_{E}(\vec{x},\vec{y})$, and
$\varphi_{\sim}(\vec{x},\vec{y})$ where $\vec{x}$ and $\vec{y}$ are tuples of
variables of length $c$. Both queries have iteration-degree at most $q$ and
rank at most $k-|\beta|-2c$. Let $V$ be $(U\cup\mathcal{N}(U))^{c}$,
$G_{\mathfrak{A}}=(V,E_{\mathfrak{A}},\sim_{\mathfrak{A}})$ be the semi-graph
defined in $(\mathfrak{A},\vec{b})$ by the interpretation of
$(\varphi_{F},\varphi_{\sim})$, and
$G_{\mathfrak{B}}=(V,E_{\mathfrak{B}},\sim_{\mathfrak{B}})$ be the
corresponding semi-graph obtained from $(\mathfrak{B},f(\vec{b}))$. The two
players now play a game on these structures through a series of rounds. At
each round $i$, the position of this game consists of a tuple $\vec{a}_{i}\in
V$, a partial injection $h_{i}:U\hookrightarrow U$ with domain of size at most
$c$, and a value $\ell_{i}\leq n^{q}$. Initially, Spoiler chooses
$\vec{a}_{0}\in(\beta\cup\mathcal{N}(U))^{c}$ and $\ell_{0}\leq n^{q}$ and
$h_{0}$ is set to the empty map.

If $\ell_{i}=0$, then the graph move ends and the main game continues from the
new position $f^{\prime}=f\cup h_{i}$. Also, Spoiler may choose to end the
graph move and continue the main game from the position $f^{\prime}=f\cup
h_{i}$. Otherwise we continue to move $i+1$ which proceeds as follows

    1. 1.

Duplicator begins by choosing a partial bijection $g_{i}:U\to U$ with the
property that $g_{i}^{-1}(f_{i}(\vec{a}_{i}))\cong_{\mathfrak{A}}\vec{a}_{i}$
where $f_{i}=f\cup h_{i}$.

    2. 2.

For each $Y\subseteq U$ with $|Y|\leq c$, Duplicator chooses an injection
$h_{Y}:Y\to X$ satisfying the following conditions for all $\vec{u},\vec{v}\in
V$. Here, for any $\vec{v}\in V$, we write $U(\vec{v})$ to denote the set of
elements of $U$ that occur in the tuple $\vec{v}$.

      1. (a)

$(g_{i}(\vec{a}_{i}),h_{U(\vec{v})}(\vec{v}))\in[E_{\mathfrak{B}}]$ if, and
only if, $(\vec{a}_{i},\vec{v})\in[E_{\mathfrak{A}}]$;

      2. (b)

$|[E_{\mathfrak{B}}]h_{U(\vec{v})}(\vec{v})|=|[E_{\mathfrak{A}}]\vec{v}|$; and

      3. (c)

$h_{U(\vec{u})}(\vec{u})=h_{U(\vec{v})}(\vec{v})$ if, and only if,
$\vec{u}=\vec{v}$.

If Duplicator cannot choose such a set of partial bijections, then it loses
the game.

    3. 3.

Spoiler chooses some $\vec{a}_{i+1}\in\vec{a}_{i}[E_{\mathfrak{A}}]$ and we
let $\ell_{i+1}=\lfloor(\ell_{i}-1)/|[E]\vec{a_{i+1}}|\rfloor$ and
$h_{i+1}=h_{U(\vec{a}_{i+1})}$.

Spoiler wins if at any point $f$ is not a partial isomorphism between
$\mathfrak{A}$ and $\mathfrak{B}$. Duplicator wins if
$|\operatorname{dom}{f}|$ reaches $k$ and Spoiler has not won.

We can now show how establishing how Duplicator winning strategies in the game
can be used to show inexpressibility results for $\textsf{LREC}_{=}$.

######  Theorem 3.2.

Suppose $\mathfrak{A}$ and $\mathfrak{B}$ are two $\tau$-structures with the
same universe $U$, $f:U\hookrightarrow U$ is a partial injection with
$f(e^{\mathfrak{A}})=f(e^{\mathfrak{B}})$ for all constants $e$ in $\tau$ and
that $\vec{a}$ enumerates the domain of $f$. If Duplicator has a winning
strategy in the $k$-step, $q$-degree $\textsf{LREC}_{=}$ game over
$\mathfrak{A},\mathfrak{B}$ and $f$, then $(\mathfrak{A},\vec{a})$ and
$(\mathfrak{B},f(\vec{a}))$ agree on all $\textsf{LREC}[\tau]$ formulas with
rank at most $k-|\operatorname{dom}(f)|$ and iteration-degree at most $q$.

###### Proof.

We prove the contra-positive, so assume that some
$\textsf{LREC}[\tau]$-formula $\varphi$ with rank at most $k-|\beta|$ and
iteration-degree at most $q$ is true in $(\mathfrak{A},\vec{a})$ and false in
$(\mathfrak{B},f(\vec{a}))$. If $k-|\beta|=0$ then $f$ does not induce a
partial isomorphism between $\mathfrak{A}$ and $\mathfrak{B}$, since otherwise
the quantifier-free formula $\varphi$ would distinguish $\vec{a}$ from
$f(\vec{a})$. Suppose then that $k-|X|\geq 1$. If $\varphi$ is of the form
$\exists x[\psi(x)]$, $\forall x[\psi(x)]$ or $[\\#x\psi(x)]=\mu$, then
Spoiler plays the extension move. Since $\varphi$ is true in
$(\mathfrak{A},\vec{a})$ and false in $(\mathfrak{B},f(\vec{a}))$, the number
of elements satisfying $\psi$ in the two structures is different. Hence, for
any bijection $g$ extending $f$ that Duplicator might pick, there is some some
$u\in U$ such that $(\mathfrak{A},\vec{a},u)$ and
$(\mathfrak{B},f(\vec{a}),g(y))$ do not agree on $\psi(x)$. That is to say,
either $\psi$ or $\neg\psi$ is a formula true in the former but false in the
latter. Either of these is a formula of rank at most $k-|\beta|-1$ and so if
Spoiler chooses $u$ and extends $f$ to $f\cup g|_{\\{u\\}}$ it wins by the
induction hypothesis.

Assume next that $\varphi$ is of the form

$[\textsf{lrec}_{\vec{x},\vec{y},\vec{p}}\varphi_{E},\varphi_{\sim},\varphi_{C}](\vec{w},\vec{r})$

where the lengths of $\vec{x}$ and $\vec{y}$ are both $c\leq(k-|\beta|)/2$
andthe length of $\vec{r}$ is $q^{\prime}\leq q$. To simplify notation, let
$\vec{a}_{\mathfrak{A}}$ denote $\vec{a}$ and $\vec{a}_{\mathfrak{B}}$ denote
$f(\vec{a})$. Let $V$ be $(U\cup\mathcal{N}(U))^{c}$, and for
$\mathfrak{S}\in\\{\mathfrak{A},\mathfrak{B}\\}$, let
$G_{\mathfrak{S}}=(V,E_{\mathfrak{S}},\sim_{\mathfrak{S}})$ be the semi-graph
obtained by the interpretation $(\varphi_{F},\varphi_{\sim})$ in
$(\mathfrak{S},\vec{a}_{\mathfrak{S}})$ and $C_{\mathfrak{S}}$ the labelling
defined on it by $\varphi_{C}$. For any $\vec{a}\in V$, we write $\tilde{a}$
for the set of elements that occur in $\vec{a}$ and $U(\tilde{a})$ for the set
of those elements of $\tilde{u}$ that are in $U$.

Spoiler then chooses the starting node $\vec{a}_{0}$ to be the
$(\mathfrak{A},\vec{a})$ interpretation of $\vec{w}$, and $\ell_{0}$ to be the
value $\langle\vec{s}\rangle$ where $\vec{s}$ is the interpretation in
$(\mathfrak{A},\vec{a})$ of $\vec{r}$. Note that by our choice of $\varphi$,
it is true that $(\vec{a}_{0},\ell_{0})\in\chi[G_{\mathfrak{A}},\langle
C_{\mathfrak{A}}\rangle]$ and
$(f(\vec{a}_{0}),\ell_{0})\not\in\chi[G_{\mathfrak{B}},\langle
C_{\mathfrak{B}}\rangle]$. We prove by induction on $i$ that if
$(\vec{a}_{i},\ell_{i})\in\chi[G_{\mathfrak{A}},\langle
C_{\mathfrak{A}}\rangle]$ if, and only if,
$(f(\vec{a}_{i}),\ell_{i})\not\in\chi[G_{\mathfrak{B}},\langle
C_{\mathfrak{B}}\rangle]$ then Spoiler has a winning strategy in the game
move. Assume without loss of generality that $(\vec{a}_{i},\ell_{i})$ is in
$\chi[G_{\mathfrak{A}},\langle C_{\mathfrak{A}}\rangle]$. For
$\mathfrak{S}\in\\{\mathfrak{A},\mathfrak{B}\\}$, let $m_{\mathfrak{S}}$ be
the number

$|\\{v\in
u[F_{\mathfrak{S}}]\mid(v,\lfloor(\ell_{i}-1)/|[F_{\mathfrak{S}}]v|\rfloor)\in\chi(G_{\mathfrak{S}},C_{\mathfrak{S}})\\}|.$

Then,either $m_{\mathfrak{A}}\neq m_{\mathfrak{B}}$ or $m_{\mathfrak{A}}\in
C_{\mathfrak{A}}$ but $m_{\mathfrak{B}}\notin C_{\mathfrak{B}}$. So, if
$m_{\mathfrak{A}}=m_{\mathfrak{B}}$ we must have the latter case, where
Spoiler can simply reset $f$ to $f_{i}$ and proceed by playing the game on the
structures $(\mathfrak{A},\vec{a},\vec{a}_{i},\vec{s})$ and
$(\mathfrak{B},f(\vec{a}),f(\vec{a}_{i}),\vec{s})$ where
$\langle\vec{s}\rangle=m_{\mathfrak{A}}=m_{\mathfrak{B}}$. Here we also have
the base case — if $\ell_{i}=0$ then $m_{\mathfrak{A}}=m_{\mathfrak{B}}=0$.
If, instead, $m_{\mathfrak{A}}\neq m_{\mathfrak{B}}$ then Spoiler proceeds to
the next step of the iteration. If Duplicator is able to come up with a valid
set of partial bijections in step 3 of the iteration, there must be some
$\vec{b}\in\vec{a}_{i}[F]$ with
$(\vec{b},\ell^{\prime})\in\chi(G_{\mathfrak{A}},C_{\mathfrak{A}})$ if and
only if
$(h_{U(\tilde{b})}(\vec{b}),\ell^{\prime})\notin\chi(G_{\mathfrak{B}},C_{\mathfrak{B}})$,
where $\ell^{\prime}=\lfloor(\ell-1)/|[F_{\mathfrak{A}}]\vec{b}|\rfloor$
(which is also equal to
$\lfloor(\ell-1)/|[F_{\mathfrak{B}}]h_{U(\tilde{b})}(\vec{b})|\rfloor$
according to the conditions Duplicator’s choice must satisfy). Thus, by the
induction hypothesis, Spoiler has a winning strategy if it picks $\vec{a}_{i}$
to be $\vec{b}$. ∎

###  3.2 Structures

Here we describe the particular instances of the path systems problem for
which we construct Duplicator winning strategies in the game we have just
defined, and outline the strategy.

Consider a tree $T=(V,E)$ to be defined as a directed graph where edges are
oriented from a parent to its children. The structures we consider are
obtained by taking the product of a complete binary tree $T$ with a large
cyclic group of prime order $\mathbb{Z}_{p}$. The unary relation $S$ then
encodes an assignment of values in $\mathbb{Z}_{p}$ to the leaves of the tree
and the ternary relation $R$ is chosen so that determining whether the target
$\mathtt{t}$ is in the upward closure of $S$ amounts to summing these values
along the tree. We give a formal definition for future reference.

######  Definition 3.3.

For a positive integer $h$, let $T=(V,E)$ be the complete binary tree of
height $h$, $L\subseteq V$ the set of its leaves and $\textbf{root}\in V$ its
root. For any prime $p$, function $s:L\to\mathbb{Z}_{p}$ and element
$t\in\mathbb{Z}_{p}$ define the structure $\mathcal{P}(h,p,s,t)$ to be the
instance of $\mathrm{PSP}$ with

  1. 1.

universe $V\times\mathbb{Z}_{p}$

  2. 2.

$\left((u,a),(v,b),(w,c)\right)\in R\iff a+b=c\text{ AND }E(w,u)\text{ AND
}E(w,v)$

  3. 3.

$S=\\{(l,\sigma(l)\mid l\in L\\}$

  4. 4.

$\mathtt{t}=(\textbf{root},t).$

Note that for each node $v\in V$ there is a unique value of
$a\in\mathbb{Z}_{p}$ for which $(v,a)$ is in the upward closure of $S$. To be
precise, $a$ is the sum (modulo $p$) of all the values of $\sigma(l)$ for
leaves $l$ below $v$ in the tree $T$. In particular $\mathcal{P}(h,p,s,t)$ is
a positive instance of $\mathrm{PSP}$ if, and only if, $t=\sum_{l\in
L}\sigma(l)$. What we aim to show is that two structures
$\mathcal{P}(h,p,s,t)$ and $\mathcal{P}(h,p,s,t^{\prime})$ with $t\neq
t^{\prime}$ are indistinguishable by $\textsf{LREC}_{=}$ formulas of rank $k$
and degree $q$ as long as $h$ and $p$ are large enough with respect to $k$ and
$q$.

Intuitively it is clear that a fixed-point definition of the upwards closure
of $S$, such as given by the LFP formula will determine in $h$ (i.e. the
height of the tree) iterations whether $\mathtt{t}$ is in the closure of $S$.
What makes this difficult for LREC is that at each element $u\in U$ there are
$p$ distinct pairs of elements $v,w\in U$ for which $(u,v,w)\in R$. The number
of paths multiplies giving $p^{h}$ distinct ways of reaching $\mathtt{t}$, and
by an appropriate choice of $p$ and $h$, we can ensure that this is not
bounded by a polynomial in the number of elements of $U$, which is $p2^{h}$.
Moreover, we cannot eliminate the multiplicity of paths by taking a suitable
quotient. Of course, this only shows that the obvious inductive method of
computing the upward closure of $S$ cannot be implemented in
$\textsf{LREC}_{=}$. To give a full proof, we have to consider all other ways
that this might be defined, and that is the role of the game.

In the winning strategy we describe, Duplicator plays particular bijections
which we now describe. Let $\mathfrak{A}$ and $\mathfrak{B}$ be two instances
of $\mathrm{PSP}$ obtained as described above from a tree $T=(V,E)$ and prime
$p$, with the same set $S$ and different values of $\mathtt{t}$. Note, in
particular, that $\mathfrak{A}$ and $\mathfrak{B}$ have the same universe
$U=V\times\mathbb{Z}_{p}$.

For any set $X\subseteq V$. A function $\rho:X\to\mathbb{Z}_{p}$ induces a
bijection $\operatorname{bij}(\rho):X\times\mathbb{Z}_{p}\to
X\times\mathbb{Z}_{p}$ given by $\operatorname{bij}(\rho)(v,a)=(v,a+\rho(v))$.
We extend this to a bijection on the set $\mathcal{D}(X)=$ given by
$f(v,a):=(v,a+\rho(a))$ for all $v\in X$ and
$(X\times\mathbb{Z}_{p})\cup\mathcal{N}(U)$, by letting it be the identity on
all elements of $\mathcal{N}(U)$. In the Duplicator strategies we describe,
all bijections played are of this form. Thus, we usually describe them just by
specifying the function $\rho$ which we call the _offset function_. We abuse
terminology somewhat and say that $\rho$ is a partial isomorphism from
$\mathfrak{A}$ to $\mathfrak{B}$ to mean that $\operatorname{bij}(\rho)$
induces a partial isomorphism.

Roughly speaking, Duplicator’s winning strategy is to play offset functions
which are zero at the leaves of the tree $T$ and offset by the difference
between the values of $\mathtt{t}$ in $\mathfrak{A}$ and $\mathfrak{B}$ at the
root. Spoiler has to try and expose this inconsistency by building a path
between the root and the leaves. We show that Duplicator can maintain a height
(depending on the parameters $k$ and $q$) below which it plays offsets of
zero, without the inconsistency being exposed. Of course, Duplicator has to
respond to graph moves in the game, so we have to consider paths in the
interpreted semigraphs, where each node may involve elements from many
different heights in the tree. This is what makes describing the Duplicator
winning strategy challenging. In the next section we develop the tools for
describing it.

##  4 Duplicator Winning Pebblings and Extender functions

The Duplicator strategies we describe in the next section for the LREC game
rely on certain combinatorial properties of the complete binary tree $T$ and
certain offset functions $\rho:T\rightarrow\mathbb{Z}_{p}$. In this section we
develop some combinatorial properties of such trees and functions that allow
us to effectively describe the strategies.

Let $T=(V,E)$ be a complete (directed) binary tree with $N=2^{n}$ leaves. The
_height_ of a node $v\in V$, denoted $\text{height}(v)$ is the distance of $v$
to a leaf (since $T$ is complete, this is the same for all leaves reachable
from $v$). Thus, if $v$ is a leaf its height is $0$ and if $v$ is the root of
$T$, its height is $n$.

Let $R_{T}$ be the set of triples $(x,y,z)$ such that $E(x,y)$ and $E(x,z)$
and let $R=\\{\\{x,y,z\\}\mid(x,y,z)\in R_{T}\\}$. In other words $R$ is the
collection of unordered sets of three elements consisting of a node of $T$
along with its two children. We say that a three element set $\\{x,y,z\\}$ is
_related_ if $\\{x,y,z\\}\in R$. We call an element of $R$ a _related triple_.

Say a set $X\subseteq V$ is _closed_ if for every related triple
$\\{x,y,z\\}\in R$, if $x,y\in X$ then $z\in X$. For every $X\subseteq V$,
there is a unique minimal closed set $\overline{X}$ such that
$X\subseteq\overline{X}$. We call $\overline{X}$ the _closure_ of $X$.

Let $\text{min-h}(X)$ denote the minimum height of any element of $X$ and
$\text{max-h}(X)$ denote the maximum height of any element of $X$.

######  Proposition 4.1.

$\text{min-h}(\overline{X})=\text{min-h}(X)$

###### Proof.

Consider the sequence of sets given by $X_{0}=X$ and
$X_{i+1}=X_{i}\cup\\{z\mid\\{x,y,z\\}\in R\text{ for some }x,y\in X_{i}\\}$.
Then $\overline{X}=\bigcup_{i}X_{i}$. A simple induction on $i$ shows that
$\text{min-h}(X_{i+1})=\text{min-h}(X_{i})$ for all $i$, establishing the
claim. ∎

For any pair of vertices $x,y\in V$, there is a unique undirected path
$z_{1},\ldots,z_{k}\in V$ such that $x=z_{1}$, $y=z_{k}$ and for all $i$ with
$1\leq i<k$, we have $E(z_{i},z_{i+1})$ or $E(z_{i+1},z_{i})$. Say that a set
$X\subseteq V$ is _connected_ whenever $x,y\in X$ the undirected path from $x$
to $y$ is contained in $X$.

A _connected component_ of a closed set $X$ is a maximal closed connected
subset of $X$. It is clear that every closed set $X$ is a disjoint union of
closed connected components.

For $v\in V$, we say a set $X\subseteq V$ _encloses_ $v$ if every path from
$v$ to a leaf goes through an element of $X$. We say that $X$ _minimally
encloses_ $v$ if $X$ encloses $v$ and no proper subset of $X$ encloses $v$.

If $X$ is a closed connected set, there is a unique element $r\in X$ with
$\text{height}(r)=\text{max-h}(X)$. Moreover, there is a set $F\subseteq X$
which minimally encloses $r$ and such that $X$ is exactly the set of elements
$y\in V$ such that $y$ is on the path from $r$ to $f$ for some $f\in F$. We
call $F$ the _frontier_ of $X$. Note that this allows the trivial case when
$X=F=\\{r\\}$. In all cases, we have $\overline{F}=X$. We write
$\text{height}(X)$ for $\text{height}(r)=\text{min-h}(X)$.

######  Proposition 4.2.

If $X$ is a closed connected set with root $r$ and frontier $F$ then

$|F|>\text{height}(X).$

###### Proof.

Let $h=\text{height}(X)$. The proof proceeds by induction on $h$. If $h=0$,
then $F=\\{r\\}$ and the inequality is satisfied. Suppose then that $h>0$, and
so there is some element in $X$ whose height is less than that of $r$. Since
$X$ is connected this implies that some child of $r$ is in $X$ and since $X$
is closed this implies both children of $r$ are in $X$. Let the two children
of $r$ be $s_{1}$ and $s_{2}$. Then, we have $X=X_{1}\cup X_{2}\cup\\{r\\}$
where $X_{1}$ and $X_{2}$ are closed connected sets with roots $s_{1}$ and
$s_{2}$ respectively. Let $F_{1}$ and $F_{2}$ be the respective frontiers of
$X_{1}$ and $X_{2}$ and note both of these are non-empty. Since
$\text{min-h}(X_{1})\geq\text{min-h}(X)$ and
$\text{height}(s_{1})=\text{height}(r)-1$, we have $\text{height}(X_{1})<h$
and so by induction hypothesis $|F_{1}|>\text{height}(X_{1})$. Since $F_{2}$
is non-empty, we have

$|F|=|F_{1}|+|F_{2}|>\text{height}(s_{1})+1-\text{min-h}(X_{1})\geq\text{height}(r)-\text{min-h}(X)=\text{height}(X)$

as required. ∎

For a closed set $X\subseteq V$, we say a function
$\rho:X\rightarrow\mathbb{Z}/p\mathbb{Z}$ is _consistent_ if whenever
$x,y,z\in X$ are such that $E(x,y)$ and $E(x,z)$, then
$\rho(x)=\rho(y)+\rho(z)$. If $X\subseteq Y$, we say that a function
$\rho^{\prime}:Y\rightarrow\mathbb{Z}/p\mathbb{Z}$ _extends_ $\rho$ if
$\rho^{\prime}|_{X}=\rho$. The following is a useful characterization of
consistent functions on closed sets.

######  Proposition 4.3.

For a closed set $X$, $\rho:X\rightarrow\mathbb{Z}/p\mathbb{Z}$ is consistent
if, and only if, for every $F\subseteq X$ and $x\in X$ such that $F$ minimally
encloses $x$, we have $\rho(x)=\sum_{y\in F}\rho(y)$.

###### Proof.

The direction from right to left is immediate, since for any $x,y,z\in X$ with
$(x,y,z)\in R_{T}$, we have that $F=\\{y,z\\}$ minimally encloses $x$. Thus,
by assumption $\rho(x)=\sum_{w\in F}\rho(w)=\rho(y)+\rho(z),$ as required.

In the other direction, assume that $\rho$ is consistent and suppose $F$
minimally encloses $x$. Let $h=\text{height}(\overline{F})$ and we proceed by
induction on $h$. If $h=0$ then $F=\\{x\\}$ and $\rho(x)=\sum_{y\in F}\rho(y)$
is clearly true. Suppose then the claim is true for all $F^{\prime}$ with
$\text{height}(\overline{F^{\prime}})\leq h$ and let $F$ be a set minimally
enclosing $x$ with $\text{height}(F)=h+1$. Let $s_{1}$ and $s_{2}$ be the two
children of $x$ and $F_{1}$ and $F_{2}$ the subsets of $F$ that minimally
enclose $s_{1}$ and $s_{2}$ respectively. Then $\sum_{y\in
F}\rho(y)=\left(\sum_{y\in F_{1}}\rho(y)\right)+\left(\sum_{y\in
F_{2}}\rho(y)\right)=\rho(s_{1})+\rho(s_{2})=\rho(x)$. Here the first equality
holds from the fact that $F_{1}$ and $F_{2}$ form a partition of $F$, the
second by induction hypothesis and the third by the consistency of $\rho$. ∎

For any (not necessarily closed) set $X\subseteq V$, we say a function
$\rho:X\rightarrow\mathbb{Z}/p\mathbb{Z}$ is _consistent_ if there is a
consistent $\rho^{\prime}:\overline{X}\rightarrow\mathbb{Z}/p\mathbb{Z}$ which
extends $\rho$. Note that if such a $\rho^{\prime}$ exists then it is unique.
We can extend Proposition 4.3 to sets $X$ that are not closed.

######  Proposition 4.4.

For any set $X$, $\rho:X\rightarrow\mathbb{Z}/p\mathbb{Z}$ is consistent if,
and only if, for every $F\subseteq X$ and $x\in X$ such that $F$ minimally
encloses $x$, we have $\rho(x)=\sum_{y\in F}\rho(y)$.

###### Proof.

In one direction, suppose $\rho$ is consistent and there is an $F\subseteq X$
minimally enclosing $x\in X$. Then this $F$ and $x$ is present in
$\overline{X}$ and so, by the consistency of $\rho$ we have
$\rho(x)=\sum_{y\in F}\rho(y)$ by Proposition 4.3.

In the other direction, suppose $\rho(x)=\sum_{y\in F}\rho(y)$ for all $F$
minimally enclosing $x$ in $X$. If $X$ is closed, there is nothing to prove by
Proposition 4.3. If not, then we can enumerate the elements of $\overline{X}$
that are not in $X$ in an order $x_{1},\ldots,x_{c}$ so that for each
$x_{i+1}$, there are elements $y,z\in X\cup\\{x_{1},\ldots,x_{i}\\}$ such that
$\\{x_{i+1},y,z\\}\in R$. Fix such an order and write $X_{i}$ for the set
$X\cup\\{x_{1},\ldots,x_{i}\\}$. We prove by induction on $i$ that we can
extend $\rho$ to a function $\rho_{i}$ on $X_{i}$ such that
$\rho_{i}(x)=\sum_{y\in F}\rho_{i}(y)$ for all $F$ minimally enclosing $x$ in
$X_{i}$. Since $X_{n}=\overline{X}$ is closed, the result then follows by
Proposition 4.3.

We let $\rho_{0}=\rho$ and the base case follows by assumption. Suppose
$\rho_{i}$ has been defined to satisfy the inductive hypothesis. If there is
exactly one pair of elements $y,z\in X_{i}$ such that $\\{x_{i+1},y,z\\}\in R$
then we extend $\rho_{i}$ to $x_{i+1}$ in the natural way. That is if $y$ and
$z$ are the two children of $x_{i+1}$ we let
$\rho_{i+1}(x_{i+1})=\rho_{i}(y)+\rho_{i}(z)$ and if $y$ is the parent and $z$
the sibling of $x_{i+1}$ we let $\rho_{i+1}(x_{i+1})=\rho_{i}(y)-\rho_{i}(z)$.
In each case, we can verify that $\rho_{i+1}$ satisfies the condition that
$\rho_{i+1}(x)=\sum_{w\in F}\rho_{i+1}(w)$ for all $F$ minimally enclosing $x$
in $X_{i+1}$. If $F\cup\\{x\\}$ does not contain $x_{i+1}$, there is nothing
to check as the condition is satisfied by induction hypothesis. Similarly, if
$F=\\{x\\}$ the condition is trivially satisfied. Otherwise, there are a
number of cases to be considered.

  * •

If $x=x_{i+1}$ and $y$ and $z$ are the two children of $x_{i+1}$ then $F$ can
be partitioned into two sets $F_{1}$ and $F_{2}$ minimally enclosing $y$ and
$z$ respectively. By induction hypothesis we have $\rho_{i}(y)=\sum_{w\in
F_{1}}\rho_{i}(w)$ and $\rho_{i}(z)=\sum_{w\in F_{2}}\rho_{i}(w)$ and so
$\rho_{i+1}(x)=\sum_{w\in F}\rho_{i+1}(w)$ as desired.

  * •

If $x=x_{i+1}$ and $y$ is the parent and $z$ the sibling of $x_{i+1}$, then
$F\cup\\{z\\}$ minimally encloses $y$ and so by induction hypothesis
$\rho_{i}(y)=\rho_{i}(z)+\sum_{w\in F}\rho_{i}(w)$. Thus, setting
$\rho_{i+1}(x_{i+1})=\rho_{i}(y)-\rho_{i}(z)$ gives the desired result.

  * •

If $x_{i+1}\in F$ and $y$ and $z$ are the two children of $x_{i+1}$ we have
that $F\setminus\\{x_{i+1}\\}\cup\\{y,z\\}$ minimally encloses $x$ and we have
$\rho_{i+1}(x)=\rho_{i}(x)=\rho_{i}(y)+\rho_{i}(z)+\sum_{w\in
F\setminus\\{x_{i+1}\\}}\rho_{i}(w)=\rho_{i+1}(x_{i+1})+\sum_{w\in
F\setminus\\{x_{i+1}\\}}\rho_{i}(w)=\sum_{w\in F}\rho_{i+1}(w).$

  * •

If $x_{i+1}\in F$ and $y$ is the parent and $z$ the sibling of $x_{i+1}$, then
it must be that $z\in F$ and also that $F\setminus\\{z,x_{i+1}\\}\cup\\{y\\}$
minimally encloses $x$. From these two facts it is easily seen that
$\rho_{i+1}(x)=\rho_{i}(x)=\sum_{w\in
F\setminus\\{z,x_{i+1}\\}\cup\\{y\\}}\rho_{i}(w)=\rho_{i}(y)-\rho_{I}(z)+\sum_{w\in
F\setminus\\{x_{i+1}\\}}\rho_{i}(w)=\rho_{i+1}(x_{i+1})+\sum_{w\in
F\setminus\\{x_{i+1}\\}}\rho_{i}(w)=\sum_{w\in F}\rho_{i+1}(w).$

The only case remaining is if both children of $x_{i+1}$, say $y_{1}$ and
$z_{1}$ as well as its parent, say $y_{2}$ and its sibling, say $z_{2}$ are
all in $X_{i}$. Then we can consistently define $\rho_{i+1}$ as before as long
as $\rho_{i}(y_{1})+\rho_{i}(z_{1})=\rho_{i}(y_{2})-\rho_{i}(z_{2})$. But,
since $\\{y_{1},z_{1},z_{2}\\}$ minimally encloses $y_{2}$, this is guaranteed
by the induction hypothesis. ∎

The situation we are often interested in is when we have a consistent function
$\rho:X\rightarrow\mathbb{Z}/p\mathbb{Z}$ and we wish to extend it to a
consistent function $\sigma:Y\rightarrow\mathbb{Z}/p\mathbb{Z}$ for some
$Y\supseteq X$ in a _minimal_ fashion. That is to say, we want to set $\sigma$
to be $0$ wherever possible. To this end, we make the following definition.

######  Definition 4.5.

Suppose $X,Y\subseteq V$ with $X\subseteq Y$ and
$\rho:X\rightarrow\mathbb{Z}/p\mathbb{Z}$ is a consistent function. We say
that $y\in\overline{Y}$ is _free_ over $\rho$ if for every
$S\subseteq\overline{Y}$ that is closed and connected with head $x$ and
frontier $F$ and $y\in F\cup\\{x\\}$: either _(i)_ $\rho(z)=0$ for each $z\in
X\cap(F\cup\\{x\\})$ ; or _(ii)_ there is a $w\in S\cap X$ such that $w\not\in
F\cup\\{x\\}$.

We now show that a consistent $\rho$ on the set $X$ can be extended to a
consistent offset function on $Y\supseteq X$ which is zero on all elements
that are free over $\rho$.

######  Proposition 4.6.

Let $X,Y\subseteq V$ with $X\subseteq Y$ and
$\rho:X\rightarrow\mathbb{Z}/p\mathbb{Z}$ be a consistent function. Suppose
$Z\subseteq\overline{Y}$ is the set of elements in $\overline{Y}$ which are
free over $\rho$ and $\sigma:Z\rightarrow\mathbb{Z}/p\mathbb{Z}$ the function
that takes all such elements to $0$. Then $\rho\cup\sigma$ is consistent.

###### Proof.

Assume, for contradiction, that $\rho^{\prime}:=\rho\cup\sigma$ is not
consistent. Then, by Proposition 4.4, there is a closed connected set
$S\subseteq X\cup Z$ with frontier $F$ and head $x$ such that
$\rho^{\prime}(x)\neq\sum_{y\in F}\rho^{\prime}(y)$. Let $S$ be a minimal such
set. Note that $F\cup\\{x\\}$ must contain an element of $Z$, since $\rho$ is
assumed to be consistent. Then, it must be the case that $\rho(z)\neq 0$ for
some $z\in X\cap(F\cup\\{x\\})$ for otherwise by definition we would have
$\rho^{\prime}(z)=0$ for all $z\in F\cup\\{x\\}$ and so
$\rho^{\prime}(x)=\sum_{y\in F}\rho^{\prime}(y)$. Then, by Definition 4.5,
there is a $w\in S\cap X$ such that $w\not\in F\cup\\{x\\}$. Let
$F^{\prime}\subseteq F$ be the unique subset of $F$ that minimally encloses
$w$. We then have two cases: either $\rho^{\prime}(w)=\rho(w)\neq\sum_{y\in
F^{\prime}}\rho^{\prime}(y)$ or $\rho^{\prime}(w)=\rho(w)=\sum_{y\in
F^{\prime}}\rho^{\prime}(y)$. In the first case, let
$S^{\prime}=\overline{F^{\prime}\cup\\{w\\}}$ and in the second, let
$S^{\prime}=\overline{F\setminus F^{\prime}\cup\\{w,x\\}}$. In either case we
have $S^{\prime}$ is a proper closed connected subset of $S$ with the property
that $\rho^{\prime}$ at its head is not the sum of the values of
$\rho^{\prime}$ at its fronitier, contradicting the minimality of $S$. ∎

We now establish the main combinatorial property of consistent offset
functions which will enable us to construct Duplicator winning strategies for
the graph move of the game.

######  Proposition 4.7.

Say we are given a set $X\subseteq V$ along with a consistent
$\rho:X\rightarrow\mathbb{Z}/p\mathbb{Z}$, and let
$Y_{1},\ldots,Y_{r}\subseteq V$ be sets with $|Y_{i}|\leq s$ for all $i$.
Then, there is a sequence of functions
$\sigma_{i}:Y_{i}\rightarrow\mathbb{Z}/p\mathbb{Z}$ such that:

  1. 1.

for each $i$ with $1\leq i<r$, $\rho\cup\sigma_{i}\cup\sigma_{i+1}$ is
consistent; and

  2. 2.

for any $i$ and $y\in Y_{i}$, if $\sigma_{i}(y)\neq 0$ then there is some
$x\in X$ with $\rho(x)\neq 0$ and
$\text{height}(y)\geq\text{height}(x)-2(|X|+s)$.

###### Proof.

For any $v\in V$, we write $T(v)$ for the subtree of $T$ rooted at $v$. We now
define, for each $i$ a set $H_{i}\subseteq V$, which we use in defining the
function $\sigma_{i}$. The set $H_{i}$ for $1\leq i\leq r$ is the set of all
vertices $u\in V$ such that all of the following conditions hold:

  * •

$u$ has a grandparent $v$ and no element $x$ of $X$ with non-zero $\rho(x)$
appears in $T(v)$;

  * •

for some $j\geq i$, all elements of $Y_{j}\cup X$ that are in $T(v)$ are in
$T(u)$; and

  * •

for all $j^{\prime}$ with $i\leq j^{\prime}<j$, there is no grandchild $w$ of
$v$ such that all elements of $Y_{j^{\prime}}\cup X$ that are in $T(v)$ are in
$T(w)$.

Note that by construction $H_{i}$ cannot contain a pair of sibling nodes.

Let $\rho_{0}=\rho$ and for each $i\geq 1$ define $\rho_{i}:X\cup
H_{i}\rightarrow\mathbb{Z}/p\mathbb{Z}$ to be the function such that
$\rho_{i}(x)=\rho(x)$ for $x\in X$ and $\rho_{i}(h)=0$ for all $h\in H_{i}$.
It easily follows from Proposition 4.6 that $\rho_{i}$ is consistent for all
$i$.

We now define the series of functions $\sigma_{i}$ by induction on $i$ having
the following two properties

  1. 1.

$\rho_{i}\cup\sigma_{i}$ is consistent; and

  2. 2.

whenever $y\in T(h)$ for some $h\in H_{i}$ and $y\in Y_{i}$, then
$\sigma_{i}(y)=0$.

For a base case, define $Y_{0}$ to be the empty set and $\sigma_{0}$ to be the
empty function. Clearly the above two properties are trivially satisfied.
Assume, by induction that $\sigma_{i}$ has been defined with the above
properties. We first show that $\eta=\rho_{i+1}\cup\sigma_{i}$ is consistent.
Suppose, towards a contradiction that it is not. Then, by Proposition 4.3
there is an $x\in\operatorname{dom}(\eta)=X\cup Y_{i}\cup H_{i+1}$ and an
$F\subseteq X\cup Y_{i}\cup H_{i+1}$ that minimally encloses $x$ such that
$\eta(x)\neq\sum_{y\in F}\eta(y)$. If $F\cup\\{x\\}$ contains no element of
$H_{i+1}$, then $\eta(x)=\sum_{y\in F}\eta(y)$ by the consistency of
$\rho_{i}\cup\sigma_{i}$, so suppose $F\cup\\{x\\}$ contains an element $h$ of
$H_{i+1}$. We argue that then $h$ is also an element of $H_{i}$ and therefore
again $\eta(x)=\sum_{y\in F}\eta(y)$ by the consistency of
$\rho_{i}\cup\sigma_{i}$. Note that any element $h$ of $H_{i+1}$ is an element
of $H_{i}$ unless the grandparent $u$ of $h$ has another grandchild $w\neq h$
such that all elements of $(Y_{i}\cup X)\cap T(u)$ are in $T(w)$. Indeed, by
definition of $H_{i+1}$, there is a $j\geq i+1$ such that all elements of
$Y_{j}\cup X$ that are in $T(u)$ are in $T(h)$. This $j$ also witnesses that
$h$ is in $H_{i}$ unless $u$ has another grandchild $w\neq h$ such that all
elements of $(Y_{i}\cup X)\cap T(u)$ are in $T(w)$. We show by cases that this
cannot happen.

_Case 1_ $h=x$. Then, by definition of $H_{i+1}$ there are no elements of $X$
in $T(x)$ that $\rho$ takes to a non-zero element and so in particular none in
$F$. Further, since $H_{i+1}$ cannot contain a pair of sibling nodes and any
frontier minimally enclosing $x$ must contain such a pair, we conclude that
$F$ contains at least one element of $Y_{i}\cup X$. Hence, the grandparent $u$
of $h$ cannot have a grandchild $w$ distinct from $h$ such that $T(w)$
contains $T(u)\cap(Y_{i}\cup X)$.

_Case 2_ : $x\not\in H_{i+1}$ is the parent of $h$. Let $u$ be the parent of
$x$. Since $T(u)$ does not contain any element of $X$ that $\rho$ takes to a
non-zero element and $x\not\in H_{i+1}$ we conclude that $x\in Y_{i}\cup X$.
Thus, there is no grandchild $w$ of $u$ such that $T(w)$ contains
$T(u)\cap(Y_{i}\cup X)$.

_Case 3:_ $x\not\in H_{i+1}$ is not the parent, but an ancestor of $h$. Then,
consider $y$, the sibling of $h$ and $z$ the sibling of the parent of $h$. We
know $y\not\in H_{i+1}$ since two sibling nodes cannot be in $H_{i+1}$. Since
$F\cap T(y)$ must enclose $y$, we conclude that at least one element of $F\cap
T(y)$ is not in $H_{i+1}$ and so is in $Y_{i}\cup X$. By the same argument,
there is an element of $Y_{i}\cup X$ in $T(z)$. Thus, the grandparent $u$ of
$h$ does not have a unique grandchild $w$ such that $T(w)$ contains
$T(u)\cap(Y_{i}\cup X)$.

Thus, $\eta$ is consistent. Let $Z$ be the set of elements in
$C=\overline{X\cup Y_{i}\cup Y_{i+1}\cup H_{i+1}}$ that are free over $\eta$.
Then by Proposition 4.6 there is a consistent extension
$\eta^{\prime}:C\rightarrow\mathbb{Z}/p\mathbb{Z}$ of $\eta$ such that
$\eta^{\prime}(x)=0$ for all $x\in Z$. We define $\sigma_{i+1}$ to be the
restriction of $\eta^{\prime}$ to $Y_{i+1}$.

We first argue that $\sigma_{i+1}$ satisfies the two properties required
inductively. That $\rho_{i+1}\cup\sigma_{i+1}$ is consistent follows from the
consistency of $\eta^{\prime}$. For the second, it suffices to show that
whenever $y\in T(h)\cap Y_{i+1}$ for some $h\in H_{i+1}$, then $y$ is free
over $\eta$. For any element $z\in\operatorname{dom}(\eta)\cap T(h)$ we have
either $z\in Y_{i}\cup X$ or $z\in H_{i+1}$. Note that $T(h)$ contains no
element of $X$ that gets taken to a non-zero element of $\rho$ by definition
of $H_{i+1}$ and so in the latter case, $\eta^{\prime}(z)=0$ again by
definition. In the former case, we have an element of $X\cup Y_{i}$ in $T(h)$
and so $h$ must be in $H_{i}$, hence $\eta(z)=0$ by induction hypothesis. So,
suppose $y\in T(h)\cap Y_{i+1}$ and let $S$ be a closed connected subset of
$C$ with frontier $F$ and head $x$ such that $y\in F\cup\\{x\\}$. If $x$ is
not in $T(h)$, then $h\in\operatorname{dom}(\eta)\cap S$ and $h\not\in
F\cup\\{x\\}$. On the other hand, if $x\in T(h)$, then $S\subseteq T(h)$ and
we have established that $\eta(z)=0$ for all $z\in
T(h)\cap\operatorname{dom}(\eta)$. This shows that $y$ is free over $\eta$.

Having defined the sequence of functions $\sigma_{i}$, we argue that they
satisfy the two properties required in the proposition. The first is immediate
from the definition. Indeed, $\rho\cup\sigma_{i}\cup\sigma_{i+1}$ is a
restriction to $X\cup Y_{i}\cup Y_{i+1}$ of the consistent function
$\eta^{\prime}$ defined at stage $i+1$ of the construction above.

For the second property, suppose towards a contradiction that there is a $y\in
Y_{i}$ with $\sigma_{i}(y)\neq 0$ and such that the shortest path from $y$ to
an ancestor $z$ with $T(z)$ containing some $x\in X$ where $\rho(x)$ is not
zero, is of length greater than $2(s+|X|)$. Let $y=u_{0},u_{1},\ldots,u_{m}$
be this path. Since, $|Y_{i}|\leq s$, there must be a $j<m-2$ such that
$T(u_{j})$, $T(u_{j+1})$ and $T(u_{j+2})$ all contain the same elements of
$Y_{i}\cup X$. Since $T(u_{j+2})$ contains no element $w$ of $X$ where
$\rho(w)$ is not zero, we conclude that $u_{j}$ is in $H_{i}$. This implies
that $\sigma_{i}(u)=0$ for all $u\in T(u_{j})$ and so in particular for $y$,
giving us the contradiction.

∎

##  5 Inexpressibility of PSP in LREC=

In this section we prove the main result of the paper. We make use of the tree
properties established in Section 4 to show further combinatorial results
about the specific subclass of semi-graphs that arise as interpretations from
the structures defined in Definition 3.3. From this we are able to arrive at a
winning strategy for Duplicator.

Let $T=(V,E)$ be a complete binary tree with $N=2^{n}$ leaves, $p$ be a prime
number, and fix a subset $\beta\subseteq V$. Intuitively, these correspond to
the parameters of the interpretation and remain fixed in our game argument.
For $m>0$ and any set $X$ of size $m$ let $\mathcal{N}(X)$ be the set $[m]$.
For $X\subseteq V$, let $\mathcal{D}(X)$ denote the set
$(X\times\mathbb{Z}_{p})\cup\mathcal{N}(V\times\mathbb{Z}_{p})$. Fix a semi-
graph $G=(W,F,\sim)$ with $W\subseteq\mathcal{D}(V)^{c}$ for some constant $c$
and $F$ the edge relation of $G$. Recall that $\cong$ denotes the symmetric
reflexive transitive closure of $\sim$, and $[G]$ denotes the graph obtained
from $G$ by taking the quotient with respect to this relation. For any
$\vec{a}\in W$, we write $\tilde{a}$ for the set of elements that occur in
$\vec{a}$ and $V(\tilde{a})$ for its projection on $V$, i.e. the set $\\{v\in
V\mid(v,d)\in\tilde{a}\text{ for some }d\\}$. For any set closed set
$X\subseteq V$, we use the term _frontier_ of $X$ to mean the union of the
frontiers of all the connected components of $X$.

For $X\subseteq V$, and consistent $\rho:X\to\mathbb{Z}_{p}$, let
$\mathcal{Z}(\rho)$ be the zero-locus of $\rho$, and $\text{null-h}(\rho)$ be
equal to $\text{min-h}(X\setminus\mathcal{Z}(\rho))-1$. For a sequence of sets
$Y_{1},Y_{2},\ldots,Y_{t}\subseteq V$, let
$\operatorname{lift}_{\rho}(Y_{1},Y_{2},\ldots,Y_{t})$ be the set of all
sequences of functions $\sigma_{i}:Y_{i}\to\mathbb{Z}_{p}$ which extend $\rho$
and satisfy the conditions of Proposition 4.7. Recall that $\rho$ induces a
bijection $\operatorname{bij}(\rho)=f:\mathcal{D}(X)\to\mathcal{D}(X)$ which
is the function where $f(v,a):=(v,a+\rho(v))$, when $(v,a)\in
X\times\mathbb{Z}_{p}$, and $f$ is the identity otherwise. For either
structure $\mathfrak{A}\in\\{G,[G]\\}$, we say $\rho$ _induces a partial
isomorphism_ over $\mathfrak{A}$ if $f$ is a partial isomorphism from
$\mathfrak{A}$ to itself. Moreover, we say $\rho$ _induces a liftable
isomorphism_ over $\mathfrak{A}$ if for all sequences $Y_{1},Y_{2},\ldots
Y_{t}$ with $|Y_{i}|\leq c$, there is some
$(\sigma_{1},\sigma_{2},\ldots,\sigma_{t})\in\operatorname{lift}_{\rho}(Y_{1},Y_{2},\ldots,Y_{t})$
such that $\sigma_{i}\cup\sigma_{i+1}$ induces a partial isomorphism over
$\mathfrak{A}$ for $i<t$. For all $d$ let $f^{d}$ denote $f$ composed with
itself $d$ times.

######  Proposition 5.1.

For $X\subseteq V$, function $\rho:X\to\mathbb{Z}_{p}$ inducing a partial
isomorphism $f=\operatorname{bij}(\rho)$ over $[G]$ and tuple
$\vec{a}\in\mathcal{D}(X)^{c}\subseteq W$, if there are
$d_{1},d_{2}\in\mathbb{Z}_{p}$ with $f^{d_{1}}(\vec{a})\cong
f^{d_{2}}(\vec{a})$ then $f(\vec{a})\cong\vec{a}$.

###### Proof.

Let $C=\\{[f^{d}(\vec{a})]\mid d\in\mathbb{Z}_{p}\\}$ denote the set of
$\cong$-equivalence classes of $f^{d}(\vec{a})$. By the fact that $f$ is a
partial isomorphism over $[G]$, we have an action of the group
$\mathbb{Z}_{p}$ on $C$ given by $[f^{d}(\vec{a})]^{i}=[f^{d+1}(\vec{a})]$ for
$i\in\mathbb{Z}_{p}$. Since $p$ is prime, $\mathbb{Z}_{p}$ has no non-trivial
subgroups and so the kernel of this action is either trivial, in which case
$f^{d_{1}}(\vec{a})\not\cong f^{d_{2}}(\vec{a})$ for all distinct $d_{1}$ and
$d_{2}$ or the kernel of the action is all of $\mathbb{Z}_{p}$, in which case
$f^{d}(\vec{a})\cong\vec{a}$ for all $d$. ∎

######  Lemma 5.2.

For $X\subseteq V$ and $\rho:X\to\mathbb{Z}_{p}$, if $\rho$ induces a liftable
isomorphism over $G$, then $\rho$ induces a partial isomorphism over $[G]$.

###### Proof.

Let $f:=\operatorname{bij}(\rho)$, and let $S=\mathcal{D}(X)^{c}\cap W$. We
show that $f$ preserves the relations $[R]\cap S^{2}$ where $R$ is either one
of $F$ or $\sim$. To this end, let $(\vec{a}_{1},\vec{a}_{2})\in[R]\cap S^{2}$
and we show $(f(\vec{a}_{1}),f(\vec{a}_{2}))$ is in $[R]\cap S^{2}$ as well.
First we fix $(\vec{b}_{1},\vec{b}_{2})\in R$ such that
$\vec{b_{i}}\cong\vec{a}_{i}$ for $i\in\\{1,2\\}$, which must exist by our
choice of $\vec{a}_{1},\vec{a}_{2}$. For each $i$ there is then a sequence
$\vec{d}_{i,1}(=\vec{a}_{i}),\vec{d}_{i,2},\ldots,\vec{d}_{i,s_{i}}(=\vec{b}_{i})$
such that $\vec{d}_{i,j}\sim\vec{d}_{i,j+1}$ or
$\vec{d}_{i,j+1}\sim\vec{d}_{i,j}$. Let $Y_{j}$ be the set
$V(\tilde{d}_{1,j})$ if $1\leq j\leq s_{1}$ or
$V(\tilde{d}_{2,s_{1}+s_{2}-j})$ if $s_{1}<j\leq s_{1}+s_{2}$. In other words,
the sequence of $Y_{j}$ forms the vertex sets of the symmetric $\sim$-path
from $\vec{a}_{1}$ to $\vec{b}_{1}$, followed by the symmetric $\sim$-path
from $\vec{b}_{2}$ to $\vec{a}_{2}$. Note that $|Y_{j}|\leq c$ for all $j$. By
the assumption that $\rho$ is a liftable isomorphism, there is a sequence
$\sigma_{j}:Y_{j}\to\mathbb{Z}_{n}$ in
$\operatorname{lift}_{\rho}(Y_{1},Y_{2},\ldots,Y_{s})$ and
$f_{j}:=\operatorname{bij}(\rho\cup\sigma_{j}\cup\sigma_{j+1})$ defines a
partial isomorphism over $G$ for all $j<s_{1}+s_{2}$. This means that for
$i\leq k$ and $j<s_{1}+s_{2}$ with $j\neq s_{1}$, $f_{j}(\vec{c}_{i,j})\sim
f_{j}(\vec{c}_{i,j+1})$ or $f_{j}(\vec{c}_{i,j+1})\sim f_{j}(\vec{c}_{i,j})$,
and $(f_{s_{1}}(\vec{b}_{1}),f_{s_{1}+1}(\vec{b}_{2}))\in R$. Thus, we
conclude that $(f(\vec{a}_{1}),f(\vec{a}_{2}))\in[R]$, as required. Since all
of the above holds for $f^{-1}$ as well, it follows immediately that $f$ is a
well defined partial isomorphism over $[G]$. ∎

For set $X\subseteq V$, function $\rho:X\to\mathbb{Z}_{p}$, and node $u\in X$,
we say $\rho$ is _zero bar $u$_ if
$X\setminus\\{u\\}\subseteq\mathcal{Z}(\rho)$. We further say $\rho$ is _a
spike at $u$_, if $\rho$ is zero bar $u$ and $\rho(u)\neq 0$.

For $\vec{a}\in W$, $M$ the frontier of $\overline{V(\tilde{a})}$, and $u\in
M\setminus\beta$, we say $u$ is _free_ in $[\vec{a}]$ if for all functions
$\rho:\beta\cup M\to\mathbb{Z}_{p}$ that are zero bar $u$, we have that $\rho$
is consistent and
$[\operatorname{bij}(\overline{\rho}|_{V(\tilde{a})})](\vec{a})\cong\vec{a}$.
We say $u$ is _bounded_ in $[\vec{a}]$ otherwise. Note that any two functions
$\rho,\sigma:\beta\cup M\to\mathbb{Z}_{p}$ that are spikes at $u$, defining
$f:=\operatorname{bij}(\overline{\rho})$ and
$g:=\operatorname{bij}(\overline{\sigma})$, we have that $g=f^{d}$ for some
$d$. Thus, by Proposition 5.1, if $\rho$ is consistent and induces a partial
isomorphism over $[G]$, then $u$ is free in $[\vec{a}]$ if and only if
$f(\vec{a})\cong\vec{a}$.

Say we have a sequence $\alpha$ of nodes
$\vec{a}_{1},\vec{a}_{2},\ldots,\vec{a}_{t}$ in $W$, some $i\leq t$, node $u$
bounded in $[\vec{a}_{i}]$, and $M$ the frontier of
$\overline{V(\tilde{a}_{i})}$. We say $\alpha$ _strongly bounds_ $u$ at $i$ if
for consistent $\rho:\beta\cup M\to\mathbb{Z}_{p}$ that are zero bar $u$, all
$j\in(i,t]$, and $\sigma:V(\tilde{a}_{j})\to\mathbb{Z}_{p}$ the function which
takes all elements to zero, we have that either $\rho\cup\sigma$ is
inconsistent or $\overline{\rho\cup\sigma}$ induces a liftable isomorphism
over $[G]$. Finally, we say $\alpha$ is a _strongly-bounding path_ if both of
the following are satisfied

  1. 1.

$(\vec{a}_{i},\vec{a}_{i+1})\in[F]$ for $i<t$ (i.e. the sequence is a directed
path); and

  2. 2.

for all $i\leq t$, and node $u$ bounded in $[\vec{a}_{i}]$, $\alpha$ strongly
bounds $u$ at $i$

The following is a key combinatorial property of strongly-bounding paths.

######  Proposition 5.3.

For a strongly-bounding path $\vec{a}_{1},\vec{a}_{2},\ldots,\vec{a}_{s}$ in
$W$, $M$ the frontier of $\overline{V(\tilde{a}_{1})}$, and node $u$ bounded
in $[\vec{a}_{1}]$, if $u$ is not contained in
$\overline{(M\setminus\\{u\\})\cup\beta\cup V(\tilde{a}_{s})}$ then there is
some $i>1$ such that $|[F]\vec{a}_{i}|\geq p$.

###### Proof.

Take $\rho:M\cup\beta\cup V(\tilde{a}_{s})\to\mathbb{Z}_{p}$ that is a spike
at $u$. By our assumption that $u$ is not contained in
$\overline{M\setminus\\{u\\}\cup\beta\cup V(\tilde{a}_{s})}$, it follows that
$\rho$ is consistent. Thus $\overline{\rho}$ induces a liftable isomorphism
over $[G]$, by the definition of a strongly-bounding path. Next take the
sequence $Y_{i}=V(\tilde{a}_{i})$ for $i\leq s$ (note that $|Y_{i}|\leq c$).
Since $\rho$ induces a liftable isomorphism over $[G]$, we know there exists a
sequence $\sigma_{i}:Y_{i}\to\mathbb{Z}_{p}$ in
$\operatorname{lift}_{\rho}(Y_{1},Y_{2},\ldots,Y_{s})$ such that each
$f_{i}:=\operatorname{bij}(\sigma_{i})$ is a partial isomorphism over $[G]$.
Let $j\leq s$ be the least such that $f_{j}(\vec{a}_{j})\cong\vec{a}_{j}$. We
know that such a $j$ exists because $\sigma_{s}$ is simply
$\rho|_{V(\tilde{a}_{s})}$, which is the constant zero function, and thus
$f_{s}(\vec{a}_{s})=\vec{a}\cong\vec{a}$. It must also be the case that $j>1$
because $\sigma_{1}$ is $\rho|_{V(\tilde{a}_{1})}$, which induces a partial
isomorphism over $[G]$ by assumption, and thus since $u$ is bounded in
$[\vec{a}_{1}]$ we have $f_{1}(\vec{a}_{1})\not\cong\vec{a}_{1}$. So, since
$j-1\geq 1$, we note by Proposition 5.1 that for all
$d_{1},d_{2}\in\mathbb{Z}_{p}$ with $d_{1}\neq d_{2}$,
$f^{d_{1}}_{j-1}(\vec{a}_{j-1})\not\cong f^{d_{2}}_{j-1}(\vec{a}_{j-1})$. By a
similar argument, one also sees that for all $d_{1},d_{2}\in\mathbb{Z}_{p}$,
$f^{d_{1}}_{j}(\vec{a}_{j})\cong f^{d_{2}}_{j}(\vec{a}_{j})$. Moreover, since
$(\vec{a}_{j-1},\vec{a}_{j})\in[F]$ and $\rho\cup\sigma_{j-1}\cup\sigma_{j}$
is consistent by Proposition 4.7, we can further conclude that for
$d\in\mathbb{Z}_{p}$, $(f^{d}(\vec{a}_{j-1}),f^{d}(\vec{a}_{j}))$ is also in
$[F]$. Together these gives us that $|[F]\vec{a}_{j}|\geq p$. ∎

The following technical lemma provides a useful bridge between the
combinatorial properties established so far and the the graph move in the
$\textsf{LREC}_{=}$ game.

######  Lemma 5.4.

Say we have $k\geq 2(c+|\beta|)$, a strongly-bounding path
$\vec{a}_{1},\vec{a}_{2},\ldots,\vec{a}_{t}\in W$, consistent
$\rho_{i},\sigma_{i}:Y_{i}\to\mathbb{Z}_{p}$ where $\sigma_{i}(u)=0$ if $u$ is
free in $[\vec{a}_{i}]$ and $\sigma_{i}(u)=\rho_{i}(u)$ otherwise, and set
$A:=\\{\vec{a}_{i}\mid|[F]\vec{a}_{i}|\geq p\\}$. Suppose for $i<t$ there is
some $\eta\in\operatorname{lift}_{\sigma_{i}}(Y_{i+1})$ with
$\rho_{i+1}=\eta|_{Y_{i+1}}$, then for all $r\geq 0$, if
$\text{null-h}(\rho_{1})-\text{null-h}(\rho_{t})\geq k^{3}r$ then $|A|\geq r$.

###### Proof.

For $i\leq t$, let $A_{i}$ denote the set $\\{\vec{a}_{j}\in A\mid j\leq i\\}$
and fix $h\geq k^{3}$. We prove the following stronger claim by induction on
$\ell$, which immediately implies the lemma.

######  Claim 1.

For $\ell\leq t$ and node $u$ in $Y_{\ell}\setminus\mathcal{Z}(\rho_{\ell})$
the following holds

  1. 1.

There exists a sequence $\mathcal{K}:=(v_{i})_{0\leq i\leq s}$ of nodes, and
sequence of natural numbers $\ell<m_{1}<\cdots<m_{s}=1$ such that the
following is true:

     * •

$v_{0}=u$ and $v_{s}\in Y_{1}$ is an ancestor of $u$.

     * •

For every $j>0$, $v_{j}$ is in the path from $v_{0}$ to $v_{s}$ and is bounded
in $[\vec{a}_{m_{j}}]$

     * •

For every $0\leq j<s$, $3k+1\leq$ height$(v_{j+1})-$height$(v_{j})\leq 4k$.

  2. 2.

For $r\geq 0$, if $\text{null-h}(\rho_{1})-\text{height}(u)\geq hr$ then
$|A_{\ell}|\geq r$

Part 1 of the claim is intended only to aid us in our proof of part 2, which
gives the lemma. We proceed by induction, so consider the case where $\ell=1$.
Then trivially we can take $\mathcal{K}$ to be $\\{u\\}$. For the second part
of the claim, we note that $\text{null-h}(\rho_{1})-\text{null-h}(\rho_{1})=0$
and thus the only interesting case is when $r$ is equal to $0$ by our choice
of $h$. Trivially, $|A_{1}|\geq 0$, so the base case holds.

For the induction step let $\ell>1$. Then we can see by our choice of the
sequence $\rho_{i},\sigma_{i}$ and Proposition 4.7 that there must be some
some ancestor $y$ of $u$ with $3k+1\leq$ height$(y)-$height$(u)\leq 4k$ and
$\sigma_{i}(y)\neq 0$ for some $i<\ell$. In particular this means $y$ is
bounded in $[\vec{a}_{i}]$ by our choice of $\sigma_{i}$. Moreover, there must
be sequences $\mathcal{K}^{\prime}$ and $m_{j}^{\prime}$ that satisfy the
induction hypothesis on $i$ and $y$. We then let $\mathcal{K}$ be the sequence
given by prepending $u$ to $\mathcal{K}^{\prime}$, $m_{1}$ be $i$, and $m_{j}$
be $m_{j-1}^{\prime}$ for $j>1$. It is easy to verify this choice of
$\mathcal{K}$ and $m_{i}$ satisfy the required conditions, so we have shown
part 1 of the claim.

For the second part take arbitrary $r\geq 0$ and assume
$\text{null-h}(\rho_{1})-\text{height}(u)\geq hr$. If $r=0$ then we are
trivially done, so assume $r>1$. Let $j\leq s$ be the largest index for which
$\text{null-h}(\rho_{1})-\text{height}(v_{j})>h(r-1)$ where
$v_{j}\in\mathcal{K}$. We begin by showing that
$\text{null-h}(\rho_{1})-\text{height}(v_{j})\leq h(r-1)+4k$. Indeed, if
$m_{j}$ is equal to $1$ this is trivial. Otherwise, it must be true that $j$
is less than $s$, since $m_{s}$ is equal to $1$ by construction. Thus
$\text{height}(v_{j+1})-\text{height}(v_{j})\leq 4k$, which implies that
$\text{null-h}(\rho_{1})-\text{height}(v_{j})\leq h(r-1)+4k$ as required,
since our choice of $j$ implies that
$\text{null-h}(\rho_{1})-\text{height}(v_{j+1})\leq h(r-1)$. From this we
further note that

$j\geq(\text{height}(v_{j})-\text{height}(u))/4k\geq(h-4k)/4k$

by our choice of $\mathcal{K}$. Hence $j\geq k$ by our choice of $h$.

We now put this together to prove that $|A_{\ell}|>|A_{m_{j}}|$from which the
claim follows using the inductive hypothesis stating $|A_{m_{j}}|\geq r-1$. To
derive a contradiction we assume that $|A_{\ell}|=|A_{m_{j}}|$. For $i\leq j$,
let $M_{i}$ be the frontier of $\overline{V(\tilde{a}_{m_{i}})}$ and let
$X_{i}$ be $M_{i}\setminus\\{v_{i}\\}\cup\beta\cup V(\tilde{a}_{\ell})$. By
our assumption that $|A_{\ell}|=|A_{m_{j}}|$ and proposition 5.3, we know that
$v_{i}$ must be contained in $\overline{X_{i}}$ for all $i\leq j$, as
otherwise there would be some $\ell^{\prime}\in(m_{j},m_{i}]$ with
$|[F]\vec{a}_{\ell^{\prime}}|\geq p$, contradicting the assumption. We show by
induction on $i$ that this implies that

$|T(c_{i})\cap(\beta\cup V(\tilde{a}_{\ell}))|\geq i$

where $c_{i}$ is the ancestor of $v_{i}$ with
$\text{height}(c_{i})-\text{height}(v_{i})=2k$. From here we can conclude that
$|T(c_{j})\cap(\beta\cup V(\tilde{a}_{\ell}))|\geq k$, which is a
contradiction, since $|\beta\cup V(\tilde{a}_{\ell})|<k$.

The base case where $i=0$ is trivial. For the induction step the goal is to
show that $(T(c_{i})\setminus T(c_{i-1}))\cap(\beta\cup V(\tilde{a}_{\ell}))$
is non empty, as that implies:

$|T(c_{i})\cap(\beta\cup V(\tilde{a}_{\ell}))|\geq 1+|T(c_{i-1})\cap(\beta\cup
V(\tilde{a}_{\ell}))|\geq 1+(i-1)=i.$

Let $Y\subseteq X_{i}\cup\\{v_{i}\\}$ be a minimal dependent set containing
$v_{i}$. We know such a $Y$ exists because $v_{i}$ is in $\overline{X_{i}}$.
Note then that $\text{height}(Y)$ can be no greater than $|X_{i}|+1\leq k$ by
Proposition 4.7 and thus, $\text{max-h}(Y)\leq\text{height}(v_{i})+k$ and
$\text{min-h}(Y)\geq\text{height}(v_{i})-k$. In particular this means that
$Y\subseteq T(c_{i})\setminus T(c_{i-1})$. Moreover, $Y$ cannot be a subset of
$M_{i}$ since $M_{i}$ is independent, so it must be the case that
$Y\cap(\beta\cup V(\tilde{a}_{\ell}))$ is non empty. We conclude that
$(T(c_{i})\setminus T(c_{i-1}))\cap(\beta\cup V(\tilde{a}_{\ell}))$ is non
empty and we are done.

∎

######  Lemma 5.5.

Let $n$ be an integer and $p$ a prime such that $p\geq n\geq
k^{3}(3q+1)(k+1)$. For $T$ a complete binary tree of height $n$ and $L$ the
set of its leaves, let $\sigma:L\to\mathbb{Z}_{p}$ be any function. Then, for
any $t,t^{\prime}\in\mathbb{Z}_{p}$, Duplicator has a winning strategy in the
$k$-step $q$-degree $\textsf{LREC}_{=}$ game played on
$\mathcal{P}(n,p,\sigma,t)$ and $\mathcal{P}(n,p,\sigma,t^{\prime})$.

###### Proof.

We prove by induction on $m$ that for $X\subseteq V$ with $|X|\leq k-m$, and
$\rho:X\to\mathbb{Z}_{p}$ with $\text{null-h}(\rho)\geq k^{3}(3q+1)m$, the
duplicator has a winning strategy on the $k$-pebble, $q$-degree game over
structures $\mathfrak{A},\mathfrak{B}$ and function $\rho$. We notice that
trivially, our starting pebble configuration $\rho_{init}$ is a special case
of the above, so the induction gives us the result.

For $m=0$ this is trivial, so assume $m>0$. Let $\beta$ be
$\operatorname{dom}(\rho)$ and $f$ be $\operatorname{bij}(\rho)$. If the
spoiler plays an extension move then Duplicator picks the function
$\sigma:V\to\mathbb{Z}_{p}$ which extends $\overline{\rho}$ by taking all
elements in $V\setminus\overline{\beta}$ to 0. By Proposition 4.7, for any
$a\in V$, $\sigma|_{X\cup\\{a\\}}$ is consistent and has null-height at least
$k^{3}(3q+1)m-k>k^{3}(3q+1)(m-1)$. Thus, by the inductive hypothesis,
Duplicator has a winning strategy when Spoiler plays the extension move.

Suppose that Spoiler plays a graph move instead. Then it chooses some
$c\leq(k-|\beta|)/2$, $d\leq q$, vectors of literals $\vec{x},\vec{y}$ of
length $c$, and $\textsf{LREC}_{=}$ queries $\varphi_{F}(\vec{x},\vec{y})$,
and $\varphi_{\sim}(\vec{x},\vec{y})$ with iteration-degree at most $q$, and
rank at most $k-|\beta|-2c$. Le the tuple
$\vec{b}=(b_{1},b_{2},\ldots,b_{|\beta|})$ enumerate $\beta$. Then, let $W$ be
$\mathcal{D}(V)$, $G_{\mathfrak{A}}=(W,F_{\mathfrak{A}},\sim_{\mathfrak{A}})$
be the semi-graph defined in $(\mathfrak{A},\vec{b})$ by the interpretation of
$(\varphi_{F},\varphi_{\sim})$, and
$G_{\mathfrak{B}}=(W,F_{\mathfrak{B}},\sim_{\mathfrak{B}})$ be the
corresponding semi-graph obtained from $(\mathfrak{B},f(\vec{b}))$. Spoiler
chooses some starting node $\vec{a}_{0}\in W\cap\mathcal{D}(\beta)^{c}$, and
starting counter $\ell_{0}\leq|\mathcal{D}(V)|^{d}$. At each step,
Duplicator’s strategy is the following. Given $\rho_{i}$, it fixes
$\sigma_{i}:V(\tilde{a}_{i})\to\mathbb{Z}_{p}$ with $\sigma_{i}(u)=0$ if $u$
is free in $[\vec{a}_{i}]$ and $\sigma_{i}(u)=\rho_{i}(u)$ otherwise. For all
$Y\subseteq V$ with $|Y|\leq c$, it then picks $\eta_{Y}$ to be in
$\operatorname{lift}_{\sigma_{i}}(Y)|_{Y}$.

For any $G_{1},G_{2}\in\\{G_{\mathfrak{A}},G_{\mathfrak{B}}\\}$, $X\subseteq
V$ with $\beta\subseteq X$ and consistent $\mu:X\to\mathbb{Z}_{p}$, we note
that by the induction hypothesis on $m-1$, if $\text{null-h}(\mu)$ is at least
$k^{3}(3q+1)(m-1)$ then $\mu$ induces a partial isomorphism between $G_{1}$
and $G_{2}$. Thus, we have that if $\text{null-h}(\mu)$ is at least
$k^{3}(3q+1)(m-1)+2k$ then by Proposition 4.7, $\mu$ induces a liftable
isomorphism between $G_{1}$ and $G_{2}$ and consequently by Lemma 5.2, $\mu$
induces a partial isomorphism between $[G_{1}]$ and $[G_{2}]$. Thus, if
$\text{null-h}(\mu)$ is at least $k^{3}(3q+1)(m-1)+4k$ then again by
Proposition 4.7, $\mu$ induces a liftable isomorphism between $[G_{1}]$ and
$[G_{2}]$.

We show that when Duplicator plays following the above strategy,
$\text{null-h}(\rho_{i})$ is greater than $k^{3}(3q+1)(m-1)+4k$ for all $i$.
This has a series of consequences that ultimately imply that Duplicator has a
winning strategy, and we spell these out first. Let $M_{i}$ be the frontier of
$\overline{V(\tilde{a}_{i})}$ for any $i$. For any $u\in M_{i}\setminus\beta$
which is free in $[\vec{a}_{i}]$, let $\mu:\beta\cup M_{i}\to\mathbb{Z}_{p}$
be the function that is zero bar $u$ and takes $u$ to
$\sigma_{i}(u)-\rho_{i}(u)$, and $g_{u}$ be the partial isomorphism induced by
$\overline{\mu}|_{\beta\cup V(\tilde{a}_{i})}$. Note that
$\text{null-h}(\overline{\mu})$ is no smaller than $\text{null-h}(\rho_{i})$,
and thus $g_{u}$ defines a partial isomorphism over $[G_{\mathfrak{A}}]$.
Then, let $g$ be the unique composition of all the $g_{u}$, where $u$ is free
in $[\vec{a}_{i}]$. It is easy to see that $g$ is equal to
$\operatorname{bij}(\sigma_{i}-\rho_{i})$, and since each $g_{u}$ defines a
partial isomorphism over $[G_{\mathfrak{A}}]$, by repeated application of
Proposition 5.1 we can show that $g(\vec{a}_{i})\cong\vec{a}_{i}$, and thus
$\sigma_{i}$ is a valid choice by Duplicator.

Moreover, fix some $Y\subseteq V$ and let $g$ now be the function induced by
$\sigma_{i}\cup\eta_{Y}$. Note again that $\text{null-h}(\sigma_{i})$ is no
smaller than $\text{null-h}(\rho_{i})$, and thus
$\text{null-h}(\sigma_{i}\cup\eta_{Y})$ is no smaller than
$k^{3}(3q+1)(m-1)+2k$ when $|Y|$ is at most $c$ by Proposition 4.7, which
implies $g$ defines a partial isomorphism between $[G_{\mathfrak{A}}]$ and
$[G_{\mathfrak{B}}]$. Therefore, Duplicator’s choices for $\eta_{Y}$ are
valid. Finally, we can see by a similar argument that the in-degree of
$[\vec{a}_{i}]$ in $[G_{\mathfrak{A}}]$ is the same as the in-degree of
$[f_{i}(\vec{a}_{i})]$ in $[G_{\mathfrak{B}}]$. Thus we have verified that as
long as $\text{null-h}(\rho_{i})$ is greater than $k^{3}(3q+1)(m-1)+4k$ for
all $i$, the graph move only ends when the spoiler decides to reset $\rho$ to
$\rho_{s}$ for some $s$. By our assumption on $\text{null-h}(\rho_{s})$, and
the inductive hypothesis on $m-1$, Duplicator has a winning strategy when such
a decision is made by Spoiler.

Therefore, if we can prove that $\text{null-h}(\rho_{i})$ is greater than
$h(3q+1)(m-1)+4k$ for all $i$ then we are done. To derive a contradiction,
assume there is some $s$ such that $\text{null-h}(\rho_{s})\leq
k^{3}(3q+1)(m-1)+4k$. Then, let $t\leq s$ be the smallest such that
$\text{null-h}(\rho_{t})\leq k^{3}(3q+1)(m-1)+k^{3}$ and take
$A:=\\{\vec{a}_{i}\mid|[F]\vec{a}_{i}|\geq p\text{ AND }0<i\leq t\\}$. By our
choice of $t$, we know that
$\text{null-h}(\sigma_{t-1})\geq\text{null-h}(\rho_{t-1})\geq
k^{3}(3q+1)(m-1)+k^{3}$ and thus for $k$ large enough we have
$\text{null-h}(\rho_{t})>k^{3}(3q+1)(m-1)+4k$ by Proposition 4.7. It is easy
to verify that $\vec{a}_{0},\vec{a}_{1},\ldots,\vec{a}_{t}$ is a strongly-
bounding path, so we invoke Lemma 5.4 to get that $|A|\geq 3q$ (since
$\text{null-h}(\rho_{1})-\text{null-h}(\rho_{t})\geq 3qk^{3}$ by choice of
$t$). Note that $|V\times\mathbb{Z}_{p}|$ is no greater than $p^{2}$, and thus
$\ell_{0}$ can be at most $p^{2q}$. However, this implies that $\ell_{t-1}$
can be at most $\ell_{0}/p^{|A|-1}<1$. Hence, we have a contradiction: as
$\ell_{t-1}$ must be 0, the graph move must terminate prior to reaching step
$t$. This completes the proof. ∎

From this our main theorem follows immediately.

######  Theorem 5.6.

$\mathrm{PSP}$ is not expressible in $\textsf{LREC}_{=}$

###### Proof.

Let $\tau$ be the vocabulary of $\mathrm{PSP}$ instances and suppose for
contradiction that there is a sentence $\varphi$ of $\textsf{LREC}_{=}[\tau]$
that defines the positive instances. Fix $k$ to be greater than the rank of
$\varphi$ and $q$ to be grater than $\operatorname{deg}(\varphi)$. Take $T$ to
be a complete binary tree of height $n\geq k^{3}(3q+1)(k+1)$ and $p$ to be a
prime with $p\geq n$. Fix a function $\sigma$ from the leaves $L$ of $T$ to
$\mathbb{Z}_{p}$ and let $\mathfrak{A}$ be the structure
$\mathcal{P}(n,p,\sigma,t)$ where $t=\sum_{l\in L}\sigma(l)$ and
$\mathfrak{B}$ to be the structure $\mathcal{P}(n,p,\sigma,t^{\prime})$ where
$t^{\prime}=t+1$. Then, by construction $\mathfrak{A}$ is a positive instance
of $\mathrm{PSP}$ so $\mathfrak{A}\models\varphi$ and $\mathfrak{B}$ is a
negative instance, so $\mathfrak{B}\not\models\varphi$. But, by Lemma 5.5, the
two structures are indistinguishable by $\varphi$ and we have a contradiction.

∎

##  6 Conclusion

Over ordered structures, the logic $\textsf{LREC}_{=}$ captures $\mathrm{L}$,
while FPC captures $\mathrm{P}$. So, it is of value to investigate the
relationship between the two logics. It was shown in [12] that
$\textsf{LREC}_{=}$ is contained in FPC, and the main result of this paper
shows the containment is proper. Our proof here uses novel techniques that
provide insight on the expressive power of $\textsf{LREC}_{=}$ and some of the
combinatorial properties of $\mathrm{PSP}$ that make it difficult to be solved
in $\mathrm{L}$.

These techniques can also be used to find further results. Firstly, the
Ehrenfeucht–Fraïssé game provides a new tool that can be used and adapted for
other inexpressibility results of the logic. Secondly, we note that the
combinatorial results in Section 4 use the characterization of a tree as a
matroid. The results can further be generalized to a larger class of finite
matroids, which would include constructing a more general definition of height
for arbitrary matroids. It is not clear whether it could be extended to all
classes of finite matroids however, as the argument relies on the fact that
the independent sets of the matroid is described concisely in the form of the
edge relation of the tree, and it is not true that all classes of finite
matroids can be described by a finite vocabulary. The results of Section 5 can
be generalized to larger classes of structures as well. This may for example
include considering other classes of matroids as the base set following from
the discussion above. Or, it may include constructing interpretations of
structures other than semi-graphs, as all that is required for the result is a
binary relation $\sim$, which is used to define a quotient structure of the
interpretation through its transitive reflexive symmetric closure.

The Path Systems Problem is not known to be in $\mathrm{L}$, and thus the
question of whether $\textsf{LREC}_{=}$ is equal to
$\textsf{FPC}\cap\mathrm{L}$ remains open. A result that they are equal would
imply that $\mathrm{L}\neq\mathrm{P}$, since $\mathrm{PSP}$ is in LFP and
hence in FPC. It also remains open for many classes of structures
$\mathcal{C}$ that are known to have logarithmic-space canonical labelling
algorithms whether $\textsf{LREC}_{=}$ captures $\mathrm{L}$ over
$\mathcal{C}$. Studying these classes may prove fruitful, as it is a direction
for solving the $\textsf{LREC}_{=}$ versus $\textsf{FPC}\cap\mathrm{L}$
problem.

As mentioned before, it remains open whether $\mathrm{PSP}$ is expressible in
some logics stronger than $\textsf{LREC}_{=}$, including the logic CLog. Of
course, one can also ask whether $\mathrm{PSP}$ is in $\mathrm{L}$ and this is
equivalent to asking if $\mathrm{L}$ is equal to $\mathrm{P}$, but the
question of whether $\mathrm{PSP}$ is in CLog does not seem to have been
investigated. Another related long-standing open problem is to find a logic
that captures $\mathrm{L}$ over all structures.

## References

  * [1] A. Atserias, A. Dawar, and J. Ochremiak.  On the power of symmetric linear programs.  In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS, pages 1–13, 2019.  doi:10.1109/LICS.2019.8785792.
  * [2] J-Y. Cai, M. Fürer, and N. Immerman.  An optimal lower bound on the number of variables for graph identification.  Combinatorica, 12(4):389–410, 1992.
  * [3] A. Dawar.  The nature and power of fixed-point logic with counting.  ACM SIGLOG News, 2(1):8–21, 2015.
  * [4] H-D. Ebbinghaus and J. Flum.  Finite Model Theory.  Springer, 2nd edition, 1999.
  * [5] K. Etessami and N. Immerman.  Tree canonization and transitive closure.  In Proceedings of Tenth Annual IEEE Symposium on Logic in Computer Science, pages 331–341, 1995.  doi:10.1109/LICS.1995.523268.
  * [6] Ronald Fagin.  Generalized first-order spectra, and polynomial. time recognizable sets.  SIAM-AMS Proc., 7, 01 1974.
  * [7] Erich Grädel and Gregory L. McColm.  On the power of deterministic transitive closures.  Inf. Comput., 119:129–135, 1995.  doi:10.1006/inco.1995.1081.
  * [8] Erich Grädel and Svenja Schalthöfer.  Choiceless Logarithmic Space.  In Peter Rossmanith, Pinar Heggernes, and Joost-Pieter Katoen, editors, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019), volume 138 of Leibniz International Proceedings in Informatics (LIPIcs), pages 31:1–31:15, Dagstuhl, Germany, 2019\. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.  URL: http://drops.dagstuhl.de/opus/volltexte/2019/10975, doi:10.4230/LIPIcs.MFCS.2019.31.
  * [9] M. Grohe and J. Mariño.  Definability and descriptive complexity on databases of bounded tree-width.  In Proc. 7th International Conference on Database Theory, volume 1540 of LNCS, pages 70–82. Springer, 1999.
  * [10] Martin Grohe.  Descriptive Complexity, Canonisation, and Definable Graph Structure Theory, volume 47 of Lecture Notes in Logic.  Cambridge University Press, 2017.
  * [11] Martin Grohe, Berit Grußien, André Hernich, and Bastian Laubner.  L-recursion and a new logic for logarithmic space.  Log. Methods Comput. Sci., 9, 2012.  doi:10.2168/LMCS-9(1:11)2013.
  * [12] Martin Grohe, Berit Grußien, André Hernich, and Bastian Laubner.  L-recursion and a new logic for logarithmic space.  Logical Methods in Computer Science, 9(1), Mar 2013.  URL: http://dx.doi.org/10.2168/LMCS-9(1:11)2013, doi:10.2168/lmcs-9(1:11)2013.
  * [13] Berit Grußien.  Capturing logarithmic space and polynomial time on chordal claw-free graphs.  Log. Methods Comput. Sci., 15, 2019.  doi:10.23638/LMCS-15(3:2)2019.
  * [14] N. Immerman.  Descriptive Complexity.  Springer, 1999.
  * [15] N. Immerman and E. S. Lander.  Describing graphs: A first-order approach to graph canonization.  In A. Selman, editor, Complexity Theory Retrospective. Springer-Verlag, 1990.
  * [16] L. Libkin.  Elements of Finite Model Theory.  Springer, 2004.