Finite Variable Counting Logics with Restricted Requantification

Let us denote by ${𝖢}^{(k_1,k_2)}$ the fragment of first-order logic with counting quantifiers in which the formulas have at most $k_1$ variables that may be requantified and at most $k_2$ variables that may not be requantified.

First, we show that many of the traditional techniques of treating counting logics can be adapted to the setting of limited requantification. Specifically, it is well known that there is a close ternary correspondence between the logic ${𝖢}^k$, the combinatorial bijective $k$-pebble game, and the famous $(k-1)$-dimensional Weisfeiler-Leman algorithm [3, 22, 26]. We develop versions of the game and the algorithm that also have a limit on the reusability of resources. For the pebble game, a limit on requantification translates into pebbles that cannot be picked up anymore, once they have been placed. For the Weisfeiler-Leman algorithm, the limit on requantification translates into having some dimensions that “cannot be reused”. In fact the translation to the algorithmic viewpoint is not as straightforward as one might hope at first. Indeed, we do not know how to define a restricted version of the classical Weisfeiler-Leman algorithm that corresponds to the logic ${𝖢}^{(k_1,k_2)}$. However, we circumvent this problem by employing the oblivious Weisfeiler-Leman algorithm (OWL). This variant is often used in the context of machine learning. In fact, Grohe [17] recently showed that $k+1$-dimensional OWL is in fact exactly as powerful as $k$-dimensional (classical) WL. We develop a resource-reuse restricted version of the oblivious algorithm and prove equivalence to our logic. Indeed, we formally prove precisely matching correspondences between the limited requantification, limited pebble reusability, and the limited reusable dimensions (Theorem 6).

Next, we conclusively clarify the relation between the logics within the two-parametric family ${𝖢}^{(k_1,k_2)}$. We show that in most cases limiting the requantifiability of a variable strictly reduces the power of the logic. We argue that no amount of requantification-restricted variables is sufficient to compensate the loss of an unrestricted variable. However, these statements are only true if at least some requantifiable variable remains. In fact, exceptionally, ${𝖢}^{(1,k_2)}$ is strictly less expressive than ${𝖢}^{(0,k_2^{\prime })}$ whenever $k_2^{\prime }>2k_2$ (Theorem 13). To show the separation results, we adapt a construction of Fürer [13] and develop a cops-and-robber game similar to those in [12, 19]. In this version, some of the cops may repeatedly change their location, while others can only choose a location once and for all. Using another graph construction, we rule out various a priori tempting ideas concerning normal forms in ${𝖢}^{(k_1,k_2)}$. To this end we show that formulas in the logics can essentially become as complicated as possible, having to repeatedly requantify all of the requantifiable variables an unbounded number of times, before using a non-requantifiable variable (Corollary 16). In terms of the pebble game, it seems a priori unclear when an optimal strategy would employ the non-reusable pebbles. However, the corollary says that in general one has to conserve the non-reusable pebbles for possibly many moves until a favorable position calls for them.

Having gone through the technical challenges that come with the introduction of reusability, puts us into a position to discuss the implications. Indeed, as our main result, we argue that our finer grained view on counting logics through restricted requantification has beneficial algorithmic implications. Specifically, we show that equivalence with respect to the logic ${𝖢}^{(k_1,k_2)}$ can be decided in polynomial time with a space complexity of $O\left(n^{k_1}\log n\right)$, hiding quadratic factors depending only on $k_1$ and $k_2$ (Theorem 24). This shows that while the requantifiable variables each incur a multiplicative linear factor in required space, the restricted variables only incur an additive polynomial factor. In particular, equivalence with respect to the logics ${𝖢}^{(0,k_2)}$ can be decided in logarithmic space. To show these statements, we leverage the fact that, because non-requantifiable variables cannot simultaneously occur free and bound, the ${𝖢}^{(k_1,k_2)}$-type of a variable assignment does not depend on the ${𝖢}^{(k_1,k_2)}$-type of assignments which disagree regarding non-requantifiable variables. Moreover, we use ideas from an algorithm of Lindell, which computes isomorphism of trees in logarithmic space [30] to implement the iteration steps of our algorithm. Generally, we believe the new viewpoint may be of interest in particular for applications in machine learning, where the WL-hierarchy appears to be too coarse for actual applications with graph neural networks (see for example [1, 2, 31, 40]). In the process of the space complexity proof, we also show that the iteration number of the resource-restricted Weisfeiler-Leman algorithm described above is at most $(k_2+1)n^{k_1}-1$ (Corollary 19).

