The Adjacent Fragment and Quine’s Limits of Decision

We introduce the adjacent fragment 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)\)-\({\rm NExpTime}\). Using known results on the fluted fragment, it follows that the satisfiability problem for the whole adjacent fragment is \({\rm 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 \(2{\rm ExpTime}\)-complete. We show that the satisfiability problem for the intersection of the adjacent and guarded adjacent fragments remains \(2{\rm ExpTime}\)-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.

Bartosz Bednarczyk, Daumantas Kojelis, Ian Pratt-Hartmann
Download Paper