On Homogeneous Models of Fluted Languages

The fluted fragment (denoted $ℱℒ$) is a fragment of first-order logic in which, roughly put, variables appear in predicates following the order in which they were quantified. For illustrative purposes, we translate the sentence “Every conductor nominates their favorite soloist to play at every concert” into this language as follows:

As a non-example, the sentences axiomatising transitivity, symmetry and reflexivity of a relation 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 [11, 13], forward [2] and adjacent [4] fragments. The fluted fragment in particular is decidable in terms of satisfiability even in the presence of counting quantifiers [19] or a distinguished transitive relation [22]. Surprisingly, the satisfiability problem for $ℱℒ$ under a combination of the two not only retains decidability but also has the finite model property [24]. We refer the reader to [23] for a survey.

In this paper we will mostly be concerned with what we call the fluted fragment with periodic counting (denoted $ℱℒ𝒫𝒞$). 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 [19, 24]. Under this new formalism, we are allowed to write formulas requesting an even number of existential witnesses. As an example, we can express sentences as “Every orchestra hires an even number of people to play first violin” in our language (see (2)).

The origins of flutedness trace back to the works of W. V. Quine [26]. It is, however, the definition given by W. C. Purdy (in [25]) that has become widespread and will be the one we use. The popularity of Purdy’s idea of flutedness is not without cause, at least when keeping the field of description logics in mind. Indeed, after a routine translation, formulas of the description logic $𝒜ℒ𝒞$ are contained in the two-variable sub-fragment of $ℱℒ𝒫𝒞$. This is even the case when $𝒜ℒ𝒞$ is augmented with role hierarchies, nominals and/or cardinality restrictions (possibly with modulo operations). We refer the reader to [12] for more details. In terms of expressive power, $ℱℒ𝒫𝒞$ closely parallels $𝒜ℒ𝒞𝒮𝒞𝒞$ – a new formalism with counting constrains expressible in quantifier-free Boolean algebra with Presburger arithmetic (see [16, 1]). Thus, noting that the guarded fragment with at least three variables becomes undecidable under counting extensions [8], and that the guarded fluted fragment has “nice” model theoretic properties such as Craig interpolation [3], fluted languages emerge as perfect candidates for generalising description logics in a multi-variable context.

In Sections 3 and 4 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 clear) homogeneously. 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 avoid Presburger quantification, which was required to establish decidability of satisfiability for $ℱℒ$ with standard counting [19].

In section 5 we show that the satisfiability problems for the fluted fragment with counting extensions become undecidable when minimal syntactic relaxations are allowed. More precisely, the section will culminate with a result showing that the finite satisfiability problem for the 3-variable adjacent fragment with counting is ${\mathrm{\Sigma }}_1^0$-complete. Additionally, the general satisfiability problem will be shown to be ${\mathrm{\Pi }}_1^0$-complete when 4 variables are used, and ${\mathrm{\Sigma }}_1^1$-complete if periodic counting is allowed. Denoting the adjacent fragment as $𝒜ℱ$, we provide a brief survey of complexity and undecidability standings in Table 1.

The work in this paper is closely related to [6] in which decidability of satisfiability is established for the two-variable fragment with periodic counting (denoted $ℱ{𝒪}_{\text{Pres}}^2$) but without a sharp complexity-theoretic bound. Our homogeneity conditions, which stem from lack of inverse relations in fluted logics, allow us to establish NExpTime-completeness for both the finite and general satisfiability problems of $ℱℒ𝒫{𝒞}^2$.

We use $\mathbb{N}$ to denote the set of integers $\{0,1,2,\mathrm{\dots }\}$, and ${\mathbb{N}}^{\ast }$ to denote $\mathbb{N}$ along with the first infinite cardinal; i.e. ${\mathbb{N}}^{\ast }=\mathbb{N}\cup \{{\mathrm{\aleph }}_0\}$. By picking some $n,p\in \mathbb{N}$ we write $n^{+p}$ for the linear set $\{n+ip\mid i\in \mathbb{N}\}$. In the extended integers ${\mathbb{N}}^{\ast }$, the cardinal ${\mathrm{\aleph }}_0$ is the maximum element under the canonical ordering “” and

• $\mathbf{■}$

  $0\cdot {\mathrm{\aleph }}_0={\mathrm{\aleph }}_0\cdot 0=0$;

• $\mathbf{■}$

  $n+{\mathrm{\aleph }}_0={\mathrm{\aleph }}_0+n={\mathrm{\aleph }}_0$ for all $n\in {\mathbb{N}}^{\ast }$; and

• $\mathbf{■}$

  $n\cdot {\mathrm{\aleph }}_0={\mathrm{\aleph }}_0\cdot n={\mathrm{\aleph }}_0$ for all $n\in {\mathbb{N}}^{\ast }\setminus \{0\}$.

