Order-invariant cluster first-order logic on graph classes of bounded degree
This work addresses the open problem of understanding order-invariant first-order logic, providing a stepping stone toward resolving its expressive power on bounded-degree graphs.
The paper introduces cluster first-order logic to study order invariance, showing that while it can define properties beyond plain first-order logic in general, its expressive power is contained within first-order logic on graph classes of bounded degree. The result is established by constructing linear orders that preserve similarity between structures.
We introduce a new logic, called \emph{cluster first-order logic}, a restricted fragment of first-order logic specifically designed to study order invariance. An order-invariant formula is one on a vocabulary that contains an order; however, whether a structure satisfies it or not is independent of the interpretation of the order. We show that while order-invariant cluster first-order logic can define properties outside the scope of plain first-order logic in general, its expressive power is included in that of first-order logic when it comes to classes of bounded degree. We establish this result by explicitly constructing linear orders such that similar structures remain similar when they are expanded with these orders. This similarity-preserving, local-to-global approach is technically involved and somewhat counterintuitive, since adding an order usually reveals distinctions that are otherwise hidden due to the locality of first-order logic. We believe that this work can be a stepping stone toward applying such techniques to plain first-order logic and toward settling the question of the expressive power of order-invariant plain first-order logic.