*This paper is a consolidated, revised and extended version of [FK23] and [Kie23]

# Alternating Quantifiers
in Uniform One-Dimensional Fragments
with an Excursion into Three-Variable Logic

Oskar Fiuk  Emanuel Kieroński0000-0002-8538-8221  Institute of Computer
Science, University of Wrocław, Poland<EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract

The uniform one-dimensional fragment of first-order logic was introduced a few
years ago as a generalization of the two-variable fragment to contexts
involving relations of arity greater than two. Quantifiers in this logic are
used in blocks, each block consisting only of existential quantifiers or only
of universal quantifiers. In this paper we consider the possibility of mixing
both types of quantifiers in blocks. We show the finite (exponential) model
property and NExpTime-completeness of the satisfiability problem for two
restrictions of the resulting formalism: in the first we require that every
block of quantifiers is either purely universal or ends with the existential
quantifier, in the second we restrict the number of variables to three; in
both equality is not allowed. We also extend the second variation to a rich
subfragment of the three-variable fragment (without equality) that still has
the finite model property and decidable, NExpTime-complete satisfiability.

###### keywords:

satisfiability problem, finite model property, uniform one-dimensional
fragment, three-variable logic

##  1 Introduction

In this paper we aim to advance the research on the uniform one-dimensional
fragment of first-order logic, $\mbox{\rm UF}_{1}$. Additionally, we will take
an excursion to the area of three-variable logic and get close to the limits
of decidability.

As $\mbox{\rm UF}_{1}$ was originally proposed as a generalization of the two-
variable fragment, $\mbox{\rm FO}^{2}$, to contexts with relations of
arbitrary arity, we set up the scene by recalling the most important facts
about $\mbox{\rm FO}^{2}$.

The two-variable fragment. $\mbox{\rm FO}^{2}$ is obtained just by restricting
first-order logic so that formulas may use only variables $x$ and $y$, and is
considered as one of the most significant decidable fragments of first-order
logic identified so far. The decidability of its satisfiability problem was
shown by Scott [Sco62] in the case without equality, and by Mortimer [Mor75]
in the case with equality. Actually, in [Mor75] it is proved that $\mbox{\rm
FO}^{2}$ has the finite model property, that is, every satisfiable $\mbox{\rm
FO}^{2}$-sentence has a finite model. Later, Grädel, Kolaitis and Vardi
[GKV97] strengthened that result by showing the exponential model property of
$\mbox{\rm FO}^{2}$, that is, every satisfiable $\mbox{\rm FO}^{2}$-sentence
has a model of size bounded exponentially in its length. The latter result
establishes that the satisfiability problem for $\mbox{\rm FO}^{2}$ is in
NExpTime. The matching lower bound follows from the earlier work by Lewis
[Lew80]. It turns out that with respect to the number of variables $\mbox{\rm
FO}^{2}$ is the maximal decidable fragment of FO, as already the three-
variable fragment, $\mbox{\rm FO}^{3}$, has undecidable satisfiability
[KMW62].

An important motivation for studying $\mbox{\rm FO}^{2}$ is that it embeds,
via the so-called standard translation, basic modal logic and many standard
description logics. Thus, $\mbox{\rm FO}^{2}$ constitutes an elegant first-
order framework for analysing those formalisms. Its simplicity and naturalness
make it also an attractive logic in itself, with applications in knowledge
representation, artificial intelligence, and verification of hardware and of
software. In the last few decades, $\mbox{\rm FO}^{2}$ together with its
extensions and variations have been extensively studied and plenty of results
have been obtained, to mention just a few of them: decidability was shown for
$\mbox{\rm FO}^{2}$ with counting quantifiers [GOR97, PST97, Pra10], one or
two equivalence relations [KO12, KMPT14], counting quantifiers and equivalence
relation [Pra15], betweenness relations [KLPS20], and its complexity was
established on words and trees, in various scenarios, including the presence
of data or counting [BMSS09, BDM+11, CW13, CW15, BBC+16].

Decidable fragments embedding $\mbox{\rm FO}^{2}$. Further applications of
$\mbox{\rm FO}^{2}$, e.g., in database theory, are limited, as $\mbox{\rm
FO}^{2}$ and its extensions mentioned above can speak non-trivially only about
relations of arity at most two, unlike many other decidable fragments studied
because of their potential applications in computer science, e.g., the guarded
fragment, GF [AvBN98], the unary negation fragment, UNFO [tCS13], the guarded
negation fragment, GNFO [BtCS15], or the fluted fragment, FF [Qui69, PST19].

Hence, a natural question arises: Is there an elegant decidable formalism
which retains full expressivity of $\mbox{\rm FO}^{2}$, but additionally,
allows one to speak non-trivially about relations of arity bigger than two? In
the recent literature, several proposals have emerged in this direction.

One of them is an idea of combining $\mbox{\rm FO}^{2}$ with GF, which can
found in Kazakov’s PhD thesis [Kaz06], and was also present in the work by
Bourish, Morak and Pieris [BMP17]. In the end, it received a more systematic
treatment in the paper by Rudolph and Šimkus [RŠ18], who formally introduced
the triguarded fragment, TGF, which is obtained from GF by allowing
quantification for subformulas with at most two free variables to be
unguarded. This yields a logic in which one can speak freely about pairs of
elements and in a local, guarded way about tuples of bigger arity. However,
TGF turns out to be undecidable with equality, but becomes decidable when
equality is forbidden. The satisfiability problem is then 2-ExpTime\- or
2-NExpTime-complete, depending on whether constants are allowed in signatures
[RŠ18]; the finite model property is retained [KR21]. A variation of the idea
above is the one-dimensional triguarded fragment [Kie19], still containing
$\mbox{\rm FO}^{2}$, which is decidable even in the presence of equality.

$\mbox{\rm FO}^{2}$ (or, actually, even its extension with counting
quantifiers, C2) combined with FF was demonstrated to be decidable by Pratt-
Hartmann [Pra21], but the complexity of its satisfiability problem is non-
elementary, as already FF alone has non-elementary complexity [PST19].
Recently, Bednarczyk, Kojelis and Pratt-Hartmann proposed a generalization of
FF, called the adjacent fragment [BKP23] which also embeds $\mbox{\rm
FO}^{2}$.

Finally, the most canonical generalization of $\mbox{\rm FO}^{2}$ to contexts
with relations of arbitrary arity, capturing the spirit of $\mbox{\rm FO}^{2}$
more faithfully than the formalisms discussed above, is the _uniform one-
dimensional fragment_ , $\mbox{\rm UF}_{1}$, proposed by Hella and Kuusisto
[HK14].

In $\mbox{\rm UF}_{1}$ quantifiers are used in blocks and each block consists
exclusively of existential or universal quantifiers, and leaves at most one
variable free; a fragment meeting this condition is called _one-dimensional_.
However, one-dimensionality alone is not sufficient for the decidability of
the satisfiability problem [HK14], and thus another restriction is needed. In
the case of $\mbox{\rm UF}_{1}$, this is the _uniformity_ restriction, which,
roughly speaking, permits to use atoms with at least two variables in the same
Boolean combination only if they use precisely the same set of variables
(atoms using only a single variable can be used freely). In effect, just as
$\mbox{\rm FO}^{2}$ contains modal logic (or even Boolean modal logic),
$\mbox{\rm UF}_{1}$ contains _polyadic_ modal logic (even with negations of
the accessibility relations, cf. [Kuu16]). In [HK14] it is shown that
$\mbox{\rm UF}_{1}$ without equality is decidable and has the finite model
property. In [KK14] this result is strengthened by proving that $\mbox{\rm
UF}_{1}$, even with a _free use_ of equalities, has the exponential model
property and thus NExpTime-complete satisfiability, exactly as $\mbox{\rm
FO}^{2}$. Here,  _free use_ means that the uniformity restriction does not
constrain the use of equality symbol.

Now, it should be evident why we regard $\mbox{\rm UF}_{1}$ as the canonical
extension of $\mbox{\rm FO}^{2}$, given that the latter naturally satisfies
both restrictions. The requirement of one-dimensionality is fulfilled whenever
a quantifier binds a variable, such as $x$, automatically leaving only $y$.
Similarly, the uniformity restriction is trivially met, since the set
$\\{x,y\\}$ admits only singleton non-empty proper subsets, implying that non-
singleton atoms must precisely mention it.

Undecidability of $\mbox{\rm FO}^{3}$. We already mentioned that the three-
variable fragment is undecidable. The first undecidability proof is due to
Kahr, Moore and Wang [KMW62]. More precisely, they demonstrated that the class
of formulas of the shape $\forall x\exists y\forall z\psi(x,y,z)$, with $\psi$
being quantifier-free and without equality, is undecidable. Apart that, there
are two other sources of undecidability of $\mbox{\rm FO}^{3}$ that are worth
highlighting here. The first one is that in $\mbox{\rm FO}^{3}$ it is possible
to specify that some binary relations are transitive (by the obvious formulas
starting with the quantification pattern $\forall\forall\forall$). This leads
us to undecidability, as already $\mbox{\rm FO}^{2}$ (and even its guarded
subfragment) with two transitive relations is undecidable (see Kazakov’s Phd
thesis [Kaz06] or [Kie05]). The second one is that the class of formulas
admitting equality and of the shape $\forall\forall\exists\psi(x,y,z)$, with
$\psi$ being quantifier-free, constitutes a three-variable subfragment of the
Gödel class with equality, which is known to be undecidable from the work of
Goldfarb [Gol84].

Our contribution. We aimed to discover attractive extensions of $\mbox{\rm
UF}_{1}$, enabling the expression of even more interesting properties while
preserving the decidability of satisfiability. As we have previously
discussed, both $\mbox{\rm UF}_{1}$ and $\mbox{\rm FO}^{2}$ are already quite
robust and significant fragments of FO. Therefore, studying their extensions
is a well-justified research direction in its own right. Moreover, this can
help us to better understand the limits of decidability, a long-standing theme
in computer science. We also believe that novel formalisms might be useful in
practice by offering powerful extensions of modal and description logics to
contexts involving relations of arity greater than two.

In the definition of $\mbox{\rm UF}_{1}$, there is a stipulation that each
block of quantifiers must exclusively use either universal or existential
quantifiers. We embarked our investigation with compelling questions: Is this
requirement necessary for decidability? What implications arise for the
complexity of satisfiability if we permit to mix quantifiers inside blocks?

For illustrative purposes, consider the following property _“every director
has an actor who played in his all famous movies”_ , which can be expressed in
FO as follows:

$\displaystyle\forall d\exists a\forall m\big{[}\big{(}Director(d)\wedge
FamousMovie(m)\big{)}\rightarrow\big{(}Actor(a)\wedge
PlayedIn(a,m,d)\big{)}\big{]}.$ (1)

As one may see, despite the fact that this formula satisfies the uniformity
condition, it does _not_ belong to $\mbox{\rm UF}_{1}$, as the subformula
starting with “$\forall m$” has two free variables: $d$ and $a$. However, if
we were able to mix quantifiers within blocks, allowing us to treat “$\forall
d\exists a\forall m$” as a single block, then the one-dimensionality
restriction would not be violated.

Another natural, although more complicated, property, also not directly
expressible in $\mbox{\rm UF}_{1}$, is _“for every Polish team there is a
referee who refereed matches of this team against every Italian team”_ , which
can be translated into FO as follows:

$\displaystyle\forall p$ $\displaystyle\big{[}PolishTeam(p)\rightarrow\exists
r\forall i\exists a\exists n\big{(}Referee(r)\wedge Arena(a)$
$\displaystyle\wedge MatchNumber(n)\wedge[ItalianTeam(i)\rightarrow
PlayedMatch(p,i,r,a,n)]\big{)}\big{]}.$ (2)

Once again, in this formula, if quantifiers could be mixed, we would then have
two blocks: “$\forall p$” and “$\exists r\forall i\exists a\exists n$”. Notice
that the subformula beginning with the second block has only one free
variable, $p$, and hence obeys the restriction of one-dimensionality.

Motivated by the examples above, we introduce an expressive variation of
$\mbox{\rm UF}_{1}$ allowing us to mix both types of quantifiers within
blocks: the _alternating uniform one-dimensional fragment_ , $\mbox{\rm
AUF}_{1}$.

We remark here that the definition of $\mbox{\rm UF}_{1}$/$\mbox{\rm
AUF}_{1}$, even though in general lead to a different formalisms, show some
similarities with the concept of _binding form_ [MP15, BM17]. We, however, do
not study this issue in more detail, noting here only that logics defined via
binding forms have lower computational complexity, fitting into the polynomial
hierarchy.

Unfortunately, we could not determinate whether the whole $\mbox{\rm AUF}_{1}$
has the finite model property, or even if its satisfiability problem is
decidable. However, we successfully managed to accomplish this task for its
two non-trivial subfragments, denoted $\mbox{\rm AUF}_{1}^{-}$ and $\mbox{\rm
AUF}_{1}^{3}$, both without equality. $\mbox{\rm AUF}_{1}^{-}$, called the
_diminished alternating uniform one-dimensional fragment_ , is obtained from
$\mbox{\rm AUF}_{1}$ by restricting the shape of quantifier blocks: each block
either consists solely of universal quantifiers or it ends with the
existential one; this idea is inspired by the definition of the Maslov’s class
$\overline{\text{K}}$ [Mas71]. $\mbox{\rm AUF}_{1}^{3}$ is just the
restriction of $\mbox{\rm AUF}_{1}$ to its three-variable subfragment.

Our main technical result is that both these subfragments, $\mbox{\rm
AUF}_{1}^{-}$ and $\mbox{\rm AUF}_{1}^{3}$, have the exponential model
property, that is, their every satisfiable formula has a model of size bounded
exponentially in its length. This immediately yields the decidability and
NExpTime-completeness of their satisfiability problems.

After we analyse $\mbox{\rm AUF}_{1}^{3}$, we take the occasion and make a
step towards a better understanding of the undecidability of $\mbox{\rm
FO}^{3}$. For this purpose, we introduce a rich, decidable subfragment of
$\mbox{\rm FO}^{3}$, containing $\mbox{\rm AUF}_{1}^{3}$, and hence also
$\mbox{\rm FO}^{2}$ (without equality). Our new fragment, $\mbox{\rm
FO}^{3}_{-}$, is defined, roughly speaking, by limiting (but not forbidding!)
the use of two “dangerous” quantifier patterns: $\forall\exists\forall$ and
$\forall\forall\forall$, identified in the paragraph on the undecidability of
$\mbox{\rm FO}^{3}$. As we restrict ourselves to the case without equality,
the third pattern $\forall\forall\exists$ does not lead directly to
undecidability, and hence we do not consider it as “dangerous”.

$\mbox{\rm FO}^{3}_{-}$, in addition to what is expressible in $\mbox{\rm
AUF}_{1}^{3}$, allows us to specify new properties not being expressible in
other discussed fragments. An example of such a property is “ _every married
couple has a child_ ”, with its natural translation into FO:

$\displaystyle\forall h\forall w\big{[}Married(h,w)\rightarrow\exists
c\big{(}ChildOf(c,h)\wedge ChildOf(c,w)\big{)}\big{]}.$ (3)

We stress that the subformula starting with “$\exists c$” is neither one-
dimensional nor uniform. However, this example is contained in $\mbox{\rm
FO}^{3}_{-}$. Hence, indeed, $\mbox{\rm FO}^{3}_{-}$ is more expressive than
$\mbox{\rm FO}^{2}$, even over signatures built out only of unary and binary
relation symbols, as demonstrated by the above formula (we remark that over
such signatures $\mbox{\rm AUF}_{1}^{3}$ syntactically collapses to $\mbox{\rm
FO}^{2}$). Therefore, we believe that $\mbox{\rm FO}^{3}_{-}$ can serve as a
foundational framework for an interesting specification language, distinct
from other proposals, giving a lot of freedom for speaking about relations of
arity at most three.

Organization of the paper. The organization of this paper is as follows.

In Section 2, we introduce our notation and terminology, define the relevant
fragments of first-order logic, and present a normal form for $\mbox{\rm
AUF}_{1}$.

In Section 3, we establish that $\mbox{\rm AUF}_{1}^{-}$ possesses the
exponential model property. We provide two proofs of the existence of
exponential size models of satisfiable $\mbox{\rm AUF}_{1}^{-}$-sentences: the
first one is constructive and involves a use of Hall’s marriage theorem, the
second one goes via the probabilistic method.

In Section 4, we show that $\mbox{\rm AUF}_{1}^{3}$ has the exponential model
property. We first solve its subclass in which we focus mainly on the
quantifier prefix $\forall\exists\forall$, and then extend the construction to
capture full $\mbox{\rm AUF}_{1}^{3}$.

In Section 5, we study the decidable extension $\mbox{\rm FO}^{3}_{-}$ of
$\mbox{\rm AUF}_{1}^{3}$. This section has two independent parts. In
Subsection 5.1, we establish the complexity of $\mbox{\rm FO}^{3}_{-}$ by
showing that for a given satisfiable $\mbox{\rm FO}^{3}_{-}$-sentence there is
an exponentially bounded structure which can be unravelled into an infinite
model and thus may serve as a _witness for satisfiability_. In Subsection 5.2,
we combine classical style constructions from Section 4 with the probabilistic
method to obtain the finite, exponential model property for $\mbox{\rm
FO}^{3}_{-}$.

In Section 6, we conclude our work by providing comments on the equality and
by discussing possible directions for further research on uniform one-
dimensional fragments.

With such an organization, certain sections of this paper may appear
redundant. Indeed, in Section 3, we provide two different proofs of the
exponential model property for $\mbox{\rm AUF}_{1}^{-}$. Further, overlap is
also present in the part of our paper concerning three-variable logic, as the
complexity results of $\mbox{\rm FO}^{3}_{-}$ from Subsection 5.1 are also
implied by the probabilistic proof of the exponential model property from
Subsection 5.2. Finally, since $\mbox{\rm FO}^{3}_{-}$ subsumes $\mbox{\rm
AUF}_{1}^{3}$ and both of them have the same NExpTime complexity, results from
Section 5 cover those from Section 4.

However, in our opinion these redundancies are well-justified. In the case of
$\mbox{\rm AUF}_{1}^{3}$, our proofs utilize two distinct views on the
problem. The classical construction highlights the combinatorial structure of
models (solved via Hall’s marriage theorem), while the probabilistic proof
reveals the quantitative results (that is almost every structure coming from
some nice family of structures is a model). For a similar aim of gaining
deeper insight, this time into the reasons for the decidability of $\mbox{\rm
FO}^{3}_{-}$, we decided to retain Subsection 5.1 with an alternative approach
for the complexity. On the contrary, the overlap between $\mbox{\rm
AUF}_{1}^{3}$ and $\mbox{\rm FO}^{3}_{-}$ is mostly to help the reader to
understand our ideas in a simpler setting first (as the proofs of the latter
are rather technically involved). Moreover, this allows us to obtain
modularization of the proof for $\mbox{\rm FO}^{3}_{-}$, as we use some
crucial part from the proof for $\mbox{\rm AUF}_{1}^{3}$ as a black box.

##  2 Preliminaries

###  2.1 Fragments of logic

We assume that the reader is familiar with the syntax of first-order logic.
Throughout the remaining, we work with signatures consisting solely of
relational symbols, thus we exclude function and constant symbols. We also
restrict ourselves to equality-free first-order logic until the final
discussion in Section 6.

