Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Adjacent Fragment and Quine's Limits of Decision

Bartosz Bednarczyk, Daumantas Kojelis, Ian Pratt-Hartmann

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.

The Adjacent Fragment and Quine's Limits of Decision

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.
Paper Structure (13 sections, 23 theorems, 39 equations, 1 figure, 3 tables)

This paper contains 13 sections, 23 theorems, 39 equations, 1 figure, 3 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Primitive generators of words
  4. Upper bounds for $\mathcal{AF}^{\ell}$ without equality
  5. Adding Equality
  6. The Guarded Subfragment
  7. Generating Words.
  8. ATMs.
  9. Encoding numbers.
  10. Encoding configurations.
  11. Encoding instances of transitions
  12. Encoding acceptance trees
  13. Extending the adjacent fragment

Key Result

Lemma 1

Let $\varphi$ be a sentence of $\mathcal{AF}^{\ell+1}$, where $\ell \geq 1$. We can compute, in polynomial time, an $\mathcal{AF}^{\ell+1}$-formula $\psi$ satisfiable over the same domains as $\varphi$, of the form where $I$ is a finite index set, and the formulas $\gamma_i$ and $\beta$ are quantifier-free; moreover, if $\varphi$ is equality-free, then so is $\psi$.

Figures (1)

  • Figure 1: Generation of abcbaaadefedadefbabf from cbadefba.

Theorems & Definitions (38)

  • Lemma 1
  • proof
  • Lemma 2: Thm. 1 of ph:primGen24
  • Lemma 3: Thm. 4 of ph:primGen24
  • Lemma 4
  • proof
  • Lemma 5
  • proof
  • Lemma 6
  • proof
  • ...and 28 more