A linear Diophantine inequation is an expression of the form $a_1{v}_1+\mathrm{\cdots }+a_n{v}_n+b\bowtie c_1{v}_1+\mathrm{\cdots }+c_n{v}_n+d,$ where ${(a_i)}_{i=1}^n,b,{(c_i)}_{i=1}^n,d$ are constant values taken form ${\mathbb{N}}^{\ast }$, $\overline{v}=v_1,\mathrm{\dots }{v}_n$ is a vector of variables, and “$\bowtie$” is any of the relations “” (each interpreted as one would assume). It is known that when the cardinal ${\mathrm{\aleph }}_0$ is disallowed, a solution for a set of such inequations may be found in NPTime [17]. The picture does not change when ${\mathrm{\aleph }}_0$ is permitted as a solution and/or constant. Indeed, we may reduce the problem of finding a solution over ${\mathbb{N}}^{\ast }$ to that of finding it over $\mathbb{N}$ as follows. First guess which variables should be mapped to ${\mathrm{\aleph }}_0$ and which should have a finite value. Then, check that each inequation featuring a variable assigned ${\mathrm{\aleph }}_0$ holds and discard them. What will be left is a system of inequations with constants in $\mathbb{N}$ and in variables assumed to be finite. See [20, Ch 7.4] for greater detail. We will allow systems of inequations to contain disjunctions.

By a word $\overline{a}\in A^n$ we mean a tuple $\overline{a}=a_1\mathrm{\cdots }{a}_n$, where $a_i\in A$ for each $i$, $1\le i\le n$. In case $n=1$, we often write $a$ instead of $\overline{a}$. By ${\overline{a}}^{-1}$ we mean the reversal of $\overline{a}$; i.e. ${\overline{a}}^{-1}=a_n\mathrm{\cdots }{a}_1$. If $\overline{a}$ and $\overline{b}$ are words we write $\overline{a}\overline{b}$ for the concatenation of the two. We use the terms “tuple” and “word” interchangeably.

Now, take some structure $𝔄$ and an $i$-tuple $\overline{a}$ of elements from $A$. Suppose $B=\{b\in A\mid 𝔄,\overline{a}b\vDash \phi \}$ for some first-order formula $\phi (x_1,\mathrm{\dots },x_{i+1})$. Fixing $n,p\in \mathbb{N}$ we extend the syntax of first-order logic with (threshold) counting quantifiers ${\exists }_{[\ge n]}$ and periodic counting quantifier ${\exists }_{[n^{+p}]}$. Semantically, $𝔄,\overline{a}\vDash {\exists }_{[\ge n]}{x}_{i+1}\phi$ if and only if $|B|\ge n$. Similarly, $𝔄,\overline{a}\vDash {\exists }_{[n^{+p}]}{x}_{i+1}\phi$ if and only if $|B|\in n^{+p}$. We refrain from further generalisation to ultimately periodic counting quantifier ${\exists }_{[n_1^{+p_1}\cup \mathrm{\cdots }\cup n_k^{+p_k}]}$ (as in [6]) as they can be expressed as a disjunction of formulas using periodic counting quantifiers ${\exists }_{[n_1^{+p_1}]}{x}_{i+1}\phi \vee \mathrm{\cdots }\vee {\exists }_{[n_k^{+p_k}]}{x}_{i+1}\phi$. Thus, a sentence such as “Every orchestra hires an even number of people to play first violin” may be written in a language with periodic counting:

Formally, the fluted fragment with periodic counting is the union of sets of formulas $ℱℒ𝒫{𝒞}^{[\mathrm{\ell }]}$ defined by simultaneous induction as follows:

1. (i)

   any atom $r(x_k,\mathrm{\dots },x_{\mathrm{\ell }})$, where $x_k,\mathrm{\dots },x_{\mathrm{\ell }}$ is a contiguous subsequence of $x_1,x_2,\mathrm{\dots }$ and $r$ is a predicate of arity $\mathrm{\ell }-k+1$, is in $ℱℒ𝒫{𝒞}^{[\mathrm{\ell }]}$;

2. (ii)

   $ℱℒ𝒫{𝒞}^{[\mathrm{\ell }]}$ is closed under Boolean combinations;

3. (iii)

   if $\phi \in ℱℒ𝒫{𝒞}^{[\mathrm{\ell }+1]}$, then ${\exists }_{[n^{+p}]}{x}_{\mathrm{\ell }+1}\phi$ is in $ℱℒ𝒫{𝒞}^{[\mathrm{\ell }]}$ for every $n,p\in \mathbb{N}$.

We write $ℱℒ𝒫𝒞={\bigcup }_{\mathrm{\ell }\ge 0}ℱℒ𝒫{𝒞}^{[\mathrm{\ell }]}$ for the set of all fluted formulas with periodic counting and define the $\mathrm{\ell }$-variable fluted fragment with periodic counting to be the set $ℱℒ𝒫{𝒞}^{\mathrm{\ell }}:=ℱℒ𝒫𝒞\cap ℱ{𝒪}^{\mathrm{\ell }}$. (Here $ℱ{𝒪}^{\mathrm{\ell }}$ is the set of first-order formulas that do not use more than $\mathrm{\ell }$ variables). We will implicitly restrict attention to signatures $\sigma \cup \{=\}$ which feature no function and/or constant symbols, and where “$=$” is always interpreted as the canonical equality relation. Lastly, we use $\forall x\phi$ interchangeably with ${\exists }_{[0^{+0}]}x\neg \phi$ whenever convenient.

