Small substructures and decidability issues for first-order logic with two variables. (English) Zbl 1284.03136

Kieroński, Emanuel; Otto, Martin

J. Symb. Log. 77, No. 3, 729-765 (2012).

The authors study a partial case of the decidability problem for FO\(^2\), the part of the first-order language over a finite relational signature consisting of formulas all of whose variables (not only the free ones) are contained in the two-element set \(\{x,y\}\). It is a known fact that the satisfiability problem for this language is decidable, and that its set of identically true sentences is decidable.
The authors give a characterization of the satisfiability problems for FO\(^2\) for classes of structures of the kind \({\mathcal {EQ}}[\tau_0;\tau_1]\), where \(\tau_0\) and \(\tau_1\) are disjoint relational signatures and \(\tau_1\) consists of at most three binary symbols; these classes consist of all structures of signatures \(\tau_0\cup\tau_1\) in which all the symbols of \(\tau_1\) are interpreted as equivalences. It follows from the obtained results that the study of the case \(|\tau_1|\leqslant 3\) is enough to have a complete picture about decidability and satisfiability for any finite number of symbols in \(\tau_1\).
Let \(\mathcal K\) be a class of structures. Denote the satisfiability problem for FO\(^2\) on \(\mathcal K\) by SAT(FO\(^2\),\({\mathcal K}\)) and the finite satisfiability problem for FO\(^2\) by FINSAT(FO\(^2\),\({\mathcal K}\)). We say that FO\(^2\) has a finite (exponential) model property over a class of structures \(\mathcal K\) if every of its satisfiable sentence has a finite model in \(\mathcal K\) (of exponentially bounded cardinaility in the length of this sentence).
The main results of the paper are the following.
Theorem.

(i)

FO\(^2\) has an exponential model property over \({\mathcal {EQ}}[\tau_0;E]\). Hence SAT(FO\(^2\),\({\mathcal {EQ}}[\tau_0;E]\)) and FINSAT(FO\(^2\),\({\mathcal {EQ}}[\tau_0;E]\)) are Nexptime-complete.

(ii)

FO\(^2\) does not possess the finite model property over \({\mathcal {EQ}}[\tau_0;E_1,E_2]\).
However, SAT(FO\(^2\),\({\mathcal {EQ}}[\tau_0;E_1,E_2]\)) is decidable in 3-Nexptime.

(iii)

SAT(FO\(^2\),\({\mathcal {EQ}}[\tau_0;E_1,E_2,E_3]\)) and FINSAT(FO\(^2\),\({\mathcal {EQ}}[\tau_0;E_1,E_2,E_3]\)) are undecidable; in fact FO\(^2\) over \({\mathcal {EQ}}[\tau_0;E_1,E_2,E_3]\) forms a conservative reduction class.

Reviewer: Andrei S. Morozov (Novosibirsk)

MSC:

03B25	Decidability of theories and sets of sentences
03C07	Basic properties of first-order languages and structures
68Q25	Analysis of algorithms and problem complexity

Keywords:

logic with two variables; small substructure property; finite substructure property; satisfiability problem; equivalence relation

References:

[1]	H. Andréka, I. Németi, and J. van Benthem Modal languages and bounded fragments of predicate logic , Journal of Philosophical Logic , vol. 27(1998), no. 3, pp. 217-274. · Zbl 0919.03013
[2]	F. Baader, D. Calvanese, D. McGuinness, D. Nardi, and P. Patel-Schneider (editors) The description logic handbook , Cambridge University Press, Cambridge,2003. · Zbl 1058.68107
[3]	R. Berger The undecidability of the domino problem , Memoirs of the American Mathematical Society , vol. 66(1966), p. 72. · Zbl 0199.30802
[4]	M. Bojańczyk, C. David, A. Muscholl, T. Schwentick, and L. Segoufin Two-variable logic on words with data , LICS , Proceedings of the 21st IEEE Symposium on Logic in Computer Science,2006, pp. 7-16.
[5]	E. Börger, E. Grädel, and Y. Gurevich The classical decision problem , Perspectives in Mathematical Logic, Springer,1997.
[6]	A. Borgida On the relative expressiveness of description logics and predicate logics , Artificial Intelligence , vol. 82(1996), pp. 353-367.
[7]	C. David, L. Libkin, and T. Tan On the satisfiability of two-variable logic over data words , LPAR , Logic for Programming, Artificial Intelligence, and Reasoning, Lecture Notes in Computer Science, vol. 6397,2010, pp. 248-262. · Zbl 1307.03020
[8]	F. Eisenbrand and G. Shmonin Carathéodory bounds for integer cones , Operations Research Letters , vol. 34(2006), no. 5, pp. 564-568. · Zbl 1152.90662
[9]	H. Ganzinger, C. Meyer, and M. Veanes The two-variable guarded fragment with transitive relations , LICS , Proceedings of the 14th Symposium on Logic in Computer Science, IEEE Computer Society, Los Alamitos, CA,1999, pp. 24-34.
[10]	W. Goldfarb The unsolvability of the Gödel class with identity , Journal of Symbolic Logic, vol. 49(1984), pp. 1237-1252. · Zbl 0576.03008
[11]	E. Grädel On the restraining power of guards , Journal of Symbolic Logic, vol. 64(1999), pp. 1719-1742. · Zbl 0958.03027
[12]	E. Grädel, P. Kolaitis, and M. Vardi On the decision problem for two-variable first-order logic , Bulletin of Symbolic Logic, vol. 3(1997), pp. 53-69. · Zbl 0873.03009
[13]	E. Grädel and M. Otto On logics with two variables , Theoretical Computer Science , vol. 224(1999), pp. 73-113. · Zbl 0948.03023
[14]	E. Grädel, M. Otto, and E. Rosen Two-variable logic with counting is decidable , LICS , Proceedings of the 12th IEEE Symposium on Logic in Computer Science,1997, pp. 306-317.
[15]	E. Grädel, M. Otto, and E. Rosen Undecidability results on two-variable logics , Archive for Mathematical Logic , vol. 38(1999), pp. 313-354. · Zbl 0927.03015
[16]	Y. Gurevich and I. Koryakov Remarks on Berger’s paper on the domino problem , Siberian Mathematical Journal , vol. 13(1972), pp. 319-321. · Zbl 0248.02053
[17]	N. Immerman and E. Lander Describing graphs: a first-order approach to graph canonization , Complexity theory retrospective (A. Selman, editor), Springer,1990, pp. 59-81.
[18]	Y. Kazakov Saturation-based decision procedures for extensions of the guarded fragment , Ph.D. thesis, Universität des Saarlandes, Saarbrücken, Germany,2006.
[19]	E. Kieroński Results on the guarded fragment with equivalence or transitive relations , CSL , Proceedings of Computer Science Logic, Lecture Notes in Computer Science, vol. 3634, Springer,2005, pp. 309-324. · Zbl 1136.03315
[20]	—- On the complexity of the two-variable guarded fragment with transitive guards , Information and Computation , vol. 204(2006), pp. 1663-1703. · Zbl 1115.03021
[21]	E. Kieroński, J. Michaliszyn, I. Pratt-Hartmann, and L. Tendera Two-variable first-order logic with equivalence closure , in preparation. · Zbl 1341.03014
[22]	E. Kieroński and M. Otto Small substructures and decidability issues for first-order logic with two variables , Proceedings of the 20th IEEE Symposium on Logic in Computer Science,LISC 2005, pp. 448-457. · Zbl 1284.03136
[23]	E. Kieroński and L. Tendera On finite satisfiability of the guarded fragment with equivalence or transitive guards , LPAR , Logic for Programming, Artificial Intelligence, and Reasoning, Lecture Notes in Computer Science, vol. 4790,2007, pp. 318-322. · Zbl 1137.03316
[24]	—- On finite satisfiability of two-variable first order logic with equivalence relations. , LICS , Proceedings of the 23rd IEEE Symposium on Logic in Computer Science,2009, pp. 123-132.
[25]	A. Manuel Two variables and two successors , Proceedings of the 35th International Symposium on Mathematical foundations of Computer Science , Lecture Notes in Computer Science, vol. 6281, Springer,MFCS 2010, pp. 513-524. · Zbl 1287.03027
[26]	M. Mortimer On languages with two variables , Zeitschrift für Mathematische Logik und Grundlagen der Mathematik , vol. 21(1975), pp. 135-140. · Zbl 0343.02009
[27]	M. Niewerth and T. Schwentick Two-variable logic and key constraints on data words , ICDT , Proceedings of the 14th International Conference on Database Theory,2011, pp. 138-149.
[28]	M. Otto Two variable first-order logic over ordered domains , Journal of Symbolic Logic, vol. 66(2001), pp. 685-702. · Zbl 0990.03005
[29]	L. Pacholski, W. Szwast, and L. Tendera Complexity of two-variable logic with counting , LICS , Proceedings of the 12th IEEE Symposium on Logic in Computer Science,1997, pp. 318-327.
[30]	T. Schwentick and T. Zeume Two-variable logic with two order relations , CSL , Proceedings of Computer Science Logic, Lecture Notes in Computer Science, vol. 6247,2010, pp. 499-513. · Zbl 1238.03030
[31]	D. Scott A decision method for validity of sentences in two variables , Journal of Symbolic Logic, vol. 27(1962), p. 377.
[32]	W. Szwast and L. Tendera On the decision problem for the guarded fragment with transitivity , LICS , Proceedings of the 16th IEEE Symposium on Logic in Computer Science,2001, pp. 147-156.