Quine's Fluted Fragment is Non-Elementary

Authors Ian Pratt-Hartmann, Wieslaw Szwast, Lidia Tendera

Thumbnail PDF


  • Filesize: 0.55 MB
  • 21 pages

Document Identifiers

Author Details

Ian Pratt-Hartmann
Wieslaw Szwast
Lidia Tendera

Cite AsGet BibTex

Ian Pratt-Hartmann, Wieslaw Szwast, and Lidia Tendera. Quine's Fluted Fragment is Non-Elementary. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 39:1-39:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


We study the fluted fragment, a decidable fragment of first-order logic with an unbounded number of variables, originally identified 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, for all m greater than 1, the intersection of the fluted fragment and the m-variable fragment of first-order logic. We show that this sub-fragment forces (m/2)-tuply exponentially large models, and that its satisfiability problem is (m/2)-NExpTime-hard. We round off by using a corrected version of Purdy's construction to show that the m-variable fluted fragment has the m-tuply exponential model property, and that its satisfiability problem is in m-NExpTime.
  • Quine
  • fluted fragment
  • Purdy
  • non-elementary
  • satisfiability
  • decidability


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. H. Andréka, J. van Benthem, and I. Németi. Modal languages and bounded fragments of predicate logic. Journal of Philosophical Logic, 27(3):217-274, 1998. Google Scholar
  2. E. Börger, E. Grädel, and Y. Gurevich. The Classical Decision Problem. Springer, 1997. Google Scholar
  3. E. Grädel, P. Kolaitis, and M. Vardi. On the decision problem for two-variable first-order logic. Bulletin of Symbolic Logic, 3(1):53-69, 1997. Google Scholar
  4. U. Hustadt, R. Schmidt, and L. Georgieva. A survey of decidable first-order fragments and description logics. Journal of Relational Methods in Computer Science, 1(3):251-276, 2004. Google Scholar
  5. C. Lutz and U. Sattler. The complexity of reasoning with Boolean modal logics. In F. Wolter, H. Wansing, M. de Rijke, and M. Zakharyaschev, editors, Advances in Modal Logic, volume 3, pages 1-20, Menlo Park, 2001. CLSI Publications. Google Scholar
  6. A. Noah. Predicate-functors and the limits of decidability in logic. Notre Dame Journal of Formal Logic, 21(4):701-707, 1980. Google Scholar
  7. W. C. Purdy. Decidability of fluted logic with indentity. Notre Dame Journal of Formal Logic, 37(1):84-104, 1996. Google Scholar
  8. W. C. Purdy. Fluted formulas and the limits of decidability. Journal of Symbolic Logic, 61(2):608-620, 1996. Google Scholar
  9. W. C. Purdy. Quine’s limits of decision. Journal of Symbolic Logic, 64(4):1439-1466, 1999. Google Scholar
  10. W. C. Purdy. Complexity and nicety of fluted logic. Studia Logica, 71:177-198, 2002. Google Scholar
  11. W. V. Quine. On the limits of decision. In Proceedings of the 14th International Congress of Philosophy, volume III, pages 57-62. University of Vienna, 1969. Google Scholar
  12. W. V. Quine. Algebraic logic and predicate functors. In The Ways of Paradox, pages 283-307. Harvard University Press, revised and enlarged edition, 1976. Google Scholar
  13. W. V. Quine. The variable. In The Ways of Paradox, pages 272-282. Harvard University Press, revised and enlarged edition, 1976. Google Scholar
  14. V. Rantala. Constituents. In R. Bogdan, editor, Jaakko Hintikka, volume 8 of Profiles, pages 43-76. Springer Netherlands, 1987. Google Scholar
  15. R. Schmidt and U. Hustadt. A resolution decision procedure for fluted logic. In D. McAllester, editor, Proceedings, CADE, number 1831 in LNAI, pages 433-448. Springer-Verlag, 2000. Google Scholar