Undecidability of satisfiability of expansions of FO[<] over words with a FO[+]-definable set
Arthur Milchior · Computability · 2017
Two new characterizations of [Formula: see text]-definable sets, i.e. sets of integers definable in first-order logic with the order relation and modular relations, are provided. Those characterizations are used to prove that satisfiability of first-order logic over words with an order relation and a [Formula: see text]-definable set that is not [Formula: see text]-definable is undecidable.