The Adjacent Fragment and Quine's Limits of Decision
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912012632588288 |
|---|---|
| author | Bednarczyk, Bartosz Kojelis, Daumantas Pratt-Hartmann, Ian |
| author_facet | Bednarczyk, Bartosz Kojelis, Daumantas Pratt-Hartmann, Ian |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2409_01231 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | The Adjacent Fragment and Quine's Limits of Decision Bednarczyk, Bartosz Kojelis, Daumantas Pratt-Hartmann, Ian Logic in Computer Science 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. |
| title | The Adjacent Fragment and Quine's Limits of Decision |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2409.01231 |