# A Uniform One-Dimensional Fragment with Alternation of Quantifiers

Emanuel Kieroński Institute of Computer Science
University of Wrocław, Poland<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 of first-order
logic 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 quantifiers in blocks. We identify a non-trivial
variation of the logic with mixed blocks of quantifiers which retains some
good properties of the two-variable fragment and of the uniform one-
dimensional fragment: it has the finite (exponential) model property and hence
decidable, NExpTime-complete satisfiability problem.

##  1 Introduction

In this paper we are going to push forward the research on the uniform one-
dimensional fragment of first-order logic. To set up the scene and locate our
results in a broader context let us first recall some facts about the two-
variable fragment, $\mbox{\rm FO}^{2}$. $\mbox{\rm FO}^{2}$, obtained just by
restricting first-order logic so that its formulas may use only variables $x$
and $y$, is one of the most important decidable fragments of first-order logic
identified so far. The decidability of its satisfiability problem was shown by
Scott [35] in the case without equality, and by Mortimer [27] in the case with
equality. In [27] it is proved that the logic has the finite model property,
that is, its every satisfiable formula has a finite model. Later, Grädel,
Kolaitis and Vardi [12] strengthened that result, by showing that every
satisfiable formula has a model of size bounded exponentially in its length.
This exponential model property led to the NExpTime upper bound on the
complexity of $\mbox{\rm FO}^{2}$ satisfiability. The matching lower bound
follows from the earlier work by Lewis [25].

An important motivation for studying $\mbox{\rm FO}^{2}$ is the fact 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 those formalisms. However, its simplicity and
naturalness make it also an attractive logic in itself, inheriting potential
applications in knowledge representation, artificial intelligence, or
verification of hardware and software from modal and description logics.
Plenty of results on $\mbox{\rm FO}^{2}$, its extensions and variations have
been obtained in the last few decades, e.g., decidability was shown for
$\mbox{\rm FO}^{2}$ with counting quantifiers [13, 28, 29], one or two
equivalence relations [20, 19], counting quantifiers and equivalence relation
[30], betweenness relations [23], its complexity was established on words and
trees, in various scenarios including the presence of data or counting [6, 5,
9, 10, 4], to mention just a few of them.

However, further applications, e.g., in database theory are limited by the
fact that $\mbox{\rm FO}^{2}$ and its extensions mentioned above can speak
non-trivially only about relations of arity at most two. This is in contrast
to some other decidable fragments studied because of their potential
applications in computer science, like the guarded fragment, GF [2], the unary
negation fragment, UNFO [8], the guarded negation fragment, GNFO [3], or the
fluted fragment, FF [33, 32].

A natural question is whether there is 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 we can find a few such formalisms.

An interesting idea is for example to combine $\mbox{\rm FO}^{2}$ with GF. The
idea can be traced back already in Kazakov’s PhD thesis [16], was present in
the work by Bourish, Morak and Pieris [7], and found a more systematic
treatment in the paper by Rudolph and Šimkus [34], who formally introduced the
triguarded fragment, TGF. TGF is obtained from GF by allowing quantification
for subformulas with at most two free variables to be unguarded. What we get
this way is a logic in which one can speak freely about pairs of elements, and
in a local, guarded way about tuples of bigger arity. 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 [34]; the finite
model property is retained [22]. A variation of the idea above is the one-
dimensional triguarded fragment [21], still containing $\mbox{\rm FO}^{2}$,
which becomes decidable even in the presence of equality.

$\mbox{\rm FO}^{2}$ (or, actually, even its extension with counting
quantifiers, C2) was also combined with FF by Pratt-Hartmann [31]. This logic
was shown decidable but the complexity of its satisfiability problem is non-
elementary, as already FF alone has non-elementary complexity [32].

Finally, probably the most canonical extension of $\mbox{\rm FO}^{2}$ to
contexts with relations of arity bigger than two, capturing the spirit of
$\mbox{\rm FO}^{2}$ more closely than the logics discussed above, is the
_uniform one-dimensional fragment_ , $\mbox{\rm UF}_{1}$, proposed by Hella
and Kuusisto [14]. In this fragment quantifiers are used in blocks and a
single block is built out only of existential or only of universal quantifiers
and leaves at most one variable free; a fragment meeting this condition is
called _one-dimensional_. Imposing one-dimensionality alone is not sufficient
for ensuring the decidability of the satisfiability problem and thus another
restriction, _uniformity_ , is applied which, roughly speaking, allows boolean
combinations of atoms only if the atoms use precisely the same set of
variables or use just one variable. 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. [24]). In [14] it is shown that $\mbox{\rm UF}_{1}$ without
equality is decidable and has the finite model property. In [17] this result
is improved by showing that the decidability is retained even if free use of
equalities is allowed (by _free use_ of equalities we mean that they need not
obey the uniformity restriction) and that the logic has exponential model
property and NExpTime-complete satisfiability problem, exactly as $\mbox{\rm
FO}^{2}$.

A question arises whether the requirement that the blocks of quantifiers from
the definition of $\mbox{\rm UF}_{1}$ must consist of quantifiers of the same
type (all universal or all existential) is necessary for decidability, that is
what happens if we allow one to mix quantifiers as, e.g., in the formula
$\forall x\exists y\forall zR(x,y,z,t)$. Let us denote the extension of
$\mbox{\rm UF}_{1}$ allowing to alternate quantifiers in blocks $\mbox{\rm
AUF}_{1}$. The motivations behind studying $\mbox{\rm AUF}_{1}$ are
multifarious. $\mbox{\rm UF}_{1}$ lies very close to the borderlines between
the decidable and undecidable, so, firstly and most importantly, analysing its
expressive extensions may enhance our understanding of these borderlines which
may be also useful in different scenarios. Secondly, the logics $\mbox{\rm
UF}_{1}$ and $\mbox{\rm AUF}_{1}$ can be useful themselves, offering
extensions of modal and description logics to contexts with relations of arity
greater than two, such as databases, orthogonal to other proposals. Thirdly,
though it is of course a matter of taste, we believe that $\mbox{\rm AUF}_{1}$
is just quite an elegant formalism, which can be justified by a relative
simplicity of its definition and a nice game-theoretic characterization of its
expressivity—natural Ehrenfeucht-style games for $\mbox{\rm UF}_{1}$ were
introduced in [17]; shifting to $\mbox{\rm AUF}_{1}$ would probably allow for
an even nicer game characterizations (though this topic is not formally
studied in this paper).

