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

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

Get full access to this article

View all access options for this article.

References

D.A.M.

Barrington,

Compton,

Straubing and

Thérien, Regular languages in

N C^{1}

, Journal of Computer and System Sciences 44(3) (1992), 478–499. doi:10.1016/0022-0000(92)90014-A.

Bruyère,

Hansel,

Michaux and

Villemaire, Logic and p-recognizable sets of integers, Bull. Belg. Math. Soc 1 (1994), 191–238.

J.R.

Büchi, Weak second-order arithmetic and finite automata, Zeitschrift für Mathematische Logik und Grudlagen der Mathematik 6 (1960), 66–92. doi:10.1002/malq.19600060105.

Choffrut, Deciding whether a relation defined in Presburger logic can be defined in weaker logics, RAIRO ITA 42(1) (2008), 121–135.

Choffrut,

Malcher,

Mereghetti and

Palano, On the expressive power of FO[+], in: LATA,

A.H.

Dediu,

Fernau and

Martín-Vide, eds, Lecture Notes in Computer Science, Vol. 6031, Springer, 2010, pp. 190–201.

D.C.

Cooper, Theorem proving in arithmetic without multiplication, Machine Intelligence 7 (1972), 91–99.

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.

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.

Finkel and

Leroux, Presburger functions are piecewise linear, Research Report LSV-08-08, Laboratoire Spécification et Vérification, ENS Cachan, France, 2008, 9 pp.

10.

Ginsburg and

E.H.

Spanier, Presburger formulas, and languages, Semigroups, Pacific Journal of Mathematics 16 (1966), 285–296. doi:10.2140/pjm.1966.16.285.

11.

Immerman, Descriptive Complexity, Springer, 1999.

12.

K.-J.

Lange, Some results on majority quantifiers over words, in: IEEE Conference on Computational Complexity, IEEE Computer Society, 2004, pp. 123–129.

13.

McNaughton and

Papert, Counter-Free Automata, M.I.T. Press, Cambridge, Mass, 1971.

14.

Michaux and

Villemaire, Presburger arithmetic and recognizability of sets of natural numbers by automata: New proofs of Cobham’s and Semenov’s theorems, Ann. Pure Appl. Logic 77(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éladeau, Formulas, regular languages and Boolean circuits, Theor. Comput. Sci. 101(1) (1992), 133–141. doi:10.1016/0304-3975(92)90152-6.

18.

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.

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 SSSR 70 (1950), 569–572 (in Russian).

21.

B.A.

Trakhtenbrot, Finite automata and logic of monadic predicates, Dokl. Akad. Nauk SSSR 140 (1961), 326–329 (in Russian).