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 -tuply exponential size, whence the satisfiability problem for this fragment is in -NExpTime. Together with other, known, complexity results, this provides tight complexity bounds for ${\cal F}{{\cal L}^m}$ for all $m \le 4$. (shrink)

The guarded fragment with transitive guards, [GF+TG], is an extension of the guarded fragment of first-order logic, GF, in which certain predicates 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. Moreover, we show that the problem is in 2E. This result is optimal since the satisfiability problem for GF is 2E-complete 1719–1742). We also show that the (...) satisfiability problem for two-variable [GF+TG] is N-hard in contrast to GF with bounded number of variables for which the satisfiability problem is E-complete. (shrink)