The Fluted Fragment with Transitivity

TL;DR

This paper investigates the satisfiability problem for the fluted fragment extended with transitive relations, showing decidability with one relation and undecidability with three relations.

Contribution

It establishes the finite model property for the one-transitive relation case and proves undecidability for the three-transitive relations case.

Findings

Finite model property with one transitive relation

Undecidability with three transitive relations

Complexity varies with the number of transitive relations

Abstract

We study the satisfiability problem for the fluted fragment extended with transitive relations. We show that the logic enjoys the finite model property when only one transitive relation is available. On the other hand we show that the satisfiability problem is undecidable already for the two-variable fragment of the logic in the presence of three transitive relations.

Equations

$$\forall x_1(\text{mbox}student(x_1)\to \neg \forall x_2(\text{mbox}prof(x_2)\to \text{mbox}admires(x_1,x_2)))$$

$$\forall x_1($$

$$\forall x_1.r(x_1,x_1)$$

$$\forall x_1\forall x_2(r(x_1,x_2)\to r(x_2,x_1))$$

$$\forall x_1\forall x_2\forall x_3(r(x_1,x_2)\wedge r(x_2,x_3)\to r(x_1,x_3)),$$

$$\exists x.\mu \forall x.\mu \forall x(\pi \to \exists y(\mu (y)\wedge \pm \mathfrak{t}(x,y)))\forall x(\pi \to \forall y({\pi }^{\prime }(y)\to \pm \mathfrak{t}(x,y))).$$

$$\forall x_1\cdots x_m.\Omega \wedge \underset{i=1}{\overset{s}{\bigwedge }}\forall x_1\cdots x_{m-1}\left({\alpha }_i\to \exists x_m.{\Gamma }_i\right)\wedge \underset{j=1}{\overset{t}{\bigwedge }}\forall x_1\cdots x_{m-1}({\beta }_j\to \forall x_m.{\Delta }_j),$$

$$\forall x\big{(}colour(x)\wedge diag(x)\wedge border(x)\rightarrow\exists y(t(x,y)\wedge colour^{\prime}(y))\big{)},$$

$$\forall x(c_{01}(x)$$

$$\forall x(d_{11}(x)$$

$$\displaystyle\!\!\!\!\!\!\!\!\!\bigwedge_{0\leq i\leq 2,\;0\leq j\leq 5}\!\!\!\!\!\!\!\!\!\!\forall x\big{(}d_{i,j}(x)\wedge\pm e(x)\rightarrow\forall y((b(x,y)\vee g(x,y)\vee r(x,y))\wedge d_{i+1,j+1}(y)\rightarrow\pm e(y))\big{)},$$

$$\mathsf{rt}(x,y):=$$

$$(c_{01}(x)\wedge d_{11}(y))\vee (c_{20}(x)\wedge d_{03}(y))\vee (c_{42}(x)\wedge d_{25}(y))\vee$$

$$\underset{(i,j)\notin \{(0,2),(1,2),(2,1),(3,1),(4,0),(5,0)\}}{\bigvee }(c_{ij}(x)\wedge c_{i+1,j}(y))\vee \underset{(i,j)\notin \{(2,1),(1,3),(0,5)\}}{\bigvee }(d_{ij}(x)\wedge d_{i+1,j}(y))$$

$$\displaystyle\bigwedge_{C\in{\cal C}}\forall x\big{(}C(x)\rightarrow\forall y\big{(}(\mathsf{rt}(x,y)\rightarrow\bigvee_{C^{\prime}:(C,C^{\prime})\in{\cal C}_{H}}C^{\prime}(y))\quad\wedge\quad(\mathsf{lt}(x,y)\rightarrow\bigvee_{C^{\prime}:(C^{\prime},C)\in{\cal C}_{H}}C^{\prime}(y))\big{)}\big{)};$$

$$\mathfrak{A}\models \mathsf{rt}(\rho (i,j),\rho (i+1,j))\dot{\vee }\mathsf{lt}(\rho (i+1,j),\rho (i,j))\wedge \mathsf{up}(\rho (i,j),\rho (i,j+1))\dot{\vee }\mathsf{dn}(\rho (i,j+1),\rho (i,j)).$$

$$\forall x_1(p(x_1)\leftrightarrow \exists x_2.\lambda )\forall x_1(p(x_1)\leftrightarrow \forall x_2.\lambda )P\leftrightarrow \forall x_1.\mu P\leftrightarrow \exists x_1.\mu ,$$

$$\forall x_1{x}_2.\Omega \wedge \underset{i=1}{\overset{s}{\bigwedge }}\forall x_1\left(p_i(x_1)\to \exists x_2.{\Gamma }_i\right)\wedge \underset{j=1}{\overset{t}{\bigwedge }}\forall x_1(q_j(x_1)\to \forall x_2.{\Delta }_j),$$

$$\underset{i=1}{\overset{s}{\bigwedge }}\underset{J\subseteq T}{\bigwedge }\forall x_2(p_i(x_2)\wedge \underset{j\in J}{\bigwedge }{q}_j(x_2))\to p_{i,J}(x_2))$$

$$\underset{J\subseteq T}{\bigwedge }\forall x_2((\underset{j\in J}{\bigwedge }{q}_j(x_2))\to q_J(x_2))$$

$$\underset{i=1}{\overset{s}{\bigwedge }}\underset{J\subseteq T}{\bigwedge }\forall x_1\left(p_{i,J}(x_1)\to \exists x_2{\left({\Gamma }_i\cup \Omega \cup \bigcup \{{\Delta }_j\mid j\in J\}\right)}^{\circ }\right)$$

$$\underset{J\subseteq T}{\bigwedge }\forall x_1\left(q_J(x_1)\to \forall x_2{\left(\Omega \cup \bigcup \{{\Delta }_j\mid j\in J\}\right)}^{\circ }\right).$$

$$\underset{i=1}{\overset{s}{\bigwedge }}\underset{J\subseteq T}{\bigwedge }\forall x_1\cdots \forall x_{m-1}(({\alpha }_i\wedge \underset{j\in J}{\bigwedge }{\beta }_j)\to p_{i,J}(x_2,\dots ,x_{m-1}))$$

$$\underset{J\subseteq T}{\bigwedge }\forall x_1\cdots \forall x_{m-1}((\underset{j\in J}{\bigwedge }{\beta }_j)\to q_J(x_2,\dots ,x_{m-1}))$$

$$\underset{i=1}{\overset{s}{\bigwedge }}\underset{J\subseteq T}{\bigwedge }\forall x_2\cdots \forall x_{m-1}(p_{i,J}(x_2,\dots ,x_{m-1})\to \exists x_m({\Gamma }_i\cup \Omega \cup \bigcup _{j\in J}{\Delta }_j{)}^{\circ })$$

$$\underset{J\subseteq T}{\bigwedge }\forall x_2\cdots \forall x_{m-1}(q_J(x_2,\dots ,x_{m-1})\to \forall x_m(\Omega \cup \bigcup _{j\in J}{\Delta }_j{)}^{\circ }).$$

$$\underset{0\le i,j\le 3}{\bigwedge }\forall x(c_{ij}(x)\to \forall y((b(x,y)\vee r(x,y))\wedge c_{ij}(y)\to x=y))$$

$$\forall x(c_{ij}(x)$$

$$\forall x(c_{i+1,j}(x)$$

$$\forall x(c_{i+1,j+1}(x)$$

$$\forall x(c_{i,j+1}(x)$$

$$\forall x(c_{ij}(x)$$

$$\forall x(c_{i+1,j}(x)$$

$$\forall x(c_{i+1,j+1}(x)$$

$$\forall x(c_{i,j+1}(x)$$

$$\underset{i=0,2}{\bigwedge }\forall x(c_{ii}(x)\to$$

$$\underset{i=1,3}{\bigwedge }\forall x(c_{ii}(x)\to$$

$$\underset{i=0,2}{\bigwedge }\forall x(c_{i,i+1}(x)\to$$

$$\underset{i=1,3}{\bigwedge }\forall x(c_{i,i-1}(x)\to$$

$$\underset{i=0,2}{\bigwedge }\forall x(c_{ii}(x)\to$$

Full text

1 Introduction

The fluted fragment, here denoted ${\mathcal{FL}}$, is a fragment of first-order logic in which, roughly speaking, the order of quantification of variables coincides with the order in which those variables appear as arguments of predicates. The allusion is presumably architectural: we are invited to think of arguments of predicates as being ‘lined up’ in columns. The following formulas are sentences of ${\mathcal{FL}}$

[TABLE]

with the ‘lining up’ of variables illustrated in Fig. 1. By contrast, none of the formulas

[TABLE]

expressing, respectively, the reflexivity, symmetry and transitivity of the relation $r$, is fluted, as the atoms involved cannot be arranged so that their argument sequences ‘line up’ in the fashion of Fig. 1.

The history of this fragment is somewhat tortuous. The basic idea of fluted logic can be traced to a paper given by W.V. Quine to the 1968 International Congress of Philosophy [19], in which the author defined the homogeneous $m$-adic formulas. Quine later relaxed this fragment, in the context of a discussion of predicate-functor logic, to what he called ‘fluted’ quantificational schemata [20], claiming that the satisfiability problem for the relaxed fragment is decidable. The viability of the proof strategy sketched by Quine was explicitly called into question by Noah [12], and the subject then taken up by W.C. Purdy [17], who gave his own definition of ‘fluted formulas’, proving decidability. It is questionable whether Purdy’s reconstruction is faithful to Quine’s intentions: the matter is clouded by differences in the definitions of predicate functors between between [12] and [20], both of which Purdy cites. In fact, Quine’s original definition of ‘fluted’ quantificational schemata appears to coincide with a logic introduced—apparently independently—by A. Herzig [4]. Rightly of wrongly, however, the name ‘fluted fragment’ has now attached itself to Purdy’s definition in [17]; and we shall continue to use it in that way in the present article. See Sec. 2 for a formal definition.

To complicate matters further, Purdy claimed in [18] that ${\mathcal{FL}}$ (i.e. the fluted fragment, in our sense, and his) has the exponential-sized model property: if a fluted formula $\varphi$ is satisfiable, then it is satisfiable over a domain of size bounded by an exponential function of the number of symbols in $\varphi$. Purdy concluded that the satisfiability problem for ${\mathcal{FL}}$ is NExpTime-complete. These latter claims are false. It was shown in [15] that, although ${\mathcal{FL}}$ has the finite model property, there is no elementary bound on the sizes of the models required, and the satisfiability problem for ${\mathcal{FL}}$ is non-elementary. More precisely, define ${\mathcal{FL}}^{m}$ to be the subfragment of ${\mathcal{FL}}$ in which at most $m$ variables (free or bound) appear. Then the satisfiability problem for ${\mathcal{FL}}^{m}$ is $\lfloor m/2\rfloor$-NExpTime-hard for all $m\geq 2$ and in $(m-2)$-NExpTime for all $m\geq 3$ [16]. It follows that the satisfiability problem for ${\mathcal{FL}}$ is Tower-complete, in the framework of [21]. These results fix the exact complexity of satisfiability of ${\mathcal{FL}}^{m}$ for small values of $m$. Indeed, the satisfiability problem for $\mbox{\rm FO}^{2}$, the two-variable fragment of first-order logic, is known to be NExpTime-complete [3], whence the corresponding problem for ${\mathcal{FL}}^{2}$ is certainly in NExpTime. Moreover, for $0\leq m\leq 1$, ${\mathcal{FL}}^{m}$ coincides with the $m$-variable fragment of first-order logic, whence its satisfiability problem is NPTime-complete. Thus, taking [math]-NExpTime to mean NPTime, we see that the satisfiability problem for ${\mathcal{FL}}^{m}$ is $\lfloor m/2\rfloor$-NExpTime-complete, at least for $m\leq 4$.

The focus of the present paper is what happens when we add to the fluted fragment the ability to stipulate that certain designated binary relations are transitive, or are equivalence relations. The motivation comes from analogous results obtained for other decidable fragments of first-order logic. Consider basic propositional modal logic K. Under the standard translation into first-order logic (yielded by Kripke semantics), we can regard K as a fragment of first-order logic—indeed as a fragment of ${\mathcal{FL}}^{2}$. From basic modal logic K, we obtain the logic K4 under the supposition that the accessibility relation on possible worlds is transitive, and the logic S5 under the supposition that it is an equivalence relation: it is well-known that the satisfiability problems for K and K4 are PSpace-complete, whereas that for S5 is NPTime-complete [11]. (For analogous results on graded modal logic, see [5].) Closely related are also description logics (cf. [1]) with role hierarchies and transitive roles. In particular, the description logic $\mathcal{SH}$, which has the finite model property, is an ExpTime-complete fragment of ${\mathcal{FL}}$ with transitivity. Similar investigations have been carried out in respect of $\mbox{\rm FO}^{2}$, which has the finite model property and whose satisfiability problem, as just mentioned, is NExpTime-complete. The finite model property is lost when one transitive relation or two equivalence relations are allowed. For equivalence, everything is known: the (finite) satisfiability problem for $\mbox{\rm FO}^{2}$ in the presence of a single equivalence relation remains NExpTime-complete, but this increases to 2-NExpTime-complete in the presence of two equivalence relations [7, 8], and becomes undecidable with three. For transitivity, we have an incomplete picture: the finite satisfiability problem for $\mbox{\rm FO}^{2}$ in the presence with a single transitive relation in decidable in 3-NExpTime [14], while the decidability of the satisfiability problem remains open (cf. [24]); the corresponding problems with two transitive relations are both undecidable [9].

Adding equivalence relations to the fluted fragment poses no new problems. Existing results on of $\mbox{\rm FO}^{2}$ with two equivalence relations can be used to show that the satisfiability and finite satisfiability problems for ${\mathcal{FL}}$ (not just ${\mathcal{FL}}^{2}$) with two equivalence relations are decidable. Furthermore, the proof that the corresponding problems for $\mbox{\rm FO}^{2}$ in the presence of three equivalence relations are undecidable can easily be seen to apply also to ${\mathcal{FL}}^{2}$. On the other hand, the situation with transitivity is much less clear. In particular, it is not known to the present authors whether the description logic $\mathcal{SHI}$, the extension of $\mathcal{SH}$ where also role inverses can be used (a feature not expressible in ${\mathcal{FL}}$), enjoys the finite model property. Some indication that flutedness interacts in interesting ways with transitivity is provided by known complexity results on various extensions of guarded two-variable fragment with transitive relations. The guarded fragment, denoted GF, is that fragment of first-order logic in which all quantification is of either of the forms $\forall\bar{v}(\alpha\rightarrow\psi)$ or $\exists\bar{v}(\alpha\wedge\psi)$, where $\alpha$ is an atomic formula (a so-called guard) featuring all free variables of $\psi$. The guarded two-variable fragment, denoted $\mbox{\rm GF}^{2}$, is the intersection of GF and $\mbox{\rm FO}^{2}$. It is straightforward to show that the addition of two transitive relations to $\mbox{\rm GF}^{2}$ yields a logic whose satisfiability problem is undecidable. However, as long as the distinguished transitive relations appear only in guards, we can extend the whole of GF with any number of transitive relations, yielding the so-called guarded fragment with transitive guards, whose satisfiability problem is in 2-ExpTime [23]. Intriguingly, in the two-variable case, we obtain a reduction in complexity if we require transitive relations in guards to point forward—i.e. allowing only $\forall v(t(u,v)\rightarrow\psi)$ rather than $\forall v(t(v,u)\rightarrow\psi)$, and similarly for existential quantification. Thus, the extension of $\mbox{\rm GF}^{2}$ with (any number of) transitive guards has a 2-ExpTime-complete satisfiability problem; however, the corresponding problem under the restriction to one-way transitive guards is ExpSpace-complete [6]. Since the above-mentioned extensions of $\mbox{\rm GF}^{2}$ also do not enjoy the finite model property, the satisfiability and the finite satisfiability problems do not coincide. Decidability and complexity bounds for the finite satisfiability problems are shown in [9, 10].

We show in the sequel that ${\mathcal{FL}}$ in the presence of a single transitive relation has the finite model property. On the other hand, the satisfiability problems for ${\mathcal{FL}}$ in the presence of three transitive relations are undecidable even for the intersection of ${\mathcal{FL}}$ with $\mbox{\rm GF}^{2}$. (Indeed, the same holds even when one of these transitive relations is constrained to be the identity.) The status of the decidability of ${\mathcal{FL}}$ with just two transitive relations remains open.

2 Preliminaries

Unless explicitly stated to the contrary, the fragments of first-order logic considered here do not contain equality. We employ purely relational signatures, i.e. no individual constants or function symbols. We do, however, allow 0-ary relations (proposition letters).

Let $\bar{x}_{\omega}=x_{1},x_{2},\ldots$ be a fixed sequence of variables. We define the sets of formulas ${\mathcal{FL}}^{[m]}$ (for $m\geq 0$) by structural induction as follows: (i) any atom $\alpha(x_{\ell},\ldots,x_{m})$, where $x_{\ell},\dots,x_{m}$ is a contiguous subsequence of $\bar{x}_{\omega}$, is in ${\mathcal{FL}}^{[m]}$; (ii) ${\mathcal{FL}}^{[m]}$ is closed under boolean combinations; (iii) if $\varphi$ is in ${\mathcal{FL}}^{[m+1]}$, then $\exists x_{m+1}\varphi$ and $\forall x_{m+1}\varphi$ are in ${\mathcal{FL}}^{[m]}$. The set of fluted formulas is defined as ${\mathcal{FL}}=\bigcup_{m\geq 0}{\mathcal{FL}}^{[m]}$. A fluted sentence is a fluted formula with no free variables. Thus, when forming Boolean combinations in the fluted fragment, all the combined formulas must have as their free variables some suffix of some prefix $x_{1},\dots,x_{m}$ of $\bar{x}_{\omega}$; and, when quantifying, only the last variable in this sequence may be bound. Note also that proposition letters (0-ary predicates) may, according to the above definitions, be combined freely with formulas: if $\varphi$ is in ${\mathcal{FL}}^{[m]}$, then so, for example, is $\varphi\wedge P$, where $P$ is a proposition letter.

Denote by ${\mathcal{FL}}^{m}$ the sub-fragment of ${\mathcal{FL}}$ consisting of those formulas featuring at most $m$ variables, free or bound. Do not confuse ${\mathcal{FL}}^{m}$ (the set of fluted formulas with at most $m$ variables, free or bound) with ${\mathcal{FL}}^{[m]}$ (the set of fluted formulas with free variables $x_{\ell},\dots,x_{m}$). These are, of course, quite different. For example, (3) is in ${\mathcal{FL}}^{2}$, and (6) is in ${\mathcal{FL}}^{3}$, but they are both in ${\mathcal{FL}}^{[0]}$. Note that ${\mathcal{FL}}^{m}$ cannot include predicates of arity greater than $m$.

For $m\geq 2$, denote by ${\mathcal{FL}^{m}{k}\mbox{\rm T}}$ the $m$-variable fluted fragment ${\mathcal{FL}}^{m}$ together with $k$ distinguished transitive relations. In addition, denote by ${\mathcal{FL}^{2}{k}\mbox{\rm T}^{\/u}}$ the sub-fragment of ${\mathcal{FL}^{2}{k}\mbox{\rm T}}$ in which no binary predicates occur except the $k$ distinguished transitive ones.

3 The decidability of fluted logic with one transitive relation

In this section, we show that the logic ${\mathcal{FL}1\mbox{\rm T}}$, the fluted fragment together with a single distinguished transitive relation $\mathfrak{t}$, has the finite model property. We proceed in stages. First, we show that ${\mathcal{FL}^{2}1\mbox{\rm T}^{\/u}}$ has a doubly exponential-sized model property. Next, we show that ${\mathcal{FL}^{2}1\mbox{\rm T}}$ has a triply exponential-sized model property, via an exponential-sized reduction to ${\mathcal{FL}^{2}1\mbox{\rm T}^{\/u}}$. Finally, for $m\geq 2$, we provide an exponential-sized reduction of the satisfiability problem for ${\mathcal{FL}^{m+1}1\mbox{\rm T}}$ to the corresponding problem for ${\mathcal{FL}^{m}1\mbox{\rm T}}$, showing that, if the target of the reduction has a model of size $N$, then the source has a model of size $O(2^{N})$. The satisfiability problems considered here will all have at least exponential complexity. Therefore, we may assume without loss of generality in this section that all signatures feature no 0-ary predicates, since their truth values can simply be guessed.

3.1 The logic ${\mathcal{FL}^{2}1\mbox{\rm T}^{\/u}}$

Fix some signature $\Sigma$ of unary predicates. We consider ${\mathcal{FL}^{2}1\mbox{\rm T}^{\/u}}$-formulas over the signature $\Sigma\cup\{\mathfrak{t}\}$, where $\mathfrak{t}$ is the distinguished transitive predicate. (Thus, $\mathfrak{t}\not\in\Sigma$.) By a 1-type over $\Sigma$, we mean a maximal consistent conjunction of literals $\pm p(x)$, where $p\in\Sigma$. If $\mathfrak{A}$ is a structure interpreting $\Sigma\cup\{\mathfrak{t}\}$, any element $a\in A$ satisfies a unique 1-type over $\Sigma$; we denote it $\mbox{\rm tp}^{\mathfrak{A}}[a]$. Since $\Sigma$ will not vary, we typically omit reference to it when speaking of 1-types. We use the letters $\pi$ and $\pi^{\prime}$ always to range over 1-types and $\mu$ always to range over arbitrary quantifier-free $\Sigma$-formulas involving just the variable $x$. We write $\pi(y)$ to indicate the result of substituting $y$ everywhere for $x$ in $\pi$, and similarly for $\pi^{\prime}$ and $\mu$.

Call a ${\mathcal{FL}^{2}1\mbox{\rm T}^{\/u}}$-formula over $\Sigma\cup\{\mathfrak{t}\}$ basic if it is of one of the forms

[TABLE]

The following Lemma is a version of the familiar ‘Scott normal form’ for ${\mathcal{FL}}^{2}$ from [22].

Lemma 3.1**.**

Let $\varphi$ be a ${\mathcal{FL}^{2}1\mbox{\rm T}^{\/u}}$-sentence. There exists a set $\Psi$ of basic ${\mathcal{FL}^{2}1\mbox{\rm T}^{\/u}}$-formulas with the following properties: (i) $\models\left(\bigwedge\Psi\right)\rightarrow\varphi$; (ii) if $\varphi$ has a model, then so has $\Psi$; (iii) $|\!|\Psi|\!|$ is bounded by a polynomial function of $|\!|\varphi|\!|$.

We say that a super-type over $\Sigma$ is a pair $\langle\pi,\Pi\rangle$, where $\pi$ is a 1-type over $\Sigma$ and $\Pi$ a set of 1-types over $\Sigma$. If $\mathfrak{A}$ is a structure interpreting the signature $\Sigma\cup\{\mathfrak{t}\}$ and $a\in A$, the super-type of $a$ in $\mathfrak{A}$, denoted $\mbox{\rm stp}^{\mathfrak{A}}[a]$, is the pair $\langle\mbox{\rm tp}^{\mathfrak{A}}[a],\Pi\rangle$, where $\Pi=\{\mbox{\rm tp}^{\mathfrak{A}}[b]\mid\mathfrak{A}\models\mathfrak{t}[a,b]\}$. Intuitively, a super-type is a description of an element in a structure specifying that element’s 1-type together with the 1-types of those elements to which it is related by $\mathfrak{t}$. If $S$ is a set of super-types, we write $\mbox{\rm tp}(S)=\{\pi\mid\langle\pi,\Pi\rangle\in S\mbox{ for some }\Pi\}$. Since $\Sigma$ will not vary, we again omit reference to it when speaking of super-types. By a certificate, we mean a pair $C=(S,\ll)$, where $S$ is a set of super-types and $\ll$ is a transitive relation on $\mbox{\rm tp}(S)$ satisfying the following conditions:

(C1)

if $\langle\pi,\Pi\rangle\in S$ and $\pi^{\prime}\in\Pi$, then there exists $\langle\pi^{\prime},\Pi^{\prime}\rangle\in S$ with $\Pi^{\prime}\subseteq\Pi$;

(C2)

if $\pi\ll\pi^{\prime}$, $\langle\pi,\Pi\rangle\in S$ and $\langle\pi^{\prime},\Pi^{\prime}\rangle\in S$, then $\{\pi^{\prime}\}\cup\Pi^{\prime}\subseteq\Pi$.

If $\mathfrak{A}$ is a structure, then the certificate of $\mathfrak{A}$, denoted $C(\mathfrak{A})$, is the pair $(S,\ll)$, where $S=\{\mbox{\rm stp}^{\mathfrak{A}}[a]\mid a\in A\}$ is the set of super-types realized in $\mathfrak{A}$, and $\pi\ll\pi^{\prime}$ if and only if $\pi$ and $\pi^{\prime}$ are realized in $\mathfrak{A}$ and $\mathfrak{A}\models\forall x(\pi\rightarrow\forall y(\pi^{\prime}(y)\rightarrow\mathfrak{t}(x,y)))$. Intuitively, a certificate is a description of a structure listing the realized super-types and containing a partial order which specifies when all elements realizing one 1-type are related by $\mathfrak{t}$ to all elements realizing another 1-type.

Lemma 3.2**.**

If $\mathfrak{A}$ is any structure interpreting $\Sigma\cup\{\mathfrak{t}\}$, $C(\mathfrak{A})$ is a certificate.

Proof 3.3**.**

Write $C(\mathfrak{A})=(S,\ll)$. Obviously $\ll$ is transitive. We must check (C1) and (C2).

(C1): Suppose $\langle\pi,\Pi\rangle\in S$ and $\pi^{\prime}\in\Pi$. Let $a$ be such that $\mbox{\rm stp}^{\mathfrak{A}}[a]=\langle\pi,\Pi\rangle$. Then there exists a $b\in A$ such that $\mbox{\rm tp}^{\mathfrak{A}}[b]=\pi^{\prime}$ and $\mathfrak{A}\models\mathfrak{t}[a,b]$. Let $\mbox{\rm stp}^{\mathfrak{A}}[b]=\langle\pi^{\prime},\Pi^{\prime}\rangle$.

(C2): Suppose $\langle\pi,\Pi\rangle\in S$ and $\langle\pi^{\prime},\Pi^{\prime}\rangle\in S$ with $\pi\ll\pi^{\prime}$, and let $a,b\in A$ be such that $\mbox{\rm stp}^{\mathfrak{A}}[a]=\langle\pi,\Pi\rangle$ and $\mbox{\rm stp}^{\mathfrak{A}}[b]=\langle\pi^{\prime},\Pi^{\prime}\rangle$. Since $\pi\ll\pi^{\prime}$, by construction of $C(\mathfrak{A})$, we have $\mathfrak{A}\models\forall x(\pi\rightarrow\forall y(\pi^{\prime}(y)\rightarrow\mathfrak{t}(x,y)))$, whence it is immediate that $\pi^{\prime}\in\Pi$ and $\Pi^{\prime}\subseteq\Pi$.

If $C=(S,\ll)$ is a certificate, and $\psi$ a basic ${\mathcal{FL}^{2}1\mbox{\rm T}^{\/u}}$-formula, we define the relation $C\models\psi$ to hold provided the following six conditions are satisfied. The motivation for this definition is provided by Lemmas 3.4 and 3.6.

1. (i)

if $\psi$ is of the form $\forall x(\pi\rightarrow\exists y(\mu(y)\wedge\mathfrak{t}(x,y)))$, then, for all $\Pi$ such that $\langle\pi,\Pi\rangle\in S$, there exists $\pi^{\prime}\in\Pi$ such that $\models\pi^{\prime}\rightarrow\mu$; 2. (ii)

if $\psi$ is of the form $\forall x(\pi\rightarrow\forall y(\pi^{\prime}(y)\rightarrow\mathfrak{t}(x,y)))$ and $\pi,\pi^{\prime}\in\mbox{\rm tp}(S)$, then $\pi\ll\pi^{\prime}$; 3. (iii)

if $\psi$ is of the form $\forall x(\pi\rightarrow\exists y(\mu(y)\wedge\neg\mathfrak{t}(x,y)))$, then, for all $\langle\pi,\Pi\rangle\in S$, there exists $\langle\pi^{\prime},\Pi^{\prime}\rangle\in S$ such that $\models\pi^{\prime}\rightarrow\mu$ and there exists no $\alpha\in\{\pi\}\cup\Pi$ such that $\alpha\ll\pi^{\prime}$; 4. (iv)

if $\psi$ is of the form $\forall x(\pi\rightarrow\forall y(\pi^{\prime}(y)\rightarrow\neg\mathfrak{t}(x,y)))$, then, for all $\langle\pi,\Pi\rangle\in S$, $\pi^{\prime}\not\in\Pi$; 5. (v)

if $\psi$ is of the form $\exists x.\mu$, then there exists $\langle\pi,\Pi\rangle\in S$ such that $\models\pi\rightarrow\mu$; 6. (vi)

if $\psi$ is of the form $\forall x.\mu$, then, for all $\langle\pi,\Pi\rangle\in S$, $\models\pi\rightarrow\mu$.

Lemma 3.4**.**

Let $\mathfrak{A}$ be a structure interpreting $\Sigma\cup\{\mathfrak{t}\}$ and let $\psi$ be a basic ${\mathcal{FL}^{2}1\mbox{\rm T}^{\/u}}$-formula over $\Sigma\cup\{\mathfrak{t}\}$. If $\mathfrak{A}\models\psi$, then $C(\mathfrak{A})\models\psi$.

Proof 3.5**.**

We write $C(\mathfrak{A})=(S,\ll)$ and consider the possible forms of $\psi$ in turn.

• •

$\psi=\forall x(\pi\rightarrow\exists y(\mu(y)\wedge\mathfrak{t}(x,y)))$: Suppose $\langle\pi,\Pi\rangle\in S$. Then there exists $a\in A$ with $\mbox{\rm stp}^{\mathfrak{A}}[a]=\langle\pi,\Pi\rangle$. Since $\mathfrak{A}\models\psi$, choose $b\in A$ such that $\mathfrak{A}\models\mu[b]$ and $\mathfrak{A}\models\mathfrak{t}[a,b]$, and let $\mbox{\rm tp}^{\mathfrak{A}}[b]=\pi^{\prime}$. Then $\models\pi^{\prime}\rightarrow\mu$ and $\pi^{\prime}\in\Pi$, as required.

• •

$\psi=\forall x(\pi\rightarrow\forall y(\pi^{\prime}(y)\rightarrow\mathfrak{t}(x,y)))$: It is immediate by the construction of $C(\mathfrak{A})$ that, if $\pi,\pi^{\prime}\in\mbox{\rm tp}(S)$, then $\pi\ll\pi^{\prime}$;

• •

$\psi=\forall x(\pi\rightarrow\exists y(\mu(y)\wedge\neg\mathfrak{t}(x,y)))$: Suppose $\langle\pi,\Pi\rangle\in S$. Then there exists $a\in A$ with $\mbox{\rm stp}^{\mathfrak{A}}[a]=\langle\pi,\Pi\rangle$. Since $\mathfrak{A}\models\psi$, choose $b\in A$ such that $\mathfrak{A}\models\mu[b]$ and $\mathfrak{A}\not\models\mathfrak{t}[a,b]$, and let $\mbox{\rm tp}^{\mathfrak{A}}[b]=\pi^{\prime}$, so that $\models\pi^{\prime}\rightarrow\mu$. We require only to show that there exists no $\alpha\in\{\pi\}\cup\Pi$ such that $\alpha\ll\pi^{\prime}$. Suppose, for contradiction, that such an $\alpha$ exists. By (C1), $\alpha\in\mbox{\rm tp}(S)$. If $\alpha=\pi$, then, by the definition of $\ll$, we have $\mathfrak{A}\models\forall x(\pi\rightarrow\forall y(\pi^{\prime}(y)\rightarrow\mathfrak{t}(x,y)))$, which contradicts the supposition that $\mathfrak{A}\not\models\mathfrak{t}[a,b]$. If $\alpha\in\Pi$, then, by the definition of $\Pi$ and $\ll$, we have an element $a^{\prime}\in A$ such that $\mbox{\rm tp}^{\mathfrak{A}}[a^{\prime}]=\alpha$, $\mathfrak{A}\models\mathfrak{t}[a,a^{\prime}]$ and $\mathfrak{A}\models\forall x(\alpha\rightarrow\forall y(\pi^{\prime}(y)\rightarrow\mathfrak{t}(x,y)))$, which again contradicts the supposition that $\mathfrak{A}\not\models\mathfrak{t}[a,b]$.

• •

$\psi=\forall x(\pi\rightarrow\forall y(\pi^{\prime}(y)\rightarrow\neg\mathfrak{t}(x,y)))$: Suppose $\langle\pi,\Pi\rangle\in S$ and let $a\in A$ be such that $\mbox{\rm stp}^{\mathfrak{A}}[a]=\langle\pi,\Pi\rangle$. Since $\mathfrak{A}\models\psi$, we have $\pi^{\prime}\not\in\Pi$.

• •

$\psi=\exists x.\mu$* or $\psi=\forall x.\mu$. Immediate by construction of $S$.*

Lemma 3.6**.**

If $C=(S,\ll)$ is a certificate, then there exists a structure $\mathfrak{A}$ over a domain of cardinality $2|S|$ such that, for any basic ${\mathcal{FL}^{2}1\mbox{\rm T}^{\/u}}$-formula $\psi$ over $\Sigma$, $C\models\psi$ implies $\mathfrak{A}\models\psi$.

Proof 3.7**.**

Define $A^{+}=\{a^{+}_{\pi,\Pi}\mid\langle\pi,\Pi\rangle\in S\}$ and $A^{-}=\{a^{-}_{\pi,\Pi}\mid\langle\pi,\Pi\rangle\in S\}$, where the various $a^{+}_{\pi,\Pi}$ and $a^{-}_{\pi,\Pi}$ are some objects (assumed distinct), and set $A=A^{+}\cup A^{-}$. Define the binary relations $T_{1}=\{\langle a^{\pm}_{\pi,\Pi},a^{+}_{\pi^{\prime},\Pi^{\prime}}\rangle\mid\{\pi^{\prime}\}\cup\Pi^{\prime}\subseteq\Pi\}$ and $T_{2}=\{\langle a^{\pm}_{\pi,\Pi},a^{\pm}_{\pi^{\prime},\Pi^{\prime}}\rangle\mid\pi\ll\pi^{\prime}\}$, and let $T$ be the transitive closure of $T_{1}\cup T_{2}$. Intuitively, we may think of the elements $a^{+}_{\pi^{\prime},\Pi^{\prime}}$ as witnessing existential formulas of the form $\exists y(\mu(y)\wedge\mathfrak{t}(x,y))$, where $\models\pi^{\prime}\rightarrow\mu$, and of the elements $a^{-}_{\pi^{\prime},\Pi^{\prime}}$ as witnessing existential formulas of the form $\exists y(\mu(y)\wedge\neg\mathfrak{t}(x,y))$. Now define $\mathfrak{A}$ on the domain $A$ by setting $\mbox{\rm tp}^{\mathfrak{A}}[a^{\pm}_{\pi,\Pi}]=\pi$ for all $\langle\pi,\Pi\rangle\in S$, and by setting $\mathfrak{t}^{\mathfrak{A}}=T$.

We observe that if $a=a^{\pm}_{\pi,\Pi}$ and $b=a^{\pm}_{\pi^{\prime},\Pi^{\prime}}$ are elements of $A$ such that $a$ is related to $b$ by either $T_{1}$ or $T_{2}$, then $\{\pi^{\prime}\}\cup\Pi^{\prime}\subseteq\Pi$. Indeed, for $T_{1}$, this is immediate by definition; and for $T_{2}$, it follows from property (C2) of certificates. It follows by induction that, if $a$ is related to $b$ by $T$, then $\{\pi^{\prime}\}\cup\Pi^{\prime}\subseteq\Pi$. To prove the lemma, we consider the possible forms of $\psi$ in turn.

• •

$\psi=\forall x(\pi\rightarrow\exists y(\mu(y)\wedge\mathfrak{t}(x,y)))$: Suppose $a=a^{\pm}_{\pi,\Pi}$. Since $C\models\psi$, there exists $\pi^{\prime}\in\Pi$ such that $\pi^{\prime}\rightarrow\mu$. By (C1), there exists $\langle\pi^{\prime},\Pi^{\prime}\rangle\in S$ such that $\Pi^{\prime}\subseteq\Pi$. Letting $b=a^{+}_{\pi^{\prime},\Pi^{\prime}}$, we have that $a$ is related to $b$ by $T_{1}$. But then $\mathfrak{A}\models\mathfrak{t}[a,b]$ and $\mathfrak{A}\models\mu[b]$ by construction of $\mathfrak{A}$.

• •

$\psi=\forall x(\pi\rightarrow\forall y(\pi^{\prime}(y)\rightarrow\mathfrak{t}(x,y)))$: Since $C\models\psi$, we have $\pi\ll\pi^{\prime}$. Suppose now $a=a^{\pm}_{\pi,\Pi}$ and $b=a^{\pm}_{\pi^{\prime},\Pi^{\prime}}$. Thus, $a$ is related to $b$ by $T_{2}$, and so by construction of $\mathfrak{A}$, $\mathfrak{A}\models\mathfrak{t}[a,b]$.

• •

$\psi=\forall x(\pi\rightarrow\exists y(\mu(y)\wedge\neg\mathfrak{t}(x,y)))$: Suppose $a=a^{\pm}_{\pi,\Pi}$. Since $C\models\psi$, there exists $\langle\pi^{\prime},\Pi^{\prime}\rangle\in S$ such that $\pi^{\prime}\rightarrow\mu$, and such that there is no $\alpha\in\{\pi\}\cup\Pi$ with $\alpha\ll\pi^{\prime}$. Now let $b=a^{-}_{\pi^{\prime},\Pi^{\prime}}$. By construction of $\mathfrak{A}$, $\mathfrak{A}\models\mu[b]$. It suffices to show that $\mathfrak{A}\not\models\mathfrak{t}[a,b]$. For otherwise, by the definition of $T$, there exists a chain of elements $a=a_{1},\dots,a_{m}=b$ with each related to the next by either $T_{1}$ or $T_{2}$ and with $a_{m-1}$ related to $a_{m}$ by $T_{2}$. (Notice that nothing can be related by $T_{1}$ to $b=a^{-}_{\pi^{\prime},\Pi^{\prime}}$.) Writing $a_{m-1}=a^{\pm}_{\alpha,\Pi^{\prime\prime}}\in S$, we see that $\alpha\ll\pi^{\prime}$, and, moreover, that $a$ is either identical to $a_{m-1}$, or related to it by $T$. As we observed above, if $a^{\pm}_{\pi,\Pi}$ is related to $a^{\pm}_{\alpha,\Pi^{\prime\prime}}$ by $T$, then $\alpha\in\Pi$. Thus, either way, $\alpha\in\{\pi\}\cup\Pi$. But we are supposing that no such $\alpha$ exists.

• •

$\psi=\forall x(\pi\rightarrow\forall y(\pi^{\prime}(y)\rightarrow\neg\mathfrak{t}(x,y)))$: Suppose $a=a^{\pm}_{\pi,\Pi}$ and $b=a^{\pm}_{\pi^{\prime},\Pi^{\prime}}$ are elements of $A$. We observed above that, if $a$ is related to $b$ by $T$, then $\pi^{\prime}\in\Pi$, contradicting the assumption that $C\models\psi$. Thus, by construction of $\mathfrak{A}$, $\mathfrak{A}\not\models\mathfrak{t}[a,b]$.

• •

$\psi=\exists x.\mu$* or $\psi=\forall x.\mu$. Immediate by construction of $\mathfrak{A}$.*

Since the number of super-types over $\Sigma$ is bounded by $2^{(2^{|\Sigma|}+|\Sigma|)}$, Lemmas 3.1–3.6 yield:

Lemma 3.8**.**

If $\varphi$ is a satisfiable formula of ${\mathcal{FL}^{2}1\mbox{\rm T}^{\/u}}$, then $\varphi$ has a model of size at most doubly exponential in $|\!|\varphi|\!|$. Hence the satisfiability problem for ${\mathcal{FL}^{2}1\mbox{\rm T}^{\/u}}$ is in $2\textsc{-NExpTime}$.

Proof 3.9**.**

A structure $\mathfrak{A}$ can be guessed and verified to be a model of any $m$-variable first-order formula $\varphi$ in time $O(|\varphi|\cdot|A|^{m})$ [26].

3.2 The logics ${\mathcal{FL}^{m}1\mbox{\rm T}}$ for $m\geq 2$

Let $\Sigma$ be a signature of predicates of positive arity, excluding $\mathfrak{t}$. An atomic formula of ${\mathcal{FL}^{m}1\mbox{\rm T}}$ involving a predicate from $\Sigma\cup\{\mathfrak{t}\}$ will be called a fluted $m$-atom over $\Sigma\cup\{\mathfrak{t}\}$. A fluted $m$-literal is a fluted $m$-atom or the negation thereof. A fluted $m$-clause is a disjunction of fluted $m$-literals. We allow the absurd formula $\bot$ (i.e. the empty disjunction) to count as a fluted $m$-clause. Thus, any literal of a fluted $m$-clause has arguments $x_{h},\dots,x_{m}$, in that order, for some $h$ ($1\leq h\leq m)$. When writing fluted $m$-clauses, we silently remove bracketing, re-order literals and delete duplicated literals as necessary. A fluted $m$-type is a maximal consistent set of fluted $m$-literals; where convenient, we identify fluted $m$-types with their conjunctions. If $\mathfrak{A}$ is a structure interpreting $\Sigma\cup\{\mathfrak{t}\}$, any tuple $a_{1},\dots,a_{m}$ from $A$ satisfies a unique fluted $m$-type; we denote it $\mbox{\rm ftp}^{\mathfrak{A}}[a_{1},\dots,a_{m}]$. Note that a fluted 1-type over $\Sigma\cup\{\mathfrak{t}\}$ coincides with what we earlier called a 1-type over $\Sigma$. Reference to the signature $\Sigma\cup\{\mathfrak{t}\}$ will as usual be suppressed when clear from context. Predicates in $\Sigma$ will be referred to as non-distinguished. Our strategy will be to reduce the (finite) satisfiability problem for ${\mathcal{FL}^{m}1\mbox{\rm T}}$ to that for ${\mathcal{FL}^{2}1\mbox{\rm T}}$ (Lemma 3.16), and thence to that for ${\mathcal{FL}^{2}1\mbox{\rm T}^{\/u}}$ (Lemma 3.13), which we have already dealt with (Lemma 3.8).

A ${\mathcal{FL}^{m}1\mbox{\rm T}}$-formula $\varphi$ ($m\geq 2$) is in clause normal form if it is of the form

[TABLE]

where $\Omega,\Gamma_{1},\dots,\Gamma_{s},\Delta_{1},\dots,\Delta_{t}$ are sets of fluted $m$-clauses, and $\alpha_{1},\dots,\alpha_{s}$, $\beta_{1},\dots,\beta_{t}$ fluted $(m-1)$-atoms. We refer to $\forall x_{1}\cdots x_{m}.\Omega$ as the static conjunct of $\varphi$, to conjuncts of the form $\forall x_{1}\cdots x_{m-1}\left(\alpha_{i}\rightarrow\exists x_{m}\Gamma_{i}\right)$ as the existential conjuncts of $\varphi$, and to conjuncts of the form $\forall x_{1}\cdots x_{m-1}(\beta_{j}\rightarrow\forall x_{m}.\Delta_{j})$ as the universal conjuncts of $\varphi$.

Using the same techniques as for Lemma 3.1, we can transform any ${\mathcal{FL}^{m}1\mbox{\rm T}}$-formula into clause normal form.

Lemma 3.10**.**

Let $\varphi$ be an ${\mathcal{FL}^{m}1\mbox{\rm T}}$-formula, $m\geq 2$. There exists an ${\mathcal{FL}^{m}1\mbox{\rm T}}$-formula $\psi$ in clause normal form such that: (i) $\models\psi\rightarrow\varphi$; and (ii) if $\varphi$ has a model then so has $\psi$; (iii) $|\!|\psi|\!|$ is bounded by a polynomial function of $|\!|\varphi|\!|$.

For fragments of first-order logic not involving equality, we are free to duplicate any element $a$ in a structure $\mathfrak{A}$. More formally, we have the following lemma, which will be used as a step in the ensuing argument.

Lemma 3.11**.**

Let $\mathfrak{A}$ be any structure, and let $z>0$. There exists a structure $\mathfrak{B}$ such that (i) if $\varphi$ is any first-order formula without equality, then $\mathfrak{A}\models\varphi$ if and only if $\mathfrak{B}\models\varphi$; (ii) $|B|=z\cdot|A|$; and (iii) if $\psi(x_{1},\dots,x_{m-1})=\exists x_{m}.\chi(x_{1},\dots,x_{m})$ is a first-order formula without equality, and $\mathfrak{B}\models\psi[b_{1},\dots,b_{m-1}]$, then there exist at least $z$ distinct elements $b$ of $B$ such that $\mathfrak{B}\models\chi[b_{1},\dots,b_{m-1},b]$.

Keeping the signature $\Sigma$ fixed, we employ the standard apparatus of resolution theorem-proving to eliminate non-distinguished predicates of arity 2 or more. Suppose $p\in\Sigma$ is a predicate of arity $m$, and let $\gamma^{\prime}$ and $\delta^{\prime}$ be fluted $m$-clauses over $\Sigma$. Then, $\gamma=p(x_{1},\dots,x_{m})\vee\gamma^{\prime}$ and $\delta=\neg p(x_{1},\dots,x_{m})\vee\delta^{\prime}$ are also fluted $m$-clauses, as indeed is $\gamma^{\prime}\vee\delta^{\prime}$. In that case, we call $\gamma^{\prime}\vee\delta^{\prime}$ a fluted resolvent of $\gamma$ and $\delta$, and we say that $\gamma^{\prime}\vee\delta^{\prime}$ is obtained by fluted resolution from $\gamma$ and $\delta$ on $p(x_{1},\dots,x_{m})$. Thus, fluted resolution is simply a restriction of the familiar resolution rule from first-order logic to the case where the resolved-on literals have maximal arity, $m$, and (in the case $m=2$) do not feature the distinguished predicate $\mathfrak{t}$. It may be helpful to note the following at this point: (i) if $\gamma$ and $\delta$ resolve to form $\epsilon$, then $\models\forall x_{1}\cdots\forall x_{m}(\gamma\wedge\delta\rightarrow\epsilon)$; (ii) the fluted resolvent of two fluted $m$-clauses may or may not involve predicates of arity $m$; (iii) in fluted resolution, the arguments of the literals in the fluted $m$-clauses undergo no change when forming the resolvent; (iv) if the fluted $m$-clause $\gamma$ involves no predicates of arity $m$, then it cannot undergo fluted resolution at all.

If $\Gamma$ is a set of fluted $m$-clauses, denote by $\Gamma^{*}$ the smallest set of fluted $m$-clauses including $\Gamma$ and closed under fluted resolution. If $\Gamma=\Gamma^{*}$, we say that it is closed under fluted resolution. We further denote by $\Gamma^{\circ}$ the result of deleting from $\Gamma^{*}$ any clause involving a non-distinguished predicate of arity $m$. Observe that, since all fluted $m$-atoms involving predicates of non-maximal arity are of the form $p(x_{h},\dots,x_{m})$ for some $h\geq 2$, it follows that $\Gamma^{\circ}$ features the variable $x_{1}$ only in the case $m=2$, and even then only in literals of the form $\pm\mathfrak{t}(x_{1},x_{2})$.

The following lemma is, in effect, nothing more than the familiar completeness theorem for (ordered) propositional resolution. Due to space limits the proof is given in Section A.2.

Lemma 3.12**.**

Let $\Gamma$ be a set of fluted $m$-clauses over a signature $\Sigma\cup\{\mathfrak{t}\}$, let $\Sigma^{\prime}$ be the result of removing all predicates of maximal arity $m$ from $\Sigma$, and let $\tau^{-}$ be a fluted $m$-type over $\Sigma^{\prime}\cup\{\mathfrak{t}\}$. If $\tau^{-}$ is consistent with $\Gamma^{\circ}$, then there exists a fluted $m$-type $\tau$ over the signature $\Sigma\cup\{\mathfrak{t}\}$ such that $\tau\supseteq\tau^{-}$ and $\tau$ is consistent with $\Gamma$.

The following lemma employs a technique from [13] to eliminate binary predicates.

Lemma 3.13**.**

Let $\varphi$ be an ${\mathcal{FL}^{2}1\mbox{\rm T}}$-formula in clause normal form over a signature $\Sigma\cup\{\mathfrak{t}\}$, and suppose that $\varphi$ has $s$ existential and $t$ universal conjuncts. Then there exists a clause normal form ${\mathcal{FL}^{2}1\mbox{\rm T}^{\/u}}$-formula $\varphi^{\prime}$ over a signature $\Sigma^{\prime}\cup\{\mathfrak{t}\}$ such that: (i) $\varphi^{\prime}$ has at most $2^{t}s$ existential and $2^{t}$ universal conjuncts; (ii) $|\Sigma^{\prime}|\leq|\Sigma|+2^{t}(s+1)$; (iii) if $\varphi$ has a model, so does $\varphi^{\prime}$; and (iv) if $\varphi^{\prime}$ has a model of size $M$, then $\varphi$ has a model of size at most $sM$.

Proof 3.14**.**

*Let $\varphi=\forall x_{1}x_{2}.\Omega\ \wedge{\bigwedge_{i=1}^{s}}\forall x_{1}\left(p_{i}(x_{1})\rightarrow\exists x_{2}.\Gamma_{i}\right)\wedge{\bigwedge_{j=1}^{t}}\forall x_{1}(q_{j}(x_{1})\rightarrow\forall x_{2}.\Delta_{j})$, where $\Omega,\Gamma_{1},\dots,\Gamma_{s},\Delta_{1},\dots,\Delta_{t}$ are sets of fluted 2-clauses, and $p_{1},\dots,p_{s}$, $q_{1},\dots,q_{t}$ unary predicates. Write $T=\{1,\dots,t\}$. For all $i$ ($1\leq i\leq s$) and all $J\subseteq T$, let $p_{i,J}$ and $q_{J}$ be new unary predicates. The intended interpretation of $p_{i,J}(x_{1})$ is “$x_{1}$ satisfies $p_{i}$, and also satisfies $q_{j}$ for every $j\in J$;” and the intended interpretation of $q_{J}(x_{1})$ is “$x_{1}$ satisfies $q_{j}$ for every $j\in J$.” Let $\varphi^{\prime}$ be the conjunction of the sentences:

   (a) $\bigwedge_{i=1}^{s}\bigwedge_{J\subseteq T}\forall x_{2}((p_{i}(x_{2})\wedge\bigwedge_{j\in J}q_{j}(x_{2}))\rightarrow p_{i,J}(x_{2}))$,

   (b) $\bigwedge_{J\subseteq T}\forall x_{2}((\bigwedge_{j\in J}q_{j}(x_{2}))\rightarrow q_{J}(x_{2}))$,

   (c) $\bigwedge_{i=1}^{s}\bigwedge_{J\subseteq T}\forall x_{1}\left(p_{i,J}(x_{1})\rightarrow\exists x_{2}\left(\Gamma_{i}\cup\Omega\cup\bigcup\{\Delta_{j}\mid j\in J\}\right)^{\circ}\right)$, and

   (d) $\bigwedge_{J\subseteq T}\forall x_{1}\left(q_{J}(x_{1})\rightarrow\forall x_{2}\left(\Omega\cup\bigcup\{\Delta_{j}\mid j\in J\}\right)^{\circ}\right).$

Observe that $\varphi^{\prime}$ contains no non-distinguished binary predicates, and hence is in ${\mathcal{FL}^{2}1\mbox{\rm T}^{\/u}}$. Clearly, $\varphi^{\prime}$ satisfies properties (i) and (ii). To show (iii), suppose $\mathfrak{A}\models\varphi$, and let $\mathfrak{A}^{\prime}$ be the structure obtained by interpreting the predicates $p_{i,J}$ and $q_{J}$ as suggested above. To show (iv), suppose $\varphi^{\prime}$ has a model of size $M$. By Lemma 3.11, $\varphi^{\prime}$ has a model $\mathfrak{B}$ of size $sM$ in which witnesses for all the conjuncts in (c) are duplicated $s$ times. We need to show that $\mathfrak{B}$ can be expanded to a model of $\varphi$. Fix $a\in B$ and suppose $a$ satisfies $p_{1}$. Let $J$ be the set of indices $j$ such that $a$ satisfies $q_{j}$. By (a), putting $i=1$, $a$ satisfies $p_{1,J}$, whence, by (c), there exists $b$ such that the pair $\langle a,b\rangle$ satisfies $\left(\Gamma_{1}\cup\Omega\cup\bigcup\{\Delta_{j}\mid j\in J\}\right)^{\circ}$. But Lemma 3.12 guarantees that we can expand $\mathfrak{B}$ by interpreting the non-distinguished binary predicates so that $\langle a,b\rangle$ satisfies $\Gamma_{1}\cup\Omega\cup\bigcup\{\Delta_{j}\mid j\in J\}$. Because of the duplication of witnesses, we can repeat with $p_{2},\dots,p_{s}$, choosing a fresh witness each time, so as to avoid clashes. Do this for all elements $a$. At the end of the process, the partially defined expansion of $\mathfrak{B}$ satisfies all the existential conjuncts of $\varphi$, and violates none of the universal or static conjuncts. A precisely similar argument shows that we may complete the expansion so that no universal or static conjuncts of $\varphi$ are violated. See Section A.3 in the Appendix for details. *

Thus, at the expense of an exponentially larger signature, we have reduced the (finite) satisfiability problem for ${\mathcal{FL}^{2}1\mbox{\rm T}}$ to that for ${\mathcal{FL}^{2}1\mbox{\rm T}^{\/u}}$. By Lemmas 3.8 and 3.13, we obtain

Lemma 3.15**.**

Let $\varphi$ be a ${\mathcal{FL}^{2}1\mbox{\rm T}}$-formula. If $\varphi$ is satisfiable, then $\varphi$ has a model of size at most triply exponential in $|\!|\varphi|\!|$. Hence the satisfiability problem for ${\mathcal{FL}^{2}1\mbox{\rm T}}$ is in 3-NExpTime.

We now establish the finite model property for the whole of ${\mathcal{FL}1\mbox{\rm T}}$ by eliminating variables from ${\mathcal{FL}^{m+1}1\mbox{\rm T}}$, where $m\geq 2$, one at a time. The proof of the following Lemma is similar to the proof of Lemma 3.13 and has been relegated to the Appendix.

Lemma 3.16**.**

Let $\varphi$ be a clause normal form ${\mathcal{FL}^{m+1}1\mbox{\rm T}}$-formula ($m\geq 2$) over a signature $\Sigma\cup\{\mathfrak{t}\}$, and suppose that $\varphi$ has $s$ existential conjuncts and $t$ universal conjuncts. Then there exists a clause normal form ${\mathcal{FL}^{m}1\mbox{\rm T}}$-formula $\varphi^{\prime}$ over a signature $\Sigma^{\prime}\cup\{\mathfrak{t}\}$ such that the following hold: (i) $\varphi^{\prime}$ has at most $2^{t}s$ existential and $2^{t}$ universal conjuncts; (ii) $|\Sigma^{\prime}|\leq|\Sigma|+2^{t}(s+1)$; (iii) if $\varphi$ has a model, so does $\varphi^{\prime}$; and (iv) if $\varphi^{\prime}$ has a model of size $M$, then $\varphi$ has a model of size at most $sM$.

Theorem 3.17**.**

Let $\varphi$ be a ${\mathcal{FL}^{m}1\mbox{\rm T}}$-formula for $m\geq 2$. If $\varphi$ is satisfiable, then $\varphi$ has a model of size at most $(m+1)$-tuply exponential in $|\!|\varphi|\!|$. Hence the satisfiability problem for ${\mathcal{FL}^{m}1\mbox{\rm T}}$ is in non-deterministic $(m+1)$-tuply exponential time.

Proof 3.18**.**

Induction on $m$. The case $m=2$ is Lemma 3.15. The inductive step is Lemma 3.16.

We mentioned in Sec. 1 that [15] establishes a lower bound of $\lfloor m/2\rfloor$-NExpTime-hard for the satisfiability problem for ${\mathcal{FL}}^{m}$. For $m\geq 3$, this appears to be the best available lower bound on the corresponding problem for ${\mathcal{FL}^{m}1\mbox{\rm T}}$. Thus, a gap remains between the best available upper and lower complexity bounds. Certainly, it follows that the satisfiability problem for ${\mathcal{FL}1\mbox{\rm T}}$ is Tower-complete, as for ${\mathcal{FL}}$.

4 Fluted Logic with more Transitive Relations

In this section we show two undecidability results for the fluted fragment with two variables, ${\mathcal{FL}}^{2}$, extended with more transitive relations, that have been informally announced in [25]. We employ the apparatus of tiling systems.

A tiling system is a tuple $\boldsymbol{\mathcal{C}}=({\mathcal{C}},{\mathcal{C}}_{H},{\mathcal{C}}_{V})$, where $\mathcal{C}$ is a finite set of tiles, and ${\mathcal{C}}_{H}$, ${\mathcal{C}}_{V}\subseteq{\mathcal{C}}\times{\mathcal{C}}$ are the horizontal and vertical constraints.

Let $S$ be either of the spaces ${\mathbb{N}}\times{\mathbb{N}}$, ${\mathbb{Z}}\times{\mathbb{Z}}$ or ${\mathbb{Z}}_{t}\times{\mathbb{Z}}_{t}$. A tiling system $\boldsymbol{\mathcal{C}}$ tiles $S$, if there exists a function $\rho:S\rightarrow{\cal C}$ such that for all $(p,q)\in S$: $(\rho(p,q),\rho(p+1,q))\in{\cal C}_{H}$ and $(\rho(p,q),\rho(p,q+1))\in{\cal C}_{V}$. The following problems are known to be undecidable (cf. e.g. [2]):

• •

Given a tiling system $\boldsymbol{\mathcal{C}}$ determine if $\boldsymbol{\mathcal{C}}$ tiles ${\mathbb{Z}}\times{\mathbb{Z}}$, or ${\mathbb{N}}\times{\mathbb{N}}$.

• •

Given a tiling system $\boldsymbol{\mathcal{C}}$ determine if $\boldsymbol{\mathcal{C}}$ tiles ${\mathbb{Z}}_{t}\times{\mathbb{Z}}_{t}$, for some $t\geq 1$.

In this section we first prove the following theorem.

Theorem 4.1**.**

The satisfiability problem for ${\mathcal{FL}^{2}3\mbox{\rm T}}$, the two-variable fluted fragment with three transitive relations, is undecidable.

Proof 4.2**.**

Suppose the signature contains transitive relations $b$ (black), $g$ (green) and $r$ (red), and additional unary predicates $e$, $e^{\prime}$, $f$, $l$, $c_{i,j}$ ($0\leq i\leq 5$, $0\leq j\leq 2$) and $d_{i,j}$ ($0\leq i\leq 2$, $0\leq j\leq 5$); we refer to the $c_{i,j}$’s and to the $d_{i,j}$’s as colours.

We reduce from the ${\mathbb{N}}\times{\mathbb{N}}$ tiling problem. We first write a formula $\varphi_{grid}$ that captures several properties of the intended expansion of the ${\mathbb{N}}\times{\mathbb{N}}$ grid as shown in Fig. 2(a). There the predicates $c_{i,j}$ and $d_{i,j}$ together define a partition of the universe as follows: an element $(k,k^{\prime})$ with $k^{\prime}>k$ (i.e. in the yellow region, above the diagonal) satisfies $c_{i,j}$ with $i=k\mod 6$, $j=k^{\prime}\mod 3$, and an element $(k,k^{\prime})$ with $k\geq k^{\prime}$ (i.e. in the pink region, on or below the diagonal) satisfies $d_{i,j}$ with $i=k\mod 3,j=k^{\prime}\mod 6$. Paths of the same transitive relation have length at most 7 and follow one of four designated patterns. Remaining unary predicates mark the following elements: $l$—left column, $f$—bottom row, $e$—main diagonal, and $e^{\prime}$—elements with coordinates $(k,k+1)$.

The formula $\varphi_{grid}$ comprises a large number of conjuncts. To help give an overview of the construction, we have organized these conjuncts into groups, each of which secures a particular property (or collection of properties) exhibited by its models. The first two properties are very simple:

1. (1)

There is an ‘initial’ element satisfying $d_{00}(x)\wedge e(x)\wedge l(x)\wedge f(x)$. 2. (2)

The predicates $c_{i,j}$ and $d_{i,j}$ together partition the universe.

The third property generates the path shown in Fig. 3(a):

1. (3)

Each element has a $b$- $r$- or $g$- successor as shown in the path shown in Fig. 3(a), and satisfying the appropriate predicates $c_{i,j}$ or $d_{i,j}$. Specifically, if a node in this path has coordinates $(x,y)$ with $y>x$, then it satisfies $c_{i,j}$ where $i=x\mod 3$ and $j=y\mod 6$; and when $y\leq x$, then the node satisfies $d_{i,j}$ where $i=x\mod 3$ and $j=y\mod 6$.

The conjuncts enforcing this property have the form

[TABLE]

where $colour$ and $colour^{\prime}$ stand for one of the predicate letters $c_{i,j}$ or $d_{i,j}$, $diag(x)$ stands for one of the literals $e^{\prime}(x)$, $\neg e^{\prime}(x)$, $e(x)$, $\neg e(x)$ or $\top$ (i.e. the logical constant true), $border(x)$ stands for one of the literals $l(x)$, $\neg l(x)$, $f(x)$, $\neg f(x)$ or $\top$, and $t$ stands for one of the transitive predicate letters $b$, $r$ or $g$. The precise combinations of the literals and predicate letters in these conjuncts can be read from Fig. 3(a) (cf. Appendix, Table. 1 for a full list).

To connect all pairs of elements that are neighbours in the standard grid we require a fourth property, which we give in schematic form as follows:

1. (4)

Certain* pairs of elements connected by one transitive relation are also connected by another, as indicated in Fig. 3(b).*

Here are some examples of the conjuncts enforcing this property:

[TABLE]

The role of these conjuncts can be explained referring to Fig. 3(b). For example, employing (4b) for the element $(1,1)$ in the intended model $\mathfrak{G}$, we get $\mathfrak{G}\models r((1,1),(1,0))$; hence by transitivity of $r$, also $\mathfrak{G}\models r((1,1),(1,2))$. This, applying (4c), implies $\mathfrak{G}\models g((1,1),(1,2))$. By (4a), we get $\mathfrak{G}\models g((0,1),(1,1))$ and, by transitivity of $g$, $\mathfrak{G}\models g((0,1),(0,2))$. The process is illustrated in Fig. 3(b); when carried on along the zig-zag path, it constructs a grid-like structure.

These conjuncts depend on having available the predicates marking the borders and the diagonals. Specifically, we require the following property:

1. (5)

the predicates $l$, $f$, $e$ and $e^{\prime}$ are distributed to mark the left-most column, the first row, the diagonal and the ‘super-diagonal’ of the grid, as indicated above. To secure this property, we add to $\varphi_{grid}$ several conjuncts, for instance:

[TABLE]

where $\pm e(x)$ denotes uniformly $e(x)$ or $\neg e(x)$. Similar conjuncts are added for the super-diagonal, left column and bottom row; and also for the connection with and between $e$ and $e^{\prime}$. The conjuncts ensuring properties (4) and (5) work in tandem. For instance, applying (5a) to (1,1) we get $e$ is true at $(2,2)$; then, following the zig-zag path and applying more conjuncts from the group (4), we get that $g((2,2),(3,3))$ holds, so the node $(3,3)$ will be marked by $e$; this will propagate along the main diagonal.

The structure $\mathfrak{G}$ depicted in Fig. 2(a) is a model of $\varphi_{grid}$. In fact, $\varphi_{grid}$ is an infinity axiom. To see this, let $\mathfrak{A}\models\varphi_{grid}$ and define an injective embedding $\rho$ of the standard grid on ${\mathbb{N}}\times{\mathbb{N}}$ into $\mathfrak{A}$ as follows. Let $next:{\mathbb{N}}\times{\mathbb{N}}\mapsto{\mathbb{N}}\times{\mathbb{N}}$ be the successor function defined on ${\mathbb{N}}\times{\mathbb{N}}$ as depicted by the zig-zag path in the left-hand picture of Fig. 3 starting at $(0,0)$ (ignoring any colours). Denote $s_{0}=(0,0)$, $s_{n}=next(s_{n-1})$ and $S_{n}=\{s_{0},\ldots,s_{n}\}$. Let $a_{0}\in A$ be an element such that $\mathfrak{A}\models d_{00}(a)\wedge e(a)\wedge l(a)\wedge f(a)$ that exists by condition (1). Define $\rho(s_{0})=a_{0}$. Now, we proceed inductively: suppose $\rho(s_{n-1})$ has already been defined in step $n-1$ of the induction and $\rho(s_{n-1})=a_{n-1}$. Let $a_{n}$ be the witness of $a_{n-1}$ for the appropriate conjunct from the group (3), i.e. where the unary literals for $x$ agree with the unary literals satisfied by $a_{n-1}$ in $\mathfrak{A}$. Define $\rho(s_{n})=a_{n}$. Using induction one can prove that $\rho$ is indeed injective: in the inductive step we assume that $\mathfrak{A}\upharpoonright\{a_{0},\ldots,a_{n-1}\}$ is isomorphic to $\mathfrak{G}\upharpoonright S_{n-1}$, and we show that $a_{n}\not\in\{a_{0},\ldots,a_{n-1}\}$ and $\mathfrak{A}\upharpoonright\{a_{0},\ldots,a_{n}\}$ and $\mathfrak{G}\upharpoonright S_{n}$ are again isomorphic. In the proof one considers several cases depending on the 1-type realized by $a_{n}$. The formula $\varphi_{grid}$ ensures that $a_{0},\ldots,a_{18}$ are all distinct, and any eight consecutive elements of the sequence $a_{0},\ldots,a_{n}$ are always distinct. Consider $a_{18}=\rho(4,2)$ that requires a witness $b\in A$ for a conjunct from the group (3) such that $\mathfrak{A}\models r(a_{18},b)\wedge d_{11}(b)$. Suppose, $b=a_{2}=\rho(1,1)$, since $\mathfrak{A}\models d_{11}(a_{2})$. Then, by transitivity of $g$, $\mathfrak{A}\models g(a_{18},a_{10})$, which is a contradiction with $\mathfrak{G}\models\neg g((4,2),(1,1))$. Other cases are similar and due to page limits have been omitted.

We are now ready to define the horizontal and vertical successors in models of of $\varphi_{grid}$. In fact, instead of defining the horizontal grid successor $\mathsf{h}$ as one binary relation, we define two disjoint binary relations $\mathsf{rt}(x,y)$ and $\mathsf{lt}(x,y)$ such that $\mathsf{rt}$ and the inverse of $\mathsf{lt}$ together give the expected horizontal grid successor; they are defined respecting the ‘direction’ of the transitive edges in the models. In the intended model $\mathsf{rt}((x_{1},y_{1}),(x_{2},y_{2}))$ holds if $x_{2}=x_{1}+1$, $y_{2}=y_{1}$ and $(x_{1},y_{1})$ and $(x_{2},y_{2})$ are connected by $b$, $g$ or $r$; and for $\mathsf{lt}((x_{1},y_{1}),(x_{2},y_{2}))$ to hold we require $x_{2}=x_{1}-1$ instead of $x_{2}=x_{1}+1$. We present the definition of $\mathsf{rt}(x,y)$ in detail below111Addition in subscripts of the $c_{i,j}$’s is always understood modulo 6 in the first position, and modulo 3 in the second position, i.e. $c_{i+a,j+b}$ denotes $c_{(i+a)\,\mathsf{mod}\>6,(j+b)\,\mathsf{mod}\>3}$. Similarly, addition in subscripts of the $d_{i,j}$’s is understood modulo 3 in the first position, and modulo 6 in the second position.

[TABLE]

The relation $\mathsf{rt}$ connects elements that are connected by $b$, $g$ or $r$ and satisfy one of the possible combinations of colours: in the second line the combinations for crossing the diagonal are listed, in the third line the left disjunction describes combinations when both elements are located above the diagonal, and in the right disjunction—when both elements are located on and below the diagonal. The definition of $\mathsf{lt}(x,y)$ complements that of $\mathsf{rt}$. Analogously, we define relations $\mathsf{up}$ and $\mathsf{dn}$ that together define the vertical grid successor.

Now we are ready to write formulas that properly assign tiles to elements of the model. We do this with a formula $\varphi_{tile}$, which again features several conjuncts enforcing various properties of its models. Fortunately, the properties in question are much simpler this time:

1. (6)

*Each node encodes precisely one tile. * 2. (7)

*Adjacent tiles respect ${\cal C}_{H}$. * 3. (8)

Adjacent tiles respect ${\cal C}_{V}$ (written as above using $\mathsf{up}$ and $\mathsf{dn}$).

*Property (6) is secured by the conjunct \forall x\big{(}\bigvee_{C\in{\cal C}}C(x)\wedge\bigwedge_{C\neq D}(\neg C(x)\vee\neg D(x))\big{)}. Property (7) is secured by the conjunct *

[TABLE]

and property (8) is analogous. We remark that these latter formulas are not strictly fluted but can be rewritten as fluted using classical tautologies (cf. formula (7) in Section B).

Finally, let $\eta_{\boldsymbol{\cal C}}$ be the conjunction of $\varphi_{grid}$ and $\varphi_{tile}$. The following Claim completes the reduction and the proof of our theorem.

Claim 1**.**

$\eta_{\boldsymbol{\cal C}}$* is satisfiable iff $\boldsymbol{\cal C}$ tiles ${\mathbb{N}}\times{\mathbb{N}}$.*

Proof: ($\Leftarrow$) If $\boldsymbol{\cal C}$ tiles ${\mathbb{N}}\times{\mathbb{N}}$ then to show that $\eta_{\boldsymbol{\cal C}}$ is satisfiable we can expand our intended model $\mathfrak{G}$ for $\varphi_{grid}$ assigning to every element of the grid a unique $C\in{\cal C}$ given by the tiling.

($\Rightarrow$) Let $\mathfrak{A}\models\eta_{\boldsymbol{\cal C}}$. Let $\rho$ be the embedding of the standard ${\mathbb{N}}\times{\mathbb{N}}$ grid into $\mathfrak{A}$ defined above. One can inductively show that $\rho$ maps neighbours in the grid to elements connected by one of the relations $\mathsf{lt},\mathsf{rt},\mathsf{up},\mathsf{dn}$ as follows ($i,j\geq 0$):

[TABLE]

*(Here, $\dot{\vee}$ is exclusive disjunction.) So, we can define a tiling of the standard grid assigning to every node $(i,j)$ the unique tile $C$ such that $\mathfrak{A}\models C(\rho(i,j))$. Conditions (7) and (8) together with the above observation ensure that this assignment satisfies the tiling conditions. *

We remark that the formula $\varphi_{grid}$ in the proof of Theorem 4.1 is an axiom of infinity, hence the satisfiability and the finite satisfiability problems do not coincide. Moreover, all formulas used in the proof are either guarded or can easily be rewritten as guarded. Furthermore, in the proof it would suffice to assume that $b$, $g$ and $r$ are interpreted as equivalence relations. Hence, we can strengthen the above theorem as follows.

Corollary 4.3**.**

The satisfiability problem for the intersection of the fluted fragment with the two-variable guarded fragment is undecidable in the presence of three transitive relations (or three equivalence relations).

Now we improve the undecidability result to the case of ${\mathcal{FL}^{2}2\mbox{\rm T}}$ with equality.

Theorem 4.4**.**

The (finite) satisfiability problem for the two-variable fluted fragment with equality is undecidable in the presence of two transitive relations.

Proof 4.5**.**

We write a formula $\varphi_{grid}$ over a signature consisting of transitive relations $b$ and $r$, and unary predicates $c_{i,j}$ ($0\leq i,j\leq 3$). The formula $\varphi_{grid}$ captures several properties of the intended expansion of the ${\mathbb{Z}}\times{\mathbb{Z}}$ grid as shown Fig. 2(b):

1. (1)

there is an initial element: $\exists x.c_{00}(x)$. 2. (2)

the predicates $c_{i,j}$ partition the universe. 3. (3)

*transitive paths do not connect distinct elements of the same colour: $\bigwedge_{0\leq i,j\leq 3}\forall x(c_{ij}(x)\rightarrow\forall y((b(x,y)\vee r(x,y))\wedge c_{ij}(y)\rightarrow x=y))$ * 4. (4)

each element belongs to a 4-element blue clique and to a 4-element red clique. 5. (5)

certain* pairs of elements connected by $r$ are also connected by $b$, and certain pairs of elements connected by $b$ are also connected by $r$.*

We have given property (5) only schematically, of course; its role is analogous to that of property (4) in the proof of Theorem 4.1. The remainder of the proof is similar to the one presented for Theorem 4.1 and due to space limits it is relegated to the Appendix. We note that $\varphi_{grid}$ has also finite models expanding a toroidal grid structure ${\mathbb{Z}}_{4m}\times{\mathbb{Z}}_{4m}$ ($m>0$) obtained by identifying elements from columns 0 and $4m$ and from rows 0 and $4m$. Hence, the proof gives undecidability for both the satisfiability and the finite satisfiability problems.

Again, the formulas used in the above proof are guarded or can be rewritten as guarded. Also it suffices to assume that $r$ is an equivalence relation. Hence we get the following

Corollary 4.6**.**

The (finite) satisfiability problem for the intersection of the fluted fragment with equality with the two-variable guarded fragment is undecidable in the presence of two transitive relations (or one transitive and one equivalence relation).

5 Conclusions

In this paper, we considered the ($m$-variable) fluted fragment in the presence of different numbers of transitive relations. We showed that ${\mathcal{FL}1\mbox{\rm T}}$ has the finite model property, but ${\mathcal{FL}^{2}3\mbox{\rm T}}$ admits axioms of infinity and the satisfiability problem for ${\mathcal{FL}^{2}3\mbox{\rm T}}$ is undecidable. This contrasts with known results for other decidable fragments, in particular, $\mbox{\rm FO}^{2}$, where the satisfiability and finite satisfiability problems are undecidable in the presence of two transitive relations, and where the finite satisfiability problem is decidable in the presence of one transitive relation. It is open whether the (finite) satisfiability problem for ${\mathcal{FL}}$ in the presence of two transitive relations, $\mathfrak{t}_{1}$ and $\mathfrak{t}_{2}$, is decidable. We point out that Lemma 3.16 in Section 3 could be generalized to normal form formulas from ${\mathcal{FL}^{m+1}2\mbox{\rm T}}$. Hence, the (finite) satisfiability problem for ${\mathcal{FL}}$ in the presence of two transitive relations is decidable if and only if the corresponding problem for ${\mathcal{FL}}^{2}$ with two transitive relations is decidable. Unfortunately neither the method of Sec. 3 (to show decidability) nor that of Sec. 4 (to show undecidability) appears to apply here. The barrier in the former case is that pairs of elements can be related by both $\mathfrak{t}_{1}$ and $\mathfrak{t}_{2}$ via divergent $\mathfrak{t}_{1}$- and $\mathfrak{t}_{2}$-chains, so that simple certificates of the kind employed for ${\mathcal{FL}^{2}1\mbox{\rm T}^{\/u}}$ do not guarantee the existence of models. The barrier in the latter case is that the grid construction has to build models featuring transitive paths of bounded length, and this seems not to be achievable with just two transitive relations. Finally, we expect that the undecidability result for ${\mathcal{FL}^{2}3\mbox{\rm T}}$ can be extended to get undecidability of the corresponding finite satisfiability problem.

Appendix A Proofs from Section 3

A.1 Proof of Lemma 3.1

We employ standard ‘re-writing’ techniques, temporarily allowing 0-ary predicates. By moving negations inward in the usual way, we may assume without loss of generality that negation symbols in $\varphi$ apply only to atoms. Suppose $\varphi_{0}$ has a subformula $\theta=\exists x_{k+1}.\zeta$ ($0\leq k<2$), where $\zeta$ is quantifier-free. Let $p$ be a fresh predicate of arity $k$ (thus: 0-ary predicates can be introduced), and again let $\varphi_{1}:=\varphi_{0}[\theta/p(x_{1},\dots,x_{k})]$ and $\psi_{1}:=\forall x_{1}\cdots\forall x_{k}(p(x_{1},\dots,x_{k})\leftrightarrow\theta)$; hence, $\models\varphi_{1}\wedge\psi_{1}\rightarrow\varphi_{0}$, and any model of $\varphi_{0}$ can be expanded to a model of $\varphi_{1}\wedge\psi_{1}$. Thus, $\psi_{1}$ is of the form $\forall x_{1}\cdots\forall x_{k}(p(x_{1},\dots,x_{k})\leftrightarrow\exists x_{k+1}.\zeta)$, where $\zeta$ is fluted and quantifier-free. Suppose, alternatively, that $\varphi_{0}$ has a subformula $\theta=\forall x_{k+1}.\zeta$. where $\zeta$ is quantifier-free. We proceed in the similarly, except that $\psi_{1}$ is of the form $\forall x_{1}\cdots\forall x_{k}(p(x_{1},\dots,x_{k})\leftrightarrow\forall x_{k+1}.\zeta)$.

Proceeding similarly with $\varphi_{1}$ in place of $\varphi_{0}$, we obtain $\varphi_{2}$ and $\psi_{2}$, and so on, until we reach some point where the ${\mathcal{FL}}^{m}$-sentence $\varphi_{s}$ is a proposition letter. Defining $\psi^{\prime}$ to be $\psi_{1}\wedge\cdots\wedge\psi_{s}\wedge\varphi_{s}$, we see that $\models\psi^{\prime}\rightarrow\varphi$, and any model of $\varphi$ can be expanded to a model of $\psi^{\prime}$. It should be clear that the size of $\psi^{\prime}$ is at most linear in the size of $\varphi$. Each of the $\psi_{i}$ and indeed $\varphi_{s}$ is either a proposition letter or (following variable re-naming) of one of the forms

[TABLE]

where $\lambda$ is a quantifier-free fluted formula in variables $x_{1},x_{2}$ and $\mu$ a quantifier-free fluted formula with variable $x_{1}$. Furthermore, we may re-write any formula $\forall x_{1}(p(x_{1})\leftrightarrow\exists x_{2}.\lambda)$ equivalently as a conjunction $\forall x_{1}(p(x_{1})\rightarrow\exists x_{2}.\lambda)\wedge\forall x_{1}(\neg p(x_{1})\rightarrow\forall x_{2}\neg\lambda)$, and similarly for $\forall x_{1}(p(x_{1})\leftrightarrow\forall x_{2}.\lambda)$.

Eliminate the 0-ary predicates by guessing their truth values and carrying out the obvious simplifications. Let $\Psi^{\prime}$ be any satisfiable collection of formulas obtained in this way if there is one (or any of them if $\varphi$ is not satisfiable). Massaging $\Psi^{\prime}$ into a set of formulas $\Psi$ of the desired forms is then completely routine.

A.2 Proof of Lemma 3.12

Enumerate the atoms $r(x_{1},\dots,x_{m})$ where $r\in\Sigma$ is of maximal arity $m$, as $\rho_{1},\dots,\rho_{n}$. Define a level-$i$ extension of $\tau^{-}$ inductively as follows: (i) $\tau^{-}$ is a level-0 extension of $\tau^{-}$; (ii) if $\tau^{\prime}$ is a level-$i$ extension of $\tau^{-}$ ($0\leq i<n$), then $\tau^{\prime}\wedge\rho_{i+1}$ and $\tau^{\prime}\wedge\neg\rho_{i+1}$ are level-$(i+1)$ extensions of $\tau^{-}$. Thus, the level-$n$ extensions of $\tau^{-}$ are exactly the fluted $m$-types over $\Sigma\cup\{\mathfrak{t}\}$ entailing $\tau^{-}$. If $\tau^{\prime}$ is a level-$i$ extension of $\tau^{-}$ ($0\leq i<n$), we say that $\tau^{\prime}$ violates a clause $\delta$ if, for every literal in $\delta$, the opposite literal is in $\tau^{\prime}$; we say that $\tau^{\prime}$ violates a set of clauses $\Delta$ if $\tau^{\prime}$ violates some $\delta\in\Delta$. We construct a sequence of level-$i$ extensions of $\tau^{-}$ ($i=0,1,\dots$) none of which violates $\Gamma^{*}$.

By definition, $\tau^{-}$ is a level-0 extension of itself. Suppose now that $\tau^{\prime}$ is a level-$i$ extension of $\tau^{-}$ ($0\leq i<n$). We claim that, if both $\tau^{\prime}\wedge\rho_{i+1}$ and $\tau^{\prime}\wedge\neg\rho_{i+1}$ violate $\Gamma^{*}$, then so does $\tau^{\prime}$. For otherwise, there must be a clause $\neg\rho_{i+1}\vee\gamma^{\prime}\in\Gamma^{*}$ violated by $\tau^{\prime}\wedge\rho_{i+1}$ and a clause $\rho_{i+1}\vee\delta^{\prime}\in\Gamma^{*}$ violated by $\tau^{\prime}\wedge\neg\rho_{i+1}$. But in that case $\tau^{\prime}$ violates the fluted resolvent $\gamma^{\prime}\vee\delta^{\prime}$, contradicting the supposition that $\tau^{\prime}$ does not violate $\Gamma^{*}$. This proves the claim. Now, since $\tau^{-}$ by hypothesis is consistent with $\Gamma^{\circ}$, it does not violate $\Gamma^{\circ}$. Therefore, since $\tau^{-}$ involves no $m$-literals $\pm r(x_{1},\dots,x_{m})$ for $r\in\Sigma$, it does not violate $\Gamma^{*}$ either. By the above claim, then, there must be at least one level-$n$ extension $\tau$ of $\tau^{-}$ which does not violate $\Gamma^{*}\supseteq\Gamma$. Since $\tau$ is a fluted $m$-type, this proves the lemma.

A.3 Proof of Lemma 3.13

Let $\varphi$ be the formula

[TABLE]

where $\Omega,\Gamma_{1},\dots,\Gamma_{s},\Delta_{1},\dots,\Delta_{t}$ are sets of fluted 2-clauses, and $p_{1},\dots,p_{s}$, $q_{1},\dots,q_{t}$ unary predicates. Write $T=\{1,\dots,t\}$. For all $i$ ($1\leq i\leq s$) and all $J\subseteq T$, let $p_{i,J}$ and $q_{J}$ be new unary predicates. The intended interpretation of $p_{i,J}(x_{1})$ is “$x_{1}$ satisfies $p_{i}$, and also satisfies $q_{j}$ for every $j\in J$;” and the intended interpretation of $q_{J}(x_{1})$ is “$x_{1}$ satisfies $q_{j}$ for every $j\in J$.” Let $\varphi^{\prime}$ be the conjunction of the sentences

[TABLE]

We claim that, if $\varphi$ is satisfiable, then so is $\varphi^{\prime}$ (see Appendix, Section A.3). This proves the lemma, since $\varphi^{\prime}$ evidently contains no non-distinguished binary predicates, and hence is in ${\mathcal{FL}^{2}1\mbox{\rm T}^{\/u}}$.

For suppose $\mathfrak{A}\models\varphi$. We expand $\mathfrak{A}$ to a model $\mathfrak{A}^{\prime}\models\varphi^{\prime}$ by setting, for all $i$ ($1\leq i\leq s$) and all $J\subseteq T$,

p_{i,J}^{\mathfrak{A}^{\prime}}=\{a\mid\text{\mathfrak{A}\models p_{i}[a]$and$\mathfrak{A}\models q_{j}[a]$for all$j\in J}\} and q_{J}^{\mathfrak{A}^{\prime}}=\{a\mid\text{\mathfrak{A}\models q_{j}[a]$for all$j\in J}\}.

To see that $\mathfrak{A}^{\prime}\models\varphi^{\prime}$, we simply check the truth of conjuncts (9)–(12) in $\mathfrak{A}^{\prime}$ in turn. Sentences (9) and (10) are immediate. For (11), fix $i$ and $J$, and suppose $\mathfrak{A}^{\prime}\models p_{i,J}[a_{1}]$. By the definition of $\mathfrak{A}^{\prime}$, $\mathfrak{A}\models p_{i}[a_{1}]$ and $\mathfrak{A}\models q_{j}[a_{1}]$ for all $j\in J$. Since $\mathfrak{A}\models\varphi$, there exists $b$ such that $\mathfrak{A}\models\Gamma_{i}[a_{1},b]$, $\mathfrak{A}\models\Omega[a_{1},b]$ and $\mathfrak{A}\models\Delta_{j}[a_{1},b]$ for all $j\in J$. Since resolution is a valid inference step, $\mathfrak{A}^{\prime}\models\left(\Gamma_{i}\cup\Omega\cup\bigcup\{\Delta_{j}\mid j\in J\}\right)^{\circ}[a_{1},b]$. This establishes the truth of (11) in $\mathfrak{A}^{\prime}$. Sentence (12) is handled similarly.

Conversely, we claim that, if $\varphi^{\prime}$ is satisfiable over a domain $A$, then $\varphi$ is satisfiable over a domain of size $s\cdot|A|$. For suppose $\mathfrak{A}\models\varphi^{\prime}$. Let $\mathfrak{B}$ be the model of $\varphi^{\prime}$ guaranteed by Lemma 3.11, where $z=s$. We may assume that $\mathfrak{A}$ and hence $\mathfrak{B}$ interpret no non-distinguished predicates of arity $2$. We proceed to expand $\mathfrak{B}$ to a model $\mathfrak{B}^{\prime}\models\varphi$ by interpreting the non-distinguished predicates of arity $2$ occurring in $\varphi$. Pick any element $a_{1}$ from $B$, and let $J$ be the set of all $j$ ($1\leq j\leq t$) such that $\mathfrak{B}\models q_{j}[a_{1}]$. Suppose also that, for some $i$ ($1\leq i\leq s$) $\mathfrak{A}\models p_{i}[a_{1}]$. From (9), $\mathfrak{B}\models p_{i,J}[a_{1}]$; and from (11), we may pick $b_{i}\in B$ such that $\mathfrak{B}\models\left(\Gamma_{i}\cup\Omega\cup\bigcup\{\Delta_{j}\mid j\in J\}\right)^{\circ}[a_{1},b_{i}]$. From the properties secured for $\mathfrak{B}$ by Lemma 3.11, we know that if, for fixed $a$, we have $\mathfrak{A}\models\alpha_{i}[a_{1}]$ for more than one value of $i$, then we may choose the corresponding elements $b_{i}$ so that they are all distinct. For each such $b_{i}$, then, let $\tau_{i}=\mbox{\rm ftp}^{\mathfrak{B}}[a_{1},b_{i}]$. Thus, $\tau_{i}(x_{1},x_{2})$ is consistent with $\left(\Gamma_{i}\cup\Omega\cup\bigcup\{\Delta_{j}\mid j\in J\}\right)^{\circ}$. By Lemma 3.12, there exists a fluted $2$-type $\tau_{i}^{+}\supseteq\tau_{i}(x_{1},x_{2})$ such that $\tau_{i}^{+}$ is consistent with $\Gamma_{i}\cup\Omega\cup\bigcup\{\Delta_{j}\mid j\in J\}$. Set $\mbox{\rm ftp}^{\mathfrak{B}^{\prime}}[a_{1},b_{i}]=\tau^{+}_{i}$. Since $\tau^{+}_{i}\supseteq\tau_{i}$, only non-distinguished binary predicates are being assigned, so that there is no clash with $\mathfrak{B}$. Moreover, since the $b_{i}$ are all distinct (for a given element $a$), these assignments do not clash with each other. In this way, every existential conjunct of $\varphi$ is witnessed in $\mathfrak{B}^{\prime}$ for every element $a$, and no static or universal conjunct of $\varphi$ is violated for the tuples from $B$ for which the binary predicates of $\Sigma$ have been defined. Now let $\langle a_{1},a_{2}\rangle$ be any ordered pair from $B$ for which the binary predicates of $\Sigma$ have not been defined, and let $J$ be the set of all $j$ ($1\leq j\leq t$) such that $\mathfrak{B}\models q_{j}[a_{1}]$. From (10), $\mathfrak{B}\models q_{J}[a_{1}]$; and from (12), $\mathfrak{B}\models\left(\Omega\cup\bigcup\{\Delta_{j}\mid j\in J\}\right)^{\circ}[a_{1},a_{2}]$. Let $\tau=\mbox{\rm ftp}^{\mathfrak{B}}[a_{1},a_{2}]$. Hence $\tau(x_{1},x_{2})$ is consistent with $\left(\Omega\cup\bigcup\{\Delta_{j}\mid j\in J\}\right)^{\circ}$. By Lemma 3.12, there exists a fluted 2-type $\tau^{+}\supseteq\tau$ such that $\tau^{+}$ is consistent with $\Omega\cup\bigcup\{\Delta_{j}\mid j\in J\}$. Set $\mbox{\rm ftp}^{\mathfrak{B}^{\prime}}[a_{1},a_{2}]=\tau^{+}$. Since $\tau^{+}\supseteq\tau$, only non-distinguished binary predicates are being assigned, so that there is no clash with $\mathfrak{B}$. Evidently, no static or universal conjunct of $\varphi$ is violated in this process. Thus, $\mathfrak{B}^{\prime}\models\varphi$, as required.

A.4 Proof of Lemma 3.16

Similar to the proof of Lemma 3.13. Taking $\varphi$ to be as in (7), write $T=\{1,\dots,t\}$. For all $i$ ($1\leq i\leq s$) and all $J\subseteq T$, let $p_{i,J}$ and $q_{J}$ be new predicates of arity $m-2$. The intended interpretation of $p_{i,J}(x_{2},\dots,x_{m-1})$ is “for some $x_{1}$, the tuple $x_{1},\dots,x_{m-1}$ satisfies $\alpha_{i}$ and also satisfies $\beta_{j}$ for every $j\in J$;” and the intended interpretation of $q_{J}(x_{2},\dots,x_{m-1})$ is “for some $x_{1}$, the tuple $x_{1},\dots,x_{m-1}$ satisfies $\beta_{j}$ for every $j\in J$.” Let $\varphi^{\prime}$ be the conjunction of the sentences

[TABLE]

We claim that, if $\varphi$ is satisfiable, then so is $\varphi^{\prime}$. Note that, since $m\geq 2$, (15) and (16) do not involve $x_{1}$. By decrementing all variable indices in these conjuncts, therefore, we obtain a formula of ${\mathcal{FL}^{m}1\mbox{\rm T}}$ as required by the lemma. The proof of the claim proceeds almost identically to Lemma 3.13.

Appendix B Proof of Theorem 4.4: undecidability of ${\mathcal{FL}^{2}2\mbox{\rm T}}$ with equality

Below we present the complete proof that have been roughly sketched in Section 4.

Suppose the signature contains two transitive relations $b$ (blue) and $r$ (red), and additional unary predicates $c_{i,j}$ ($0\leq i\leq 3$, $0\leq j\leq 3$) called colours. We write a formula $\varphi_{grid}$ capturing several properties of the intended expansion of the ${\mathbb{Z}}\times{\mathbb{Z}}$ grid as shown in Fig. 4. There, each element with coordinates $(k,l)$ satisfies $c_{i,j}$, where $i=k\mod 4$ and $j=l\mod 4$ and the transitive relations connect only some elements that are close in the grid. The formula $\varphi_{grid}$ is a conjunction of the following statements.

1. (1)

there is an initial element: $\exists xc_{00}(x)$. 2. (2)

the predicates $c_{i,j}$ enforce a partition of the universe: $\forall x\dot{\bigvee}_{0\leq i\leq 3}\dot{\bigvee}_{0\leq j\leq 3}c_{i,j}(x)$. 3. (3)

transitive paths do not connect distinct elements of the same colour:

[TABLE] 4. (4)

-each element belongs to a 4-element blue clique; this property is expressed by writing the following conjuncts for each $i,j\in\{0,2\}$:

[TABLE]

-each element belongs to a 4-element red clique; we write the following conjuncts for each $i,j\in\{1,3\}$:

[TABLE] 5. (5)

• a group of formulas saying that some pairs of elements connected by $r$ are also connected by $b$:

[TABLE]

• a group of formulas saying that some pairs of elements connected by $b$ are also connected by $r$:

[TABLE]

One can note that $\varphi_{grid}$ has also finite models expanding a toroidal grid structure ${\mathbb{Z}}_{4m}\times{\mathbb{Z}}_{4m}$ ($m>0$) obtained by identifying elements from columns 0 and $4m$ and from rows 0 and $4m$.

In order to encode tilings using two-variable logics it actually suffices to define structures that are grid-like. A structure $\mathfrak{G}=(G,h,v)$ with two binary relation $h$ and $v$ is grid-like, if one of the standard grids ${\mathbb{N}}\times{\mathbb{N}}$, ${\mathbb{Z}}\times{\mathbb{Z}}$ or ${\mathbb{Z}}_{t}\times{\mathbb{Z}}_{t}$ can be homomorphically embedded into $\mathfrak{G}$. To show that a structure $\mathfrak{G}$ is grid-like it suffices to require that $\mathfrak{G}\models\forall x(\exists yh(x,y)\wedge\exists yv(x,y))$ (note that this is an ${\mathcal{FL}}^{2}$-formula) and the following confluence property holds

[TABLE]

The confluence property above uses four variables and is not fluted. We will enforce it in ${\mathcal{FL}}^{2}{}$ using the transitive relations. Let us introduce the following definitions:

[TABLE]

Let $\mathfrak{A}\models\varphi_{grid}$. We show that every model $(\mathfrak{A},\mathsf{h},\mathsf{v})$ of $\varphi_{grid}$ is grid-like. We first show that $\mathfrak{A}$ satisfies $\forall x(\exists y\mathsf{h}(x,y)\wedge\exists y\mathsf{v}(x,y))$. One considers several cases depending on the values of the unary predicates.

Let $a\in A$ and assume $\mathfrak{A}\models c_{00}(a)$. By (4) there are $a_{1},a_{2},a_{3},a_{4}\in A$ such that $\mathfrak{A}\models b(a,a_{1})\wedge c_{10}(a_{1})\wedge b(a_{1},a_{2})\wedge c_{11}(a_{2})\wedge b(a_{2},a_{3})\wedge c_{01}(a_{3})\wedge b(a_{3},a_{4})\wedge c_{00}(a_{4})$. By (3) $a=a_{4}$ and by transitivity of $b$ the elements $a,a_{1},a_{2},a_{3}$ form a blue clique in $\mathfrak{A}$. Hence, $\mathfrak{A}\models\mathsf{h}(a,a_{1})\wedge\mathsf{v}(a,a_{3})$.

The same argument works if $a$ has one of the colours $c_{02},c_{20}$ or $c_{22}$ and, similarly, applying (5) instead of (4) when $a$ has the colours $c_{11},c_{31},c_{13}$ or $c_{33}$.

Consider now the case $\mathfrak{A}\models c_{10}(a)$. By (4) there is $a^{\prime}\in A$ such that $\mathfrak{A}\models b(a,a^{\prime})\wedge c_{11}(a^{\prime})$, hence $\mathfrak{A}\models\mathsf{v}(a,a^{\prime})$. Moreover, by (4) there are $a_{1},a_{2},a_{3},a_{4}\in A$ such that $\mathfrak{A}\models r(a,a_{1})\wedge c_{13}(a_{1})\wedge r(a_{1},a_{2})\wedge c_{23}(a_{2})\wedge r(a_{2},a_{3})\wedge c_{20}(a_{3})\wedge r(a_{3},a_{4})\wedge c_{10}(a_{4})$. By (3) $a=a_{4}$ and by transitivity of $r$ the elements $a,a_{1},a_{2},a_{3}$ form a red clique in $\mathfrak{A}$. By (6d) $\mathfrak{A}\models b(a,a_{1})$, hence $\mathfrak{A}\models\mathsf{h}(a,a_{1})$.

Remaining cases are shown similarly.

Now, we show the confluence property (*). Let $a,a^{\prime},b,b^{\prime}\in A$ and $\mathfrak{A}\models\mathsf{h}(a,b)\wedge\mathsf{v}(a,a^{\prime})\wedge\mathsf{h}(b,b^{\prime})$. One needs to consider several cases depending on the colour of $a$, in each of them showing that $\mathfrak{A}\models\mathsf{h}(a^{\prime},b^{\prime})$. For instance:

• •

$\mathfrak{A}\models c_{00}(a)$. Then $\mathfrak{A}\models c_{01}(a^{\prime})\wedge b(a,a^{\prime})\wedge b(a,b)\wedge c_{10}(b)\wedge b(b,b^{\prime})\wedge c_{11}(b^{\prime})$. By (4) $b^{\prime}$ is a member of a blue clique containing elements of colours $c_{11},c_{01},c_{00},c_{10}$. Since by (3) the relation $b$ does not connect distinct elements of the same colour, $a^{\prime}$ belongs to the blue clique of $b^{\prime}$ and $\mathfrak{A}\models b(a^{\prime},a)$. Now, by transitivity of $b$, $\mathfrak{A}\models\mathsf{h}(a^{\prime},b^{\prime})$.

• •

$\mathfrak{A}\models c_{30}(a)$. Then $\mathfrak{A}\models c_{31}(a^{\prime})\wedge b(a,a^{\prime})\wedge r(a,b)\wedge c_{00}(b)\wedge b(b,b^{\prime})\wedge c_{01}(b^{\prime})$. Similarly as above, $b$ belongs to a red clique of $a$, hence $\mathfrak{A}\models r(b,a)$. By (6a), $\mathfrak{A}\models b(b,a)$. Moreover, $b^{\prime}$ is in a blue clique of $b$, and so $\mathfrak{A}\models b(b^{\prime},b)$. By transitivity of $b$, $\mathfrak{A}\models b(b^{\prime},a^{\prime})$. Now, by (7c), $\mathfrak{A}\models r(b^{\prime},a^{\prime})$. By (4), $a^{\prime}$ is a member of a red clique that, by (3), must contain $b^{\prime}$. Hence $\mathsf{h}(a^{\prime},b^{\prime})$ holds.

Remaining cases can be shown in a similar way. Hence, every model of $\varphi_{grid}$ is grid-like. Now we ensure that we also can assign tiles to elements of the grid-like models using fluted formulas. The task in $\mbox{\rm FO}^{2}$ is easy, it suffices to require that

1. (6)

each node encodes precisely one tile:  $\forall x(\dot{\bigvee}_{C\in{\cal C}}Cx)$, 2. (7)

adjacent tiles respect ${\cal C}_{H}$ and ${\cal C}_{V}$:

[TABLE]

The above two formulas are not fluted but can be written as fluted. Namely, using first-order tautologies, each conjunct in (7a) can be equivalently written as follows:

[TABLE]

and similarly for (7b). Let $\eta_{\boldsymbol{\cal C}}$ be the conjunction of $\varphi_{grid}$ with the properties (6) and (7) written in ${\mathcal{FL}}^{2}$, as explained. It is routine to show that we have simultaneously reduced the plane tiling problem (respectively, the torus tiling problem) to the (finite) satisfiability problem. If $\boldsymbol{\cal C}$ tiles any of the spaces ${\mathbb{Z}}\times{\mathbb{Z}}$ or ${\mathbb{Z}}_{t}\times{\mathbb{Z}}_{t}$, for some $t$, we expand the grids to our intended models. In the opposite direction, when $\mathfrak{G}\models\eta_{\boldsymbol{\cal C}}$ and $\mathfrak{G}$ is infinite we obtain a tiling of ${\mathbb{Z}}\times{\mathbb{Z}}$; in case $\mathfrak{G}$ is finite we obtain a tiling of ${\mathbb{Z}}_{t}\times{\mathbb{Z}}_{t}$ with $t$ divisible by 4. As a result we conclude that the satisfiability and the finite satisfiability problems for ${\mathcal{FL}}^{2}{}$ with two transitive relations are undecidable.

Appendix C Table defining conjuncts in group (3) of the proof of Theorem 4.1