The Adjacent Fragment and Quine’s Limits of Decision

Bartosz BednarczykBartosz Bednarczyk, Daumantas KojelisDaumantas Kojelis, Ian Pratt-HartmannIan Pratt-Hartmann

Download

Bartosz Bednarczyk, Daumantas Kojelis, Ian Pratt-Hartmann
The Adjacent Fragment and Quine’s Limits of Decision
Journal of Logic and Computation, to appear

Details
Bibtex

KurzfassungAbstract
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 2ExpTime-complete. We show that the satisfiability problem for the intersection of the adjacent and guarded adjacent fragments remains 2ExpTime-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.
Projekt:Project: DeciGUT
Forschungsgruppe:Research Group: Computational LogicComputational Logic

@article{BKP2025,
  author  = {Bartosz Bednarczyk and Daumantas Kojelis and Ian Pratt-Hartmann},
  title   = {The Adjacent Fragment and Quine’s Limits of Decision},
  journal = {Journal of Logic and Computation},
  year    = {2025}
}