Abstract We study the fluted fragment, a decidable fragment of first-order logic with an unbounded number of variables, motivated by the work of W. V. Quine. We show that the satisfiability problem for this fragment has nonelementary complexity, thus refuting an earlier published claim by W. C. Purdy that it is in NExpTime. More precisely, we consider ${\cal F}{{\cal L}^m}$ , the intersection of the fluted fragment and the m-variable fragment of first-order logic, for all $m \ge 1$ . We show that, for $m \ge 2$ , this subfragment forces $\left\lfloor {m/2} \right\rfloor$ -tuply exponentially large models, and that its satisfiability problem is $\left\lfloor {m/2} \right\rfloor$ -NExpTime-hard. We further establish that, for $m \ge 3$ , any satisfiable ${\cal F}{{\cal L}^m}$ -formula has a model of at most ( $m - 2$ )-tuply exponential size, whence the satisfiability (= finite satisfiability) problem for this fragment is in ( $m - 2$ )-NExpTime. Together with other, known, complexity results, this provides tight complexity bounds for ${\cal F}{{\cal L}^m}$ for all $m \le 4$ .

Abstract We study the satisfiability problem for two-variable first-order logic over structures with one transitive relation. We show that the problem is decidable in 2-NExpTime for the fragment consisting of formulas where existential quantifiers are guarded by transitive atoms. As this fragment enjoys neither the finite model property nor the tree model property, to show decidability we introduce a novel model construction technique based on the infinite Ramsey theorem. We also point out why the technique is not sufficient to obtain decidability for the full two-variable logic with one transitive relation; hence, contrary to our previous claim, [FO$^2$ with one transitive relation is decidable, STACS 2013: 317-328], the status of the latter problem remains open.

We study the fluted fragment, a decidable fragment of first-order logic with an unbounded number of variables, originally identified by W.V. Quine. We show that the satisfiability problem for this fragment has non-elementary complexity, thus refuting an earlier published claim by W.C. Purdy that it is in NExpTime. More precisely, we consider, for all m greater than 1, the intersection of the fluted fragment and the m-variable fragment of first-order logic. We show that this sub-fragment forces (m/2)-tuply exponentially large models, and that its satisfiability problem is (m/2)-NExpTime-hard. We round off by using a corrected version of Purdy's construction to show that the m-variable fluted fragment has the m-tuply exponential model property, and that its satisfiability problem is in m-NExpTime.

We show that the satisfiability problem for the two-variable first-order logic, FO^2, over transitive structures when only one relation is required to be transitive, is decidable. The result is optimal, as FO^2 over structures with two transitive relations, or with one transitive and one equivalence relation, are known to be undecidable, so in fact, our result completes the classification of FO^2-logics over transitive structures with respect to decidability. We show that the satisfiability problem is in 2-NExpTime. Decidability of the finite satisfiability problem remains open.

The guarded fragment with transitive guards, [GF+TG], is an extension of GF in which certain relations are required to be transitive, transitive predicate letters appear only in guards of the quantifiers and the equality symbol may appear everywhere. We prove that the decision problem for [GF+TG] is decidable. This answers the question posed in (Ganzinger et al., 1999). Moreover, we show that the problem is 2EXPTIME-complete. This result is optimal since the satisfiability problem for GF is 2EXPTIME-complete (Gradel, 1999). We also show that the satisfiability problem for two-variable [GF+TG] is NEXPTIME-hard in contrast to GF with bounded number of variables for which the satisfiability problem is EXPTIME-complete.

