On the of Limits of Decision: the Adjacent Fragment of First-Order Logic (Extended Abstract)

Abstract

We define 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) 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 efect 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

• eol>decidability
• satisfiability
• variable-ordered logics
• complexity

-

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 sufix of 1 · · · . forward fragment [ 9 ], we insist only that ¯ be an infix

In the ordered fragment, due to A. Herzig [8], by contrast, we insist that ¯ be a prefix of 1 · · · . In the

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 ≥

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 aforded by the forward

of 1 · · · . fragment yields no diference in expressive power [13].

Say that a word ¯ over the alphabet {1, . . . , } ( ≥ letters difer by at most 1. For example, 321222343 is adjacent, but 132 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 0) is adjacent if the indices of neighbouring ∀1∀2∀3∃4∀5 (︀ (1232345) → (1234345))︀ lfuted, ordered and forward fragments; the inclusion is strict, since the formulas is a validity of ℱ , as can be seen by assigning 4 the same value as 2. Evidently, ℱ includes the ∀1 (11), ∀12(︀ (12) → (21))︀ , expressing transitivity; i.e. stating that is reflexive and symmetric, respectively, are in ℱ . It is worth noting that the formula ∀123 ︁( (︀ (12) ∧ (23))︀ → (13) , ︁) ︁(

︁( is not in ℱ as the variable 2 is skipped in the atom (13).

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: ∀12 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: ∀12 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 ≤ < ). We write A to denote the set of adjacent functions : [1, ] → [1, ]. Since [ 1, 0 ] = ∅, we have A0 = {∅}, and A0 = ∅ 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 1 for all 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 ︁) ︁) a b f e d a b c ¯ ¯ a b c b a a a d e f e d a d e f b a b f ( + 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 difer 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 dificult 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 efect 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 hard. ℱ ℓ is in (ℓ − 2) − NExpTime and ⌊ℓ/2⌋ − NExpTime

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 encoding 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.

[12] R. Jaakkola, Ordered fragments of first-order logic, in: F. Bonchi, S. J. Puglisi (Eds.), 46th International 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 interpolation, 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 ifrst-order logic, ArXiV abs/2305.03133 (2023). arXiv:2305.03133.

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ématiques 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.