Going deep and going wide: Counting logic and homomorphism indistinguishability over graphs of bounded treedepth and treewidth
Pith reviewed 2026-05-22 17:42 UTC · model grok-4.3
The pith
Two graphs agree on all k-variable quantifier-rank-q counting logic sentences precisely when no homomorphism from a k-pebble forest cover of depth q distinguishes them.
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
Core claim
The central claim is that the equivalence relation induced by k-variable quantifier-rank-q sentences of first-order logic with counting coincides exactly with homomorphism indistinguishability over the class of graphs admitting a k-pebble forest cover of depth q. This class is homomorphism-distinguishing closed, and the induced indistinguishability relation is strictly finer than the one obtained from the intersection of treewidth-(k-1) graphs and treedepth-q graphs when q is large enough relative to k. The class itself is characterized by the existence of a winning monotone strategy for Cop in a cops-and-robbers game of appropriate width and length.
What carries the argument
A k-pebble forest cover of depth q, which is a graph equipped with a forest decomposition and a pebbling assignment that together bound the number of rounds and pebbles needed in a game; this structure serves as the test objects whose homomorphisms reproduce the distinctions made by the logic fragment.
If this is right
- The class of graphs admitting k-pebble forest covers of depth q is homomorphism-distinguishing closed.
- For large enough q this class strictly contains the intersection of treewidth at most k-1 and treedepth at most q.
- The strict containment between the graph classes lifts to a strict containment between the two homomorphism indistinguishability relations they induce.
- The class admits an exact characterization by the existence of monotone winning strategies in a cops-and-robbers game whose pebble number and round number are bounded by k and q.
Where Pith is reading between the lines
- If the equivalence holds, then deciding whether two graphs satisfy the same sentences of the logic fragment reduces to checking homomorphism existence over a class whose structure is governed by a monotone game.
- The same monotonicity transformation technique may extend to other game characterizations that arise in logical or algorithmic contexts on graphs.
- The separation result suggests that logical power cannot be captured by any single bounded-width parameter that combines treewidth and treedepth in the obvious way.
Load-bearing premise
The procedure that converts an arbitrary winning cops-and-robbers strategy into a monotone one by first forming a pre-tree-decomposition and then performing a breadth-first cleaning step preserves both the winning property and the round bound on every branch of the decomposition.
What would settle it
A pair of graphs that satisfy identical k-variable quantifier-rank-q counting sentences yet are distinguished by a homomorphism from some graph admitting a k-pebble forest cover of depth q would falsify the claimed equivalence.
read the original abstract
We study the expressive power of first-order logic with counting quantifiers, especially the $k$-variable and quantifier-rank-$q$ fragment, using homomorphism indistinguishability. Recently, Dawar, Jakl, and Reggio~(2021) proved that two graphs satisfy the same $k$-variable and quantifier-rank-$q$ sentences if and only if they are homomorphism indistinguishable over the class of graphs admitting a $k$-pebble forest cover of depth $q$. After reproving this result using elementary means, we provide a graph-theoretic analysis of this graph class. This allows us to separate it from the intersection of the class of all graphs of treewidth at most $k-1$ and the class of all graphs of treedepth at most $q$, provided that $q$ is sufficiently larger than $k$. We are able to lift this separation to a (semantic) separation of the respective homomorphism indistinguishability relations. We do this by showing that the graph classes of all graphs of treedepth at most $q$ and of graphs admitting a $k$-pebble forest cover of depth $q$ are homomorphism distinguishing closed, as conjectured by Roberson~(2022). In order to prove Roberson's conjecture for the class of graphs admitting a $k$-pebble forest cover of depth $q$ we characterise the class in terms of a monotone Cops-and-Robber game.The crux is to prove that if Cop has a winning strategy then Cop also has a winning strategy that is monotone.To that end, we show how to transform Cop's winning strategy into a pre-tree-decomposition, which is inspired by decompositions of matroids, and then applying an intricate breadth-first `cleaning up' procedure along the pre-tree-decomposition (which may temporarily lose the property of representing a strategy), in order to achieve monotonicity while controlling the number of rounds simultaneously across all branches of the decomposition via a vertex exchange argument.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper reproves that two graphs satisfy the same k-variable, quantifier-rank-q sentences of first-order logic with counting if and only if they are homomorphism indistinguishable over graphs admitting a k-pebble forest cover of depth q. It then provides a graph-theoretic analysis showing this class strictly contains the intersection of treewidth-(k-1) and treedepth-q graphs for sufficiently large q, and lifts the separation to the homomorphism indistinguishability relations by proving that both the treedepth-q class and the k-pebble forest cover class are homomorphism-distinguishing closed (confirming Roberson's conjecture for the latter). The closure proof for the pebble-forest class rests on a monotone Cops-and-Robber characterization obtained by transforming arbitrary winning strategies into pre-tree-decompositions followed by breadth-first cleaning and vertex exchange.
Significance. If the results hold, this supplies an elementary reproof of a central equivalence between counting logic and homomorphism indistinguishability, together with a strict separation from the natural intersection of bounded-treewidth and bounded-treedepth classes. Confirming homomorphism-distinguishing closure for these classes resolves a conjecture and clarifies the landscape of indistinguishability relations. The elementary reproof and the explicit graph-theoretic separation are clear strengths.
major comments (1)
- [monotone Cops-and-Robber characterization] The section on the monotone Cops-and-Robber characterization: the vertex-exchange step in the breadth-first cleaning procedure along the pre-tree-decomposition must simultaneously preserve the round bound q on every branch while restoring monotonicity. Because this step is load-bearing for both the equivalence to quantifier-rank-q sentences and the homomorphism-distinguishing closure, a more explicit argument or small illustrative example confirming that no branch exceeds depth q would strengthen the claim.
Simulated Author's Rebuttal
We thank the referee for the positive assessment of our manuscript and for the constructive suggestion to strengthen the presentation of the monotone Cops-and-Robber characterization. We address the single major comment below and will revise the manuscript accordingly.
read point-by-point responses
-
Referee: [monotone Cops-and-Robber characterization] The section on the monotone Cops-and-Robber characterization: the vertex-exchange step in the breadth-first cleaning procedure along the pre-tree-decomposition must simultaneously preserve the round bound q on every branch while restoring monotonicity. Because this step is load-bearing for both the equivalence to quantifier-rank-q sentences and the homomorphism-distinguishing closure, a more explicit argument or small illustrative example confirming that no branch exceeds depth q would strengthen the claim.
Authors: We agree that an expanded explanation of the vertex-exchange step would improve clarity. In the revised version we will insert a detailed paragraph immediately after the description of the breadth-first cleaning procedure that explicitly tracks the round counter on each branch of the pre-tree-decomposition. We will also add a short worked example (a 4-vertex pre-tree-decomposition with two branches) showing the sequence of vertex exchanges, the resulting bags, and the verification that every branch remains of depth at most q while monotonicity is restored. This addition directly addresses the load-bearing role of the argument for both the logical equivalence and the homomorphism-distinguishing closure. revision: yes
Circularity Check
Derivation self-contained from standard graph-theoretic definitions and game rules
full rationale
The paper reproves the Dawar-Jakl-Reggio equivalence using elementary means from first-order logic with counting and homomorphism indistinguishability. It then characterizes the k-pebble forest cover class via a monotone Cops-and-Robber game, transforming arbitrary winning strategies into pre-tree-decompositions followed by breadth-first cleaning and vertex exchange. These steps are presented as direct constructions from game rules and decomposition properties, without reducing any central claim (homomorphism-distinguishing closure, separation from treewidth/treedepth intersection) to a fitted parameter, self-definition, or load-bearing self-citation. The cited results (Dawar et al. 2021, Roberson 2022) are external and the proofs remain independent of the paper's own fitted values or prior outputs.
Axiom & Free-Parameter Ledger
axioms (2)
- standard math Standard definitions of treewidth, treedepth, and homomorphism indistinguishability from prior literature.
- domain assumption Existence of a winning strategy in the k-pebble cops-and-robbers game implies existence of a pre-tree-decomposition.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.