Order-invariant cluster first-order logic on graph classes of bounded degree

TL;DR

This paper introduces cluster first-order logic to analyze order invariance and shows its expressive power aligns with first-order logic on bounded degree graph classes, using a novel similarity-preserving approach.

Contribution

It defines a new logic for order invariance and proves its equivalence to first-order logic on bounded degree graphs through a local-to-global similarity construction.

Findings

Order-invariant cluster first-order logic can define properties outside plain first-order logic.

On bounded degree graphs, its expressive power is contained within first-order logic.

A similarity-preserving, local-to-global approach is used to establish this result.

Abstract

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.