A Fine-Grained Hierarchy of Hard Problems in the Separated Fragment

TL;DR

This paper introduces a detailed complexity analysis of the separated fragment (SF) in logic, establishing a hierarchy based on the degree of variable interaction and proving the precise computational complexity for each level.

Contribution

It defines the degree of interaction as a new measure and proves the $k$-NEXPTIME-completeness of SF-satisfiability for each degree level, refining understanding of SF's complexity.

Findings

SF-satisfiability is $k$-NEXPTIME-complete for each degree $k$.

SF-satisfiability is non-elementary in the general case.

Introduces the degree of interaction as a novel complexity measure.

Abstract

Recently, the separated fragment (SF) has been introduced and proved to be decidable. Its defining principle is that universally and existentially quantified variables may not occur together in atoms. The known upper bound on the time required to decide SF's satisfiability problem is formulated in terms of quantifier alternations: Given an SF sentence $\exists \vec{z} \forall \vec{x}_1 \exists \vec{y}_1 \ldots \forall \vec{x}_n \exists \vec{y}_n . \psi$ in which $\psi$ is quantifier free, satisfiability can be decided in nondeterministic $n$-fold exponential time. In the present paper, we conduct a more fine-grained analysis of the complexity of SF-satisfiability. We derive an upper and a lower bound in terms of the degree of interaction of existential variables (short: degree)}---a novel measure of how many separate existential quantifier blocks in a sentence are connected via joint occurrences of variables in atoms. Our main result is the $k$-NEXPTIME-completeness of the satisfiability problem for the set $SF_{\leq k}$ of all SF sentences that have degree $k$ or smaller. Consequently, we show that SF-satisfiability is non-elementary in general, since SF is defined without restrictions on the degree. Beyond trivial lower bounds, nothing has been known about the hardness of SF-satisfiability so far.

Equations

$$\varphi:=\exists\vec{\mathbf{y}}.\bigwedge_{i\in I}\Bigl{(}\chi_{i}(\vec{\mathbf{z}})\vee\bigvee_{k\in K_{i}}\eta_{k}(\vec{\mathbf{y}},\vec{\mathbf{z}})\Bigr{)}$$

$$\bigwedge_{\text{\scriptsize$\begin{array}[]{c}S\subseteq I\\ S\neq\emptyset\end{array}$ \normalsize}}\Bigl{(}\bigvee_{i\in S}\chi_{i}(\vec{\mathbf{z}})\Bigr{)}\vee\bigvee_{f\in\mathcal{F}}\Bigl{(}\exists\vec{\mathbf{y}}.\bigwedge_{i\in S}\eta_{f(i)}(\vec{\mathbf{y}},\vec{\mathbf{z}})\Bigr{)}~{}.$$

$$\text{len}(\varphi)+\text{len}(\varphi)\cdot\partial_{\varphi}\cdot\bigl{(}{2^{\uparrow\partial_{\varphi}}(\text{len}(\varphi))}\bigr{)}^{\partial_{\varphi}}~{}.$$

$$\varphi:=\forall x_{n}\exists y_{n}\ldots\forall x_{1}\exists y_{1}.\bigwedge_{i=1}^{4n}\bigl{(}P_{i}(x_{1},\ldots,x_{n})\leftrightarrow Q_{i}(y_{1},\ldots,y_{n})\bigr{)}~{}.$$

$$\text{Sat($\text{SF}_{\partial\leq k}$)}\not\in\text{NTIME}\bigl{(}{2^{\uparrow k}(cn/\log n)}\bigr{)}$$

$$\text{Sat(SF)}\not\in\text{NTIME}\bigl{(}{2^{\uparrow d\cdot\sqrt{n/\log n}}(2)}\bigr{)}~{}.$$

$${\psi }_1:=$$

$${\psi }_2:=$$

$$\ell$$

$${\psi }_3:=$$

$${\psi }_4:=$$

$$\ell$$

$${\psi }_5:=$$

$${\psi }_6:=$$

$$j^{\prime }$$

$${\psi }_7:=$$

$$\displaystyle\hskip 111.94409pt\wedge\;\;\bigl{(}\text{Succ}({\underline{\ell}},j^{\prime},j)\wedge\text{Succ}({\underline{\ell}},j^{\prime\prime},j)\rightarrow j^{\prime}\approx j^{\prime\prime}\bigr{)}$$

$$j$$

$${\psi }_8:=$$

$$c_1,\dots ,c_{\mu }$$

$${\psi }_9:=$$

$$\displaystyle\hskip 176.52722pt\wedge\bigl{(}J^{*}({\underline{\ell}},j,i,1)\wedge J({\underline{\ell}},j,i,0)\rightarrow J({\underline{\ell}},j^{\prime},i,1)\bigr{)}$$

$$\displaystyle\hskip 176.52722pt\wedge\bigl{(}J^{*}({\underline{\ell}},j,i,0)\wedge J({\underline{\ell}},j,i,1)\rightarrow J({\underline{\ell}},j^{\prime},i,1)\bigr{)}$$

$$\displaystyle\hskip 176.52722pt\wedge\bigl{(}J^{*}({\underline{\ell}},j,i,0)\wedge J({\underline{\ell}},j,i,0)\rightarrow J({\underline{\ell}},j^{\prime},i,0)\bigr{)}\Bigr{)}$$

$$\ell$$

$$2^{\uparrow \ell }(\mu )$$

$${\psi }_{10}:=$$

$$j$$

$${\psi }_{11}:=$$

$${\psi }_{12}:=$$

$${\psi }_{13}:=$$

$$\displaystyle\hskip 137.77734pt\wedge\bigl{(}J^{*}({\underline{\ell}},j,i,0)\rightarrow\neg J^{*}({\underline{\ell}},j,i,1)\bigr{)}$$

$${\psi }_{14}:=$$

$$J^{\ast }(\underline{\ell },j,d_{\ell -1},1)$$

$${\psi }_{15}:=$$

$$\displaystyle\hskip 172.22168pt\wedge\bigl{(}J({\underline{\ell}},j,i,0)\rightarrow J^{*}({\underline{\ell}},j,i^{\prime},0)\bigr{)}$$

$$\displaystyle\hskip 172.22168pt\wedge\bigl{(}J^{*}({\underline{\ell}},j,i,0)\rightarrow J^{*}({\underline{\ell}},j,i^{\prime},0)\bigr{)}$$

$$J^{\ast }$$

$${\text{eq}}_{j,\tilde{j}}^1:=$$

$${\text{eq}}_{j,\tilde{j}}^{\ell }:=$$

$$\displaystyle\hskip 247.13808pt\wedge\bigl{(}J({\underline{\ell}},j,i,1)\leftrightarrow J({\underline{\ell}},\widetilde{j},\widetilde{i},1)\bigr{)}$$

$$\ell >1$$

$${\psi }_{16}:=$$

$$\ell$$

$${\chi }_1:=$$

$$c_1,\dots ,c_{\mu }$$

$${\chi }_2:=$$

$$J$$

$${\chi }_3:=$$

Full text

1 Introduction

In [17] the separated fragment (SF) of first-order logic with equality is introduced. Its defining principle is that universally and existentially quantified variables may not occur together in atoms. (Topmost existential quantifier blocks are exempt from this rule.) SF properly generalizes both the Bernays–Schönfinkel–Ramsey (BSR) fragment ($\exists^{*}\forall^{*}$-sentences with equality) and the relational monadic fragment without equality (MFO). Still, the satisfiability problem for SF is decidable.

In computational logic formulas are often classified based on the shape of quantifier prefixes. There is a wealth of results that separate decidable first-order formulas from undecidable ones in this fashion, see [3] for references. The definition of the BSR fragment is only one example. In the context of computational complexity, hierarchies are defined, such as the polynomial hierarchy, where the hardness of problems is assumed to grow with the number of quantifier alternations that are allowed to occur.

Although the definition of SF breaks with the paradigm of restricting quantifier prefixes, the known upper bound on the complexity of SF-satisfiability is again based on quantifier prefixes: Deciding whether an SF sentence $\varphi:=\exists\vec{\mathbf{z}}\,\forall\vec{\mathbf{x}}_{1}\exists\vec{\mathbf{y}}_{1}\ldots\forall\vec{\mathbf{x}}_{n}\exists\vec{\mathbf{y}}_{n}.\psi$ with quantifier-free $\psi$ is satisfiable requires a nondeterministic computing time that is at most $n$-fold exponential in the length of $\varphi$ (cf. Theorem 17 in [17]). On the one hand, we complement this result with a corresponding lower bound in the present paper. That is, we show that SF-satisfiability is indeed non-elementary. On the other hand, we derive a refined upper bound that is based on the degree $\partial$ of interaction of existential variables. An overview of the resulting hierarchy of complete problems is depicted in Figure 1. Intuitively, $\varphi$ exhibits a degree $\partial_{\varphi}=k$, if variables from $k$ distinct existential quantifier blocks interact. We say that two variables $x,y$ interact, if they occur together in at least one atom or if there is a third variable $z$ that interacts with both $x$ and $y$ (i.e. the property is transitive). For instance, in the SF sentence \forall x_{1}\exists y_{1}v_{1}\forall x_{2}\exists y_{2}v_{2}\forall x_{3}\exists y_{3}v_{3}.\;\bigl{(}P(x_{1},x_{2},x_{3})\wedge\neg Q(y_{1},y_{3})\bigr{)}\vee P(y_{2},v_{2},v_{3})\vee\neg Q(y_{3},v_{1}) the sets $\{y_{1},y_{3},v_{1}\}$ and $\{y_{2},v_{2},v_{3}\}$ form the maximal sets of interacting existential variables. Since each of these sets contains variables from at most two distinct quantifier blocks, the formula exhibits a degree $\partial=2$.

In Section 4.1, and in particular in Theorem 13, we observe that the satisfiability problem for $\text{SF}_{\partial\leq k}$—the set of all SF sentences $\varphi$ with $\partial_{\varphi}\leq k$—lies in $k$-NExpTime. It is worth mentioning that this result adequately accounts for the known complexity of MFO-satisfiability. For every MFO sentence $\varphi$ we trivially have $\partial_{\varphi}=1$, since all occurring predicate symbols have an arity of at most one. Theorem 13 entails that MFO-satisfiability is in NExpTime, which is well known. Still, this bound is not reproducible with the analysis of the complexity of SF-satisfiability conducted in [17].

Apparently, non-elementary satisfiability problems are not very widespread among the decidable fragments of classical fist-order logic known today. We show in Section 5 that SF falls into this category. To the present author’s knowledge, the only known companion in this respect is the fluted fragment (FL). Indeed, Pratt-Hartmann, Szwast, and Tendera show in [14] that satisfiability of fluted sentences with at most $2k$ variables is $k$-NExpTime-hard. Moreover, they argue that satisfiability of fluted sentences with at most $k$ variables lies in $k$-NExpTime. Although a significant gap between these lower and upper bounds remains to be closed, the fluted fragment seems to comprise a similar hierarchy of hard problems as SF does.

Another characteristic of SF is that it enjoys a small model property. More precisely, given an SF sentence $\varphi$, one can compute a positive integer $n$ that depends on the degree $\partial_{\varphi}$ and the length of $\varphi$ such that, if there is a model of $\varphi$ at all, then there also is a model whose domain contains at most $n$ elements. Many first-order fragments are known to enjoy a small model property. The BSR fragment and MFO are among the classical ones (see [3] for references). More recently defined fragments include the two-variable fragment (FO2) [12], [8], the fluted fragment (FL) [15], [16], [14], the guarded fragment (GF) [1], [7], the guarded negation fragment (GNF) [2], and the uniform one-dimensional fragment (UF1) [11]. While GNF and UF1 are incomparable, GNF extends GF, and UF1 can be considered as a generalization of FO2. Guarded fragments and the two-variable fragment have received quite some attention due to the fact that modal logics have natural translations into them. As a continuation of that theme, we shall see in Section 3.1 how classes of sentences enjoying a small model property can be effectively translated into subclasses of SF. During the translation process the length of formulas increases by a factor that is logarithmic in the size of small models of the original. One benefit of translating non-SF sentences into SF sentences is that in SF one can natively express concepts such as transitivity and basic counting quantifiers (Proposition 5). This is not always possible in other fragments enjoying a small model property. For example, transitivity cannot be expressed in FO2, GF, and FL.

Summing up, the main contributions are:

(i) Based on the novel concept of the degree of interaction of existential variables, we substantially refine the existing analysis of the time required to decide SF-satisfiability. More concretely, we show that a satisfiable SF sentence $\varphi$ with $\partial_{\varphi}=k$ has a model whose domain is of a size that is at most $k$-fold exponential in the length of $\varphi$ (Section 4, Theorem 13). With this refined approach we can close the complexity gap for the class of strongly separated sentences (Corollary 15) that was left open in [17]. Moreover, the complexity of MFO can be explained in the refined framework.

(ii) We complement the complexity analysis with corresponding lower bounds in two respects. We first derive a lower bound on the length of shortest BSR sentences that are equivalent to a given SF sentence (Section 4.2, Theorem 16). In Section 5, we prove $k$-NExpTime-hardness of satisfiability for the class of SF sentences $\varphi$ with $\partial_{\varphi}=k$ (Theorem 21). Since SF is in general defined without restrictions on the degree $\partial_{\varphi}$, our result implies that SF-satisfiability is non-elementary.

(iii) We devise a simple translation from classes of first-order sentences that enjoy a small model property into SF (Proposition 4). Moreover, we argue that SF can express basic counting quantifiers (Proposition 5).

In order to facilitate smooth reading, most proofs are only sketched in the main text and presented in full in the appendix. The present paper is the full version of the extended abstract [18].

2 Preliminaries

We mainly reuse the basic notions from [17]. We repeat the definition of necessary concepts and notation for the sake of completeness.

We consider first-order logic formulas. The underlying signature shall not be mentioned explicitly, but will become clear from the current context. For the distinguished equality predicate we use $\approx$. We follow the convention that negation binds strongest, that conjunction binds stronger than disjunction, and that all of the aforementioned bind stronger than implication. The scope of quantifiers shall stretch as far to the right as possible. By $\text{len}(\cdot)$ we denote a reasonable measure of the length of formulas satisfying $\text{len}(\varphi\rightarrow\psi)=\text{len}(\neg\varphi\vee\psi)$ and $\text{len}(\varphi\leftrightarrow\psi)=\text{len}((\neg\varphi\vee\psi)\wedge(\varphi\vee\neg\psi))$.

We write $\varphi(x_{1},\ldots,x_{m})$ to denote a formula $\varphi$ whose free variables form a subset of $\{x_{1},\ldots,x_{m}\}$. In all formulas we tacitly assume that no variable occurs freely and bound at the same time and that no variable is bound by two different occurrences of quantifiers, unless explicitly stated otherwise. For convenience, we sometimes identify tuples $\vec{\mathbf{x}}$ of variables with the set containing all the variables that occur in $\vec{\mathbf{x}}$. We write $\text{{vars}}(\varphi)$ to address the set of all variable symbols that occur in $\varphi$. Similarly, $\text{{consts}}(\varphi)$ denotes the set of all constant symbols in $\varphi$. We denote substitution by \varphi\bigl{[}x/t\bigr{]} if every free occurrence of $x$ in $\varphi$ is to be substituted with the term $t$.

A literal is an atom or a negated atom, and a clause is a disjunction of literals. We say that a formula is in conjunctive normal form (CNF), if it is a conjunction of clauses, possibly preceded by a quantifier prefix. A formula in CNF is Horn if every clause contains at most one non-negated literal. It is Krom if every clause contains at most two literals at all.

A sentence $\varphi:=\forall\vec{\mathbf{x}}_{1}\exists\vec{\mathbf{y}}_{1}\ldots\forall\vec{\mathbf{x}}_{n}\exists\vec{\mathbf{y}}_{n}.\psi$ is in standard form, if it is in negation normal form (i.e. every negation symbol occurs directly before an atom) and $\psi$ is quantifier free, contains exclusively the Boolean connectives $\wedge,\vee,\neg$, and does not contain non-constant function symbols. The tuples $\vec{\mathbf{x}}_{1}$ and $\vec{\mathbf{y}}_{n}$ may be empty, i.e. the quantifier prefix does not have to start with a universal quantifier, and it does not have to end with an existential quantifier. Moreover, we require that every variable occurring in the quantifier prefix does also occur in $\psi$.

As usual, we interpret a formula $\varphi$ with respect to given structures. A structure $\mathcal{A}$ consists of a nonempty universe $\mathfrak{U}_{\mathcal{A}}$ (also: domain) and interpretations $f^{\mathcal{A}}$ and $P^{\mathcal{A}}$ of all considered function and predicate symbols, respectively, in the usual way. Given a formula $\varphi$, a structure $\mathcal{A}$, and a variable assignment $\beta$, we write $\mathcal{A},\beta\models\varphi$ if $\varphi$ evaluates to true under $\mathcal{A}$ and $\beta$. We write $\mathcal{A}\models\varphi$ if $\mathcal{A},\beta\models\varphi$ holds for every $\beta$. The symbol $\mathrel{|}\joinrel\Relbar\joinrel\mathrel{|}$ denotes (semantic) equivalence of formulas, i.e. $\varphi\mathrel{|}\joinrel\Relbar\joinrel\mathrel{|}\psi$ holds whenever for every structure $\mathcal{A}$ and every variable assignment $\beta$ we have $\mathcal{A},\beta\models\varphi$ if and only if $\mathcal{A},\beta\models\psi$. We call two sentences $\varphi$ and $\psi$ equisatisfiable if $\varphi$ has a model if and only if $\psi$ has one.

A structure $\mathcal{A}$ is a substructure of a structure $\mathcal{B}$ (over the same signature) if (1) $\mathfrak{U}_{\mathcal{A}}\subseteq\mathfrak{U}_{\mathcal{B}}$, (2) $c^{\mathcal{A}}=c^{\mathcal{B}}$ for every constant symbol $c$, (3) $P^{\mathcal{A}}=P^{\mathcal{B}}\cap\mathfrak{U}_{\mathcal{A}}^{m}$ for every $m$-ary predicate symbol $P$, and (4) $f^{\mathcal{A}}(\mathfrak{a}_{1},\ldots,\mathfrak{a}_{m})=f^{\mathcal{B}}(\mathfrak{a}_{1},\ldots,\mathfrak{a}_{m})$ for every $m$-ary function symbol $f$ and every $m$-tuple $\langle\mathfrak{a}_{1},\ldots,\mathfrak{a}_{m}\rangle\in\mathfrak{U}_{\mathcal{A}}^{m}$. The following is a standard lemma, see, e.g., [5] for a proof.

Lemma 1** (Substructure lemma).**

Let $\varphi$ be a first-order sentence in prenex normal form without existential quantifiers and let $\mathcal{A}$ be a substructure of $\mathcal{B}$. $\mathcal{B}\models\varphi$ entails $\mathcal{A}\models\varphi$.

Lemma 2** (Miniscoping).**

Let $\varphi,\psi,\chi$ be arbitrary first-order formulas, and assume that $x$ does not occur freely in $\chi$.

\begin{array}[]{lcl}\exists x.(\varphi\vee\psi)&\mathrel{|}\joinrel\Relbar\joinrel\mathrel{|}&(\exists x_{1}.\varphi)\vee(\exists x_{2}.\psi)~{},\\ \exists x.(\varphi\circ\chi)&\mathrel{|}\joinrel\Relbar\joinrel\mathrel{|}&(\exists x.\varphi)\circ\chi~{},\\ \forall x.(\varphi\wedge\psi)&\mathrel{|}\joinrel\Relbar\joinrel\mathrel{|}&(\forall x_{1}.\varphi)\wedge(\forall x_{2}.\psi)~{},\\ \forall x.(\varphi\circ\chi)&\mathrel{|}\joinrel\Relbar\joinrel\mathrel{|}&(\forall x.\varphi)\circ\chi~{},\end{array}

where $\circ\in\{\wedge,\vee\}$.

We use the notation $[k]$ to abbreviate the set $\{1,\ldots,k\}$ for any positive integer $k$. Moreover, $\mathfrak{P}$ shall be used as the power set operator, i.e. $\mathfrak{P}S$ denotes the set of all subsets of a given set $S$. Finally, we need some notation for the tetration operation. We define ${2^{\uparrow k}(m)}$ inductively: ${2^{\uparrow 0}(m)}:=m$ and ${2^{\uparrow k+1}(m)}:=2^{\left({2^{\uparrow k}(m)}\right)}$.

3 The separated fragment

Let $\varphi$ be a first-order formula. We call two disjoint sets of variables $X$ and $Y$ separated in $\varphi$ if and only if for every atom $A$ occurring in $\varphi$ we have $\text{{vars}}(A)\cap X=\emptyset$ or $\text{{vars}}(A)\cap Y=\emptyset$.

Definition 3** (Separated fragment (SF), [17]).**

The separated fragment (SF) of first-order logic consists of all existential closures of prenex formulas without non-constant function symbols in which existentially quantified variables are separated from universally quantified ones. More precisely, SF consists of all first-order sentences with equality but without non-constant function symbols that are of the form $\exists\vec{\mathbf{z}}\,\forall\vec{\mathbf{x}}_{1}\exists\vec{\mathbf{y}}_{1}\ldots\forall\vec{\mathbf{x}}_{n}\exists\vec{\mathbf{y}}_{n}.\,\psi$, in which $\psi$ is quantifier-free, and in which the sets $\vec{\mathbf{x}}_{1}\cup\ldots\cup\vec{\mathbf{x}}_{n}$ and $\vec{\mathbf{y}}_{1}\cup\ldots\cup\vec{\mathbf{y}}_{n}$ are separated.

The tuples $\vec{\mathbf{z}}$ and $\vec{\mathbf{y}}_{n}$ may be empty, i.e. the quantifier prefix does not have to start with an existential quantifier and it does not have to end with an existential quantifier either.

Notice that the variables in $\vec{\mathbf{z}}$ are not subject to any restriction concerning their occurrences.

In [17] the authors show that the satisfiability problem for SF sentences (SF-satisfiability) is decidable. Before we start investigating the complexity issues related to SF-satisfiability, we elaborate on the expressiveness of SF.

3.1 Expressiveness

Every SF sentence is equivalent to a BSR sentence ([17], Lemma 6). We shall outline in Section 4 how to analyze the blow-up that we have to incur during this translation process and how it depends on the degree of interaction of existential variables. Since the BSR fragment enjoys a small model property (cf. Proposition 6), SF inherits the small model property from BSR. However, regarding the size of minimal models of satisfiable formulas, SF sentences are much more compact. While satisfiable BSR sentences have models whose domain is linear in the length of the formula, satisfiable SF sentences can enforce domains of a size that cannot be bounded from above by a finite tower of exponentials. We provide first evidence for this fact in Theorem 16, where we give a non-elementary lower bound on the length of equivalent BSR sentences. This lower bound even applies to the SF-Horn-Krom subfragment of SF. Moreover, we exploit the capability of SF sentences $\varphi$ to enforce models of $\partial_{\varphi}$-fold exponential size in the proof of the $k$-NExpTime-hardness of SF-satisfiability (for every $k\geq 1$).

Apart from compactness of representation, and from the perspective of satisfiability, all first-order fragments that enjoy small model properties share a common ground of expressiveness. Neglecting efficiency, every sentence $\varphi$ from such a fragment can be effectively translated into a (finite) propositional formula $\phi$ in such a way that from a satisfying variable assignment for $\phi$ one can straightforwardly reconstruct a (Herbrand) model of $\varphi$. The reason is simply that universal quantification can then be understood as finite conjunction (over a finite domain) and existential quantification can be conceived as finite disjunction.

The following proposition illustrates why SF is to some extent prototypical for first-order fragments that enjoy a small model property.

Proposition 4**.**

Consider any nonempty class $\mathcal{C}$ of first-order formulas without non-constant function symbols for which we know a computable mapping $f:\mathcal{C}\to\mathbb{N}$ such that every satisfiable $\varphi$ in $\mathcal{C}$ has a model of size at most $f(\varphi)$. Then there exists an effective translation $T$ from $\mathcal{C}$ into SF such that for every $\varphi\in\mathcal{C}$ (a) every model of $T(\varphi)$ is also a model of $\varphi$, (b) every model of $\varphi$ whose size is at most $f(\varphi)$ can be extended to a model of $T(\varphi)$ over the same domain, and (c) the length of $T(\varphi)$ lies in \mathcal{O}\bigl{(}\text{len}(\varphi)\cdot\log f(\varphi)\cdot\log\log f(\varphi)\bigr{)}.

Proof.

We outline the translation $T$ for some given input sentence $\varphi$, which we assume to be in negation normal form (without loss of generality). Let $m:=\lceil\log_{2}f(\varphi)\rceil$ and let $Q_{1},\ldots,Q_{m}$ be unary predicate symbols that do not occur in $\varphi$. For all terms $s,t$ we define $s\mathrel{\hat{\approx}}t$ as abbreviation of $\bigwedge_{i=1}^{m}Q_{i}(s)\leftrightarrow Q_{i}(t)$. In order to restrict the domain to $2^{m}$ elements, we conjoin the formula ${\chi_{\text{fin}}}:=\forall xy.\,x\!\mathrel{\hat{\approx}}\!y\rightarrow x\!\approx\!y$. Since in any structure $\mathcal{A}$ there are at most $2^{m}$ domain elements that can be distinguished by their membership in the sets $Q_{1}^{\mathcal{A}},\ldots,Q_{m}^{\mathcal{A}}$, it is clear that $\mathcal{A}\models{\chi_{\text{fin}}}$ entails $|\mathfrak{U}_{\mathcal{A}}|\leq 2^{m}$. Moreover, we observe the following property.

• ($*$)

Let $\mathcal{A}$ be any structure, let $\beta$ be any variable assignment over $\mathcal{A}$’s domain, and let $s,t$ be two terms. If $\mathcal{A}\models{\chi_{\text{fin}}}$ holds, then we get $\mathcal{A},\beta\models s\mathrel{\hat{\approx}}t$ if and only if $\mathcal{A},\beta\models s\approx t$.

This means, if we restrict our attention to domains with at most $2^{m}$ domain elements, we can now use a separated form of equality.

• ($**$)

Let $\psi$ be any first-order formula and let $v$ be some variable that does not occur in $\psi$. Then $\psi$ is equivalent to $\forall v.\,u\approx v$ \rightarrow\;\psi\bigl{[}u/v\bigr{]}.

We can transform $\varphi$ into an equivalent sentence $\varphi^{\prime}$ by consecutively replacing each subformula of the form $\exists y.\psi$ in $\varphi$ with \exists y\forall v.\;y\!\approx\!v\rightarrow\psi\bigl{[}y/v\bigr{]}, where we assume $v$ to be fresh (one fresh variable for every replaced subformula). Consequently, every atom in $\varphi^{\prime}$ that is not an equation contains exclusively universally quantified variables. Moreover, ($**$) implies that $\varphi$ and $\varphi^{\prime}$ are equivalent.

Let $\varphi^{\prime\prime}$ be the result of replacing all equations $y\approx v,v\approx y$ in $\varphi^{\prime}$ in which $y$ is existentially quantified and $v$ universally quantified with the formula $y\mathrel{\hat{\approx}}v$. We then set $\varphi_{\text{SF}}:={\chi_{\text{fin}}}\wedge\varphi^{\prime\prime}$. By ($*$), any model of $\varphi_{\text{SF}}$ is also a model of $\varphi$. Conversely, any model $\mathcal{A}$ of $\varphi$ that has at most $2^{m}$ domain elements can be converted into a model $\mathcal{B}$ of $\varphi_{\text{SF}}$ by defining the relations $Q_{1}^{\mathcal{B}},\ldots,Q_{m}^{\mathcal{B}}$ in an appropriate way. ∎

The $\varphi_{\text{SF}}$ in the above proof belongs to a subfragment of SF that we call strongly separated (cf. Definition 14) and whose satisfiability problem is complete for NExpTime (cf. Corollary 15).

Unfortunately, the translation methodology of Proposition 4 does not help in the quest for new decidable first-order fragments. The reason is simply that we already need arguments leading to a small model property before we can start the translation process, as we need information about the size of the models that have to be considered. Nevertheless, such translations can be useful in view of the expressiveness of SF that other first-order fragments, such as FO2, the fluted fragment, and GF, lack. For instance, SF sentences can naturally express the axioms of equivalence, most prominently, transitivity. Hence, fundamental and interesting properties of predicates that have to be assumed at the meta-level when dealing with less expressive logics can be formalized directly in SF. Moreover, basic counting quantifiers can be defined natively in SF and do not have to be introduced via special operators. More precisely, given any formula $\exists^{\geq n}y.\,\varphi$ with positive $n$ and without non-constant function symbols, its standard translation \exists y_{1}\ldots y_{n}.\bigwedge_{i=1}^{n}\varphi\bigl{[}y/y_{i}\bigr{]}\wedge\bigwedge_{i<j}y_{i}\!\not\approx\!y_{j} is not in conflict with the separateness conditions of SF’s definition, if the set $\{y_{1},\ldots,y_{n}\}$ is separated in $\varphi$ from the set of universally quantified variables.

Proposition 5**.**

Counting quantifiers $\exists^{\geq n}$ with positive integer $n$ are expressible in SF.

3.2 Basic complexity considerations

We first recall the well-known small model properties of SF’s subfragments BSR and MFO (see [3] for references).

Proposition 6**.**

Let $\varphi:=\exists\vec{\mathbf{z}}\,\forall\vec{\mathbf{x}}.\psi$ be a satisfiable BSR sentence, i.e. $\psi$ is quantifier free and does not contain non-constant function symbols. There is a model $\mathcal{A}\models\varphi$ such that |\mathfrak{U}_{\mathcal{A}}|\leq\max\bigl{(}|\vec{\mathbf{z}}|+|\text{{consts}}(\varphi)|,1\bigr{)}.

We make use of this property when we derive an upper bound on the size of small models for satisfiable SF sentences, as our approach will be based on an effective translation of SF sentences into equivalent BSR sentences.

Proposition 7**.**

Let $\varphi:=\exists\vec{\mathbf{z}}\,\forall\vec{\mathbf{x}}_{1}\exists\vec{\mathbf{y}}_{1}\ldots$ $\forall\vec{\mathbf{x}}_{n}\exists\vec{\mathbf{y}}_{n}.\psi$ be a satisfiable monadic sentence without equality and without non-constant function symbols, i.e. all predicate symbols in $\varphi$ are of arity $1$. Moreover, assume that $\varphi$ contains $k$ distinct predicate symbols. There is a model $\mathcal{A}\models\varphi$ such that $|\mathfrak{U}_{\mathcal{A}}|\leq 2^{k}$.

Notice that the shape of the quantifier prefix does not contribute to the upper bound.

The following lemma links bounds on the size of models with the computing time that is required to decide satisfiability.

Lemma 8** (cf. [3], Proposition 6.0.4).**

Let $\varphi$ be a first-order sentence in prenex normal form containing $n$ universally quantified variables. The question whether $\varphi$ has a model of cardinality $m$ can be decided nondeterministically in time p\bigl{(}m^{n}\cdot\text{len}(\varphi)\bigr{)} for some polynomial $p$.

With this lemma at hand, it is enough to prove a small model property for a given class of first-order sentences, in order to bound the worst-case time complexity of the corresponding satisfiability problem from above. This is exactly what the authors of [17] have done for SF.

Proposition 9** ([17], Theorem 17).**

Let $\varphi:=\exists\vec{\mathbf{z}}\,\forall\vec{\mathbf{x}}_{1}\exists\vec{\mathbf{y}}_{1}\ldots\forall\vec{\mathbf{x}}_{n}\exists\vec{\mathbf{y}}_{n}.\psi$ be an SF sentence for some quantifier-free $\psi$. There is some equivalent BSR sentence $\exists\vec{\mathbf{u}}\,\forall\vec{\mathbf{v}}.\psi^{\prime}$ in which the number of occurring constant symbols plus the number of existential quantifiers is at most \text{len}(\varphi)+n\cdot\text{len}(\varphi)\cdot\bigl{(}{2^{\uparrow n}(\text{len}(\varphi))}\bigr{)}^{n}. As a result, satisfiability of $\varphi$ can be decided nondeterministically in time that is at most $n$-fold exponential in $\text{len}(\varphi)$.

Clearly, applying this result to an MFO sentence substantially overshoots the actual worst-case time requirements. To stress it again, the notion of the degree of interaction is a remedy to this sort of inaccuracies, as we shall see in Section 4.

A special case that is worth considering, before we investigate the complexity of full SF, is the class of SF sentences that do not contain universal quantifiers. This species of formulas coincides with the purely existential fragment of first-order logic without non-constant function symbols, and it is a close relative of propositional logic. Recall that SAT is NP-complete [4], Horn-SAT is P-complete [10, 13], and 2SAT is NL-complete [9].

Proposition 10**.**

1. (i)

Satisfiability for the class of SF sentences without universal quantifiers is NP-complete. 2. (ii)

Satisfiability for the class of SF-Horn sentences without universal quantifiers is P-complete. 3. (iii)

Satisfiability for the class of SF-Krom sentences without universal quantifiers and without equality is NL-complete.

Proof sketch.

The proof of (i) – (iii) proceeds by reductions to the corresponding satisfiability problems for propositional logic and back. This is straightforwardly done by Skolemization as long as we consider only SF sentences without equality (cf. Lemma 26 in the appendix).

In the latter cases, we first Skolemize exhaustively, producing $\varphi_{\text{gnd}}$, which is ground and contains only Skolem constants and no non-constant function symbols. Then we use the standard trick to eliminate the equality predicate $\approx$. We introduce a fresh binary relation symbols $E$ and replace every equation $c\approx d$ with an atom $E(c,d)$. Moreover, we add axioms for reflexivity, symmetry, transitivity, and congruence. Of course, we do not use the universally quantified axioms but rather add their instances with respect to all the constant symbols that occur in $\varphi_{\text{gnd}}$. To avoid an exponential blow-up in the case of the congruence axioms, we only add the instances that affect non-equational atoms which really occur in $\varphi_{\text{gnd}}$.

Let $\phi$ be the propositional formula that results from $\varphi_{\text{gnd}}$ by replacing every ground atom $A$ with the propositional variable $p_{A}$. We observe that \text{len}(\phi)\in\mathcal{O}\bigl{(}\text{len}(\varphi)^{3}\bigr{)}. Moreover, if $\varphi$ is a Horn formula, then $\phi$ is Horn. Notice that the outlined elimination of equality does not preserve the Krom property. ∎

4 Translation of SF sentences into BSR sentences

In this section, we analyze the transformation process from SF into the BSR fragment from the perspective of the degree of interaction of existential variables. Our aim is to derive upper and lower bounds on the length of the resulting BSR-formulas. Roughly speaking, in the first phase of the translation process all quantifiers are moved inwards as far as possible (cf. the proof of Lemma 12). In order to do so, we first transform the sentence in question into a formula in CNF. After that, we employ the well-known rules of miniscoping (cf. Lemma 2), supplemented by the rule formulated in the following lemma.

Lemma 11**.**

Let $I$ and $K_{i}$, $i\in I$, be sets that are finite, nonempty, and pairwise disjoint. The elements of these sets serve as indices. Let

[TABLE]

be some first-order formula where the $\chi_{i}$ and the $\eta_{k}$ denote arbitrary subformulas that we treat as indivisible units in what follows. We say that $f:I\to\bigcup_{i\in I}K_{i}$ is a selection function if for every $i\in I$ we have $f(i)\in K_{i}$. We denote the set of all selection functions of this form by $\mathcal{F}$.

Then $\varphi$ is equivalent to $\varphi^{\prime}:=$

[TABLE]

Proof sketch.

The proof of this lemma follows a conceptually simple strategy. Using the distributivity of $\wedge$ over $\vee$, we first transform $\varphi$ into a disjunction of conjunctions of the indivisible units $\chi_{i}(\vec{\mathbf{z}})$ and $\eta_{k}(\vec{\mathbf{y}},\vec{\mathbf{z}})$. Then, exploiting the equivalences in Lemma 2, we push the existential quantifier block $\exists\vec{\mathbf{y}}$ inwards such that it only binds conjunctions of units $\eta_{k}(\vec{\mathbf{y}},\vec{\mathbf{z}})$. This is possible, because none of the variables in $\vec{\mathbf{y}}$ occurs in any of the $\chi_{i}(\vec{\mathbf{z}})$. From this point on, we treat the newly emerged subformulas $\exists\vec{\mathbf{y}}.\bigwedge_{k^{\prime}}\eta_{k^{\prime}}(\vec{\mathbf{y}},\vec{\mathbf{z}})$ as if they were indivisible. We then transform the formula back into a conjunction of disjunctions of indivisible units, this time using the distributivity of $\vee$ over $\wedge$. It then remains to show that the result of this transformation exhibits a highly redundant structure and is actually equivalent to $\varphi^{\prime}$. ∎

4.1 Degree of interaction of existential variables and the size of small models

Consider the formula $\varphi:=\exists\vec{\mathbf{z}}\,\forall\vec{\mathbf{x}}_{1}\exists\vec{\mathbf{y}}_{1}\ldots$ $\forall\vec{\mathbf{x}}_{n}\exists\vec{\mathbf{y}}_{n}.\psi$ in standard form in which $\psi$ is quantifier free and in which the sets $\vec{\mathbf{x}}:=\vec{\mathbf{x}}_{1}\cup\ldots\cup\vec{\mathbf{x}}_{n}$ and $\vec{\mathbf{y}}:=\vec{\mathbf{y}}_{1}\cup\ldots\cup\vec{\mathbf{y}}_{n}$ are separated. In addition, we assume that $\vec{\mathbf{x}}_{1}$ and $\vec{\mathbf{y}}_{1}$ are nonempty. The tuple $\vec{\mathbf{z}}$, on the other hand, may be empty.

For any $j\in[n]$ and any variable $y\in\vec{\mathbf{y}}_{j}$ we say that $y$ is a level-$j$ variable, denoted $\text{lvl}(y)=j$. For any nonempty set $Y\subseteq\vec{\mathbf{y}}$ of existentially quantified variables and any positive integer $k$ we say that $Y$ has degree $k$ in $\varphi$, denoted $\partial_{Y,\varphi}=k$, if $k$ is the maximal number of distinct variables $y_{1},\ldots,y_{k}\in Y$ that belong to different levels in $\varphi$, i.e. $\text{lvl}(y_{1})<\ldots<\text{lvl}(y_{k})$. We say that $\varphi$’s degree of interaction of existential variables (short: degree) is $k$, denoted $\partial_{\varphi}=k$, if $k$ is the smallest positive integer such that we can partition $\vec{\mathbf{y}}$ into $m>0$ parts $Y_{1},\ldots,Y_{m}$ that are all pairwise separated in $\varphi$ and for which k=\max\bigl{\{}k_{j}\bigm{|}\partial_{Y_{j},\varphi}=k_{j},1\leq j\leq m\bigr{\}}. Sentences $\varphi:=\exists\vec{\mathbf{z}}\,\forall\vec{\mathbf{x}}.\,\psi$ in standard form with quantifier-free $\psi$ are said to have degree zero, i.e. $\partial_{\varphi}=0$, if $\vec{\mathbf{x}}$ is empty and we define $\partial_{\varphi}=1$ if $\vec{\mathbf{x}}$ is nonempty.

Lemma 12**.**

Let $\varphi:=\exists\vec{\mathbf{z}}\,\forall\vec{\mathbf{x}}_{1}\exists\vec{\mathbf{y}}_{1}\ldots\forall\vec{\mathbf{x}}_{n}\exists\vec{\mathbf{y}}_{n}.\psi$ be an SF sentence of positive degree $\partial_{\varphi}$ in standard form. Let $\mathcal{L}_{\varphi}(\vec{\mathbf{y}})$ denote the set of all literals in $\varphi$ that contain at least one variable $y\in\vec{\mathbf{y}}:=\vec{\mathbf{y}}_{1}\cup\ldots\cup\vec{\mathbf{y}}_{n}$. There exists a sentence $\varphi_{\text{BSR}}=\exists\vec{\mathbf{z}}\,\exists\vec{\mathbf{u}}\,\forall\vec{\mathbf{v}}.\psi_{\text{BSR}}$ in standard form with quantifier-free $\psi_{\text{BSR}}$ that is equivalent to $\varphi$ and contains at most |\vec{\mathbf{z}}|+|\vec{\mathbf{y}}|\cdot\partial_{\varphi}\cdot\bigl{(}{2^{\uparrow\partial_{\varphi}}(|\mathcal{L}_{\varphi}(\vec{\mathbf{y}})|)}\bigr{)}^{\partial_{\varphi}} leading existential quantifiers.

Proof sketch.

Let $\vec{\mathbf{x}}:=\vec{\mathbf{x}}_{1}\cup\ldots\cup\vec{\mathbf{x}}_{n}$. We transform $\varphi$ into CNF and then apply Lemma 11 and the rules of miniscoping given in Lemma 2 to push all quantifier blocks inwards. Since the sets $\vec{\mathbf{x}}$ and $\vec{\mathbf{y}}$ are separated in $\varphi$, these operations can be performed in such a way that in the resulting formula $\varphi^{\prime}$ no universal quantifier lies within the scope of any existential quantifier (other than the ones in $\exists\vec{\mathbf{z}}$) and vice versa. After removing redundant parts from $\varphi^{\prime}$, the depth of nestings of existential quantifier blocks (interspersed with conjunctive connectives in $\varphi^{\prime}$’s syntax tree) can be upper bounded by $\partial_{\varphi}$. As a consequence, $\varphi^{\prime}$ contains at most ${2^{\uparrow\partial_{\varphi}}(|\mathcal{L}_{\varphi}(\vec{\mathbf{y}})|)}$ distinct subformulas that are of the form $\exists y.\psi^{\prime}$ and do not lie within the scope of any quantifier. After further transformations, we obtain a formula \varphi^{\prime\prime}:=\bigvee_{k}\bigl{(}\chi_{k}(\vec{\mathbf{x}})\wedge\bigwedge_{r_{k}}\eta_{r_{k}}(\vec{\mathbf{y}})\bigr{)} where the $r_{k}$ range over at most ${2^{\uparrow\partial_{\varphi}}(|\mathcal{L}_{\varphi}(\vec{\mathbf{y}})|)}$ indices. Moreover, every constituent $\bigwedge_{r_{k}}\eta_{r_{k}}$ in $\varphi^{\prime\prime}$ contains at most $|\vec{\mathbf{y}}|\cdot\sum_{k^{\prime}=1}^{\partial_{\varphi}}\prod_{d=k^{\prime}}^{\partial_{\varphi}}{2^{\uparrow d}(|\mathcal{L}_{\varphi}(\vec{\mathbf{y}})|)}$ occurrences of existential quantifiers. Since these existential quantifiers distribute over the topmost disjunction when we move them outwards to the front of the sentence $\varphi^{\prime\prime}$, and since the universal quantifiers in the $\chi_{k}$ may also be moved back outwards, one can show that $\varphi$ is equivalent to some BSR sentence with at most |\vec{\mathbf{y}}|\cdot\partial_{\varphi}\cdot\bigl{(}{2^{\uparrow\partial_{\varphi}}(|\mathcal{L}_{\varphi}(\vec{\mathbf{y}})|)}\bigl{)}^{\partial_{\varphi}} leading existential quantifiers. ∎

Proposition 6 now entails that any satisfiable SF-sentence $\varphi$ has a model of size at most

[TABLE]

Theorem 13**.**

Let $k$ be any positive integer. The satisfiability problem for the class of SF sentences $\varphi$ in standard form with degree $\partial_{\varphi}\!\leq\!k$ can be decided in nondeterministic $k$-fold exponential time.

Together with Proposition 10(i), this establishes the upper bounds depicted in Figure 1.

In cases where $\partial_{\varphi}=1$, Expression (1) simplifies to $\text{len}(\varphi)+\text{len}(\varphi)\cdot 2^{\text{len}(\varphi)}$. The syntactic class of sentences satisfying this property is called strongly separated in [17].

Definition 14** ([17]).**

Let $\varphi:=\forall\vec{\mathbf{x}}_{1}\exists\vec{\mathbf{y}}_{1}\ldots$ $\forall\vec{\mathbf{x}}_{n}\exists\vec{\mathbf{y}}_{n}.\psi$ be an SF sentence and assume that $\psi$ is quantifier free. We say that $\varphi$ belongs to the strongly separated fragment (SSF) if and only if the sets $\vec{\mathbf{x}}:=\vec{\mathbf{x}}_{1}\cup\ldots\cup\vec{\mathbf{x}}_{n}$ and $\vec{\mathbf{y}}_{1},\ldots,\vec{\mathbf{y}}_{n}$ are all pairwise separated in $\varphi$.

Since MFO and BSR sentences fall into this syntactic category, and since their decision problem is known to be NExpTime-hard, we obtain the following corollary.

Corollary 15**.**

The satisfiability problem for SSF is NExpTime-complete.

Notice that the presented method can explain the asymptotic complexity of MFO-satisfiability and yields a reasonable upper bound on the size of small models of satisfiable MFO sentences. This works in spite of the fact that monadic sentences may contain arbitrarily nested alternating quantifiers. This is a considerable improvement compared to the methods used in [17].

Let $\varphi$ be any SF sentence with the maximally possible degree $\partial_{\varphi}=n$, where $n$ is the number of occurring $\forall\exists$-alternations. Then the upper bound shown in Expression (1) regarding the number of elements in small models fits the corresponding result entailed by Proposition 9. As one consequence, Theorem 13 in the present paper subsumes Theorem 17 in [17]. Moreover, Corollary 15 improves the double exponential upper bound on SSF-satisfiability given in Theorem 15 in [17]. Finally, it is worth noticing that all SF sentences with the quantifier prefix $\exists^{*}\forall^{*}\exists^{*}\forall^{*}$ belong to the strongly separated fragment. Hence, Corollary 15 subsumes Theorem 14 in [17]. The latter stipulates NExpTime-completeness of SF sentences with quantifier prefix $\exists^{*}\forall^{*}\exists^{*}$. Clearly, the refined analysis based on the degree of interaction of existential variables, rather than the number of quantifier alternations, yields significantly tighter results in many cases.

4.2 Lower bounds on the length of equivalent BSR formulas

Before we derive lower bounds on the time that is required to decide SF-satisfiability in the worst case, we establish lower bounds on the length of the results of the translation from SF into the BSR fragment.

Theorem 16**.**

There is a class of SF sentences that are Horn and Krom such that for every positive integer $n$ the class contains a sentence $\varphi$ of degree $\partial_{\varphi}=n$ and with a length linear in $n$ for which any equivalent BSR sentence contains at least $\sum_{k=1}^{n}{2^{\uparrow k}(n)}$ leading existential quantifiers.

Proof sketch.

Recall that $[n]$ abbreviates the set $\{1,\ldots,n\}$ and that $\mathfrak{P}S$ denotes the power set of a given set $S$. Let $n\geq 1$ be some positive integer. Consider the following first-order sentence in which the sets $\{x_{1},\ldots,x_{n}\}$ and $\{y_{1},\ldots,y_{n}\}$ are separated:

[TABLE]

Notice that we change the orientation of the indices in the quantifier prefix in this proof.

In order to construct a particular model of $\varphi$, we inductively define the following sets: \mathcal{S}_{1}:=\bigl{\{}S\subseteq[4n]\bigm{|}|S|=2n\bigr{\}}, \mathcal{S}_{k+1}:=\bigl{\{}S\in\mathfrak{P}\mathcal{S}_{k}\bigm{|}|S|=\tfrac{1}{2}\cdot|\mathcal{S}_{k}|\bigr{\}} for every $k$, $1<k\leq n$. Hence, we observe

|\mathcal{S}_{1}|={{4n}\choose{2n}}\geq\bigl{(}\frac{4n}{2n}\bigr{)}^{2n}=2^{2n},

|\mathcal{S}_{2}|={{|\mathcal{S}_{1}|}\choose{|\mathcal{S}_{1}|/2}}\geq\bigl{(}\frac{|\mathcal{S}_{1}|}{|\mathcal{S}_{1}|/2}\bigr{)}^{|\mathcal{S}_{1}|/2}\geq 2^{2^{2n-1}},

$\qquad\vdots$

$|\mathcal{S}_{n}|={{|\mathcal{S}_{n-1}|}\choose{|\mathcal{S}_{n-1}|/2}}\geq 2^{2^{2^{\vdots^{2^{2n-1}-1}}-1}}\geq{2^{\uparrow n}(n+1)}$.

We now define the structure $\mathcal{A}$ as follows:

• •

\mathfrak{U}_{\mathcal{A}}:=\bigcup_{k=1}^{n}\bigl{\{}\mathfrak{a}^{(k)}_{S},\mathfrak{b}^{(k)}_{S}\bigm{|}S\in\mathcal{S}_{k}\bigr{\}},

• •

P_{i}^{\mathcal{A}}:=\bigl{\{}\langle\mathfrak{a}^{(1)}_{S_{1}},\ldots,\mathfrak{a}^{(n)}_{S_{n}}\rangle\in\mathfrak{U}_{\mathcal{A}}^{n}\bigm{|}i\in S_{1}\in S_{2}\in\ldots\in S_{n}\bigr{\}} for $i=1,\ldots,4n$, and

• •

Q_{i}^{\mathcal{A}}:=\bigl{\{}\langle\mathfrak{b}^{(1)}_{S_{1}},\ldots,\mathfrak{b}^{(n)}_{S_{n}}\rangle\in\mathfrak{U}_{\mathcal{A}}^{n}\bigm{|}i\in S_{1}\in S_{2}\in\ldots\in S_{n}\bigr{\}} for $i=1,\ldots,4n$.

One can easily show that $\mathcal{A}$ is a model of $\varphi$. Moreover, employing a game-theoretic argument, one can show the following property:

• ($*$)

the substructure induced by $\mathcal{A}$’s domain after removing at least one of the $\mathfrak{b}^{(k)}_{S}$ does not satisfy $\varphi$.

We know that $\mathfrak{U}_{\mathcal{A}}$ contains at least $\sum_{k=1}^{n}{2^{\uparrow k}(n)}$ elements of the form $\mathfrak{b}^{(k)}_{S}$.

Using ($*$) and the substructure lemma, one can argue that any BSR sentence $\varphi_{*}$ that is semantically equivalent to $\varphi$ must contain at least $\sum_{k=1}^{n}{2^{\uparrow k}(n)}$ leading existential quantifiers.

The key idea is that $\varphi_{*}$, which is satisfied by $\mathcal{A}$, must contain one existential quantifier for each and every $\mathfrak{b}^{(k)}_{S}$. Otherwise, there would be one $\mathfrak{b}^{(k)}_{S}$, call it $\mathfrak{b}_{*}$, such that we could remove $\mathfrak{b}_{*}$ from $\mathcal{A}$’s domain and any tuple $\langle\ldots,\mathfrak{b}_{*},\ldots\rangle$ from the sets $Q_{i}^{\mathcal{A}}$, and the resulting structure would then still be a model of $\varphi_{*}$. But this would contradict ($*$).

Since every atom $Q_{i}(y_{1},\ldots,y_{n})$ contains $n$ variables from existential quantifier blocks that are separated by universal ones, the degree $\partial_{\varphi}$ of $\varphi$ is $n$. Moreover, $\varphi$ can easily be transformed into a CNF that is Horn and Krom at the same time.

Hence, the theorem holds. ∎

Theorem 16 entails that there is no elementary upper bound on the length of the BSR sentences that result from an equivalence-preserving transformation of SF sentences into BSR. On the other hand, by Lemma 12, there is an elementary upper bound, if we only consider SF sentences up to a certain degree.

5 Lower bounds on the computational complexity of SF-satisfiability

In this section we establish lower bounds on the worst-case time complexity of SF-satisfiability. Our arguments will be based on a particular form of bounded domino (or tiling) problems developed by Grädel (see [6] and [3], Section 6.1.1). By $\mathbb{Z}_{t}$ we denote the set of integers $\{0,\ldots,t-1\}$ for any positive $t\geq 1$.

Definition 17** ([3], Definition 6.1.1).**

A domino system $\mathfrak{D}:=\langle\mathcal{D},\mathcal{H},\mathcal{V}\rangle$ is a triple where $\mathcal{D}$ is a finite set of tiles and $\mathcal{H},\mathcal{V}\subseteq\mathcal{D}\times\mathcal{D}$ are binary relations determining the allowed horizontal and vertical neighbors of tiles, respectively. Consider the torus $\mathbb{Z}_{t}^{2}:=\mathbb{Z}_{t}\times\mathbb{Z}_{t}$ and let $\overline{D}:=D_{0}\ldots D_{n-1}$ be a word over $\mathcal{D}$ of length $n\leq t$. The letters of $\overline{D}$ represent tiles. We say that $\mathfrak{D}$ tiles the torus $\mathbb{Z}_{t}^{2}$ with initial condition $\overline{D}$ if and only if there exists a mapping $\tau:\mathbb{Z}_{t}^{2}\to\mathcal{D}$ such that for every $\langle x,y\rangle\in\mathbb{Z}_{t}^{2}$ the following conditions hold, where “$+1$” denotes increment modulo $t$.

1. (a)

If $\tau(x,y)=D$ and $\tau(x+1,y)=D^{\prime}$, then $\langle D,D^{\prime}\rangle\in\mathcal{H}$. 2. (b)

If $\tau(x,y)=D$ and $\tau(x,y+1)=D^{\prime}$, then $\langle D,D^{\prime}\rangle\in\mathcal{V}$. 3. (c)

$\tau(i,0)=D_{i}$ for $i=0,\ldots,n-1$.

Definition 18** ([3], Definition 6.1.5).**

Let $T:\mathbb{N}\to\mathbb{N}$ be a function and let $\mathfrak{D}:=\langle\mathcal{D},\mathcal{H},\mathcal{V}\rangle$ be a domino system. The problem $\text{DOMINO}(\mathfrak{D},T(n))$ is the set of those words $\overline{D}$ over the alphabet $\mathcal{D}$ for which $\mathfrak{D}$ tiles $\mathbb{Z}_{T(|\overline{D}|)}^{2}$ with initial condition $\overline{D}$.

Domino problems provide a convenient way of deriving lower bounds via reductions. Suppose we are given some well-behaved time bound $T(n)$ that grows sufficiently fast. Further assume there is a reasonable translation from $\text{DOMINO}(\mathfrak{D},T(n))$ into some problem $\mathcal{L}$ where the length of the results is upper bounded by a function $g(n)$. It follows that the time required to solve the hardest instances of $\mathcal{L}$ lies in \Omega\bigl{(}T(h(n))\bigr{)}, where $h(n)$ may be conceived as an inverse of $g(n)$ from an asymptotic point of view. The next proposition formalizes this observation.

Proposition 19** ([3], Theorem 6.1.8).**

Let $T:\mathbb{N}\!\to\!\mathbb{N}$ be a time-constructible function with $T(c^{\prime}n)^{2}\in o(T(n))$ for some constant $c^{\prime}>0$ and let $\mathcal{L}$ be a problem such that for every domino system $\mathfrak{D}$ we have $\text{DOMINO}(\mathfrak{D},T(n))\leq_{g(n)}\mathcal{L}$, i.e. $\text{DOMINO}(\mathfrak{D},T(n))$ is polynomially reducible to $\mathcal{L}$ via length order g(n) (cf. Definition 6.1.7 in [3]). Moreover, let $h:\mathbb{N}\to\mathbb{N}$ be a function such that $h(d\cdot g(n))\in\mathcal{O}(n)$ for any positive $d$. There exists a positive constant $c>0$ such that $\mathcal{L}\not\in\text{NTIME}(T(c\cdot h(n)))$.

Subsections 5.1 and 5.2 are devoted to the purpose of outlining the following reductions.

Lemma 20**.**

1. (i)

Fix some positive integer $k>0$ and let $\mathfrak{D}$ be an arbitrary domino system. Let Sat($\text{SF}_{\partial\leq k}$) be the set containing all satisfiable SF sentences whose degree $\partial$ is at most $k$. We have \text{DOMINO}\bigl{(}\mathfrak{D},{2^{\uparrow k}(n)}\bigr{)}\leq_{n\cdot\log n}\text{Sat(\text{SF}_{\partial\leq k})}. 2. (ii)

Fix some positive integer $m>1$ and let $\mathfrak{D}$ be an arbitrary domino system. Let Sat(SF) be the set containing all satisfiable SF sentences. We have $\text{DOMINO}(\mathfrak{D},{2^{\uparrow n}(m)})\leq_{n^{2}\cdot\log n}\text{Sat(SF)}$.

Having these reduction results at hand, Proposition 19 implies the sought lower bounds on SF-satisfiability for classes of sentences with bounded degree and the class of unbounded SF sentences.

Theorem 21**.**

There are positive constants $c,d>0$ for which

[TABLE]

and

[TABLE]

These lower bounds also hold if we do not allow equality in SF, see Section 5.3. The remainder of Section 5 is devoted to the formalization of sufficiently large tori in SF and to the translation from a given domino system $\mathfrak{D}=\langle\mathcal{D},\mathcal{H},\mathcal{V}\rangle$ (for nonempty $\mathcal{D},\mathcal{H},\mathcal{V}$) plus an initial condition $\overline{D}$ into an SF sentence $\varphi$ such that $\varphi$ is satisfiable if and only if $\overline{D}\in\text{DOMINO}(\mathfrak{D},T_{i}(|\overline{D}|))$ with $T_{1}(n)={2^{\uparrow\kappa}(n)}$ for any given $\kappa>0$ and $T_{2}(n)={2^{\uparrow n}(\mu)}$ for any given $\mu>1$.

5.1 Enforcing a large domain

The following description gives a somewhat simplified view. Technical details will follow.

A crucial part in the reduction is that a grid of size $t\times t$ has to be encoded, where $t$ defines the required computing time and we assume $t:={2^{\uparrow\kappa}(\mu)}$ for positive integers $\kappa$ and $\mu>1$ that we consider as parameters of the construction.

Every point $p$ on the grid is represented by a pair $p=\langle x,y\rangle$, where each of the coordinates $x$ and $y$ is represented by a bit string of length \log\bigl{(}{2^{\uparrow\kappa}(\mu)}\bigr{)}={2^{\uparrow\kappa-1}(\mu)}. Given a bit string $\overline{b}$, we represent the $j$-th bit $b_{j}$ by the truth value of the atom $J({\underline{\kappa}},\overline{b},j)$, where ${\underline{\kappa}}$ is the constant used to address the topmost level of a hierarchy of $\kappa+1$ sets of indices. The crux of our approach is that we have to enforce the existence of sufficiently many indices $j$, namely ${2^{\uparrow\kappa-1}(\mu)}$ many, to address the single bits of $\overline{b}$. Again, we address each of these indices as a bit string, this time of length ${2^{\uparrow\kappa-2}(\mu)}$.

Thus, we proceed in an inductive fashion, building up a hierarchy of indices with $\kappa+1$ levels. The lowest level, level zero, is inhabited by $\mu$ indices, which we represent as constants with distinct values. For every $\ell\geq 1$ any index $j$ on the $\ell$-th level is represented by a bit string consisting of ${2^{\uparrow\ell-1}(\mu)}$ bits, i.e. the $\ell$-th level of the index hierarchy contains ${2^{\uparrow\ell}(\mu)}$ indices. The $i$-th bit of an $\ell$-th-level index $j$ corresponds to the truth value of the atom $J({\underline{\ell}},j,i)$.

Example 22**.**

Assume $\mu=2$ and $\kappa=3$.

index set of number

level indices of indices

0 $\{\mathfrak{c}_{1},\mathfrak{c}_{2}\}\hfill$ 2

1 $\{00,01,10,11\}\hfill$ 4

2 $\{0000,0001,\ldots,1111\}\hfill$ 16

3 $\{0,1\}^{16}$ $65536$

On every index level, the bits of one index are indexed by the indices from the previous level. We illustrate this for the word $1010$ on all levels from 2 down to 0. The bits of 1010 on level two are indexed by bit strings from level one, each of them having a length of two. The bits of the indices of level one are themselves indexed by objects of level zero which are some values $\mathfrak{c}_{1},\mathfrak{c}_{2}$ assigned to the constants $c_{1},c_{2}$. To improve readability, we connect the bits of words by dashes.

level 2: 1 — —— — 0 — —— — 1 — —— — 0

$\uparrow$

$\uparrow$

$\uparrow$

$\uparrow$

level 1: 0 — 0

0 — 1

1 — 0

1 — 1

$\uparrow$

$\uparrow$

$\uparrow$

$\uparrow$

$\uparrow$

$\uparrow$

$\uparrow$

$\uparrow$

level 0: $\mathfrak{c}_{1}$

$\mathfrak{c}_{2}$

$\mathfrak{c}_{1}$

$\mathfrak{c}_{2}$

$\mathfrak{c}_{1}$

$\mathfrak{c}_{2}$

$\mathfrak{c}_{1}$

$\mathfrak{c}_{2}$

For technical reasons the number of indices per level grows slightly slower than described above (cf. Lemma 24). The described index hierarchies can be encoded by SF formulas with the quantifier prefix $\exists^{*}(\forall\exists)^{\kappa}$ that have a length that is polynomial in $\kappa$ and $\mu$. We use the following constant and predicate symbols with the indicated meaning:

${\underline{0}},{\underline{1}},\ldots,{\underline{\kappa}}$ constants denoting the levels from [math] to $\kappa$,

$c_{1},\ldots,c_{\mu}$ denote the indices at level 0,

$d_{1},\ldots,d_{\kappa}$ $d_{\ell}$ is the min. index at level $\ell$,

$e_{1},\ldots,e_{\kappa}$ $e_{\ell}$ is the max. index at level $\ell$,

$L({\underline{\ell}},j)$ index $j$ belongs to level $\ell$,

$\text{MinIdx}({\underline{\ell}},j)$ $j$ is a min. index at level $\ell$,

$\text{MaxIdx}({\underline{\ell}},j)$ $j$ is a max. index at level $\ell$,

$J({\underline{\ell}},j,i,b)$ the $i$-th bit of the index $j$ at level $\ell$ is $b$,

$J^{*}({\underline{\ell}},j,i,b)$ $b=1$ indicates that all the bits of the index $j$ that

are less significant than $j$’s $i$-th bit are 1,

$\text{Succ}({\underline{\ell}},j,j^{\prime})$ $j^{\prime}$ is the successor index of $j$ at level $\ell$.

On every level we establish an ordering over the indices of that level. We use the usual ordering on natural numbers encoded in binary. Moreover, we formalize the usual successor relation on these numbers by the predicate Succ.

One difficulty that we encounter is that we cannot assert the existence of successors simply by adding $\forall j\exists j^{\prime}.\,\text{Succ}({\underline{\ell}},j,j^{\prime})$, as $j$ and $j^{\prime}$ would not be separated. Therefore, we fall back on a trick: we start from the equivalent formula $\forall j\exists\widetilde{j}j^{\prime}.\,j\!\approx\!\widetilde{j}\wedge\text{Succ}({\underline{\ell}},\widetilde{j},j^{\prime})$, and replace the atom $j\!\approx\!\widetilde{j}$ by a subformula $\text{eq}^{\ell}_{j,\widetilde{j}}$ in which $j$ and $\widetilde{j}$ are separated and which expresses a certain similarity between $j$ and $\widetilde{j}$ instead of identity. However, we specify the hierarchy of indices in a sufficiently strong way such that the similarity expressed by $\text{eq}^{\ell}_{j,\widetilde{j}}$ actually coincides with identity.

Next, we formalize the described index hierarchies in $\text{SF}_{\partial\leq\kappa}$. Every formula is accompanied by a brief description of its purpose. We shall try to use as few non-Horn sentences as possible.

[TABLE]

[TABLE]

[TABLE]

Until now, we have only introduced sentences that can easily be transformed into SF sentences in Horn form, existential variables are separated from universal ones, as all quantifiers occur with positive polarity, and consequents of implications are (conjunctions of) literals.

Regarding the length of the above sentences, we observe the following:

• •

$\text{len}(\psi_{1})\in\mathcal{O}(\kappa^{2}\log\kappa)$

• •

$\text{len}(\psi_{2}),\ldots,\text{len}(\psi_{7}),\text{len}(\psi_{9}),\ldots,\text{len}(\psi_{15})\in\mathcal{O}(\kappa\log\kappa)$

• •

\text{len}(\psi_{8})\in\mathcal{O}\bigl{(}\mu(\log\kappa+\log\mu)\bigr{)}

• •

\text{len}\bigl{(}\text{eq}^{1}_{j,j^{\prime}}\bigr{)}\in\mathcal{O}\bigl{(}\mu(\log\kappa+\log\mu)\bigr{)}

• •

\text{len}\bigl{(}\text{eq}^{\ell}_{j,j^{\prime}}\bigr{)}\in\mathcal{O}(\log\kappa)+\text{len}\bigl{(}\text{eq}^{1}_{j,j^{\prime}}\bigr{)}

• •

\text{len}(\psi_{16})\in\mathcal{O}\bigl{(}\kappa^{2}\log\kappa+\kappa\mu(\log\kappa+\log\mu)\bigr{)}

In total, this yields $\text{len}(\psi_{1}\wedge\ldots$ \wedge\psi_{16})\in\mathcal{O}\bigl{(}\kappa^{2}\log\kappa+\kappa\mu(\log\kappa+\log\mu)\bigr{)}.

The following three sentences do not produce Horn formulas when transformed into CNF. They serve the purpose of removing spurious elements from the model. In particular, $\chi_{3}$ is essential to enforce large models for $\kappa\geq 2$.

[TABLE]

Notice that $\chi_{3}$ is (almost) an SF sentence, since the $\forall\widetilde{i}$ turns into a $\exists\widetilde{i}$ as soon as we bring the sentence into prenex normal form. Regarding the length of $\chi_{1},\chi_{2},\chi_{3}$, we observe $\text{len}(\chi_{1})\in\mathcal{O}(\log\kappa+\mu\log\mu)$, $\text{len}(\chi_{2})\in\mathcal{O}(\kappa\log\kappa)$, and \text{len}(\chi_{3})\in\mathcal{O}\bigl{(}\kappa^{2}\log\kappa+\kappa\mu(\log\kappa+\log\mu)\bigr{)}. Hence, we overall have \text{len}(\chi_{1}\wedge\chi_{2}\wedge\chi_{3})\in\mathcal{O}\bigl{(}\kappa^{2}\log\kappa+\kappa\mu(\log\kappa+\log\mu)\bigr{)}.

Consider any model $\mathcal{A}$ of $\psi_{1}\wedge\ldots$ $\wedge\psi_{16}\wedge\chi_{1}\wedge\chi_{2}\wedge\chi_{3}$.

Definition 23**.**

We define the following sets and relations: \mathcal{I}_{\ell}:=\bigl{\{}\mathfrak{a}\in\mathfrak{U}_{\mathcal{A}}\mid\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a}]\models L({\underline{\ell}},j)\bigr{\}} for every $\ell=0,\ldots,\kappa$; ${\prec_{\ell}}\subseteq\mathcal{I}_{\ell}\times\mathcal{I}_{\ell}$ for every $\ell=0,\ldots,\kappa$ such that $\mathfrak{a}\prec_{\ell}\mathfrak{a}^{\prime}$ holds if and only if $\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},j^{\prime}{\mathop{\mapsto}}\mathfrak{a}^{\prime}]\models\text{Succ}({\underline{\ell}},j,j^{\prime})$.

Lemma 24**.**

For every $\ell=1,\ldots,\kappa$ we have $|\mathcal{I}_{\ell}|=p$ where $p:=2^{|\mathcal{I}_{\ell-1}|-1}+1={2^{\uparrow\ell}(\mu-1)}+1$. Moreover, there is a unique chain $\mathfrak{a}_{1}\prec_{\ell}\ldots\prec_{\ell}\mathfrak{a}_{p}$ comprising all elements in $\mathcal{I}_{\ell}$.

Leaving out the non-Horn parts $\chi_{1},\chi_{2},\chi_{3}$ renders the lemma invalid for $\ell>1$. On the other hand, for $\kappa=1$ the sentence $\psi_{1}\wedge\ldots\wedge\psi_{16}$—which can be transformed into an equivalent Horn sentence—has only models $\mathcal{A}$ for which $\mathcal{I}_{1}$ contains at least $2^{\mu-1}+1$ elements. Notice that this could be used to derive ExpTime-hardness of satisfiability for the class of Horn SF sentences of degree $1$. But such lower bounds are already known for the Horn subfragments of MFO and of the BSR fragment, which are proper subsets of SF’s Horn subfragment.

5.2 Formalizing a tiling of the torus

In order to formalize a given domino problem $\mathfrak{D}=\langle\mathcal{D},\mathcal{H},\mathcal{V}\rangle$ and an initial condition $\overline{D}$, we introduce the following constant and predicate symbols:

$H(x,y,x^{\prime},y^{\prime})$ $\langle x^{\prime},y^{\prime}\rangle$ is the horiz. neighbor of $\langle x,y\rangle$,

i.e. $x^{\prime}=x+1$ (mod ${2^{\uparrow\kappa}(\mu-1)}+1$) and $y^{\prime}=y$,

$V(x,y,x^{\prime},y^{\prime})$ $\langle x^{\prime},y^{\prime}\rangle$ is the vert. neighbor of $\langle x,y\rangle$,

${\underline{D}}(x,y)$ $\langle x,y\rangle$ is tiled with $D\in\mathcal{D}$,

$f_{1},\ldots,f_{|\overline{D}|}$ constants addressing points $\langle 0,0\rangle,\ldots,\langle|\overline{D}|-1,0\rangle$.

With the ideas we have seen when formalizing the index hierarchy, it is now fairly simple to formalize the torus. For instance, the following sentence makes sure that every point that is not on the “edge” of the torus has a horizontal neighbor.

[TABLE]

The next sentence, on the other hand, makes sure that the rules of the domino system $\mathfrak{D}$ are obeyed.

[TABLE]

Proceeding this way, the formalization $\eta$ of a domino system in SF requires a length in \mathcal{O}\bigl{(}\widehat{n}\log\widehat{n}\bigr{)}, where $\widehat{n}:=\max\{\kappa,\mu,|\overline{D}|,|\mathcal{D}|^{2}\}$.

Lemma 25**.**

Assume that $\mathcal{D}$, $\mathcal{H}$, and $\mathcal{V}$ are nonempty and let $\mathcal{A}$ be a model of the sentence $\psi_{1}\wedge\ldots\wedge\psi_{16}\wedge\chi_{1}\wedge\chi_{2}\wedge\chi_{3}\wedge\eta$. $\mathcal{A}$ induces a tiling $\tau$ of $\mathbb{Z}_{t}^{2}$ with initial condition $\overline{D}:=D_{1},\ldots,D_{n}$, where $t:={2^{\uparrow\kappa}(\mu-1)}+1$.

5.3 Replacing the equality predicate

Since SF can express reflexivity, symmetry, transitivity, and congruence properties, it is easy to formulate an SF sentence without equality that is equisatisfiable to $\psi_{1}\wedge\ldots\wedge\psi_{16}\wedge\chi_{1}\wedge\chi_{2}\wedge\chi_{3}\wedge\eta$ and uses atoms $E(s,t)$ instead of $s\approx t$. In addition to replacing equational atoms as indicated, we add the usual axioms concerning the fresh predicate symbol $E$. Overall, the additional formulas have a length that lies in \mathcal{O}\bigl{(}\kappa\log\kappa+|\mathcal{D}|\log|\mathcal{D}|\bigr{)}.

Consequently, the hardness result that we have obtained for SF with equality can be directly transferred to SF without equality. Moreover, notice that all the above formulas can be transformed into Horn form. Hence, one could also replace $\approx$ by $E$ in hardness proofs for the Horn subfragment of SF.

6 Conclusion

We stress in this paper that an analysis of the computational complexity of satisfiability problems can greatly benefit from an analysis of how variables occur together in atoms instead of exclusively considering the number of occurring quantifier alternations. What we have not yet taken into account is the Boolean structure of sentences. This may widen the scope of our methods considerably and may moreover help understand where the hardness of satisfiability problems stems from.

Consider a quantified Boolean formula $\varphi:=\forall\vec{\mathbf{x}}_{1}\exists\vec{\mathbf{y}}_{1}\ldots\forall\vec{\mathbf{x}}_{n}\exists\vec{\mathbf{y}}_{n}.\psi$ with quantifier-free $\psi$. All satisfiable formulas of this shape together form a hard problem residing on the $n$-th level of the polynomial hierarchy. But what if, for instance, $\psi$ has the form \bigl{(}\bigwedge_{i}K_{i}\bigr{)}\wedge\bigl{(}\bigvee_{j}L_{j}\bigr{)}, where the $K_{i}$ and the $L_{j}$ are literals and none of the existential variables in $\bigwedge_{i}K_{i}$ occurs in $\bigvee_{j}L_{j}$? Since Boolean variables cannot jointly occur in atoms, $\varphi$ can be transformed into the equivalent formula $\exists\vec{\mathbf{y}}_{1}\ldots\vec{\mathbf{y}}_{n}\forall\vec{\mathbf{x}}_{1}\ldots\vec{\mathbf{x}}_{n}.\psi$ by application of the rules of miniscoping (cf. Lemma 2). Apparently, $\varphi$ belongs to a class of QBF sentences that resides on the first level of the polynomial hierarchy rather than on the $n$-th.

Perhaps it is time to reconsider some of the definitions that are based on the shape of quantifier prefixes alone.

Acknowledgments

The author would like to thank the anonymous reviewers for valuable hints and suggestions.

Appendix

Appendix A Details regarding Section 3.2

Lemma 26**.**

1. (i)

Satisfiability for the class of SF sentences $\varphi$ without universal quantifiers and without equality can be decided nondeterministically in \text{poly}\bigl{(}\text{len}(\varphi)\bigr{)} time. 2. (ii)

Satisfiability for the class of SF-Horn sentences $\varphi$ without universal quantifiers and without equality can be decided deterministically in \text{poly}\bigl{(}\text{len}(\varphi)\bigr{)} time. 3. (iii)

Satisfiability for the class of SF-Krom sentences $\varphi$ without universal quantifiers and without equality can be decided nondeterministically using space that is logarithmic in $\text{len}(\varphi)$.

Proof.

We show that we can reduce the above SF-satisfiability problems to the respective satisfiability problems for propositional logic and vice versa.

Let $\varphi$ be a first-order sentence without non-constant function symbols that does not contain any universal quantifiers. Skolemization of all its existential quantifiers leads to the equisatisfiable ground sentence $\varphi_{\text{gnd}}$ in which every atom has the shape $P(c_{1},\ldots,c_{m})$. Let $A_{1},\ldots,A_{k}$ be a complete enumeration of all the atoms—without duplicates—that occur in $\varphi_{\text{gnd}}$. Let $q_{1},\ldots,q_{k}$ be a list of pairwise distinct propositional variables. We construct the propositional formula $\phi$ from $\varphi_{\text{gnd}}$ by replacing every atom $A_{i}$ with $q_{i}$. Clearly, any model of $\mathcal{A}$ of $\varphi_{\text{gnd}}$ induces a model $\mathcal{B}$ of $\phi$: $\mathcal{B}\models q_{i}$ if and only if $\mathcal{A}\models A_{i}$. Conversely, any model $\mathcal{B}^{\prime}$ of $\phi$ induces a Herbrand model $\mathcal{A}^{\prime}$ of $\varphi$: $\mathcal{A}^{\prime}\models A_{i}$ if and only if $\mathcal{B}^{\prime}\models q_{i}$. Consequently, deciding satisfiability of $\varphi$ can be reduced to deciding satisfiability of $\phi$. Moreover, we observe the following properties.