Variables in fluted logics convey no meaningful information. Indeed, since the arity of every predicate in $\sigma \cup \{=\}$ is fixed and each atom features a suffix of the variable quantification order, we may employ what we call variable-free notation. As an example, formulas (1) and (2) may be (respectively) written as

without ambiguity (up to a shift of variable indices). Writing ${\forall }^{\mathrm{\ell }}$ for $\forall x_1\mathrm{\cdots }\forall x_{\mathrm{\ell }}$, we will employ variable-free notation extensively throughout subsequent sections.

Fix a first-order formula $\phi$ with periodic counting quantifiers. We assume that numeric values are encoded in binary and write $\Vert \phi \Vert$ for the number of symbols used in $\phi$. We point out that the signature of $\phi$ (which we write as $\text{sig}(\phi )$ for brevity) is no larger than $\Vert \phi \Vert$.

Now, let $\phi$ be a formula in $ℱℒ𝒫{𝒞}^{\mathrm{\ell }+1}$. We say that $\phi$ is in normal-form if it takes the following shape

where $R,T$ are sets of indices, each ${\alpha }_r,{\beta }_t$ is a quantifier-free formula in $\mathrm{\ell }$ variables, each ${\gamma }_r,{\delta }_t$ is a quantifier-free formula in $\mathrm{\ell }+1$ variables, and each $n_r^{+p_r},n_t^{+p_t}$ is a linear set. Using standard rewriting techniques we prove the following in Appendix A.

Notice that the negation before the periodic counting quantifier in the second conjunct of (5) is not moved-inwards. This is done deliberately so as to avoid computing complements of linear sets, which may be of exponential size as a function of $\Vert \phi \Vert$.

Now, let $𝔄$ be a structure over a finite signature $\sigma \cup \{=\}$. We say that an atom is $(\mathrm{\ell }+1)$-fluted if it features a suffix of $x_1,\mathrm{\dots },x_{\mathrm{\ell }+1}$ as arguments. The fluted atomic $(\mathrm{\ell }+1)$-type $\tau$ of $a\overline{b}c\in A^{\mathrm{\ell }+1}$ (denoted ${\mathrm{𝖿𝗍𝗉}}_{\mathrm{\ell }+1}^{𝔄}(a\overline{b}c)$) is then the set of $(\mathrm{\ell }+1)$-fluted (possibly negated) atoms over $\sigma \cup \{=\}$ with arity no greater than $\mathrm{\ell }+1$ that are satisfied by $a\overline{b}c$ in $𝔄$. We invite the reader to view the tuple $a\overline{b}$ as emitting $\tau$, and $\overline{b}c$ as absorbing $\tau$. Write $\tau {\upharpoonright }_{[2,\mathrm{\ell }+1]}$ for the fluted $\mathrm{\ell }$-type $\pi$ obtained by deleting entries in $\tau$ of arity greater than $\mathrm{\ell }$ and decrementing variable indices by 1. We say that a fluted $\mathrm{\ell }$-type $\pi$ is an endpoint of a fluted $(\mathrm{\ell }+1)$-type $\tau$ if $\tau {\upharpoonright }_{[2,\mathrm{\ell }+1]}=\pi$. We define ${\mathrm{𝖥𝖳𝖯}}_{\mathrm{\ell }+1}^{\sigma }$ to be the set of all fluted $(\mathrm{\ell }+1)$-types over $\sigma \cup \{=\}$.

The fluted $\mathrm{\ell }$-profile of $a\overline{b}\in A^{\mathrm{\ell }}$ (denoted ${\mathrm{𝖿𝗉𝗋}}_{\mathrm{\ell }}^{𝔄}(a\overline{b})$) is a function $\rho$ mapping $\tau \in {\mathrm{𝖥𝖳𝖯}}_{\mathrm{\ell }+1}^{\sigma }$ to the number of times $a\overline{b}$ emits $\tau$. Formally, $\rho (\tau )=|\{c\in A\mid {\mathrm{𝖿𝗍𝗉}}_{i+1}^{𝔄}(a\overline{b}c)=\tau \}|.$ If $\phi$ is a quantifier-free $ℱℒ𝒫{𝒞}^{\mathrm{\ell }+1}$-formula, we write $\rho \vDash {\exists }_{[n^{+p}]}\phi$ just in case ${\sum }_{\tau \in {\mathrm{𝖥𝖳𝖯}}_{\mathrm{\ell }+1}^{\sigma }}^{\tau \vDash \phi }\rho (\tau )\in n^{+p}$. Clearly, $\rho \vDash {\exists }_{[n^{+p}]}\phi$ if and only if $𝔄,a\overline{b}\vDash {\exists }_{[n^{+p}]}\phi$.