Justifying the new concepts of restricted reusability, we observe that there are interesting graph classes that are identified by the logics ${𝖢}^{(k_1,k_2)}$. We argue that ${𝖢}^{(0,d+1)}$ identifies all graphs of tree-depth at most $d$ (Theorem 27) and that ${𝖢}^{(2,2)}$ identifies all $3$-connected planar graphs (Theorem 33).

After briefly providing necessary preliminaries (Section 2) we formally introduce the logics ${𝖢}^{(k_1,k_2)}$, the pebble game with non-reusable pebbles, the $(k_1,k_2)$-dimensional oblivious Weisfeiler-Leman algorithm, and prove the correspondence theorem between them (Section 3). We then relate the power of the logics to each other and rule out certain normal forms (Section 4). We then analyze the space complexity (Section 5) and finally provide two classes of graphs that are identified by our logics (Section 6).

In addition to the references above, let us mention related investigations. Over time, a large body of work on descriptive complexity has evolved. For insights into fundamental results regarding bounded variable logics, we refer to classic texts [25, 26, 33, 34]. However, highlighting the importance of the counting logics ${𝖢}^k$, let us at least mention the Immerman-Vardi theorem [24, 39]. It says that on ordered structures, least fixed-point logic LFP captures P. Since LFP has the same expressive power as IFP+C on ordered structures, also IFP+C, whose expressive power is closely related to the expressive power of the logics ${𝖢}^k$, captures P. We should also mention the work of Hella [22] introducing the bijective $k$-pebble game which forms the basis for our resource restricted versions.

(Counting logics on graph classes)

Because of the close correspondence between the logic ${𝖢}^k$ and the $(k-1)$-dimensional Weisfeiler-Leman algorithm, our investigations are closely related to the notion of the Weisfeiler-Leman dimension of a graph defined in [15]. Given a graph $G$ this is the least number of variables $k$ such that ${𝖢}^{k+1}$ identifies $G$. In particular, on every graph class of bounded Weisfeiler-Leman dimension, the corresponding finite variable counting logic captures isomorphism. Graph classes with bounded Weisfeiler-Leman dimension include graphs with a forbidden minor [14] and graphs of bounded rank-width (or equivalently clique width) [20], which in both cases is also shown to imply that IFP+C captures P on these classes. For a comprehensive survey we refer to [27]. Our observations for planar graphs follow from techniques bounding the number of variables required for the identification of planar graphs [28]. Other recent classes not already captured by the results on excluded minors and rank-width include, for example, some polyhedral graphs [29], some strongly regular graphs [4], and permutation graphs [21].

(Logic and tree decompositions)

In [9] and independently [8] it was shown that ${𝖢}^k$-equivalence is characterized by homomorphism counts from graphs of tree-width at most $k-1$. Likewise, homomorphism counts from bounded tree-depth graphs characterize equivalence in counting logic of bounded quantifier-rank [16]. Recently, these results were unified to characterize logical equivalence in finite variable counting logics with bounded quantifier-rank in terms of homomorphism counts [12].

(Space complexity)

Ideas underlying Lindell’s logspace algorithm for tree isomorphism have also been used in the context of planar graphs [6] and more generally bounded genus graphs [10]. Similar results exist for classes of bounded tree-width [5, 11].

(Further recent results)

Let us mention some quite recent results in the vicinity of our work that cannot be found in the surveys mentioned above. Regarding the quantifier-rank within counting logics, there is a recent superlinear lower bound [19] improving Fürer’s linear lower bound construction [13]. Further, very recent work on logics with counting includes results on rooted unranked trees [23] and inapproximability of questions on unique games [35]. Finally, there has been a surge in research on descriptive complexity within the context of machine learning (see [17, 36, 37]).