We briefly recall that the _satisfiability problem_ for a fragment of first-
order logic asks whether a sentence from it has a model. We say that a
fragment has the _finite model property_ if its every satisfiable sentence has
a finite model. Further, we speak about the _exponential model property_ if
its every satisfiable sentence $\varphi$ has a model bounded by
$2^{p(|\varphi|)}$, with $p(x)$ being a polynomial and $|\varphi|$ is the
length of $\varphi$, measured in any reasonable fashion. On the contrary, the
size of a model is just the size of its domain.

AUF1. Now, we formally introduce the _alternating uniform one-dimensional
fragment_ , $\mbox{\rm AUF}_{1}$, playing a central role in our
investigations. We define an atom as a $V$-_atom_ if its set of variables is
exactly $V$. Then the set of $\mbox{\rm AUF}_{1}$-formulas is defined as the
smallest set such that:

  * (i)

Every atom using at most one variable is in $\mbox{\rm AUF}_{1}$.

  * (ii)

$\mbox{\rm AUF}_{1}$ is closed under Boolean combinations.

  * (iii)

Let $V$ be a set of variables, and $v_{1},\ldots,v_{k}$ be its enumeration. If
$\psi(v_{1},\dots,v_{k})$ is a Boolean combination of $V$-atoms and $\mbox{\rm
AUF}_{1}$-formulas with free variables in $V$, then
$\mbox{Q}_{1}v_{1},\ldots,\mbox{Q}_{k}v_{k}\psi(v_{1},\dots,v_{k})$ and
$\mbox{Q}_{2}v_{2},\ldots,\mbox{Q}_{k}v_{k}\psi(v_{1},\dots,v_{k})$, where the
$\mbox{Q}_{i}$’s are quantifiers, both belong to $\mbox{\rm AUF}_{1}$.

For a clearer understanding of point (iii) in the above definition, consider
the following example (here we focus only on syntactic issues; this formula is
not very meaningful):

$\displaystyle\exists x\forall y\exists z$
$\displaystyle\big{[}T(x,y,x,y,z)\vee P(x)\vee S(x,x)\vee\forall x\exists
z\big{(}\neg R(x,y,z)\big{)}$ $\displaystyle\vee\forall x\forall y\big{(}\neg
S(y,x)\wedge P(x)\big{)}\vee\exists x\exists z\big{(}R(z,y,x)\big{)}\big{]}.$
(4)

In this example: $P(x)$ and $S(x,x)$ are $\\{x\\}$-atoms, which are by point
(i) also $\mbox{\rm AUF}_{1}$-subformulas, and $T(x,y,x,y,z)$ is an
$\\{x,y,z\\}$-atom. We have also the following $\mbox{\rm
AUF}_{1}$-subformulas with quantifiers: $\forall x\exists z\big{(}\neg
R(x,y,z)\big{)}$ and $\exists x\exists z\big{(}R(z,y,x)\big{)}$, which both
leave one variable free, $y$; and $\forall x\forall y\big{(}S(y,x)\wedge
P(x)\big{)}$, which is a closed subformula. We obtain the whole formula by
applying rule (iii), with the quantifier sequence
$\mbox{Q}_{1},\mbox{Q}_{2},\mbox{Q}_{3}$ being “$\exists\forall\exists$”, to
the disjunction of the mentioned $\mbox{\rm AUF}_{1}$-subformulas and a
$\\{x,y,z\\}$-atom $T(x,y,x,y,z)$. Notice that the atom $T(x,y,x,y,z)$ cannot
be replaced in this example by, say, an atom $T(x,y,x,y,x)$, as it does not
use precisely all the variables $\\{x,y,z\\}$. The reader can find two other
examples of $\mbox{\rm AUF}_{1}$-formulas in Introduction: (1) and (1).

After becoming acquainted with the definition of $\mbox{\rm AUF}_{1}$, we
proceed to discuss its relevant subfragments. First, we remark that $\mbox{\rm
AUF}_{1}$ is defined, mostly for the clarity of presentation, _not_ as an
extension of $\mbox{\rm UF}_{1}$ originally defined in [HK14], but rather as
an extension of the _strongly_ uniform one-dimensional fragment, $\mbox{\rm
sUF}_{1}$, introduced in [KK15] and being a subfragment of $\mbox{\rm
UF}_{1}$. Formally, $\mbox{\rm sUF}_{1}$ is obtained by modifying point (iii)
of the definition of $\mbox{\rm AUF}_{1}$: we are obligated to use the
quantifiers of the same type for the $\mbox{Q}_{i}$’s. Here is an example of a
formula in $\mbox{\rm sUF}_{1}$ (again, only syntax matters):

$\displaystyle\forall x\forall y\forall z\big{[}P(x)\vee R(y,y,y)\vee
R(z,y,x)\vee\exists y\exists z\big{(}\neg R(y,z,x)\wedge\neg R(x,y,z)\wedge
P(y)\big{)}\big{]}.$ (5)

In this case, we have two blocks: universal one, “$\forall x\forall y\forall
z$”, and existential one, “$\exists y\exists z$”.

For interested readers, we explain the original _uniform one-dimensional
fragment_ , $\mbox{\rm UF}_{1}$: it is defined similarly to $\mbox{\rm
sUF}_{1}$ — every block must use the same type of quantifiers, but, in point
(iii) of the definition, the non-unary atoms do _not_ have to use the whole
set $\\{v_{1},\ldots,v_{k}\\}$ of variables, but rather all those atoms use
the same subset of this set, e.g., in (5), we can replace $R(y,z,x)$ and
$R(x,y,z)$ with, say, $R(x,z,z)$ and $R(x,x,z)$, so they both use the same
subset of variables $\\{x,z\\}$ in the subformula beginning with “$\exists
y\exists z$” (see [KK15] for further discussion on variations of $\mbox{\rm
UF}_{1}$). Our approach could perhaps be adapted to capture the full
$\mbox{\rm UF}_{1}$, but the technical details would then become awkward.

Another subfragment, which we consider, is $\mbox{\rm AUF}_{1}^{-}$: it
consists of $\mbox{\rm AUF}_{1}$-formulas in negation normal form which can be
generated if we restrict the point (iii) of the definition of $\mbox{\rm
AUF}_{1}$ to allow us to use only _diminished_ sequences for the
$\mbox{Q}_{i}$’s. We say that a sequence of quantifiers is _diminished_ if it
either is purely universal or ends with the existential quantifier. Notice
that (2.1) is a valid $\mbox{\rm AUF}_{1}^{-}$-formula, as its every maximal
block of quantifiers is diminished: “$\exists\forall\exists$”,
“$\forall\exists$”, “$\exists\exists$” end with the existential quantifier,
and “$\forall\forall$” is a purely universal block. Here is another example of
an $\mbox{\rm AUF}_{1}^{-}$-formula:

$\displaystyle\forall x\forall y\forall z\big{[}R(x,y,z)\vee\exists
tT(x,t)\wedge\exists tT(y,t)\wedge\exists tT(z,t)\big{]}.$ (6)

On the contrary, (1) is _not_ an $\mbox{\rm AUF}_{1}^{-}$-formula, as it
begins with the quantifier block: “$\forall\exists\forall$”.

The last subfragment of our interest is $\mbox{\rm AUF}_{1}^{3}$: the three-
variable subfragment of $\mbox{\rm AUF}_{1}$. The formula (2.1) is, again, a
valid example, this time of an $\mbox{\rm AUF}_{1}^{3}$-formula, as it uses
three-variables: $x,y,z$. Notice, that we can reintroduce variables freely.

FO${}^{\rm{\bf 3}}_{-}$. Finally, we leave the realm of $\mbox{\rm AUF}_{1}$
and reach a broad subfragment of $\mbox{\rm FO}^{3}$: $\mbox{\rm FO}^{3}_{-}$,
containing full $\mbox{\rm FO}^{2}$ (without equality) and reaching into the
area of $\mbox{\rm FO}^{3}$ even further than $\mbox{\rm AUF}_{1}^{3}$. Its
definition may seem very technical, however our motivations become clear in
Section 5, where we introduce its normal form. To avoid some distracting
circumlocutions, we restrict our attention to formulas in negation normal
form. Formally, the set of $\mbox{\rm FO}^{3}_{-}$-formulas is the smallest
set of formulas over variables $x,y,z$ such that:

  * (i)

Every literal using at most one variable is in $\mbox{\rm FO}^{3}_{-}$.

  * (ii)

$\mbox{\rm FO}^{3}_{-}$ is closed under positive Boolean combinations.

  * (iii)

Let $v$ be a variable. If $\psi$ is a positive Boolean combination of
$\mbox{\rm FO}^{3}_{-}$-formulas and literals, then $\exists v\psi$ belongs to
$\mbox{\rm FO}^{3}_{-}$.

  * (iv)

Let $v,v^{\prime}$ be distinct variables. If $\psi$ is a positive Boolean
combination of $\mbox{\rm FO}^{3}_{-}$-formulas with free variables in
$\\{v,v^{\prime}\\}$ and literals using the variables $v$ and $v^{\prime}$,
then $\forall v\psi$ is in $\mbox{\rm FO}^{3}_{-}$.

  * (v)

Let $v,v^{\prime}$ be any variables. If $\psi$ is a positive Boolean
combination of $\mbox{\rm FO}^{3}_{-}$-formulas with at most one free variable
and literals using precisely all of $x,y,z$, then $\exists v\forall
v^{\prime}\psi$ and $\forall v\forall v^{\prime}\psi$ both belong to
$\mbox{\rm FO}^{3}_{-}$.

We remark that in the above definition $v$ and $v^{\prime}$ always represent
variables from the set $\\{x,y,z\\}$. The main restriction on $\mbox{\rm
FO}^{3}$ formulas, which we impose in (v), is limiting the use of quantifier
patterns ending with the universal quantifier and binding subformulas with
three free variables. On the contrary, existential quantification in (iii) and
universal quantification for subformulas with two free variables in (iv) can
be used quite freely.

It is readily verified that the negation normal form of any sentence in
$\mbox{\rm FO}^{2}$, or in $\mbox{\rm AUF}_{1}^{3}$, is indeed in $\mbox{\rm
FO}^{3}_{-}$. For example, to show that $\forall x\forall y\neg R(x,y)$ is in
$\mbox{\rm FO}^{3}_{-}$, we first use rule (iv) (with $v:=y$ and
$v^{\prime}:=x$) to generate $\forall y\neg R(x,y)$, and then again use rule
(iv) (with $v:=x$ and $v^{\prime}:=y$). To show that $\forall x\exists
y\forall zP(x,y,z)$ is in $\mbox{\rm FO}^{3}_{-}$, we first generate $\exists
y\forall zP(x,y,z)$ using rule (v) (with $v:=y$, $v^{\prime}:=z$), and then
use rule (iv) (with $v:=x$ and arbitrary $v^{\prime}$). A more complicated
example of a formula in $\mbox{\rm FO}^{3}_{-}$ is left for the reader to
contemplate:

$\displaystyle\forall x\forall y\big{[}\neg R(x,y)\vee\exists
z\big{(}S(x,z)\wedge S(y,z)\wedge[\neg T(x,z,y)\vee\forall xS(x,z)\vee\exists
x\forall y(T(z,y,x)\wedge P(y))]\big{)}\big{]}.$ (7)

Additionally, two simpler examples are present in Introduction (see (1) and
(3)).

We finish this subsection with a comment on the non-symmetric treatment of
universal and existential quantifiers in $\mbox{\rm AUF}_{1}^{-}$ and
$\mbox{\rm FO}^{3}_{-}$, which causes that these formalisms are not closed
under negation. This is in contrast to, e.g., $\mbox{\rm FO}^{2}$, $\mbox{\rm
UF}_{1}$ and $\mbox{\rm AUF}_{1}$, but similar to some other known decidable
classes of first-order formulas, like the prefix classes or the unary negation
fragment, UNFO, [tCS13].

###  2.2 Notation, outer-structures and outer-types

We refer to structures using Fraktur capital letters, and to their domains
using the corresponding Roman capitals. If ${\mathfrak{A}}$ is a structure and
$B$ is a subset of $A$, then we denote by
${\mathfrak{A}}\\!\\!\restriction\\!\\!B$ the restriction of ${\mathfrak{A}}$
to its subdomain $B$.

We usually use $a,b,\ldots$ to denote elements from the domains of structures,
and $x$, $y$, $\ldots$ for variables, all of these possibly with some
decorations. For a tuple of elements $\overline{x}$, we write
$\psi(\overline{x})$ to denote that all the free variables of $\psi$ are in
$\overline{x}$.

In the context of uniform fragments, it is convenient to speak about some
partially defined (sub)structures which we will call outer-(sub)structures. An
_outer-structure_ over a signature $\sigma$ consists of its domain $A$ and a
function specifying the truth-value of every fact $P(\overline{a})$, for
$P\in\sigma$ and a tuple $\overline{a}$ of elements of $A$ of length equal to
the arity of $P$, such that $\overline{a}$ either contains all the elements of
$A$ or just one of them. The truth values of all the other facts remain
unspecified. Every structure naturally induces an outer-structure. Also, given
a structure ${\mathfrak{A}}$ and its subdomain $B$ we denote by
${\mathfrak{A}}\\!\\!\restriction\\!\\!_{*}B$ the _outer-substructure_ of
${\mathfrak{A}}$ with domain $B$, that is the induced outer-structure of
${\mathfrak{A}}\\!\\!\restriction\\!\\!B$.

An (atomic) $1$-type over a signature $\sigma$ is a $\sigma$-structure over
the domain $\\{1\\}$. A $k$-_outer-type_ is an outer-structure over
$\\{1,\ldots,k\\}$. Let ${\mathfrak{A}}$ be a structure and $a\in A$ an
element of its domain. We denote by ${\rm tp}^{{{\mathfrak{A}}}}({a})$ the
$1$-type _realized_ in ${\mathfrak{A}}$ by $a$, _i.e._ , the $1$-type obtained
from ${\mathfrak{A}}\\!\\!\restriction\\!\\!\\{a\\}$ by renaming the element
$a$ to $1$. Let $a_{1},\ldots,a_{k}\in A$ be pairwise distinct elements. We
denote by ${\rm otp}^{{{\mathfrak{A}}}}({a_{1},\ldots,a_{k}})$ the $k$-outer-
type _realized_ in ${\mathfrak{A}}$ by the tuple $a_{1},\ldots,a_{k}$, _i.e._
, the $k$-outer-type obtained from
${\mathfrak{A}}\\!\\!\restriction\\!\\!_{*}\\{a_{1},\ldots,a_{k}\\}$ by
renaming the element $a_{i}$ to $i$, for $i=1,\ldots,k$. We remark that the
notions of $1$-types and $1$-outer-types coincide.

Note that to fully specify a structure over a signature containing relation
symbols of arity at most $\ell$, it suffices to define its domain $A$, and,
for every subset $B$ of $A$ of size at most $\ell$, the outer-type of some
tuple consisting of all the elements of $B$.

In our proofs, we will need to bound the number of all possible $k$-outer-
types over a given signature, hence we state the following lemma, whose proof
is obvious.

######  Lemma 1.

Let $\sigma$ be a purely relational finite signature containing relational
symbols of arity at most $\ell$ for some fixed $\ell$. Then the number of all
possible $k$-outer-types, for $k\leqslant\ell$, is an exponential function of
$|\sigma|$. This holds in particular for the number of $1$-types.

_The pull operation._ When defining logical structures, we will heavily use
the following _pull operation_. Let ${\mathfrak{C}}$ be a partially defined
structure, and let ${\mathfrak{A}}$ be a fully defined structure. If
$c_{1},\ldots,c_{k}$ is a sequence of pairwise distinct elements of $C$, and
$a_{1},\ldots,a_{k}$ is a sequence of not necessarily pairwise distinct
elements of $A$, then we write
${\mathfrak{C}}\\!\\!\restriction\\!\\!\\{c_{1},\ldots,c_{k}\\}\leftarrow
pull({\mathfrak{A}},c_{1}\leftarrow a_{1},\ldots,c_{k}\leftarrow a_{k})$ to
specify that ${\mathfrak{C}}\\!\\!\restriction\\!\\!\\{c_{1},\ldots,c_{k}\\}$
is copied from
${\mathfrak{A}}\\!\\!\restriction\\!\\!\\{a_{1},\ldots,a_{k}\\}$. Formally,
for every relation symbol $R$ and every sequence of indices
$i_{1},\ldots,i_{\ell}$, where $\ell$ is the arity of $R$, we set
${\mathfrak{C}}\models R(c_{i_{1}},\ldots,c_{i_{\ell}})$ iff
${\mathfrak{A}}\models R(a_{i_{1}},\ldots,a_{i_{\ell}})$.

We also introduce a variant of the pull operation for specifying outer-
substructures. Under the assumptions as stated above, we write
${\mathfrak{C}}\\!\\!\restriction\\!\\!_{*}\\{c_{1},\ldots,c_{k}\\}\leftarrow
pull^{*}({\mathfrak{A}},c_{1}\leftarrow a_{1},\ldots,c_{k}\leftarrow a_{k})$
to mean that only the outer-substructure on $\\{c_{1},\ldots,c_{k}\\}$ is
being defined.

We will always use the pull operation in such contexts that no conflicts with
previously defined parts of ${\mathfrak{C}}$ will arise. In particular, the
$1$-types of the $c_{i}$’s will be always defined before any use of this pull
operation, and further these $1$-types must agree, _i.e._ , for all
$i=1,\dots,k$, ${\rm tp}^{{{\mathfrak{C}}}}({c_{i}})={\rm
tp}^{{{\mathfrak{A}}}}({a_{i}})$. The following fact easily follows from the
definition.

######  Lemma 2.

Let ${\mathfrak{A}}$ and ${\mathfrak{C}}$ be structures, let
$a_{1},\ldots,a_{k}$ be a sequence of elements of $A$, and let
$c_{1},\ldots,c_{k}$ be a sequence of distinct elements of $C$. If the
substructure ${\mathfrak{C}}\\!\\!\restriction\\!\\!\\{c_{1},\ldots,c_{k}\\}$
was defined by
${\mathfrak{C}}\\!\\!\restriction\\!\\!\\{c_{1},\ldots,c_{k}\\}\leftarrow
pull({\mathfrak{A}},c_{1}\leftarrow a_{1},\ldots,c_{k}\leftarrow a_{k})$
(resp.
${\mathfrak{C}}\\!\\!\restriction\\!\\!_{*}\\{c_{1},\ldots,c_{k}\\}\leftarrow
pull^{*}({\mathfrak{A}},c_{1}\leftarrow a_{1},\ldots,c_{k}\leftarrow a_{k})$),
then, for any first-order quantifier-free formula without equality
$\psi(x_{1},\ldots,x_{l})$ (resp. build out of atoms which use all the
variables $x_{1},\ldots,x_{l}$ or just one of them) and any sequence of
indices $i_{1},\ldots,i_{l}$, we have
${\mathfrak{A}}\models\psi(a_{i_{1}},\ldots,a_{i_{l}})\text{ iff
}{\mathfrak{C}}\models\psi(c_{i_{1}},\ldots,c_{i_{l}})$.

###  2.3 Normal form of $\mbox{\rm AUF}_{1}$

We introduce a normal form of $\mbox{\rm AUF}_{1}$-sentences, inspired by
Scott’s normal form for $\mbox{\rm FO}^{2}$ (cf. [Sco62, GKV97]), together
with an efficient procedure for converting an arbitrary $\mbox{\rm
AUF}_{1}$-sentence into equisatisfiable one being in this normal form.

We say that an $\mbox{\rm AUF}_{1}$-formula is _simple_ if its shape is
$\mbox{Q}_{1}v_{1}\ldots\mbox{Q}_{k}v_{k}\psi(v_{1},\ldots,v_{k})$, with the
$\mbox{Q}_{i}$’s being quantifiers, and $\psi$ being a quantifier-free formula
with variables in $\\{v_{1},\dots,v_{k}\\}$. Additionally, we require that all
the $v_{i}$’s are distinct. We remark that we permit here the empty sequence
of quantifiers: a Boolean combination of $0$-ary predicates. Finally, an
$\mbox{\rm AUF}_{1}$-formula is in _normal form_ if it is a conjunction of the
so-defined simple formulas.

Now, we describe our translation procedure. The general idea behind it is to
iteratively replace subformulas with fresh $0$\- and $1$-ary symbols, and then
axiomatize them. More precisely, let $\varphi$ be an $\mbox{\rm
AUF}_{1}$-sentence. We assume that it is in negation normal form, as we can
use standard procedures for this. We apply the following transformation step
in loop, until $\varphi$ reaches its normal form. In each step, select $\psi$
as one of its innermost $\mbox{\rm AUF}_{1}$-subformulas beginning with a
quantifier. There are two cases:

  * •

If $\psi$ has a free variable, _i.e._ , its shape is
$\mbox{Q}_{2}v_{2}\ldots\mbox{Q}_{k}v_{k}\psi_{0}(v_{1},\ldots,v_{k})$, with
$\psi_{0}$ being quantifier-free, add the conjunct, $\mu_{\psi}$, (partially)
axiomatising a fresh unary symbol $P_{\psi}$:

$\displaystyle\forall v_{1}\mbox{Q}_{2}v_{2}\ldots\mbox{Q}_{k}v_{k}\big{[}\neg
P_{\psi}(v_{1})\vee\psi_{0}(v_{1},\ldots,v_{k})\big{]},$ (8)

and replace then $\psi$ by $P_{\psi}(v_{1})$ in $\varphi$; formally $\varphi$
is now $\varphi[P_{\psi}(v_{1})/\psi]\wedge\mu_{\psi}$.

  * •

Otherwise, $\psi$ is a proper subsentence, _i.e._ , its shape is
$\mbox{Q}_{1}v_{1}\ldots\mbox{Q}_{k}v_{k}\psi_{0}(v_{1},\ldots,v_{k})$, with
$\psi_{0}$ being quantifier-free, add the conjunct, $\nu_{\psi}$, (partially)
axiomatising a fresh nullary symbol $E_{\psi}$:

$\displaystyle\mbox{Q}_{1}v_{1}\ldots\mbox{Q}_{k}v_{k}\big{[}\neg
E_{\psi}\vee\psi_{0}(v_{1},\ldots,v_{k})\big{]},$ (9)

and replace then $\psi$ by $E_{\psi}$ in $\varphi$; formally $\varphi$ is now
$\varphi[E_{\psi}/\psi]\wedge\nu_{\psi}$.

It is readily verified that this procedure runs in polynomial time and
produces a normal form $\mbox{\rm AUF}_{1}$-sentence, possibly over a
signature extended by fresh $0$\- and $1$-ary symbols. Moreover, one can
verify that our reduction preserves both $\mbox{\rm AUF}_{1}^{-}$ and
$\mbox{\rm AUF}_{1}^{3}$: if the input formula is in $\mbox{\rm AUF}_{1}^{-}$
($\mbox{\rm AUF}_{1}^{3}$), then output formula remains in $\mbox{\rm
AUF}_{1}^{-}$ ($\mbox{\rm AUF}_{1}^{3}$), respectively. It is slightly less
trivial to demonstrate that our algorithm indeed produces an equisatisfiable
sentence. This is proven in the following lemma.

######  Lemma 3.

Let $\varphi$ be an $\mbox{\rm AUF}_{1}$-sentence, and let $\varphi_{\rm{NF}}$
be its normal form obtain via our algorithm. Then every model of $\varphi$ can
be expanded to a model of $\varphi_{\rm{NF}}$, and every model of
$\varphi_{\rm{NF}}$ is a model of $\varphi$.

######  Proof 2.1.

Let $\varphi_{t}$ be a formula obtained after $t$ steps of our procedure (then
$\varphi_{0}$ is just $\varphi$). It is enough to show the equisatisfiability
of $\varphi_{t}$ and $\varphi_{t+1}$ in each step $t$. As the two cases follow
the same line of reasoning, we focus on the first one, _i.e._ , the selected
subformula $\psi$ of $\varphi_{t}$ has a free variable $v$, and hence
$\varphi_{t+1}$ is $\varphi_{t}[P_{\psi}(v)/\psi]\wedge\mu_{\psi}$.

Suppose that ${\mathfrak{A}}$ is a model of $\varphi_{t}$, then we obtain a
model ${\mathfrak{A}}^{\prime}$ of $\varphi_{t+1}$ by interpreting the fresh
unary symbol $P_{\psi}$ as the set $\\{a\in
A:{\mathfrak{A}}\models\psi[a]\\}$. Hence, obviously,
${\mathfrak{A}}^{\prime}\models\mu_{\psi}$ and also
${\mathfrak{A}}^{\prime}\models\varphi_{t}[P_{\psi}(v_{1})/\psi]$.

In the opposite direction, we assume that ${\mathfrak{A}}^{\prime}$ is a model
of $\varphi_{t+1}$. It may happen that the subformula $\psi(v)$ is true in
more points than $P_{\psi}(v)$, indeed, the added conjunct $\mu_{\psi}$ only
entails $\psi(v)$, but not vice-versa. However, it suffices to guarantee that
${\mathfrak{A}}^{\prime}\models\varphi_{t}$, as $\varphi_{t}$ is in negation
normal form, and thus $\psi$ does not appear in the scope of the negation
symbol.

An artefact of our algorithm is that it may introduce fresh $0$-ary symbols,
which are a relatively uncommon feature in FO. However, in the context of
satisfiability, we can further simplify our normal form formulas by
eliminating these inconvenient symbols: it is enough to nondeterministically
guess the truth values of $0$-ary predicates, replace them by $\top$ or
$\bot$, in accordance with the guess, and then simplify the formulas
accordingly. Hence, we have the following corollary:

######  Corollary 4.

If the subfragment of normal form sentences of $\mbox{\rm AUF}_{1}^{-}$
($\mbox{\rm AUF}_{1}^{3}$) possesses the finite, exponential model property,
then the whole $\mbox{\rm AUF}_{1}^{-}$ ($\mbox{\rm AUF}_{1}^{3}$) also admits
it, respectively. Consequently, the NExpTime upper bound on the complexity of
satisfiability of normal form sentences is also transferred.

##  3 Diminished alternating uniform one-dimensional fragment

In this section we will work on $\mbox{\rm AUF}_{1}^{-}$. We first note that
the decidability of the satisfiability problem for $\mbox{\rm AUF}_{1}^{-}$
follows from the results on Maslov class $\overline{\text{K}}$ (the dual of
the Maslov class K). Sentences of $\overline{\text{K}}$ are often presented in
prenex form. They are then of the following shape

$\displaystyle\exists y_{1}\ldots\exists y_{k}\forall x_{1}\ldots\forall
x_{l}\mbox{Q}_{1}z_{1}\ldots\mbox{Q}_{l}z_{m}\psi,$ (10)

where the $\mbox{Q}_{i}$ are quantifiers, $\psi$ is a quantifier-free formula
without equality and every atom of $\psi$ satisfies one of the following
conditions: (i) it contains at most one $x_{i}$\- or $z_{i}$-variable, (ii) it
contains all the $x_{i}$-variables and no $z_{i}$-variables, or (iii) it
contains an existentially quantified variable $z_{j}$ and no $z_{i}$-variables
with $i>j$.

Decidability of the satisfiability problem for $\overline{\text{K}}$ (or,
actually, the equivalent validity problem for K) was shown by Maslov [Mas71]
by his own inverse method. Later, a few resolution-based proofs were proposed.
A proof by Hustadt and Schmidt [HS99] works also for the class
$\overline{\text{DK}}$ of conjunctions of $\overline{\text{K}}$-sentences.

Now, one easily observes that every $\mbox{\rm AUF}_{1}^{-}$-normal form
conjunct is a prenex $\overline{\text{K}}$-sentence. Indeed, every conjunct
containing only universal quantifiers is of the form (10) with $k=m=0$ and its
every atom satisfies either condition (i) or (ii); every conjunct whose
quantifier prefix ends with the existential quantifier is of the form (10)
with $k=l=0$ and its every atom satisfies (i) or (iii).

Hence any normal form $\mbox{\rm AUF}_{1}^{-}$-sentence belongs to
$\overline{\text{DK}}$ and we can infer:

######  Theorem 5.

The satisfiability problem for $\mbox{\rm AUF}_{1}^{-}$ is decidable.

We recall that the precise complexity of $\overline{\text{DK}}$ and of
$\overline{\text{K}}$ has not yet been established. It seems that a closer
inspection of the resolution procedure from [HS99] could give some elementary
upper bound on the complexity of $\overline{\text{DK}}$-satisfiability
problem. This bound, however, would not be no better than doubly
exponential111Ullrich Hustadt, private communication, 2024.. This would still
leave a gap, as the best lower bound, inherited from $\mbox{\rm FO}^{2}$, is
NExpTime. It is also not known if $\overline{\text{DK}}$ or
$\overline{\text{K}}$ have the finite model property and if their finite
satisfiability problem is decidable.

We now show the following result. Besides just proving the finite model
property for $\mbox{\rm AUF}_{1}^{-}$, it will also allow us to establish the
exact complexity of its satisfiability problem.222In the upcoming work [FKM24]
we will revisit $\overline{\text{K}}$/$\overline{\text{DK}}$ and show that
their satisfiability problems are both NExpTime-complete and that both have
the finite, exponential model property. This will be sufficient to infer
NExpTime-completeness of $\mbox{\rm AUF}_{1}^{-}$, and in fact will cover the
results from this subsection. The case of
$\overline{\text{K}}$/$\overline{\text{DK}}$ is, however, much more involved
than the case of $\mbox{\rm AUF}_{1}^{-}$ and we believe that presenting here
simpler, direct decidability proofs for the latter is valuable.

######  Theorem 6.

$\mbox{\rm AUF}_{1}^{-}$ has the exponential model property, hence its
satisfiability (= finite satisfiability) problem is NExpTime-complete.

In the rest of this section we prove the above theorem. Actually, we propose
two different arguments for the existence of small finite models: the first
one is constructive, the second—probabilistic. In both we look at satisfaction
of $\mbox{\rm AUF}_{1}^{-}$ sentences via the concept of _satisfaction
forests_. We start with the constructive variant, but the reader willing to
see first perhaps a bit simpler probabilistic proof may read Section 3.1 and
then jump directly to Section 3.3.

By Lemma 4 we may restrict attention to normal form sentences without $0$-ary
predicates. For convenience we split the set of the conjuncts of a normal form
sentence $\varphi$ into those whose all quantifiers are universal and those
which end with the existential quantifier:

$\displaystyle\varphi=\bigwedge_{1\leqslant i\leqslant
m_{\scriptscriptstyle\exists}}\varphi^{\scriptscriptstyle\exists}_{i}\wedge\bigwedge_{1\leqslant
i\leqslant
m_{\scriptscriptstyle\forall}}\varphi^{\scriptscriptstyle\forall}_{i},$ (11)

where
$\varphi^{\scriptscriptstyle\exists}_{i}=\mbox{Q}_{1}^{i}x_{1}\mbox{Q}_{2}^{i}x_{2}\ldots\mbox{Q}_{k_{i}{-}1}^{i}x_{k_{i}{-}1}\exists
x_{k_{i}}\psi^{\scriptscriptstyle\exists}_{i},$
$\varphi^{\scriptscriptstyle\forall}_{i}=\forall x_{1}\ldots
x_{l_{i}}\psi^{\scriptscriptstyle\forall}_{i},$ for
$\mbox{Q}_{j}^{i}\in\\{\forall,\exists\\}$,
$\psi^{\scriptscriptstyle\exists}_{i}=\psi^{\scriptscriptstyle\exists}_{i}(x_{1},x_{2},\ldots,x_{k_{i}})$
and
$\psi^{\scriptscriptstyle\forall}_{i}=\psi^{\scriptscriptstyle\forall}_{i}(x_{1},\ldots,x_{l_{i}})$.
By $M$ we denote the maximal number of variables in a conjunct of $\varphi$.

###  3.1 Satisfaction forests

In this subsection we introduce _satisfaction forests_ , which are auxiliary
structures (partially) describing some finite models of normal form $\mbox{\rm
AUF}_{1}^{-}$ sentences. We first explain how to extract a satisfaction forest
from a given model ${\mathfrak{B}}$ of a normal form sentence $\varphi$. Then
we formally define satisfaction forests and relate their existence to the
existence of finite models of normal form sentences.

####  3.1.1 Extracting a satisfaction forest from a model

Let $\varphi$ be a normal form $\mbox{\rm AUF}_{1}^{-}$ sentence and let
${\mathfrak{B}}$ be its model. Assume that $\varphi$ is as in (11). The
satisfaction forest will be a collection of labelled trees, one tree for each
existential conjunct of $\varphi$, showing how this conjunct is satisfied in
${\mathfrak{B}}$. There will be two labelling functions: $\mathcal{L}_{1}$
will assign elements from $B$ to tree nodes (with the exception of the root,
which will be assigned the special empty label) and $\mathcal{L}_{2}$ will
assign outer-substructures of ${\mathfrak{B}}$ to the branches of the trees.
By a _branch_ we mean here a sequence of elements $d_{1},\ldots,d_{k_{i}}$
such that $d_{1}$ is a child of the root, $d_{k_{i}}$ is a leaf, and each
$d_{i+1}$ is a child of $d_{i}$. An initial segment of a branch will be called
a _partial branch_.

It is helpful to think that a satisfaction forest just represents a winning
strategy of the existential player in the standard verification game for
${\mathfrak{B}}$ and $\varphi$.

Consider a single existential conjunct
$\varphi^{\scriptscriptstyle\exists}_{i}=\mbox{Q}_{1}^{i}x_{1}\mbox{Q}_{2}^{i}x_{2}\ldots\mbox{Q}_{k_{i}{-}1}^{i}x_{k_{i}{-}1}\exists
x_{k_{i}}\psi^{\scriptscriptstyle\exists}_{i}$ of $\varphi$. Its satisfaction
tree $\mathcal{T}_{i}$ is built in the following process.

Start with the root and label it by the empty label. The root forms _level_
$0$ of the tree. _Level_ $j$ (or _level_ $x_{j}$), $0<j\leqslant k_{i}$ will
correspond to the quantifier $\mbox{Q}^{i}_{j}$ and hence to the variable
$x_{j}$. Assume level $j-1$ has been constructed, for $0<j\leqslant k_{i}$.
For each of its nodes $d$:

  * •

If $\mbox{Q}^{i}_{j}=\forall$ then for each element $b\in B$ add a child
$d^{\prime}$ of $d$ to $\mathcal{T}_{i}$ and set
$\mathcal{L}_{1}(d^{\prime}):=b$. Nodes added in this step are called
_universal nodes_.

  * •

If $\mbox{Q}^{i}_{j}=\exists$ then let $d_{1},\ldots,d_{j-1}=d$ be the
sequence of non-root nodes on the partial branch ending at $d$, ordered from
the child of the root towards $d$. Choose in ${\mathfrak{B}}$ an element $b$
such that

${\mathfrak{B}}\models\mbox{Q}_{j+1}^{i}x_{j+1}\ldots\mbox{Q}_{k_{i}-1}^{i}x_{k_{i}-1}\exists
x_{k_{i}}\psi^{\scriptscriptstyle\exists}_{i}(\mathcal{L}_{1}(d_{1}),\ldots,\mathcal{L}_{1}(d_{j-1}),b,x_{j+1},\ldots,x_{k_{i}}).$

By the choice of the labels for $d_{1},\ldots,d_{j-1}$ and the fact that
${\mathfrak{B}}\models\varphi^{\scriptscriptstyle\exists}_{i}$, it is clear
that such an element exists. If $j<k_{i}$ then we call $b$ an _intermediate
witness_ for $\varphi^{\scriptscriptstyle\exists}_{i}$, and if $j=k_{i}$ we
call it a _final witness_ for $\varphi^{\scriptscriptstyle\exists}_{i}$. Add a
single child $d^{\prime}$ of $d$ to $\mathcal{T}_{i}$ and set
$\mathcal{L}_{1}(d^{\prime})=b$. This node $d^{\prime}$ is called an
_existential node_.

For a branch $\flat$ of the above-defined tree we denote by $Set(\flat)$ the
set of labels of the non-root elements of $\flat$, by $Set^{-}(\flat)$ the set
of labels of non-root and non-leaf elements of $\flat$ and by $Seq(\flat)$ the
sequence of the labels of the non-root elements of $\flat$, ordered from the
child of the root towards the leaf.

We now define function $\mathcal{L}_{2}$ assigning labels to the branches of
the tree. For a branch $\flat$, we set $\mathcal{L}_{2}(\flat)$ to be the
outer-structure ${\mathfrak{B}}\\!\\!\restriction\\!\\!_{*}Set(\flat)$.

To declare some properties of satisfaction forests we need the following
notions. An outer-structure ${\mathfrak{H}}$ is
$\varphi^{\scriptscriptstyle\forall}_{i}$-_compatible_ , if for every sequence
$a_{1},\ldots,a_{l_{i}}$ of elements of $H$ such that
$\\{a_{1},\ldots,a_{l_{i}}\\}=H$ we have
${\mathfrak{H}}\models\psi^{\scriptscriptstyle\forall}_{i}(a_{1},\ldots,a_{l_{i}})$.
An outer-structure is $\varphi^{\scriptscriptstyle\forall}$-_compatible_ if it
is $\varphi^{\scriptscriptstyle\forall}_{i}$-compatible for every conjunct
$\varphi^{\scriptscriptstyle\forall}_{i}$. Further, a set of $1$-types
$\\{\alpha_{1},\ldots,\alpha_{k}\\}$ is
$\varphi^{\scriptscriptstyle\forall}$-_compatible_ if for any $1\leqslant
m\leqslant M$, any set of distinct elements $H=\\{a_{1},\ldots,a_{m}\\}$ and
any assignment
$f:\\{a_{1},\ldots,a_{m}\\}\rightarrow\\{\alpha_{1},\ldots,\alpha_{k}\\}$ one
can build a $\varphi^{\scriptscriptstyle\forall}$-compatible outer-structure
on $H$ in which, for every $1\leqslant i\leqslant m$, the $1$-type of $a_{i}$
is $f(a_{i})$.

We now collect some properties of the tree $\mathcal{T}_{i}$ and its
labellings for $\varphi^{\scriptscriptstyle\exists}_{i}$ constructed as above.

  1. (T1)

for $1\leqslant j\leqslant k_{i}$, and every node $d$ from level $j-1$:

    1. (a)

if $\mbox{Q}_{j}^{i}=\forall$ then $d$ has precisely $|B|$ children, labelled
by distinct elements of $B$ (recall that each of these children is called a
universal node)

    2. (b)

if $\mbox{Q}_{j}^{i}=\exists$ then $d$ has precisely one child (recall that
this child is called an existential node),

  2. (T2)

for every branch $\flat\in\mathcal{T}_{i}$, if
$Seq(\flat)=(a_{1},\ldots,a_{k_{i}})$, we have
$\mathcal{L}(\flat)\models\psi^{\scriptscriptstyle\exists}_{i}(a_{1},\ldots,a_{k_{i}})$,

  3. (T3)

for every pair of branches $\flat_{1},\flat_{2}\in\mathcal{T}_{i}$, for every
$a\in B$ such that $a\in Set(\flat_{1})$ and $a\in Set(\flat_{2})$ the
$1$-types of $a$ in $\mathcal{L}_{2}(\flat_{1})$ and in
$\mathcal{L}_{2}(\flat_{2})$ are identical,

  4. (T4)

for every pair of branches $\flat_{1},\flat_{2}\in\mathcal{T}_{i}$ such that
$Set(\flat_{1})=Set(\flat_{2})$ we have that
$\mathcal{L}_{2}(\flat_{1})=\mathcal{L}_{2}(\flat_{2})$,

  5. (T5)

for every branch $\flat\in\mathcal{T}_{i}$, $\mathcal{L}_{2}(\flat)$ is
$\varphi^{\scriptscriptstyle\forall}$-compatible.

If $\mathcal{T}_{i}$ meets the above properties it is called a _satisfaction
tree over_ $B$ for $\varphi^{\scriptscriptstyle\exists}_{i}$.

We then collect some properties of the whole sequence of trees
${\mathfrak{T}}=(\mathcal{T}_{1},\ldots,\mathcal{T}_{m_{\scriptscriptstyle\exists}})$
and their labellings constructed for $\varphi$ and ${\mathfrak{B}}$.

  1. (F1)

for every $i$, $\mathcal{T}_{i}$ is a satisfaction tree over $B$ for
$\varphi^{\scriptscriptstyle\exists}_{i}$,

  2. (F2)

for every pair of branches
$\flat_{1}\in\mathcal{T}_{i},\flat_{2}\in\mathcal{T}_{j}$, $i\not=j$, for
every $a\in B$ such that $a\in Set(\flat_{1})$ and $a\in Set(\flat_{2})$ the
$1$-types of $a$ in $\mathcal{L}(\flat_{1})$ and in $\mathcal{L}(\flat_{2})$
are identical,

  3. (F3)

for every pair of branches
$\flat_{1}\in\mathcal{T}_{i},\flat_{2}\in\mathcal{T}_{j}$, $i\not=j$ such that
$Set(\flat_{1})=Set(\flat_{2})$ we have that
$\mathcal{L}_{2}(\flat_{1})=\mathcal{L}_{2}(\flat_{2})$,

  4. (F4)

the set of all $1$-types appearing in the outer-structures defined as labels
of the branches of the trees in ${\mathfrak{T}}$ is
$\varphi^{\scriptscriptstyle\forall}$-compatible.

Properties (T3), (T4), (F2) and (F3) will be sometimes called the _(forest)
consistency conditions_.

The sequence of trees
${\mathfrak{T}}=(\mathcal{T}_{1},\ldots,\mathcal{T}_{m_{\scriptscriptstyle\exists}})$
and the labelling functions $\mathcal{L}_{1},\mathcal{L}_{2}$, constructed as
above for the structure ${\mathfrak{B}}$ and the sentence $\varphi$ satisfies
conditions (T1)-(T5) and (F1)-(F4).

######  Proof 3.1.

It is not difficult to see that each of the $\mathcal{T}_{i}$ satisfies
(T1)-(T5) and that the whole sequence satisfies (F1)-(F3). The only non-
obvious point is (F4). Let us prove that it is true. Let
$\alpha_{1},\ldots,\alpha_{k}$ be the list of all $1$-types appearing in the
outer-structures assigned by $\mathcal{L}_{2}$ to the branches in the whole
forest ${\mathfrak{T}}$. Let $m$ be a natural number,
$H=\\{a_{1},\ldots,a_{m}\\}$ be a set of fresh distinct elements and
$f:\\{a_{1},\ldots,a_{m}\\}\rightarrow\\{\alpha_{1},\ldots,\alpha_{k}\\}$ an
assignment of $1$-types to these elements. We need to construct a
$\varphi^{\scriptscriptstyle\forall}$-compatible outer-structure on $H$ in
which, for every $i$, the $1$-type of $a_{i}$ is $f(a_{i})$. For each $i$
choose an element $g(a_{i})\in B$ such that ${\rm
tp}^{{\mathfrak{B}}}(g(a_{i}))=f(a_{i})$; $g$ need not be injective.

Let us define the outer-structure ${\mathfrak{H}}$ on $H$ by first setting the
$1$-type of each $a_{i}$ to be $f(a_{i})$, and then setting
${\mathfrak{H}}\\!\\!\restriction\\!\\!_{*}\\{a_{1},\ldots,a_{m}\\}\leftarrow\text{pull}^{*}({\mathfrak{B}},g(a_{1}),\ldots,g(a_{m}))$.

We claim that so defined ${\mathfrak{H}}$ is
$\varphi^{\scriptscriptstyle\forall}$-compatible. To see this take any
conjunct $\varphi^{\scriptscriptstyle\forall}_{i}$ and any sequence of
elements $c_{1},\ldots,c_{l_{i}}$ such that $\\{c_{1},\ldots,c_{l_{i}}\\}=H$
and assume to the contrary that
${\mathfrak{H}}\not\models\psi^{\scriptscriptstyle\forall}_{i}(c_{1},\ldots,c_{l_{i}})$.
But then
${\mathfrak{B}}\not\models\psi^{\scriptscriptstyle\forall}_{i}(g(c_{1}),\ldots,g(c_{l_{i}}))$,
as the truth-values of the appropriate atoms appearing in
$\psi^{\scriptscriptstyle\forall}_{i}$ in the two considered structures
coincide by our definition of ${\mathfrak{H}}$. Contradiction.

####  3.1.2 Satisfaction forests and the existence of finite models

Let $\varphi$ be a normal form $\mbox{\rm AUF}_{1}^{-}$ sentence (we do not
assume that a model of $\varphi$ is known). Formally, a _satisfaction forest_
for $\varphi$ _over a domain_ $B$ is a sequence of trees
${\mathfrak{T}}=(\mathcal{T}_{1},\ldots,\mathcal{T}_{m_{\scriptscriptstyle\exists}})$
together with labelling functions $\mathcal{L}_{1}$, $\mathcal{L}_{2}$,
assigning elements of $B$ to the nodes of the $\mathcal{T}_{i}$ (with the
exception of their roots to which the special empty label is assigned) and,
respectively, outer-structures to their branches, such that each of the trees
$\mathcal{T}_{i}$ satisfies conditions (T1)-(T5) and the whole sequence
satisfies conditions (F1)-(F4), with respect to $\mathcal{L}_{1}$,
$\mathcal{L}_{2}$.

######  Lemma 7.

A normal form $\mbox{\rm AUF}_{1}^{-}$ sentence $\varphi$ has a model over a
domain $B$ iff it has a satisfaction forest over $B$.

######  Proof 3.2.

Left-to-right implication is justified by the extraction of a satisfaction
forest from a given finite model of $\varphi$ described in Section 3.1.1, and
in particular by Claim 3.1.1.

In the opposite direction assume that a satisfaction forest over a finite
domain $B$ for $\varphi$ is given. We construct a model ${\mathfrak{B}}$ of
$\varphi$ over the domain $B$. The construction is natural:

_Step 1: $1$-types._ The $1$-type of an element $b\in B$ is defined as the
$1$-type of $b$ in the structure $\mathcal{L}_{2}(\flat)$ for an arbitrarily
chosen branch $\flat$, in an arbitrarily chosen tree $\mathcal{T}_{i}$, for
which $b\in Set(\flat)$.

_Step 2: Witnesses._ For every tree $\mathcal{T}_{i}$ and its every branch
$\flat$ of $\mathcal{T}_{i}$ define the outer-structure on $Set(\flat)$ in
accordance with $\mathcal{L}_{2}(\flat)$.

_Step 3: Completion._ For any set of distinct elements
$\\{b_{1},\ldots,b_{k}\\}$ whose outer-structure is not yet defined, choose
any $\varphi^{\scriptscriptstyle\forall}$-compatible outer-structure which
retains the already defined $1$-types of the $b_{i}$.

Properties (T3), (F2), (T4) and (F3) guarantee that Step 1 and Step 2 can be
performed without conflicts and the existence of an appropriate outer-
structure in Step 3 is guaranteed by (F4).

It remains to see that ${\mathfrak{B}}\models\varphi$. Consider any
existential conjunct of $\varphi$, that is a conjunct
$\varphi^{\scriptscriptstyle\exists}_{i}=\mbox{Q}_{1}^{i}x_{1}\mbox{Q}_{2}^{i}x_{2}\ldots\mbox{Q}_{k_{i}{-}1}^{i}x_{k_{i}{-}1}\exists
x_{k_{i}}\psi^{\scriptscriptstyle\exists}_{i}$. The satisfaction tree
$\mathcal{T}_{i}$ witnesses that $\varphi^{\scriptscriptstyle\exists}_{i}$
indeed holds: it describes all possible substitutions for universally
quantified variables, and shows how intermediate and final witnesses for
existential quantifiers can be chosen. Consider now any universal conjunct
$\varphi^{\scriptscriptstyle\forall}_{i}=\forall x_{1}\ldots
x_{l_{i}}\psi^{\scriptscriptstyle\forall}_{i}$ and let
$b_{1},\ldots,b_{l_{i}}$ be any sequence of elements of $B$ (possibly with
repetitions). Let $H=\\{b_{1},\ldots,b_{l_{i}}\\}$. The outer-structure on $H$
has been defined either in Step 2 or in Step 3. In both cases we know that it
is $\varphi^{\scriptscriptstyle\forall}$-compatible, in particular it is
$\varphi^{\scriptscriptstyle\forall}_{i}$-compatible, so
${\mathfrak{H}}\models\psi_{i}^{\forall}(b_{1},\ldots,b_{l_{i}})$.

###  3.2 From a model to a satisfaction forest over a small finite domain

We are ready to present the main construction of this section in which we show
that every satisfiable $\mbox{\rm AUF}_{1}^{-}$-sentence has a satisfaction
forest over a small finite domain.

Let ${\mathfrak{A}}$ be a (possibly infinite) model of a normal form sentence
$\varphi$ of the shape as in (11). We show how to construct a satisfaction
forest over a domain of size bounded exponentially in $|\varphi|$. By Lemma 7
this will guarantee that $\varphi$ has a finite model over such a bounded
domain.

####  3.2.1 Domain

Let $L$ be the number of $1$-types (over the signature of $\varphi$) realized
in ${\mathfrak{A}}$, and let these types be enumerated as
$\alpha_{0},\ldots,\alpha_{L-1}$. Recall that $M$ is the maximal number of
variables in a conjunct of $\varphi$. We define the domain $B$ to be
$\\{0,\ldots,2M-1\\}\times\\{0,\ldots,m_{\scriptscriptstyle\exists}-1\\}\times\\{0,\ldots,(M-1)^{M-1}-1\\}\times\\{0,\ldots,L-1\\}$.
Note that $M$ and $m_{\scriptscriptstyle\exists}$ are bounded linearly and $L$
is bounded exponentially in $|\varphi|$, and hence $|B|$ is indeed bounded
exponentially in $|\varphi|$.

For convenience let us split $B$ into the sets $B_{i}=\\{(i,*,*,*)\\}$ (here
and in the sequel $*$ will be sometimes used as a wildcard in the tuples
denoting elements of the domain). We will sometimes call $B_{i}$ the $i$-th
_layer_ of $B$.

####  3.2.2 Some simple combinatorics: Extension functions

During the construction of the satisfaction forest we will design a special
strategy for assigning labels to the leaves. To this end we introduce an
auxiliary combinatorial tool, which we will call _extension functions_.

Let us recall a well known Hall’s marriage theorem [Hal35]. A _matching_ in a
bipartite graph $(G_{1},G_{2},E$) is a partial injective function
$f:G_{1}\rightarrow G_{2}$ such that if $f(a)=b$ then $(a,b)\in E$.

######  Theorem 8 (Hall).

Let $(G_{1},G_{2},E)$ be a bipartite graph. There exists a matching covering
$G_{1}$ iff for any set $W\subseteq G_{1}$ the number of vertices of $G_{2}$
incident to the edges emitted from $W$ is greater or equal to $|W|$.

For a natural number $n$, let $[n]$ denote the set $\\{0,\ldots,n-1\\}$ and
for $1\leqslant l\leqslant n$ let $[n]^{l}$ denote the set of all subsets of
$[n]$ of cardinality $l$.

######  Lemma 9.

For every $l,m\in{\mathbb{N}}$ such that $1\leqslant l<m$ there exists a
$1{-}1$ function $ext_{l}:[2m]^{l}\rightarrow[2m]^{l+1}$ such that for any
$S\in[2m]^{l}$ we have that $S\subseteq ext_{l}(S)$.

######  Proof 3.3.

Consider the bipartite graph $([2m]^{l},[2m]^{l+1},E)$ such that
$(S,S^{\prime})\in E$ iff $S\subseteq S^{\prime}$. To show that a desired
$ext_{l}$ exists it suffices to show the existence of a matching covering
entirely the set $[2m]^{l}$. To this end we apply Hall’s marriage theorem. In
our graph every node from $[2m]^{l}$ has degree $2m-l$ (given an $l$-element
subset of $[2m]$ it can be expanded to an $l+1$ subset just by adding to it
precisely one of the remaining $2m-l$ elements) and every node from
$[2m]^{l+1}$ has degree $l+1$ (to obtain an $l$-element subset of a
$l+1$-subset one just removes one of the elements of the latter). Take a
subset $W$ of $[2m]^{l}$. The nodes of this subset are incident to
$|W|\cdot(2m-l)$ edges in total. Let us see that the number of nodes in
$[2m]^{l+1}$ incident to a node from $W$ is greater than or equal to $|W|$.
Indeed, assume to the contrary that it is not. Then at most $|W|-1$ nodes
absorb $|W|\cdot(2m-l)$ edges emitted by $W$, but this means that
$|W|\cdot(2m-l)\leqslant(|W|-1)\cdot(l+1)$. Rearranging this inequality we get
that $|W|(2m-2l-1)+l+1\leqslant 0$. But using the assumption that $0<l<m$ we
have that $(2m-2l-1)>0$ and hence $|W|(2m-2l-1)+l+1$ must be greater than $0$,
too. Contradiction. Thus our graph satisfies the Hall’s theorem assumptions
which guarantee the existence of a matching from $[2m]^{l}$ to $[2m]^{l+1}$,
covering entirely $[2m]^{l}$. This matching can be taken as $ext_{l}$.

For every $1\leqslant l<M$ choose an extension function
$ext_{l}:[2M]^{l}\rightarrow[2M]^{l+1}$ and let
$ext=\bigcup_{l=1}^{M-1}ext_{l}$, that is, $ext$ is a function which takes a
non-empty subset of $[2M]$ of size at most $M-1$ and returns a superset
containing precisely one new element. Obviously $ext$ remains an injective
function.

####  3.2.3 Construction of a satisfaction forest

We now describe how to construct a satisfaction forest
${\mathfrak{T}}=(\mathcal{T}_{1},\ldots,\mathcal{T}_{m_{\scriptscriptstyle\exists}})$
over the domain $B$ with labellings $\mathcal{L}_{1}$, $\mathcal{L}_{2}$ for
$\varphi$. It should be helpful to announce how we are going to take care of
the consistency conditions for the whole forest:

  * •

Conditions (F2) and (T3): With every element $a=(*,*,*,l)\in B$ we associate
the $1$-type $\alpha_{l}$. Whenever $a$ will be used as a label of a node in a
satisfaction tree then its $1$-type in the outer-structure defined for any
branch containing a node labelled with $a$ will be set to $\alpha_{l}$.

  * •

Conditions (F3) and (T4): for a a pair of distinct branches $\flat_{1}$,
$\flat_{2}$ (either belonging to the same tree or to two different trees) we
will simply have $Set(\flat_{1})\not=Set(\flat_{2})$. This condition will be
ensured by an appropriate use of the extension function. Here it is important
that the last quantifier in every
$\varphi^{\scriptscriptstyle\exists}_{i}$-conjunct is existential, and hence
the last node of every branch in $\mathcal{T}_{i}$ is also existential, so we
can freely choose its label from $B$.

Let us explain how to construct a single
$\varphi^{\scriptscriptstyle\exists}_{i}$-satisfaction tree $\mathcal{T}_{i}$
over $B$ and its labellings. The general shape of $\mathcal{T}_{i}$ is
determined by $\varphi^{\scriptscriptstyle\exists}_{i}$ and $B$: we know how
many nodes we need, we know which of them are existential, and which are
universal, we know the labels of the universal nodes. It remains to assign
labels to existential nodes (elements of $B$) and to branches (outer-
structures on the set of elements formed from the labels of the nodes on a
branch).

We define an auxiliary function $\mathfrak{pat}$ which for every node of
$\mathcal{T}_{i}$ returns _a pattern element_ from ${\mathfrak{A}}$. We will
choose $\mathfrak{pat}(d)$, so that its $1$-type is equal to type of
$\mathcal{L}_{1}(d)$. We emphasize that patterns are defined for the nodes of
the tree and not for elements of $B$, in particular it is not harmful if two
nodes belonging to two different branches, but having the same label have the
same pattern element.

Consider a node $d_{k}$ and assume that all its non-root ancestors
$d_{1},\dots,d_{k-1}$ have the function $\mathfrak{pat}$ and their labels
already defined. We proceed as follows:

  * •

If $d_{k}$ is universal then its label $\mathcal{L}_{1}(d_{k})$ is known

    * –

If $\mathcal{L}_{1}(d_{k})=\mathcal{L}_{1}(d_{j})$ for some $j<k$ then we set
$\mathfrak{pat}(d_{k})=\mathfrak{pat}(d_{j})$.

    * –

If the label $\mathcal{L}_{1}(d_{k})$ is not used by the ancestors of $d_{k}$
then choose as $\mathfrak{pat}(d_{k})$ an arbitrary element of
${\mathfrak{A}}$ of the $1$-type assigned to $\mathcal{L}_{1}(d_{k})$. (In
particular, we may use an element which was used by one of the ancestors of
$d$)

  * •

If $d_{k}$ is existential then we need to define both $\mathcal{L}_{1}(d_{k})$
and $\mathfrak{pat}(d_{k})$. By our construction we have that

$\displaystyle{\mathfrak{A}}\models\exists
x_{k}\mbox{Q}_{k+1}^{i}x_{k+1}\ldots\mbox{Q}_{k_{i}-1}^{i}x_{k_{i}-1}\exists
x_{k_{i}}\psi^{\scriptscriptstyle\exists}_{i}(\mathfrak{pat}(d_{1}),\ldots,\mathfrak{pat}(d_{k-1}),x_{k},x_{k+1},\ldots,x_{k_{i}}).$

We choose an element $w\in A$ witnessing the previous formula, i.e., an
element such that

${\mathfrak{A}}\models\mbox{Q}_{k+1}^{i}x_{k+1}\ldots\mbox{Q}_{k_{i}-1}^{i}x_{k_{i}-1}\exists
x_{k_{i}}\psi^{\scriptscriptstyle\exists}_{i}(\mathfrak{pat}(d_{1}),\ldots,\mathfrak{pat}(d_{k-1}),w,x_{k+1},\ldots,x_{k_{i}})$

and set $\mathfrak{pat}(d_{k})=w$. To define the label of $d_{k}$ we consider
two cases:

    * –

If $d_{k}$ is not a leaf then:

      * *

if $\mathfrak{pat}(d_{j})=w$ for some $j<k$ then set
$\mathcal{L}_{1}(d_{k})=\mathcal{L}_{1}(d_{j})$

      * *

otherwise we choose as $\mathcal{L}_{1}(d_{k})$ an arbitrary element of $B$
which has assigned the $1$-type ${\rm tp}^{{\mathfrak{A}}}(w)$, not used by
the ancestors of $d_{k}$ (there are many copies of each $1$-type in $B$ so it
is always possible).

    * –

If $d_{k}$ is a leaf then let $\flat$ be the branch of $d_{k}$ and let
$S=\\{j:\mathcal{L}_{1}(d_{l})\in B_{j}\mbox{ for some }l<k\\}$. Of course,
$|S|<k\leqslant M$ so $ext(S)$ is defined. Let $s$ be the unique member of
$ext(S)\setminus S$. We take as $\mathcal{L}_{1}(d_{k})$ an element
$(s,i,t,l)\in B_{s}$ where $l$ is such that $\alpha_{l}={\rm
tp}^{{\mathfrak{A}}}(w)$, and where $t$ is chosen so that none of the branches
$\flat^{\prime}$ of the current tree for which the labels have been already
defined such that $Set^{-}(\flat^{\prime})=Set^{-}(\flat)$ used $(s,i,t,l)$ as
the label of its leaf. We indeed have enough elements for this, since
obviously $|Set^{-}(\flat)|\leqslant M-1$ and thus there are at most
$(M-1)^{M-1}$ different branches whose nodes from the first $M-1$ levels are
labelled by elements of $|Set^{-}(\flat)|$ (recall that there are
$(M-1)^{M-1}$ possible choices for $t$).

Take now any branch $\flat$ of $\mathcal{T}_{i}$. It remains to define the
outer-structure $\mathcal{L}_{2}(\flat)$. For any relational symbol $R$ of
arity $m$ and any sequence $a_{i_{1}},\ldots,a_{i_{m}}$ of elements of
$Set(\flat)$ containing all the elements of $Set(\flat)$ we set
$R(a_{i_{1}},\ldots,a_{i_{m}})$ to be true iff
$R(\mathfrak{pat}(a_{i_{1}}),\ldots,\mathfrak{pat}(a_{i_{m}}))$ is true in
${\mathfrak{A}}$. For every $a_{j}$ its $1$-type is set to be equal to the
$1$-type of $\mathfrak{pat}(a_{j})$. This completes the definition of the
outer-structure $\mathcal{L}_{2}(\flat)$ on $Set(\flat)$. Note that the
construction ensures that this outer-structure satisfies
$\psi_{i}^{\exists}(Seq(\flat))$.

####  3.2.4 Correctness

Let us now see that the above-defined satisfaction forest indeed satisfies all
the required conditions.

  * •

Conditions (T1), (T2) and (T3) should be clear.

  * •

For (T4) we show that there is no pair of branches $\flat_{1}$, $\flat_{2}$ in
a tree $\mathcal{T}_{i}$ with $Set(\flat_{1})=Set(\flat_{2})$. For a branch
$\flat$ denote $S_{\flat}=\\{j:\mathcal{L}_{1}(d)\in B_{j}\mbox{ for some
}n\in\flat\\}$. Take any pair $\flat_{1}$, $\flat_{2}$ of different branches
from $\mathcal{T}_{i}$. If $S_{\flat_{1}}\not=S_{\flat_{2}}$ then obviously
$Set(\flat_{1})\not=Set(\flat_{2})$. In the opposite case, due to the use of
the function $ext$, the labels of the leaves of $\flat_{1}$ and $\flat_{2}$
belong to the same layer $B_{s}$, and no other labels of nodes from both
branches belong to $B_{s}$. This means that if
$Set^{-}(\flat_{1})\not=Set^{-}(\flat_{2})$ then still
$Set(\flat_{1})\not=Set(\flat_{2})$. On the other hand, if
$Set^{-}(\flat_{1})=Set^{-}(\flat_{2})$ then by our construction the leaves of
$\flat_{1}$ and $\flat_{2}$ are two different elements $b_{1}=(s,i,x,*)$ and
$b_{2}=(s,i,y,*)$ from layer $B_{s}$, and $b_{1}\in Set(\flat_{1})$ but
$b_{1}\not\in Set(\flat 2)$ and thus $Set(\flat_{1})\not=Set(\flat_{2})$.

  * •

To show that (T5) holds assume to the contrary that for some branch $\flat$,
${\mathfrak{H}}=\mathcal{L}_{2}(\flat)$ is not
$\varphi^{\scriptscriptstyle\forall}$-compatible; take $i$ for which it is not
$\varphi^{\scriptscriptstyle\forall}_{i}$-compatible. So, for some sequence
$a_{1},\ldots,a_{l_{1}}$ such that $\\{a_{1},\ldots,a_{l_{1}}\\}=Set(\flat)=H$
we have
${\mathfrak{H}}\not\models\psi^{\scriptscriptstyle\forall}_{i}(a_{1},\ldots,a_{l_{i}})$.
But then the definition of the outer-structure in $\mathcal{L}_{2}(\flat)$
implies that
${\mathfrak{A}}\not\models\psi^{\scriptscriptstyle\forall}_{i}(\mathfrak{pat}(a_{1}),\ldots,\mathfrak{pat}(a_{l_{i}}))$,
that is ${\mathfrak{A}}$ violates $\varphi^{\scriptscriptstyle\forall}_{i}$.
Contradiction.

  * •

Conditions (F1), (F2) should be clear.

  * •

For (F3) we show that there is no pair of branches $\flat_{1}$ in a tree
$\mathcal{T}_{i}$ and $\flat_{2}$ in $\mathcal{T}_{j}$ for $i\not=j$, with
$Set(\flat_{1})=Set(\flat_{2})$. We proceed as in the argument for (T4), in
the last step observing that the leaves $b_{1}$ and $b_{2}$ are different from
each other since $b_{1}=(s,i,*,*)$ and $b_{2}=(s,j,*,*)$ for some $i\not=j$.

  * •

For (F4) we reason precisely as in the reasoning for (F4) in the proof of the
Claim in Section 3.1 (we just replace the structure ${\mathfrak{B}}$ from this
proof with the currently considered structure ${\mathfrak{A}}$).

####  3.2.5 Complexity of satisfiability

To complete the proof of Theorem 6 we need to see that the satisfiability
problem for $\mbox{\rm AUF}_{1}^{-}$ is NExpTime-complete.

The lower bound is inherited from the lower bound for $\mbox{\rm FO}^{2}$
without equality [Lew80].

Let us turn to the upper bound. By Lemma 4 it suffices to show how to decide
satisfiability of a normal form sentence $\varphi$. As we have seen if
$\varphi$ is satisfiable then it has a model with exponentially bounded
domain. We guess some natural description of such a model ${\mathfrak{A}}$. We
note that this description is also of exponential size with respect to
$|\varphi|$: Indeed, we need to describe some number (linearly bounded in
$|\varphi|$) of relations of arity at most $|\varphi|$, and it is
straightforward, taking into consideration the size of the domain, that a
description of a single such relation is at most exponential in $|\varphi|$. A
verification of a single normal form conjunct in the guessed structure can be
done in an exhaustive way, by considering all possible substitutions for the
variables.

Alternatively, instead of guessing a model, one could guess a satisfaction
forest for $\varphi$. Again, a routine inspection reveals that the size of its
description can be bounded exponentially in $|\varphi|$; also the verification
of the properties (T1)-(T5), (F1)-(F4) would not be problematic.

###  3.3 An alternative proof by the probabilistic method

In this subsection we reprove Theorem 6 by a use of the probabilistic method.
In the context of the decision problem for fragments of first-order logic this
method was used first by Gurevich and Shelah to show the finite model property
for the Gödel class without equality [GS83]. Our approach is inspired by this,
though it is more complicated due to the character of our logic. We will also
present an analysis of the size of a minimal model whose existence is
guaranteed by our reasoning.

It will be convenient to employ the following notion. We say that a structure
${\mathfrak{A}}$ _properly satisfies_ a sentence $\varphi$ if the existential
player can win any play of the standard verification game using a strategy
which requires her to always substitute fresh elements (that is elements that
have not yet been used in the play) for the existentially quantified
variables. Similarly a satisfaction forest is _proper_ if for every
existential node its $\mathcal{L}_{1}$-label does not label any of its
ancestors.

It is easy to see that any satisfiable equality-free first-order sentence is
properly satisfied in some model. For example, if
${\mathfrak{A}}\models\varphi$ then $\varphi$ is properly satisfied in the
structure ${\mathfrak{A}}^{\prime}$ defined as the structure over the domain
$A\times{\mathbb{N}}$ such that
${\mathfrak{A}}^{\prime}\\!\\!\restriction\\!\\!\\{(a_{1},i_{1}),\ldots,(a_{k},i_{k})\\}\leftarrow
pull({\mathfrak{A}},(a_{1},i_{1})\leftarrow
a_{1},\ldots,(a_{k},i_{k})\leftarrow a_{k})$, for all $k$, the $a_{j}$ and the
$i_{j}$. Indeed, for any $a\in A$, the elements $(a,0),(a,1),\ldots$ are then
indistinguishable and the existential player has then always many “proper”
choices. Similarly, any satisfiable $\mbox{\rm AUF}_{1}^{-}$ sentence has a
proper satisfaction forest that can be naturally extracted from a proper
model.

####  3.3.1 Compressed satisfaction forest.

Let $\varphi$ be a satisfiable normal form $\mbox{\rm AUF}_{1}^{-}$-sentence
as in (11) and let ${\mathfrak{A}}\models\varphi$ be its arbitrary (possibly
infinite) proper model.

Let
${\mathfrak{T}}=(\mathcal{T}_{1},\ldots,\mathcal{T}_{m_{\scriptscriptstyle\exists}})$
with labelling functions $\mathcal{L}_{1},\mathcal{L}_{2}$ be a proper
satisfaction forest for $\varphi$ over the domain $A$. Recalling that $M$ is
the maximal number of variables in a conjunct of $\varphi$, let
$\mbox{\large\boldmath$\alpha$}=\\{{\rm tp}^{{{\mathfrak{A}}}}({a}):a\in A\\}$
be the set of $1$-types realized in ${\mathfrak{A}}$ and
$\mbox{\large\boldmath$\beta$}=\\{{\rm
otp}^{{{\mathfrak{A}}}}({a_{1},\ldots,a_{k}}):1\leqslant k\leqslant
M,a_{1},\ldots a_{k}\text{ distinct elements of }A\\}$ the set of all relevant
outer-types realized in ${\mathfrak{A}}$.

We first rebuild ${\mathfrak{T}}$ into a _compressed_ satisfaction forest
${\mathfrak{T}}^{*}=(\mathcal{T}_{1}^{*},\ldots,\mathcal{T}^{*}_{m_{\scriptscriptstyle\exists}})$,
with labellings $\mathcal{L}^{*}_{1},\mathcal{L}^{*}_{2}$ in which the
labelling function for nodes returns elements of
$\mbox{\large\boldmath$\alpha$}\cup{\rm Vars}$ rather than elements of $A$ and
the labelling function for branches returns outer-types rather then outer-
structures on subsets of the domain of $A$. The intuition is as follows. If
the $\mathcal{L}_{1}^{*}$-label of a node $d$ from a level $x$ is an
$\alpha\in\mbox{\large\boldmath$\alpha$}$ then $d$ represents the assignment
(during a play of the verification game) of any element of $1$-type $\alpha$
for $x$, while if it is an $y\in{\rm Vars}$ then $d$ represents assigning for
$x$ the element which is already assigned for $y$.

In the first step, we define the new labelling of nodes,
$\mathcal{L}_{1}^{*}$. For every $\mathcal{T}_{i}$ and its every node $d$:

  * •

if there is an ancestor of $d$ with the same label as $d$, then take such an
ancestor $d^{\prime}$ which is closest to the root; let its level be the level
$x_{i}$; set $\mathcal{L}_{1}^{*}(d)=x_{i}$.

  * •

if there is no such an ancestor then set $\mathcal{L}_{1}^{*}(d)={\rm
tp}^{{\mathfrak{A}}}(\mathcal{L}_{1}(d))$.

Next we cut some nodes of the $\mathcal{T}_{i}$ leaving only its sufficient
“compressed” representation. In the depth-first manner, for every tree
$\mathcal{T}_{i}$ and its every node $d$, if the children of $d$ belong to a
universal level $x_{i}$ then, for every
$\alpha\in\mbox{\large\boldmath$\alpha$}$ mark one of the children
$d^{\prime}$ of $d$ such that ${\rm
tp}^{{\mathfrak{A}}}(\mathcal{L}_{1}(d^{\prime}))=\alpha$, and mark all the
children $d^{\prime}$ of $d$ for which $\mathcal{L}_{1}^{*}(d^{\prime})\in{\rm
Vars}$. After this, remove all the subtrees rooted at unmarked children of
$d$. Denote $\mathcal{T}_{i}^{*}$ the trees so-obtained.

Finally, define the labelling function $\mathcal{L}^{*}_{2}$: for each branch
$\flat$ that survived the above process let $Seq^{*}(\flat)$ denotes the
subsequence of $Seq(\flat)$ in which only the first occurrence of every
element is retained. As $\mathcal{L}_{2}^{*}(\flat)$ we take ${\rm
otp}^{{{\mathfrak{A}}}}({Seq^{*}(\flat)})$.

Let
$\mbox{\large\boldmath$\beta$}_{wit}:=\\{\mathcal{L}_{2}^{*}(\flat):\flat\text{
is a branch of }\mathcal{T}^{*}_{i}\text{ for some }i\\}$, and let
$\mbox{\large\boldmath$\beta$}_{wit}^{+}$ be the closure of
$\mbox{\large\boldmath$\beta$}_{wit}$ under permutations of the domains of
outer-types:
$\mbox{\large\boldmath$\beta$}_{wit}^{+}:=\\{\beta\in\mbox{\large\boldmath$\beta$}:\text{there
is }\beta^{\prime}\in\mbox{\large\boldmath$\beta$}_{wit}\text{ isomorphic to
}\beta\\}$. For every $1\leqslant k\leqslant M$ and every sequence of
$1$-types $\alpha_{1},\ldots,\alpha_{k}$ choose a $k$-outer-type in which the
$1$-type of the element $i$ is $\alpha_{i}$. Let
$\mbox{\large\boldmath$\beta$}_{cmp}$ be the set of the so-chosen outer-types.
Let
$\mbox{\large\boldmath$\beta$}^{*}=\mbox{\large\boldmath$\beta$}_{wit}\cup\mbox{\large\boldmath$\beta$}_{cmp}$.

Note that the degree of nodes of $\mathcal{T}_{i}^{*}$ is bounded by
$|\mbox{\large\boldmath$\alpha$}\cup{\rm Vars}|$ and the number of branches by
$(|\mbox{\large\boldmath$\alpha$}\cup{\rm Vars}|)^{M}$. Hence the number of
outer-types in $|\mbox{\large\boldmath$\beta$}^{*}|$ is not greater than
$M!\cdot(|\mbox{\large\boldmath$\alpha$}\cup{\rm
Vars}|)^{M}+M|\mbox{\large\boldmath$\alpha$}|^{M}$, which is exponential in
$|\varphi|$.

We say that a (partial) branch $\flat=(d_{1},\ldots,d_{k})$ of
$\mathcal{T}_{i}^{*}$ _corresponds_ to a sequence of elements
$a_{1},\ldots,a_{k}$ of $A$ if for all $i=1,\ldots,k$:

  * •

whenever $a_{i}\not=a_{j}$ for all $j<i$ then $\mathcal{L}_{1}^{*}(d_{i})={\rm
tp}^{{{\mathfrak{A}}}}({a_{i}}),$

  * •

if $a_{i}=a_{j}$ for some $j<i$ then, denoting by $j_{0}$ the smallest such
$j$, $\mathcal{L}_{1}^{*}(d_{i})=x_{j_{0}}.$

Of course, a branch may correspond to many different sequences of elements.

####  3.3.2 Random structures.

Let us enumerate the $1$-types in $\alpha$ as
$\alpha_{0},\ldots,\alpha_{L-1}$. For every $n\in{\mathbb{N}}$ we generate a
random structure ${\mathfrak{A}}_{s}$ in the following steps:

_Stage 0: The Domain._ Set $A_{n}=\\{0,\ldots,L-1\\}\times\\{1,\ldots,n\\}$.

_Stage 1: The $1$-types_. For every $(i,j)$ set ${\rm
tp}^{{{\mathfrak{A}}_{n}}}({(i,j)}):=\alpha_{i}$.

_Stage 2: The $k$-outer-types for $2\leqslant k\leqslant M$_. For every subset
of $A$ of size at most $M$ take an arbitrary enumeration of its elements
$a_{1},\ldots,a_{k}$ and let $\alpha_{1},\ldots,\alpha_{k}$ be the sequence of
their $1$-types in ${\mathfrak{A}}$. Let $\mbox{\large\boldmath$\beta$}_{0}$
be the set of $k$-outer-types $\beta$ from $\mbox{\large\boldmath$\beta$}^{*}$
for which $\beta\\!\\!\restriction\\!\\!i=\alpha_{i}$, for $i=1,\ldots,k$.
$\mbox{\large\boldmath$\beta$}_{0}$ is not empty by the construction of
$\mbox{\large\boldmath$\beta$}_{cmp}$. Choose ${\rm
otp}^{{{\mathfrak{A}}_{n}}}({a_{1},\ldots,a_{k}})$ randomly from
$\mbox{\large\boldmath$\beta$}_{0}$, with uniform probability.

_Stage 3: The $k$-outer-types for $k>M$_. For every subset of $A$ of size
bigger than $M$ take an enumeration $a_{1},\ldots,a_{k}$ of its elements and
set ${\rm otp}^{{{\mathfrak{A}}_{n}}}({a_{1},\ldots,a_{k}})$ arbitrarily, e.g.
by setting all the non-unary facts to be false.

####  3.3.3 Probability estimation

Let us now estimate the probability ${\rm
Prob}[{\mathfrak{A}}_{n}\not\models\varphi]$. As all the outer-types in
$\mbox{\large\boldmath$\beta$}^{*}$ are taken from a model of $\varphi$ they
are all $\varphi^{\scriptscriptstyle\forall}$-compatible, so we have that
${\mathfrak{A}}_{n}\models\varphi^{\scriptscriptstyle\forall}$. Hence:

${\rm Prob}[{\mathfrak{A}}_{n}\not\models\varphi]={\rm
Prob}[\bigcup_{i=1}^{m_{\scriptscriptstyle\exists}}{\mathfrak{A}}_{n}\not\models\varphi^{\scriptscriptstyle\exists}_{i}]\leqslant\sum_{i=1}^{m_{\scriptscriptstyle\exists}}{\rm
Prob}[{\mathfrak{A}}_{n}\not\models\varphi^{\scriptscriptstyle\exists}_{i}]$

Consider a single conjunct
$\varphi^{\scriptscriptstyle\exists}_{i}=\mbox{Q}_{1}^{i}x_{1}\mbox{Q}_{2}^{i}x_{2}\ldots\mbox{Q}_{k_{i}{-}1}^{i}x_{k_{i}{-}1}\exists
x_{k_{i}}\psi^{\scriptscriptstyle\exists}_{i}$. Let $l$ be the number of
universal quantifiers in $\varphi^{\scriptscriptstyle\exists}_{i}$. We
estimate ${\rm
Prob}[{\mathfrak{A}}\not\models\varphi^{\scriptscriptstyle\exists}_{i}]$ by
the probability that this formula is satisfied under a fixed strategy of
choosing intermediate witnesses, compatible with the strategy recorded in
$\mathcal{T}^{*}_{i}$:

${\rm
Prob}[{\mathfrak{A}}_{n}\not\models\varphi^{\scriptscriptstyle\exists}_{i}]\leqslant{\rm
Prob}[\bigcup_{\overline{a}\in A_{n}^{l}}{\mathfrak{A}}_{n}\not\models\exists
x_{k_{i}}\psi^{\scriptscriptstyle\exists}_{i}(f(\overline{a}),x_{k_{i}})]$

where $\overline{b}=f(\overline{a})$ is the tuple of length $k_{i}-1$ and is
obtained as follows: if the $j$-th universal quantifier is on position $m$
then $a_{j}$ is put on the $m$-th position of $\overline{b}$. For example if
$\varphi^{\scriptscriptstyle\exists}_{i}=\forall x_{1}\forall x_{2}\exists
x_{3}\forall x_{4}\exists x_{5}\exists
x_{6}\psi^{\scriptscriptstyle\exists}_{i}$ then for a tuple
$(a_{1},a_{2},a_{3})$ we get $\overline{b}=(a_{1},a_{2},b_{3},a_{3},b_{5})$,
for some $b_{3},b_{5}$ which will be specified in a moment. To fill in the
positions corresponding to the existential quantifiers we proceed from left to
write. To find $b_{j}$ we look at the already defined sequence
$b_{1},\ldots,b_{j-1}$. Let $\flat$ be the partial branch of
$\mathcal{T}^{*}_{i}$ corresponding to this sequence. Let $d$ be the next
element on this branch (it is unique, as it belongs to an existential level)
and let $\alpha_{u}=\mathcal{L}^{*}_{1}(d)$. As $b_{j}$ we take the element
$(u,t)$, where $t$ is the smallest index such that
$(u,t)\not\in\\{b_{1},\ldots,b_{j-1}\\}$.

Of course

${\rm Prob}[\bigcup_{\overline{a}\in
A_{n}^{l}}{\mathfrak{A}}_{n}\not\models\exists
x_{k_{i}}\psi^{\scriptscriptstyle\exists}_{i}(f(\overline{a}),x_{k_{i}})]\leqslant\sum_{\overline{a}\in
A_{n}^{l}}{\rm Prob}[{\mathfrak{A}}_{n}\not\models\exists
x_{k_{i}}\psi^{\scriptscriptstyle\exists}_{i}(f(\overline{a}),x_{k_{i}})]$

We need to estimate ${\rm Prob}[{\mathfrak{A}}_{n}\not\models\exists
x_{k_{i}}\psi^{\scriptscriptstyle\exists}_{i}(f(\overline{a}),x_{k_{i}})]$.
Let us consider the partial branch of $\mathcal{T}^{*}_{i}$ corresponding to
$f(\overline{a})$. Let $d$ be the element in the last existential level
completing this branch, and denote the whole branch by $\flat$. Let
$\alpha_{u}=\mathcal{L}_{1}^{*}(d)$. There are at least $n-k_{i}+1$ elements
of $1$-type $\alpha_{u}$ is ${\mathfrak{A}}_{n}$ that do not appear in
$f(\overline{a})$. Consider a single such element $b$. In the process of
defining the outer-types in ${\mathfrak{A}}_{n}$ the outer-type of some tuple
being a permutation of $(f(\overline{a}),b)$ was chosen randomly from
$\mbox{\large\boldmath$\beta$}^{*}$. One possible candidate for this outer-
type was the corresponding permutation of the outer-type
$\mathcal{L}_{2}^{*}(\flat)$. If it was this particular outer-type that was
chosen then
${\mathfrak{A}}_{n}\models\psi^{\scriptscriptstyle\exists}_{i}(f(\overline{a}),b)$.
The chance for this was at least $1/|\mbox{\large\boldmath$\beta$}^{*}|$.
Hence

${\rm
Prob}[{\mathfrak{A}}_{n}\not\models\psi^{\scriptscriptstyle\exists}_{i}(f(\overline{a}),b)]\leqslant
1-1/|\mbox{\large\boldmath$\beta$}^{*}|.$

For distinct candidate final witnesses $b_{j}$ as above the events
$[{\mathfrak{A}}_{n}\not\models\psi^{\scriptscriptstyle\exists}_{i}(f(\overline{a}),b_{j})]$
are independent (note that this is the place in our reasoning where we use the
assumption that the considered quantifier prefix ends with the existential
quantifier), which implies:

${\rm Prob}[{\mathfrak{A}}_{n}\not\models\exists
x_{k_{i}}\psi^{\scriptscriptstyle\exists}_{i}(f(\overline{a}),x_{k_{i}})]\leqslant(1-1/|\mbox{\large\boldmath$\beta$}^{*}|)^{n-k_{i}+1}.$

Then, noting that the number of tuples $\overline{a}\in A_{n}^{l}$ is
$(nL)^{l}$:

${\rm
Prob}[{\mathfrak{A}}_{n}\not\models\varphi^{\scriptscriptstyle\exists}_{i})]\leqslant(nL)^{l}\cdot(1-1/|\mbox{\large\boldmath$\beta$}^{*}|)^{n-k_{i}+1}$

and finally

${\rm Prob}[{\mathfrak{A}}_{n}\not\models\varphi]\leqslant
m_{\scriptscriptstyle\exists}\cdot(nL)^{M}\cdot(1-1/|\mbox{\large\boldmath$\beta$}^{*}|)^{n-M+1}.$

As the parameters $m_{\scriptscriptstyle\exists}$, $L$, $M$ and
$|\mbox{\large\boldmath$\beta$}^{*}|$ are independent from $n$ the limit of
the above estimation as $n\rightarrow\infty$ is $0$. So, for sufficiently
large $n$ it is smaller than $1$ that is for some $n$ ${\rm
Prob}[{\mathfrak{A}}_{n}\models\varphi]>0$. This means that there is a finite
model of $\varphi$.

####  3.3.4 Size of models.

We can estimate the size of models obtained as above via the probabilistic
method by further analysing the last estimation on ${\rm
Prob}[{\mathfrak{A}}_{n}\not\models\varphi]$. More precisely, we need to find
a bound on $n$ (as a function of $|\varphi|$) for which ${\rm
Prob}[{\mathfrak{A}}_{n}\not\models\varphi]<1$, and hence conclude the
existence of model ${\mathfrak{A}}_{n}$ of size $nL$ (as the domain of
${\mathfrak{A}}_{n}$ is $\\{1,\dots,L\\}\times\\{1,\dots,n\\}$). The following
claim establishes such a bound.

There exists an exponential function $f(x)$ such that ${\rm
Prob}[{\mathfrak{A}}_{n}\not\models\varphi]<1$ for all $n\geqslant
f(|\varphi|)$.

######  Proof 3.4.

First, recall that we already established that
$|\mbox{\large\boldmath$\beta$}^{*}|$ is at most exponential in $|\varphi|$,
hence there exists a polynomial $p(x)$ such that
$|\mbox{\large\boldmath$\beta$}^{*}|<2^{p(|\varphi|)}$. Similarly, by Lemma 1
the number of 1-types $L$ can be bounded by $2^{q(|\varphi|)}$ for some
polynomial $q(x)$. We may assume that $p(x)$ and $q(x)$ are monotonic and at
least $10x$. Finally, observe that $m_{\scriptscriptstyle\exists}$ and $M$ are
at most $|\varphi|$.

Hence, we can rewrite the right side of (3.3.3) in terms of
$p(|\varphi|),q(|\varphi|)$ and $|\varphi|$:

$m_{\scriptscriptstyle\exists}\cdot(nL)^{M}\cdot(1-1/|\mbox{\large\boldmath$\beta$}^{*}|)^{n-M+1}\leqslant|\varphi|\cdot(n2^{q(|\varphi|)})^{|\varphi|}\cdot(1-1/2^{p(|\varphi|)})^{n-|\varphi|+1}.$

Now, we choose a function $f(x)$ such that for all $n\geqslant f(|\varphi|)$
the right side of the inequality above is strictly less than $1$. Let
$f(x)=20\cdot 2^{2\cdot p(x)}\cdot q(x)\cdot\ln(2)\cdot x^{2}$, which is
clearly an exponential function. Hence, to conclude we need to show that

$x\cdot(f(x)\cdot 2^{q(x)})^{x}\cdot(1-1/2^{p(x)})^{f(x)-x+1}<1.$

We use the well-known inequality $1-y\leqslant e^{-y}$ to obtain that

$x\cdot(f(x)\cdot 2^{q(x)})^{x}\cdot(1-1/2^{p(x)})^{f(x)-x+1}\leqslant
x\cdot(f(x)\cdot 2^{q(x)})^{x}\cdot\exp(-(f(x)-x+1)/2^{p(x)})<1.$

Then we apply natural logarithm to simplify:

$\ln(x)+x\cdot\ln f(x)+x\cdot q(x)\cdot\ln(2)-(f(x)-x+1)/2^{p(x)}<0$

and further we rearrange the terms:

$2^{p(x)}\cdot\ln(x)+2^{p(x)}\cdot x\cdot\ln f(x)+2^{p(x)}\cdot x\cdot
q(x)\cdot\ln(2)+x{-}1<f(x).$

We can see that each of $2^{p(x)}\cdot\ln(x)$, $2^{p(x)}\cdot x\cdot
q(x)\cdot\ln(2)$ and $x{-}1$ is loosely less than $f(x)/5$. Thus, it is left
to show that $2^{p(x)}\cdot x\cdot\ln f(x)$ is also less than $f(x)/5$.
However this is not difficult to see either, as $2^{p(x)}\cdot x<\sqrt{f(x)}$
by the definition of $f(x)$ and also $\ln y<\sqrt{y}/5$ for all $y\geqslant
1280$. Therefore, as $f(x)$ is monotonic and already $f(1)\geqslant 1280$, we
have that

$2^{p(x)}\cdot x\cdot\ln f(x)<\sqrt{f(x)}\cdot\sqrt{f(x)}/5=f(x)/5,$

which finishes the proof.

##  4 The three-variable alternating uniform one-dimensional fragment

The aim of this section is to show the following result for $\mbox{\rm
AUF}_{1}^{3}$.

######  Theorem 10.

$\mbox{\rm AUF}_{1}^{3}$ has the exponential model property. Hence the
satisfiability problem (=finite satisfiability problem) for $\mbox{\rm
AUF}_{1}^{3}$ is NExpTime-complete.

Clearly, the upper bound in the second part of this theorem is implied by the
first part: to verify that a given $\mbox{\rm AUF}_{1}^{3}$ sentence is
satisfiable we just guess a description of its appropriately bounded model and
verify it (in a straightforward manner). We recall that the corresponding
lower bound is retained from $\mbox{\rm FO}^{2}$ without equality [Lew80].

Recall that by Lemma 4 we can restrict attention to normal form formulas as in
(8) without $0$-ary predicates. For convenience we eliminate conjuncts whose
quantifier prefix starts with the existential quantifier, like $\exists
x\mbox{Q}y\mbox{Q}z\eta_{i}$, by replacing them by $\forall x\exists
yP(y)\wedge\forall x\mbox{Q}y\mbox{Q}z(P(x)\rightarrow\eta_{i})$, for a fresh
symbol $P$. We also replace conjuncts $\forall x\psi(x)$ whose quantifier
prefix consists just of a single universal quantifier, by $\forall x\forall
y\psi(x)$.

Hence, a normal form $\mbox{\rm AUF}_{1}^{3}$ sentence we can be written as
$\varphi=\varphi_{1}\wedge\varphi_{2}$ for

$\displaystyle\varphi_{1}=$
$\displaystyle\bigwedge_{i\in\mathcal{I}_{1}}\forall x\forall
y\varphi_{i}(x,y)\wedge\bigwedge_{i\in\mathcal{I}_{2}}\forall x\forall
y\forall z\varphi_{i}(x,y,z)\wedge\bigwedge_{i\in\mathcal{I}_{3}}\forall
x\exists y\forall z\varphi_{i}(x,y,z),\text{ and}$ $\displaystyle\varphi_{2}=$
$\displaystyle\bigwedge_{i\in\mathcal{I}_{4}}\forall x\exists
y\varphi_{i}(x,y)\wedge\bigwedge_{i\in\mathcal{I}_{5}}\forall x\forall
y\exists z\varphi_{i}(x,y,z)\wedge\bigwedge_{i\in\mathcal{I}_{6}}\forall
x\exists y\exists z\varphi_{i}(x,y,z),$

where the $\mathcal{I}_{i}$ are pairwise disjoint sets of indices, and all the
$\varphi_{i}$ are uniform Boolean combinations of atoms over the appropriate
sets of variables ($\\{x,y,z\\}$ or $\\{x,y\\}$), that is of atoms containing
either all of the free variables of $\varphi_{i}$ or just one of them.

Conjuncts indexed by $\mathcal{I}_{i}$, $1\leqslant i\leqslant 6$, will be
sometimes called the $\mathcal{I}_{i}$-conjuncts.

For the rest of this section we fix an $\mbox{\rm AUF}_{1}^{3}$ normal form
sentence $\varphi=\varphi_{1}\wedge\varphi_{2}$ and its model
${\mathfrak{A}}$. We show how to construct a small model of $\varphi$.
Compared to small model constructions for other fragments of first-order
logic, one non-typical problem we need to deal with here is respecting
$\mathcal{I}_{3}$-conjuncts, that is conjuncts starting with the quantifier
pattern $\forall\exists\forall$. To help the reader understand what happens,
we split our construction into two parts. We first build (Subsection 4.1) a
small model ${\mathfrak{B}}\models\varphi_{1}$; here we indeed need to
concentrate mostly on the $\mathcal{I}_{3}$-conjuncts. Then (Subsection 4.2)
we will use ${\mathfrak{B}}$ as a building block in the construction of a
finite, exponentially bounded, model for the whole $\varphi$. By Lemma 4, this
suffices to prove Theorem 10.

###  4.1 Dealing with $\forall\exists\forall$-conjuncts.

Here, we give a construction of a model ${\mathfrak{B}}$ satisfying all the
($\mathcal{I}_{1}\cup\mathcal{I}_{2}\cup\mathcal{I}_{3}$)-conjuncts (i.e.
${\mathfrak{B}}\models\varphi_{1}$). To properly handle the
$\mathcal{I}_{3}$-conjuncts, we pick for every $j\in\mathcal{I}_{3}$ a witness
function $\mathfrak{f}_{j}:A\rightarrow A$ such that for every $a\in A$ we
have ${\mathfrak{A}}\models\forall z\varphi_{j}(a,\mathfrak{f}_{j}(a),z)$. An
element $\mathfrak{f}_{j}(a)$ will be sometimes called a _witness_ for $a$ and
$\varphi_{j}$ (or for $a$ and the appropriate $\mathcal{I}_{3}$-conjunct).
Similar terminology will be also used later for conjuncts from $\varphi_{2}$.
Here and in the rest of this section we will use the convention that when
referring to the indexes of $\mathcal{I}_{3}$-conjuncts, we will use the
letter $j$, while for the other groups of conjuncts (or in situations where it
is not relevant which group of conjuncts is considered) we will usually use
the letter $i$.

Let us introduce the following definition of a _generalized type_ of an
element $a\in A$. Formally, denoting $\alpha$ the set of $1$-types realized in
${\mathfrak{A}}$, a generalized type is the following tuple:

$\tau=(\alpha(\tau),\beta(\tau),j(\tau),s(\tau))\in\mbox{\large\boldmath$\alpha$}\times(\mbox{\large\boldmath$\alpha$}\cup\\{\bot\\})\times(\\{1,\ldots|\mathcal{I}_{3}|\\}\cup\\{\bot\\})\times\mbox{\large\boldmath$\alpha$}^{|\mathcal{I}_{3}|}.$

We say that an element $a\in A$ realizes a generalized type $\tau$ if:

  * •

$\alpha(\tau)$ is the 1-type of $a$;

  * •

if $\beta(\tau)\neq\bot$ then there exists an element $b\in A$ such that
$\beta(\tau)$ is the 1-type of $b$ and $a$ is the witness for $b$ and the
$\mathcal{I}_{3}$-conjunct with index $j(\tau)$, i.e. $f_{j(\tau)}(b)=a$; and
if $\beta(\tau)=\bot$ then we do not impose any requirements, except that
$j(\tau)=\bot$;

  * •

$s(\tau)=(s(\tau)_{1},\ldots,s(\tau)_{|\mathcal{I}_{3}|})$ is the sequence of
1-types of witnesses for $a$ for all the $\mathcal{I}_{3}$-conjuncts, i.e.,
$s(a)_{j}={\rm tp}^{{{\mathfrak{A}}}}({f_{j}(a)})$ for all $1\leqslant
j\leqslant|\mathcal{I}_{3}|$.

Intuitively, if $a$ realizes $\tau$, then $\tau$ captures the information
about the 1-types of $a$ itself and all the witnesses of $a$, from the
perspective of an element $b$ witnessed by $a$ (if such an element $b$
exists). We want to stress that one element might realize potentially _many_
generalized types, since the choices of $\beta(\tau)$ and $j(\tau)$ might not
be unique. The set of generalized types realized by $a$ in ${\mathfrak{A}}$ is
denoted ${\rm gtp}(a)$.

Let ${\rm gtp}({\mathfrak{A}}):=\bigcup_{a\in A}{\rm gtp}(a)$ be the set of
all generalized types realized in ${\mathfrak{A}}$. For each $\tau\in{\rm
gtp}({\mathfrak{A}})$ pick a single representative $\mathfrak{pat}_{\rm
gtp}(\tau)=a_{\tau}$ such that $\tau\in{\rm gtp}(a)$ (we do not require
$\mathfrak{pat}_{\rm gtp}$ to be 1-1).

_Stage 0: The domain._ Let the domain of ${\mathfrak{B}}$ be the set

$B={\rm gtp}({\mathfrak{A}})\times\\{0,1,2,3\\}.$

We will sometimes call the sets $B_{m}=\\{(\tau,m):\tau\in{\rm
gtp}({\mathfrak{A}})\\}$ _layers_. We can naturally lift the function
$\mathfrak{pat}_{\rm gtp}$ to the function $\mathfrak{pat}:B\to A$:
$\mathfrak{pat}((\tau,m))=\mathfrak{pat}_{\rm gtp}(\tau)$.

Before proceeding to the construction, we need one more definition, namely the
definition of _witnessing graph_ which will contain a _declaration_ about who
is a witness for whom for $\mathcal{I}_{3}$-conjuncts in the final structure
${\mathfrak{B}}$. More precisely, a _pre-witnessing graph_ is a directed graph
$\mathcal{G}^{\prime}_{w}=(B,E^{\prime})$ and an edge-labelling function
$\ell:E^{\prime}\rightarrow\\{1,\ldots,|\mathcal{I}_{3}|\\}$ such that
$b_{1}=(\tau_{1},m_{1})$ is connected to $b_{2}=(\tau_{2},m_{2})$ by an arc
$e$ with label $\ell(e)=j(\tau_{2})$ if $m_{1}+1=m_{2}(\text{mod }4)$,
$\beta(\tau_{2})=\alpha(\tau_{1})$, and
$s(\tau_{1})_{j(\tau_{2})}=\alpha(\tau_{2})$. As the reader may notice the
pre-witnessing graph connects only elements which are in consecutive layers
(modulo 4), for every vertex there is at least one outgoing arc in every
colour, and there are no multiple arcs between the same pair of elements.
Finally, we “functionalize” the graph by restricting the arc-set $E^{\prime}$
to contain exactly one outgoing arc in each colour for every vertex. Let this
new arc-set be $E$. Thus, we obtain a _witnessing graph_
$\mathcal{G}_{w}=(B,E)$ and write $b_{1}\leadsto_{j}b_{2}$ if $b_{1}$ is
connected to $b_{2}$ with an arc coloured by $j$.

The construction itself will be given by the following iterative algorithm.
The role of the generalized types and the witnessing graph is to guide the
algorithm in selecting patterns from ${\mathfrak{A}}$ to be pulled into
${\mathfrak{B}}$, avoiding potential conflicts between different conjuncts
(especially) of type $\mathcal{I}_{3}$. For the clarity of the presentation,
all the conditions present in the algorithm need to be taken modulo
permutation of the considered elements in each step, and by
$\mathfrak{f}_{j}^{-1}(a)$ we mean to take any $b\in A$ satisfying
$\mathfrak{f}_{j}(b)=a$. The algorithm: Stage 1: 1-types. We set the $1$-types
of elements $b$ in ${\mathfrak{B}}$, as given by $\alpha(b)$.

Stage 2: 2-outer-types. For all pairs
$\\{b_{1}=(\tau_{1},m_{1}),b_{2}=(\tau_{2},m_{2})\\}$ of elements from $B$,
$b_{1}\not=b_{2}$ do:

  * •

if ${\rm otp}^{{{\mathfrak{B}}}}({b_{1},b_{2}})$ is already defined then
continue.

  * •

if $b_{1}\leadsto_{j}b_{2}$ for some $j$ then set
$({\mathfrak{B}}\\!\\!\restriction\\!\\!\\{b_{1},b_{2}\\})\leftarrow
pull({\mathfrak{A}},b_{1}\leftarrow
a_{\tau_{1}},b_{2}\leftarrow\mathfrak{f}_{j}(a_{\tau_{1}}))$.

  * •

otherwise, set
$({\mathfrak{B}}\\!\\!\restriction\\!\\!\\{b_{1},b_{2}\\})\leftarrow
pull({\mathfrak{A}},b_{1}\leftarrow a_{\tau_{1}},b_{2}\leftarrow
a_{\tau_{2}})$.

Stage 3: 3-outer-types. For all triples
$\\{b_{1}=(\tau_{1},m_{1}),b_{2}=(\tau_{2},m_{2}),b_{3}=(\tau_{3},m_{3})\\}$
of pairwise distinct elements from $B$ do:

  * •

if ${\rm pretp}^{{{\mathfrak{B}}}}({b_{1},b_{2},b_{3}})$ is already defined
then continue.

  * •

if $b_{1}\leadsto_{j}b_{2}$ and $b_{2}\leadsto_{k}b_{3}$, for some $j,k$ then
set

${\mathfrak{B}}\\!\\!\restriction\\!\\!_{*}\\{b_{1},b_{2},b_{3}\\}\leftarrow
pull^{*}({\mathfrak{A}},b_{1}\leftarrow\mathfrak{f}_{j}^{-1}(a_{\tau_{2}}),b_{2}\leftarrow
a_{\tau_{2}},b_{3}\leftarrow\mathfrak{f}_{k}(a_{\tau_{2}})).$

  * •

if $b_{1}\leadsto_{j}b_{2}$ and $b_{1}\leadsto_{k}b_{3}$ for some $j,k$ then
set

${\mathfrak{B}}\\!\\!\restriction\\!\\!_{*}\\{b_{1},b_{2},b_{3}\\}\leftarrow
pull^{*}({\mathfrak{A}},b_{1}\leftarrow
a_{\tau_{1}},b_{2}\leftarrow\mathfrak{f}_{j}(a_{\tau_{1}}),b_{3}\leftarrow\mathfrak{f}_{k}(a_{\tau_{1}})).$

  * •

if $b_{2}\leadsto_{j}b_{1}$ and $b_{3}\leadsto_{k}b_{1}$ then set

${\mathfrak{B}}\\!\\!\restriction\\!\\!_{*}\\{b_{1},b_{2},b_{3}\\}\leftarrow
pull^{*}({\mathfrak{A}},b_{1}\leftarrow
a_{\tau_{1}},b_{2}\leftarrow\mathfrak{f}_{j}^{-1}(a_{\tau_{1}}),b_{3}\leftarrow\mathfrak{f}_{k}^{-1}(a_{\tau_{1}})).$

  * •

if $b_{1}\leadsto_{j}b_{2}$ for some $j$ and $b_{3}$ is connected to neither
$b_{1}$ nor $b_{2}$ in the witnessing graph then set

${\mathfrak{B}}\\!\\!\restriction\\!\\!_{*}\\{b_{1},b_{2},b_{3}\\}\leftarrow
pull^{*}({\mathfrak{A}},b_{1}\leftarrow
a_{\tau_{1}},b_{2}\leftarrow\mathfrak{f}_{j}(a_{\tau_{1}}),b_{3}\leftarrow
a_{\tau_{3}}).$

  * •

otherwise, set
${\mathfrak{B}}\\!\\!\restriction\\!\\!_{*}\\{b_{1},b_{2},b_{3}\\}\leftarrow
pull^{*}({\mathfrak{A}},b_{1}\leftarrow a_{\tau_{1}},b_{2}\leftarrow
a_{\tau_{2}},b_{3}\leftarrow a_{\tau_{3}})$.

${\mathfrak{B}}\models\varphi_{1}$.

######  Proof 4.1.

Most of the proof follows from the same case analysis as in the algorithm
itself. Hence, we give just a sketch and leave some details for the reader.

First notice that in the final structure ${\mathfrak{B}}$ all the
$\mathcal{I}_{1}$\- and $\mathcal{I}_{2}$-conjuncts are satisfied, since we
have defined all the $2$\- and $3$-outer-types in ${\mathfrak{B}}$ by copying
(pulling) them from ${\mathfrak{A}}$. More precisely, let $\forall x\forall
y\forall z\varphi_{i}(x,y,z)$ be one of the $\mathcal{I}_{2}$-conjuncts (for
$\mathcal{I}_{1}$-conjuncts the situation is analogous). Thanks to the
uniformity of our logic, all the atoms in $\varphi_{i}$ either use all the
variables $x,y,z$ or just one of them. Hence, if we evaluate
$\varphi_{i}(a,b,c)$ on any three (not necessary distinct) elements $a,b,c\in
B$, the value of $\varphi_{i}(a,b,c)$ depends only on: the 1-types of $a,b,c$,
and the connections joining all the three elements $a,b,c$ simultaneously.
Since, the 1-types are fixed beforehand, and the connections joining all the
elements $a,b,c$ are pulled as a outer-structure from a valid model
${\mathfrak{A}}$, then ${\mathfrak{B}}\models\varphi_{i}(a,b,c)$ must hold by
Lemma 2. One can also notice, that no conflicts were introduced when copying
different outer-structures. Indeed, in the algorithm we defined outer-
structure on every at most three-element subset of $B$ exactly once, and the
outer-structures cannot speak about any proper subset of elements of its
domain, except the 1-types which where fixed already in _Step 1_.

Let us now explain that the $\mathcal{I}_{3}$-conjuncts are satisfied. Let
$\forall x\exists y\forall z\varphi_{j}(x,y,z)$ be any
$\mathcal{I}_{3}$-conjunct. Fix an element an assume that $b\in B_{m}$. We
need to see that in the next layer, i.e. $B_{(m+1)\text{mod }4}$, there exists
an element that can serve as a witness for $b$. It is equivalent to having an
outgoing edge from $b$ coloured by $j$. Indeed, if there exists such an edge
then the witnessing graph forces us to pick an appropriate pattern from a
model ${\mathfrak{A}}$. Recall that each layer $B_{m}$ consists of pairs
$(\tau,m)$, where $\tau$ ranges over all generalized types realized in
${\mathfrak{A}}$. Therefore, there must be a representative $a$ realizing
$\tau$ in ${\mathfrak{A}}$. Hence, we have an element $\mathfrak{f}_{j}(a)$,
such that ${\mathfrak{A}}\models\forall
z\varphi_{j}(a,\mathfrak{f}_{j}(a),z)$, which itself realizes some other
generalized type $\tau^{\prime}$. Thus, in $B_{(m+1)\text{mod }4}$ we have an
element $b^{\prime}=(\tau^{\prime},(m+1)\text{mod }4)$ satisfying
$b\leadsto_{j}b^{\prime}$. The fact that ${\mathfrak{B}}\models\forall
z\varphi_{j}(b,b^{\prime},z)$ comes from the same line of arguments as in the
previous paragraph.

In the resulting structure ${\mathfrak{B}}$, similarly as for the structure
${\mathfrak{A}}$, we define witness functions $\mathfrak{f}_{j}:B\to B$ for
each $\mathcal{I}_{3}$-conjunct. More precisely, we can set
$\mathfrak{f}_{j}(b)=b^{\prime}$ if $b\leadsto_{j}b^{\prime}$; from the
construction it follows that ${\mathfrak{B}}\models\forall
z\varphi_{j}(b,\mathfrak{f}_{i}(b),z)$. Note that the new functions
$\mathfrak{f}_{j}$ are not necessarily 1-1, but they are without fixpoints and
have disjoint images.

Finally, we give a bound on the size of the produced structure
${\mathfrak{B}}$. The number of generalized types can be trivially bounded by
$t(t+1)(|\mathcal{I}_{3}|+1)t^{|{\mathcal{I}_{3}}|}$, where
$t=|\mbox{\large\boldmath$\alpha$}|$. As mentioned in the Preliminaries (Lemma
1) $t$ can be bounded by a function exponential in $|\varphi|$, and
$|\mathcal{I}_{3}|$ is clearly polynomial in $|\varphi|$. Hence: The domain of
${\mathfrak{B}}$ is bounded exponentially in $|\varphi|$.

###  4.2 Finite model property for $\mbox{\rm AUF}_{1}^{3}$

Now we build a model ${\mathfrak{C}}\models\varphi_{1}\wedge\varphi_{2}$. It
will be composed out of some number of copies of the structure
${\mathfrak{B}}\models\varphi_{1}$ from the previous subsection, carefully
connected to provide witnesses for conjuncts from $\varphi_{2}$.

_Stage 0: The domain._ Denote
$\mathcal{I}=\mathcal{I}_{4}\cup\mathcal{I}_{5}\cup\mathcal{I}_{6}$. Let us
form ${\mathfrak{C}}$ over the following finite domain.

$C=B\times\mathcal{I}\times\\{0,1\\}\times\\{0,\ldots,5\\}.$

For every $i\in\mathcal{I},u=0,1$, and $0\leqslant m\leqslant 5$ make the
substructure
${\mathfrak{C}}\\!\\!\restriction\\!\\!(B\times\\{i\\}\times\\{u\\}\times\\{m\\})$
isomorphic to ${\mathfrak{B}}$, via the natural isomorphism sending each
$(b,i,u,m)$ to $b$. We also naturally transfer the functions
$\mathfrak{f}_{j}$ and $\mathfrak{pat}$ from ${\mathfrak{B}}$ to
${\mathfrak{C}}$, setting
$\mathfrak{f}_{j}((b,i,u,m))=(\mathfrak{f}_{j}(b),i,u,m)$ and
$\mathfrak{pat}((b,i,u,m))=\mathfrak{pat}(b)$, for all $b,i,u,m$. For
convenience we split $C$ into five subsets
$C_{m}=B\times\mathcal{I}\times\\{0,1\\}\times\\{m\\}$, for $m=0,\ldots,5$.

In the next stages we will successively take care of the all types of
conjuncts of $\varphi$. We will provide witnesses for $\mathcal{I}_{4}$-,
$\mathcal{I}_{5}-$, and $\mathcal{I}_{6}$-conjuncts, using a strategy, which
guarantees no conflicts, e.g., if a $3$-outer-type is defined on a tuple
$c_{1},c_{2},c_{3}$ to make $c_{3}$ a witness for $c_{1}$, $c_{2}$ for an
$\mathcal{I}_{5}$-conjunct, then this tuple will not be used any more for a
similar task (e.g., to make $c_{1}$ a witness for $c_{2},c_{3}$). To design
such a strategy we fix an auxiliary $1-1$ function $\mathfrak{chc}$ taking a
subset of $\\{0,\ldots,5\\}$ of size two and extending it by $1$ element from
$\\{0,\ldots,5\\}$. Such a function exists by Lemma 9. Having provided the
witnesses we will carefully complete the structure ensuring that for every
$c\in C$, $\mathfrak{f}_{j}(c)$ remains a witness for $c$ and the
$\mathcal{I}_{3}$-conjunct indexed by $j$.

_Stage 1: Witnesses for $\mathcal{I}_{4}$-conjuncts._ For every $c\in C$ and
every $i\in\mathcal{I}_{4}$ repeat the following. Let $m$ be the index such
that $c\in C_{m}$. Let $a=\mathfrak{pat}(c)$. Let $a^{\prime}\in A$ be such
that ${\mathfrak{A}}\models\varphi_{i}(a,a^{\prime})$. It may happen that
$a^{\prime}=a$. Take as $c^{\prime}$ any element from
$B\times\\{i\\}\times\\{0\\}\times\\{m+1(\text{mod }6)\\}$ with the same
$1$-type as $a^{\prime}$. Set
$({\mathfrak{C}}\\!\\!\restriction\\!\\!\\{c,c^{\prime}\\})\leftarrow
pull({\mathfrak{A}},c\leftarrow a,c^{\prime}\leftarrow a^{\prime})$.

_Stage 2: Witnesses for $\mathcal{I}_{5}$-conjuncts._ For every unordered pair
of elements $c_{1},c_{2}\in C$, $c_{1}\not=c_{2}$ and every
$i\in\mathcal{I}_{5}$ repeat the following. Let $m_{1},m_{2}$ be the indices
such that $c_{1}\in C_{m_{1}}$ and $c_{2}\in C_{m_{2}}$. We choose two pattern
elements $a_{1},a_{2}\in A$ with the same $1$-types as $c_{1}$ and, resp.,
$c_{2}$, and an index $m^{\prime}$ as follows.

  * (a)

If $c_{2}=\mathfrak{f}_{j}(c_{1})$ for some $j$ (in this case $m_{1}=m_{2}$),
then let $a_{1}=\mathfrak{pat}(c_{1})$ and let
$a_{2}=\mathfrak{f}_{j}(a_{1})$; set $m^{\prime}=m_{1}+1(\text{mod }6)$.

  * (b)

If $c_{1}=\mathfrak{f}_{j}(c_{2})$ for some $j$ ($m_{1}=m_{2}$), then let
$a_{2}=\mathfrak{pat}(c_{2})$ and let $a_{1}=\mathfrak{f}_{j}(a_{2})$; set
$m^{\prime}=m_{1}+1(\text{mod }6)$.

  * (c)

If none of the above holds then let $a_{1}=\mathfrak{pat}(c_{1})$,
$a_{2}=\mathfrak{pat}(c_{2})$ (it may happen that $a_{1}=a_{2}$); if
$m_{1}=m_{2}$ then set $m^{\prime}=m_{1}+1(\text{mod }6)$, otherwise set
$m^{\prime}$ to be the only element of
$\mathfrak{chc}(\\{m_{1},m_{2}\\})\setminus\\{m_{1},m_{2}\\}$.

Let $a^{\prime}\in A$ be such that
${\mathfrak{A}}\models\varphi_{i}(a_{1},a_{2},a^{\prime})$ and let
$a^{\prime\prime}$ be such that
${\mathfrak{A}}\models\varphi_{i}(a_{2},a_{1},a^{\prime\prime})$. Take as
$c^{\prime}$ any element from
$B\times\\{i\\}\times\\{0\\}\times\\{m^{\prime}\\}$ with the same $1$-type as
$a^{\prime}$, and as $c^{\prime\prime}$ any element from
$B\times\\{i\\}\times\\{1\\}\times\\{m^{\prime}\\}$ with the same $1$-type as
$a^{\prime\prime}$. Set
${\mathfrak{C}}\\!\\!\restriction\\!\\!_{*}\\{c_{1},c_{2},c^{\prime}\\}\leftarrow
pull^{*}({\mathfrak{A}},c_{1}\leftarrow a_{1},c_{2}\leftarrow
a_{2},c^{\prime}\leftarrow a^{\prime}))$ and set
${\mathfrak{C}}\\!\\!\restriction\\!\\!_{*}\\{c_{2},c_{1},c^{\prime\prime}\\}\leftarrow
pull^{*}({\mathfrak{A}},c_{2}\leftarrow a_{2},c_{1}\leftarrow
a_{1},c^{\prime\prime}\leftarrow a^{\prime\prime})$.

Additionally, for any $c\in C$ and any $i\in\mathcal{I}_{5}$ repeat the
following. Let $m$ be the index such that $c\in C_{m}$. Let
$a=\mathfrak{pat}(c)$. Let $a^{\prime}\in A$ be such that
${\mathfrak{A}}\models\varphi_{i}(a,a,a^{\prime})$. Take as $c^{\prime}$ any
element from $B\times\\{i\\}\times\\{0\\}\times\\{m+1(\text{mod }6)\\}$ with
the same $1$-type as $a^{\prime}$. Set
$({\mathfrak{C}}\\!\\!\restriction\\!\\!\\{c,c^{\prime}\\})\leftarrow
pull({\mathfrak{A}},c\leftarrow a,c^{\prime}\leftarrow a^{\prime})$.

_Stage 3: Witnesses for $\mathcal{I}_{6}$-conjuncts._ For every $c\in C$, and
every $i\in\mathcal{I}_{6}$ repeat the following. Let $m$ be the index such
that $c\in C_{m}$. Let $a=\mathfrak{pat}(c)$. Let
$a^{\prime},a^{\prime\prime}\in A$ be such that
${\mathfrak{A}}\models\varphi_{i}(a,a^{\prime},a^{\prime\prime})$. Take as
$c^{\prime}$ any element in $C_{m}$, in a different copy of ${\mathfrak{B}}$
than $c$, with the same $1$-type as $a^{\prime}$. Take as $c^{\prime\prime}$
any element in $B\times\\{i\\}\times\\{0\\}\times\\{m+1(\text{mod }6)\\}$ with
the same $1$-type as $a^{\prime\prime}$ and set
${\mathfrak{C}}\\!\\!\restriction\\!\\!_{*}\\{c,c^{\prime},c^{\prime\prime}\\}\leftarrow
pull^{*}({\mathfrak{A}},c\leftarrow a,c^{\prime}\leftarrow
a^{\prime},c^{\prime\prime}\leftarrow a^{\prime\prime})$.

_Stage 4: Taking care of the $\mathcal{I}_{3}$-conjuncts in ${\mathfrak{C}}$._
For every $c\in C$, for every $c^{\prime}\in C$ and every
$j\in\mathcal{I}_{3}$ such that the outer-substructure on
$\\{c,\mathfrak{f}_{j}(c),c^{\prime}\\}$ has not yet been defined (note that
the elements $c,\mathfrak{f}_{j}(c),c^{\prime}$ must be pairwise distinct in
this case) find any $a^{\prime}\in A$ with the same $1$-type as $c^{\prime}$,
take $a=\mathfrak{pat}(c)$ and set
${\mathfrak{C}}\\!\\!\restriction\\!\\!_{*}\\{c,\mathfrak{f}_{j}(c),c^{\prime}\\}\leftarrow
pull^{*}({\mathfrak{A}},c\leftarrow
a,\mathfrak{f}_{j}(c)\leftarrow\mathfrak{f}_{j}(a),c^{\prime}\leftarrow
a^{\prime})$.

_Stage 5: Completing ${\mathfrak{C}}$._ For any tuple of pairwise distinct
elements $c_{1},c_{2},c_{3}\in C$ for which the outer-substructure of
${\mathfrak{C}}$ on has not yet been defined set
${\mathfrak{C}}\\!\\!\restriction\\!\\!_{*}\\{c_{1},c_{2},c_{3}\\}\leftarrow
pull^{*}({\mathfrak{A}},c_{1}\leftarrow\mathfrak{pat}(c_{1}),c_{2}\leftarrow\mathfrak{pat}(c_{2}),c_{3}\leftarrow\mathfrak{pat}(c_{3}))$.
Similarly, for any pair of distinct elements $c_{1},c_{2}\in C$ for which the
substructure of ${\mathfrak{C}}$ has not yet been defined, set
${\mathfrak{C}}\\!\\!\restriction\\!\\!\\{c_{1},c_{2}\\}\leftarrow
pull({\mathfrak{A}},c_{1}\leftarrow\mathfrak{pat}(c_{1}),c_{2}\leftarrow\mathfrak{pat}(c_{2}))$.

${\mathfrak{C}}\models\varphi$.

######  Proof 4.2.

The purely universal conjuncts of $\varphi$ ($\mathcal{I}_{1}-$ and
$\mathcal{I}_{2}$-conjuncts) are satisfied since every $1$-type, $2$-outer-
type and $3$-outer-type defined in ${\mathfrak{C}}$ is copied (pulled) from
${\mathfrak{A}}$ (either in this subsection or in the previous one where
${\mathfrak{B}}$ was constructed), which is a model of $\varphi$. All elements
have witnesses for $\mathcal{I}_{4}$\- $\mathcal{I}_{5}$-, and
$\mathcal{I}_{6}$-conjuncts, as this is guaranteed in Stages 1, 2, and 3,
respectively. Finally, for every $c$ and every $j\in\mathcal{I}_{3}$,
$\mathfrak{f}_{j}(c)$ is a witness for $c$ and $\forall x\exists y\forall
z\varphi_{j}(x,y,z)$ in its copy of ${\mathfrak{B}}$. In Stage 4 we carefully
define $3$-outer-types on tuples consisting of $c,\mathfrak{f}_{j}(c)$ and
elements from the other copies of ${\mathfrak{B}}$, so that
$\mathfrak{f}_{j}(c)$ remains a witness for $c$ in the whole structure
${\mathfrak{C}}$.

The only point which remains to be explained is that there are no conflicts in
assigning types to tuples of elements. First note that there are no conflicts
when assigning $2$-outer-types. They are defined in Stage 1 and in the last
paragraph of Stage 2 (and completed in Stage 5–but this Stage may not be a
source of conflicts as it sets only the types which have not been set before).
The strategy is that the elements from $C_{m}$ look for witnesses in
$C_{m+1\text{ mod }5}$ and if an element $c$ looks for witnesses for conjuncts
indexed by different $i_{1},i_{2}$ then it always looks for them in different
copies of ${\mathfrak{B}}$. (A reader familiar with [GKV97] may note that the
way we deal with $2$-outer-types is similar to the one used in that paper,
where three sets of elements are used and the witnessing scheme is modulo
$3$.) Considering $3$-outer-types, they are set in Stages 2, and 3 (plus the
completion in Stage 4 and Stage 5). No outer-type definition from Stage 2 can
conflict with an outer-type definition from Stage 3: in Stage 2 we define
outer-types on tuples consisting of elements either belonging two three
different $C_{m}$, or two of them belongs to the same $C_{m}$ and the third
one to $C_{m+1}$, to a copy of ${\mathfrak{B}}$ indexed by $\mathcal{I}_{5}$;
in Stage 3 we set outer-types on tuples consisting of two elements from the
same $C_{m}$ and an element from $C_{m+1}$, but from a copy of
${\mathfrak{B}}$ indexed by $\mathcal{I}_{6}$. Definitions from the same
stage, involving two different $C_{m}$ do not conflict with each other due to
our circular witnessing scheme requiring elements from $C_{m}$ to look for
witnesses in $C_{m+1}$. The most interesting case is setting $3$-outer-types
for elements from $3$ different $C_{m}$-s (Stage 2). This is done without
conflict since the function $\mathfrak{chc}$ is $1-1$.

Since $|C|=8|B||\mathcal{I}|$, $|\mathcal{I}|$ is linear in $|\varphi|$ and
$|B|$ is exponential in $\varphi$ we see that $|C|$ is bounded exponentially
in $|\varphi|$, which completes the proof of Theorem. 10.

##  5 An excursion into three-variable logic

The main technical advance in this Section will be showing that the
decidability is retained if we relax the uniformity conditions in normal form
for $\mbox{\rm AUF}_{1}^{3}$, by allowing the formulas $\varphi_{i}$ in
$\mathcal{I}_{5}$\- and $\mathcal{I}_{6}$-conjuncts to be arbitrary (not
necessarily uniform) Boolean combinations of atoms. We believe that this
result is interesting in itself, but additionally it allows us to define a
pretty rich decidable class of $\mbox{\rm FO}^{3}$ formulas with nested
quantification, which we call $\mbox{\rm FO}^{3}_{-}$. Recall that $\mbox{\rm
FO}^{3}_{-}$ is defined in Preliminaries, where we also observed that it
contains both $\mbox{\rm FO}^{2}$ and $\mbox{\rm AUF}_{1}^{3}$.

Let us see that we are indeed able to reduce $\mbox{\rm FO}^{3}_{-}$ sentences
to normal form resembling that of $\mbox{\rm AUF}_{1}^{3}$. We say that an
$\mbox{\rm FO}^{3}_{-}$ sentence is in normal form if
$\varphi=\varphi_{1}\wedge\varphi_{2}$ for

$\displaystyle\varphi_{1}=\bigwedge_{i\in\mathcal{I}_{2}}\forall x\forall
y\forall z\varphi_{i}(x,y,z)\wedge\bigwedge_{i\in\mathcal{I}_{3}}\forall
x\exists y\forall z\varphi_{i}(x,y,z),\text{ and }$
$\displaystyle\varphi_{2}=\bigwedge_{i\in\mathcal{I}_{5}}\forall x\forall
y\exists z(x\not=y\rightarrow\varphi_{i}(x,y,z)),$

where the $\varphi_{i}$ for $i\in\mathcal{I}_{2}\cup\mathcal{I}_{3}$ are
positive Boolean combinations of literals using either one variable or all
variables from $\\{x,y,z\\}$ (uniform combinations), and the $\varphi_{i}$ for
$i\in\mathcal{I}_{5}$ are positive Boolean combinations of arbitrary literals
(without equality). We note that even though we generally do not admit
equality we allow ourselves to use $x\not=y$ as a premise in
$\mathcal{I}_{5}$-conjuncts; as we will see this use of equality simplifies
model constructions. Those conjuncts are actually equivalent to some equality-
free conjuncts $\forall x\forall y\exists z\varphi_{i}^{\prime}(x,y,z)$, and
hence Lemma 2, concerning the pull operation, holds for normal form $\mbox{\rm
FO}^{3}_{-}$ formulas.

######  Lemma 11.

(i) The satisfiability problem for $\mbox{\rm FO}^{3}_{-}$ can be reduced in
nondeterministic polynomial time to the satisfiability problem for normal form
$\mbox{\rm FO}^{3}_{-}$ sentences. (ii) If the class of all normal form
$\mbox{\rm FO}^{3}_{-}$ sentences has the finite (exponential) model property
then also the whole $\mbox{\rm FO}^{3}_{-}$ has the finite (exponential) model
property.

######  Proof 5.1.

(Sketch) We proceed as in the case of $\mbox{\rm AUF}_{1}^{-}$, introducing
new relation symbols to represent subformulas starting with a block of
quantifiers. This time we need symbols of arity $0$, $1$ and $2$. In
particular, subformulas of the form $\exists v\forall v^{\prime}\eta$
($\forall v\forall v^{\prime}\eta$) with a free variable $v^{\prime\prime}$
are replaced by $P(v^{\prime\prime})$ for a fresh symbol $P$ and axiomatized
by $\forall v^{\prime\prime}\exists v\forall
v^{\prime}(P(v^{\prime\prime})\rightarrow\eta)$ ($\forall
v^{\prime\prime}\forall v\forall
v^{\prime}(P(v^{\prime\prime})\rightarrow\eta)$), and subformulas $\exists
v\eta(v,v^{\prime},v^{\prime\prime})$ are replaced by
$R(v^{\prime},v^{\prime\prime})$ which is axiomatized by $\forall v\forall
v^{\prime}\exists
v^{\prime\prime}(R(v^{\prime},v^{\prime\prime})\rightarrow\eta))$. This way,
possibly by renaming the variables, we get a formula of the shape as in
$\mbox{\rm AUF}_{1}^{3}$-normal form but allowing the formulas $\varphi_{i}$
for $i\in\mathcal{I}_{5}\cup\mathcal{I}_{6}$ to be arbitrary (not necessarily
uniform) Boolean combinations of atoms. We can now eliminate
$\mathcal{I}_{1}$-, $\mathcal{I}_{4}$\- and $\mathcal{I}_{6}$-conjuncts. We
first proceed with $\mathcal{I}_{6}$-conjuncts $\forall x\exists y\exists
z\varphi_{i}(x,y,z)$, replacing them with the conjunctions of $\forall
x\exists yR(x,y)$ and $\forall x\forall y\exists
z(R(x,y)\rightarrow\varphi_{i}(x,y,z))$, for a fresh binary symbol $R$. Then
for $\mathcal{I}_{1}$-conjuncts $\forall x\forall y\varphi_{i}(x,y)$, we just
equip them with a dummy existential quantifier: $\forall x\forall y\exists
z\varphi_{i}(x,y)$, and for $\mathcal{I}_{4}$-conjuncts $\forall x\exists
y\varphi_{i}(x,y)$ we add a dummy universal quantifier and rename variables:
$\forall x\forall y\exists z\varphi_{i}(x,z)$. We end up with only
$\mathcal{I}_{5}$-conjuncts in the $\varphi_{2}$ part of $\varphi$. Finally,
any conjunct of the form $\forall x\forall y\exists z\varphi_{i}(x,y,z)$ is
replaced by $\forall x\forall y\exists
z(x\not=y\rightarrow\varphi_{i}(x,y,z)\wedge\varphi_{i}(x,x,z))$. It should be
clear that our transformations are sound over the domains consisting of at
least two elements. (Singleton models can be enumerated and checked
separately.)

###  5.1 The complexity of $\mbox{\rm FO}^{3}_{-}$

In this Section we show that $\mbox{\rm FO}^{3}_{-}$ is decidable, moreover
its satisfiability problem is still in NExpTime. Concerning the obtained
results, this subsection is a bit redundant, as in the next subsection,
applying an alternative, probabilistic approach, we demonstrate the
exponential model property for $\mbox{\rm FO}^{3}_{-}$, which immediately
gives the same NExpTime-upper bound on the complexity of the satisfiability
problem, and additionally proves the same bound on the complexity of the
finite satisfiability problem.

We decided to keep this subsection (although presenting some constructions and
proofs in a slightly more sketchy way), since it gives some additional insight
in the nature of the considered problems. We proceed here in a rather
classical way: we show that a normal form $\mbox{\rm FO}^{3}_{-}$ sentence
$\varphi$ is satisfiable iff it has a certain _witness for satisfiability_ ,
of exponentially bounded size, as stated in the following lemma. Such a
witness of satisfiability is a structure which is “almost” a model of
$\varphi$. It will turn out that one can quite easily (i) extract a witness
from a given model of $\varphi$ and (ii) unwind a witness into a proper
infinite model of $\varphi$. In both directions we use a chase-like procedure.

######  Lemma 12.

A normal form $\mbox{\rm FO}^{3}_{-}$ sentence
$\varphi=\varphi_{1}\wedge\varphi_{2}$ is satisfiable iff there exists a
structure ${\mathfrak{D}}$ of size bounded by $h(|\varphi|)$ for some fixed
exponential function $h$, and functions without fixed points
$\mathfrak{f}_{j}:D\rightarrow D$ for $j\in\mathcal{I}_{3}$, such that:

  * (a)

${\mathfrak{D}}\models\varphi_{1}$

  * (b)

for every $d,d^{\prime}\in D$ and every $j\in\mathcal{I}_{3}$ we have
${\mathfrak{D}}\models\varphi_{j}(d,\mathfrak{f}_{j}(d),d^{\prime})$.

  * (c)

for every $i\in\mathcal{I}_{5}$, for every $2$-type $\beta$ realized in
${\mathfrak{D}}$, there is a realization $(d,d^{\prime})$ of $\beta$ and an
element $d^{\prime\prime}$ such that $d^{\prime\prime}\not=d$,
$d^{\prime\prime}\not=d^{\prime}$ and
${\mathfrak{D}}\models\varphi_{i}(d,d^{\prime},d^{\prime\prime})$.

  * (c’)

for every $i\in\mathcal{I}_{5}$, for every $2$-type $\beta$ realized in
${\mathfrak{D}}$ by a pair $(d_{0},\mathfrak{f}_{j}(d_{0}))$ for some $d_{0}$
and $j$, there is $d\in D$ such that for $d^{\prime}=\mathfrak{f}_{j}(d)$ the
pair $(d,d^{\prime})$ has type $\beta$ and there is an element
$d^{\prime\prime}$ such that $d^{\prime\prime}\not=d$,
$d^{\prime\prime}\not=d^{\prime}$ and
${\mathfrak{D}}\models\varphi_{i}(d,d^{\prime},d^{\prime\prime})$.

A structure ${\mathfrak{D}}$, together with the functions $\mathfrak{f}_{j}$
meeting the conditions of the above lemma will be called _a witness of
satisfiability for $\varphi$_. As we see ${\mathfrak{D}}$ satisfies the
$\mathcal{I}_{2}$\- and $\mathcal{I}_{3}$-conjuncts of $\varphi$ (Conditions
(a), (b)), but need not to satisfy the $\mathcal{I}_{5}$-conjuncts. However,
if a pair $d_{0},d_{0}^{\prime}$ does not have a witness for an
$\mathcal{I}_{5}$-conjunct, then there is an appropriate “similar” pair
$d,d^{\prime}$ having such a witness (Conditions (c), (c’)).

Let us first prove the left-to-right direction of Lemma 12.

Left-to-right: extracting a witness of satisfiability from a model.

_Stage 1: The building block ${\mathfrak{B}}$._ Let ${\mathfrak{A}}$ be a
model of a normal form $\mbox{\rm FO}^{3}_{-}$ formula
$\varphi=\varphi_{1}\wedge\varphi_{2}$. Let $\alpha$ and $\beta$ be the sets
of all 1-types and all 2-outer-types realized in ${\mathfrak{A}}$,
respectively. Since our logic does not support equality, wlog. we assume that
for each 1-type $\alpha\in\mbox{\large\boldmath$\alpha$}$, there exists a pair
$a,b\in{\mathfrak{A}}$ realizing the 2-outer-type
$\beta\in\mbox{\large\boldmath$\beta$}$ which “unwinds” $\alpha$, which means
that: ${\rm tp}^{{{\mathfrak{A}}}}({a})={\rm
tp}^{{{\mathfrak{A}}}}({b})=\alpha$, and for each relation symbol $R$ in the
signature it holds: ${\mathfrak{A}}\models R(a,b)$ iff ${\mathfrak{A}}\models
R(a,a)$, and ${\mathfrak{A}}\models R(b,a)$ iff ${\mathfrak{A}}\models
R(a,a)$.

Let ${\mathfrak{B}}$ be the finite structure constructed for $\varphi_{1}$ and
${\mathfrak{A}}$ as in Section 4.1. It will serve as a building block in the
construction of a witness of satisfiability ${\mathfrak{D}}$ for $\varphi$.
Inspecting the construction of ${\mathfrak{B}}$ we note that the set of
$1$-types realized in ${\mathfrak{B}}$ is precisely $\alpha$ and the set of
$2$-types is contained in $\beta$; and regarding the size of ${\mathfrak{B}}$,
it is exponentially bounded in $|\varphi|$. Let $\mathfrak{f}_{j}:B\to B$ for
$j\in\mathcal{I}_{3}$ be the witness functions defined as in Section 4.1.

_Stage 2: The domain of ${\mathfrak{D}}_{s}$._ The witness of satisfiability
${\mathfrak{D}}$ will consists of some number of copies of the structure
${\mathfrak{B}}$, say $k$ (will be clarified later). More precisely, we will
construct a sequence of structures
${\mathfrak{D}}_{0},{\mathfrak{D}}_{1},\dots,{\mathfrak{D}}_{k-1}$, where
${\mathfrak{D}}_{0}$ is isomorphic to ${\mathfrak{B}}$ and
${\mathfrak{D}}_{k-1}={\mathfrak{D}}$. Each ${\mathfrak{D}}_{s+1}$ will be
created from ${\mathfrak{D}}_{s}$ by attaching a fresh disjoint copy of
${\mathfrak{B}}$, providing an $\mathcal{I}_{5}$-witness for some pair of
elements of $({\mathfrak{D}}_{s+1}\\!\\!\restriction\\!\\!D_{s})$, and then
completing the structure.

Formally, the domain of ${\mathfrak{D}}_{s}$ is the set

$D_{s}=B\times\\{0,\dots,s\\}.$

We make the structure
${\mathfrak{D}}_{s}\\!\\!\restriction\\!\\!(B\times\\{s\\})$ isomorphic to
${\mathfrak{B}}$ and for $s>0$ we make the structure
${\mathfrak{D}}_{s}\\!\\!\restriction\\!\\!(B\times\\{0,\dots,s-1\\})$
isomorphic to ${\mathfrak{D}}_{s-1}$. We should think that $B\times\\{0\\}$ is
the “main” copy of ${\mathfrak{B}}$ and $B\times\\{m\\}$ for $m>0$ are
auxiliary copies that will help us to satisfy the conditions (c) and (c’). We
can adopt the functions $\mathfrak{f}_{j}:B\to B$ to the functions
$\mathfrak{f}_{j}:D_{s}\to D_{s}$ by letting
$\mathfrak{f}_{j}((b,m))=(\mathfrak{f}_{j}(b),m)$.

We introduce a notion of an _extended 2-type_
$(\beta,j)\in\mbox{\large\boldmath$\beta$}\times(\mathcal{I}_{3}\cup\\{\bot\\})$
which except the information about the 2-outer-type contains an information
about whether one of the element (of a pair realizing this $2$-type) is an
$\mathcal{I}_{3}$-witness for the other. We say that