Small substructures and decidability issues for first-order logic with two variables (Q2915891)

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.NEWLINENEWLINEThe 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\).NEWLINENEWLINELet \(\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).NEWLINENEWLINEThe main results of the paper are the following.NEWLINENEWLINETheorem.{\parindent=0.8cm\begin{itemize}\item[(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 \textsc{Nexptime}-complete.\item[(ii)] FO\(^2\) does not possess the finite model property over \({\mathcal {EQ}}[\tau_0;E_1,E_2]\).NEWLINENEWLINE However, SAT(FO\(^2\),\,\({\mathcal {EQ}}[\tau_0;E_1,E_2]\)) is decidable in 3-\textsc{Nexptime}. \item[(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.NEWLINENEWLINE\end{itemize}}