1. (a)

$\text{len}(\phi)\leq\text{len}(\varphi)$. 2. (b)

If $\varphi$ is a Horn formula, then $\phi$ is Horn. 3. (c)

If $\varphi$ is a Krom formula, then $\phi$ is Krom. ∎

Lemma 27**.**

There is an effective translation $T$ from the class of SF sentences with equality but without universal quantifiers into the class of ground first-order sentences without equality such that for every $\varphi$ from the former class we have that

1. (a)

every model of $T(\varphi)$ is a model of $\varphi$, 2. (b)

every model of $\varphi$ can be extended to a model of $T(\varphi)$ over the same domain, 3. (c)

\text{len}(T(\varphi))\in\mathcal{O}\bigl{(}\text{len}(\varphi)^{3}\bigr{)}, 4. (d)

If $\varphi$ is Horn, then $T(\varphi)$ is Horn as well.

Proof.

We describe the translation $T$ informally. Let $\varphi$ be some SF sentence that contains equality but no universal quantifiers. Let $\varphi_{\text{Sk}}$ be the result of Skolemizing the leading existential quantifier block in $\varphi$. Notice that $\varphi_{\text{Sk}}$ neither contains quantifiers nor non-constant function symbols. Let $E$ be a binary predicate symbol that does not occur in $\varphi_{\text{Sk}}$. We construct the following ground formulas:

[TABLE]

Let $\psi_{\text{cong}}$ be the conjunction of all ground formulas of the form $E(c_{1},d_{1})\wedge\ldots\wedge E(c_{m},d_{m})\wedge P(c_{1},\ldots,c_{m})\;\rightarrow\;P(d_{1},\ldots,d_{m})$ where $c_{1},d_{1},\ldots,c_{m},d_{m}\in\text{{consts}}(\varphi_{\text{Sk}})$ and $P$ is an $m$-ary predicate symbol in $\varphi_{\text{Sk}}$. We write $\psi^{\prime}_{\text{cong}}$ to denote the restriction of $\psi_{\text{cong}}$ to formulas $E(c_{1},d_{1})\wedge\ldots\wedge E(c_{m},d_{m})\wedge P(c_{1},\ldots,c_{m})\;\rightarrow\;P(d_{1},\ldots,d_{m})$ whose constituents $P(c_{1},\ldots,c_{m})$ and $P(d_{1},\ldots,d_{m})$ actually occur in $\varphi_{\text{Sk}}$.

Let $\varphi^{\prime}$ be the result of replacing every equation $c\approx d$ in $\varphi_{\text{Sk}}$ with the atom $E(c,d)$.

Claim I: $\varphi_{\text{Sk}}$ is satisfiable if and only if $\varphi^{\prime}\wedge\varphi_{\text{refl}}\wedge\varphi_{\text{symm}}\wedge\varphi_{\text{trans}}\wedge\varphi_{\text{cong}}$ is satisfiable.

Proof: Let $\mathcal{A}$ be a model of $\varphi_{\text{Sk}}$. By the Substructure Lemma, we may assume that $\mathcal{A}$’s universe is \bigl{\{}c^{\mathcal{A}}\bigm{|}c\in\text{{consts}}(\varphi_{\text{Sk}})\bigr{\}}. We now construct a model $\mathcal{B}\models\varphi^{\prime}\wedge\varphi_{\text{refl}}\wedge\varphi_{\text{symm}}\wedge\varphi_{\text{trans}}\wedge\varphi_{\text{cong}}$ from $\mathcal{A}$. We take over $\mathcal{A}$’s domain and its interpretation of the predicate symbols and constant symbols in $\varphi_{\text{Sk}}$. We define $E$’s interpretation under $\mathcal{B}$ such that E^{\mathcal{B}}:=\bigl{\{}\langle\mathfrak{a},\mathfrak{a}\rangle\bigm{|}\mathfrak{a}\in\mathfrak{U}_{\mathcal{A}}\bigr{\}}. Hence, for all $c,d\in\text{{consts}}(\varphi_{\text{Sk}})$ we observe $\mathcal{B}\models E(c,d)$ if and only if $\mathcal{B}\models c\approx d$. Consequently, $\mathcal{B}$ must be a model of $\varphi_{\text{Sk}}$ and $\varphi^{\prime}\wedge\varphi_{\text{refl}}\wedge\varphi_{\text{symm}}\wedge\varphi_{\text{trans}}\wedge\varphi_{\text{cong}}$.

Let $\mathcal{B}^{\prime}$ be a model of $\varphi^{\prime}\wedge\varphi_{\text{refl}}\wedge\varphi_{\text{symm}}\wedge\varphi_{\text{trans}}\wedge\varphi_{\text{cong}}$. By the Substructure Lemma, we may assume that $\mathcal{B}^{\prime}$’s universe is \mathfrak{U}_{\mathcal{B}^{\prime}}=\bigl{\{}c^{\mathcal{B}^{\prime}}\bigm{|}c\in\text{{consts}}(\varphi^{\prime})\bigr{\}}. We now construct a model $\mathcal{A}^{\prime}\models\varphi_{\text{Sk}}$ from $\mathcal{B}^{\prime}$. Because of $\mathcal{B}^{\prime}\models\varphi_{\text{refl}}\wedge\varphi_{\text{symm}}\wedge\varphi_{\text{trans}}\wedge\varphi_{\text{cong}}$, we know that $E^{\mathcal{B}^{\prime}}$ is a congruence relation over $\mathfrak{U}_{\mathcal{B}^{\prime}}$. We define the universe of $\mathcal{A}^{\prime}$ to be the quotient set $\mathfrak{U}_{\mathcal{A}^{\prime}}:=\mathfrak{U}_{\mathcal{B}^{\prime}}/_{E^{\mathcal{B}^{\prime}}}$. Moreover, we define $c^{\mathcal{A}^{\prime}}:=[c^{\mathcal{B}^{\prime}}]_{E^{\mathcal{B}^{\prime}}}$ for every $c\in\text{{consts}}(\varphi_{\text{Sk}})$. For every congruence class $[\mathfrak{a}]_{E^{\mathcal{B}^{\prime}}}$ we know that two domain elements $d^{\mathcal{B}^{\prime}},e^{\mathcal{B}^{\prime}}\in[\mathfrak{a}]_{E^{\mathcal{B}^{\prime}}}$ are indistinguishable by the relations $P^{\mathcal{B}^{\prime}}$ for which $P$ occurs in $\varphi^{\prime}$. Therefore, we can use the following definition for every $m$-ary predicate symbol $P$ in $\varphi^{\prime}$ (including $E$): P^{\mathcal{A}^{\prime}}:=\bigl{\{}\bigl{\langle}[\mathfrak{a}_{1}]_{E^{\mathcal{B}^{\prime}}},\ldots,[\mathfrak{a}_{m}]_{E^{\mathcal{B}^{\prime}}}\bigr{\rangle}\bigm{|}\langle\mathfrak{a}_{1},\ldots,\mathfrak{a}_{m}\rangle\in P^{\mathcal{B}^{\prime}}\bigr{\}}. This yields $\mathcal{A}^{\prime}\models\varphi^{\prime}$ and for all $c,d\in\text{{consts}}(\varphi^{\prime})$ we observe $\mathcal{A}^{\prime}\models E(c,d)$ if and only if $\mathcal{A}^{\prime}\models c\approx d$. Hence, $\mathcal{A}^{\prime}\models\varphi_{\text{Sk}}$. $\Diamond$

It now remains to show equisatisfiability of $\varphi^{\prime}\wedge\varphi_{\text{refl}}\wedge\varphi_{\text{symm}}\wedge\varphi_{\text{trans}}\wedge\varphi_{\text{cong}}$ and $\varphi^{\prime}\wedge\varphi_{\text{refl}}\wedge\varphi_{\text{symm}}\wedge\varphi_{\text{trans}}\wedge\varphi^{\prime}_{\text{cong}}$. The direction from left to right is obvious.

Claim II: Any model $\mathcal{A}\models\varphi^{\prime}\wedge\varphi_{\text{refl}}\wedge\varphi_{\text{symm}}\wedge\varphi_{\text{trans}}\wedge\varphi^{\prime}_{\text{cong}}$ gives rise to a model $\mathcal{B}\models\varphi^{\prime}\wedge\varphi_{\text{refl}}\wedge\varphi_{\text{symm}}\wedge\varphi_{\text{trans}}\wedge\varphi_{\text{cong}}$.

Proof: Let $P(c_{1},\ldots,c_{m})$ and $P(d_{1},\ldots,d_{m})$ be two atoms that occur in $\varphi^{\prime}$. We observe the following property:

• ($*$)

If $E^{\mathcal{A}}$ contains the pairs $\langle c_{1},d_{1}\rangle,\ldots,\langle c_{m},d_{m}\rangle$, then $\mathcal{A}\models\psi^{\prime}_{\text{cong}}$ entails that $\mathcal{A}\models P(c_{1},\ldots,c_{m})$ holds if and only if $\mathcal{A}\models P(d_{1},\ldots,d_{m})$ does.

We define $\mathcal{B}$ such that $\mathfrak{U}_{\mathcal{B}}:=\mathfrak{U}_{\mathcal{A}}$, $E^{\mathcal{B}}:=E^{\mathcal{A}}$, and $c^{\mathcal{B}}:=c^{\mathcal{A}}$ for every $c\in\text{{consts}}(\varphi^{\prime})$. Moreover, for every $m$-ary predicate symbol $P$ occurring in $\varphi^{\prime}$ and every tuple $\langle\mathfrak{a}_{1},\ldots,\mathfrak{a}_{m}\rangle\in\mathfrak{U}_{\mathcal{B}}$ we set $\langle\mathfrak{a}_{1},\ldots,\mathfrak{a}_{m}\rangle\in P^{\mathcal{B}}$ if and only if there is some atom $P(c_{1},\ldots,c_{m})$ in $\varphi^{\prime}$ for which we have $\langle c_{1}^{\mathcal{B}},\mathfrak{a}_{1}\rangle,\ldots,\langle c_{m}^{\mathcal{B}},\mathfrak{a}_{m}\rangle\in E^{\mathcal{B}}$. Due to ($*$), we know that $\mathcal{B}\models\varphi^{\prime}$ still holds. By construction of $\mathcal{B}$, we moreover observe $\mathcal{B}\models\varphi_{\text{refl}}\wedge\varphi_{\text{symm}}\wedge\varphi_{\text{trans}}\wedge\varphi_{\text{cong}}$. $\Diamond$

We set $T(\varphi):=\varphi^{\prime}\wedge\varphi_{\text{refl}}\wedge\varphi_{\text{symm}}\wedge\varphi_{\text{trans}}\wedge\varphi^{\prime}_{\text{cong}}$. It is easy to see that if $\varphi$ is Horn then $T(\varphi)$ is Horn as well. Moreover, the length of $T(\varphi)$ is upper bounded by k\cdot\bigl{(}\text{len}(\varphi^{\prime})+|\text{{consts}}(\varphi_{\text{Sk}})|^{3}+\text{len}(\varphi^{\prime})\cdot|\text{At}(\varphi_{\text{Sk}})|^{2}\bigr{)} for some positive integer $k$, where $\text{At}(\varphi_{\text{Sk}})$ denotes the set of all non-equational atoms that occur in $\varphi_{\text{Sk}}$. ∎

Proposition 10**.**

1. (i)

Satisfiability for the class of SF sentences without universal quantifiers is NP-complete. 2. (ii)

Satisfiability for the class of SF-Horn sentences without universal quantifiers is P-complete. 3. (iii)

Satisfiability for the class of SF-Krom sentences without universal quantifiers and without equality is NL-complete.

Proof.

The membership in the respective complexity classes is settled in Lemmas 26 and 27. It remains to reduce the respective SAT problems to the corresponding satisfiability problems for SF.

Let $\phi^{\prime}$ be some propositional sentence and let $q_{1},\ldots,q_{k}$ be a complete list of all propositional variables occurring in $\phi^{\prime}$ (without duplicates). Let $c_{1},\ldots,c_{k}$ be pairwise distinct constant symbols. We construct the first-order sentence $\varphi^{\prime}$ from $\phi^{\prime}$ by replacing every $q_{i}$ by the atom $P(c_{i})$. By similar arguments as we have used in the proof of Lemma 26, we can show that $\phi^{\prime}$ is satisfiable if and only if $\varphi^{\prime}$ is satisfiable. Moreover, we observe the following properties.

1. (a)

\text{len}(\varphi)\in\mathcal{O}\bigl{(}\text{len}(\phi)\bigr{)}. 2. (b)

If $\phi$ is a Horn formula, then $\varphi^{\prime}$ is Horn. 3. (c)

If $\phi$ is a Krom formula, then $\varphi$ is Krom. ∎

Appendix B Details regarding Section 4

Lemma 11**.**

Let $I$ and $K_{i}$, $i\in I$, be sets that are finite, nonempty, and pairwise disjoint. The elements of these sets serve as indices. Let

[TABLE]

be some first-order formula where the $\chi_{i}$ and the $\eta_{k}$ denote arbitrary subformulas that we treat as indivisible units in what follows. We say that $f:I\to\bigcup_{i\in I}K_{i}$ is a selection function if for every $i\in I$ we have $f(i)\in K_{i}$. We denote the set of all selection functions of this form by $\mathcal{F}$.

$\varphi$ is equivalent to

[TABLE]

Proof.

For the sake of readability we sometimes reuse variables in different occurrences of quantifiers in this proof. Using distributivity of $\wedge$ over $\vee$, we transform $\varphi$ into an equivalent disjunction of conjunctions:

[TABLE]

Since the existential quantifier block distributes over the topmost disjunction, we can move this block inwards and obtain the equivalent formula

[TABLE]

At this point, we employ distributivity of $\vee$ over $\wedge$ to transform this result into an equivalent conjunction of disjunctions $\varphi^{\prime\prime}:=\bigwedge_{j}\bigvee_{\ell}\psi_{j,\ell}$ in which for every index $j$ and every pair $\langle T,f\rangle\in(\mathfrak{P}I)\times\mathcal{F}$ there is exactly one $\ell$ such that

• •

either $\psi_{j,\ell}=\chi_{i}$ for some $i\in T$

• •

or $\psi_{j,\ell}=\exists\vec{\mathbf{y}}.\bigwedge_{i\in I\setminus T}\eta_{f(i)}(\vec{\mathbf{y}},\vec{\mathbf{z}})$.

In order to show that $\varphi^{\prime\prime}$ is semantically equivalent to $\varphi^{\prime}$, we prove the following claims.

Claim I: Every disjunction $\bigvee_{\ell}\psi_{j,\ell}$ in $\varphi^{\prime\prime}$ is subsumed by a disjunction

[TABLE]

for some nonempty $S\subseteq I$.

Proof: Fix some index $j$ and consider $\bigvee_{\ell}\psi_{j,\ell}$. We set S:=\bigl{\{}i\in I\bigm{|}\text{\psi_{j,\ell}=\chi_{i}$for some$\ell}\bigr{\}}. Consider the set $\overline{S}:=I\setminus S$. By definition of $S$, we know that none of the $\chi_{i}$ with $i\in\overline{S}$ is a constituent of $\bigvee_{\ell}\psi_{j,\ell}$. For every selection function $f\in\mathcal{F}$ there is some disjunct

[TABLE]

in (2) of which we know that none of the $\chi_{i}$ in it has been picked as constituent of $\bigvee_{\ell}\psi_{j,\ell}$ when constructing $\varphi^{\prime\prime}$. Hence, due to the definition of $\varphi^{\prime\prime}$, there must be some $\ell_{*}$ such that $\psi_{j,\ell_{*}}=\exists\vec{\mathbf{y}}.\bigwedge_{i\in I\setminus\overline{S}}\eta_{f(i)}(\vec{\mathbf{y}},\vec{\mathbf{z}})$, where $I\setminus\overline{S}=S$.

Consequently, $\bigvee_{\ell}\psi_{j,\ell}$ is subsumed by $\psi^{\prime}_{S}$. $\Diamond$

Claim II: Each of the subsuming disjunctions $\psi^{\prime}_{S}$ in Claim I is indeed equivalent to some disjunction $\bigvee_{\ell}\psi_{j,\ell}$ in $\varphi^{\prime\prime}$.

Proof: Fix some nonempty $S_{*}\subseteq I$ and consider $\psi^{\prime}_{S_{*}}$. We obtain the equivalent disjunction $\psi_{*}$ from the disjuncts in (2) as follows. For every $T\subseteq I$ with nonempty $T\cap S_{*}$ we pick one of the $\chi_{i}$ with $i\in T\cap S_{*}$ as constituent of $\psi_{*}$. For every $T\subseteq I$ for which $T\cap S_{*}$ is empty and any $f\in\mathcal{F}$ we pick $\exists\vec{\mathbf{y}}.\bigwedge_{i\in I\setminus T}\eta_{f(i)}(\vec{\mathbf{y}},\vec{\mathbf{z}})$ as constituent of $\psi_{*}$. Since $S_{*}$ is nonempty, $T$ must be a proper subset of $I$ and thus $I\setminus T$ is also nonempty.

For every constituent of the form $\exists\vec{\mathbf{y}}.\bigwedge_{i\in T^{\prime}}\eta_{f(i)}(\vec{\mathbf{y}},\vec{\mathbf{z}})$ that belongs to the disjunction $\psi_{*}$ we know that $S_{*}\subseteq T^{\prime}$. Hence, $\psi_{*}$ is of the form

[TABLE]

for certain sets $S^{\prime}_{j}\subseteq I\setminus S_{*}$. Among the $S^{\prime}_{j}$ is, in particular, the empty set, originating from $T=I\setminus S_{*}$. In this case, we have S^{\prime}_{j}=\bigl{(}I\setminus T\bigr{)}\setminus S_{*}=\bigl{(}I\setminus(I\setminus S_{*})\bigr{)}\setminus S_{*}=\emptyset. Hence, we can equivalently transform $\psi_{*}$ into

[TABLE]

By the absorption axiom of Boolean algebra, we finally obtain the equivalent disjunction

[TABLE]

Thus, the claimed equivalence holds.

We have not yet explicitly explained why the first subformula $\bigvee_{i\in S_{*}}\chi_{i}(\vec{\mathbf{z}})$ of $\psi_{*}$ covers $S_{*}$ completely. But this is easy to see, when one takes the singleton sets $T=\{i\}$ for every $i\in S_{*}$ into account, for which we pick the $\chi_{i}$ as a constituents of $\psi_{*}$. $\Diamond$

This completes the proof of the lemma. ∎

Lemma 12**.**

Let $\varphi:=\exists\vec{\mathbf{z}}\,\forall\vec{\mathbf{x}}_{1}\exists\vec{\mathbf{y}}_{1}\ldots\forall\vec{\mathbf{x}}_{n}\exists\vec{\mathbf{y}}_{n}.\psi$ be an SF sentence of positive degree $\partial_{\varphi}$ in standard form. Let $\mathcal{L}_{\varphi}(\vec{\mathbf{y}})$ denote the set of all literals in $\varphi$ that contain at least one variable $y\in\vec{\mathbf{y}}:=\vec{\mathbf{y}}_{1}\cup\ldots\cup\vec{\mathbf{y}}_{n}$. There exists a sentence $\varphi_{\text{BSR}}=\exists\vec{\mathbf{z}}\,\exists\vec{\mathbf{u}}\,\forall\vec{\mathbf{v}}.\psi_{\text{BSR}}$ in standard form with quantifier-free $\psi_{\text{BSR}}$ that is equivalent to $\varphi$ and contains at most |\vec{\mathbf{z}}|+|\vec{\mathbf{y}}|\cdot\partial_{\varphi}\cdot\bigl{(}{2^{\uparrow\partial_{\varphi}}(|\mathcal{L}_{\varphi}(\vec{\mathbf{y}})|)}\bigr{)}^{\partial_{\varphi}} leading existential quantifiers.

Proof.

For convenience, we pretend that $\vec{\mathbf{z}}$ is empty. The argument works for nonempty $\vec{\mathbf{z}}$ as well. Let $\vec{\mathbf{x}}:=\vec{\mathbf{x}}_{1}\cup\ldots\cup\vec{\mathbf{x}}_{n}$. We transform $\varphi$ into an equivalent CNF formula of the form

[TABLE]

where $I$ and the $K_{i}$ are finite, pairwise disjoint sets of indices, the subformulas $\chi_{i}$ are disjunctions of literals, and the $L_{k}$ are literals. By Lemma 11, we can construct an equivalent formula of the form

[TABLE]

where $\mathcal{F}$ is the set of all selection functions over the index sets $K_{i}$, $i\in I$. For the sake of readability we sometimes reuse variables in different occurrences of quantifiers in this proof. Applying ordinary miniscoping, we may move inward the universal quantifier block $\forall\vec{\mathbf{x}}_{n}$ and thus obtain

[TABLE]

We can now iterate these two steps in an alternating fashion until all quantifier blocks have been moved inwards in the described way. The constituents of the result \varphi^{(3)}:=\bigwedge_{q}\Bigl{(}\chi^{(3)}_{q}\vee\bigvee_{p}\eta^{(3)}_{qp}\Bigr{)} of this process have the form

[TABLE]

where the $S_{\ell_{1},\ldots,\ell_{n}-1}$ are certain subsets of $I$, and

[TABLE]

where the $K_{\ell^{\prime}_{1},\ldots,\ell^{\prime}_{n-1}}$ are certain subsets of $\bigcup_{i\in I}K_{i}$.

By definition of $\partial_{\varphi}$, we may assume that there is some positive integer $m$ and a partition of the set $\vec{\mathbf{y}}$ into $m$ nonempty subsets $Y_{1},\ldots,Y_{m}$ such that $Y_{1},\ldots,Y_{m}$ are all pairwise separated in $\varphi$ and for every $j$, $1\leq j\leq m$, we have $\partial_{Y_{j}}\leq\partial_{\varphi}$. Since the sets $Y_{1},\ldots,Y_{m}$ are pairwise separated in $\varphi$, we may partition the set $\mathcal{L}_{\varphi}(\vec{\mathbf{y}})$ into subsets $\mathcal{L}_{\varphi}(Y_{1}),\ldots,\mathcal{L}_{\varphi}(Y_{m})$ such that each $\mathcal{L}_{\varphi}(Y_{j})$ contains exactly the literals in $\varphi$ that contain at least one variable from $Y_{j}$. This means, we can rewrite every $\eta^{(3)}_{qp}$ into the form

[TABLE]

where the sets $K^{1}_{\ell^{\prime}_{1},\ldots,\ell^{\prime}_{n-1}},\ldots,K^{m}_{\ell^{\prime}_{1},\ldots,\ell^{\prime}_{n-1}}$ constitute a partition of $K_{\ell^{\prime}_{1},\ldots,\ell^{\prime}_{n-1}}$. (Some of these parts may be empty.) We then observe the following equivalences.

[TABLE]

For every $\eta^{(4)}_{qp}$, we call the result of the above transformation $\eta^{(5)}_{qp}$. In cases where the set $\vec{\mathbf{y}}_{i}\cap Y_{j}$ is empty, the existential quantifier block vanishes. For every $j\in[m]$ there are at most $\partial_{Y_{j}}$ nonempty sets $\vec{\mathbf{y}}_{i}\cap Y_{j}$. Hence, every $\eta^{(5)}_{qp}$ contains at most $\partial_{\varphi}$ nested existential quantifier blocks that are separated by in-between conjunctive connectives in the syntax tree.

We obtain $\varphi^{(5)}$ from $\varphi^{(3)}$ by replacing every constituent $\eta^{(3)}_{qp}$ with the corresponding $\eta^{(5)}_{qp}$ after applying the idempotence axioms of Boolean Algebra exhaustively to remove redundant conjuncts.

Let \kappa:=\max\bigl{\{}|\mathcal{L}_{\varphi}(Y_{j})|\bigm{|}j\in[m]\bigr{\}}. Due to the idempotence axioms, the following upper bounds can be shown inductively for any positive integer $d$, starting from $d=1$: Modulo idempotence, there are at most ${2^{\uparrow d}(\kappa)}$ formulas of the form

[TABLE]

For the sentence \varphi^{(5)}=\bigwedge_{q}\Bigl{(}\chi^{(3)}_{q}\vee\bigvee_{p}\eta^{(5)}_{qp}\Bigr{)} this means that it contains at most ${2^{\uparrow\partial_{\varphi}}(\kappa)}$ distinct subformulas (not occurrences thereof!) that are of the form $\exists y.\psi^{\prime}$ and do not lie within the scope of any quantifier. We treat every such subformula $\exists y.\psi^{\prime}$ and every subformula $\chi^{(3)}_{q}$ as indivisible unit and, employing distributivity of $\wedge$ over $\vee$, transform $\varphi^{(5)}$ into a disjunction of conjunctions \varphi^{(6)}:=\bigvee_{s}\Bigl{(}\bigwedge_{r_{1}}\chi^{(6)}_{r_{1}}\wedge\bigwedge_{r_{2}}\eta^{(6)}_{r_{2}}\Bigr{)} where the $\chi^{(6)}_{r_{1}}$ have the same shape as the $\chi^{(3)}_{q}$, and the $\eta^{(6)}_{r_{2}}$ are of the form

[TABLE]

for a certain $j$ and certain indices $i_{1},\ldots,i_{\partial_{Y_{j}}}$ with $1\leq i_{1}<\ldots<i_{\partial_{Y_{j}}}\leq n$, all depending on $r_{2}$.

Due to previous observations, we know that, modulo idempotence, $r_{2}$ ranges over at most ${2^{\uparrow\partial_{\varphi}}(\kappa)}$ indices. Moreover, any $\ell_{k}$ in any $\eta^{(6)}_{r_{2}}$ ranges over at most ${2^{\uparrow\partial_{\varphi}-k}(\kappa)}$ indices. Consequently, every constituent $\bigwedge_{r_{2}}\eta^{(6)}_{r_{2}}$ in $\varphi^{(6)}$ contains at most $\max_{i,j}|\vec{\mathbf{y}}_{i}\cap Y_{j}|\cdot\sum_{k^{\prime}=1}^{\partial_{\varphi}}\prod_{d=k^{\prime}}^{\partial_{\varphi}}{2^{\uparrow d}(\kappa)}$ occurrences of existential quantifiers.

Since these existential quantifiers distribute over the topmost disjunction when we move them outwards to the front of the sentence $\varphi^{(6)}$, and since the universal quantifiers in the $\chi^{(6)}_{q}$ may also be moved back outwards, we have shown that $\varphi$ is equivalent to some BSR sentence with at most |\vec{\mathbf{y}}|\cdot\partial_{\varphi}\cdot\bigl{(}{2^{\uparrow\partial_{\varphi}}(\kappa)}\bigl{)}^{\partial_{\varphi}} leading existential quantifiers. ∎

Appendix C Details regarding Section 4.2

Theorem 16**.**

There is a class of SF sentences that are Horn and Krom such that for every positive integer $n$ the class contains a sentence $\varphi$ of degree $\partial_{\varphi}=n$ and with a length linear in $n$ for which any equivalent BSR sentence contains at least $\sum_{k=1}^{n}{2^{\uparrow k}(n)}$ leading existential quantifiers.

Proof.

Let $n\geq 1$ be some positive integer. Consider the following first-order sentence in which the sets $\{x_{1},\ldots,x_{n}\}$ and $\{y_{1},\ldots,y_{n}\}$ are separated:

[TABLE]

Notice that we change the orientation of the indices in the quantifier prefix in this proof.

In order to construct a particular model of $\varphi$, we inductively define the following sets: \mathcal{S}_{1}:=\bigl{\{}S\subseteq[4n]\bigm{|}|S|=2n\bigr{\}}, \mathcal{S}_{k+1}:=\bigl{\{}S\in\mathfrak{P}\mathcal{S}_{k}\bigm{|}|S|=\tfrac{1}{2}\cdot|\mathcal{S}_{k}|\bigr{\}} for every $k>1$. Hence, we observe that

|\mathcal{S}_{1}|\;=\;{{4n}\choose{2n}}\;\geq\;\bigl{(}\frac{4n}{2n}\bigr{)}^{2n}\;=\;2^{2n},

|\mathcal{S}_{2}|\;=\;{{|\mathcal{S}_{1}|}\choose{|\mathcal{S}_{1}|/2}}\;\geq\;\bigl{(}\frac{|\mathcal{S}_{1}|}{|\mathcal{S}_{1}|/2}\bigr{)}^{|\mathcal{S}_{1}|/2}\;=\;2^{|\mathcal{S}_{1}|/2}\;\geq\;2^{2^{2n}/2}\;=\;2^{2^{2n-1}},

$\qquad\vdots$

$|\mathcal{S}_{n}|\;=\;{{|\mathcal{S}_{n-1}|}\choose{|\mathcal{S}_{n-1}|/2}}\;\geq\;2^{|\mathcal{S}_{n-1}|/2}\;\geq\;2^{2^{2^{\vdots^{2^{2n-1}-1}}-1}}\;\geq\;{2^{\uparrow n}(2n-(n-1))}\;=\;{2^{\uparrow n}(n+1)}$,

where the inequality ${n\choose k}\geq(n/k)^{k}$ can be found in T. Cormen et al. Introduction to Algorithms (McGraw-Hill Higher Education, 2nd edition, 2001.), page 1097, for example.

Having the sets $\mathcal{S}_{k}$, we now define the structure $\mathcal{A}$ as follows:

• •

\mathfrak{U}_{\mathcal{A}}:=\bigcup_{k=1}^{n}\bigl{\{}\mathfrak{a}^{(k)}_{S},\mathfrak{b}^{(k)}_{S}\bigm{|}S\in\mathcal{S}_{k}\bigr{\}},

• •

P_{i}^{\mathcal{A}}:=\bigl{\{}\langle\mathfrak{a}^{(1)}_{S_{1}},\ldots,\mathfrak{a}^{(n)}_{S_{n}}\rangle\in\mathfrak{U}_{\mathcal{A}}^{n}\bigm{|}i\in S_{1}\in S_{2}\in\ldots\in S_{n}\bigr{\}} for $i=1,\ldots,4n$, and

• •

Q_{i}^{\mathcal{A}}:=\bigl{\{}\langle\mathfrak{b}^{(1)}_{S_{1}},\ldots,\mathfrak{b}^{(n)}_{S_{n}}\rangle\in\mathfrak{U}_{\mathcal{A}}^{n}\bigm{|}i\in S_{1}\in S_{2}\in\ldots\in S_{n}\bigr{\}} for $i=1,\ldots,4n$.

Clearly, for any choice of $S_{1},\ldots,S_{n}$ and every $i$, $1\leq i\leq 4n$, we have

[TABLE]

For any other choice of tuples $\langle\mathfrak{c}_{1},\ldots,\mathfrak{c}_{n}\rangle$, i.e. there do not exist sets $S_{1}\in\mathcal{S}_{1},\ldots,S_{n}\in\mathcal{S}_{n}$ such that $\langle\mathfrak{c}_{1},\ldots,\mathfrak{c}_{n}\rangle$ equals $\langle\mathfrak{a}^{(1)}_{S_{1}},\ldots,\mathfrak{a}^{(n)}_{S_{n}}\rangle$ or $\langle\mathfrak{b}^{(1)}_{S_{1}},\ldots,\mathfrak{b}^{(n)}_{S_{n}}\rangle$, we observe $\mathcal{A},[x_{1}{\mathop{\mapsto}}\mathfrak{c}_{1},\ldots,x_{n}{\mathop{\mapsto}}\mathfrak{c}_{n}]\not\models P_{i}(x_{1},\ldots,x_{n})$ and $\mathcal{A},[y_{1}{\mathop{\mapsto}}\mathfrak{c}_{1},\ldots,y_{n}{\mathop{\mapsto}}\mathfrak{c}_{n}]\not\models Q_{i}(y_{1},\ldots,y_{n})$ for every $i$. Hence,

[TABLE]

Consequently, $\mathcal{A}$ is a model of $\varphi$.

Consider the following simple two-player game with Players $\mathfrak{A}$ and $\mathfrak{B}$ where both players have complete and instantaneous knowledge about all moves that are made by either player. In the first round $\mathfrak{A}$ moves first by picking some domain element $\mathfrak{a}^{(n)}_{S_{\mathfrak{A},n}}$ for some set $S_{\mathfrak{A},n}\in\mathcal{S}_{n}$. $\mathfrak{B}$ knows about $\mathfrak{A}$’s choice and answers by picking a domain element $\mathfrak{b}^{(n)}_{S_{\mathfrak{B},n}}$ for some set $S_{\mathfrak{B},n}\in\mathcal{S}_{n}$. The game continues for $n-1$ more rounds, where in every round Player $\mathfrak{A}$ picks a domain element $\mathfrak{a}^{(j)}_{S_{\mathfrak{A},j}}$ with $S_{\mathfrak{A},j}\in S_{\mathfrak{A},j+1}$ and $\mathfrak{B}$ answers by picking some $\mathfrak{b}^{(j)}_{S_{\mathfrak{B},j}}\in S_{\mathfrak{B},j+1}$. Hence, in the last round the chosen domain elements $\mathfrak{a}^{(1)}_{S_{\mathfrak{A},1}}$ and $\mathfrak{b}^{(1)}_{S_{\mathfrak{B},1}}$ are such that $S_{\mathfrak{A},1}$ and $S_{\mathfrak{B},1}$ are both nonempty subsets of $[4n]$. Player $\mathfrak{A}$ wins if and only if

[TABLE]

for some $i\in[4n]$, and Player $\mathfrak{B}$ wins if and only if

[TABLE]

for every $i\in[4n]$. Since $\mathcal{A}$ is a model of $\varphi$, there must exist a winning strategy for $\mathfrak{B}$.

Claim: There is exactly one winning strategy for $\mathfrak{B}$, namely, for every $j=n,\ldots,1$ Player $\mathfrak{B}$ picks the element $\mathfrak{b}^{(j)}_{S_{\mathfrak{A},j}}$ in round $n-j+1$, i.e. for every $j$ we have $S_{\mathfrak{B},j}=S_{\mathfrak{A},j}$.

Proof: It is easy to see that the described strategy is a winning strategy for $\mathfrak{B}$.

Assume $\mathfrak{B}$ deviates from this strategy. This means there exists some $j_{*}$, $1\leq j_{*}\leq n$, such that $\mathfrak{B}$ did not adhere to the described strategy in the $(n-j_{*}+1)$st round, i.e. $S_{\mathfrak{B},j_{*}}\neq S_{\mathfrak{A},j_{*}}$.

We show by induction on $j_{*}$ that $\mathfrak{A}$ has a winning strategy from this deviation point on.

For the base case $j=1$ we consider two distinct nonempty sets $S_{\mathfrak{A},1},S_{\mathfrak{B},1}\subseteq[4n]$. There must be some index $i_{*}$ that belongs to one of the two sets but not to the other, i.e. $i_{*}\in(S_{\mathfrak{A},1}\cup S_{\mathfrak{B},1})\setminus(S_{\mathfrak{A},1}\cap S_{\mathfrak{B},1})$.

Suppose that $i_{*}\in S_{\mathfrak{A},1}\setminus S_{\mathfrak{B},1}$. Hence, we can construct the chain $i_{*}\in S_{\mathfrak{A},1}\in\ldots\in S_{\mathfrak{A},n}$, by definition of the allowed moves. This entails $\mathcal{A},[x_{1}{\mathop{\mapsto}}\mathfrak{a}^{(1)}_{S_{\mathfrak{A},1}},\ldots,x_{n}{\mathop{\mapsto}}\mathfrak{a}^{(n)}_{S_{\mathfrak{A},n}}]\models P_{i_{*}}(x_{1},\ldots,x_{n})$. On the other hand, we know $\mathcal{A},[y_{1}{\mathop{\mapsto}}\mathfrak{b}^{(1)}_{S_{\mathfrak{B},1}},\ldots,y_{n}{\mathop{\mapsto}}\mathfrak{b}^{(n)}_{S_{\mathfrak{B},n}}]\not\models Q_{i_{*}}(y_{1},\ldots,y_{n})$, because of $i_{*}\not\in S_{\mathfrak{B},1}$. Hence, $\mathfrak{A}$ wins and the chosen strategy cannot be a winning strategy for $\mathfrak{B}$.

The case where $i_{*}\in S_{\mathfrak{B},1}\setminus S_{\mathfrak{A},1}$ is symmetric and $\mathfrak{A}$ also wins.

For the inductive case we fix some $j_{*}>1$. Since $S_{\mathfrak{A},j_{*}}$ and $S_{\mathfrak{B},j_{*}}$ are distinct but have the same number of elements, there is some set $S^{\prime}\in S_{\mathfrak{A},j_{*}}\setminus S_{\mathfrak{B},j_{*}}$. If $\mathfrak{A}$ picks $\mathfrak{a}^{(j_{*}-1)}_{S_{\mathfrak{A},j_{*}-1}}:=\mathfrak{a}^{(j_{*}-1)}_{S^{\prime}}$ in the following round, we have $S_{\mathfrak{B},j_{*}-1}\neq S_{\mathfrak{A},j_{*}-1}$ for any choice $\mathfrak{b}^{(j_{*}-1)}_{S_{\mathfrak{B},j_{*}-1}}$ that $\mathfrak{B}$ could possibly make. By induction, $\mathfrak{A}$ has a winning strategy starting from the next round of the game. Hence, there is a winning strategy starting from the current round. $\Diamond$

The just proved claim would still hold true if we allowed $\mathfrak{B}$ to freely pick any element of the domain $\mathfrak{U}_{\mathcal{A}}$ at every round. The reason is that for any choice of elements $\mathfrak{a}^{(n)}_{S_{\mathfrak{A},n}},\ldots,\mathfrak{a}^{(1)}_{S_{\mathfrak{A},1}}$ made by $\mathfrak{A}$ with $S_{\mathfrak{A},1}\in\ldots\in S_{\mathfrak{A},n}\in\mathcal{S}_{n}$ we know that $S_{\mathfrak{A},1}$ is nonempty. Hence, we can always find some $i_{*}\in S_{\mathfrak{A},1}$ such that $\langle\mathfrak{a}^{(n)}_{S_{\mathfrak{A},n}},\ldots,\mathfrak{a}^{(1)}_{S_{\mathfrak{A},1}}\rangle\in P_{i_{*}}^{\mathcal{A}}$. On the other hand, for any sequence $\mathfrak{c}_{n},\ldots,\mathfrak{c}_{1}$ picked by $\mathfrak{B}$ that does not comply with the rules of the described game, we have $\langle\mathfrak{c}_{n},\ldots,\mathfrak{c}_{1}\rangle\not\in Q_{i_{*}}^{\mathcal{A}}$.

This result proves the following observation for any of the $\mathfrak{b}^{(k)}_{S}$:

• ($*$)

removing $\mathfrak{b}^{(k)}_{S}$ from $\mathcal{A}$’s domain and restricting the sets $Q_{i}^{\mathcal{A}}$ to subsets of \bigl{(}\mathfrak{U}_{\mathcal{A}}\setminus\{\mathfrak{b}^{(k)}_{S}\}\bigr{)}^{n} yields a structure that does not satisfy $\varphi$.

The reason is simply that in this case player $\mathfrak{A}$ can always prevent $\mathfrak{B}$ from reaching a state of the game where $\mathfrak{B}$ can apply the described winning strategy.

We have already analyzed the size of the sets $\mathcal{S}_{k}$. Due to the observed lower bounds, we know that $\mathfrak{U}_{\mathcal{A}}$ contains at least $\sum_{k=1}^{n}{2^{\uparrow k}(n)}$ elements of the form $\mathfrak{b}^{(k)}_{S}$.

Next, we argue that any sentence $\varphi_{*}$ (in prenex normal form) that is semantically equivalent to $\varphi$ and starts with a quantifier prefix of the form $\exists^{*}\forall^{*}$ contains at least $\sum_{k=1}^{n}{2^{\uparrow k}(n)}$ leading existential quantifiers.

Let $\varphi_{*}:=\exists y_{1}\ldots y_{m}\forall x_{1}\ldots x_{\ell}.\chi_{*}$ (with $\chi_{*}$ being quantifier-free) be a sentence with minimal $m$ that is semantically equivalent to $\varphi$. Since $\mathcal{A}$ is also a model of $\varphi_{*}$, we know that there is a sequence of elements $\mathfrak{c}_{1},\ldots,\mathfrak{c}_{m}$ taken from the domain $\mathfrak{U}_{\mathcal{A}}$ such that $\mathcal{A},[y_{1}{\mathop{\mapsto}}\mathfrak{c}_{1},\ldots,y_{m}{\mathop{\mapsto}}\mathfrak{c}_{m}]\models\forall x_{1}\ldots x_{\ell}.\chi_{*}$. Consequently, we can extend $\mathcal{A}$ to a model $\mathcal{A}_{*}$ (over the same domain) of the Skolemized formula \varphi_{\text{Sk}}:=\forall x_{1}\ldots x_{\ell}.\chi_{*}\bigl{[}y_{1}/c_{1},\ldots,y_{m}/c_{m}\bigr{]} by adding $c_{j}^{\mathcal{A}_{*}}:=\mathfrak{c}_{j}$ for $j=1,\ldots,m$. On the other hand, every model of the Skolemized formula $\varphi_{\text{Sk}}$ immediately yields a model of $\varphi_{*}$.

The signature underlying $\varphi_{\text{Sk}}$ comprises exactly the constant symbols $c_{1},\ldots,c_{m}$ and does not contain any other function symbols. Suppose $m<\sum_{k=1}^{n}{2^{\uparrow k}(n)}$. Hence, there is some $\mathfrak{b}^{(k)}_{S}$ with $S\in\mathcal{S}_{k}$ such that for every $j$ we have $c_{j}^{\mathcal{A}_{*}}\neq\mathfrak{b}^{(k)}_{S}$. By the Substructure Lemma, the following substructure $\mathcal{B}$ of $\mathcal{A}_{*}$ constitutes a model of $\varphi_{Sk}$: $\mathfrak{U}_{\mathcal{B}}:=\mathfrak{U}_{\mathcal{A}_{*}}\setminus\{\mathfrak{b}^{(k)}_{S}\}$, $P_{i}^{\mathcal{B}}:=P_{i}^{\mathcal{A}_{*}}\cap\mathfrak{U}_{\mathcal{B}}^{n}=P_{i}^{\mathcal{A}_{*}}$ and $Q_{i}^{\mathcal{B}}:=Q_{i}^{\mathcal{A}_{*}}\cap\mathfrak{U}_{\mathcal{B}}^{n}$ for every $i$, and $c_{j}^{\mathcal{B}}:=c_{j}^{\mathcal{A}_{*}}$ for every $j$.

But then $\mathcal{B}$ must also be a model of both $\varphi_{*}$ and $\varphi$, since every model of $\varphi_{\text{Sk}}$ is a model of $\varphi_{*}$, and because we assumed $\varphi_{*}$ and $\varphi$ to be semantically equivalent. This contradicts Observation ($*$), and thus we must have $m\geq\sum_{k=1}^{n}{2^{\uparrow k}(n)}$.

Since every atom $Q_{i}(y_{1},\ldots,y_{n})$ contains $n$ variables from existential quantifier blocks that are interspersed with universal quantifier blocks, the degree $\partial_{\varphi}$ of $\varphi$ is $n$. Moreover, $\varphi$ can easily be transformed into a CNF that is Horn and Krom at the same time. Hence, the theorem holds. ∎

Appendix D Details regarding Section 5

The following theorems illustrate why the domino problems defined in Section 5 readily lend themselves to deriving lower bounds on worst-case computing time.

Theorem 28** ([3], Theorem 6.1.2).**

Let $M$ be a simple nondeterministic one-tape Turing machine with input alphabet $\Gamma$. Then there is a domino system $\mathfrak{D}=\langle\mathcal{D},\mathcal{H},\mathcal{V}\rangle$ and a linear-time reduction which takes any input $w\in\Gamma^{*}$ to a word $\overline{D}\in\mathcal{D}^{*}$ with $|w|=|\overline{D}|$ such that

• •

If $M$ accepts $w$ in time $t_{0}$ with space $s_{0}$, then $\mathfrak{D}$ tiles $\mathbb{Z}_{s}\times\mathbb{Z}_{t}$ with initial condition $\overline{D}$ for all $s\geq s_{0}+2$ and $t\geq t_{0}+2$;

• •

If $M$ does not accept $w$, then $\mathfrak{D}$ does not tile $\mathbb{Z}_{s}\times\mathbb{Z}_{t}$ with initial condition $\overline{D}$ for any $s,t\geq 2$.

By a simple Turing machine the authors of [3] mean a nondeterministic one-tape Turing machine $M$ over the input alphabet $\Gamma$ that meets the following conditions:

“The alphabet of $M$ contains $\Gamma$ and at least one other symbol $\Box$ (blank). $M$ works on a semi-infinite tape and never tries to move left from the left-most tape cell. At every stage of the computation there is some $s$ such the tape cells $0,\ldots,s$ contain only non-blank symbols, all other tape cells contain $\Box$; in particular, to the right of a blank only other blanks may appear. Furthermore, we assume that $M$ has a unique accepting configuration: the machine is in the unique accepting state $q_{a}$, the tape contains only blanks and the head is in position [math].

These conditions do not restrict computational power. Every language accepted in time $T(n)$ and space $S(n)$ by some one-tape nondeterministic Turing machine is accepted within the same time and space bounds by a simple Turing machine, as long as $S(n),T(n)\geq 2n$.” [3], page 243

Theorem 29** ([3], Theorem 6.1.6).**

We call a function $T:\mathbb{N}\to\mathbb{N}$ time constructible if there exists a deterministic Turing machine making precisely $T(n)$ steps on inputs of length $n$.

Let $T:\mathbb{N}\to\mathbb{N}$ be a time-constructible function with $T(c^{\prime}n)^{2}\in o(T(n))$ for some constant $c^{\prime}>0$. There exists a domino system $\mathfrak{D}$ and a constant $c>0$ such that $\text{DOMINO}(\mathfrak{D},T(n))\not\in\text{NTIME}(T(cn))$.

Recall our notation for the tetration operation ${2^{\uparrow k}(m)}$, which we defined inductively: ${2^{\uparrow 0}(m)}:=m$ and ${2^{\uparrow k+1}(m)}:=2^{\left({2^{\uparrow k}(m)}\right)}$. In addition, we shall use the short-hand ${2^{\uparrow k}}$ to abbreviate ${2^{\uparrow k}(2)}$.

Since we intend to plug in the function ${2^{\uparrow n}}$ for $T(n)$, we need to verify the condition \bigl{(}{2^{\uparrow c^{\prime}n}}\bigr{)}^{2}\in o({2^{\uparrow n}}) for some positive constant $c^{\prime}$. Setting $c^{\prime}:=\tfrac{1}{2}$ entails the following.

Lemma 30**.**

For every positive constant $c>0$ there exists some positive integer $n_{0}>0$ such that for every $n\geq n_{0}$ we have

[TABLE]

Proof.

We distinguish two cases:

Suppose $c\geq 1$. We observe

1. (1)

\Bigl{(}{2^{\uparrow\lceil n/2\rceil}}\Bigr{)}^{2}\;=\;2^{2\cdot 2^{{2^{\uparrow\lceil n/2\rceil-2}}}}\;=\;2^{2^{1+{2^{\uparrow\lceil n/2\rceil-2}}}}, and 2. (2)

$c\cdot{2^{\uparrow n}}\;\;\geq\;\;{2^{\uparrow n}}\;\;=\;\;2^{2^{{2^{\uparrow n-2}}}}$.

Hence, it suffices to show there is some $n_{0}\geq 2$ such that $1+{2^{\uparrow\lceil n/2\rceil-2}}\;\leq\;{2^{\uparrow n-2}}$ holds for every $n\geq n_{0}$. One possible choice is $n_{0}=4$

Suppose $0<c<1$. We set $d:=\tfrac{1}{c}$. Due to $d>1$, $\log_{2}d$ is defined. Moreover, we observe

[TABLE]

Hence, in order to prove that there is some $n_{0}$ such that d\cdot\Bigl{(}{2^{\uparrow\lceil n/2\rceil}}\Bigr{)}^{2}\leq{2^{\uparrow n}} holds for every $n\geq n_{0}$, it suffices to show that there is some $n_{0}$ such that

[TABLE]

where $d^{\prime}:=\log_{2}(\log_{2}d+2)$. The proof thus boils down to asking whether the difference ${2^{\uparrow n-2}}-{2^{\uparrow\lceil n/2\rceil-2}}$ exceeds any constant value $d^{\prime}$ for sufficiently large $n$. This is certainly the case. ∎

Lemma 31**.**

Let $k\geq 1$ be some positive integer. For every positive constant $c>0$ there exists some positive integer $n_{0}\geq 1$ such that for every $n\geq n_{0}$ we have

[TABLE]

Proof.

Let $k=1$. We observe

[TABLE]

If $c\geq 1$, then $2^{n/2}\leq c\cdot 2^{n}$ is obvious.

Assume $0<c<1$ and set $d:=\tfrac{1}{c}$. Hence, $d>1$. If remains to show $d\cdot 2^{n/2}\leq 2^{n}$ for every sufficiently large $n$. Due to $2^{n}=2^{n/2+n/2}=2^{n/2}\cdot 2^{n/2}$, we observe $d\cdot 2^{n/2}\leq 2^{n/2}\cdot 2^{n/2}$ if and only if $d\leq 2^{n/2}$. But the latter certainly holds for sufficiently large $n$.

Let $k=2$. If $c\geq 1$, then ${2^{\uparrow 2}(n)}\leq c\cdot{2^{\uparrow 2}(n)}$. It thus suffices to show $2^{2^{n/4}}\leq 2^{2^{n}}$ or, equivalently, $\tfrac{1}{4}n+1\leq n$ for sufficiently large $n$. But this is obviously true.

Assume $0<c<1$ and define $d:=\tfrac{1}{c}$. It follows that $d>1$. It remains to show $d\cdot 2^{2^{n/4+1}}\leq 2^{2^{n}}$ for sufficiently large $n$. Due to $2^{2^{n}}=2^{2^{n/2}\cdot 2^{n/2}}\geq 2^{2^{n/2}+2^{n/2}}=2^{2^{n/2}}\cdot 2^{2^{n/2}}$ with $d\leq 2^{2^{n/2}}$ and $2^{2^{n/4+1}}\leq 2^{2^{n/2}}$ for sufficiently large $n$, we also observe $d\cdot 2^{2^{n/4+1}}\leq 2^{2^{n/2}}\cdot 2^{2^{n/2}}\leq 2^{2^{n}}$ for sufficiently large $n$.

Analogous arguments holds for every $k\geq 2$. ∎

Appendix E Details regarding Section 5.1

We investigate the properties of models of the SF sentences given in Section 5.1. For the remainder of this subsection we therefore consider a model $\mathcal{A}$ of the sentence $\psi_{1}\wedge\ldots\wedge\psi_{16}\wedge\chi_{1}\wedge\chi_{2}\wedge\chi_{3}$.

Definition 32**.**

We define the following sets and relations:

• •

\mathcal{I}_{\ell}:=\bigl{\{}\mathfrak{a}\in\mathfrak{U}_{\mathcal{A}}\mid\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a}]\models L({\underline{\ell}},j)\bigr{\}} for every $\ell=0,\ldots,\kappa$.

• •

${\prec_{\ell}}\subseteq\mathcal{I}_{\ell}\times\mathcal{I}_{\ell}$ for every $\ell=0,\ldots,\kappa$ such that $\mathfrak{a}\prec_{\ell}\mathfrak{a}^{\prime}$ holds if and only if $\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},j^{\prime}{\mathop{\mapsto}}\mathfrak{a}^{\prime}]\models\text{Succ}({\underline{\ell}},j,j^{\prime})$.

• •

\mathcal{F}_{\ell}:=\{f:\mathcal{I}_{\ell}\to\{0,1\}\mid\text{f$is total and for every$\mathfrak{a}$for which$\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a}]\models\text{MaxIdx}({\underline{\ell}},j) we}                                      \text{have that f(\mathfrak{a})=1$entails$f(\mathfrak{b})=0$for every$\mathfrak{b}\neq\mathfrak{a}}\}

for every $\ell=0,\ldots,\kappa-1$.

• •

For every $\ell=0,\ldots,\kappa-1$ and two total functions $f,g:\mathcal{I}_{\ell}\to\{0,1\}$ we write $f\sqsubset_{\ell}g$ if and only if

• –

there is some integer $p$ and a unique chain $\mathfrak{a}_{1}\prec_{\ell}\ldots\prec_{\ell}\mathfrak{a}_{p}$ comprising all elements in $\mathcal{I}_{\ell}$, and

• –

incrementing the bit string $f(\mathfrak{a}_{1})f(\mathfrak{a}_{2})\ldots f(\mathfrak{a}_{p})$ (interpreted as number encoded in binary where the leftmost bit is the least significant one) by one yields $g(\mathfrak{a}_{1})g(\mathfrak{a}_{2})\ldots g(\mathfrak{a}_{p})$.

• •

\mathcal{S}_{\ell,f}:=\bigl{\{}\mathfrak{a}\in\mathcal{I}_{\ell}\mid\text{\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},i{\mathop{\mapsto}}\mathfrak{b}]\models} \text{J({\underline{\ell}},j,i,f(\mathfrak{b}))$for every$\mathfrak{b}\in\mathcal{I}_{\ell-1}}\bigr{\}}

for every $\ell=1,\ldots,\kappa$ and every $f\in\mathcal{F}_{\ell-1}$.

• •

For every $\ell=1,\ldots,\kappa$ and two elements $\mathfrak{a},\mathfrak{a}^{\prime}\in\mathcal{I}_{\ell}$ we write $\mathfrak{a}\sim_{\ell}\mathfrak{a}^{\prime}$ if and only if for every $\mathfrak{b}\in\mathcal{I}_{\ell-1}$ we observe

• –

$\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},i{\mathop{\mapsto}}\mathfrak{b}]\models J({\underline{\ell}},j,i,0)$ if and only if $\mathcal{A},[j^{\prime}{\mathop{\mapsto}}\mathfrak{a}^{\prime},i{\mathop{\mapsto}}\mathfrak{b}]\models J({\underline{\ell}},j^{\prime},i,0)$ and

• –

$\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},i{\mathop{\mapsto}}\mathfrak{b}]\models J({\underline{\ell}},j,i,1)$ if and only if $\mathcal{A},[j^{\prime}{\mathop{\mapsto}}\mathfrak{a}^{\prime},i{\mathop{\mapsto}}\mathfrak{b}]\models J({\underline{\ell}},j^{\prime},i,1)$.

Proposition 33**.**

For every $\ell$, $1\leq\ell\leq\kappa$, $\sim_{\ell}$ is an equivalence relation.

Proposition 34**.**

For all distinct $\ell,\ell^{\prime}$, $0\leq\ell,\ell^{\prime}\leq\kappa$, $\mathcal{I}_{\ell}$ and $\mathcal{I}_{\ell^{\prime}}$ are disjoint.

Lemma 35**.**

Let $\mathfrak{a},\mathfrak{a}^{\prime}\in\mathcal{I}_{\ell}$ for some $\ell$, $1\leq\ell\leq\kappa$. Let $f,g:\mathcal{I}_{\ell-1}\to\{0,1\}$ be two total functions such that for every $\mathfrak{b}\in\mathcal{I}_{\ell-1}$ we have $\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},i{\mathop{\mapsto}}\mathfrak{b}]\models J({\underline{\ell}},j,i,f(\mathfrak{b}))$ and $\mathcal{A},[j^{\prime}{\mathop{\mapsto}}\mathfrak{a}^{\prime},i{\mathop{\mapsto}}\mathfrak{b}]\models J({\underline{\ell}},j^{\prime},i,g(\mathfrak{b}))$. Moreover, assume there is a unique chain $\mathfrak{c}_{1}\prec_{\ell-1}\ldots\prec_{\ell-1}\mathfrak{c}_{p}$ comprising all elements in $\mathcal{I}_{\ell-1}$.

Then $\mathfrak{a}\prec_{\ell}\mathfrak{a}^{\prime}$ implies $f\sqsubset_{\ell-1}g$.

Proof.

Since $\mathfrak{c}_{1}$ is the only element in $\mathcal{I}_{\ell-1}$ for which there is no element $\mathfrak{c}^{\prime}\in\mathcal{I}_{\ell-1}$ with $\mathfrak{c}^{\prime}\prec_{\ell-1}\mathfrak{c}_{1}$, $\mathcal{A}\models\psi_{2}\wedge\psi_{3}$ implies $\mathcal{A},[i\mapsto\mathfrak{c}_{1}]\models\text{MinIdx}({\underline{\ell-1}},i)$.

Let $f^{*}:\mathcal{I}_{\ell-1}\to\{0,1\}$ be defined such that

• •

$f^{*}(\mathfrak{b})=0$ if and only if $\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},i{\mathop{\mapsto}}\mathfrak{b}]\models J^{*}({\underline{\ell}},j,i,0)$ and

• •

$f^{*}(\mathfrak{b})=1$ if and only if $\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},i{\mathop{\mapsto}}\mathfrak{b}]\models J^{*}({\underline{\ell}},j,i,1)$.

This function is well-defined because of $\mathcal{A}\models\psi_{13}$. Due to $\mathcal{A}\models\chi_{2}\wedge\psi_{14}\wedge\psi_{15}$ it is also total.

$\mathcal{A}\models\psi_{14}$ enforces $\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},i{\mathop{\mapsto}}\mathfrak{c}_{1}]\models J^{*}({\underline{\ell}},j,i,1)$, i.e. $f^{*}(\mathfrak{c}_{1})=1$. Moreover, for any $k$ with $1<k\leq p$, we have $f^{*}(\mathfrak{c}_{k})=1$ if and only if $f(\mathfrak{c}_{1})=\ldots=f(\mathfrak{c}_{k-1})=1$, because of $\mathcal{A}\models\psi_{15}$.

$\mathcal{A}\models\psi_{9}$ together with our assumption $\mathfrak{a}\prec_{\ell}\mathfrak{a}^{\prime}$ translates to the following property, which we phrase in terms of operations on bits:

• ($**$)

for every $k$, $1\leq k\leq p$, we observe $g(\mathfrak{c}_{k})=f(\mathfrak{c}_{k})\oplus f^{*}(\mathfrak{c}_{k})$

where $\oplus$ denotes exclusive or. But this corresponds to an increase of the bit string $f(\mathfrak{c}_{1})\ldots f(\mathfrak{c}_{p})$ by one (where $f(\mathfrak{c}_{1})$ is the least significant bit).

Hence, $f\sqsubset_{\ell-1}g$. ∎

Lemma 36**.**

Let $\mathfrak{a},\mathfrak{a}^{\prime}\in\mathcal{I}_{\ell}$ for some $\ell$, $1\leq\ell\leq\kappa$.

If $\mathfrak{a}$ and $\mathfrak{a}^{\prime}$ belong to the same $\mathcal{S}_{\ell,f}$ for some function $f\in\mathcal{F}_{\ell-1}$, then $\mathfrak{a}\sim_{\ell}\mathfrak{a}^{\prime}$.

Proof.

By totality of $f$, it follows that for every $\mathfrak{b}\in\mathcal{I}_{\ell-1}$ we have $\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},i{\mathop{\mapsto}}\mathfrak{b}]\models J({\underline{\ell}},j,i,f(\mathfrak{b}))$ and $\mathcal{A},[j^{\prime}{\mathop{\mapsto}}\mathfrak{a}^{\prime},i{\mathop{\mapsto}}\mathfrak{b}]\models J({\underline{\ell}},j^{\prime},i,f(\mathfrak{b}))$. Moreover, $\mathcal{A}\models\psi_{13}$ entails $\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},i{\mathop{\mapsto}}\mathfrak{b}]\not\models J({\underline{\ell}},j,i,\overline{f(\mathfrak{b})})$ and $\mathcal{A},[j^{\prime}{\mathop{\mapsto}}\mathfrak{a}^{\prime},i{\mathop{\mapsto}}\mathfrak{b}]\not\models J({\underline{\ell}},j^{\prime},i,\overline{f(\mathfrak{b})})$ where $\overline{f(\mathfrak{b})}:=1-f(\mathfrak{b})$ is the complement of $f(\mathfrak{b})$. This results in $\mathfrak{a}\sim_{\ell}\mathfrak{a}^{\prime}$. ∎

Lemma 37**.**

Let $\mathfrak{a},\mathfrak{a}^{\prime}\in\mathcal{I}_{\ell}$ for some $\ell$, $1\leq\ell\leq\kappa$. Moreover, let $f$ be some function in $\mathcal{F}_{\ell-1}$.

If $\mathfrak{a}$ belongs to $\mathcal{S}_{\ell,f}$ and we have $\mathfrak{a}\sim_{\ell}\mathfrak{a}^{\prime}$, then $\mathfrak{a}^{\prime}\in\mathcal{S}_{\ell,f}$.

Proof.

By totality of $f$, it follows that for every $\mathfrak{b}\in\mathcal{I}_{\ell-1}$ we have $\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},i{\mathop{\mapsto}}\mathfrak{b}]\models J({\underline{\ell}},j,i,f(\mathfrak{b}))$. Moreover, $\mathcal{A}\models\psi_{13}$ entails $\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},i{\mathop{\mapsto}}\mathfrak{b}]\not\models J({\underline{\ell}},j,i,\overline{f(\mathfrak{b})})$ where $\overline{f(\mathfrak{b})}:=1-f(\mathfrak{b})$ is the complement of $f(\mathfrak{b})$.

Since we assume $\mathfrak{a}\sim_{\ell}\mathfrak{a}^{\prime}$, we know that these properties transfer to $\mathfrak{a}^{\prime}$. Hence, for every $\mathfrak{b}\in\mathcal{I}_{\ell-1}$ we observe $\mathcal{A},[j^{\prime}{\mathop{\mapsto}}\mathfrak{a}^{\prime},i{\mathop{\mapsto}}\mathfrak{b}]\models J({\underline{\ell}},j^{\prime},i,f(\mathfrak{b}))$ and $\mathcal{A},[j^{\prime}{\mathop{\mapsto}}\mathfrak{a}^{\prime},i{\mathop{\mapsto}}\mathfrak{b}]\not\models J({\underline{\ell}},j^{\prime},i,\overline{f(\mathfrak{b})})$. Consequently, $\mathfrak{a}^{\prime}\in\mathcal{S}_{\ell,f}$. ∎

Lemma 38**.**

Consider some $\ell$, $0\leq\ell\leq\kappa-1$. If there is a unique chain $\mathfrak{a}_{1}\prec_{\ell}\ldots\prec_{\ell}\mathfrak{a}_{p}$ comprising all elements in $\mathcal{I}_{\ell}$, then we can uniquely arrange all functions in $\mathcal{F}_{\ell}$ into a chain $f_{1}\sqsubset_{\ell}\ldots\sqsubset_{\ell}f_{p^{\prime}}$ where $p^{\prime}=|\mathcal{F}_{\ell}|=2^{p-1}+1$.

Proof.

Let $\{0,1\}^{p}$ be the set of all bit strings of length $p$. If we interpret each of them as a number encoded in binary (where we assume the leftmost bit to be the least significant one), we can uniquely arrange the $2^{p-1}+1$ smallest bit strings in $\{0,1\}^{p}$ into a chain

[TABLE]

where the indices reflect the represented numerical value and $<$ is intended to be the usual ordering based on this value. Since we assume the rightmost bit to be the most significant one, it is [math] in $\overline{b}_{0},\ldots,\overline{b}_{2^{p-1}-1}$. Accordingly, $\overline{b}_{2^{p-1}}$ is the bit string with all zeros except for the most significant bit, i.e. $\overline{b}_{2^{p-1}}=0\ldots 01$.

Obviously, the following mapping $\mu$ induces a one-to-one correspondence between bit strings and all the mappings in $\mathcal{F}_{\ell}$: $\mu(f):=f(\mathfrak{a}_{1})f(\mathfrak{a}_{2})\ldots f(\mathfrak{a}_{p})$. By definition of $\sqsubset_{\ell}$, we have $f\sqsubset_{\ell}g$ if and only if $\mu(f)+1=\mu(g)$.

Consequently, we obtain the chain $\mu^{-1}(\overline{b}_{0})\sqsubset_{\ell}\mu^{-1}(\overline{b}_{1})\sqsubset_{\ell}\ldots\sqsubset_{\ell}\mu^{-1}(\overline{b}_{2^{p-1}-1})\sqsubset_{\ell}\mu^{-1}(\overline{b}_{2^{p-1}})$. ∎

Lemma 39**.**

We observe that $\mathcal{I}_{0}=\{c_{1}^{\mathcal{A}},\ldots,c_{\mu}^{\mathcal{A}}\}$ with $|\mathcal{I}_{0}|=\mu$. Moreover, there is a unique chain $c_{1}^{\mathcal{A}}\prec_{0}\ldots\prec_{0}c_{\mu}^{\mathcal{A}}$.

Proof.

$\mathcal{A}\models\chi_{1}$ entails that $\mathcal{I}_{0}\subseteq\{c_{1}^{\mathcal{A}},\ldots,c_{\mu}^{\mathcal{A}}\}$. Due to $\mathcal{A}\models\psi_{8}$ we have $c_{1}^{\mathcal{A}}\prec_{0}\ldots\prec_{0}c_{\mu}^{\mathcal{A}}$. By $\mathcal{A}\models\psi_{6}$, $\mathfrak{a}\prec_{0}\mathfrak{b}$ entails $\mathfrak{a},\mathfrak{b}\in\mathcal{I}_{0}$. Hence, $\{c_{1}^{\mathcal{A}},\ldots,c_{\mu}^{\mathcal{A}}\}\subseteq\mathcal{I}_{0}$

We next show that all $c_{1}^{\mathcal{A}},\ldots,c_{\mu}^{\mathcal{A}}$ are pairwise distinct.

Claim: For every index $j\geq 2$ the first $j$ elements $c_{1}^{\mathcal{A}},\ldots,c_{j}^{\mathcal{A}}$ are distinct.

Proof: We proceed by induction on $j$.

For $j=2$, $c_{1}^{\mathcal{A}}\neq c_{2}^{\mathcal{A}}$ must hold, for otherwise $c_{1}^{\mathcal{A}}\prec_{0}c_{2}^{\mathcal{A}}$ contradicts $\mathcal{A}\models\psi_{7}$ which entails $\mathcal{A}\models\forall j.\;\neg\text{Succ}({\underline{0}},j,j)$.

Let $j\geq 3$ and assume, by induction, that the elements $c_{1}^{\mathcal{A}},\ldots,c_{j-1}^{\mathcal{A}}$ are all pairwise distinct. Suppose there is some index $i_{*}$, $1\leq i_{*}<j$, such that $c_{i_{*}}^{\mathcal{A}}=c_{j}^{\mathcal{A}}$. We distinguish two cases: In case $i_{*}=1$, we have $c_{j-1}^{\mathcal{A}}\prec_{0}c_{1}^{\mathcal{A}}$. But this contradicts $\mathcal{A}\models\psi_{2}$.

In case of $i_{*}>1$, $\mathcal{A}\models\psi_{7}$ entails $c_{i_{*}-1}^{\mathcal{A}}=c_{j-1}^{\mathcal{A}}$, since we have $c_{i_{*}-1}^{\mathcal{A}}\prec_{0}c_{i_{*}}^{\mathcal{A}}$ and $c_{j-1}^{\mathcal{A}}\prec_{0}c_{j}^{\mathcal{A}}$, and since we assumed $c_{i_{*}}^{\mathcal{A}}=c_{j}^{\mathcal{A}}$. But this contradicts our inductive hypothesis, because $i_{*}-1$ and $j-1$ are distinct indices and thus the inductive hypothesis implies that $c_{i_{*}-1}^{\mathcal{A}}$ and $c_{j-1}^{\mathcal{A}}$ are distinct. $\Diamond$

The above claim entails $|\mathcal{I}_{0}|=\mu$.

$\mathcal{A}\models\psi_{8}$ entails $c_{1}^{\mathcal{A}}\prec_{0}\ldots\prec_{0}c_{\mu}^{\mathcal{A}}$. By the above arguments, we know that this chain comprises all elements in $\mathcal{I}_{0}$. Moreover, due to $\mathcal{A}\models\psi_{7}$, this chain is the only chain satisfying the desired properties. ∎

Lemma 40**.**

For every $\ell=1,\ldots,\kappa$ the following properties are satisfied:

1. (i)

For all $\mathfrak{a},\widetilde{\mathfrak{a}}\in\mathcal{I}_{\ell}$ for which $\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},\widetilde{j}{\mathop{\mapsto}}\widetilde{\mathfrak{a}}]\models\text{eq}^{\ell}_{j,\widetilde{j}}$ it follows $\mathfrak{a}\sim_{\ell}\widetilde{\mathfrak{a}}$. 2. (ii)

All $\mathfrak{a},\widetilde{\mathfrak{a}}\in\mathcal{I}_{\ell}$ with $\mathfrak{a}\sim_{\ell}\widetilde{\mathfrak{a}}$ satisfy $\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},\widetilde{j}{\mathop{\mapsto}}\widetilde{\mathfrak{a}}]\models\text{eq}^{\ell}_{j,\widetilde{j}}$. 3. (iii)

For every $f\in\mathcal{F}_{\ell-1}$ the set $\mathcal{S}_{\ell,f}$ is nonempty. 4. (iv)

$\mathcal{I}_{\ell}=\bigcup_{f\in\mathcal{F}_{\ell-1}}\mathcal{S}_{\ell,f}$. 5. (v)

For every $f\in\mathcal{F}_{\ell-1}$ the set $\mathcal{S}_{\ell,f}$ contains exactly one element. 6. (vi)

There is a unique chain $\mathfrak{a}_{1}\prec_{\ell}\ldots\prec_{\ell}\mathfrak{a}_{p}$ comprising all elements in $\mathcal{I}_{\ell}$, and $\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a}_{1}]\models\text{MinIdx}({\underline{\ell}},j)$ and $\mathcal{A},[j^{\prime}{\mathop{\mapsto}}\mathfrak{a}_{p}]\models\text{MaxIdx}({\underline{\ell}},j^{\prime})$ hold.

Proof.

We proceed by induction on $\ell$.

Base case: $\ell=1$.

Ad (i). Due to the assumption $\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},\widetilde{j}{\mathop{\mapsto}}\widetilde{\mathfrak{a}}]\models\text{eq}^{1}_{j,\widetilde{j}}$, the construction of $\text{eq}^{1}_{j,\widetilde{j}}$ entails

[TABLE]

By Lemma 39, we know that $\mathfrak{b}\in\mathcal{I}_{0}$ entails $\mathfrak{b}=c_{i}^{\mathcal{A}}$ for some $i$, $1\leq i\leq\mu$. Consequently, for every $\mathfrak{b}\in\mathcal{I}_{0}$, $\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},i{\mathop{\mapsto}}\mathfrak{b}]\models J({\underline{1}},j,i,0)$ holds if and only if $\mathcal{A},[\widetilde{j}{\mathop{\mapsto}}\widetilde{\mathfrak{a}},i{\mathop{\mapsto}}\mathfrak{b}]\models J({\underline{1}},\widetilde{j},i,0)$ does. This entails $\mathfrak{a}\sim_{\ell}\widetilde{\mathfrak{a}}$, because of $\mathcal{A}\models\psi_{13}\wedge\chi_{2}$.

Ad (ii). By definition of $\sim_{1}$, $\mathfrak{a}\sim_{1}\widetilde{\mathfrak{a}}$ entails that for every $\mathfrak{b}\in\mathcal{I}_{0}$ we have

• •

$\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},i{\mathop{\mapsto}}\mathfrak{b}]\models J({\underline{1}},j,i,0)$ if and only if $\mathcal{A},[\widetilde{j}{\mathop{\mapsto}}\widetilde{\mathfrak{a}},i{\mathop{\mapsto}}\mathfrak{b}]\models J({\underline{1}},\widetilde{j},i,0)$ and

• •

$\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},i{\mathop{\mapsto}}\mathfrak{b}]\models J({\underline{1}},j,i,1)$ if and only if $\mathcal{A},[\widetilde{j}{\mathop{\mapsto}}\widetilde{\mathfrak{a}},i{\mathop{\mapsto}}\mathfrak{b}]\models J({\underline{1}},\widetilde{j},i,1)$.

Moreover, Lemma 39 states that $\mathcal{I}_{0}=\{c_{1}^{\mathcal{A}},\ldots,c_{\mu}^{\mathcal{A}}\}$. Since $\mathfrak{a},\widetilde{\mathfrak{a}}$ belong to $\mathcal{I}_{1}$, we conclude $\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},\widetilde{j}{\mathop{\mapsto}}\widetilde{\mathfrak{a}}]\models\text{eq}^{1}_{j,\widetilde{j}}$.

Ad (iii). $\mathcal{A}\models\psi_{8}$ entails $c_{1}^{\mathcal{A}}\prec_{0}\ldots\prec_{0}c_{\mu}^{\mathcal{A}}$. By Lemma 39, we know that this chain comprises all elements in $\mathcal{I}_{0}$. Moreover, due to $\mathcal{A}\models\psi_{7}$, this chain is the only chain satisfying this property. Hence, by Lemma 38, we can arrange all functions in $\mathcal{F}_{0}$ into a sequence $f_{1}\sqsubset_{0}\ldots\sqsubset_{0}f_{p}$ for $p=2^{\mu-1}+1$. Clearly, $f_{1}$ maps every element $\mathfrak{b}\in\mathcal{I}_{0}$ to $f_{1}(\mathfrak{b})=0$, and $f_{p}$ maps every element $\mathfrak{b}\in\mathcal{I}_{0}\setminus\{c_{\mu}^{\mathcal{A}}\}$ to $f_{p}(\mathfrak{b})=0$ and $c_{\mu}^{\mathcal{A}}$ to $f_{p}(c_{\mu}^{\mathcal{A}})=1$. By $\mathcal{A}\models\psi_{3}\wedge\psi_{10}$, we know that $\mathcal{A},[j{\mathop{\mapsto}}d_{1}^{\mathcal{A}},i{\mathop{\mapsto}}\mathfrak{b}]\models J({\underline{1}},j,i,0)$ for every $\mathfrak{b}\in\mathcal{I}_{0}$. Hence, $d_{1}^{\mathcal{A}}\in S_{1,f_{1}}$.

We next show that for every $k$, $1\leq k<p$, if $S_{1,f_{k}}$ is nonempty, then $S_{1,f_{k+1}}$ is nonempty. Let $\mathfrak{a}$ be an element of $S_{1,f_{k}}$. Because of $k<p$, we know that $\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},i{\mathop{\mapsto}}c_{\mu}^{\mathcal{A}}]\models J({\underline{1}},j,i,0)$. By virtue of (i) and due to $\mathcal{A}\models\psi_{16}$ we conclude that there are elements $\widetilde{\mathfrak{a}},\widetilde{\mathfrak{a}}^{\prime}\in\mathcal{I}_{1}$ such that $\mathfrak{a}\sim_{1}\widetilde{\mathfrak{a}}$ and $\widetilde{\mathfrak{a}}\prec_{1}\widetilde{\mathfrak{a}}^{\prime}$. By Lemma 35, this results in $\widetilde{\mathfrak{a}}^{\prime}\in\mathcal{S}_{\ell,f_{k+1}}$.

