一句话：证明有根无秩树上任意一元一阶查询都可在带计数的二变量一阶逻辑中表达。
论文研究有限、有根、无秩、无序且节点标记的树，这类树仅含父子关系以及用于节点标签的一元谓词。核心问题是：树上一阶逻辑的一元查询是否都能由带计数的二变量一阶逻辑表达。作者证明答案为是：每个一元一阶查询都等价于该受限逻辑公式，并指出这一表达完备性此前在树逻辑文献中未被明确猜想。证明方法引入节点局部等价概念的全局变体，将局部等价扩展到整棵树，并通过计数局部等价节点的祖先来构造等价公式。评估为纯数学证明，未涉及实现或实验。
We consider the class of finite, rooted, unranked, unordered, node-labeled trees. Such trees are represented as structures with only the parent-child relation, in addition to any number of unary predicates for node labels. We prove that every unary first-order query over the considered class of trees is already expressible in two-variable first-order logic with counting. Somewhat to our surprise, we have not seen this result being conjectured in the extensive literature on logics for trees. Our proof is based on a global variant of local equivalence notions on nodes of trees. This variant applies to entire trees, and involves counting ancestors of locally equivalent nodes.
@inproceedings{HellingsGBG23,
title = {Expressive Completeness of Two-Variable First-Order Logic with Counting for First-Order Logic Queries on Rooted Unranked Trees},
author = {Jelle Hellings and Marc Gyssens and Jan Van Den Bussche and Dirk Van Gucht},
booktitle = {LICS},
year = {2023},
doi = {10.1109/lics56636.2023.10175828}
}