# Quine's Fluted Fragment Revisited

## TL;DR

This paper investigates the computational complexity of the fluted fragment of first-order logic, revealing it is non-elementary and providing tight bounds for various sub-fragments, correcting earlier misconceptions about its complexity.

## Contribution

It establishes the non-elementary complexity of the fluted fragment and provides precise complexity bounds for its sub-fragments, correcting previous assumptions.

## Key findings

- Satisfiability for the fluted fragment is non-elementary.
- Models for $l^m$ require $loor{m/2}$-tuply exponential size.
- Satisfiability for $l^m$ is in ($m-2$)-NExpTime for $m \\geq 3$.

## 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$.