The first step to understand $\mbox{\rm AUF}_{1}$ was done in the companion
paper [11], where we show the decidability and the finite model property of
the three variable restriction of this logic, $\mbox{\rm AUF}_{1}^{3}$; in
that paper $\mbox{\rm AUF}_{1}^{3}$ is then made a basis for obtaining a rich
decidable subclass of the three-variable fragment, $\mbox{\rm FO}^{3}$.

Turning now to our current contribution, we first remark that in this paper we
still do not answer the question whether the whole $\mbox{\rm AUF}_{1}$ has
decidable satisfiability. We however make another step towards understanding
$\mbox{\rm AUF}_{1}$ by identifying its fragment, $\mbox{\rm AUF}_{1}^{-}$,
which contains full $\mbox{\rm FO}^{2}$ without equality, allows for mixed
blocks of quantifiers of unbounded length, has NExpTime-complete
satisfiability problem, and has the exponential model property. Additionally,
we observe that if we allow for a free use of equality in $\mbox{\rm
AUF}_{1}^{-}$ then we lose the finite model property.

The main restriction of $\mbox{\rm AUF}_{1}^{-}$, compared to full $\mbox{\rm
AUF}_{1}$, is that it admits only blocks of quantifiers that are purely
universal or end with the existential quantifier. Additionally, mostly for the
clarity of presentation, we will define $\mbox{\rm AUF}_{1}^{-}$ not as an
extension of the version of $\mbox{\rm UF}_{1}$ originally defined in [14],
but rather as an extension of the _strongly_ uniform one-dimensional fragment,
$\mbox{\rm sUF}_{1}$, introduced in [18]. The definition of $\mbox{\rm
AUF}_{1}^{-}$ is inspired by the definition of the Maslov class
$\overline{\mbox{\rm K}}$ [26] and, as we will see in a moment, the
decidability of $\mbox{\rm AUF}_{1}^{-}$ can be shown by a reduction to
conjunctions of sentences in $\overline{\mbox{\rm K}}$, whose decidability was
shown by the resolution method by Hustadt and Schmidt [15]. However, this
reduction does not allow us to establish the precise compleixty of $\mbox{\rm
AUF}_{1}^{-}$, since, to the best of our knowledge, the precise complexity of
the Maslov class has not been established. It is also not known whether
$\overline{\mbox{\rm K}}$ has the finite model property.

##  2 Preliminaries

###  2.1 Notation and terminology

We assume that the reader is familiar with first-order logic. We work with
purely relational signatures with no constants nor function symbols. We refer
to structures using Fraktur capital letters, and to their domains using the
corresponding Roman capitals. Given a structure ${\mathfrak{A}}$ and some
$B\subseteq A$ 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 of structures, and $x$, $y$,
$\ldots$ for variables; all of these possibly with some decorations. For a
tuple of variables $\overline{x}$ we use $\psi(\overline{x})$ to denote that
the free variables of $\psi$ are in $\overline{x}$.

In the context of uniform logics it is convenient to speak about some
partially defined (sub)structures which we will call _pre-(sub)structures_. A
pre-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}$ contains all elements of $A$ or
just one of them. The truth values of all the other facts remain unspecified.
We will use Fraktur letters decorated with $*$ to denote pre-structures: a
pre-structure with domain $A$ will be denoted by ${\mathfrak{A}}^{*}$. If a
structure ${\mathfrak{A}}$ is fully defined, ${\mathfrak{A}}^{*}$ denotes its
induced pre-structure. Similarly, if $B\subseteq A$ is a subdomain of some
structure ${\mathfrak{A}}$ we donote by ${\mathfrak{B}}^{*}$ the pre-structure
$({\mathfrak{A}}\\!\\!\restriction\\!\\!B)^{*}$ and call it a pre-substructure
of ${\mathfrak{A}}$.

An (atomic) $1$-type over a signature $\sigma$ is a maximal consistent set of
atomic or negated atomic formulas over $\sigma$ using at most one variable
$x$. We often identify a $1$-type with the conjunction of its elements. We
will usually be interested in $1$-types over signatures $\sigma$ consisting of
the relation symbols used in some given formula. Observe that the number of
$1$-types is bounded by a function which is exponential in $|\sigma|$, and
hence also in the length of the formula. This is because a $1$-type just
corresponds to a subset of $\sigma$.

Let ${\mathfrak{A}}$ be a structure, and let $a\in A$. We denote by ${\rm
tp}^{{{\mathfrak{A}}}}({a})$ the unique atomic 1-type _realized_ in
${\mathfrak{A}}$ by the element $a$, _i.e._ , the $1$-type $\alpha(x)$ such
that ${\mathfrak{A}}\models\alpha(a)$.

###  2.2 Satisfiability and finite model property

Let $\mathcal{L}$ be a class of first-order formulas (a logic). The _(finite)
satisfiability problem_ for $\mathcal{L}$ takes as its input a sentence from
$\mathcal{L}$ and verifies if it has a (finite) model. $\mathcal{L}$ has the
_finite model property_ if every satisfiable sentence in $\mathcal{L}$ has a
finite model; $\mathcal{L}$ has the _exponential model property_ if there is a
fixed exponential function $f$ such that every satisfiable sentence $\varphi$
has a finite model over a domain whose size if bounded by $f(|\varphi|)$
(where the length of $\varphi$, $|\varphi|$, is measured in any reasonable
fashion).

###  2.3 Logics

