We identify the computational complexity of the satisfiability problem for FO2., 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 ofits decision problem has not been pinpointed so far. In 1975 M ortiiner proved that FO2 has thefinite-modelproperty, which means that if an FO2-sentence is satisfiable, then it has a finite model. Moreover, Mortimer showed that every satisfiable FO2 -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 FO -sentence has a model whose size is at most exponential in the size of the sentence. As a co resequence, we establish that the satisfiability problem for FO2 is NEXPTIME-complete.
展开▼
