0000000000434581
AUTHOR
Wieslaw Szwast
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 intersectionof the fluted fragment and the m-variable fragment of first-order logic. We show that this subfragment 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 f…
FO^2 with one transitive relation is decidable
We show that the satisfiability problem for the two-variable first-order logic, FO^2, over transitive structures when only one relation is required to be transitive, is decidable. The result is optimal, as FO^2 over structures with two transitive relations, or with one transitive and one equivalence relation, are known to be undecidable, so in fact, our result completes the classification of FO^2-logics over transitive structures with respect to decidability. We show that the satisfiability problem is in 2-NExpTime. Decidability of the finite satisfiability problem remains open.