In the sequel we will assume that all structures are countable. This comes with no loss of generality as $ℱℒ𝒫𝒞$ is subsumed by the countable fragment of infinitary logic ${ℒ}_{{\omega }_1,\omega }$; a language for which the downward Löwenheim-Skolem Theorem holds (folklore, see [15, p. 69]). Note that, in $ℱℒ𝒫𝒞$, the finite model property fails as $\neg {\exists }_{[0^{+1}]}\top$ is an axiom of infinity.

In this section we restrict attention to the two-variable fluted fragment with periodic counting. To achieve decidability of (finite) satisfiability we first specify what kind of “nice” models we will be looking for. Take any $\sigma$-structure $𝔄$ and $\pi \in {\mathrm{𝖥𝖳𝖯}}_1^{\sigma }$. For convenience, we write $A_{\pi }$ for the set of all elements $a\in A$ with ${\mathrm{𝖿𝗍𝗉}}^{𝔄}(a)=\pi$. We say that $\pi$ is globally homogeneous in $𝔄$ if ${\mathrm{𝖿𝗉𝗋}}^{𝔄}(a)={\mathrm{𝖿𝗉𝗋}}^{𝔄}(b)$ for each $a,b\in A_{\pi }$. That is to say, $\pi$ is globally homogeneous in $𝔄$ if, for each $\tau \in {\mathrm{𝖥𝖳𝖯}}_2^{\sigma }$, the number of fluted 2-types $\tau$ emitted is the same for each element in $A_{\pi }$. The structure $𝔄$ is globally homogeneous if each $\pi \in {\mathrm{𝖥𝖳𝖯}}_1^{\sigma }$ is globally homogeneous in $𝔄$.

For the remainder of the section fix some normal-form $ℱℒ𝒫{𝒞}^2$-sentence $\phi$. We claim that if $\phi$ is a satisfiable, then it is satisfiable in a globally homogeneous model. To see this, take some structure $𝔄\vDash \phi$ and a pair of elements $cd\in A^2$ that realised the fluted 2-type $\tau$ in $𝔄$. Since $\tau$ consists of fluted formulas, it does not feature atoms of the form $p(x_1)$ and $p(x_2,x_1)$. Referencing $\tau$ only, we lack information to deduce what formulas are satisfied by the pair $dc$ in $𝔄$. On the other hand, $𝔄,cd\vDash \psi$ if and only if $\tau \vDash \psi$ for each quantifier-free $ℱℒ𝒫{𝒞}^2$-formula $\psi$. Thus, if we were to in any way alter the fluted 2-type of $dc$ in $𝔄$, the set of quantifier-free $ℱℒ𝒫{𝒞}^2$-formulas satisfied by $cd$ in $𝔄$ would not change.

Taking a step back, take any $\pi \in {\mathrm{𝖥𝖳𝖯}}_1^{\sigma }$ and recall that $A_{\pi }\subseteq A$ is the set of all elements realising the 1-type $\pi$ in $𝔄$. We redefine 2-types emitted by elements of $A_{\pi }$ in $𝔄$ in such a way that makes $\pi$ globally homogeneous in the rewiring of $𝔄$. Let us fix any $a\in A_{\pi }$ and write $\rho ={\mathrm{𝖿𝗉𝗋}}^{𝔄}(a)$. The element $a$ and profile $\rho$ picked will serve as an “example” of how the rest of $A_{\pi }$ should form fluted 2-types with other elements of the model. Taking any $b\in A_{\pi }\setminus \{a\}$ and $c\in A\setminus \{a,b\}$ we see that it is impossible to prohibit $b$ from emitting the fluted 2-type ${\mathrm{𝖿𝗍𝗉}}^{𝔄}(ac)$ to $c$ via any normal-form $ℱℒ𝒫{𝒞}^2$-formula. We thus allow $b$ to impersonate $a$ in $𝔄$ by rewiring the fluted 2-type ${\mathrm{𝖿𝗍𝗉}}^{𝔄}(bc)$ to be ${\mathrm{𝖿𝗍𝗉}}^{𝔄}(ac)$ for each $c\in A\setminus \{a,b\}$ and, additionally, by resetting ${\mathrm{𝖿𝗍𝗉}}^{𝔄}(ba)$ to be the 2-type ${\mathrm{𝖿𝗍𝗉}}^{𝔄}(ab)$ and ${\mathrm{𝖿𝗍𝗉}}^{𝔄}(bb)$ to be ${\mathrm{𝖿𝗍𝗉}}^{𝔄}(aa)$. Clearly, only fluted 2-types emitted by $b$ were reconsidered in this procedure, thus pairs in $(A\setminus \{b\})\times A$ satisfy the same quantifier-free $ℱℒ𝒫{𝒞}^2$-formulas as before. To see that $𝔄$ still models $\phi$ we need only show that $b$ does not violate ${\alpha }_r\to {\exists }_{[n_r^{+p_r}]}{\gamma }_r$ and ${\beta }_t\to \neg {\exists }_{[n_t^{+p_t}]}{\delta }_t$ for each $r\in R$ and $t\in T$. By our rewiring procedure, we have that ${\mathrm{𝖿𝗉𝗋}}^{𝔄}(a)=\rho ={\mathrm{𝖿𝗉𝗋}}^{𝔄}(b)$. Thus,

