December 7, 2020Julien Grange (INRIA Rennes)
Successor-invariant first-order logic is the extension of first-order logic where one has access to an additional successor relation on the elements of the structure, as long as the validity of formulas is independent on the choice of a particular successor.
It has been shown by Rossman that this formalism allows to express properties that are not FO-definable.
However, his separating example involves dense classes of structures, and the expressive power of successor-invariant first-order logic is an open question for sparse classes of structures.
We prove that when the degree is bounded, successor-invariant first-order logic is no more expressive than first-order logic.