On the Decision Problem for Two-Variable First-Order Logic
Grädel, Erich ; Kolaitis, Phokion G. ; Vardi, Moshe Y.
Bull. Symbolic Logic, Tome 3 (1997) no. 1, p. 53-69 / Harvested from Project Euclid
We identify the computational complexity of the satisfiability problem for $\text{FO}^{2}$, the fragment of first-order logic consisting of all relational first-order sentences with at most two distinct variables. Although this fragment was shown to be decidable a long time ago, the computational complexity of its decision problem has not been pinpointed so far. In 1975 Mortimer proved that $\text{FO}^{2}$ has the finite-model property, which means that if an $\text{FO}^{2}$-sentence is satisfiable, then it has a finite model. Moreover, Mortimer showed that every satisfiable $\text{FO}^{2}$-sentence has a model whose size is at most doubly exponential in the size of the sentence. In this paper, we improve Mortimer's bound by one exponential and show that every satisfiable $\text{FO}^{2}$-sentence has a model whose size is at most exponential in the size of the sentence. As a consequence, we establish that the satisfiability problem for $\text{FO}^{2}$ is NEXPTIME-complete.
Publié le : 1997-03-14
Classification: 
@article{1182353488,
     author = {Gr\"adel, Erich and Kolaitis, Phokion G. and Vardi, Moshe Y.},
     title = {On the Decision Problem for Two-Variable First-Order Logic},
     journal = {Bull. Symbolic Logic},
     volume = {3},
     number = {1},
     year = {1997},
     pages = { 53-69},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1182353488}
}
Grädel, Erich; Kolaitis, Phokion G.; Vardi, Moshe Y. On the Decision Problem for Two-Variable First-Order Logic. Bull. Symbolic Logic, Tome 3 (1997) no. 1, pp.  53-69. http://gdmltest.u-ga.fr/item/1182353488/