Quine's Fluted Fragment Revisited

2018/12/16 by Pratt-Hartmann, I., Szwast, W., Tendera, L.
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.1812.06440

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 FL^m, the intersection of the fluted fragment and the m-variable fragment of first-order logic, for all m ≥ 1. We show that, for m ≥ 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 ≥ 3, any satisfiable 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 FL^m for all m ≤ 4.

Related

• The Adjacent Fragment and Quine's Limits of Decision
• Ordered fragments of first-order logic
• On Homogeneous Model of Fluted Languages
• The Fluted Fragment with Transitivity
• On the Limits of Decision: the Adjacent Fragment of First-Order Logic