Undecidability of satisfiability of expansions of FO[<] over words with a FO[+]-definable set

Article type: Research Article

Authors: Milchior, Arthur^{a; b; c}

Affiliations: [a] IRIF, Université Paris 7 – Denis Diderot, France | [b] CNRS UMR 8243, Université Paris Diderot – Paris 7, Case 7014, 75205 Paris Cedex 13, France | [c] Université Paris-Est, LACL (EA 4219), UPEC, F-94010 Créteil, France. Arthur.Milchior@liafa.univ-paris-diderot.fr. http://www.liafa.univ-paris-diderot.fr/web9/equiprech/fichepers_fr.php?id=353

Abstract: Two new characterizations of FO[<,mod]-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 FO[+]-definable set that is not FO[<,mod]-definable is undecidable.

Keywords: Finite model theory, first order logic, arithmetic, undecidability

DOI: 10.3233/COM-170069

Journal: Computability, vol. 6, no. 4, pp. 333-363, 2017