The Adjacent Fragment and Quine's Limits of Decision

TL;DR

This paper introduces the adjacent fragment of first-order logic, explores its computational complexity, and examines how adjacency restrictions influence decidability and complexity in related logical fragments.

Contribution

It defines the adjacent fragment, analyzes its properties, and studies the impact of adjacency on the complexity and decidability of various first-order logic fragments.

Findings

Adjacent fragment has the finite model property.

Satisfiability for k-variable sub-fragment is in (k-1)-NExpTime.

Whole adjacent fragment is Tower-complete.

Abstract

We introduce the adjacent fragment AF of first-order logic, obtained by restricting the sequences of variables occurring as arguments in atomic formulas. The adjacent fragment generalizes (after a routine renaming) the two-variable fragment of first-order logic as well as the so-called fluted fragment. We show that the adjacent fragment has the finite model property, and that the satisfiability problem for its k-variable sub-fragment is in (k-1)-NExpTime. Using known results on the fluted fragment, it follows that the satisfiability problem for the whole adjacent fragment is Tower-complete. We additionally consider the effect of the adjacency requirement on the well-known guarded fragment of first-order logic, whose satisfiability problem is TwoExpTime-complete. We show that the satisfiability problem for the intersection of the adjacent and guarded adjacent fragments remains TwoExpTime-hard. Finally, we show that any relaxation of the adjacency condition on the allowed order of variables in argument sequences yields a logic whose satisfiability and finite satisfiability problems are undecidable.