We study the fluted fragment of first-order logic which is often viewed as a multi-variable non-guarded extension to various systems of description logics lacking role-inverses. In this paper we show that satisfiable fluted sentences (even under reasonable extensions) admit special kinds of “nice” models which we call globally/locally homogeneous. Homogeneous models allow us to simplify methods for analysing fluted logics with counting quantifiers and establish a novel result for the decidability of the (finite) satisfiability problem for the fluted fragment with periodic counting. More specifically, we will show that the (finite) satisfiability problem for the language is Tower-complete. If only two variable are used, computational complexity drops toNExpTimecompleteness. We supplement our findings by showing that generalisations of fluted logics with counting, such as the adjacent fragment with counting, have finite and general satisfiability problems which are, respectively, Σ01and Π10-complete. Additionally, satisfiability becomes Σ11-complete if periodic counting quantifiers are permitted.
1) → ∃ 2(( 2) ∧ ( 1, 2) ∧ ∀ 3(( 3) → ( 1, 2, 3)))).
(1) of arityℓ−+1 , is in ℱ ℒ
[ℓ]; Sentences axiomatising transitivity, symmetry and reflexivity are not in the fluted fragment.
The fluted fragment is a member of argument-sequence logics – a family of decidable (in terms of
satisfiability) fragments of first-order logic which also includes the ordered [
In this paper we will mostly be concerned with what we call thflueted fragment with periodic counting (denoted ℱ ℒ ). Formally, this language is the union of sets of formulasℱ ℒ simultaneous induction as follows: (i) any atom ( , … , ℓ), where , … , ℓ is a contiguous subsequence of 1, 2, … and is a predicate (ii) ℱ ℒ (iii) if ∈ ℱ ℒ https://daumantaskojelis.github.io/ (D. Kojelis) [ℓ] is closed under Boolean combinations; [ℓ+1], then ∃[ + ] ℓ+1 is in ℱ ℒ [ℓ] for every, ∈ ℕ
CEUR Workshop
ISSN1613-0073
Semantically, , ̄⊧ ∃ [ + ] ℓ+1 if and only if |{ ∈ ∣ ⊧ []}̄| ∈ { + ∣ ∈ ℕ} . We write ℱ ℒ ∶= ⋃ℓ≥0 ℱ ℒ [ℓ] for the set of all fluted formulas with periodic counting and define the ℓ-variable fragment ofℱ ℒ to be the set ℱ ℒ ℓ ∶= ℱ ℒ ∩ ℱ ℓ.
We remark that periodic counting quantifiers generalise standard (threshold) counting quantifiers
which have been an object of intensive study as an extension for the fluted fragment in the past few
years [
The origins offlutedness trace back to the works of W. V. Quine9[]. It is, however, the definition
given by W. C. Purdy (in [
In this paper we establish that classes of models of satisfiable ℱ ℒ -sentences always contain a
“nice” structure in which elements behave (in a sense that we will make clearh)omogeneously. Utilising
this behaviour we will show that the fluted fragment extended with periodic counting quantifiers has
a decidable satisfiability problem. Intriguingly, even though periodic counting quantifiers generalise
standard counting quantifiers, our methodology allows us to avoidPresburger quantification , which was
required to establish decidability of satisfiability forℱ ℒ with standard counting [
To contrast our decidability results, we show that the satisfiability problems for the fluted fragment with counting extensions become undecidable when minimal syntactic relaxations are allowed. More precisely, we show that the finite satisfiability problem for the 3-variable adjacent fragment with counting is Σ01-complete. Additionally, the general satisfiability problem will be shown to be Π01complete when 4 variables are used, andΣ11-complete if periodic counting is allowed. Denoting the adjacent fragment as ℱ , we provide a survey of complexity and undecidability standings in Tabl1e.
The work in this paper is closely related to1[
The full paper is published in the proceedings of the 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025) [17]. The accompanying technical report with detailed proofs is available on arxiv [18].
standard counting periodic
ℱ ℒ 2 NExp-c [19] NExp-c [21] NExp-c Th 5
ℱ ℒ ℓ
(ℓ−2)-NExp [20]
(ℓ−1)-NExp [
ℱ 3
NExp-c [
ℱ
(−2) -NExp [
We restrict attention to normal-form fluted sentences without counting quantifiers: ⋀ ∀ 1( ( 1) → ∀ 2 ( 1, 2)) ∧ ⋀ ∀ 1( ( 1) → ∃ 2 ( 1, 2)), ∈ ∈ (3) where , are quantifier-free ℱ ℒ 1-formulas and , are quantifier free ℱ ℒ 2-formulas indexed by ifnite sets and . We allow equality symbols to be present in both and .
Take Σ to be any function- and constant-free signature. A flutedℓ-type overΣ is a maximal consistent set of fluted formulas formed by taking ( ℓ−+1 , … , ℓ) or¬( ℓ−+1 , … , ℓ) for ∈ Σ ∪ {=} of arity ≤ ℓ . Each ℓ-tuple ̄ in any given Σ-structure realises a unique fluted ℓ-type (denoted ftp []̄ ) such that1 ±( ℓ−+1 , … , ℓ) ∈ ftp []̄ if ⊧ ±[ ℓ−+1 , … , ℓ].
Now, keep the Σ-structure and take to be a 1-type overΣ. Writing ∶= { ∈ ∣ tfp [] = } we say that is globally homogeneous in if there is some ∈ such that, for all ∈ , the following holds: • ftp [] = ftp [] , • ftp [] = tfp [] , and • ftp [] = tfp [] for each ∈ ∖ {, }
.
Suppose now, that is not globally homogeneous in . We proceed by modifying the structur e in such a way that the resulting structur e ′ has being globally homogeneous, whilst also maintaining tfp ′[] = tfp [] for all ∈ ∖ and ∈ . The crux of our construction is that, when given distinct elements , ∈ , there is no relation between the fluted 2-types of and . To start the construction, let ′ be a structure interpretingΣ over the domain and, for each ∈ ∖ and ∈ , set ftp ′[] ∶= ftp [] . Notice that, for each ∈ , ftp ′[] = ftp [] by the previous assignment. Take any ∈ and call it the example element. Now, set ftp ′[] ∶= ftp [] , ftp ′[] ∶= ftp [] and ftp ′[] ∶= ftp [] for each ∈ and ∈ ∖ {, } . It is easy to verify that no redefinitions take place. Moreover, 1 = 2 ∈ ftp ′[] if and only if = for each, ∈ . We claim ⊧ implies ′ ⊧ ; it being understood that is a normal-formℱ ℒ 2-sentence. To see this, we need only consider elements ∈ and verify that they meet the universal and existential requirements of. Let ∈ be the example element picked previously. Sinceftp ′[] = ftp [] = , we have that ′ ⊧ [] if ⊧ [] for all ∈ . Supposing indeed that ⊧ [] , let ∈ be such that ⊧ [] . If = , then ′ ⊧ [] . In case = , then ′ ⊧ [] . If neither is the case, then ′ ⊧ [] . Either way we have that ′, ⊧ ( 1) → ∃ 2 ( 1, 2) as required. The argument as to wh y ′, ⊧ ( 1) → ∀ 2 ( 1, 2) is analogous.
Notice that, in the rewiring above, elements∉ have not been touched; i.e.ftp ′[] ∶= tfp [] for each ∈ . We may run the procedure onevery fluted 1-type thus obtaining a model in which every 1-type is globally homogeneous. We invite the reader to think of such models as structures in which elements are “stripped of their individuality”. Thus, we need only be concerned with how 1- and 2-types interact with one-another.
It should be clear that restricting attention to globally homogeneous models greatly simplifies the task of determining satisfiability. As it turns out, there are appropriate generalisations of global homogeneity for multi-variable fragments ofℱ ℒ; even in the presence of syntactic extensions such as periodic counting quantifiers. We refer the reader to the full article for details. 1± stands for the negation symbol¬ or lack thereof. Both instances o±f are to evaluate to the same symbol. The work is supported by the NCN grant 2018/31/B/ST6/03662.
The author(s) have not employed any Generative AI tools. 2022, August 22-26, 2022, Vienna, Austria, volume 241 ofLIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, pp. 15:1–15:14. [16] M. Benedikt, E. V. Kostylev, T. Tan, Two variable logic with ultimately periodic counting, SIAM
Journal on Computing 53 (2024) 884–968. [17] D. Kojelis, On Homogeneous Models of Fluted Languages, in: J. Endrullis, S. Schmitz (Eds.), 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025), volume 326 oLfeibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 2025, pp. 9:1–9:20. URL: https://drops.dagstuhl.de/entities/document/10.4230/ LIPIcs.CSL.2025.9. doi:10.4230/LIPIcs.CSL.2025.9. [18] D. Kojelis, On homogeneous model of fluted languages, 2024. URL: https://arxiv.org/abs/2411.1908 4.
arXiv:2411.19084. [19] E. Grädel, P. G. Kolaitis, M. Y. Vardi, On the decision problem for two-variable first-order logic,
The Bulletin of Symbolic Logic 3 (1997) 53–69. [20] I. Pratt-Hartmann, W. Szwast, L. Tendera, The fluted fragment revisited, Journal of Symbolic Logic 84 (2019) 1020–1048. [21] I. Pratt-Hartmann, The two-variable fragment with counting revisited, in: Logic, Language, Information and Computation, 17th International Workshop, WoLLIC 2010, Brasilia, Brazil, July 6-9, 2010. Proceedings, volume 6188 ofLecture Notes in Computer Science, Springer, 2010, pp. 42–54.