For $n\in {\mathbb{N}}_{+}$ we use $[n]$ to denote the $n$-element set $\{1,\mathrm{\dots },n\}$. We use the notation $\{\{v_1,\mathrm{\dots },v_n\}\}$ for multisets. For $k_1,k_2\in {\mathbb{N}}_{+}$, we fix the variable sets $[x_{k_1}]≔\{x_1,\mathrm{\dots },x_{k_1}\}$, $[y_{k_2}]≔\{y_1,\mathrm{\dots },y_{k_2}\}$, and $[x_{k_1},y_{k_2}]≔\{x_1,\mathrm{\dots },x_{k_1},y_1,\mathrm{\dots },y_{k_2}\}$. Given a set $V$, a partial function $\alpha :[x_{k_1},y_{k_2}]\rightharpoonup V$ assigns to every variable $z\in [x_{k_1},y_{k_2}]$ at most one element $\alpha (z)\in V$. If $\alpha$ does not assign an element to $z$, we write $\alpha (z)=\perp$. Also, we write $\mathrm{im}(\alpha )$ for the image of $\alpha$. With a finite set $V$ and $\alpha :[x_{k_1},y_{k_2}]\rightharpoonup V$ we associate the total function $\overline{\alpha }:[x_{k_1},y_{k_2}]\to V\dot{\cup }\{\perp \}$, which we also view as a $[x_{k_1},y_{k_2}]$-indexed $(k_1+k_2)$-tuple. For $z\in [x_{k_1},y_{k_2}]$ and $v\in V$, the function $\alpha [z/v]$ is defined as $\alpha$ but with $\alpha (z)$ replaced by $v$.

A graph is a pair $G=(V(G),E(G))$ consisting of a finite set $V(G)$ of vertices and a set $E(G)\subseteq \left(\genfrac{}{}{0pt}{}{V(G)}{2}\right)$ of edges. We write $|G|$ for the number of vertices, called the order of $G$. For a vertex $v\in V(G)$ we define the neighborhood $N_G(v)≔\{w\in V(G):\{v,w\}\in E(G)\}$ and the degree $d_G(v)≔|N_G(v)|$ of $v$ in $G$. We call $v$ universal in $G$ if $N_G(v)=V(G)\setminus \{v\}$. A colored graph consists of a graph $G$ and a coloring function $\chi :V(G)\to C$ with a finite, ordered set $C$ of colors. For a colored graph $G$ and vertices $v_1,\mathrm{\dots },v_n\in V(G)$ the graph $G_{(v_1,\mathrm{\dots },v_n)}$ is obtained by assigning new and distinct colors to the vertices $v_1,\mathrm{\dots },v_n$ in $G$. The vertices $v_1,\mathrm{\dots },v_n$ are then called individualized. An isomorphism of (colored) graphs $G$ and $H$ is a bijection $\phi :V(G)\to V(H)$ that preserves edges, non-edges, and vertex-colors.

We denote the complete graph on $n$ vertices by $K_n$, that is, the graph with vertex set $[n]$ and all possible edges included. A star of degree $n$ is a graph consisting of one universal vertex of degree $n$ and its neighbors of degree $1$.

First-order logic with counting $𝖢$ is an extension of first-order logic by counting quantifiers ${\exists }^{\ge k}$ for all $k\in \mathbb{N}$. These intuitively state that there exist at least $k$ distinct vertices satisfying the formula that follows.

Over the language of colored graphs with variable set $𝒱$, formulas are inductively built up from atomic formulas (for stating equality or adjacency of vertices as well as for stating that a vertex has a given vertex color) via negation ($\neg$), conjunction ($\wedge$), disjunction ($\vee$), implication ($\to$), and quantification over vertices via $\forall$, $\exists$ and the counting quantifiers ${\exists }^{\ge k}$. For a colored graph $G$, a variable assignment $\alpha :𝒱\to V(G)$, and a formula $\phi \in 𝖢$, we write $G,\alpha \vDash \phi$ if the graph $G$ together with the variable assignment $\alpha$ satisfies the formula $\phi$.

The quantifier-rank $\mathrm{qr}(\phi )$ of a formula $\phi$ is the maximum depth of nested quantifiers in the formula. The set of free variables $\mathrm{free}(\phi )$ of a formula $\phi$ is defined as the set of all variables that occur outside the scope of a corresponding quantifier in $\phi$. If $\mathrm{free}(\phi )=\mathrm{\varnothing }$ the formula $\phi$ is called a sentence. The set of bound variables $\mathrm{bound}(\phi )$ is the set of all variables that occur quantified in $\phi$. If we restrict to a finite set of $k\in {\mathbb{N}}_{+}$ variables, the resulting logic is called $k$-variable counting logic and denoted by ${𝖢}^k$. For $r\in \mathbb{N}$ the quantifier-rank-$r$ counting logic ${𝖢}_r$ is obtained by restricting formulas in $𝖢$ to quantifier-rank at most $r$. The $k$-variable quantifier-rank-$r$ counting logic is defined as ${𝖢}_r^k≔{𝖢}^k\cap {𝖢}_r$.

