Expressive Completeness of Two-Variable First-Order Logic with Counting for First-Order Logic Queries on Rooted Unranked Trees.

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.