As the starting point we define the logic s$\mbox{\rm UF}_{1}$ (without
equality), called in [18] the _strongly restricted uniform one-dimensional
fragment_. Formally, for a relational signature $\sigma$, the set of
$\sigma$-formulas of s$\mbox{\rm UF}_{1}$ is the smallest set $\mathcal{F}$
such that:

  * •

every $\sigma$-atom using at most one variable is in $\mathcal{F}$

  * •

$\mathcal{F}$ is closed under Boolean connectives

  * •

if $\varphi(x_{0},\ldots,x_{k})$ is a Boolean combination of formulas in
$\mathcal{F}$ with free variables in $\\{x_{0},\ldots,x_{k}\\}$ and
atoms111Please note that those atoms need not to belong to $\mathcal{F}$.
built out of precisely all of the variables $x_{0},\ldots,x_{k}$ (in an
arbitrary order, possibly with repetitions) then $\exists
x_{0},\ldots,x_{k}\varphi$, $\exists x_{1},\ldots,x_{k}\varphi$, $\forall
x_{0},\ldots,x_{k}\varphi$ and $\forall x_{1},\ldots,x_{k}\varphi$ are in
$\mathcal{F}$.

Example formulas in s$\mbox{\rm UF}_{1}$ are:

$\forall xyz(P(x)\wedge P(y)\wedge P(z)\rightarrow R(x,y,z)\vee\neg
S(z,z,x,y))$ $\forall x(P(x)\rightarrow\exists yz(\neg R(y,z,x)\wedge(\neg
R(x,y,z)\vee P(y))))$

For interested readers we say that (non-restricted) _uniform one-dimensional
fragment_ is defined as above but in the last point of the definition the non-
unary atoms must not necessarily use the whole set $\\{x_{0},\ldots,x_{k}\\}$
of variables but rather all those atoms use the same subset of this set (see
[14]).

By $\mbox{\rm AUF}_{1}$ we denote the extension of s$\mbox{\rm UF}_{1}$
without equality with _alternation of quantifiers in blocks_. The set of
$\sigma$-formulas of $\mbox{\rm AUF}_{1}$ is the smallest set $\mathcal{F}$
such that:

  * •

every $\sigma$-atom using at most one variable is in $\mathcal{F}$

  * •

$\mathcal{F}$ is closed under Boolean connectives

  * •

if $\varphi(x_{0},\ldots,x_{k})$ is a Boolean combination of formulas in
$\mathcal{F}$ with free variables in $\\{x_{0},\ldots,x_{k}\\}$ and atoms
built out of precisely all of the variables $x_{0},\ldots,x_{k}$ (in an
arbitrary order, possibly with repetitions) then
$\mbox{Q}_{0}x_{0}\ldots\mbox{Q}_{k}x_{k}\varphi$ and
$\mbox{Q}_{1}x_{1}\ldots\mbox{Q}_{k}x_{k}\varphi$ are in $\mathcal{F}$, where
each $\mbox{Q}_{i}$ is one of $\exists,\forall$.

Finally, we define a subset $\mbox{\rm AUF}_{1}^{-}$ of $\mbox{\rm AUF}_{1}$
by requiring that its formulas are written in negation normal form NNF (that
is negation is used only in front of atomic formulas, and the only other
Boolean connectives are $\vee$ and $\wedge$), and that every sequence of
quantifiers in the last point of the definition either contains only universal
quantifiers or the last quantifier $\mbox{Q}_{k}$ is existential. In
$\mbox{\rm AUF}_{1}^{-}$ we can write, e.g.:

$\forall xy\exists z(\neg P(x)\wedge\neg P(y)\vee R(x,y,z))$ $\forall
x(P(x)\vee\exists y\forall z\exists tS(x,y,z,t))$ $\forall
xyz(R(x,y,z)\vee\exists tT(x,t)\wedge\exists tT(y,t)\wedge\exists tT(z,t))$

Observe that $\mbox{\rm AUF}_{1}^{-}$ contains the whole s$\mbox{\rm UF}_{1}$
and hence also $\mbox{\rm FO}^{2}$. (For example the $\mbox{\rm FO}^{2}$
sentence $\exists x\forall y\psi(x,y)$ belongs to s$\mbox{\rm UF}_{1}$, since
one may think that it has two blocks of quantifiers, both of length one, and
indeed one of them is purely universal and the other ends with $\exists$.)

###  2.4 Normal forms and basic decidability result

We introduce normal form for $\mbox{\rm AUF}_{1}^{-}$ formulas, generalizing
Scott’s normal form for $\mbox{\rm FO}^{2}$ (cf. [35, 12]). We start with a
version involving $0$-ary predicates, called _weak_ normal form, and then
explain how to remove them. In our normal form as well as in some intermediate
formulas we allow ourselves to use implications which are usually not allowed
in NNF formulas, but here they are very natural (note that converting them to
disjunctions using the basic law $p\rightarrow q\equiv\neg p\vee q$ will not
affect the blocks of quantifiers). We say that a $\mbox{\rm AUF}_{1}^{-}$
sentence is in _weak normal form_ if it is a conjunction of formulas having
one of the following shapes.

$\displaystyle\mbox{Q}_{1}x_{1}\ldots\mbox{Q}_{k}x_{k}\psi(x_{1},\ldots,x_{k}),$
(1) $\displaystyle
E\rightarrow\mbox{Q}_{1}x_{1}\ldots\mbox{Q}_{k}x_{k}\psi(x_{1},\ldots,x_{k}),$
(2)

where

  * •

$k\geqslant 0$ is a natural number

  * •

the $x_{i}$ are distinct variables

  * •

$\psi$ is a quantifier-free $\mbox{\rm AUF}_{1}^{-}$ formula (Boolean
combination of atoms, each of them containing all the variables
$x_{1},\ldots,x_{k}$ or at most one of them)

  * •

every $\mbox{Q}_{i}$ is a quantifier (universal or existential) and either all
the $\mbox{Q}_{i}$ are universal (_universal conjunct_) or $\mbox{Q}_{k}$ is
existential (_existential conjunct_)

  * •

$E$ is a $0$-ary relation symbol

In particular, in a formula of type (1), $k$ may be equal to $0$; in this case
$\psi$ is a Boolean combination of $0$-ary predicates.

######  Lemma 1.

Let $\varphi$ be a $\mbox{\rm AUF}_{1}^{-}$ sentence. Then there exists a
polynomially computable $\mbox{\rm AUF}_{1}^{-}$ sentence $\varphi^{\prime}$
in weak normal form over a signature extending the signature of $\varphi$ by
some fresh unary and $0$-ary relation symbols, such that (i) every model of
$\varphi$ can be expanded to a model of $\varphi^{\prime}$ and (ii) every
model of $\varphi^{\prime}$ is a model of $\varphi$.

###### Proof.

(Sketch) Assume that $\varphi$ is in NNF. Take an innermost subformula
$\psi_{0}$ starting with a maximal block of quantifiers. If it has a free
variable, that is, is of the form

$\mbox{Q}_{1}x_{1}\ldots\mbox{Q}_{k}x_{k}\psi(x_{1},\ldots,x_{k},y)$

replace it by $P(y)$, for a fresh unary symbol $P$, and add the following
normal form conjunct $\varphi_{\psi_{0}}$ (partially) axiomatising $P$.

$\forall
y\mbox{Q}_{1}x_{1}\ldots\mbox{Q}_{k}x_{k}(P(y)\rightarrow\psi(x_{1},\ldots,x_{k},y)).$

In other words, $\varphi$ is replaced by
$\varphi(P(y)/\psi_{0})\wedge\varphi_{\psi_{0}}$.

If $\psi_{0}$ is a proper subsentence, that is it is of the form

$\mbox{Q}_{1}x_{1}\ldots\mbox{Q}_{k}x_{k}\psi(x_{1},\ldots,x_{k}),$

then replace it by $E$, for a fresh $0$-ary symbol $E$ and add the conjunct

$E\rightarrow\mbox{Q}_{1}x_{1}\ldots\mbox{Q}_{k}x_{k}\psi(x_{1},\ldots,x_{k}).$

Repeat this process as long as possible. Note that we indeed append conjuncts
belonging to $\mbox{\rm AUF}_{1}^{-}$.

The above process is similar to Scott’s reduction of $\mbox{\rm FO}^{2}$
formulas to their normal form. Besides the natural modifications needed to
deal with sequences of quantifiers rather than with single quantifiers, the
main difference is that in the appended conjuncts axiomatizing the freshly
introduced unary and $0$-ary predicates, we write implications in only one
direction. This is sound as our initial formula is assumed to be in NNF.
Indeed, consider a single step of the reduction, assuming that the case with a
free variable in $\psi_{0}$ applies. In this step
$\varphi^{\prime}=\varphi(P(y)/\psi_{0})\wedge\varphi_{\psi_{0}}$ is produced
from $\varphi$. Assuming that ${\mathfrak{A}}\models\varphi$ we obtain a model
${\mathfrak{A}}^{\prime}$ of $\varphi^{\prime}$ by making the unary relation
$P$ true at all elements $a$ of $A$ such that
${\mathfrak{A}}\models\psi_{0}[a]$. This makes the appended conjunct
$\varphi_{\psi_{0}}$ true; obviously, also $\varphi(P(y)/\psi_{0})$ remains
true. In the opposite direction assume
${\mathfrak{A}}^{\prime}\models\varphi^{\prime}$. It may happen that the
subformula $\psi_{0}(y)$ of $\varphi$ is true in ${\mathfrak{A}}^{\prime}$ in
more points than $P(y)$ is. However, to guarantee that $\varphi$ is true it
suffices that it is true _at least_ at those points where $P(y)$ is, which is
ensured by the appended conjunct $\varphi_{\psi_{0}}$; this is because
$\varphi$ is assumed to be in NNF and thus $\psi_{0}$ appears in $\varphi$ in
the scope of no negation symbol. We reason similarly for the case when
$\psi_{0}$ is a subsentence. ∎

For our purposes, that is showing the finite model property for $\mbox{\rm
AUF}_{1}^{-}$ and demonstrating that its satisfiability problem is in
NExpTime, we can further simplify our formulas, by eliminating $0$-ary
predicates. What we can do is to guess the truth values for all the $0$-ary
predicates and replace them by $\top$ or $\bot$, in accordance with the guess.
In particular, the conjuncts of the form
$E\rightarrow\mbox{Q}_{1}x_{1}\ldots\mbox{Q}_{k}x_{k}\psi(x_{1},\ldots,x_{k})$
are eliminated if $E$ is guessed to be $\bot$ and replaced just by
$\mbox{Q}_{1}x_{1}\ldots\mbox{Q}_{k}x_{k}\psi(x_{1},\ldots,x_{k})$ if $E$ is
guessed to be $\top$.

It is convenient to split the set of the resulting conjuncts into those whose
all quantifiers are universal and those which end with the existential
quantifier. We say that a sentence $\varphi$ is in _normal form_ if it is of
the following shape:

$\displaystyle\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},$ (3)

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}})$.

The discussion above justifies the following.

######  Lemma 2.

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

The reduction to normal form described above allows us to easily prove the
decidability of the satisfiability problem for $\mbox{\rm AUF}_{1}^{-}$. This
can be done by using the results on the Maslov Class $\overline{\text{K}}$
(which is a dual of the Maslov class K). Full definition of
$\overline{\text{K}}$ is quite complicated and can be found, e.g., in [15].
For our purposes it is sufficient to say that when converted to prenex form
$\overline{\text{K}}$ formulas look as follows:

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

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$.

Now, one easily observes that every $\mbox{\rm AUF}_{1}^{-}$-normal form
conjunct belongs to $\overline{\text{K}}$. Indeed, every
$\varphi^{\scriptscriptstyle\forall}_{i}$-conjunct is of the form (4) with
$m=l=0$ and its every atom satisfies either condition (i) or (ii); every
$\varphi^{\scriptscriptstyle\exists}_{i}$-conjunct is of the form (4) with
$m=k=0$ and every atom satisfying (i) or (iii).

Hence any normal form formula belongs to $\overline{\text{DK}}$, the class of
conjunctions of formulas in $\overline{\text{K}}$. The satisfiability problem
for $\overline{\text{K}}$ was shown to be decidable in [26]. This result was
extended to the class $\overline{\text{DK}}$ in [15]. This gives us the basic
decidability result.

######  Theorem 3.

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

We recall that the precise complexity of $\overline{\text{DK}}$ has not been
established. It is also not known if $\overline{\text{DK}}$ has the finite
model property and if its finite satisfiability is decidable. The same
questions for $\overline{\text{K}}$ are also open.

##  3 Finite model property

The following theorem is the main results of this paper. 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.

######  Theorem 4.

$\mbox{\rm AUF}_{1}^{-}$ has the exponential model property.

The rest of this section is devoted to a proof of the above theorem. By Lemma
2 we may restrict attention to formulas of the form (3).

###  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 finite 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 finite model. Assume that $\varphi$ is as in (3). 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}}$. The labelling function will be denoted $\mathcal{L}$ and
will assign elements from $B$ to tree nodes (with the exception of the root,
which will be assigned the special empty label).

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}$. Its satisfaction tree
$\mathcal{T}_{i}$ is built in the following process.

Start with a root labelled with the empty label. The root forms level $0$ of
the tree. Level $j$, $0<j\leqslant k_{i}$ will correspond to the quantifier
$\mbox{Q}^{i}_{j}$. Assume level $j-1$ has been constructed, for $0<j\leqslant
k_{i}$. For each of its nodes $n$:

  * •

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

  * •

If $\mbox{Q}^{i}_{j}=\exists$ then let $n_{1},\ldots,n_{j-1}=n$ be the
sequence of non-root nodes on the branch of $n$, ordered from the child of the
root towards $n$. 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}(n_{1}),\ldots,\mathcal{L}(n_{j-1}),b,x_{k+1},\ldots,x_{k_{i}}).$

It is clear that such an element exists. If $j<k_{i}$ then we call it an
_intermediate witness_ for $\varphi^{\scriptscriptstyle\exists}_{i}$, and if
$j=k_{i}$ we call it the _final witness_ for
$\varphi^{\scriptscriptstyle\exists}_{i}$. Add a single child $n^{\prime}$ of
$n$ to $\mathcal{T}_{i}$ and set $\mathcal{L}(n^{\prime})=b$. The added
element 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 non-root elements of $\flat$, ordered from the child of the
root towards the leaf.

We further overload the function $\mathcal{L}$ by allowing it to define also
labels for branches of the tree (by a _branch_ we mean here a sequence of
elements $n_{1},\ldots,n_{k_{i}}$ such that $n_{1}$ is a child of the root,
$n_{k_{i}}$ is a leaf, and each $n_{i+1}$ is a child of $n_{i}$). We label
each branch $\flat$ with the pre-substructure of ${\mathfrak{B}}$ over
$Set(\flat)$.

To declare some properties of satisfaction forests we need the following
notions. A pre-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}})$.
A pre-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 a 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 pre-structure on
$H$ in which, for every $i$, the $1$-type of $a_{i}$ is $f(a_{i})$.

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

  1. (T1)

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

    1. (a)

if $\mbox{Q}_{j}^{i}=\forall$ then $n$ 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 $n$ has precisely one child (recall that
this child is called an existential node)

  2. (T2)

for every branch $\flat\in\mathcal{T}_{i}$, assuming
$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}(\flat_{1})$ and in $\mathcal{L}(\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}(\flat_{1})=\mathcal{L}(\flat_{2})$.

  5. (T5)

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

Now we collect some properties of the whole sequence of trees
$\mathcal{T}_{1},\ldots,\mathcal{T}_{m_{\scriptscriptstyle\exists}}$
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}(\flat_{1})=\mathcal{L}(\flat_{2})$

  4. (F4)

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

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

######  Claim 5.

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

###### Proof.

(Sketch) 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
pre-structures defined in the whole forest. Let $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 pre-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 pre-structure ${\mathfrak{H}}^{*}$ on $H$ by setting the $1$-type
of $a_{i}$ to be $f(a_{i})$, and for every relation symbol $R$, and every
sequence $c_{1},\ldots,c_{l}$ of elements of $H$ such that $l$ is the arity of
$R$ and $\\{c_{1},\ldots,c_{l}\\}=H$, setting the truth-value of the atom
$R(c_{1},\ldots,c_{l})$ to be equal to the truth-value of
$R(g(c_{1}),\ldots,g(c_{l}))$ in ${\mathfrak{B}}$. 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 atoms appearing in
$\psi^{\scriptscriptstyle\forall}_{i}$ in the two considered structures
appropriately 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
$\mathcal{T}_{1},\ldots,\mathcal{T}_{m_{\scriptscriptstyle\exists}}$ together
with a labelling function $\mathcal{L}$, 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 pre-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).

######  Lemma 6.

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

###### Proof.

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 5.

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}(\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 pre-structure on $Set(\flat)$ in
accordance with $\mathcal{L}(\flat)$.

_Step 3: Completion._ For any set of distinct elements
$\\{b_{1},\ldots,b_{k}\\}$ whose pre-structure is not yet defined, choose any
$\varphi^{\scriptscriptstyle\forall}$-compatible pre-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 pre-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 pre-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 domain

We are ready to present the main construction of this paper in which we show
that every satisfiable formula has a satisfaction forest over a small domain.

Let ${\mathfrak{A}}$ be a (possibly infinite) model of a normal form sentence
$\varphi$ of the shape as in (3). We show how to construct a satisfaction
forest over a domain of size bounded exponentially in $|\varphi|$. By Lemma 6
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_{1},\ldots,\alpha_{L}$. Let $K=\max\\{k_{i}:1\leqslant i\leqslant
m_{\scriptscriptstyle\exists}\\}$. We define the domain $B$ to be
$\\{1,\ldots,2K\\}\times\\{1,\ldots,m_{\scriptscriptstyle\exists}\\}\times\\{1,\ldots,(K-1)^{K-1}\\}\times\\{1,\ldots,L\\}$.
Note that $K$ 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. 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 7 (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 $\\{1,\ldots,n\\}$ and for
$1\leqslant l\leqslant n$ let $[n]^{l}$ denote the set of all subsets of $[n]$
of cardinality $l$.

######  Lemma 8.

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

###### Proof.

Consider the bipartite graph $([2K]^{l},[2K]^{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 $[2K]^{l}$. To this end we apply Hall’s marriage theorem. In
our graph every node from $[2K]^{l}$ has degree $2K-l$ (given an $l$-element
subset of $[2K]$ it can be expanded to an $l+1$ subset just by adding to it
precisely one of the remaining $2K-l$ elements) and every node from
$[2K]^{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 $[2K]^{l}$. The nodes of this subset are incident to
$|W|\cdot(2K-l)$ edges in total. Let us see that the number of nodes in
$[2K]^{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(2K-l)$ edges emitted by $W$, but this means that
$|W|\cdot(2K-l)\leqslant(|W|-1)\cdot(l+1)$. Rearranging this inequality we get
that $|W|(2K-2l-1)+l+1\leqslant 0$. But using the assumption that $0<l<K$ we
have that $(2K-2l-1)>0$ and hence the whole left-hand side of the last
inequality must be greater than $0$. Contradiction. Thus our graph satisfies
the Hall’s theorem assumptions which guarantee the existence of a matching
from $[2K]^{l}$ to $[2K]^{l+1}$, covering entirely $[2K]^{l}$. This matching
can be taken as $ext_{l}$. ∎

Choose an extension function $ext_{l}$ for every $l$ and let
$ext=\bigcup_{l=1}^{K-1}ext_{l}$, that is, $ext$ is a function which takes a
non-empty subset of $[2K]$ of size at most $K-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
$\mathcal{T}_{1},\ldots,\mathcal{T}_{m_{\scriptscriptstyle\exists}}$ for
$\varphi$ over the domain $B$. 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 pre-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 $\mathcal{T}_{i}$, a
$\varphi^{\scriptscriptstyle\exists}_{i}$-satisfaction tree over $B$. 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 (pre-structures on the set of elements
formed from the labels of the nodes on a branch).

We define an auxiliary function $pat$ which for every node of
$\mathcal{T}_{i}$ returns _a pattern element_ from ${\mathfrak{A}}$. We will
choose $pat(n)$, so that its $1$-type is equal to type of $\mathcal{L}(n)$. We
remark, that if two nodes from different branches have the same label then
they do not need to have the same pattern element.

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

  * •

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

    * –

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

    * –

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

  * •

If $n_{k}$ is existential then we need to define both $\mathcal{L}(n)$ and
$pat(n)$. 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}(pat(n_{1}),\ldots,pat(n_{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}(pat(n_{1}),\ldots,pat(n_{k-1}),w,x_{k+1},\ldots,x_{k_{i}})$

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

    * –

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

      * *

if $pat(n_{j})=w$ for some $j<k$ then set
$\mathcal{L}(n_{k})=\mathcal{L}(n_{j})$

      * *

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

    * –

If $n_{k}$ is a leaf then let $\flat$ be the branch of $n_{k}$ and let
$S=\\{j:n_{l}\in B_{j}\mbox{ for some }l<k\\}$. Of course, $|S|<k\leqslant K$
so $ext(S)$ is defined. Let $s$ be the unique member of $ext(S)\setminus S$.
We take as $\mathcal{L}(n_{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 K-1$ and thus there are at most $(K-1)^{K-1}$
different branches whose nodes from the first $K-1$ levels are labelled by
elements of $|Set^{-}(\flat)|$ (recall that there are $(K-1)^{K-1}$ possible
choices for $t$).

Take now any branch $\flat$ of $\mathcal{T}_{i}$. It remains to define the
pre-structure $\mathcal{L}(\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(pat(a_{i_{1}}),\ldots,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 $pat(a_{j})$.
This completes the definition of the pre-structure on $Set(\flat)$. Note that
this ensures that this pre-structure satisfies
$\psi_{i}^{\exists}(Seq(\flat))$.

###  3.3 Correctness

Let us now see that the 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$, $\flat^{\prime}$
in a tree $\mathcal{T}_{i}$ with $Set(\flat)=Set(\flat^{\prime})$. Indeed, we
have chosen as labels of the leaves of $\flat$ and $\flat^{\prime}$ two
different elements $b=(s,i,x,*)$ and $b^{\prime}=(s,i,y,*)$ of a layer $B_{s}$
which is not inhabited by the elements of $Set^{-}(\flat)$ or
$Set^{-}(\flat^{\prime})$ (due to the use of the function $ext$). So $b\in
Set(\flat)$ but $b\not\in Set(\flat^{\prime})$ and thus
$Set(\flat)\not=Set(\flat^{\prime})$.

  * •

To show that (T5) holds assume to the contrary that for some branch $\flat$,
${\mathfrak{H}}^{*}=\mathcal{L}(\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 pre-structure in $\mathcal{L}(\flat)$ implies
that
${\mathfrak{A}}\not\models\psi^{\scriptscriptstyle\forall}_{i}(pat(a_{1}),\ldots,pat(a_{l_{i}}))$,
that is ${\mathfrak{A}}$ violates $\varphi^{\scriptscriptstyle\forall}_{i}$.
Contradiction.

  * •

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

  * •

For (F3) the argument is similar to the argument for (T4): We show that there
is is pair of branches $\flat_{1}$, $\flat_{2}$ in a tree $\mathcal{T}_{i}$,
and resp., $\mathcal{T}_{j}$, $i\not=j$, with $Set(\flat_{1})=Set(\flat_{2})$.
Again, this follows from the fact that we have chosen as labels of the leaves
of $\flat_{1}$ and $\flat_{2}$ two different elements $b$ and $b^{\prime}$ of
a layer $B_{s}$ which is not inhabited by the elements of $Set^{-}(\flat_{1})$
or $Set^{-}(\flat_{2})$. This time the elements $b_{1}$ and $b_{2}$ are
different from each other since $b_{1}=(s,i,*,*)$ and $b_{2}=(s,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}}$).

An immediate consequence of Thm. 4 is:

######  Theorem 9.

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

###### Proof.

The lower bound is inherited from the lower bound for $\mbox{\rm FO}^{2}$
[25]. Let us turn to the upper bound.

By Lemma 2 it suffices to show how to decide satisfiability of a normal form
sentence $\varphi$. By Theorem 4 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. ∎

##  4 Infinity axiom with free use of equality

In this section we note that allowing for free use of equality in our logic
changes the situation significantly: we lose the finite model property. We
recall that in the case of $\mbox{\rm UF}_{1}$ free use of equality does not
spoil the decidability and even does not change the complexity.

In the recent paper [11] we note that the fragment with arbitrary blocks of
quantifiers $\mbox{\rm AUF}_{1}$ and with free use of equality contains
infinity axioms (satisfiable formulas without finite models), by constructing
the following three-variable formula:

$\exists xS(x)\wedge\forall x\exists y\forall z(\neg S(y)\wedge
R(x,y,z)\wedge(x=z\vee\neg R(z,y,x))),$

which has no finite models but is satisfied in the model whose universe is the
set of natural numbers, $S$ is true only at $0$ and $Rxyz$ is true iff
$y=x+1$.

The above example can be simply adapted to the case of $\mbox{\rm
AUF}_{1}^{-}$ with free use of equality. We just add a dummy existentially
quantified variable $t$ and require it to be equal to the previous,
universally quantified variable $z$. To accommodate all the variables we
increase the arity of $R$ by $2$ (one can think that the first and the last
position of $R$ from the previous example have been doubled):

$\exists xS(x)\wedge\forall x\exists y\forall z\exists t.(t=z\wedge\neg
S(y)\wedge R(x,x,y,z,t)\wedge(x=z\vee\neg R(z,t,y,x,x))).$

##  5 Conclusions

We identified a non-trivial uniform one-dimensional logic in which a use of
mixed blocks of quantifiers is allowed, strictly extending the two-variable
fragment $\mbox{\rm FO}^{2}$ without equality and the previously defined
fragment $\mbox{\rm sUF}_{1}$ without equality. We proved that, similarly to
$\mbox{\rm FO}^{2}$ and s$\mbox{\rm UF}_{1}$, this logic has the finite,
exponential model property and NExpTime-complete satisfiability problem.

There are two interesting directions, orthogonal to each other, in which it
would be valuable to extend our work. The first is investigating the
decidability, complexity and the status of the finite model property for full
$\mbox{\rm AUF}_{1}$ without equality, that is to see what happens to our
logic if arbitrary blocks of quantifiers, possibly ending with the universal
quantifier, are allowed. As already mentioned, in our recent work [11] we
answered this question for the three variable restriction, $\mbox{\rm
AUF}_{1}^{3}$, of $\mbox{\rm AUF}_{1}$ by showing the exponential model
property and NExpTime-completeness of its satisfiability problem.

The second idea is to revive the research on Maslov Class
$\overline{\text{K}}$, by attempting to determine the precise complexity of
its satisfiability problem and investigating whether it has the finite model
property. When designing the fragment $\mbox{\rm AUF}_{1}^{-}$ we took some
inspiration from the definition of $\overline{\text{K}}$, and indeed we were
able to reduce satisfiability of the former to the latter. We believe that
what we have learned working on $\mbox{\rm AUF}_{1}^{-}$ will prove useful in
the case of $\overline{\text{K}}$.

There are also some probably slightly less attractive, but still interesting,
a bit more technical questions that one can try to answer. For example, what
happens to our logic if a use of equalities/inequalities (free or uniform) or
constants is allowed.

## Acknowledgement

This work is supported by NCN grant No. 2021/41/B/ ST6/00996.

## References

  * [1]
  * [2] H. Andréka, J. van Benthem & I. Németi (1998): _Modal Languages and Bounded Fragments of Predicate Logic_.  Journal of Philosophical Logic 27, pp. 217–274, 10.1023/A:1004275029985.
  * [3] V. Bárány, B. ten Cate & L. Segoufin (2015): _Guarded Negation_.  J. ACM 62(3), p. 22, 10.1145/2701414.
  * [4] S. Benaim, M. Benedikt, W. Charatonik, E. Kieronski, R. Lenhardt, F. Mazowiecki & J. Worrell (2016): _Complexity of Two-Variable Logic on Finite Trees_.  ACM Trans. Comput. Log. 17(4), pp. 32:1–32:38, 10.1145/2996796.
  * [5] M. Bojańczyk, C. David, A. Muscholl, T. Schwentick & L. Segoufin (2011): _Two-variable logic on data words_.  ACM Trans. Comput. Log. 12(4), p. 27, 10.1145/1970398.1970403.
  * [6] M. Bojanczyk, A. Muscholl, T. Schwentick & L. Segoufin (2009): _Two-variable logic on data trees and XML reasoning_.  J. ACM 56(3), 10.1145/1516512.1516515.
  * [7] P. Bourhis, M. Morak & A. Pieris (2017): _Making Cross Products and Guarded Ontology Languages Compatible_.  In: IJCAI 2017, pp. 880–886, 10.24963/ijcai.2017/122.
  * [8] B. ten Cate & L. Segoufin (2013): _Unary negation_.  Logical Methods in Comp. Sc. 9(3), 10.2168/LMCS-9(3:25)2013.
  * [9] W. Charatonik & P. Witkowski (2013): _Two-Variable Logic with Counting and Trees_.  In: LICS 2013, pp. 73–82, 10.1109/LICS.2013.12.
  * [10] W. Charatonik & P. Witkowski (2015): _Two-variable Logic with Counting and a Linear Order_.  In: CSL 2015, LIPIcs 41, pp. 631–647, 10.4230/LIPIcs.CSL.2015.631.
  * [11] O. Fiuk & E. Kieroński (2023): _An excursion to the border of decidability: between two- and three-variable logic_.  In: LPAR 2023, EPiC Series in Computing 94, pp. 205–223, 10.29007/1xns.
  * [12] E. Grädel, P. Kolaitis & M. Y. Vardi (1997): _On the decision problem for two-variable first-order logic_.  Bulletin of Symbolic Logic 3(1), pp. 53–69, 10.2307/421196.
  * [13] E. Grädel, M. Otto & E. Rosen (1997): _Two-variable logic with counting is decidable_.  In: LICS 1997, pp. 306–317, 10.1109/LICS.1997.614957.
  * [14] L. Hella & A. Kuusisto (2014): _One-dimensional Fragment of First-order Logic_.  In: Proceedings of Advances in Modal Logic, 2014, pp. 274–293.  Available at http://www.aiml.net/volumes/volume10/Hella-Kuusisto.pdf.
  * [15] U. Hustadt & R. Schmidt (1999): _Maslov’s Class K Revisited_.  In: Automated Deduction — CADE-16, pp. 172–186, 10.1007/3-540-48660-7_12.
  * [16] Y. Kazakov (2006): _Saturation-based decision procedures for extensions of the guarded fragment_.  Ph.D. thesis, Universität des Saarlandes, Saarbrücken, Germany.
  * [17] E. Kieronski & A. Kuusisto (2014): _Complexity and Expressivity of Uniform One-Dimensional Fragment with Equality_.  In: MFCS 2014, Part I, Lecture Notes in Computer Science 8634, pp. 365–376, 10.1007/978-3-662-44522-8_31.
  * [18] E. Kieronski & A. Kuusisto (2015): _Uniform One-Dimensional Fragments with One Equivalence Relation_.  In: CSL 2015, LIPIcs 41, pp. 597–615, 10.4230/LIPIcs.CSL.2015.597.
  * [19] E. Kieronski, J. Michaliszyn, I. Pratt-Hartmann & L. Tendera (2014): _Two-Variable First-Order Logic with Equivalence Closure_.  SIAM J. Comput. 43(3), pp. 1012–1063, 10.1137/120900095.
  * [20] E. Kieroński & M. Otto (2012): _Small Substructures and Decidability Issues for First-Order Logic with Two Variables._ Journal of Symbolic Logic 77, pp. 729–765, 10.2178/jsl/1344862160.
  * [21] Emanuel Kieronski (2019): _One-Dimensional Guarded Fragments_.  In: MFCS 2019, LIPIcs 138, pp. 16:1–16:14, 10.4230/LIPIcs.MFCS.2019.16.
  * [22] Emanuel Kieronski & Sebastian Rudolph (2021): _Finite Model Theory of the Triguarded Fragment and Related Logics_.  In: LICS 2021, pp. 1–13, 10.1109/LICS52264.2021.9470734.
  * [23] Andreas Krebs, Kamal Lodaya, Paritosh K. Pandya & Howard Straubing (2020): _Two-variable logics with some betweenness relations: Expressiveness, satisfiability and membership_.  Log. Methods Comput. Sci. 16(3), 10.23638/LMCS-16(3:16)2020.
  * [24] Antti Kuusisto (2016): _On the Uniform One-dimensional Fragment_.  In: Description Logics 2016, CEUR Workshop Proceedings 1577\.
  * [25] H. R. Lewis (1980): _Complexity results for classes of quantificational formulas_.  Journal of Computer and System Sciences 21(3), pp. 317 – 353, 10.1016/0022-0000(80)90027-6.
  * [26] S. J. Maslov (1971): _The inverse method for establishing deducibility for logical calculi_.  The Calculi of Symbolic Logic I: Proceedings of the Steklov Institute of Mathematics 98\.
  * [27] M. Mortimer (1975): _On languages with two variables_.  Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 21, pp. 135–140, 10.1002/malq.19750210118.
  * [28] L. Pacholski, W. Szwast & L. Tendera (1997): _Complexity of two-variable logic with counting_.  In: LICS 1997, pp. 318–327, 10.1109/LICS.1997.614958.
  * [29] I. Pratt-Hartmann (2010): _The Two-Variable Fragment with Counting Revisited_.  In: WoLLIC 2010, pp. 42–54, 10.1007/978-3-642-13824-9_4.
  * [30] Ian Pratt-Hartmann (2015): _The two-variable fragment with counting and equivalence_.  Math. Log. Q. 61(6), pp. 474–515, 10.1002/malq.201400102.
  * [31] Ian Pratt-Hartmann (2021): _Fluted Logic with Counting_.  In: ICALP 2021, LIPIcs 198, pp. 141:1–141:17, 10.4230/LIPIcs.ICALP.2021.141.
  * [32] Ian Pratt-Hartmann, Wieslaw Szwast & Lidia Tendera (2019): _The Fluted Fragment Revisited_.  J. Symb. Log. 84(3), pp. 1020–1048, 10.1017/jsl.2019.33.
  * [33] W. V. Quine (1969): _On the limits of decision_.  In: Proceedings of the 14th International Congress of Philosophy, III, pp. 57–62.
  * [34] Sebastian Rudolph & Mantas Šimkus (2018): _The Triguarded Fragment of First-Order Logic_.  In: LPAR 2018, EPiC Series in Computing 57, pp. 604–619, 10.29007/m8ts.
  * [35] Dana Scott (1962): _A decision method for validity of sentences in two variables_.  Journal Symbolic Logic 27, p. 477.