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

Order-invariant first-order logic allows formulas to use an auxiliary linear order, provided that their truth does not depend on the chosen order. In this talk, I will introduce cluster first-order logic (CFO), a fragment of first-order logic designed to study this phenomenon. We show that order-invariant CFO can express properties beyond first-order logic in general, but that on graph classes of bounded degree, every order-invariant CFO property is first-order definable. I will discuss the main idea behind the proof: constructing suitable linear orders that preserve an appropriate notion of logical similarity between graphs.

Joint work with Julien Grange.