Two new characterizations of -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 -definable set that is not -definable is undecidable.
D.A.M.Barrington, K.Compton, H.Straubing and D.Thérien, Regular languages in , Journal of Computer and System Sciences44(3) (1992), 478–499. doi:10.1016/0022-0000(92)90014-A.
2.
V.Bruyère, G.Hansel, C.Michaux and R.Villemaire, Logic and p-recognizable sets of integers, Bull. Belg. Math. Soc1 (1994), 191–238.
3.
J.R.Büchi, Weak second-order arithmetic and finite automata, Zeitschrift für Mathematische Logik und Grudlagen der Mathematik6 (1960), 66–92. doi:10.1002/malq.19600060105.
4.
C.Choffrut, Deciding whether a relation defined in Presburger logic can be defined in weaker logics, RAIRO ITA42(1) (2008), 121–135.
5.
C.Choffrut, A.Malcher, C.Mereghetti and B.Palano, On the expressive power of FO[+], in: LATA, A.H.Dediu, H.Fernau and C.Martín-Vide, eds, Lecture Notes in Computer Science, Vol. 6031, Springer, 2010, pp. 190–201.
6.
D.C.Cooper, Theorem proving in arithmetic without multiplication, Machine Intelligence7 (1972), 91–99.
7.
C.C.Elgot, Decision problems of finite automata design and related arithmetics, Trans. Amer. Math. Soc.98 (1961), 21–52. doi:10.1090/S0002-9947-1961-0139530-9.
8.
C.C.Elgot and M.O.Rabin, Decidability and undecidability of extensions of second (first) order theory of (generalized) successor, J. Symb. Log.31(2) (1966), 169–181. doi:10.2307/2269808.
9.
A.Finkel and J.Leroux, Presburger functions are piecewise linear, Research Report LSV-08-08, Laboratoire Spécification et Vérification, ENS Cachan, France, 2008, 9 pp.
10.
S.Ginsburg and E.H.Spanier, Presburger formulas, and languages, Semigroups, Pacific Journal of Mathematics16 (1966), 285–296. doi:10.2140/pjm.1966.16.285.
K.-J.Lange, Some results on majority quantifiers over words, in: IEEE Conference on Computational Complexity, IEEE Computer Society, 2004, pp. 123–129.
13.
R.McNaughton and S.Papert, Counter-Free Automata, M.I.T. Press, Cambridge, Mass, 1971.
14.
C.Michaux and R.Villemaire, Presburger arithmetic and recognizability of sets of natural numbers by automata: New proofs of Cobham’s and Semenov’s theorems, Ann. Pure Appl. Logic77(3) (1996), 251–277. doi:10.1016/0168-0072(95)00022-4.
15.
M.L.Minsky, Recursive unsolvability of post’s problem of “tag”: And other topics in theory of turing machines, Group report, Massachusetts Institute of Technology, Lincoln Laboratory, 1960.
16.
A.A.Muchnik, The definable criterion for definability in Presburger arithmetic and its applications, Theor. Comput. Sci.290(3) (2003), 1433–1444. doi:10.1016/S0304-3975(02)00047-6.
17.
P.Péladeau, Formulas, regular languages and Boolean circuits, Theor. Comput. Sci.101(1) (1992), 133–141. doi:10.1016/0304-3975(92)90152-6.
18.
M.Presburger, Über die vollständigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchen, die addition als einzige operation hervortritt, in: Comptes Rendus du Premier Congrès des Mathématicienes des Pays Slaves, Warsaw, 1927, pp. 92–101, 395.
19.
H.Straubing, Finite Automata, Formal Logic, and Circuit Complexity, Birkhäuser, 1994.
20.
B.A.Trakhtenbrot, Impossibility of an algorithm for the decision problem in finite classes, Doklady Akademii Nauk SSSR70 (1950), 569–572(in Russian).
21.
B.A.Trakhtenbrot, Finite automata and logic of monadic predicates, Dokl. Akad. Nauk SSSR140 (1961), 326–329(in Russian).
