Quine's Fluted Fragment is Non-Elementary
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
39:1-39:21
Regular Paper
Ian
Pratt-Hartmann
Ian Pratt-Hartmann
Wieslaw
Szwast
Wieslaw Szwast
Lidia
Tendera
Lidia Tendera
10.4230/LIPIcs.CSL.2016.39
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.
E. Börger, E. Grädel, and Y. Gurevich. The Classical Decision Problem. Springer, 1997.
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.
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.
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.
A. Noah. Predicate-functors and the limits of decidability in logic. Notre Dame Journal of Formal Logic, 21(4):701-707, 1980.
W. C. Purdy. Decidability of fluted logic with indentity. Notre Dame Journal of Formal Logic, 37(1):84-104, 1996.
W. C. Purdy. Fluted formulas and the limits of decidability. Journal of Symbolic Logic, 61(2):608-620, 1996.
W. C. Purdy. Quine’s limits of decision. Journal of Symbolic Logic, 64(4):1439-1466, 1999.
W. C. Purdy. Complexity and nicety of fluted logic. Studia Logica, 71:177-198, 2002.
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.
W. V. Quine. Algebraic logic and predicate functors. In The Ways of Paradox, pages 283-307. Harvard University Press, revised and enlarged edition, 1976.
W. V. Quine. The variable. In The Ways of Paradox, pages 272-282. Harvard University Press, revised and enlarged edition, 1976.
V. Rantala. Constituents. In R. Bogdan, editor, Jaakko Hintikka, volume 8 of Profiles, pages 43-76. Springer Netherlands, 1987.
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.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode