Unary quantifiers, transitive closure, and relations of large degree

This paper studies expressivity bounds for extensions of first-order logic with counting and unary quantifiers in the presence of relations of large degree. There are several motivations for this work. First, it is known that first-order logic with counting quantifiers captures uniform TC° over ordered structures. Thus, proving expressivity bounds for first-order with counting can be seen as an attempt to show TC° ⊂≠ DLOG using techniques of descriptive complexity. Second, the presence of auxiliary built-in relations (e.g., order, successor) is known to make a big impact on expressivity results in finite-model theory and database theory. Our goal is to extend techniques from “pure” setting to that of auxiliary relations.

Until now, all known results on the limitations of expressive power of the counting and unary-quantifier extensions of first-order logic dealt with auxiliary relations of “small” degree. For example, it is known that these logics fail to express some DLOG-queries in the presence of a successor relation. Our main result is that these extensions cannot define the deterministic transitive closure (a DLOG-complete problem) in the presence of auxiliary relations of “large” degree, in particular, those which are “almost linear orders.” They are obtained from linear orders by replacing them by “very thin” preorders on arbitrarily small number of elements. We show that the technique of the proof (in a precise sense) cannot be extended to provide the proof of separation of TC° from DLOG. We also discuss a general impact of having built-in (pre)orders, and give some expressivity statements in the pure setting that would imply separation results for the ordered case.

Part of this work was done when the first author was visiting Institute of Systems Science.