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

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.

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
PDF
BibTeX
XML
Cite

\textit{E. Kieroński} and \textit{M. Otto}, J. Symb. Log. 77, No. 3, 729--765 (2012; Zbl 1284.03136)

### 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. |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.