As a general reference on finite variable logics, we refer to [33].

Let $k\ge 1$ and $G$ be a colored graph. The $k$-dimensional Weisfeiler-Leman algorithm (short $k$-WL) iteratively computes a coloring of the $k$-tuples of vertices of $G$. We also view the $k$-tuples as total functions $\overline{\alpha }:\{x_1,\mathrm{\dots },x_k\}\to V(G)$. Initially, each tuple $\overline{\alpha }\in V{(G)}^k$ is colored by ${\mathrm{wl}}_k^{(0)}(G,\overline{\alpha })≔{\mathrm{atp}}_k(G,\overline{\alpha })$. Here, ${\mathrm{atp}}_k(G,\overline{\alpha })$ is the atomic type of $\overline{\alpha }$ in $G$, i.e., the set of all atomic formulas with variables in $\{x_1,\mathrm{\dots },x_k\}$ satisfied by the colored graph $G[\mathrm{im}(\alpha )]$ together with the assignment $\alpha$. For every $r\in \mathbb{N}$, we then inductively set

whenever $k\ge 2$, but for the case $k=1$ we set

We write ${\mathrm{wl}}_k^{(r)}(G)$ for the coloring of all $k$-tuples of vertices of $G$ assigning ${\mathrm{wl}}_k^{(r+1)}(G,\overline{\alpha })$ to $\overline{\alpha }$. Since the definition of ${\mathrm{wl}}_k^{(r+1)}(G,\overline{\alpha })$ includes the color ${\mathrm{wl}}_k^{(r)}(G,\overline{\alpha })$ of the previous iteration, the coloring ${\mathrm{wl}}_k^{(r+1)}(G)$ refines the coloring ${\mathrm{wl}}_k^{(r)}(G)$. That is, whenever ${\mathrm{wl}}_k^{(r+1)}(G,\overline{{\alpha }_1})={\mathrm{wl}}_k^{(r+1)}(G,\overline{{\alpha }_2})$ for $\overline{{\alpha }_1},\overline{{\alpha }_2}\in V{(G)}^k$, then we also have ${\mathrm{wl}}_k^{(r)}(G,\overline{{\alpha }_1})={\mathrm{wl}}_k^{(r)}(G,\overline{{\alpha }_2})$. Since there are exactly ${|V(G)|}^k$-many $k$-tuples of vertices, there exists an such that ${\mathrm{wl}}_k^{(r)}(G)$ induces the same partition of color classes as ${\mathrm{wl}}_k^{(r+1)}(G)$. It follows from the definition of the refinement that this implies ${\mathrm{wl}}_k^{(r)}(G)$ induces the same partition as ${\mathrm{wl}}_k^{(r^{\prime })}(G)$ for all $r^{\prime }\ge r$. In this case we say that $k$-WL stabilizes after at most $r$ iterations on the graph $G$. If $r$ is minimal with this property, we write ${\mathrm{wl}}_k^{(\mathrm{\infty })}(G)≔{\mathrm{wl}}_k^{(r+1)}(G)$ and call ${\mathrm{wl}}_k^{(\mathrm{\infty })}(G)$ the stable coloring. For a second colored graph $H$, we say that $k$-WL distinguishes $G$ and $H$ after $r$ iterations if there exists a color $c$ such that $|\{\overline{\alpha }\in V{(G)}^k:{\mathrm{wl}}_k^{(r)}(G,\overline{\alpha })=c\}|\ne |\{\overline{\beta }\in V{(H)}^k:{\mathrm{wl}}_k^{(r)}(H,\overline{\beta })=c\}|.$

Besides the classical $k$-dimensional Weisfeiler-Leman algorithm, there also exists a variant, called the $(k+1)$-dimensional oblivious Weisfeiler-Leman algorithm (short $(k+1)$-OWL). This variant colors $(k+1)$-tuples of vertices, which we again view as total functions $\overline{\alpha }:\{x_1,\mathrm{\dots },x_{k+1}\}\to V(G)$. Initially, all tuples are colored by their atomic type: ${\mathrm{owl}}_{k+1}^{(0)}(G,\overline{\alpha })≔{\mathrm{atp}}_{k+1}(G,\overline{\alpha })$. Then, this coloring is iteratively refined by setting

The stable coloring ${\mathrm{owl}}_{k+1}^{(\mathrm{\infty })}(G)$ and the notion of distinguishing graphs is defined as for $k$-WL.

It turns out that $k$-WL and $(k+1)$-OWL have the same distinguishing power.

