Uniform One-Dimensional Fragments with One Equivalence Relation.

The uniform one-dimensional fragment U1 of first-order logic was introduced recently as a natural generalization of the two-variable fragment FO2 to contexts with relation symbols of all arities. It was shown that U1 has the exponential model property and NEXPTIME-complete satisfiability problem. In this paper we investigate two restrictions of U1 that still contain FO2. We call these logics RU1 and SU1, or the restricted and strongly restricted uniform one-dimensional fragments. We introduce Ehrenfeucht-Fraisse games for the logics and prove that while SU1 and RU1 are expressively equivalent, they are strictly contained in U1. Furthermore, we consider extensions of the logics SU1, RU1 and U1 with unrestricted use of a single built-in equivalence relation E. We prove that while all the obtained systems retain the finite model property, their complexities differ. Namely, the satisfiability problem is NEXPTIME-complete for SU1(E) and 2NEXPTIME-complete for both RU1(E) and U1(E). Finally, we show undecidability of some natural extensions of SU1.