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{F}\mathcal{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 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\ge 3$, any satisfiable ${\mathcal{F}\mathcal{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 ${\mathcal{F}\mathcal{L}}^m$ for all $m\le 4$.