Let $C^2_p$ denote the class of first-order sentences with two variables and with additional quantifiers "there exists exactly (at most, at least) i" for $i\leq p$, and let $C^2$ be the union of $C^2_p$ taken over all integers p. We prove that the satisfiability problem for $C^2_1$ sentences is NEXPTIME-complete. This strengthens the results by [E. Grädel, Ph. Kolaitis, and M. Vardi, Bull. Symbolic Logic, 3 (1997), pp. 53--69], who showed that the satisfiability problem for the first-order two-variable logic $L^2$ is NEXPTIME-complete and by [E. Grädel, M. Otto, and E. Rosen, 12th Annual IEEE Symposium on Logic in Computer Science, 1997, pp. 306--317], who proved the decidability of $C^2$. Our result easily implies that the satisfiability problem for $C^2$ is in nondeterministic, doubly exponential time. It is interesting that $C^2_1$ is in NEXPTIME in spite of the fact that there are sentences whose minimal (and only) models are of doubly exponential size. It is worth noticing that by a recent result of [E. Grädel, M. Otto, and E. Rosen, Proceedings of 14th Annual Symposium on Theoretical Aspects of Computer Science, Lecture Notes in Comput. Sci. 1200, Springer-Verlag, Berlin, 1997], extensions of two-variable logic $L^2$ by a weak access to cardinalities through the Härtig (or equicardinality) quantifier is undecidable. The same is true for extensions of $L^2$ by very weak forms of recursion. The satisfiability problem for logics with a bounded number of variables has applications in artificial intelligence, notably in modal logics (see, e.g., [W. van der Hoek and M. De Rijke, J. Logic Comput., 5 (1995), pp. 325--345]), where counting comes in the context of graded modalities and in description logics, where counting can be used to express so-called number restrictions (see, e.g., [A. Borgida, Artificial Intelligence, 82 (1996), pp. 353--367]).

Let C/sub k//sup 2/ denote the class of first order sentences with two variables and with additional quantifiers "there exists exactly (at most, at least) m", for m/spl les/k, and let C/sup 2/ be the union of C/sub k//sup 2/ taken over all integers k. We prove that the problem of satisfiability of sentences of C/sub 1//sup 2/ is NEXPTIME-complete. This strengthens a recent result of E. Gradel, Ph. Kolaitis and M. Vardi (1997) who proved that the satisfiability problem for the first order two-variable logic L/sup 2/ is NEXPTIME-complete and a very recent result by E. Gradel, M. Otto and E. Rosen (1997) who proved the decidability of C/sup 2/. Our result easily implies that the satisfiability problem for C/sup 2/ is in non-deterministic, doubly exponential time. It is interesting that C/sub 1//sup 2/ is in NEXPTIME in spite of the fact, that there are sentences whose minimal (and only) models are of doubly exponential size.

It is proved that the 0-1 law does not hold for the class of existential second sentences whose first order part is in the minimal Godel class, i.e. has the quantifier prenex consisting of two universal quantifiers followed by just one existential quantifier. This completes the classification of existential second order sentences for which the 0-1 law holds. It is also proved that asymptotic probabilities of sentences as above form a dense subset of the unit interval.>

In [9] and [10] P. Kolaitis and M. Vardi proved that the 0-1 law holds for the second-order existential sentences whose first-order parts are formulas of Bernays-Schonfinkel or Ackermann prefix classes. They also provided several examples of second-order formulas for which the 0-1 law does not hold, and noticed that the classification of second-order sentences for which the 0-1 law holds resembles the classification of decidable cases of first-order prenex sentences. The only cases they have not settled are the cases of Gödel classes with and without equality. In this paper we confirm the conjecture of Kolaitis and Vardi that the 0-1 law does not hold for the existential second-order sentences whose first-order part is in Gödel prenex form with equality. The proof we give is based on a modification of the example employed by W. Goldfarb [5] in his proof that, contrary to the Gödel claim [6], the class of Gödel prenex formulas with equality is undecidable.

P. Kolaitis and M. Vardi (see Proc. 19th ACM Symp. on Theory of Computing, p.425-35 (1987), and Proc. 3rd Ann. Symp. on Logic in Computer Science, p.2-11 (1988)) proved that the 0-1 law holds for the second-order existential sentences whose first-order parts are formulas of Bernays-Schonfinkel or Ackermann prefix classes. They also provided several examples of second-order formulas for which the 0-1 law does not hold and noticed that the classification of second-order sentences for which the 0-1 law holds resembles the classification of decidable cases of prenex first-order sentences. The only cases they have not settled were the cases of Godel classes with and without equality. The authors confirm the conjecture of Kolaitis and Vardi that the 0-1 law does not hold for the existential second-order sentences whose first-order part is in the godel prenex form with equality.>