First, consider the game ${\mathrm{CR}}_{(k_1,k_2)}(G_{(k_1-1)\times (k_1{2}^{2k_2^{\prime }}+1)})$. The cops can build a barrier in the middle of the grid and move it towards the robber only using reusable cops. This is a winning strategy for the cops since the size of the component containing the robber is decreased by a constant in each round and eventually vanishes. On the other hand, we show that the robber has a winning strategy in the game ${\mathrm{CR}}_{(k_1^{\prime },k_2^{\prime })}(G_{(k_1-1)\times (k_1{2}^{2k_2^{\prime }}+1)})$ by induction on $k_2^{\prime }$. The base case for $k_2^{\prime }=0$ is the game ${\mathrm{CR}}_{(k_1^{\prime },0)}(G_{(k_1-1)\times (k_1+1)})$, for which the robber has a winning strategy as a barrier can be built, but not moved. For the inductive step assume $k_2^{\prime }>0$ and consider the game ${\mathrm{CR}}_{(k_1^{\prime },k_2^{\prime }+1)}(G_{(k_1-1)\times (k_1{2}^{2k_2^{\prime }+2}+1)})$. Using only reusable cops, the cops can reduce the size of the robber component with a barrier. However, the size remains at least $(k_1-1)\cdot (k_1{2}^{2k_2^{\prime }+1}+1)$, since the robber can choose the larger induced component. When a reusable cop is reused before a non-reusable cop was used to build another barrier, the reusable barrier breaks down and the robber as an escape strategy. Using non-reusable cops, the cops can build another wall to reduce the size of the robber component to $(k_1-1)\cdot (k_1{2}^{2k_2^{\prime }}+1)$. Again, the robber chooses the larger induced component. But now the remaining game is ${\mathrm{CR}}_{(k_1^{\prime },k_2^{\prime }-k_1+2)}(G_{(k_1-1)\times (k_1{2}^{2k_2^{\prime }}+1)})$ and we have $k_2^{\prime }\ge k_2^{\prime }-k_1+2$. Thus, by the inductive hypothesis the robber has a winning strategy for the remaining game. $◀$

Second, we show the advantages of mere capacity: When the base graph is chosen as a complete graph, the robber can choose any edge independently of the choice of vertices by the cops and the only possibility to win for the cops is to have sufficient capacity. In this case, capacity is more valuable than reusability.

In the game ${\mathrm{CR}}_{(k_1,k_2)}(K_{k_1+k_2})$, the cops have a winning strategy just by covering all base vertices. In contrast, in the game ${\mathrm{CR}}_{(k_1^{\prime },k_2^{\prime })}(K_{k_1+k_2})$ the robber has a winning strategy. Whenever a cop is picked up there is one edge that is not incident to a cop and thus yields a safe escape for the robber. $◀$

Third, we treat the special case of a single requantifiable variable: Intuitively, at least two reusable cops are needed to move a barrier for an arbitrarily large distance in a base graph. When only one single reusable cop is available, the distance that can be covered by a barrier of cops is bounded by $2k_1+1$ because for every other move a non-reusable cop must be used. The perfect binary tree of depth $d$ is the binary tree $B^d$ such that all interior vertices have two children and all leaves have the same depth.

In the game ${\mathrm{CR}}_{(1,k_2)}(B^{2k_2})$, the cops have a winning strategy by alternately using non-reusable cops and the reusable cop. In the game ${\mathrm{CR}}_{(0,2k_2)}(B^{2k_2})$ the robber has a winning strategy as the non-reusable cops are exhausted before the robber is caught. This yields ${𝖢}^{(1,k_2)}⋠{𝖢}^{(0,2k_2)}$. For $k_2^{\prime }\le 2k_2$ we get ${𝖢}^{(1,k_2)}⋠{𝖢}^{(0,k_2^{\prime })}$ since the robber wins with the same strategy in ${\mathrm{CR}}_{(0,k_2^{\prime })}(B^{2k_2})$. For $k_2^{\prime }>2k_2$, let (S) have a winning strategy for ${\mathrm{BP}}_{(1,k_2)}(G,H)$. Then (S) has a winning strategy for ${\mathrm{BP}}_{(1,k_2)}^{2k_2+1}(G,H)$ since consecutive moves involving the pebble pair $x_1$ can be replaced by a single move instead. The winning strategy for (S) in ${\mathrm{BP}}_{(1,k_2)}^{2k_2+1}(G,H)$ directly yields a winning strategy for (S) in ${\mathrm{BP}}_{(0,k_2^{\prime })}(G,H)$: For every pebble pair played by (S) in ${\mathrm{BP}}_{(1,k_2)}^{2k_2+1}(G,H)$, the player (S) can use a new pair in ${\mathrm{BP}}_{(0,k_2^{\prime })}(G,H)$. $◀$

