Addition-Invariant FO and Regularity

We consider formulas which, in addition to the symbols in the vocabulary, may use two designated symbols -<; and + that must be interpreted as a linear order and its associated addition. Such a formula is called addition-invariant if, for each fixed interpretation of the initial vocabulary, its result is independent of the particular interpretation of -<; and +. This paper studies the expressive power of addition invariant first-order logic, +-inv-FO, on the class of finite strings. Our first main result gives a characterization of the regular languages definable in +-inv-FO: we show that these are exactly the languages definable in FO with extra predicates, denoted by “lm” for short, for testing the length of the string modulo some fixed number. Our second main result shows that every language definable in +-inv-FO, that is bounded or commutative or deterministic context-free, is regular. As an immediate consequence of these two main results, we obtain that +-inv-FO is equivalent to FO(lm) on the class of finite colored sets. Our proof methods involve Ehrenfeucht-Fraïssé games, tools from algebraic automata theory, and reasoning about semi-linear sets.