Ad (iv). As a consequence of $\mathcal{A}\models\psi_{13}$ there is a unique partial function $g_{\mathfrak{a}}:\mathcal{I}_{0}\to\{0,1\}$ for every $\mathfrak{a}\in\mathcal{I}_{1}$ such that for every $\mathfrak{b}\in\mathcal{I}_{0}$ we have $\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},i{\mathop{\mapsto}}\mathfrak{b}]\models J({\underline{1}},j,i,g_{\mathfrak{a}}(\mathfrak{b}))$ if and only if $g_{\mathfrak{a}}$ is defined for $\mathfrak{b}$. Because of $\mathcal{A}\models\chi_{2}$, we know that $g_{\mathfrak{a}}$ must be total.

For every $\mathfrak{a}\in\mathcal{I}_{1}$ where $g_{\mathfrak{a}}(c_{\mu}^{\mathcal{A}})=0$ we have $g_{\mathfrak{a}}\in\mathcal{F}_{0}$ and thus also $\mathfrak{a}\in\mathcal{S}_{1,g_{\mathfrak{a}}}$.

Because of $\mathcal{A}\models\psi_{5}\wedge\psi_{11}\wedge\psi_{12}$ we know that $\mathcal{A}\models\text{MaxIdx}({\underline{1}},e_{1})$ and that $e_{1}^{\mathcal{A}}$ is the only element in $\mathcal{I}_{1}$ for which $\mathcal{A},[j{\mathop{\mapsto}}e_{1}^{\mathcal{A}},i{\mathop{\mapsto}}c_{\mu}^{\mathcal{A}}]\models J({\underline{1}},j,i,1)$.

It remains to show that for every $\mathfrak{b}\in\mathcal{I}_{0}$ with $\mathfrak{b}\neq c_{\mu}^{\mathcal{A}}$ we have $\mathcal{A},[j{\mathop{\mapsto}}e_{1}^{\mathcal{A}},i{\mathop{\mapsto}}\mathfrak{b}]\models J({\underline{1}},j,i,0)$. But this is a consequence of (iii) and the fact that the total function $f_{*}$ mapping all elements $\mathfrak{b}$ in $\mathcal{I}_{0}$ but $c_{\mu}^{\mathcal{A}}$ to $f_{*}(\mathfrak{b})=0$ belongs to $\mathcal{F}_{0}$, and thus $\mathcal{S}_{1,f_{*}}$ is nonempty. In particular, $\mathcal{S}_{1,f_{*}}=\{e_{1}^{\mathcal{A}}\}$.

Consequently, $\mathcal{I}_{1}$ cannot contain any elements that do not lie in $\bigcup_{f\in\mathcal{F}_{0}}\mathcal{S}_{1,f}$.

Ad (v). Consider any set $\mathcal{S}_{1,f}$. By virtue of (iii), $\mathcal{S}_{1,f}$ contains at least one element. Suppose we are given two elements $\mathfrak{a},\mathfrak{a}^{\prime}$ in $\mathcal{S}_{1,f}$. By virtue of Lemma 36, this means $\mathfrak{a}\sim_{1}\mathfrak{a}^{\prime}$.

Because of $\mathcal{A}\models\chi_{3}$, there are two elements $\widetilde{\mathfrak{a}},\widetilde{\mathfrak{a}}^{\prime}\in\mathcal{I}_{1}$ for which (i) entails $\mathfrak{a}\sim_{1}\widetilde{\mathfrak{a}}$ and $\mathfrak{a}^{\prime}\sim_{1}\widetilde{\mathfrak{a}}^{\prime}$. By symmetry and transitivity of $\sim_{1}$, we have $\widetilde{\mathfrak{a}}\sim_{1}\widetilde{\mathfrak{a}}^{\prime}$. Hence, we observe

[TABLE]

Consequently, $\mathcal{A}\models\chi_{3}$ leads to $\mathfrak{a}=\mathfrak{a}^{\prime}$.

Ad (vi). As we have seen in the proof of Lemma 38, we can define a bijective mapping $\mu$ that maps the functions in $\mathcal{F}_{0}$ to bit strings of length $\mu$ that either have a [math] as most significant bit or correspond to $0\ldots 01$ (where the most significant bit is the rightmost one).

Let $p:=2^{\mu-1}+1$. By virtue of Lemma 38, we can uniquely construct a chain

[TABLE]

comprising all functions in $\mathcal{F}_{0}$.

Properties (iv) and (v) together yield that $\mathcal{I}_{1}=\{\mathfrak{a}_{1},\ldots,\mathfrak{a}_{p}\}$ where $\mathfrak{a}_{k}\in\mathcal{S}_{1,f_{k}}$ for every $k=1,\ldots,p$. Lemma 35 says that for any $\mathfrak{a}_{k},\mathfrak{a}_{k^{\prime}}$ with $\mathfrak{a}_{k}\prec_{1}\mathfrak{a}_{k^{\prime}}$ we also observe $f_{k}\sqsubset_{0}f_{k^{\prime}}$. By definition of $\sqsubset_{0}$ and the fact that all the $f_{k},f_{k^{\prime}}$ are distinct, it clearly holds that $f_{k}\sqsubset_{0}f_{k^{\prime}}$ implies $k^{\prime}=k+1$ and $1\leq k<k^{\prime}\leq p$. Hence, $\mathfrak{a}_{k}\prec_{1}\mathfrak{a}_{k^{\prime}}$ can only hold if $k^{\prime}=k+1$ and $1\leq k<k^{\prime}\leq p$.

Consider any element $\mathfrak{a}\in\mathcal{I}_{1}$ for which $\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},i{\mathop{\mapsto}}c_{\mu}^{\mathcal{A}}]\models J({\underline{1}},j,i,0)$. By $\mathcal{A}\models\psi_{16}$, we know that there are elements $\widetilde{\mathfrak{a}},\widetilde{\mathfrak{a}}^{\prime}\in\mathcal{I}_{1}$ such that $\widetilde{\mathfrak{a}}\prec_{1}\widetilde{\mathfrak{a}}^{\prime}$ and $\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},\widetilde{j}{\mathop{\mapsto}}\widetilde{\mathfrak{a}}]\models\text{eq}^{1}_{j,\widetilde{j}}$. By (i), the latter translates to $\mathfrak{a}\sim_{1}\widetilde{\mathfrak{a}}$.

Let $g,\widetilde{g}$ be functions such that $\mathfrak{a}\in\mathcal{S}_{1,g}$ and $\widetilde{\mathfrak{a}}\in\mathcal{S}_{1,\widetilde{g}}$. Such functions exist by virtue of (iv). However, $\mathfrak{a}\sim_{1}\widetilde{\mathfrak{a}}$ entails $g=\widetilde{g}$, by Lemma 37. But then (v) leads to $\mathfrak{a}=\widetilde{\mathfrak{a}}$. Consequently, we have $\mathfrak{a}\prec_{1}\widetilde{\mathfrak{a}}^{\prime}$. By (v), this means that all but one element in $\mathcal{I}_{1}$ must have a successor in $\mathcal{I}_{1}$ and all but one elements in $\mathcal{I}_{1}$ are successor in $\mathcal{I}_{1}$. Hence, we obtain the chain $\mathfrak{a}_{1}\prec_{1}\mathfrak{a}_{2}\prec_{1}\ldots\prec_{1}\mathfrak{a}_{p-1}\prec_{1}\mathfrak{a}_{p}$ where $\mathfrak{a}_{1}=d_{1}^{\mathcal{A}}$ and $\mathfrak{a}_{p}=e_{1}^{\mathcal{A}}$.

Inductive case $\ell>1$.

Ad (i). Due to the assumption $\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},\widetilde{j}{\mathop{\mapsto}}\widetilde{\mathfrak{a}}]\models\text{eq}^{\ell}_{j,\widetilde{j}}$ with $\ell>1$, the construction of $\text{eq}^{\ell}_{j,\widetilde{j}}$ entails

[TABLE]

By inductive application of (i), $\mathcal{A},[i{\mathop{\mapsto}}\mathfrak{b},\widetilde{i}{\mathop{\mapsto}}\widetilde{\mathfrak{b}}]\models\text{eq}^{\ell-1}_{i,\widetilde{i}}$ entails $\mathfrak{b}\sim_{\ell-1}\widetilde{\mathfrak{b}}$. Inductive application of (iv) implies that $\mathfrak{b}\in\mathcal{S}_{\ell-1,f}$ for some $f\in\mathcal{F}_{\ell-1}$. By Lemma 37 together with $\mathfrak{b}\sim_{\ell-1}\widetilde{\mathfrak{b}}$, we conclude $\widetilde{\mathfrak{b}}\in\mathcal{S}_{\ell-1,f}$. Now, inductive application of (v) leads to $\mathfrak{b}=\widetilde{\mathfrak{b}}$. This means we in fact have

[TABLE]

In other words, $\mathfrak{a}\sim_{\ell}\widetilde{\mathfrak{a}}$.

Ad (ii). By definition of $\sim_{\ell}$, $\mathfrak{a}\sim_{\ell}\widetilde{\mathfrak{a}}$ entails that for every $\mathfrak{b}\in\mathcal{I}_{\ell-1}$ we have

• •

$\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},i{\mathop{\mapsto}}\mathfrak{b}]\models J({\underline{1}},j,i,0)$ if and only if $\mathcal{A},[\widetilde{j}{\mathop{\mapsto}}\widetilde{\mathfrak{a}},i{\mathop{\mapsto}}\mathfrak{b}]\models J({\underline{1}},\widetilde{j},i,0)$ and

• •

$\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},i{\mathop{\mapsto}}\mathfrak{b}]\models J({\underline{1}},j,i,1)$ if and only if $\mathcal{A},[\widetilde{j}{\mathop{\mapsto}}\widetilde{\mathfrak{a}},i{\mathop{\mapsto}}\mathfrak{b}]\models J({\underline{1}},\widetilde{j},i,1)$.

By (i) and the fact that $\sim_{\ell-1}$ is an equivalence relation and thus $\mathfrak{b}\sim_{\ell-1}\mathfrak{b}$, we conclude $\mathcal{A},[i{\mathop{\mapsto}}\mathfrak{b},\widetilde{i}{\mathop{\mapsto}}\mathfrak{b}]\models\text{eq}^{\ell-1}_{i,\widetilde{i}}$ for every $\mathfrak{b}\in\mathcal{I}_{\ell-1}$. Consequently, $\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},\widetilde{j}{\mathop{\mapsto}}\widetilde{\mathfrak{a}}]\models\text{eq}^{\ell}_{j,\widetilde{j}}$.

Ad (iii). By inductive application of (vi), we know that there is a unique chain $\mathfrak{b}_{1}\prec_{\ell-1}\ldots\prec_{\ell-1}\mathfrak{b}_{p}$ comprising all elements in $\mathcal{I}_{\ell-1}$. Moreover, we observe $\mathcal{A},[i{\mathop{\mapsto}}\mathfrak{b}_{1}]\models\text{MinIdx}({\underline{\ell-1}},i)$ and $\mathcal{A},[i{\mathop{\mapsto}}\mathfrak{b}_{p}]\models\text{MaxIdx}({\underline{\ell-1}},i)$. Hence, by Lemma 38, we can arrange all mappings in $\mathcal{F}_{\ell-1}$ into a sequence $f_{1}\sqsubset_{\ell-1}\ldots\sqsubset_{\ell-1}f_{p^{\prime}}$ where $p^{\prime}=2^{p-1}+1$.

Clearly, $f_{1}$ maps every element $\mathfrak{b}\in\mathcal{I}_{\ell-1}$ to $f_{1}(\mathfrak{b})=0$, and $f_{p^{\prime}}$ maps every element $\mathfrak{b}_{k}$ with $k<p$ to $f_{p^{\prime}}(\mathfrak{b}_{k})=0$ and $\mathfrak{b}_{p}$ to $f_{p^{\prime}}(\mathfrak{b}_{p})=1$. By $\mathcal{A}\models\psi_{3}\wedge\psi_{10}$, we know that $\mathcal{A},[j{\mathop{\mapsto}}d_{\ell}^{\mathcal{A}},i{\mathop{\mapsto}}\mathfrak{b}]\models J({\underline{\ell}},j,i,0)$ for every $\mathfrak{b}\in\mathcal{I}_{\ell-1}$. Hence, $d_{\ell}^{\mathcal{A}}\in S_{\ell,f_{1}}$.

We next show that for every $k$, $1\leq k<p^{\prime}$, if $S_{\ell,f_{k}}$ is nonempty, then $S_{\ell,f_{k+1}}$ is nonempty. Let $\mathfrak{a}$ be an element of $S_{\ell,f_{k}}$. Because of $k<p^{\prime}$, we know that $\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},i{\mathop{\mapsto}}\mathfrak{b}_{p}]\models J({\underline{\ell}},j,i,0)$. By virtue of (i) and due to $\mathcal{A}\models\psi_{16}$ we conclude that there are elements $\widetilde{\mathfrak{a}},\widetilde{\mathfrak{a}}^{\prime}\in\mathcal{I}_{\ell}$ such that $\mathfrak{a}\sim_{\ell}\widetilde{\mathfrak{a}}$ and $\widetilde{\mathfrak{a}}\prec_{\ell}\widetilde{\mathfrak{a}}^{\prime}$. Moreover, Lemma 37 leads to $\widetilde{\mathfrak{a}}\in S_{\ell,f_{k}}$. By Lemma 35, this results in $\widetilde{\mathfrak{a}}^{\prime}\in\mathcal{S}_{\ell,f_{k+1}}$.

Ad (iv). As a consequence of $\mathcal{A}\models\psi_{13}$ there is a unique partial mapping $g_{\mathfrak{a}}:\mathcal{I}_{\ell-1}\to\{0,1\}$ for every $\mathfrak{a}\in\mathcal{I}_{\ell}$ such that for every $\mathfrak{b}\in\mathcal{I}_{\ell-1}$ we have $\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},i{\mathop{\mapsto}}\mathfrak{b}]\models J({\underline{\ell}},j,i,g_{\mathfrak{a}}(\mathfrak{b}))$ if and only if $g_{\mathfrak{a}}$ is defined for $\mathfrak{b}$. Because of $\mathcal{A}\models\chi_{2}$, we know that $g_{\mathfrak{a}}$ must be total.

For every $\mathfrak{a}\in\mathcal{I}_{\ell}$ where $g_{\mathfrak{a}}(e_{\ell-1}^{\mathcal{A}})=0$ we have $g_{\mathfrak{a}}\in\mathcal{F}_{\ell-1}$ and thus also $\mathfrak{a}\in\mathcal{S}_{\ell,g_{\mathfrak{a}}}$.

Because of $\mathcal{A}\models\psi_{5}\wedge\psi_{11}\wedge\psi_{12}$ we know that $\mathcal{A}\models\text{MaxIdx}({\underline{\ell}},e_{\ell})$ and that $e_{\ell}^{\mathcal{A}}$ is the only element in $\mathcal{I}_{\ell}$ for which $\mathcal{A},[j{\mathop{\mapsto}}e_{\ell}^{\mathcal{A}},i{\mathop{\mapsto}}e_{\ell-1}^{\mathcal{A}}]\models J({\underline{\ell}},j,i,1)$.

It remains to show that for every $\mathfrak{b}\in\mathcal{I}_{\ell-1}$ with $\mathfrak{b}\neq e_{\ell-1}^{\mathcal{A}}$ we have $\mathcal{A},[j{\mathop{\mapsto}}e_{\ell}^{\mathcal{A}},i{\mathop{\mapsto}}\mathfrak{b}]\models J({\underline{\ell}},j,i,0)$. But this is a consequence of (iii) and the fact that the total function $f_{*}$ mapping all elements $\mathfrak{b}$ in $\mathcal{I}_{\ell-1}$ but $e_{\ell-1}^{\mathcal{A}}$ to $f_{*}(\mathfrak{b})=0$ belongs to $\mathcal{F}_{\ell-1}$, and thus $\mathcal{S}_{\ell,f_{*}}$ is nonempty. In particular, $\mathcal{S}_{\ell,f_{*}}=\{e_{\ell}^{\mathcal{A}}\}$.

Consequently, $\mathcal{I}_{\ell}$ cannot contain any elements that do not lie in $\bigcup_{f\in\mathcal{F}_{\ell-1}}\mathcal{S}_{\ell,f}$.

Ad (v). Consider any set $\mathcal{S}_{\ell,f}$. By virtue of (iii), $\mathcal{S}_{\ell,f}$ contains at least one element. Suppose we are given two elements $\mathfrak{a},\mathfrak{a}^{\prime}$ in $\mathcal{S}_{\ell,f}$. By virtue of Lemma 36, this means $\mathfrak{a}\sim_{\ell}\mathfrak{a}^{\prime}$.

Because of $\mathcal{A}\models\chi_{3}$, there are two elements $\widetilde{\mathfrak{a}},\widetilde{\mathfrak{a}}^{\prime}\in\mathcal{I}_{\ell}$ for which (i) entails $\mathfrak{a}\sim_{\ell}\widetilde{\mathfrak{a}}$ and $\mathfrak{a}^{\prime}\sim_{\ell}\widetilde{\mathfrak{a}}^{\prime}$. By symmetry and transitivity of $\sim_{\ell}$, we have $\widetilde{\mathfrak{a}}\sim_{\ell}\widetilde{\mathfrak{a}}^{\prime}$. Hence, we observe

[TABLE]

Consequently, $\mathcal{A}\models\chi_{3}$ leads to $\mathfrak{a}=\mathfrak{a}^{\prime}$.

Ad (vi). As we have seen in the proof of Lemma 38, we can define a bijective mapping $\mu$ that maps the functions in $\mathcal{F}_{\ell-1}$ to bit strings of length $\mu$ that either have a [math] as most significant bit or correspond to $0\ldots 01$ (where the most significant bit is the rightmost one).

Let $p^{\prime}:=2^{|\mathcal{I}_{\ell-1}|-1}+1$. By virtue of Lemma 38, we can uniquely construct a chain

[TABLE]

comprising all functions in $\mathcal{F}_{\ell-1}$.

Properties (iv) and (v) together yield that $\mathcal{I}_{\ell}=\{\mathfrak{a}_{1},\ldots,\mathfrak{a}_{p^{\prime}}\}$ where $\mathfrak{a}_{k}\in\mathcal{S}_{\ell,f_{k}}$ for every $k=1,\ldots,p^{\prime}$. Lemma 35 says that for any $\mathfrak{a}_{k},\mathfrak{a}_{k^{\prime}}$ with $\mathfrak{a}_{k}\prec_{\ell}\mathfrak{a}_{k^{\prime}}$ we observe $f_{k}\sqsubset_{\ell-1}f_{k^{\prime}}$. By definition of $\sqsubset_{\ell-1}$ and the fact that all the $f_{k},f_{k^{\prime}}$ are distinct, it clearly holds that $f_{k}\sqsubset_{\ell-1}f_{k^{\prime}}$ implies $k^{\prime}=k+1$ and $1\leq k<k^{\prime}\leq p^{\prime}$. Hence, $\mathfrak{a}_{k}\prec_{\ell}\mathfrak{a}_{k^{\prime}}$ can only hold if $k^{\prime}=k+1$ and $1\leq k<k^{\prime}\leq p^{\prime}$.

Consider any element $\mathfrak{a}\in\mathcal{I}_{\ell}$ for which $\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},i{\mathop{\mapsto}}e_{\ell-1}^{\mathcal{A}}]\models J({\underline{\ell}},j,i,0)$. By $\mathcal{A}\models\psi_{16}$, we know that there are elements $\widetilde{\mathfrak{a}},\widetilde{\mathfrak{a}}^{\prime}\in\mathcal{I}_{\ell}$ such that $\widetilde{\mathfrak{a}}\prec_{\ell}\widetilde{\mathfrak{a}}^{\prime}$ and $\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},\widetilde{j}{\mathop{\mapsto}}\widetilde{\mathfrak{a}}]\models\text{eq}^{\ell}_{j,\widetilde{j}}$. By (i), the latter translates to $\mathfrak{a}\sim_{\ell}\widetilde{\mathfrak{a}}$.

Let $g,\widetilde{g}$ be functions such that $\mathfrak{a}\in\mathcal{S}_{\ell,g}$ and $\widetilde{\mathfrak{a}}\in\mathcal{S}_{\ell,\widetilde{g}}$. Such functions exist by virtue of (iv). However, $\mathfrak{a}\sim_{\ell}\widetilde{\mathfrak{a}}$ entails $g=\widetilde{g}$, by Lemma 37. Moreover, (v) leads to $\mathfrak{a}=\widetilde{\mathfrak{a}}$. Consequently, we have $\mathfrak{a}\prec_{\ell}\widetilde{\mathfrak{a}}^{\prime}$. By (v), this means that all but one element in $\mathcal{I}_{\ell}$ must have a successor in $\mathcal{I}_{\ell}$ and all but one element in $\mathcal{I}_{\ell}$ are successor in $\mathcal{I}_{\ell}$. Hence, we obtain the chain $\mathfrak{a}_{1}\prec_{\ell}\mathfrak{a}_{2}\prec_{\ell}\ldots\prec_{\ell}\mathfrak{a}_{p^{\prime}-1}\prec_{\ell}\mathfrak{a}_{p^{\prime}}$ where $\mathfrak{a}_{1}=d_{\ell}^{\mathcal{A}}$ and $\mathfrak{a}_{p^{\prime}}=e_{\ell}^{\mathcal{A}}$. ∎

The following is a corollary of the previous lemma, and so is Lemma 24.

Corollary 41**.**

For every $\ell=1,\ldots,\kappa$ we have $|\mathcal{I}_{\ell}|=p$ where $p:=2^{|\mathcal{I}_{\ell-1}|-1}+1={2^{\uparrow\ell}(\mu-1)}+1$. Moreover, there is a unique chain $\mathfrak{a}_{1}\prec_{\ell}\ldots\prec_{\ell}\mathfrak{a}_{p}$ comprising all elements in $\mathcal{I}_{\ell}$, and $\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a}_{1}]\models\text{MinIdx}({\underline{\ell}},j)$ and $\mathcal{A},[j^{\prime}{\mathop{\mapsto}}\mathfrak{a}_{p}]\models\text{MaxIdx}({\underline{\ell}},j^{\prime})$.

Appendix F Details regarding Section 5.2

The following sentences encode a given domino problem $\mathfrak{D}:=\langle\mathcal{D},\mathcal{H},\mathcal{V}\rangle$ plus an initial condition $\overline{D}$, which is a finite word over $\mathcal{D}$. We try to make as many sentences as possible Horn.

[TABLE]

[TABLE]

The sentences $\eta_{17}$ and $\eta_{18}$ express the initial condition $\overline{D}$ where the lower left domino tiles are predefined to be the sequence $\overline{D}=D_{1}\ldots D_{n}$.

Regarding the length of the sentences $\eta_{1},\ldots,\eta_{18}$, we observe the following:

• •

$\text{len}(\eta_{1}),\text{len}(\eta_{2}),\text{len}(\eta_{4}),\ldots,\text{len}(\eta_{8}),\text{len}(\eta_{10}),\ldots,\text{len}(\eta_{12})\in\mathcal{O}(\log\kappa)$

• •

\text{len}(\eta_{3}),\text{len}(\eta_{9})\in\mathcal{O}\bigl{(}\kappa\log\kappa+\mu(\log\kappa+\log\mu)+|\mathcal{D}|\log|\mathcal{D}|\bigr{)}

• •

\text{len}(\eta_{13})\in\mathcal{O}\bigl{(}|\mathcal{D}|(\log|\mathcal{D}|+\log\kappa)\bigr{)}

• •

\text{len}(\eta_{14})\in\mathcal{O}\bigl{(}|\mathcal{D}|^{2}\log|\mathcal{D}|\bigr{)}

• •

\text{len}(\eta_{15})\in\mathcal{O}\bigl{(}|\mathcal{H}|\log|\mathcal{D}|\bigr{)}=\mathcal{O}\bigl{(}|\mathcal{D}|^{2}\log|\mathcal{D}|\bigr{)}

• •

\text{len}(\eta_{16})\in\mathcal{O}\bigl{(}|\mathcal{H}|\log|\mathcal{D}|\bigr{)}=\mathcal{O}\bigl{(}|\mathcal{D}|^{2}\log|\mathcal{D}|\bigr{)}

• •

\text{len}(\eta_{17})\in\mathcal{O}\bigl{(}\log\kappa+n\log n\bigr{)}

• •

\text{len}(\eta_{18})\in\mathcal{O}\bigl{(}\log\kappa+n(\log n+\log|\mathcal{D}|)\bigr{)}

In total, the length of $\eta_{1}\wedge\ldots\wedge\eta_{18}$ lies in \mathcal{O}\bigl{(}\widehat{n}\log\widehat{n}\bigr{)}, where $\widehat{n}:=\max\{\kappa,\mu,n,|\mathcal{D}|^{2}\}$.

For the remainder of this subsection we consider a model $\mathcal{A}$ of the sentence $\psi_{1}\wedge\ldots\wedge\psi_{16}\wedge\chi_{1}\wedge\chi_{2}\wedge\chi_{3}\wedge\eta_{1}\wedge\ldots\wedge\eta_{18}$. Moreover, we take over the notation from Definition 23.