Having already argued that $𝔄,a\vDash {\alpha }_r\to {\exists }_{[n_r^{+p_r}]}{\gamma }_r$ and $𝔄,a\vDash {\beta }_t\to \neg {\exists }_{[n_t^{+p_t}]}{\delta }_t$ for each $r\in R$ and $t\in T$ we therefore conclude that $𝔄\vDash \phi$.

Since the only 2-types redefined are those emitted by $b$, we can run this construction in parallel for each element in $A_{\pi }\setminus \{a\}$. Clearly, this renders $\pi$ globally homogeneous in the rewired model. Since elements in $A\setminus A_{\pi }$ are left untouched by our rewiring, we can repeat this procedure for each $\pi \in {\mathrm{𝖥𝖳𝖯}}_1^{\sigma }$ thus proving the following:

In globally homogeneous structures elements realising the same fluted 1-type are, in a sense, stripped away of their individuality as they all realise the same fluted 1-profile. When the globally homogeneous structure $𝔄$ is clear from context, we can unambiguously write ${\rho }_{\pi }$ for the fluted 1-profile realised by each element of $A_{\pi }$ (for $\pi \in {\mathrm{𝖥𝖳𝖯}}_1^{\sigma }$).

When considering the (finite) satisfiability problem for normal-form $ℱℒ𝒫{𝒞}^2$-sentences such as $\phi$, we will confine ourselves to the search of globally homogeneous models. More precisely, we will produce a system of linear Diophantine inequations $\mathrm{\Psi }$ that has a solution over ${\mathbb{N}}^{\ast }$ if and only if $\phi$ is satisfiable in a globally homogeneous model. For this purpose, let ${(x_{\pi })}_{\pi \in {\mathrm{𝖥𝖳𝖯}}_1^{\sigma }}$, ${(y_{\pi ,\tau })}_{\pi \in {\mathrm{𝖥𝖳𝖯}}_1^{\sigma }}^{\tau \in {\mathrm{𝖥𝖳𝖯}}_2^{\sigma }}$, ${(i_{\pi ,r})}_{\pi \in {\mathrm{𝖥𝖳𝖯}}_1^{\sigma }}^{r\in R}$, and ${(j_{\pi ,t})}_{\pi \in {\mathrm{𝖥𝖳𝖯}}_1^{\sigma }}^{t\in T}$ be sequences of variables. Intuitively, the value assigned to $x_{\pi }$ will represent the number of elements realising the fluted 1-type $\pi$; $y_{\pi ,\tau }$ – the number times the 2-type $\tau$ is emitted by an element realising $\pi$; and with $i_{\pi ,r}$ and $j_{\pi ,t}$ acting as periodic counters for elements realising $\pi$ when considering linear sets $n_r^{+p_r}$ and $n_t^{+p_t}$. To be more precise, when given a satisfying assignment for $\mathrm{\Psi }$, we will build a globally homogeneous $𝔄\vDash \phi$ with

On the other hand, we will have that any globally homogeneous model $𝔄\vDash \phi$ gives rise to a solution of $\mathrm{\Psi }$ with the following assignments for all $\pi \in {\mathrm{𝖥𝖳𝖯}}_1^{\sigma }$, $\tau \in {\mathrm{𝖥𝖳𝖯}}_2^{\sigma }$, $r\in R$ and $t\in T$:¹¹1 In case $p_r$ (resp. $p_t$) is $0$, we allow $i_{\pi ,r}$ (resp. $j_{\pi ,t}$) to take any integer value.

We will proceed first by showing that the latter assignment satisfies our (yet to be defined) system of inequations $\mathrm{\Psi }:={\mathrm{\Psi }}_1\cup \mathrm{\cdots }\cup {\mathrm{\Psi }}_6$.

When considering any model $𝔄\vDash \phi$ we have that the domain $A={\bigcup }_{\pi \in {\mathrm{𝖥𝖳𝖯}}_1^{\sigma }}{A}_{\pi }$ is non-empty. The following is thus trivially satisfied by the assignment $x_{\pi }:=A_{\pi }$:

Additionally, picking any element $a\in A_{\pi }$ (for any $\pi \in {\mathrm{𝖥𝖳𝖯}}_1^{\sigma }$) and picking any ${\pi }^{\prime }\in {\mathrm{𝖥𝖳𝖯}}_{{\pi }^{\prime }}^{\sigma }$, we have that the number of fluted 2-types emitted by $a$ to $A_{{\pi }^{\prime }}$ must be $|A_{{\pi }^{\prime }}|=x_{{\pi }^{\prime }}$. Assuming that $𝔄$ is globally homogeneous, we may fixate on the fact that the shared profile ${\rho }_{\pi }$ of $\pi$ has exactly $|A_{{\pi }^{\prime }}|$ witnesses for fluted 2-types with the endpoint ${\pi }^{\prime }$, or, more formally, ${\sum }_{\tau \in {\mathrm{𝖥𝖳𝖯}}_2^{\sigma }}^{\tau {\upharpoonright }_{[2,2]}={\pi }^{\prime }}\rho (\tau )=|A_{{\pi }^{\prime }}|$. Thus, the assignment $y_{\pi ,\tau }:={\rho }_{\pi }(\tau )$ satisfies the following set of inequations:

Of course, under the supposition that $\pi \vDash {\alpha }_r$ for some $r\in R$ and $\pi \in {\mathrm{𝖥𝖳𝖯}}_1^{\sigma }$ such that $|A_{\pi }|\ge 1$, we have that ${\rho }_{\pi }\vDash {\exists }_{[n_r^{+p_r}]}{\gamma }_r$. Clearly, $k:={\sum }_{\tau \in {\mathrm{𝖥𝖳𝖯}}_2^{\sigma }}^{\tau \vDash {\gamma }_r}{\rho }_{\pi }(\tau )$ must be a member of the linear set $n_r^{+p_r}$. Thus, there is a period counter $i_{\pi ,r}\in \mathbb{N}$ such that $k=n_r+i_{\pi ,r}{p}_r$. Turning the equation around we get that $i_{\pi ,r}=(k-n_r)/p_r$. Recalling that ${\rho }_{\pi }(\tau )=y_{\pi ,\tau }$ for all $\tau \in {\mathrm{𝖥𝖳𝖯}}_2^{\sigma }$, we have that the following is satisfied by our assignments:

On the other hand, supposing $\pi \vDash {\beta }_t$ for some $t\in T$ and with $\pi \in {\mathrm{𝖥𝖳𝖯}}_1^{\sigma }$ such that $|A_{\pi }|\ge 1$, we have that ${\rho }_{\pi }\vDash ̸{\exists }_{[n_t^{+p_t}]}{\delta }_r$, thus leaving $k:={\sum }_{\tau \in {\mathrm{𝖥𝖳𝖯}}_2^{\sigma }}^{\tau \vDash {\gamma }_r}{\rho }_{\pi }(\tau )$ outside of the linear set $n_t^{+p_t}$. Notice that this happens when the following conditions are met:

1. 1.

   ; or

2. 2.

   $p_t\ne 0$ and $k>m$ for each $m\in n_t^{+p_t}$ (which only happens when $k={\mathrm{\aleph }}_0$); or

3. 3.

   $p_t=0$ and $k>n_t$; or

4. 4.

   for some $m\in n_t^{+p_t}$ we have .

Note that the listed conditions are exhaustive. We translate the requirements 1–4 into four functions ${\mathrm{\Theta }}_1,\mathrm{\dots },{\mathrm{\Theta }}_4$ which map fluted 1-types paired with indices in $T$ to linear equations. The functions are then defined as follows:

• $\mathbf{■}$

  ,

• $\mathbf{■}$

  ${\mathrm{\Theta }}_2(\pi ,t):={\sum }_{\tau \in {\mathrm{𝖥𝖳𝖯}}_2^{\sigma }}^{\tau \vDash {\delta }_t}{y}_{\pi ,\tau }={\mathrm{\aleph }}_0$,

• $\mathbf{■}$

  ,

• $\mathbf{■}$

  .

Since $k$ adheres to at least one of the four conditions, we write the following clauses for eligible fluted $1$-types:

To verify that $j_{\pi ,\tau }=\lfloor (k-n_t)/p_t\rfloor$ is indeed a satisfying assignment for ${\mathrm{\Psi }}_4$, we need only consider case 4. For this assume that for some $m\in n_t^{+p_t}$. We can thus write $m=n_t+j{p}_t$. Since $j_{\pi ,\tau }=\lfloor (k-n_t)/p_t\rfloor$, we conclude that $j_{\pi ,\tau }=j$ thus satisfying ${\mathrm{\Theta }}_4(\pi ,t)$.

Reflecting on the semantics of the equality predicate, we see that for any given $\pi \in {\mathrm{𝖥𝖳𝖯}}_1^{\sigma }$ in any globally homogeneous model $𝔄\vDash \phi$ there is exactly one $\tau \in {\mathrm{𝖥𝖳𝖯}}_2^{\sigma }$ such that $\tau$ features the non-negated equality predicate and ${\rho }_{\pi }(\tau )\ne 0$. More precisely, ${\rho }_{\pi }(\tau )=1$ and the endpoint of $\tau$ is $\pi$. We have that our assignment respects this condition and thus satisfies the following inequations:

Finally, we forbid the periodic counters ${(i_{\pi ,r})}_{\pi \in {\mathrm{𝖥𝖳𝖯}}_1^{\sigma }}^{r\in R}$ and ${(j_{\pi ,t})}_{\pi \in {\mathrm{𝖥𝖳𝖯}}_1^{\sigma }}^{t\in R}$ from taking the value ${\mathrm{\aleph }}_0$:

Putting everything together, we have engineered a system of equations $\mathrm{\Psi }={\mathrm{\Psi }}_1\cup \mathrm{\cdots }\cup {\mathrm{\Psi }}_6$ that is satisfied by extracting relevant cardinalities (see (7)) from homogeneous models of $\phi$.