With the previous lemmas we can determine the relation of the logics ${𝖢}^{(k_1,k_2)}$ and ${𝖢}^{(k_1^{\prime },k_2^{\prime })}$ for any given combination of parameters.

This settles the question of how the use of non-requantifiable variables affects the expressive power of the logic. For the investigation of the logic ${𝖢}^{(k_1,k_2)}$ for fixed parameters, it is also of interest how the non-requantifiable variables behave in concrete formulas of the logic. This relates closely to asking whether there are normal forms for the logic ${𝖢}^{(k_1,k_2)}$ with respect to reusability. We give a precise answer to this question that rules out many such normal forms. The idea is to construct a new family of base graphs that allow the use of non-reusable cops only after all reusable cops have been used a certain number of times.

For $k_1>1$, we consider the game ${\mathrm{CR}}_{(k_1,k_2)}(B_{(k_1-1)\times 2r}^{k_2+1})$, see Figure 1. The cops have the following winning strategy: First, they build a barrier in the root grid (behind the bridge vertex) by occupying one full column using $k_1$ reusable cops. The barrier can then be moved towards the robber using the additional reusable cop. When the barrier reaches the last column, the two subtrees induced by the children of the root grid are disconnected components with respect to the cops. Thus, the robber has to choose an edge in one of these components to escape to. The cops move the barrier into the corresponding subtree, which essentially results in the game ${\mathrm{CR}}_{(k_1,k_2)}(B_{(k_1-1)\times 2r}^{k_2})$. In every grid of the tree, the cops encounter a bridge vertex that can be covered by one of the $k_2$ non-reusable cops. The game continues inductively for $\mathrm{\Omega }(r{k}_2)$ rounds, until the cops use the last remaining non-reusable cop to cover the bridge vertex in a leaf grid. The barrier can be moved to the end of the grid and the robber will be caught. Now assume a new non-reusable cop $y$ has been used before all reusable cops have been (re)used $r$ times at some point of the game. Then the barrier was not moved out of the current grid at this point, since all reusable cops have to be moved at least $r$ times to achieve this. Hence, the robber has not chosen a new subtree so far and can pick an edge in a subtree that does not contain $y$. The cops need to move the barrier into that subtree and use non-reusable cops for the bridge vertices. Since $y$ was used in another subtree, at some point there will be no non-reusable cops left to cover a bridge vertex and the barrier cannot be moved further without breaking down. Thus, the robber can escape indefinitely. For $k_1=1$ we consider the game ${\mathrm{CR}}_{(1,k_2)}(B^{2k_2})$. The cops have the following winning strategy: First, the reusable cop $x_1$ is placed in the root node. This disconnects the subtrees induced by the two children of the root node for the robber, and the robber has to choose an edge in one of the subtrees of depth $2k_2-1$. Accordingly, a non-reusable cop $y_1$ is placed on the node inducing that subtree, which again disconnects two subtrees of depth $2k_2-2$. The cop $x_1$ can be picked up again from the root node to be placed on the corresponding subtree. Inductively, the cops alternately use non-reusable cops $y_j$ and the reusable cop $x_1$ to cover the next child node. After $2k_2$ moves, the induced subtree is of depth $0$ and the robber is caught in the edge to a leaf node. If two non-reusable cops are used consecutively, similar to the case $k_1>1$, there are no non-reusable cops left at depth $2k_2-1$ and the remaining reusable cop does not suffice to catch the robber. $◀$

Again using Theorem 6 this result translates into the language of logic as follows:

The necessity of this pattern of (re)quantification rules out various normal forms with respect to requantification for ${𝖢}^{(k_1,k_2)}$ one might have hoped to have. In particular, it is not sufficient to quantify all non-requantifiable variables directly one after the other.

Regarding classical logics without restricted requantification, Theorem 13 and Corollary 16 yield that for $k_1,k_2\ge 1$ the power of ${𝖢}^{(k_1,k_2)}$ to distinguish graphs is not identical to that of ${𝖢}^k,{𝖢}_r,$ or ${𝖢}_r^k$ for all $k,r\in \mathbb{N}$.