Definition 42**.**

We define the following relations:

• •

${\prec^{H}}\subseteq\mathcal{I}_{\kappa}^{2}\times\mathcal{I}_{\kappa}^{2}$ such that $\langle\mathfrak{a},\mathfrak{b}\rangle\prec^{H}\langle\mathfrak{a}^{\prime},\mathfrak{b}^{\prime}\rangle$ holds if and only if $\mathcal{A},[x{\mathop{\mapsto}}\mathfrak{a},y{\mathop{\mapsto}}\mathfrak{b},x^{\prime}{\mathop{\mapsto}}\mathfrak{a}^{\prime},y^{\prime}{\mathop{\mapsto}}\mathfrak{b}^{\prime}]\models H(x,y,x^{\prime},y^{\prime})$.

• •

${\prec^{V}}\subseteq\mathcal{I}_{\kappa}^{2}\times\mathcal{I}_{\kappa}^{2}$ such that $\langle\mathfrak{a},\mathfrak{b}\rangle\prec^{V}\langle\mathfrak{a}^{\prime},\mathfrak{b}^{\prime}\rangle$ holds if and only if $\mathcal{A},[x{\mathop{\mapsto}}\mathfrak{a},y{\mathop{\mapsto}}\mathfrak{b},x^{\prime}{\mathop{\mapsto}}\mathfrak{a}^{\prime},y^{\prime}{\mathop{\mapsto}}\mathfrak{b}^{\prime}]\models V(x,y,x^{\prime},y^{\prime})$.

Lemma 43**.**

For all pairs $\langle\mathfrak{a},\mathfrak{b}\rangle,\langle\mathfrak{a}^{\prime},\mathfrak{b}^{\prime}\rangle\in\mathcal{I}_{\kappa}^{2}$ we observe the following properties.

1. (i)

$\langle\mathfrak{a},\mathfrak{b}\rangle\prec^{H}\langle\mathfrak{a}^{\prime},\mathfrak{b}^{\prime}\rangle$ entails that $\mathfrak{b}=\mathfrak{b}^{\prime}$ and that either $\mathfrak{a}\prec_{\kappa}\mathfrak{a}^{\prime}$ or $\mathfrak{a}=e_{\kappa}^{\mathcal{A}}$ and $\mathfrak{a}^{\prime}=d_{\kappa}^{\mathcal{A}}$. 2. (ii)

$\mathfrak{a}=e_{\kappa}^{\mathcal{A}}$ and $\mathfrak{a}^{\prime}=d_{\kappa}^{\mathcal{A}}$ entails $\langle\mathfrak{a},\mathfrak{b}\rangle\prec^{H}\langle\mathfrak{a}^{\prime},\mathfrak{b}\rangle$ for every $\mathfrak{b}\in\mathcal{I}_{\kappa}$. 3. (iii)

$\mathfrak{a}\prec_{\kappa}\mathfrak{a}^{\prime}$ implies $\langle\mathfrak{a},\mathfrak{b}\rangle\prec^{H}\langle\mathfrak{a}^{\prime},\mathfrak{b}\rangle$ for every $\mathfrak{b}\in\mathcal{I}_{\kappa}$. 4. (iv)

$\langle\mathfrak{a},\mathfrak{b}\rangle\prec^{V}\langle\mathfrak{a}^{\prime},\mathfrak{b}^{\prime}\rangle$ entails that $\mathfrak{a}=\mathfrak{a}^{\prime}$ and that either $\mathfrak{b}\prec_{\kappa}\mathfrak{b}^{\prime}$ or $\mathfrak{b}=e_{\kappa}^{\mathcal{A}}$ and $\mathfrak{b}^{\prime}=d_{\kappa}^{\mathcal{A}}$. 5. (v)

$\mathfrak{b}=e_{\kappa}^{\mathcal{A}}$ and $\mathfrak{b}^{\prime}=d_{\kappa}^{\mathcal{A}}$ entails $\langle\mathfrak{a},\mathfrak{b}\rangle\prec^{V}\langle\mathfrak{a},\mathfrak{b}^{\prime}\rangle$ for every $\mathfrak{a}\in\mathcal{I}_{\kappa}$. 6. (vi)

$\mathfrak{b}\prec_{\kappa}\mathfrak{b}^{\prime}$ implies $\langle\mathfrak{a},\mathfrak{b}\rangle\prec^{V}\langle\mathfrak{a},\mathfrak{b}^{\prime}\rangle$ for every $\mathfrak{a}\in\mathcal{I}_{\kappa}$.

Proof.

Property (i) follows by $\mathcal{A}\models\eta_{1}\wedge\eta_{2}\wedge\eta_{5}\wedge\eta_{6}$. Property (ii) follows by $\mathcal{A}\models\eta_{4}$.

In order to show Property (iii), we have to argue a bit more. First of all, we conclude $\mathfrak{a}\neq e_{\kappa}^{\mathcal{A}}$, by $\mathcal{A}\models\psi_{2}\wedge\psi_{4}$. Because of $\mathcal{A}\models\eta_{3}$ and Lemma 40(i), for all $\mathfrak{a},\mathfrak{b}$ with $\mathfrak{a}\neq e_{\kappa}^{\mathcal{A}}$ there must exist $\widetilde{\mathfrak{a}},\widetilde{\mathfrak{b}},\widetilde{\mathfrak{a}}^{\prime}\in\mathcal{I}_{\kappa}$ such that $\mathfrak{a}\sim_{\kappa}\widetilde{\mathfrak{a}}$, $\mathfrak{b}\sim_{\kappa}\widetilde{\mathfrak{b}}$, and $\langle\widetilde{\mathfrak{a}},\widetilde{\mathfrak{b}}\rangle\prec^{H}\langle\widetilde{\mathfrak{a}}^{\prime},\widetilde{\mathfrak{b}}\rangle$. Due to Lemma 37 in combination with Lemma 40(v), we get $\mathfrak{a}=\widetilde{\mathfrak{a}}$ and $\mathfrak{b}=\widetilde{\mathfrak{b}}$. Thus, we have $\langle\mathfrak{a},\mathfrak{b}\rangle\prec^{H}\langle\widetilde{\mathfrak{a}}^{\prime},\mathfrak{b}\rangle$. Moreover, $\mathfrak{a}\neq e_{\kappa}^{\mathcal{A}}$ together with (i) leads to $\mathfrak{a}\prec_{\kappa}\widetilde{\mathfrak{a}}^{\prime}$. Since we assumed $\mathfrak{a}\prec_{\kappa}\mathfrak{a}^{\prime}$, Lemma 40(vi) says that $\mathfrak{a}^{\prime}$ is the only element satisfying $\mathfrak{a}\prec_{\kappa}\mathfrak{a}^{\prime}$, i.e. $\widetilde{\mathfrak{a}}^{\prime}=\mathfrak{a}^{\prime}$. Consequently, it in fact holds $\langle\mathfrak{a},\mathfrak{b}\rangle\prec^{H}\langle\mathfrak{a}^{\prime},\mathfrak{b}\rangle$.

Properties (iv) to (vi) can be proved analogously to the first three properties using $\mathcal{A}\models\eta_{7}\wedge\ldots\wedge\eta_{12}$. ∎

Lemma 44**.**

Let $r:={2^{\uparrow\kappa}(\mu-1)}+1$. There is a bijective mapping $\rho:\mathbb{Z}_{r}^{2}\to\mathcal{I}_{\kappa}^{2}$ such that $\rho(0,0)=\langle d_{\kappa}^{\mathcal{A}},d_{\kappa}^{\mathcal{A}}\rangle$ and for every pair $\langle s,t\rangle\in\mathbb{Z}_{r}^{2}$ we have

• •

$\rho(s,t)\prec^{H}\rho(s+1,t)$ and

• •

$\rho(s,t)\prec^{V}\rho(s,t+1)$.

where $+$ stands for addition modulo $r$.

Proof.

By Corollary 41 we know that there is a unique chain $\mathfrak{a}_{1}\prec_{\kappa}\ldots\prec_{\kappa}\mathfrak{a}_{r}$ comprising all elements in $\mathcal{I}_{\kappa}$. Notice that $\mathfrak{a}_{k},\mathfrak{a}_{k^{\prime}}$ with $k\neq k^{\prime}$ are distinct. We define $\rho$ so that $\rho(s,t):=\langle\mathfrak{a}_{s+1},\mathfrak{a}_{t+1}\rangle$ for all $s,t\in\mathbb{Z}_{r}=\{0,\ldots r-1\}$.

Obviously, $\rho$ is bijective. Since $\mathfrak{a}_{1}$ is the only element in $\mathcal{I}_{\kappa}$ for which there is no $\mathfrak{b}$ in the above chain with $\mathfrak{b}\prec_{\kappa}\mathfrak{a}_{1}$, $\mathcal{A}\models\psi_{2}\wedge\psi_{3}$ enforces $\mathfrak{a}_{1}=d_{\kappa}^{\mathcal{A}}$. Hence, $\rho(0,0)=\langle d_{\kappa}^{\mathcal{A}},d_{\kappa}^{\mathcal{A}}\rangle$.

Since $\mathfrak{a}_{r}$ is the only element in $\mathcal{I}_{\kappa}$ for which there is no $\mathfrak{b}^{\prime}$ in the above chain with $\mathfrak{a}_{r}\prec_{\kappa}\mathfrak{b}^{\prime}$, $\mathcal{A}\models\psi_{4}\wedge\psi_{5}$ enforces $\mathfrak{a}_{r}=e_{\kappa}^{\mathcal{A}}$. Hence, Lemma 43(ii) entails $\rho(r-1,t)\prec^{H}\rho(0,t)$ for every $t\in\mathbb{Z}_{r}$. Moreover, the existence of the above chain together with Lemma 43(iii) leads to $\rho(s,t)\prec^{H}\rho(s+1,t)$ for every $s\in\mathbb{Z}_{r}\setminus\{r-1\}$ and every $t\in\mathbb{Z}_{r}$. Consequently, we observe $\rho(s,t)\prec^{H}\rho(s+1,t)$—modulo $r$—for every pair $\langle s,t\rangle\in\mathbb{Z}_{r}^{2}$.

By similar arguments, we may infer $\rho(s,t)\prec^{V}\rho(s,t+1)$ for every pair $\langle s,t\rangle\in\mathbb{Z}_{r}^{2}$. ∎

Lemma 45**.**

Assume that $\mathcal{D}$, $\mathcal{H}$, and $\mathcal{V}$ are nonempty. For all pairs $\langle\mathfrak{a},\mathfrak{b}\rangle\in\mathcal{I}_{\kappa}$ we have $\mathcal{A},[x{\mathop{\mapsto}}\mathfrak{a},y{\mathop{\mapsto}}\mathfrak{b}]\models{\underline{D}}(x,y)$ for exactly one $D\in\mathcal{D}$.

Proof.

Due to $\mathcal{A}\models\eta_{15}\wedge\eta_{16}$, we observe the following properties for all pairs $\langle\mathfrak{a},\mathfrak{b}\rangle,\langle\mathfrak{a}^{\prime},\mathfrak{b}^{\prime}\rangle\in\mathcal{I}_{\kappa}^{2}$:

• •

$\langle\mathfrak{a},\mathfrak{b}\rangle\!\prec^{H}\!\!\langle\mathfrak{a}^{\prime},\mathfrak{b}^{\prime}\rangle$ implies that there are $D,D^{\prime}\in\mathcal{D}$ such that $\langle D,D^{\prime}\rangle\in\mathcal{H}$ and $\mathcal{A},[x{\mathop{\mapsto}}\mathfrak{a},y{\mathop{\mapsto}}\mathfrak{b}]\models{\underline{D}}(x,y)$ and $\mathcal{A},[x{\mathop{\mapsto}}\mathfrak{a}^{\prime},y{\mathop{\mapsto}}\mathfrak{b}^{\prime}]\models{\underline{D}}^{\prime}(x,y)$.

• •

$\langle\mathfrak{a},\mathfrak{b}\rangle\!\prec^{V}\!\!\langle\mathfrak{a}^{\prime},\mathfrak{b}^{\prime}\rangle$ implies that there are $D,D^{\prime}\in\mathcal{D}$ such that $\langle D,D^{\prime}\rangle\in\mathcal{V}$ and $\mathcal{A},[x{\mathop{\mapsto}}\mathfrak{a},y{\mathop{\mapsto}}\mathfrak{b}]\models{\underline{D}}(x,y)$ and $\mathcal{A},[x{\mathop{\mapsto}}\mathfrak{a}^{\prime},y{\mathop{\mapsto}}\mathfrak{b}^{\prime}]\models{\underline{D}}^{\prime}(x,y)$.

By virtue of Lemma 44, we know that there is a bijection $\rho$ such that for every pair $\langle\mathfrak{a},\mathfrak{b}\rangle$ in the image of $\rho$ there is another pair $\langle\mathfrak{a}^{\prime},\mathfrak{b}^{\prime}\rangle$ such that $\langle\mathfrak{a},\mathfrak{b}\rangle\prec^{H}\langle\mathfrak{a}^{\prime},\mathfrak{b}^{\prime}\rangle$ or $\langle\mathfrak{a},\mathfrak{b}\rangle\prec^{V}\langle\mathfrak{a}^{\prime},\mathfrak{b}^{\prime}\rangle$. Since the image of $\rho$ is $\mathcal{I}_{\kappa}^{2}$, this means that there is at least one $D\in\mathcal{D}$ for every pair $\langle\mathfrak{a},\mathfrak{b}\rangle\in\mathcal{I}_{\kappa}^{2}$ such that $\mathcal{A},[x{\mathop{\mapsto}}\mathfrak{a},y{\mathop{\mapsto}}\mathfrak{b}]\models{\underline{D}}(x,y)$.

Finally, because of $\mathcal{A}\models\eta_{14}$ we know that there is at most one $D\in\mathcal{D}$ for every pair $\langle\mathfrak{a},\mathfrak{b}\rangle\in\mathcal{I}_{\kappa}^{2}$ such that $\mathcal{A},[x{\mathop{\mapsto}}\mathfrak{a},y{\mathop{\mapsto}}\mathfrak{b}]\models{\underline{D}}(x,y)$. ∎

Lemma 25**.**

Let $r:={2^{\uparrow\kappa}(\mu-1)}+1$ and assume that $\mathcal{D}$, $\mathcal{H}$, and $\mathcal{V}$ are nonempty. $\mathcal{A}$ induces a tiling $\tau$ of $\mathbb{Z}_{r}^{2}$ with initial condition $\overline{D}:=D_{1},\ldots,D_{n}$.

Proof.

Let $\rho$ be a bijection according to Lemma 44. We define the mapping $\tau$ such that $\tau(s,t):=D$ if and only if $\rho(s,t)=\langle\mathfrak{a},\mathfrak{b}\rangle$ and $\mathcal{A},[x{\mathop{\mapsto}}\mathfrak{a},y{\mathop{\mapsto}}\mathfrak{b}]\models{\underline{D}}(x,y)$. By Lemma 45, we know that $\tau$ is well defined.

By $\mathcal{A}\models\eta_{17}\wedge\eta_{18}$, we know that $\mathcal{A},[x{\mathop{\mapsto}}\mathfrak{a},y{\mathop{\mapsto}}\mathfrak{b}]\models{\underline{D}}_{i}(x,y)$ for $\langle\mathfrak{a},\mathfrak{b}\rangle=\rho(i,0)$ and $i=0,\ldots,n-1$. Hence, $\tau$ satisfies the initial condition.

By definition of $\rho$ and because of $\mathcal{A}\models\eta_{15}\wedge\eta_{16}$, we observe the following:

• •

For every pair $\langle s,t\rangle\in\mathbb{Z}_{r}^{2}$ there are pairs $\langle D,D^{\prime}\rangle\in\mathcal{H}$, $\langle\mathfrak{a},\mathfrak{b}\rangle=\rho(s,t)$, and $\langle\mathfrak{a}^{\prime},\mathfrak{b}^{\prime}\rangle=\rho(s+1,t)$ such that

• –

$\mathcal{A},[x{\mathop{\mapsto}}\mathfrak{a},y{\mathop{\mapsto}}\mathfrak{b}]\models{\underline{D}}(x,y)$ and

• –

$\mathcal{A},[x{\mathop{\mapsto}}\mathfrak{a}^{\prime},y{\mathop{\mapsto}}\mathfrak{b}^{\prime}]\models{\underline{D}}^{\prime}(x,y)$.

• •

For every pair $\langle s,t\rangle\in\mathbb{Z}_{r}^{2}$ there are pairs $\langle D,D^{\prime}\rangle\in\mathcal{V}$, $\langle\mathfrak{a},\mathfrak{b}\rangle=\rho(s,t)$, and $\langle\mathfrak{a}^{\prime},\mathfrak{b}^{\prime}\rangle=\rho(s,t+1)$ such that

• –

$\mathcal{A},[x{\mathop{\mapsto}}\mathfrak{a},y{\mathop{\mapsto}}\mathfrak{b}]\models{\underline{D}}(x,y)$ and

• –

$\mathcal{A},[x{\mathop{\mapsto}}\mathfrak{a}^{\prime},y{\mathop{\mapsto}}\mathfrak{b}^{\prime}]\models{\underline{D}}^{\prime}(x,y)$.

Consequently, the mapping $\tau$ constitutes a proper tiling of $\mathbb{Z}_{r}^{2}$. ∎

Appendix G Details regarding Section 5.3

The following sentences comprise the axioms of reflexivity, symmetry, transitivity, and several axioms of congruence ($\psi^{\prime}_{1},\ldots,\psi^{\prime}_{12},\eta^{\prime}_{1},\ldots,\eta^{\prime}_{10}$) for the binary predicate $E$ that is introduced to replace equality.

[TABLE]

[TABLE]

Regarding the length of the above sentences, we observe the following:

• •

$\text{len}(\psi^{\prime}_{1}),\text{len}(\psi^{\prime}_{2}),\text{len}(\psi^{\prime}_{3})\in\mathcal{O}(1)$,

• •

$\text{len}(\eta^{\prime}_{1}),\ldots,\text{len}(\eta^{\prime}_{8})\in\mathcal{O}(1)$,

• •

$\text{len}(\psi^{\prime}_{4}),\ldots,\text{len}(\psi^{\prime}_{12})\in\mathcal{O}(\kappa\log\kappa)$,

• •

\text{len}(\eta^{\prime}_{9}),\text{len}(\eta^{\prime}_{10})\in\mathcal{O}\bigl{(}|\mathcal{D}|\log|\mathcal{D}|\bigr{)}.

Lemma 26**.**

Let $\varphi:=\psi_{1}\wedge\ldots\psi_{16}\wedge\chi_{1}\wedge\chi_{2}\wedge\chi_{3}\wedge\eta_{1}\wedge\ldots\wedge\eta_{18}$. Let $\widehat{\varphi}$ be the result of replacing every atom $s\approx t$ in $\varphi$ with $E(s,t)$. Moreover, let $\psi^{\prime}:=\psi^{\prime}_{1}\wedge\ldots\wedge\psi^{\prime}_{12}$ and $\eta^{\prime}:=\eta^{\prime}_{1}\wedge\ldots\wedge\eta^{\prime}_{10}$.

1. (i)

Every model $\mathcal{A}\models\varphi$ can be extended to a model $\mathcal{B}\models\widehat{\varphi}\wedge\psi^{\prime}\wedge\eta^{\prime}$ over the same domain. 2. (ii)

From every model $\mathcal{B}\models\widehat{\varphi}\wedge\psi^{\prime}\wedge\eta^{\prime}$ we can construct a model $\mathcal{A}\models\varphi$.

Proof.

Ad (i). Let $\mathcal{A}$ be a model of $\varphi$. We define $\mathcal{B}$ exactly like $\mathcal{A}$ except for the interpretation of $E$, which we define to be $E^{\mathcal{B}}:=\{\langle\mathfrak{a},\mathfrak{a}\rangle\mid\mathfrak{a}\in\mathfrak{U}_{\mathcal{A}}\}$. Clearly, we have $\mathcal{B}\models\varphi$ and also $\mathcal{B}\models\widehat{\varphi}$. Moreover, it is easy to see that $\mathcal{B}\models\psi^{\prime}\wedge\eta^{\prime}$.

Ad (ii). Let $\mathcal{B}$ be a model of $\widehat{\varphi}\wedge\psi^{\prime}\wedge\eta^{\prime}$. For all domain elements $\mathfrak{a},\mathfrak{b}\in\mathfrak{U}_{\mathfrak{B}}$ we write $\mathfrak{a}\sim_{E}\mathfrak{b}$ if and only if $\mathcal{B},[j{\mathop{\mapsto}}\mathfrak{a},j^{\prime}{\mathop{\mapsto}}\mathfrak{b}]\models E(j,j^{\prime})$. Due to $\mathcal{B}\models\psi^{\prime}_{1}\wedge\psi^{\prime}_{2}\wedge\psi^{\prime}_{3}$, we know that $\sim_{E}$ constitutes an equivalence relation on $\mathfrak{U}_{\mathcal{B}}$. Let $\mathfrak{U}_{\mathcal{B}}/_{\sim_{E}}$ be the set of all equivalence classes induced by $\sim_{E}$.

Claim I: Consider two variable assignments $\beta,\beta^{\prime}$ such that for every variable $j$ we have $\beta(j)\sim_{E}\beta^{\prime}(j)$. For every atom $A$ occurring in $\widehat{\varphi}$ we have $\mathcal{B},\beta\models A$ if and only if $\mathcal{B},\beta^{\prime}\models A$.

Proof: We distinguish two cases: Let $A=P(\ldots)$, where $P$ is one of the predicate symbols $L$, MinIdx, MaxIdx, Succ, $J$, $J^{*}$, $H$, $V$, or ${\underline{D}}$ with $D\in\mathcal{D}$. Then the claim follows due to $\mathcal{B}\models\psi^{\prime}\wedge\eta^{\prime}$ and the definition of $\sim_{E}$.

Let $A=E(j,i)$. Assume $\mathcal{B},\beta\models E(j,i)$. Hence, we have $\beta^{\prime}(j)\sim_{E}\beta(j)\sim_{E}\beta(i)\sim_{E}\beta^{\prime}(i)$. By transitivity of $\sim_{E}$ it follows that $\beta^{\prime}(j)\sim_{E}\beta^{\prime}(i)$, and thus we have $\mathcal{B},\beta^{\prime}\models E(j,i)$.

Assume $\mathcal{B},\beta^{\prime}\models E(j,i)$. Hence, we have $\beta(j)\sim_{E}\beta^{\prime}(j)\sim_{E}\beta^{\prime}(i)\sim_{E}\beta(i)$. By transitivity of $\sim_{E}$ it follows that $\beta(j)\sim_{E}\beta(i)$, and thus we have $\mathcal{B},\beta\models E(j,i)$. $\Diamond$

We define the structure $\mathcal{A}$ as follows:

• •

We define $\mathfrak{U}_{\mathcal{A}}$ such that it contains exactly one representative from every equivalence class in $\mathfrak{U}_{\mathcal{B}}/_{\sim_{E}}$.

• •

For every constant symbol $c$ occurring in $\widehat{\varphi}$ we set $c^{\mathcal{A}}:=\mathfrak{c}$, where $\mathfrak{c}$ is the representative in $\mathfrak{U}_{\mathcal{A}}$ such that it represents the $\sim_{E}$-class of $c^{\mathcal{B}}$, i.e. $[\mathfrak{c}]_{\sim_{E}}=[c^{\mathcal{B}}]_{\sim_{E}}$.

• •

For every predicate symbol $P$ occurring in $\widehat{\varphi}$ we set $P^{\mathcal{A}}:=P^{\mathcal{B}}\cap\mathfrak{U}_{\mathcal{A}}^{m}$, where $m$ is the arity of $P$.

Claim II: $\mathcal{A}\models\widehat{\varphi}$.

Proof: By construction of $\mathfrak{U}_{\mathcal{A}}$, we can find for every variable assignment $\beta$ mapping variables to elements in $\mathfrak{U}_{\mathcal{B}}$ another variable assignment $\beta^{\prime}$ mapping every variable to an element in $\mathfrak{U}_{\mathcal{A}}$ such that $\beta(j)\sim_{E}\beta^{\prime}(j)$ holds for every variable $j$. Consequently, using Claim I, we can show that $\mathcal{A}\models\widehat{\varphi}$ holds by induction on the structure of $\widehat{\varphi}$. $\Diamond$

From the definition of $\mathcal{A}$ it follows that $E^{\mathcal{A}}=\{\langle\mathfrak{a},\mathfrak{a}\rangle\mid\mathfrak{a}\in\mathfrak{U}_{\mathcal{A}}\}$. Hence, for all $\mathfrak{a},\mathfrak{b}\in\mathfrak{U}_{\mathcal{A}}$ we have $\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},j^{\prime}{\mathop{\mapsto}}\mathfrak{b}]\models E(j,j^{\prime})$ if and only if $\mathcal{A},[j{\mathop{\mapsto}}\mathfrak{a},j^{\prime}{\mathop{\mapsto}}\mathfrak{b}]\models j\approx j^{\prime}$. This observation together with Claim II entails $\mathcal{A}\models\varphi$. ∎