We now move on to the converse direction:

We now generalise our results on homogeneity and decidability of satisfiability for higher-arity formulas of $ℱℒ𝒫𝒞$. Thus, throughout this section, we will be working in the $(\mathrm{\ell }+1)$-variable sub-fragment of $ℱℒ𝒫𝒞$, where $\mathrm{\ell }\ge 2$ is fixed.

Firstly, we lift our homogeneity conditions to the multivariable setting. Suppose $𝔄$ is a $\sigma$-structure and take any $(\mathrm{\ell }-1)$-tuple $\overline{b}$ from $A$ and $\pi \in {\mathrm{𝖥𝖳𝖯}}_{\mathrm{\ell }}^{\sigma }$. Let $A_{\pi \leftarrow \overline{b}}$ be the set $\{a\in A\mid {\mathrm{𝖿𝗍𝗉}}^{𝔄}(a\overline{b})=\pi \}$. We say that $\pi$ is $\overline{b}$-homogeneous in $𝔄$ if for each $a,a^{\prime }\in A_{\pi \leftarrow \overline{b}}$ and all $c\in A$ we have that ${\mathrm{𝖿𝗍𝗉}}^{𝔄}(a\overline{b}c)={\mathrm{𝖿𝗍𝗉}}^{𝔄}(a^{\prime }\overline{b}c)$. That is to say, $\overline{b}c$ absorbs the same fluted $(\mathrm{\ell }+1)$-type from each $\mathrm{\ell }$-tuple $a\overline{b}$ that realises the fluted $\mathrm{\ell }$-type $\pi$. If each $\pi \in {\mathrm{𝖥𝖳𝖯}}_{\mathrm{\ell }}^{\sigma }$ is $\overline{b}$-homogeneous in $𝔄$, then we say that the $(\mathrm{\ell }-1)$-tuple $\overline{b}$ is homogeneous in $𝔄$. Finally, if each $(\mathrm{\ell }-1)$-tuple $\overline{b}$ is homogeneous in $𝔄$, then we say that $𝔄$ is locally $\mathrm{\ell }$-homogeneous.

When considering satisfiable normal-form $ℱℒ𝒫{𝒞}^{\mathrm{\ell }+1}$-sentences we can, without loss of generality, confine ourselves to locally $\mathrm{\ell }$-homogeneous structures. To see this fix some normal-form $ℱℒ𝒫{𝒞}^{\mathrm{\ell }+1}$-sentence $\phi$ and take $\overline{b}\in A^{\mathrm{\ell }-1}$ and $a,a^{\prime }\in A_{\pi \leftarrow \overline{b}}$. Proceeding similarly as before Lemma 2 we see that the fluted $(\mathrm{\ell }+1)$-type of $a^{\prime }\overline{b}c$ does not impact the satisfaction of quantifier-free $ℱℒ𝒫{𝒞}^{\mathrm{\ell }+1}$-formulas by $c{\overline{b}}^{-1}{a}^{\prime }$. Thus, redefining the fluted $(\mathrm{\ell }+1)$-types emitted by $a^{\prime }\overline{b}$ will not alter the satisfaction of quantifier-free $ℱℒ𝒫{𝒞}^{\mathrm{\ell }+1}$-formulas by other tuples. Notice again that it is impossible to prohibit ${\mathrm{𝖿𝗍𝗉}}^{𝔄}(a\overline{b}c)\ne {\mathrm{𝖿𝗍𝗉}}^{𝔄}(a^{\prime }\overline{b}c)$ by a normal-form formula. Thus, by setting ${\mathrm{𝖿𝗍𝗉}}^{𝔄}(a^{\prime }\overline{b}c):={\mathrm{𝖿𝗍𝗉}}^{𝔄}(a\overline{b}c)$ for each $c\in A$ and repeating the procedure for each $a^{\prime }\in A_{\pi \leftarrow \overline{b}}\setminus \{a\}$, we will have that $\pi$ is $\overline{b}$-homogeneous in $𝔄$. Clearly $𝔄\vDash \phi$ as the tuples rewired by this procedure (i.e. $a^{\prime }\overline{b}$ with $a^{\prime }\in A_{\pi \leftarrow \overline{b}}\setminus \{a\}$) now emit $\tau \in {\mathrm{𝖥𝖳𝖯}}_{\mathrm{\ell }+1}^{\sigma }$ to a given witness if and only if $a\overline{b}$ does. The rewired tuples thus satisfy the same exact $ℱℒ𝒫{𝒞}^{\mathrm{\ell }+1}$-formulas with at most 1 quantifier as $a\overline{b}$ does. Repeating the procedure for all $\pi \in {\mathrm{𝖥𝖳𝖯}}_{\mathrm{\ell }}^{\sigma }$ and $\overline{b}\in A^{\mathrm{\ell }-1}$ we will have the following:

Using local $\mathrm{\ell }$-homogeneity coupled with variable reduction techniques prevalent in studies of fluted logics (see [21]), we will establish a decidability result for the (finite) satisfiability problem of $ℱℒ𝒫{𝒞}^{\mathrm{\ell }+1}$. More specifically, fixing a normal-form $ℱℒ𝒫{𝒞}^{\mathrm{\ell }+1}$-sentence $\phi$ we will compute a normal-form $ℱℒ𝒫{𝒞}^{\mathrm{\ell }}$-sentence $\psi$ that is satisfiable in structures holding just enough information to build locally $\mathrm{\ell }$-homogeneous models for $\phi$. To aid motivation, we fix $𝔄$ to be any locally $\mathrm{\ell }$-homogeneous model of $\phi$. We shall construct $\psi$ whilst also expanding $𝔄$ into ${𝔄}^{\prime }\vDash \psi$. Note that the construction depends exclusively on the syntactic properties of $\phi$.

First, set ${𝔄}^{\prime }:=𝔄$. Take ${(q_{\pi })}_{\pi \in {\mathrm{𝖥𝖳𝖯}}_{\mathrm{\ell }}^{\sigma }}$ to be a sequence of fresh $(\mathrm{\ell }-1)$-ary predicate symbols. In ${𝔄}^{\prime }$ we decorate $(\mathrm{\ell }-1)$-tuples $\overline{b}$ over $A$ with $q_{\pi }$ just in case we have that $A_{\pi \leftarrow \overline{b}}\ne \mathrm{\varnothing }$. That is to say, $q_{\pi }^{{𝔄}^{\prime }}$ remembers which $(\mathrm{\ell }-1)$-tuples can be extended (by appending an element to the left) to realise the fluted $\mathrm{\ell }$-type $\pi$. It is clear that ${𝔄}^{\prime }$ models the following:

Proceeding similarly, let ${(s_{\pi ,\tau })}_{\pi \in {\mathrm{𝖥𝖳𝖯}}_{\mathrm{\ell }}^{\sigma }}^{\tau \in {\mathrm{𝖥𝖳𝖯}}_{\mathrm{\ell }+1}^{\sigma }}$ be a sequence of new $\mathrm{\ell }$-ary predicates. Intuitively, we will have $\overline{b}c\in s_{\pi ,\tau }^{{𝔄}^{\prime }}$ if in $𝔄$ it is the case that $\overline{b}c$ absorbs the fluted $(\mathrm{\ell }+1)$-type $\tau$ emitted from $a\overline{b}$ for some $a\in A_{\pi \leftarrow \overline{b}}$. Notice that, by local $\mathrm{\ell }$-homogeneity, if $\overline{b}c$ absorbs $\tau$ from some $a\overline{b}$ with $a\in A_{\pi \leftarrow \overline{b}}$, then it absorbs $\tau$ from $a^{\prime }\overline{b}$ for all $a^{\prime }\in A_{\pi \leftarrow \overline{b}}$. Thus, by our construction, $s_{\pi ,\tau }$ is the unique predicate amongst ${(s_{\pi ,{\tau }^{\prime }})}^{{\tau }^{\prime }\in {\mathrm{𝖥𝖳𝖯}}_{\mathrm{\ell }+1}^{\sigma }}$ satisfied by $\overline{b}c$ in ${𝔄}^{\prime }$. Clearly, ${𝔄}^{\prime }$ models:

Again taking $\overline{b}\in A^{\mathrm{\ell }-1}$ and any $\pi \in {\mathrm{𝖥𝖳𝖯}}_{\mathrm{\ell }}^{\sigma }$ suppose $\pi \vDash {\alpha }_r$ for some $r\in R$. In case $A_{\pi \leftarrow \overline{b}}$ is non-empty (thus guaranteeing $\overline{b}\in q_{\pi }^{{𝔄}^{\prime }}$), we pick any $a\in A_{\pi \leftarrow \overline{b}}$ and write $S=\{c\in A\mid 𝔄,a\overline{b}c\vDash {\gamma }_r\}$. Since $\pi$ is $\overline{b}$-homogeneous in $𝔄$, the exact element in $A_{\pi \leftarrow \overline{b}}$ we pick has no effect on $S$. By our construction, $S$ is then exactly the set of element $c\in A$ such that ${𝔄}^{\prime },\overline{b}c\vDash {\bigvee }_{\tau \in {\mathrm{𝖥𝖳𝖯}}_{\mathrm{\ell }+1}^{\sigma }}^{\tau \vDash {\gamma }_r}{s}_{\pi ,\tau }$. Since $|S|\in n_r^{+p_r}$ it is then immediate that ${𝔄}^{\prime }$ models the following:

Similar observations follow whenever $\pi \vDash {\beta }_t$ for some $t\in T$. This time, however, the cardinality of $S=\{c\in A\mid 𝔄,a\overline{b}c\vDash {\delta }_r\}$ must be outside the set $n_r^{+p_r}$. Clearly, ${𝔄}^{\prime }$ models:

Writing $\psi :={\psi }_1\wedge \mathrm{\cdots }\wedge {\psi }_4$ we have shown the following: