=Paper=
{{Paper
|id=Vol-3739/abstract-7
|storemode=property
|title=On the of Limits of Decision:
the Adjacent Fragment of First-Order Logic (Extended Abstract)
|pdfUrl=https://ceur-ws.org/Vol-3739/abstract-7.pdf
|volume=Vol-3739
|authors=Bartosz Bednarczyk,Daumantas Kojelis,Ian Pratt-Hartmann
|dblpUrl=https://dblp.org/rec/conf/dlog/BednarczykKP24
}}
==On the of Limits of Decision:
the Adjacent Fragment of First-Order Logic (Extended Abstract)==
https://ceur-ws.org/Vol-3739/abstract-7.pdf
On the of Limits of Decision:
the Adjacent Fragment of First-Order Logic
(Extended Abstract)
Bartosz Bednarczyk1,2 , Daumantas Kojelis3 and Ian Pratt-Hartmann3,4
1
Computational Logic Group, Technische UniversitΓ€t Dresden, Germany
2
Institute of Computer Science, University of WrocΕaw, Poland
3
Department of Computer Science, University of Manchester, UK
4
Institute of Computer Science, University of Opole, Poland
Abstract
We define the adjacent fragment πβ± of first-order logic, obtained by restricting the sequences of variables occur-
ring as arguments in atomic formulas. The adjacent fragment generalizes (after a routine renaming) two-variable
logic as well as the fluted fragment. We show that the adjacent fragment has the finite model property, and that
its satisfiability problem is no harder than for the fluted fragment (and hence is Tower-complete). We further
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. Finally, we study the effect
of the adjacency requirement on the well-known guarded fragment (π’β±) of first-order logic. We show that the
satisfiability problem for the guarded adjacent fragment (π’π) remains 2ExpTime-hard, thus strengthening the
known lower bound for π’β±.
Keywords
decidability, satisfiability, variable-ordered logics, complexity
The quest to find fragments of first-order logic for which satisfiability is algorithmically decidable
has been a central undertaking of mathematical logic since the appearance of Hilbert and Ackermannβs
GrundzΓΌge der theoretischen Logik [1, 2] almost a century ago. The great majority of such fragments so
far discovered, however, belong to just three families: (i) quantifier prefix fragments [3], where we are
restricted to prenex formulas with a specified quantifier sequence; (ii) two-variable logics [4], where the
only logical variables occurring as arguments of predicates are π₯1 and π₯2 ; and (iii) guarded logics [5],
where quantifiers are relativized by atomic formulas featuring all the free variables in their scope.
There is, however, a fourth family of decidable logics, originating in the work of
W.V.O. Quine [6], and based on restricting the allowed sequences of variables occurring as arguments
in atomic formulas. This family of logics, which includes the fluted fragment, the ordered fragment and
the forward fragment, has languished in relative obscurity. In our paper, we investigate the potential
for obtaining decidable fragments in this way, identifying a new fragment, which we call the adjacent
fragment. This fragment not only includes the fluted, ordered and forward fragments, but also subsumes,
in a sense we make precise, the two-variable fragment. We show that the satisfiability problem for the
adjacent fragment is decidable, and determine bounds on its complexity.
To explain how restrictions on argument orderings work, we consider presentations of first-order logic
without equality over purely relational signatures, employing individual variables from the alphabet
{π₯1 , π₯2 , π₯3 , . . .}. Any atomic formula in this logic has the form π(π₯ Β― ), where π is a predicate of arity
π β₯ 0 and π₯ Β― is a word over the alphabet of variables of length π. Call a first-order formula π index-
normal if, for any quantified sub-formula ππ₯π π of π, π is a Boolean combination of formulas that
are either atomic with free variables among π₯1 , . . . , π₯π , or have as their major connective a quantifier
DL 2024: 37th International Workshop on Description Logics, June 18β21, 2024, Bergen, Norway
bartosz.bednarczyk@cs.uni.wroc.pl (B. Bednarczyk); daumantas.kojelis@manchester.ac.uk (D. Kojelis);
ian.pratt@manchester.ac.uk (I. Pratt-Hartmann)
{ https://bartoszjanbednarczyk.github.io/ (B. Bednarczyk); https://daumantaskojelis.github.io/ (D. Kojelis);
https://www.cs.man.ac.uk/~ipratt/ (I. Pratt-Hartmann)
0000-0002-8267-7554 (B. Bednarczyk); 0000-0002-1632-9498 (D. Kojelis); 0000-0003-0062-043X (I. Pratt-Hartmann)
Β© 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
ceur-ws.org
Workshop ISSN 1613-0073
Proceedings
binding π₯π+1 . By re-indexing variables, any first-order formula can easily be written as a logically
equivalent index-normal formula. In the fluted fragment, denoted β±β, as defined by W. Purdy [7],
we confine attention to index-normal formulas, but additionally insist that any atom occurring in a
context in which π₯π is quantified have the form π(π₯πβπ+1 Β· Β· Β· π₯π ), i.e. π(π₯ Β― ) with π₯
Β― a suffix of π₯1 Β· Β· Β· π₯π .
In the ordered fragment, due to A. Herzig [8], by contrast, we insist that π₯ Β― be a prefix of π₯1 Β· Β· Β· π₯π . In the
forward fragment [9], we insist only that π₯ Β― be an infix of π₯1 Β· Β· Β· π₯π .
All these logics have the finite model property, and hence are decidable for satisfiability. Denoting by
β±βπ the sub-fragment of β±β involving at most π variables (free or bound), the satisfiability problem for
β±βπ is known to be in (πβ2)-NExpTime for all π β₯ 3, and βπ/2β-NExpTime-hard for all π β₯ 2 [10].
Thus, satisfiability for the whole fluted fragment is Tower-complete, in the system of trans-elementary
complexity classes due to [11]. By contrast, the satisfiability problem for ordered fragment is known
to be PSpace-complete [8, 12]. On the other hand, the apparent liberalization afforded by the forward
fragment yields no difference in expressive power [13].
Say that a word π₯ Β― over the alphabet {π₯1 , . . . , π₯π } (π β₯ 0) is adjacent if the indices of neighbouring
letters differ by at most 1. For example, π₯3 π₯2 π₯1 π₯2 π₯2 π₯2 π₯3 π₯4 π₯3 is adjacent, but π₯1 π₯3 π₯2 is not. The
adjacent fragment, denoted πβ±, is analogous to the fluted, ordered and forward fragments, but we
allow any atom π(π₯ Β― ) to occur in a context where π₯π is available for quantification as long as π₯ Β― is an
adjacent word over {π₯1 , . . . , π₯π }. As a simple example, the formula
(οΈ )οΈ
βπ₯1 βπ₯2 βπ₯3 βπ₯4 βπ₯5 π(π₯1 π₯2 π₯3 π₯2 π₯3 π₯4 π₯5 ) β π(π₯1 π₯2 π₯3 π₯4 π₯3 π₯4 π₯5 )
is a validity of πβ±, as can be seen by assigning π₯4 the same value as π₯2 . Evidently, πβ± includes the
fluted, ordered and forward fragments; the inclusion is strict, since the formulas
βπ₯1 π(π₯1 π₯1 ),
(οΈ )οΈ
βπ₯1 π₯2 π(π₯1 π₯2 ) β π(π₯2 π₯1 ) ,
stating that π is reflexive and symmetric, respectively, are in πβ±. It is worth noting that the formula
expressing transitivity; i.e.
(οΈ(οΈ )οΈ )οΈ
βπ₯1 π₯2 π₯3 π(π₯1 π₯2 ) β§ π(π₯2 π₯3 ) β π(π₯1 π₯3 ) ,
is not in πβ± as the variable π₯2 is skipped in the atom π(π₯1 π₯3 ).
To further aid intuition, we provide the following (possible) translations of english sentences into
πβ±. βEvery student taking a programming course also takes some maths courseβ can be written as:
(οΈ )οΈ)οΈ
βπ₯1 π₯2 Prog(π₯1 ) β§ Stud(π₯2 ) β§ Takes(π₯2 , π₯1 ) β βπ₯3 Math(π₯3 ) β§ Takes(π₯2 , π₯3 )
(οΈ
βEvery languages student either recommends Norwegian to their peers or is recommended Norwegian
by someoneβ may be written as:
(οΈ )οΈ)οΈ
βπ₯1 π₯2 Stud(π₯1 ) β§ Nor(π₯2 ) β βπ₯3 Rec(π₯1 , π₯2 , π₯3 ) β¨ βπ₯3 Rec(π₯3 , π₯2 , π₯1 ) .
(οΈ )οΈ (οΈ
In the sequel we will define the fragment formally.
Let π and π be non-negative integers. For any integers π and π, we write [π, π] to denote the set of
integers β such that π β€ β β€ π. A function π : [1, π] β [1, π] is adjacent if |π (π + 1)βπ (π)| β€ 1 for all
π (1 β€ π < π). We write Aπ π to denote the set of adjacent functions π : [1, π] β [1, π]. Since [1, 0] = β
,
we have A0π = {β
}, and Aπ 0 = β
if π > 0. Let π΄ be a non-empty set. A word π Β― over the alphabet π΄
is simply a tuple of elements from π΄. Accordingly, π΄ denotes the set of words over π΄ having length
π
exactly π, and π΄* is the set of all finite words over π΄. Any function π : [1, π] β [1, π] (adjacent or
not) induces a natural map from π΄π to π΄π defined by π Β―π = ππ (1) Β· Β· Β· ππ (π) , where π
Β― = π1 Β· Β· Β· ππ . If
π β Aπ (i.e. if π is adjacent), we may think of π
π Β― as the result of a βwalkβ on the tuple π
π Β―, starting at
the element ππ (1) , and moving left, right, or remaining stationary according to the sequence of values
π
Β―
b a
f
c b a d e
Β―π
π
a b c b a a a d e f e d a d e f b a b f
Figure 1: Generation of abcbaaadefedadefbabf from cbadefba.
π (π + 1)βπ (π) (1 β€ π < π). We may picture a walk as a piecewise linear function, with the generated
word superimposed on the abscissa and the generating word on the ordinate, c.f. Figure 1.
For any π β₯ 0, denote by xπ the fixed word π₯1 Β· Β· Β· π₯π (if π = 0, this is the empty word). A π-atom is
an expression π(xππ ), where π is a predicate of some arity π β₯ 0, and π : [1, π] β [1, π]. Thus, in a
π-atom, each argument is a variable chosen from xπ . If π is adjacent, we speak of an adjacent π-atom.
Thus, in an adjacent π-atom, the indices of neighbouring arguments differ by at most one. When π β€ 2,
the adjacency requirement is vacuous, and in this case we prefer to speak simply of π-atoms. Proposition
letters (predicates of arity π = 0) count as (adjacent) π-atoms for all π β₯ 0, taking π to be the empty
function. When π = 0, we perforce have π = 0, since otherwise, there are no functions from [1, π]
to [1, π]; thus the 0-atoms are precisely the proposition letters.
We define the sets of first-order formulas πβ± [π] by simultaneous structural induction:
1. every adjacent π-atom is in πβ± [π] ;
2. πβ± [π] is closed under Boolean combinations;
3. if π is in πβ± [π+1] , βπ₯π+1 π and βπ₯π+1 π are in πβ± [π] .
Formally, we call πβ± = πβ₯0 πβ± [π] the adjacent fragment. Note that formulas of πβ± contain no
βοΈ
individual constants, function symbols or equality.
As every word over {π₯1 , π₯2 } is adjacent, we may transform any formula of the two-variable fragment
without equality, FO2 , in polynomial time, to a logically equivalent formula of πβ±. The converse is true
over signatures with predicates of arity at most two. Since the system of basic multimodal propositional
logic is, under the standard translation to first-order logic, included within FO2 , this logic is similarly
subsumed by πβ±, as indeed is its notational variant, the description logic πβπ (see, e.g. [14]).
We show that the satisfiability problem for the restriction of the adjacent fragment to formulas
involving at most π variables (free or bound) is in (πβ2)-NExpTime for all π β₯ 3βand hence no more
difficult than the π-variable fluted fragment, which it properly contains. The critical step in our analysis
is [15, Theorem 3.1]βa theorem on the combinatorics of strings, which may be of independent interest.
We also consider minimal relaxations of adjacency involving the fragment with just three variables,
and show that, in all cases of interest, the satisfiability and finite satisfiability problems for the resulting
logics are undecidable. Thus, adjacency is as far as we can go in seeking decidable fragments based on
straightforward argument ordering restrictions of the type envisaged by Quine.
The adjacent fragment is incomparable in expressive power to the guarded fragment. Moreover, the
satisfiability problem for the union of π’β± and πβ± is undecidable, as one can use adjacent formulas to
introduce any π-ary universal relations, which makes π’β± as expressive as first-order logic. Therefore,
we study the effect of the adjacency restriction on π’β±. We investigate the complexity of satisfiability for
the guarded adjacent fragment π’π, showing that the problem is 2ExpTime-complete, thus sharpening
the existing 2ExpTime-hardness proof for π’β± [16].
Denoting πβ± β for the β-variable adjacent fragment we establish the following results using a variable
reduction technique similar to that as for the fluted fragment.
Theorem 1. The (finite) satisfiability problem for πβ± β is in (β β 2) β NExpTime and ββ/2β β NExpTime-
hard.
This allows us to conclude the following about the whole fragment.
Theorem 2. The (finite) satisfiability problem for πβ± is Tower-complete.
We also sharpen existing lower bounds for the (finite) satisfiability of the guarded fragment by encod-
ing an alternating turing machine running in exponential space in an adjacent way thus establishing
the following.
Theorem 3. The (finite) satisfiability problem for π’π is 2ExpTime-complete.
The full paper is published in the proceedings of the 50th International Colloquium on Automata,
Languages, and Programming (ICALP 2023) [15]. The accompanying technical report with detailed
proofs is available on arxiv [17].
Acknowledgments
Bartosz Bednarczyk is supported by the ERC Consolidator Grant No. 771779 (DeciGUT). Daumantas
Kojelis and Ian Pratt-Hartmann are supported by the NCN grant 2018/31/B/ST6/03662.
References
[1] D. Hilbert, W. Ackerman, GrundzΓΌge der theoretischen Logik, Springer, Berlin, 1928.
[2] D. Hilbert, W. Ackerman, Principles of Mathematical Logic, Chelsea, New York, 1950.
[3] E. BΓΆrger, E. GrΓ€del, Y. Gurevich, The Classical Decision Problem, Perspectives in Mathematical
Logic, Springer, 1997.
[4] L. Henkin, Logical Systems Containing Only a Finite Number of Symbols, SΓ©minaire de mathΓ©ma-
tiques supΓ©rieures, Presses de lβUniversitΓ© de MontrΓ©al, 1967. URL: https://books.google.pl/books?
id=0jPQAAAAMAAJ.
[5] H. AndrΓ©ka, I. NΓ©meti, J. van Benthem, Modal languages and bounded fragments of predicate
logic, Journal of Philosophical Logic 27 (1998) 217β274. doi:10.1023/a:1004275029985.
[6] W. V. O. Quine, On the limits of decision, in: Proceedings of the 14th International Congress of
Philosophy, volume III, University of Vienna, 1969, pp. 57β62.
[7] W. C. Purdy, Fluted formulas and the limits of decidability, The Journal of Symbolic Logic 61
(1996) 608β620. URL: http://www.jstor.org/stable/2275678.
[8] A. Herzig, A new decidable fragment of first order logic, in: Abstracts of the 3rd Logical Biennial
Summer School and Conference in honour of S. C. Kleene, Varna, Bulgaria, 1990.
[9] B. Bednarczyk, Exploiting forwardness: Satisfiability and query-entailment in forward guarded
fragment, in: W. Faber, G. Friedrich, M. Gebser, M. Morak (Eds.), Logics in Artificial Intelligence
- 17th European Conference, JELIA 2021, Virtual Event, May 17-20, 2021, Proceedings, volume
12678 of Lecture Notes in Computer Science, Springer, 2021, pp. 179β193. URL: https://doi.org/10.
1007/978-3-030-75775-5_13. doi:10.1007/978-3-030-75775-5\_13.
[10] I. Pratt-Hartmann, W. Szwast, L. Tendera, The fluted fragment revisited, Journal of Symbolic Logic
84 (2019) 1020β1048.
[11] S. Schmitz, Complexity hierarchies beyond elementary, ACM Transactions on Computational
Logic 8 (2016). URL: https://doi.org/10.1145/2858784. doi:10.1145/2858784.
[12] R. Jaakkola, Ordered fragments of first-order logic, in: F. Bonchi, S. J. Puglisi (Eds.), 46th Interna-
tional Symposium on Mathematical Foundations of Computer Science, MFCS 2021, August 23-27,
2021, Tallinn, Estonia, volume 202 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum fΓΌr Informatik,
2021, pp. 62:1β62:14. URL: https://doi.org/10.4230/LIPIcs.MFCS.2021.62. doi:10.4230/LIPIcs.
MFCS.2021.62.
[13] B. Bednarczyk, R. Jaakkola, Towards a model theory of ordered logics: Expressivity and interpo-
lation, in: S. Szeider, R. Ganian, A. Silva (Eds.), 47th International Symposium on Mathematical
Foundations of Computer Science, MFCS 2022, August 22-26, 2022, Vienna, Austria, volume
241 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum fΓΌr Informatik, 2022, pp. 15:1β15:14. URL:
https://doi.org/10.4230/LIPIcs.MFCS.2022.15. doi:10.4230/LIPIcs.MFCS.2022.15.
[14] U. Hustadt, R. A. Schmidt, L. Georgieva, A survey of decidable first-order fragments and description
logics, Journal of Relational Methods in Computer Science 1 (2004) 251β276.
[15] B. Bednarczyk, D. Kojelis, I. Pratt-Hartmann, On the Limits of Decision: the Adjacent Fragment
of First-Order Logic, in: K. Etessami, U. Feige, G. Puppis (Eds.), 50th International Colloquium
on Automata, Languages, and Programming (ICALP 2023), volume 261 of Leibniz International
Proceedings in Informatics (LIPIcs), Schloss Dagstuhl β Leibniz-Zentrum fΓΌr Informatik, Dagstuhl,
Germany, 2023, pp. 111:1β111:21. URL: https://drops-dev.dagstuhl.de/entities/document/10.4230/
LIPIcs.ICALP.2023.111. doi:10.4230/LIPIcs.ICALP.2023.111.
[16] E. GrΓ€del, On the restraining power of guards, The Journal of Symbolic Logic 64 (1999) 1719β1742.
URL: http://www.jstor.org/stable/2586808.
[17] B. Bednarczyk, D. Kojelis, I. Pratt-Hartmann, On the limits of decision: the adjacent fragment of
first-order logic, ArXiV abs/2305.03133 (2023). arXiv:2305.03133.