Quine's Fluted Fragment Revisited

Abstract

We study the fluted fragment, a decidable fragment of first-order logic with an unbounded number of variables, originally identified in 1968 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 $\mathcal{FL}^m$, the intersection of the fluted fragment and the $m$-variable fragment of first-order logic, for all $m \geq 1$. We show that, for $m \geq 2$, this sub-fragment forces $\lfloor m/2\rfloor$-tuply exponentially large models, and that its satisfiability problem is $\lfloor m/2\rfloor$-NExpTime-hard. We further establish that, for $m \geq 3$, any satisfiable $\mathcal{FL}^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 $\mathcal{FL}^m$ for all $m \leq 4$.