We study the expressive power of first-order logic with counting quantifiers, especially the $k$-variable and quantifier-rank-$q$ fragment $\mathsf{C}^k_q$, using homomorphism indistinguishability. Recently, Dawar, Jakl, and Reggio (2021) proved that two graphs satisfy the same $\mathsf{C}^k_q$-sentences iff they are homomorphism indistinguishable over the class $\mathcal{T}^k_q$ 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 $\mathcal{T}^k_q$. This allows us to separate $\mathcal{T}^k_q$ from the intersection $\mathcal{TW}_{k-1} \cap \mathcal{TD}_q$, provided that $q$ is sufficiently larger than $k$. Here $\mathcal{TW}_{k-1}$ is the class of all graphs of treewidth at most $k-1$ and $\mathcal{TD}_q$ is the class of all graphs of treedepth at most $q$. We are able to lift this separation to a separation of the respective homomorphism indistinguishability relations $\equiv_{\mathcal{T}^k_q}$ and $\equiv_{\mathcal{TW}_{k-1} \cap \mathcal{TD}_q}$. We do this by showing that the classes $\mathcal{TD}_q$ and $\mathcal{T}^k_q$ are homomorphism distinguishing closed, as conjectured by Roberson (2022). In order to prove Roberson's conjecture for $\mathcal{T}^k_q$, we characterise $\mathcal{T}^k_q$ 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 transform Cops' winning strategy into a pree-tree-decomposition, which is inspired by decompositions of matroids, and then apply an intricate breadth-first cleaning up procedure along the pree-tree-decomposition (which may temporarily lose the property of representing a strategy). Thereby, we achieve monotonicity while controlling the number of rounds across all branches of the decomposition via a vertex exchange argument.
翻译:我们通过同态不可区分性研究带计数量词的一阶逻辑的表达能力,特别是 $k$ 变量且量词秩为 $q$ 的片段 $\mathsf{C}^k_q$。最近,Dawar、Jakl 和 Reggio(2021)证明,两个图满足相同的 $\mathsf{C}^k_q$ 语句当且仅当它们在允许深度为 $q$ 的 $k$-卵石森林覆盖的图类 $\mathcal{T}^k_q$ 上是同态不可区分的。在利用初等方法重新证明此结果后,我们对 $\mathcal{T}^k_q$ 进行了图论分析。这使得我们能够将 $\mathcal{T}^k_q$ 与交集 $\mathcal{TW}_{k-1} \cap \mathcal{TD}_q$ 分离开来,前提是 $q$ 充分大于 $k$。这里 $\mathcal{TW}_{k-1}$ 是所有树宽至多为 $k-1$ 的图的类,而 $\mathcal{TD}_q$ 是所有树深至多为 $q$ 的图的类。我们能够将这种分离提升到相应同态不可区分关系 $\equiv_{\mathcal{T}^k_q}$ 和 $\equiv_{\mathcal{TW}_{k-1} \cap \mathcal{TD}_q}$ 的分离。我们通过证明类 $\mathcal{TD}_q$ 和 $\mathcal{T}^k_q$ 是同态区分封闭的来实现这一点,正如 Roberson(2022)所猜想的那样。为了证明 Roberson 关于 $\mathcal{T}^k_q$ 的猜想,我们通过一种单调的警察与强盗游戏来刻画 $\mathcal{T}^k_q$。关键在于证明如果警察有必胜策略,那么警察也存在一个单调的必胜策略。为此,我们将警察的必胜策略转化为一种预树分解(这受到拟阵分解的启发),然后沿着预树分解应用一种复杂的广度优先清理过程(该过程可能会暂时失去表示策略的性质)。通过这种方式,我们在通过顶点交换论证控制分解所有分支上的回合数的同时,实现了单调性。