1934 LABEL:LastPageApr. 11, 2022Jul. 12, 2023

*This work was partially supported by EGIDE/DAAD-Procope TAMTV. It is a considerably extended version of the first part of the extended abstract [HK15] from FoSSaCS 2015

[a] [b]

# On Presburger arithmetic extended
with non-unary counting quantifiers*

Peter Habermehl0000-0002-7982-0946  and  Dietrich Kuske  IRIF, Université
Paris Cité, France<EMAIL_ADDRESS>TU Ilmenau, Germany
<EMAIL_ADDRESS>
###### Abstract.

We consider a first-order logic for the integers with addition. This logic
extends classical first-order logic by modulo-counting, threshold-counting and
exact-counting quantifiers, all applied to tuples of variables (here, residues
are given as terms while moduli and thresholds are given explicitly). Our main
result shows that satisfaction for this logic is decidable in two-fold
exponential space. If only threshold- and exact-counting quantifiers are
allowed, we prove an upper bound of alternating two-fold exponential time with
linearly many alternations. This latter result almost matches Berman’s exact
complexity of first-order logic without counting quantifiers.

To obtain these results, we first translate threshold- and exact-counting
quantifiers into classical first-order logic in polynomial time (which already
proves the second result). To handle the remaining modulo-counting quantifiers
for tuples, we first reduce them in doubly exponential time to modulo-counting
quantifiers for single elements. For these quantifiers, we provide a
quantifier elimination procedure similar to Reddy and Loveland’s procedure for
first-order logic and analyse the growth of coefficients, constants, and
moduli appearing in this process. The bounds obtained this way allow to
restrict quantification in the original formula to integers of bounded size
which then implies the first result mentioned above.

Our logic is incomparable with the logic considered by Chistikov et al. in
2022. They allow more general counting operations in quantifiers, but only
unary quantifiers. The move from unary to non-unary quantifiers is non-
trivial, since, e.g., the non-unary version of the Härtig quantifier results
in an undecidable theory.

###### Key words and phrases:

Presburger arithmetic, quantifier elimination, counting quantifiers, non-unary
quantifiers, decision procedure

The authors thank Christian Schwarz from TU Ilmenau for proofreading the paper
and for correcting two mistakes. They also thank the reviewers of this paper
for pointing to some inaccuracies.

##  1\. Introduction

Presburger arithmetic is the first-order theory of the structure
${\mathcal{Z}}$, i.e., the integers with addition, comparison, binary
relations $\equiv_{k}$ (standing for equality modulo $k$) for all $k\geqslant
2$, and all constants $c\in{\mathbb{Z}}$. Presburger [Pre30] developed a
quantifier elimination procedure for this theory and therefore showed its
decidability. The upper complexity bounds of three-fold exponential time
[Opp78] and of two-fold exponential space [FR79] have been shown before Berman
[Ber80] proved the exact complexity to be two-fold exponential alternating
time with linearly many alternations. Further results in this direction
concern the complexity of fragments of Presburger arithmetic [RL78, Grä88,
Sch97, Haa14].

Classical first-order logic can be extended by allowing further quantifiers
besides $\exists$ and $\forall$. One such quantifier was introduced by Härtig
in [Här62] and is therefore known as Härtig quantifier (usually denoted $I$,
cf. [HKPV91] for a survey on this Härtig quantifier). The formula
$Ix\colon\bigl{(}\varphi(x),\psi(x)\bigr{)}$ expresses the equality of the
number of witnesses $x$ for $\varphi(x)$ and for $\psi(x)$, resp. Apelt, in
[Ape66], considered this extension $\mathrm{FO}[Ix]$ of classical first-order
logic for the structure of integers with addition. He provides a system of
axioms and derivation rules whose completeness he proves using a quantifier
elimination. Since the system of axioms and the derivation relation are
decidable, he infers that the $\mathrm{FO}[Ix]$-theory of the integers with
addition is decidable. Alternatively, this decidability follows since Apelt’s
quantifier elimination is effective and the truth of quantifier free
statements is decidable.

Another possibility of extending classical first-order logic was considered by
Schweikardt [Sch05] who added the threshold-counting quantifier
$\exists^{\geqslant t}x$ (here, $t$ is a term, $x$ a variable, and the formula
$\exists^{\geqslant t}x\,\varphi$ says “there are at least $t$ witnesses $x$
for the formula $\varphi$”); it is not difficult to see that this extension
$\mathrm{FO}[\exists^{\geqslant t}x]$ is equally expressive as Apelt’s
extension $\mathrm{FO}[Ix]$. She provided an effective quantifier elimination
procedure for the quantifier $\exists^{\geqslant t}x$ implying the
decidability. An alternative quantifier elimination for
$\mathrm{FO}[\exists^{\geqslant t}x]$ was given by Chistikov et al. [CHM21,
CHM22].

It should be noted that we do not know any elementary upper bounds for the
quantifier elimination procedures from [Ape66, Sch05, CHM21, CHM22] for the
logics $\mathrm{FO}[Ix]$ and $\mathrm{FO}[\exists^{\geqslant t}x]$.
Consequently, no elementary upper bounds for the respective theories of the
integers are known.

In our earlier conference paper [HK15], we obtained such an elementary upper
bound for the logic $\mathrm{FO}[\exists^{(q,p)}x]$ (here, $q$ and $p$ stand
for natural numbers, $x$ for a variable, and a formula of the form
$\exists^{(q,p)}x\,\varphi$ expresses “the number of witnesses $x$ for
$\varphi$ is congruent to $q$ modulo $p$”). More precisely, we presented a
quantifier elimination procedure for this logic, analysed the size of
coefficients, constants, and moduli appearing in the resulting formula, and
inferred that quantification can be bounded to integers of at most triply-
exponential absolute value; as a result, the theory can be decided in doubly
exponential space which matches the best known upper bound for Presburger
arithmetic using deterministic Turing machines. Extending Klaedtke’s automata-
based decision procedure for Presburger arithmetic [Kla08], our conference
paper also contains an automata-based decision procedure for this logic that
runs in triply exponential time (which is the optimal time bound known for
deterministic Turing machines [Opp78]).

In [CHM22], Chistikov et al. analysed their quantifier elimination procedure
for the logic $\mathrm{FO}[\exists^{\geqslant t}x]$. For two fragments, called
“$F$” and “monadically guarded PAC”, respectively, they obtained elementary
upper bounds for the decision problems. The following results follow since the
two logics are contained in the two named fragments.

  * •

The $\mathrm{FO}[\exists^{(t,p)}x,\exists^{\geqslant
c}x,\exists^{=c}x]$-theory of the integers is decidable in doubly exponential
space (here, $t$ stands for a term, $p$ and $c$ for natural numbers, and $x$
for a variable).

  * •

The $\mathrm{FO}[\exists^{\geqslant c}x,\exists^{=c}x]$-theory of the integers
can be decided by an alternating Turing machine using doubly exponential time
and linearly many alternations (in this logic, no modulo-counting quantifiers
are allowed and the thresholds are given explicitly). More precisely, the
number of alternations is not only bounded by the _length_ , but even by the
_depth_ of the formula.

These two upper bounds coincide with the best known upper bounds for
Presburger arithmetic wrt. deterministic and alternating Turing machines,
resp.

It should be noted that all logics considered so far extend classical first
order logic by _unary_ quantifiers, i.e., the quantifiers $I$,
$\exists^{\geqslant t}$, and $\exists^{(t,p)}$ bind a single variable. They
can easily be extended to bind tuples of variables, e.g., the formula

$I(x^{\prime},y^{\prime})\colon\bigl{(}(x^{\prime}=0\land 0\leqslant
y^{\prime}<z),(0\leqslant x^{\prime}<x\land 0\leqslant y^{\prime}<y)\bigr{)}$

expresses that the number $z$ of pairs $(0,y^{\prime})$ satisfying $0\leqslant
y^{\prime}<z$ equals the number $x\cdot y$ of pairs $(x^{\prime},y^{\prime})$
satisfying $0\leqslant x^{\prime}<x$ and $0\leqslant y^{\prime}<y$, i.e.,
$z=x\cdot y$. Hence, allowing this non-unary Härtig quantifier $I\overline{x}$
leads to an undecidable theory, the resulting logic
$\mathrm{FO}[I\overline{x}]$ does not possess effective quantifier
elimination, and the same applies for the non-unary version of the threshold-
counting quantifier $\exists^{\geqslant t}\overline{x}$. Chistikov et al. ask
in the introduction of [CHM21] whether non-unary counting quantifiers
$\exists^{\geqslant c}\overline{x}$ and $\exists^{=c}\overline{x}$ lead to
(efficiently) decidable theories. In this paper, we answer this question in
the affirmative proving that the non-unary versions of the quantifiers
$\exists^{(t,p)}\overline{x}$, $\exists^{\geqslant c}\overline{x}$, and
$\exists^{\geqslant c}\overline{x}$ (where the threshold is given explicitly)
behave much better than Härtig’s quantifier $I$. Namely, we prove the two
complexity bounds that follow from the work by Chistikov et al. on the
fragments “$F$” and “monadically guarded PAC” also for the non-unary
quantifiers:

  * •

The $\mathrm{FO}[\exists^{(t,p)}\overline{x},\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}]$-theory of the integers is decidable
in doubly exponential space (here, $t$ stands for a term, $p$ and $c$ for
natural numbers, and $\overline{x}$ for a tuple of variables).

  * •

The $\mathrm{FO}[\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}]$-theory of the integers can be
decided by an alternating Turing machine using doubly exponential time and
linearly many alternations. As opposed to the above mentioned result on the
unary versions of these quantifiers, we cannot prove that the number of
alternations is bounded by the depth of the formula.

Despite the similarity of results, we cannot follow the route of proof used by
Chistikov et al. since they start from their handling of the unary Härtig
quantifier which cannot be extended to its non-unary version. Differently, we
proceed as follows.

  1. (1)

In polynomial time, we compute from a formula in the full logic
$\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x},\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}\bigr{]}$ an equivalent formula in the
fragment $\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x}]$, that is, non-unary
threshold- and exact-counting quantifiers can be eliminated in polynomial
time. This procedure does not introduce new modulo-counting quantifiers;
consequently, from a formula from $\mathrm{FO}[\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}]$, it computes an equivalent formula
from classical first-order logic $\mathrm{FO}$. Since the “block depth” (a
notion defined later, it is bounded by the length of the formula) of the
resulting formula is linear in the size of the original one, we obtain that
the satisfaction relation for $\mathrm{FO}[\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}]$ is decidable in two-fold exponential
alternating time with $O(n)$ many alternations. Note that this is very close
to Berman’s optimal result for $\mathrm{FO}$ where only $n$ alternations are
necessary [Ber80].

  2. (2)

We provide a quantifier elimination procedure for the logic
$\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x}]$ and therefore, by the first
result, for the full logic
$\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x},\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}\bigr{]}$. It follows that this full
logic agrees in expressive power with classical first-order logic
$\mathrm{FO}$.

  3. (3)

Analysing the size of constants, coefficients, and moduli appearing in this
procedure, we can restrict quantification to integers of bounded size. As a
result, we get a decision procedure in two-fold exponential space for the full
logic $\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x},\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}\bigr{]}$. Note that this equals the
best known upper bound using Turing machines for classical first-order logic
$\mathrm{FO}$ from [FR79].

##  2\. Preliminaries

We consider $0$ a natural number.

#### The structure

The universe of the structure ${\mathcal{Z}}$ is the set of integers
${\mathbb{Z}}$. On this set, we consider the constants $c\in{\mathbb{Z}}$, the
binary function $+$, the binary relation $<$, and the binary relations
$\equiv_{k}$ for $k\geqslant 2$ (with $m\equiv_{k}n$ iff $k$ divides $m-n$).

#### Terms and assignments

We will use the countable set $\\{x_{i}\mid i\in{\mathbb{N}}\\}$ of variables.
_Terms_ are defined by induction: $x_{i}$ and $c$ are terms for
$i\in{\mathbb{N}}$ and $c\in{\mathbb{Z}}$, and $as$ and $s+t$ are terms
whenever $a\in{\mathbb{Z}}$ and $s$ and $t$ are terms (we write $-s$ for the
term $(-1)\cdot s$ and $s-t$ for $s+(-1)\cdot t$).

An _assignment_ is a function $f\colon\\{x_{i}\mid
i\in{\mathbb{N}}\\}\to{\mathbb{Z}}$ that assigns integers to variables. In a
natural way, an assignment $f$ is extended to a function (also denoted $f$)
that maps terms to integers. Two terms $s$ and $t$ are _equivalent_ if
$f(s)=f(t)$ holds for all assignments $f$; we write $s\Leftrightarrow t$ to
denote that $s$ and $t$ are equivalent.111Usually, one writes $s\equiv t$ for
the equivalence of terms and formulas, but this might lead to confusion in
this paper because of the central role of the relations $\equiv_{k}$ for
$k\geqslant 2$.

A term is in _normal form_ if it is of the form
$t^{\prime}=\bigl{(}\cdots(a_{1}x_{i_{1}}+a_{2}x_{i_{2}})+\cdots
a_{n}x_{i_{n}}\bigr{)}+c$ with $i_{1}<i_{2}<\cdots<i_{n}$,
$a_{1},\dots,a_{n}\neq 0$, and $c\in{\mathbb{Z}}$. Note that, for any term
$t$, there exists a unique equivalent term in normal form. For a term $t$ with
normal form $t^{\prime}$, we call $a_{j}$ the coefficient of $x_{i_{j}}$ and
$c$ the constant; note that coefficients are non-zero, but the constant can be
zero (in which case we call the term $t$ _constant-free_).

If the normal form of a term $t$ does not contain the variable $x_{i}$, then
we call $t$ an _$x_{i}$ -free term_.

#### Atomic formulas

Expressions of the form $s<t$ (also written $t>s$) and $s\equiv_{k}t$ for
terms $s$ and $t$ and a natural number $k\geqslant 1$ are called _atomic
formulas_. We extend an assignment $f$ to a function (also denoted $f$) that
maps atomic formulas to the truth values $\mathrm{t\\!t}$ and
$\mathrm{f\\!f}$: $f(s<t)=\mathrm{t\\!t}$ iff $f(s)<f(t)$ and
$f(s\equiv_{k}t)=\mathrm{t\\!t}$ iff $k$ divides $f(s)-f(t)=f(s-t)$. Two
atomic formulas $\alpha$ and $\beta$ are _equivalent_ if $f(\alpha)=f(\beta)$
holds for all assignments $f$; we write $\alpha\Leftrightarrow\beta$ for this
fact.

Let $x$ be a variable. An atomic formula $\varphi$ is _$x$ -separated_ if
there are an $x$-free term $t$ and a non-negative integer $a\in{\mathbb{N}}$
such that $\varphi$ is of the form $ax<t$, $t<ax$, or $ax\equiv_{k}t$. If $t$
is an $x$-free term, then, e.g., the formula $0x\equiv_{k}t$ is $x$-separated.
Since $0$ is the normal form of $0x$, also the formulas $0\equiv_{k}t$, $0<t$,
and $t<0$ are considered to be $x$-separated (despite the fact that it does
not mention $x$ at all). It follows that, for any atomic formula $\alpha$ and
any variable $x$, there exists an equivalent $x$-separated atomic formula.

An atomic formula is _constant separated_ if it is of the form $c<s$, $s<c$,
or $s\equiv_{k}c$ where $s$ is a constant-free term and $c\in{\mathbb{Z}}$ a
constant. Again, for any atomic formula $\alpha$, there exists an equivalent
constant separated atomic formula.

#### Formulas

Formulas of classical first-order logic are built from atomic formulas using
the quantifier $\exists$ (applied to single variables) and the Boolean
combinators negation, conjunction, implication, and equivalence. We extend
this classical logic by quantifiers that allow _threshold-_ ($\exists^{\geq
c}$) and _exact-counting_ ($\exists^{=c}$) as well as _modulo counting_
($\exists^{(t,p)}$), all applied to _tuples_ of variables. _Formulas_ of the
logic $\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x},\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}\bigr{]}$ are defined by induction:

  1. (1)

Any atomic formula is a formula.

  2. (2)

If $\varphi$ and $\psi$ are formulas, then so are $\lnot\varphi$,
$\varphi\land\psi$, $\varphi\lor\psi$, $\varphi\to\psi$ and
$\varphi\leftrightarrow\psi$.

  3. (3)

If $\varphi$ is a formula and $y$ a variable, then $\exists y\colon\varphi$ is
a formula.

  4. (4)

If $\varphi$ is a formula, $t$ a term, $y_{1},\dots,y_{\ell}$ (with
$\ell\geqslant 1$) distinct variables, and $p\geqslant 2$ a natural number,
then $\exists^{(t,p)}(y_{1},\dots,y_{\ell})\colon\varphi$ is a formula.

  5. (5)

If $\varphi$ is a formula, $y_{1},\dots,y_{\ell}$ (with $\ell\geqslant 1$) are
distinct variables, and $c\geqslant 1$ is a natural number, then
$\exists^{\geqslant c}(y_{1},\dots,y_{\ell})\colon\varphi$ and
$\exists^{=c}(y_{1},\dots,y_{\ell})\colon\varphi$ are formulas.

The size $|\varphi|$ of a formula $\varphi$ is the amount of space needed to
write it down (we assume integers to be written in binary and variables to
have size one).

For certain fragments of the logic
$\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x},\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}\bigr{]}$ we use the following naming
scheme.

  * •

$\mathrm{FO}[\cdots,\exists^{(t,p)}\overline{x}\cdots]$ denotes that item (4)
can be used in the construction of formulas without any restriction.
$\mathrm{FO}[\cdots,\exists^{(q,p)}\overline{x}\cdots]$ limits the use of item
(4) to the case that $t$ is a constant from ${\mathbb{N}}$ (and not an
arbitrary term), and $\mathrm{FO}[\cdots,\exists^{(q,p)}x\cdots]$ requires, in
addition, that (4) is only used with $\ell=1$, i.e., we can use the unary
modulo-counting quantifiers with constant residue, only.

  * •

$\mathrm{FO}[\cdots,\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}\cdots]$ denotes that item (5) can be
used in the construction of formulas without any restriction. Similarly to the
above, $\mathrm{FO}[\cdots,\exists^{\geqslant c}x,\exists^{=c}x\cdots]$
restricts the use of item (5) to the case $\ell=1$, i.e., we can use the unary
threshold- and exact-counting quantifiers, only.

######  Remark 1.

The logics $\mathrm{FO}[\exists^{\geqslant c}x,\exists^{=c}x]$,
$\mathrm{FO}\bigl{[}\exists^{(q,p)}x]$, and
$\mathrm{FO}[\exists^{(q,p)}x,\exists^{\geqslant c}x,\exists^{=c}x]$ are often
denoted $\mathrm{C}$, $\mathrm{FO}{+}\mathrm{MOD}$ and $\mathrm{C{+}MOD}$,
respectively.

We can further extend an assignment $f$ in the standard way to a function
(also denoted $f$) that maps formulas to the truth values $\mathrm{t\\!t}$ and
$\mathrm{f\\!f}$.

Before we define the semantics of quantified formulas, we need the following
definitions. For $\ell\geqslant 1$, $\overline{y}=(y_{1},\dots,y_{\ell})$ an
$\ell$-tuple of distinct variables, and
$\overline{a}=(a_{1},\dots,a_{\ell})\in{\mathbb{Z}}^{\ell}$, we let
$f_{\overline{y}/\overline{a}}$ be the assignment that maps the variable
$y_{i}$ to the value $a_{i}$ (for all $1\leqslant i\leqslant\ell$) and, apart
from this, coincides with the assignment $f$. In other words,
$f_{\overline{y}/\overline{a}}(y_{i})=a_{i}$ for all $1\leqslant
i\leqslant\ell$ and $f_{\overline{y}/\overline{a}}(x)=f(x)$ for all variables
$x\notin\\{y_{1},\dots,y_{\ell}\\}$.

To define the semantics of the quantifiers, let $\varphi$ be a formula, $t$ a
term, $y_{1},\dots,y_{\ell}$ distinct variables, $p\geqslant 2$, and
$c\geqslant 1$. With $\overline{y}=(y_{1},\dots,y_{\ell})$, we then define the
following:

  * •

$f\bigl{(}\exists y_{1}\colon\varphi\bigr{)}=\mathrm{t\\!t}$ iff there exists
$a\in{\mathbb{Z}}$ such that $f_{y_{1}/a}(\varphi)=\mathrm{t\\!t}$.

  * •

$f\bigl{(}\exists^{(t,p)}\overline{y}\colon\varphi\bigr{)}=\mathrm{t\\!t}$ iff
the set $\\{\overline{a}\in{\mathbb{Z}}^{\ell}\mid
f_{\overline{y}/\overline{a}}(\varphi)=\mathrm{t\\!t}\\}$ is finite and

$\Bigl{|}\bigl{\\{}\overline{a}\in{\mathbb{Z}}^{\ell}\colon
f_{\overline{y}/\overline{a}}(\varphi)=\mathrm{t\\!t}\bigr{\\}}\Bigr{|}\equiv_{p}f(t)\,.$

In other words, the formula $\exists^{(t,p)}\overline{y}\colon\varphi$
expresses that the number of witnessing tuples $\overline{y}$ for $\varphi$ is
(modulo $p$) congruent to the value of the term $t$.

  * •

$f\bigl{(}\exists^{\geqslant
c}\overline{y}\colon\varphi\bigr{)}=\mathrm{t\\!t}$ iff

$\Bigl{|}\bigl{\\{}\overline{a}\in{\mathbb{Z}}^{\ell}\colon
f_{\overline{y}/\overline{a}}(\varphi)=\mathrm{t\\!t}\bigr{\\}}\Bigr{|}\geqslant
c\,.$

In other words, the formula $\exists^{\geqslant c}\overline{y}\colon\varphi$
expresses that the number of witnessing tuples $\overline{y}$ for $\varphi$ is
at least $c$ (and possibly infinite). With $\ell=1$, $\exists^{\geqslant 1}$
is the usual existential quantifier $\exists$. This easy observation allows us
to consider $\exists$ as an abbreviation and therefore to skip item (3) in the
definition of fragments of the full logic
$\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x},\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}\bigr{]}$, provided item (5) is allowed
with $\ell=1$.

  * •

$f\bigl{(}\exists^{=c}\overline{y}\colon\varphi\bigr{)}=\mathrm{t\\!t}$ iff
$\bigl{|}\\{\overline{a}\in{\mathbb{Z}}^{\ell}\mid
f_{\overline{y}/\overline{a}}(\varphi)=\mathrm{t\\!t}\\}\bigr{|}=c$.

Two formulas $\alpha$ and $\beta$ are _equivalent_ if $f(\alpha)=f(\beta)$
holds for all assignments $f$; we write $\alpha\Leftrightarrow\beta$ for this
fact.

Clearly, the formula $\exists^{=c}\overline{y}\colon\varphi$ is equivalent to
$\exists^{\geqslant c}\overline{y}\colon\varphi\land\lnot\exists^{\geqslant
c+1}\overline{y}\colon\varphi$, i.e., we can eliminate any occurrence of
$\exists^{=c}$ without changing the semantics of a formula. But this
elimination may increase the size of the formula exponentially.

Note that $f(s<t\lor s>t)=\mathrm{t\\!t}$ iff $f(s)\neq f(t)$ since $<$ is a
strict linear order on the set ${\mathbb{Z}}$. Therefore, we will write $s=t$
as abbreviation of the formula $\lnot(s<t\lor s>t)$. Similarly, $s\leqslant t$
stands for $\lnot s>t$ and sequences of comparisons like $s_{1}\leqslant
s_{2}\leqslant s_{3}$ denote the conjunction $s_{1}\leqslant s_{2}\land
s_{2}\leqslant s_{3}$. Similarly, we write $\forall x\,\varphi$ as
abbreviation for $\lnot\exists x\,\lnot\varphi$.

We define the quantifier-depth $\mathrm{qd}(\varphi)$ of formulas
$\varphi\in\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x},\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}\bigr{]}$ by induction:

  * •

If $\varphi$ is an atomic formula, then $\mathrm{qd}(\varphi)=0$.

  * •

If $\varphi=\lnot\alpha$, then $\mathrm{qd}(\varphi)=\mathrm{qd}(\alpha)$.

  * •

If
$\varphi\in\\{\alpha\land\beta,\alpha\lor\beta,\alpha\to\beta,\alpha\leftrightarrow\beta\\}$,
then
$\mathrm{qd}(\varphi)=\max\bigl{\\{}\mathrm{qd}(\alpha),\mathrm{qd}(\beta)\bigr{\\}}$.

  * •

If $\varphi=\exists x\colon\alpha$, then
$\mathrm{qd}(\varphi)=1+\mathrm{qd}(\alpha)$.

  * •

If $\varphi$ is any of the formulas $\exists^{\geqslant
c}(y_{1},\dots,y_{\ell})\colon\alpha$,
$\exists^{=c}(y_{1},\dots,y_{\ell})\colon\alpha$, or
$\exists^{(t,p)}(y_{1},\dots,y_{\ell})\colon\alpha$, then
$\mathrm{qd}(\varphi)=\ell+\mathrm{qd}(\alpha)$.

Note that the quantifier depth depends on the length of tuples of variables
that follow a quantifier, i.e., it increases by $\ell$ whenever we prepend a
quantifier $\exists^{\dots}(y_{1},\dots,y_{\ell})$ to a formula.

The overall goal of this paper is to obtain an elementary decision procedure
for the full logic
$\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x},\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}\bigr{]}$. As a first step, we will
transform a formula $\alpha$ from
$\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x},\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}\bigr{]}$ into an equivalent formula
$\beta$ from $\mathrm{FO}\bigl{[}\exists^{(q,p)}x]$, that will later be
transformed into an equivalent quantifier-free formula $\gamma$. To control
the form of the resulting formulas $\beta$ and $\gamma$, we define the
following sets.

Let
$\varphi\in\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x},\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}\bigr{]}$ be a formula. Then
$\textsc{Coeff}(\varphi)\subseteq{\mathbb{Z}}$ is the set of integers $0,\pm
1,\pm 2$ and $\pm a$ where $a$ is a coefficient in the term $s_{1}-s_{2}$ for
some atomic formula $s_{1}<s_{2}$ from $\varphi$. Similarly,
$\textsc{Const}(\varphi)\subseteq{\mathbb{Z}}$ is the set of integers $0,\pm
1$, $\pm 2$, and $\pm c$ where $c$ is the constant term in $s_{1}-s_{2}$ for
some atomic formula $s_{1}<s_{2}$ from $\varphi$.

The set $\textsc{Mod}(\varphi)\subseteq{\mathbb{N}}$ contains $1$ and all
integers $k\geqslant 1$ such that an atomic formula of the form
$s_{1}\equiv_{k}s_{2}$ or some quantifier $\exists^{(t,k)}$ appears in
$\varphi$. Finally,
$\mathbf{P}(\varphi)=\textsc{Coeff}(\varphi)\cup\textsc{Mod}(\varphi)$.

Consider the following formula $\varphi$:

$\displaystyle\exists^{(17x+25,23)}(y_{1},y_{2})\colon 2y_{1}<3y_{2}\land
4y_{2}<56$ $\displaystyle\land$ $\displaystyle\exists^{\geqslant
343}y\colon{-}13x+2<3x+y-2\land 57x\equiv_{13}2y+27$

Then we have

$\displaystyle\textsc{Coeff}(\varphi)$ $\displaystyle=\\{0,\pm 1,\pm 2,\pm
3,\pm 4,\pm 16\\}\,,$ $\displaystyle\textsc{Const}(\varphi)$
$\displaystyle=\\{0,\pm 1,\pm 2,\pm 56,\pm 4\\}\,$
$\displaystyle\textsc{Mod}(\varphi)$ $\displaystyle=\\{1,13,23\\}\,,\text{
and}$ $\displaystyle\mathbf{P}(\varphi)$ $\displaystyle=\\{0,\pm 1,\pm 2,\pm
3,\pm 4,\pm 16,23,13\\}\,.$

Note that $\textsc{Coeff}(\varphi)$ and $\textsc{Const}(\varphi)$ depend on
subformulas of the form $s<t$, but not on subformulas of the form
$s\equiv_{k}t$. On the other hand, $\textsc{Mod}(\varphi)$ only depends on
subformulas of the form $s\equiv_{k}t$ and on the moduli $k$ of modulo-
counting quantifiers $\exists^{(t,k)}$ appearing in $\varphi$.

###  2.1. An excursion into Presburger arithmetic

Berman proved in [Ber80] that Presburger arithmetic is complete for the class
STA$(*,2^{2^{O(n)}},n)$ of all problems that can be solved by an alternating
Turing machine in doubly exponential time with $n$ alternations. Here, we are
mainly interested in the proof of the upper bound. He presents this proof in a
very sketchy way essentially saying that Ferrante and Rackoff have shown in
[FR79] that quantification can be reduced to integers of at most triply
exponential size (which can be represented in doubly exponential space). It
should be noted that this latter result holds for any formula, no matter
whether it is in prenex normal form or it contains the Boolean connective
$\leftrightarrow$. Berman’s result actually means that the algorithm by
Ferrante and Rackoff can be implemented on an alternating Turing machine with
the above time and alternation bound. Looking into the algorithm from [FR79],
one sees that the formula is first transformed into prenex normal form and
that then, the alternation of the Turing machine equals the quantifier
alternation depth of the resulting formula. Note that turning a formula into
prenex normal form is possible in polynomial time whenever the Boolean
connectives are restricted to $\lnot$, $\lor$, $\land$, and $\to$. Differently
here, we also allow the connective $\leftrightarrow$ which gives a convenient
way to write certain formulas succinctly. But in the presence of this
connective, we do not know how to compute equivalent formulas in prenex normal
form in polynomial time.

For later reference, we now sketch a proof that, also in the presence of
$\leftrightarrow$, Berman’s upper bound holds. Since the computation of prenex
normal forms is too costly, we need another bound for the alternation. To this
aim, we define the _block depth_ of a formula. Intuitively, the block depth
$\mathrm{bd}^{\mathrm{FO}}(\alpha)$ of the formula $\alpha\in\mathrm{FO}$
bounds the number of blocks of existential quantifiers along any path in the
syntax tree of $\alpha$.

  * •

$\mathrm{BD}^{\mathrm{FO}}_{0}$ is the set of atomic formulas.

  * •

For $n\geqslant 1$, the set $\mathrm{BD}^{\mathrm{FO}}_{n}$ contains the
formulas of the form $\exists x_{1}\,\exists x_{2}\,\dots\,\exists
x_{m}\colon\beta$ where $m\geqslant 0$ and $\beta$ is a Boolean combination
(possibly using $\lnot$, $\land$, $\lor$, $\to$, and $\leftrightarrow$) of
formulas from $\mathrm{BD}^{\mathrm{FO}}_{n-1}$.

  * •

The _block depth_ $\mathrm{bd}^{\mathrm{FO}}(\alpha)$ of a formula
$\alpha\in\mathrm{FO}$ is the minimal natural number $n$ with
$\alpha\in\mathrm{BD}^{\mathrm{FO}}_{n}$.

Note that the block depth of any formula is at most half of its depth (which
is the maximal length of a branch in the syntax tree) and therefore half of
its length.

With this definition in place, we can now formulate Berman’s upper bound for
first-order logic in presence of the Boolean connective $\leftrightarrow$.

######  Theorem 2.

There is an alternating Turing machine that, on input of a closed formula
$\varphi\in\mathrm{FO}$, decides in time doubly exponential in $|\varphi|$
with $2\,\mathrm{bd}^{\mathrm{FO}}(\varphi)\leqslant|\varphi|$ alternations
whether $\varphi$ holds or not.

######  Proof 2.1 (Proof sketch).

The alternating algorithm runs as follows:

  * •

If $\varphi$ is atomic, then validity of the closed formula $\varphi$ is
checked deterministically.

  * •

Now let $\varphi=\exists x_{1}\dots\exists x_{m}\colon\psi$ where $\psi$ is a
Boolean combination of formulas $\sigma_{1},\dots,\sigma_{\ell}$ of block
depth at most $n$. Then the alternating algorithm first guesses $m$ integers
$k_{1},\dots,k_{m}$ of bounded size (which suffices by [FR79]) as well as a
set $X\subseteq\\{1,2,\dots,\ell\\}$. Then, it branches universally checking
that

    1. (1)

the Boolean combination $\psi$ holds while assuming $X$ is the set of indices
$i$ such that $\sigma_{i}(k_{1},\dots,k_{m})$ holds,

    2. (2)

for all $i\in X$, the closed formula $\sigma_{i}(k_{1},\dots,k_{m})$ holds,
and

    3. (3)

for all $j\in\\{1,2,\dots,\ell\\}\setminus X$, the closed formula
$\sigma_{j}(k_{1},\dots,k_{m})$ does not hold.

Thus, the algorithm first branches existentially and then universally before
checking whether the corresponding formulas $\sigma_{i}$ of block depth
$\leqslant n$ hold or not.

##  3\. Existential and unary modulo-counting quantifiers suffice

In this section, we will transform a formula from
$\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x},\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}\bigr{]}$ into an equivalent one from
$\mathrm{FO}\bigl{[}\exists^{(q,p)}x]$. Note that the logic
$\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x}]$ is an intermediate logic
between these two logics:

  * •

In the logic
$\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x},\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}\bigr{]}$, we can use the non-unary
threshold- and exact-counting quantifiers $\exists^{\geqslant
c}(x_{1},\dots,x_{\ell})$ and $\exists^{=c}(x_{1},\dots,x_{\ell})$ while
$\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x}]$ does not allow threshold-
and exact-counting quantification.

  * •

$\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x}]$ allows non-unary modulo-
counting quantifiers $\exists^{(t,p)}(x_{1},\dots,x_{\ell})$ with $t$ an
arbitrary term while $\mathrm{FO}\bigl{[}\exists^{(q,p)}x]$ allows only unary
modulo-counting quantification of the form $\exists^{(q,p)}x$ with
$q\in{\mathbb{N}}$.

We will transform a formula from
$\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x},\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}\bigr{]}$ first into an equivalent
formula from $\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x}]$, i.e., we will
eliminate threshold counting quantifiers. In a second step, the resulting
formula from $\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x}]$ will be
translated into an equivalent one from $\mathrm{FO}\bigl{[}\exists^{(q,p)}x]$,
i.e., we will eliminate non-unary modulo-counting quantifiers as well as terms
as residue. Both these transformations will leave the sets of coefficients,
constants, and moduli unchanged; the first transformation will be done in
polynomial time while the second one uses doubly exponential time.

###  3.1. Elimination of threshold- and exact-counting quantifiers

Here, we give the transformation from
$\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x},\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}\bigr{]}$ to
$\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x}]$. We will provide a
polynomial-time transformation that does not change the sets Coeff, Const, and
Mod. In addition, this transformation will not introduce new modulo-counting
quantifiers so that formulas from $\mathrm{FO}[\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}]$ get translated into equivalent
formulas $\varphi$ from first-order logic222Stefan Göller (private
communication) explained to us a polynomial translation of formulas from
$\mathrm{FO}[\exists^{\geqslant c}x]$ to $\mathrm{FO}$. The work in this
section is an extension and elaboration of his idea. whose validity can then
be checked using Theorem 2.

We now come to the translation, i.e., to the elimination of threshold- and
exact-counting quantifiers for tuples. First note that the formulas
$\exists^{=c}\overline{y}\colon\varphi$ and $\exists^{\geqslant
c}\overline{y}\colon\varphi\land\lnot\exists^{\geqslant
c+1}\overline{y}\colon\varphi$ are clearly equivalent, i.e., semantically,
there is no need for the exact-counting quantifier $\exists^{=c}$. But
applying this replacement to all exact-counting quantifiers in a formula
increases the size of the formula exponentially. Similarly,
$\exists^{\geqslant c}\overline{y}\colon\varphi$ is equivalent to

$\displaystyle\exists\overline{y_{1}}\,\exists\overline{y_{2}}\,\dots\,\exists\overline{y_{c}}\colon$
$\displaystyle\bigwedge_{1\leqslant i<j\leqslant
c}\lnot\overline{y_{i}}=\overline{y_{j}}$
$\displaystyle\land\forall\overline{y}\colon\biggl{(}\Bigl{(}\bigvee_{1\leqslant
i\leqslant c}\overline{y}=\overline{y_{i}}\Bigr{)}\to\varphi\biggr{)}$

(where $(y^{1},y^{2},\dots,y^{\ell})=(y_{i}^{1},\dots,y_{i}^{\ell})$
abbreviates $\bigwedge_{1\leqslant j\leqslant\ell}y^{j}=y^{j}_{i}$). Since the
constant $c$ is written in binary, already the prefix of existential
quantifiers is of exponential length, i.e., also this transformation incurs an
exponential blow-up in formula size. Finally note that the non-unary
quantifiers $\exists\overline{y}$ and $\forall\overline{y}$ are equivalent to
$\exists y^{1}\,\exists y^{2}\cdots\exists y^{\ell}$ and $\forall
y^{1}\,\forall y^{2}\cdots\forall y^{\ell}$, respectively.

Thus, we saw that any formula from
$\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x},\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}\bigr{]}$ can be transformed into an
equivalent one from $\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x}]$ (and
similarly for $\mathrm{FO}[\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}]$ and $\mathrm{FO}$), but at the cost
of an exponential size increase. Our first result shows that this size
increase can be avoided.

The crucial part in this construction is the elimination of a threshold- or
exact-counting quantifier in front of a formula from
$\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x}]$ or from $\mathrm{FO}$,
respectively. This construction adapts a binary search strategy. For instance,
the formula $\exists^{=2c}y\colon y_{0}\leqslant y<y_{1}\land\varphi(y)$
expresses that the interval333All intervals in this paper are considered as
sets of integers or of tuples of integers. $[y_{0},y_{1})$ contains precisely
$2c$ many numbers $y$ satisfying $\varphi$. This is equivalent to saying that
there exists some number $y_{\frac{1}{2}}$ in the said interval such that both
intervals $[y_{0},y_{\frac{1}{2}})$ and $[y_{\frac{1}{2}},y_{1})$ contain
precisely $c$ numbers satisfying $\varphi$. The constructed formula then
contains the conjunction of the two formulas
$\exists^{=c}y\colon\bigl{(}y_{0}\leqslant
y<y_{\frac{1}{2}}\land\varphi(y)\bigr{)}$ and
$\exists^{=c}y\colon\bigl{(}y_{\frac{1}{2}}\leqslant
y<y_{1}\land\varphi(y)\bigr{)}$. Therefore, using this binary-search idea
alone does not prevent an exponential blow-up. The solution is to replace the
conjunction of these two formulas by an expression of the form

$\forall
a,b\colon\Bigl{(}(a,b)\in\\{(y_{0},y_{\frac{1}{2}}),(y_{\frac{1}{2}},y_{1})\\}\to\exists^{=c}y\colon\bigl{(}a\leqslant
y<b\land\varphi(y)\bigr{)}\Bigr{)}\,.$

This idea (known as Fischer-Rabin-trick) goes back to [FR74] where it is
attributed to earlier work by Fischer and Meyer as well as by Strassen without
specifying concrete publications.

A similar idea transforms the formula $\exists^{=2c+1}y\colon y_{0}\leqslant
y<y_{1}\land\varphi(y)$ into

$\exists
y_{\frac{1}{2}}\colon\begin{array}[t]{cl}&y_{0}<y_{\frac{1}{2}}<y_{1}\\\
\land&\varphi(y_{\frac{1}{2}})\\\ \land&\forall
a,b\colon\Bigl{(}(a,b)\in\\{(y_{0},y_{\frac{1}{2}}),(y_{\frac{1}{2}}+1,y_{1})\\}\to\exists^{=c}y\colon\bigl{(}a\leqslant
y<b\land\varphi(y)\bigr{)}\Bigr{)}\,.\end{array}$

Note that this results in an exponential increase in formula size since the
formula $\varphi$ is mentioned twice. To avoid this size increase, we
“postpone” the evaluation of the formula $\varphi(y_{\frac{1}{2}})$. Slightly
more precisely, the above construction proceeds recursively since in both
cases, we have the subformula $\exists^{=c}y\colon\bigl{(}a\leqslant
y<b\land\varphi(y)\bigr{)}$. Along this recursion, we collect in some set $V$
all the variables $y_{\frac{1}{2}}$ seen in between that are required to
satisfy $\varphi$. At the very end of the recursion, we write down the formula

$\forall y\colon\bigl{(}(\bigvee_{x\in V}x=y)\to\varphi(y)\bigr{)}$

expressing all the “postponed” requirements at once.

The above idea is based on the linear order on the integers. If we consider
the non-unary quantifier $\exists^{=c}\overline{y}$, the role of this linear
order $\leqslant$ is played by the lexicographic order on tuples
$\overline{y}$.

The proof of the following lemma formalises the above ideas. The crucial
requirement is that the formula and its block depth shall grow only by a small
summand (the latter makes sense only in case the formula $\varphi$ does not
contain any modulo-counting quantifiers, i.e., belongs to $\mathrm{FO}$).

######  Lemma 3.

Let $\alpha=\exists^{\geqslant c}\overline{y}\colon\varphi$ or
$\alpha=\exists^{=c}\overline{y}\colon\varphi$ with
$\varphi\in\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x}]$. There exists a
formula $\psi\in\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x}]$ with
$\psi\iff\alpha$, $\textsc{Const}(\psi)=\textsc{Const}(\alpha)$,
$\textsc{Coeff}(\psi)=\textsc{Coeff}(\alpha)$, and
$\textsc{Mod}(\psi)=\textsc{Mod}(\alpha)$.

Furthermore, $|\psi|\leqslant|\varphi|+O(\ell\cdot\log c)$ where $\ell$ is the
length of the tuple of variables $\overline{y}$ and the formula $\psi$ can be
computed from $\alpha$ in time $|\varphi|+O(\ell\cdot\log c)$.

If $\varphi$ belongs to $\mathrm{FO}$, then also $\psi\in\mathrm{FO}$ and the
block depth of $\psi$ is at most
$\mathrm{bd}^{\mathrm{FO}}(\varphi)+2\lceil\log(c)\rceil+2$.

######  Proof 3.1.

Before formalising the above idea, we need some notational preparation. For an
$\ell$-tuple of variables $\overline{x}=(x_{1},\dots,x_{\ell})$ and an
assignment $f$, we write $f(\overline{x})$ for the tuple
$\bigl{(}f(x_{1}),f(x_{2}),\dots,f(x_{\ell})\bigr{)}\in{\mathbb{Z}}^{\ell}$.
Furthermore (being a bit pedantic), we write $\exists\overline{x}$ for
$\exists x_{1}\,\exists x_{2}\,\cdots\,\exists x_{\ell}$ and similarly for the
universal quantifier.

For $\ell\geqslant 1$, let $\leqslant^{\ell}_{\mathrm{lex}}$ denote the
lexicographic order on ${\mathbb{Z}}^{\ell}$. By induction on $\ell$, we
construct formulas
$(y_{1},\dots,y_{\ell})<^{\ell}_{\mathrm{lex}}(z_{1},\dots,z_{\ell})$ as
follows:

  * •

$y_{1}<^{1}_{\mathrm{lex}}z_{1}$ stands for $y_{1}<z_{1}$.

  * •

$(y_{1},\dots,y_{\ell})<^{\ell}_{\mathrm{lex}}(z_{1},\dots,z_{\ell})$ stands
for $y_{1}<z_{1}\lor
y_{1}=z_{1}\land(y_{2},\dots,y_{\ell})<^{\ell-1}_{\mathrm{lex}}(z_{2},\dots,z_{\ell})$.

Then, for any assignment $f$, we have
$f(\overline{y}<^{\ell}_{\mathrm{lex}}\overline{z})=\mathrm{t\\!t}$ iff
$f(\overline{y})<^{\ell}_{\mathrm{lex}}f(\overline{z})$. Similarly, the
formulas

$\displaystyle(\overline{y}\leqslant^{\ell}_{\mathrm{lex}}\overline{z})$
$\displaystyle=\lnot(\overline{z}<^{\ell}_{\mathrm{lex}}\overline{y})$ and
$\displaystyle S(\overline{y},\overline{z})$
$\displaystyle=\bigl{(}\overline{y}<^{\ell}_{\mathrm{lex}}\overline{z}\land\lnot\exists\overline{x}\colon(\overline{y}<^{\ell}_{\mathrm{lex}}\overline{x}<^{\ell}_{\mathrm{lex}}\overline{z})\bigr{)}$

hold under the assignment $f$ iff
$f(\overline{y})\leqslant^{\ell}_{\mathrm{lex}}f(\overline{z})$ and
$f(\overline{y})$ is the immediate predecessor of $f(\overline{z})$ in
$({\mathbb{Z}}^{\ell},\leqslant^{\ell}_{\mathrm{lex}})$, respectively. Later,
we will need that all these formulas $\beta$ are of size $O(\ell)$ and satisfy
$\textsc{Const}(\beta)=\textsc{Coeff}(\beta)=\\{0,\pm 1,\pm 2\\}$ and
$\textsc{Mod}(\beta)=\\{1\\}$.

We fix fresh $\ell$-tuples of variables $\overline{z}_{\mathrm{left}}$,
$\overline{z}_{\mathrm{middle}}$, $\overline{z}_{\mathrm{right}}$,
$\overline{z_{1}}$, $\overline{z_{2}}$, and $\overline{z_{3}}$ that have no
variable in common.

By induction on $n\geqslant 0$, we will now construct for any finite set $V$
of $\ell$-tuples of variables a formula $\psi_{n,V}$ with the following
property: Let $f$ be an assignment such that

  * •

$f(\overline{z}_{\mathrm{left}})<^{\ell}_{\mathrm{lex}}f(\overline{z}_{\mathrm{right}})$
and

  * •

no tuple $\overline{v}$ from $V$ satisfies
$f(\overline{z}_{\mathrm{left}})\leqslant^{\ell}_{\mathrm{lex}}f(\overline{v})<^{\ell}_{\mathrm{lex}}f(\overline{z}_{\mathrm{right}})$.

In other words, the interval
$\bigl{[}f(\overline{z}_{\mathrm{left}}),f(\overline{z}_{\mathrm{right}})\bigr{)}\subseteq({\mathbb{Z}}^{\ell},\leqslant^{\ell}_{\mathrm{lex}})$
is not empty, but contains none of the values $f(\overline{v})$ for
$\overline{v}\in V$. Our construction of the formula $\psi_{n,V}$ will ensure
that it holds under such an assignment $f$, i.e.,
$f(\psi_{n,V})=\mathrm{t\\!t}$, iff

  * •

for all tuples $\overline{v}$ from $V$, we have
$f\bigr{(}\varphi(\overline{v})\bigr{)}=\mathrm{t\\!t}$ (more precisely:
$f\bigl{(}\forall\overline{x}\colon(\overline{x}=\overline{v}\to\varphi)\bigr{)}=\mathrm{t\\!t}$)
and

  * •

there are precisely $n$ tuples $\overline{m}\in{\mathbb{Z}}^{\ell}$ such that
$f(\overline{z}_{\mathrm{left}})\leqslant^{\ell}_{\mathrm{lex}}\overline{m}<^{\ell}_{\mathrm{lex}}f(\overline{z}_{\mathrm{right}})$
and $f_{\overline{x}/\overline{m}}(\varphi)=\mathrm{t\\!t}$.

In this construction, it will be convenient to write $\overline{w}\in V$ for
$\bigvee_{\overline{v}\in V}\overline{v}=\overline{w}$, i.e., for the
semantical property that $f(\overline{w})$ is one of the tuples of integers
$f(\overline{v})$ with $\overline{v}\in V$.

We start with $n=0$ and $n=1$:

$\displaystyle\psi_{0,V}$
$\displaystyle=\forall\overline{x}\colon\bigl{(}(\overline{z}_{\mathrm{left}}\leqslant^{\ell}_{\mathrm{lex}}\overline{x}<^{\ell}_{\mathrm{lex}}\overline{z}_{\mathrm{right}}\lor\overline{x}\in
V)\to(\varphi\leftrightarrow\overline{x}\in V)\bigr{)}$
$\displaystyle\psi_{1,V}$
$\displaystyle=\exists\overline{z}_{\mathrm{middle}}\colon\begin{array}[t]{cl}&\overline{z}_{\mathrm{left}}\leqslant^{\ell}_{\mathrm{lex}}\overline{z}_{\mathrm{middle}}<^{\ell}_{\mathrm{lex}}\overline{z}_{\mathrm{right}}\\\
\land&\forall\overline{x}\colon\bigl{(}(\overline{z}_{\mathrm{left}}\leqslant^{\ell}_{\mathrm{lex}}\overline{x}<^{\ell}_{\mathrm{lex}}\overline{z}_{\mathrm{right}}\lor\overline{x}\in
V)\to(\varphi\leftrightarrow\overline{x}\in
V\cup\\{\overline{z}_{\mathrm{middle}}\\})\bigr{)}\end{array}$

For the induction step, we now construct $\psi_{2n,V}$ and $\psi_{2n+1,V}$
with $n\geqslant 1$. The former is the simpler case:

$\psi_{2n,V}=\exists\overline{z_{1}},\overline{z_{2}},\overline{z_{3}}\colon\begin{array}[t]{cl}&\overline{z}_{\mathrm{left}}=\overline{z_{1}}<^{\ell}_{\mathrm{lex}}\overline{z_{2}}<^{\ell}_{\mathrm{lex}}\overline{z_{3}}=\overline{z}_{\mathrm{right}}\\\
\land&\forall\overline{z}_{\mathrm{left}},\overline{z}_{\mathrm{right}}\colon\Bigl{(}(\overline{z}_{\mathrm{left}},\overline{z}_{\mathrm{right}})\in\bigl{\\{}(\overline{z_{1}},\overline{z_{2}}),(\overline{z_{2}},\overline{z_{3}})\bigr{\\}}\to\psi_{n,V}\Bigr{)}\end{array}$

Note that $(\overline{z}_{\mathrm{left}},\overline{z}_{\mathrm{right}})$ is a
$2\ell$-tuple of variables so that
$(\overline{z}_{\mathrm{left}},\overline{z}_{\mathrm{right}})\in\bigl{\\{}(\overline{z_{1}},\overline{z_{2}}),(\overline{z_{2}},\overline{z_{3}})\bigr{\\}}$
is shorthand for the formula

$(\overline{z}_{\mathrm{left}}=\overline{z_{1}}\land\overline{z}_{\mathrm{right}}=\overline{z_{2}})\lor(\overline{z}_{\mathrm{left}}=\overline{z_{2}}\land\overline{z}_{\mathrm{right}}=\overline{z_{3}})\,.$

The idea of the formula $\psi_{2n,V}$ is to divide the interval
$\bigl{[}f(\overline{z}_{\mathrm{left}}),f(\overline{z}_{\mathrm{right}})\bigr{)}=\bigl{[}f(\overline{z_{1}}),f(\overline{z_{3}})\bigr{)}$
into two subintervals
$\bigl{[}f(\overline{z_{1}}),f(\overline{z_{2}})\bigr{)}$ and
$\bigl{[}f(\overline{z_{2}}),f(\overline{z_{3}})\bigr{)}$ and to verify that
both these intervals satisfy the formula $\psi_{n,V}$, i.e., contain in
particular precisely $n$ witnesses for $\varphi$.

To also construct $\psi_{2n+1,V}$, we need another $\ell$-tuple
$\overline{z_{2}}^{\prime}$ of fresh variables and set

$\psi_{2n+1,V}=\exists\overline{z_{1}},\overline{z_{2}}^{\prime},\overline{z_{2}},\overline{z_{3}}\colon\\!\\!\\!\\!\\!\\!\\!\\!\begin{array}[t]{cl}&\overline{z}_{\mathrm{left}}=\overline{z_{1}}<^{\ell}_{\mathrm{lex}}\overline{z_{2}}^{\prime}<^{\ell}_{\mathrm{lex}}\overline{z_{2}}<^{\ell}_{\mathrm{lex}}\overline{z_{3}}=\overline{z}_{\mathrm{right}}\land
S(\overline{z_{2}}^{\prime},\overline{z_{2}})\\\
\land&\forall\overline{z}_{\mathrm{left}},\overline{z}_{\mathrm{right}}\colon\Bigl{(}(\overline{z}_{\mathrm{left}},\overline{z}_{\mathrm{right}})\in\bigl{\\{}(\overline{z_{1}},\overline{z_{2}}^{\prime}),(\overline{z_{2}},\overline{z_{3}})\bigr{\\}}\to\psi_{n,V\cup\\{\overline{z_{2}}^{\prime}\\}}\Bigr{)}\,.\end{array}$

Here, the idea is to divide the interval
$I=\bigl{[}f(\overline{z}_{\mathrm{left}}),f(\overline{z}_{\mathrm{right}})\bigr{)}=\bigl{[}f(\overline{z_{1}}),f(\overline{z_{3}})\bigr{)}$
into the half-open interval
$I_{1}=\bigl{[}f(\overline{z_{1}}),f(\overline{z_{2}}^{\prime})\bigr{)}$ and
the open interval
$I_{2}=\bigl{(}f(\overline{z_{2}}^{\prime}),f(\overline{z_{3}})\bigr{)}$ and
to verify that both these intervals satisfy the formula
$\psi_{n,V\cup\\{\overline{z_{2}}^{\prime}\\}}$, i.e., contain in particular
precisely $n$ witnesses for $\varphi$, and that $f(\overline{z_{2}}^{\prime})$
satisfies $\varphi$. Since $I$ is the disjoint union of the intervals $I_{1}$,
$\\{f(\overline{z_{2}}^{\prime})\\}$, and $I_{2}$, this ensures that the
interval $I$ contains precisely $2n+1$ witnesses for $\varphi$.

Then the formula

$\exists\overline{z}_{\mathrm{left}},\overline{z}_{\mathrm{right}}\colon\bigl{(}(\overline{z}_{\mathrm{left}}<^{\ell}_{\mathrm{lex}}\overline{z}_{\mathrm{right}}\land\psi_{c,\emptyset}\bigr{)}$

is equivalent to $\exists^{\geqslant c}\overline{x}\colon\varphi$ since it
expresses that some interval contains precisely $c$ witnesses for $\varphi$.
Furthermore, the formula

$\exists\overline{z_{1}},\overline{z_{2}}\,\forall\overline{z}_{\mathrm{left}},\overline{z}_{\mathrm{right}}\colon\bigl{(}(\overline{z}_{\mathrm{left}}\leqslant^{\ell}_{\mathrm{lex}}\overline{z_{1}}\land\overline{z_{2}}\leqslant^{\ell}_{\mathrm{lex}}\overline{z}_{\mathrm{right}})\to\psi_{c,\emptyset}\bigr{)}$

is equivalent to $\exists^{=c}\overline{x}\colon\varphi$ since it expresses
that for some interval, any superinterval contains precisely $c$ witnesses for
$\varphi$.

It remains to analyse the size of the resulting formula as well as the block
depth in case $\varphi\in\mathrm{FO}$.

To estimate the size of $\psi_{c,\emptyset}$, note the following:

  * •

The size of the formulas $\psi_{0,V}$ and $\psi_{1,V}$ is of the form
$|\varphi|+O\bigl{(}\ell\cdot\log(c)\bigr{)}$ since we allow the Boolean
connective $\leftrightarrow$ in our formulas and since the size of $V$ is
bounded by $\lceil\log(c)\rceil$ (the formula size doubles if we consider
$\leftrightarrow$ as abbreviation).

  * •

The size increase when moving from $\psi_{n,V}$ to $\psi_{2n,V}$ is bounded by
a summand of size $O(\ell)$ and the same applies to the construction of
$\psi_{2n+1,V}$ from $\psi_{n,V\cup\\{\overline{z_{2}}^{\prime}\\}}$.

It follows that
$|\psi_{c,\emptyset}|\leqslant|\varphi|+\varkappa\cdot\ell\cdot\log(c)$ for
some constant $\varkappa$. One sees easily that the same holds for the formula
$\psi$ and that it can be constructed in time
$|\varphi|+O\bigl{(}\ell\cdot\log(c)\bigr{)}$.

Now suppose $\varphi\in\mathrm{FO}$. Since in the construction, we only
introduce classical existential quantifiers, we obtain
$\psi_{c,\emptyset}\in\mathrm{FO}$. We want to analyse the block depth of
$\psi_{c,\emptyset}$. First note that

$\displaystyle\mathrm{bd}^{\mathrm{FO}}(\psi_{0,V}),\mathrm{bd}^{\mathrm{FO}}(\psi_{1,V})$
$\displaystyle\leqslant\mathrm{bd}^{\mathrm{FO}}(\varphi)+2\,,$
$\displaystyle\mathrm{bd}^{\mathrm{FO}}(\psi_{2n,V})$
$\displaystyle\leqslant\mathrm{bd}^{\mathrm{FO}}(\psi_{n,V})+2\,,\text{ and}$
$\displaystyle\mathrm{bd}^{\mathrm{FO}}(\psi_{2n+1,V})$
$\displaystyle\leqslant\mathrm{bd}^{\mathrm{FO}}(\psi_{n,V\cup\\{\overline{z_{2}}^{\prime}\\}})+2\,.$

It follows that
$\mathrm{bd}^{\mathrm{FO}}(\psi_{c,V})\leqslant\mathrm{bd}^{\mathrm{FO}}(\varphi)+2\cdot\lceil\log(c)\rceil$.
In the final step, the block depth increases by at most $2$. Hence we obtain
$\mathrm{bd}^{\mathrm{FO}}(\psi)\leqslant\mathrm{bd}^{\mathrm{FO}}(\varphi)+2\lceil\log(c)\rceil+2$.

The above lemma can be applied iteratively to all threshold- and exact-
counting quantifiers. Hence, from a formula from
$\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x},\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}\bigr{]}$, we obtain an equivalent
formula in $\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x}]$, and from a
formula from $\mathrm{FO}[\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}]$, we obtain a formula from
$\mathrm{FO}$. In order to bound the block depth of this formula from
$\mathrm{FO}$, we extend its definition to formulas from
$\mathrm{FO}[\exists^{\geqslant c}\overline{x},\exists^{=c}\overline{x}]$ as
follows:

  * •

$\mathrm{BD}_{0}$ is the set of atomic formulas.

  * •

For $n\geqslant 1$, the set $\mathrm{BD}_{n}$ contains the formulas of the
following forms:

    * –

$\exists x_{1}\,\exists x_{2}\,\dots\,\exists x_{m}\colon\beta$ where
$m\geqslant 0$ and $\beta$ is a Boolean combination (possibly using $\lnot$,
$\land$, $\lor$, $\to$, and $\leftrightarrow$) of formulas from
$\mathrm{BD}_{n-1}$

    * –

$\exists^{\geqslant c}\overline{x}\colon\beta$ or
$\exists^{=c}\overline{x}\colon\beta$ where $\beta$ is a Boolean combination
of formulas from $\mathrm{BD}_{n-2\lceil\log_{2}c\rceil-2}$

  * •

The _block depth_ $\mathrm{bd}(\alpha)$ of a formula
$\alpha\in\mathrm{FO}[\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}]$ is the minimal natural number $n$
with $\alpha\in\mathrm{BD}_{n}$.

Note that the block depth of a formula from $\mathrm{FO}[\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}]$ is at most twice the length of the
formula (since the constants $c$ in $\exists^{\geqslant c}$ and $\exists^{=c}$
are written in binary). Furthermore, if $\alpha\in\mathrm{FO}$, then
$\mathrm{bd}^{\mathrm{FO}}(\alpha)=\mathrm{bd}(\alpha)$.

######  Proposition 4.

From a formula
$\varphi\in\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x},\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}\bigr{]}$, one can construct in time
polynomial in $|\varphi|$ an equivalent formula
$\psi\in\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x}]$.

In addition, we have $\textsc{Coeff}(\psi)\subseteq\textsc{Coeff}(\varphi)$,
$\textsc{Const}(\psi)\subseteq\textsc{Const}(\varphi)$, and
$\textsc{Mod}(\psi)\subseteq\textsc{Mod}(\varphi)$.

Furthermore, if $\varphi\in\mathrm{FO}[\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}]$, then the resulting formula $\psi$
belongs to $\mathrm{FO}$ and the block depth $\mathrm{bd}(\psi)$ of $\psi$
equals that of $\varphi$.

######  Proof 3.2.

Let $\varphi_{0}=\varphi$ contain $n$ threshold- or exact-counting
quantifiers. We construct, inductively, formulas $\varphi_{i+1}$ from
$\varphi_{i}$ using Lemma 3 that contain one threshold- or exact-counting
quantifier less. When constructing $\varphi_{i+1}$, suppose we eliminate a
quantifier of the form $\exists^{\geqslant c_{i}}(y_{1},\dots,y_{\ell_{i}})$
or $\exists^{=c_{i}}(y_{1},\dots,y_{\ell_{i}})$. Then $\varphi_{i+1}$ can be
constructed from $\varphi_{i}$ in time
$|\varphi_{i}|+O\bigl{(}\ell_{i}\cdot\log(c_{i})\bigr{)}$. Since
$\sum_{0\leqslant i<n}\ell_{i}\leqslant|\varphi|$ and $\sum_{0\leqslant
i<n}\log(c_{i})\leqslant|\varphi|$, the construction of $\varphi_{n}$ can be
carried out in time polynomial in $|\varphi|$.

Now suppose $\varphi\in\mathrm{FO}[\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}]$. Then the formula $\varphi_{n}$
belongs to $\mathrm{FO}$. Furthermore, when moving from $\varphi_{i}$ to
$\varphi_{i+1}$, the block depth does not increase.

From Berman’s upper bound for Presburger arithmetic, we get immediately the
following for the logic $\mathrm{FO}[\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}]$, i.e., the fragment of
$\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x},\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}\bigr{]}$ without modulo-counting
quantifiers.

######  Corollary 5.

Satisfaction of a closed formula $\varphi\in\mathrm{FO}[\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}]$ can be decided in doubly exponential
alternating time with linearly many alternations.

######  Proof 3.3.

The transformation of $\varphi$ into an equivalent closed formula $\psi$ from
$\mathrm{FO}$ increases the size of the formula only polynomially and the
resulting block depth belongs to $O(|\varphi|)$. Hence the claim follows from
Berman’s Theorem 2.

Somewhat surprisingly, the above result says that adding the quantifiers
$\exists^{\geqslant c}\overline{x}$ and $\exists^{=c}\overline{x}$ does not
increase the complexity of the decision procedure; for the unary version of
the above logic, i.e., for $\mathrm{FO}[\exists^{\geqslant
c}x,\exists^{=c}x]$, this was already observed in [CHM22].

###  3.2. Elimination of non-unary modulo-counting quantifiers

Here, we give the transformation from
$\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x}]$ to
$\mathrm{FO}\bigl{[}\exists^{(q,p)}x]$. We will provide a transformation that
can be computed in doubly exponential time and does not change the sets Coeff,
Const, and Mod, nor the quantifier depth.

The crucial task in this section is to express a non-unary quantification
$\exists^{(t,p)}(y_{1},\dots,y_{\ell})$ (where the remainder is given as a
term $t$) using only unary modulo-counting quantifications where the remainder
is given as a constant. The first step is obvious: Using a case distinction,
we replace $\exists^{(t,p)}\overline{y}\colon\varphi$ by the disjunction of
all formulas $t\equiv_{p}r\land\exists^{(r,p)}\overline{y}\colon\varphi$ for
$0\leqslant r<p$. As a second step, one has to eliminate the quantification
over a tuple $\overline{y}$. We explain the basic idea using the formula
$\exists^{(0,2)}(y_{1},y_{2})\colon\rho(y_{1},y_{2})$ where $\rho$ is some
formula and $R$ is the set of pairs of integers satisfying $\rho$. We have to
express that $R$ is finite and its number of elements is even.

Assuming $R$ to be finite, its size is even iff the number of elements $y_{1}$
with

$\Bigl{|}\bigl{\\{}y_{2}\bigm{|}(y_{1},y_{2})\in R\bigr{\\}}\Bigr{|}\text{
odd}$

is even. This can be expressed by the formula

$\exists^{(0,2)}y_{1}\,\exists^{(1,2)}y_{2}\colon\rho(y_{1},y_{2})\,.$

Further, $R$ is finite iff its number of elements is even or odd. But this
would not eliminate the non-unary quantification. Alternatively, $R$ is finite
iff it is bounded, i.e., if

$\exists z\,\forall y_{1}\,\forall
y_{2}\,\bigl{(}\rho(y_{1},y_{2})\to|y_{1}|,|y_{2}|\leqslant z\bigr{)}$

holds. Although being a simple formula, its quantifier rank is larger than
that of the formula we started with. Yet another characterisation of
finiteness of $R$ is “only finitely many elements can be extended to a tuple
from $R$ and no element can be extended in infinitely many ways”. The
following formula expresses precisely this:

$\displaystyle\exists^{(0,2)}y_{1}\,\exists
y_{2}\colon\rho(y_{1},y_{2})\lor\exists^{(1,2)}y_{1}\,\exists
y_{2}\colon\rho(y_{1},y_{2})$ $\displaystyle\land$ $\displaystyle\forall
y_{1}\,\Bigl{(}\exists^{(0,2)}y_{2}\colon\rho(y_{1},y_{2})\lor\exists^{(1,2)}y_{2}\colon\rho(y_{1},y_{2})\Bigr{)}$

The proof of the following lemma formalises this idea (and extends it to other
moduli and remainder given as terms). In other words, it shows how to
eliminate a single non-unary modulo-counting quantifier.

######  Lemma 6.

Let $\alpha=\exists^{(t,p)}\overline{y}\colon\varphi$ with
$\varphi\in\mathrm{FO}\bigl{[}\exists^{(q,p)}x]$. There exists a formula
$\psi\in\mathrm{FO}\bigl{[}\exists^{(q,p)}x]$ with $\psi\iff\alpha$,
$\textsc{Const}(\psi)=\textsc{Const}(\alpha)$,
$\textsc{Coeff}(\psi)=\textsc{Coeff}(\alpha)$,
$\textsc{Mod}(\psi)=\textsc{Mod}(\alpha)$, and
$\mathrm{qd}(\psi)=\mathrm{qd}(\alpha)$.

Furthermore, $\psi$ can be constructed from $\alpha$ in time
$O\bigl{(}p^{p\cdot\ell}\cdot|\alpha|\bigr{)}$ where $\ell$ is the length of
the tuple $\overline{y}$.

Note that the modulus $p$ is given in binary. Hence the time bound is doubly
exponential in the size of the formula $\alpha$.

######  Proof 3.4.

First suppose $\ell=1$ and consider the formula

$\psi:=\bigvee_{0\leqslant
r<p}(r\equiv_{p}t\land\exists^{(r,p)}y_{1}\colon\varphi)$

which is clearly equivalent to $\alpha$ and has all the properties required by
the claim of the lemma.

So suppose $\ell>1$. First, we construct inductively a formula from
$\mathrm{FO}\bigl{[}\exists^{(q,p)}x]$ expressing that there are only finitely
many tuples $\overline{y}$ satisfying $\varphi$ (for $0\leqslant n<\ell-1$):

$\displaystyle\eta_{\ell-1}(y_{1},\dots,y_{\ell-1})=$
$\displaystyle\bigvee_{0\leqslant i<p}\exists^{(i,p)}y_{\ell}\colon\varphi$
$\displaystyle\eta_{n}(y_{1},\dots,y_{n})=$ $\displaystyle\bigvee_{0\leqslant
i<p}\exists^{(i,p)}y_{n+1}\,\exists(y_{n+2},\dots,y_{\ell})\colon\varphi$
$\displaystyle\land\forall y_{n+1}\colon\eta_{n+1}(y_{1},\dots,y_{n+1})$

Let $(y_{1},\dots,y_{\ell-1})$ be any tuple of integers. The formula
$\eta_{\ell-1}$ expresses that the tuple $(y_{1},\dots,y_{\ell-1})$ can be
extended to a tuple satisfying $\varphi$ in only finitely many ways.

Now let $(y_{1},\dots,y_{\ell-2})$ be any tuple of integers. The first line of
the formula $\eta_{\ell-2}$ expresses that the tuple
$(y_{1},\dots,y_{\ell-2})$ can be extended to a tuple
$(y_{1},\dots,y_{\ell-1})$ that allows a further extension to a tuple
satisfying $\varphi$ in only finitely many ways. The second line expresses
that, for any integer $y_{\ell-1}$, there are only finitely many extensions of
the tuple $(y_{1},\dots,y_{\ell-1})$ to a tuple $(y_{1},\dots,y_{\ell})$
satisfying $\varphi$. Hence, $\eta_{\ell-2}$ expresses that there are only
finitely many extensions of $(y_{1},\dots,y_{\ell-2})$ satisfying $\varphi$.

Arguing inductively, we obtain that $\eta_{0}$ expresses that there are only
finitely many tuples $(y_{1},\dots,y_{\ell})$ satisfying $\varphi$.

Now consider the formula

$\beta=\bigvee_{0\leqslant
r<p}\bigl{(}r\equiv_{p}t\land\eta_{0}\land\exists^{(r,p)}\overline{y}\colon\varphi\bigr{)}$

that is equivalent with $\alpha$. It remains to rewrite
$\exists^{(r,p)}\overline{y}\colon\varphi$ into a formula from
$\mathrm{FO}\bigl{[}\exists^{(q,p)}x]$. In this construction, we can assume
that $\eta_{0}$ holds, i.e., that there are only finitely many tuples
$(y_{1},\dots,y_{\ell})$ satisfying $\varphi$. To this aim, consider the
$\mathrm{FO}\bigl{[}\exists^{(q,p)}x]$-formulas (for $0\leqslant n<\ell-1$ and
$0\leqslant d<p$)

$\displaystyle\delta_{\ell-1}^{d}(y_{1},\dots,y_{\ell-1})$
$\displaystyle=\exists^{(d,p)}y_{\ell}\colon\varphi\text{ and}$
$\displaystyle\delta_{n}^{d}(y_{1},\dots,y_{n})$
$\displaystyle=\bigvee_{(*)}\bigwedge_{0<i<p}\exists^{(d_{i},p)}y_{n+1}\colon\delta_{n+1}^{i}(y_{1},\dots,y_{n+1})$

where the disjunction $(*)$ extends over all tuples $(d_{1},\dots,d_{p-1})$
over $\\{0,1,\dots,p-1\\}$ such that

$\sum_{0<i<p}d_{i}\cdot i\equiv_{p}d\,.$ (1)

Let $(y_{1},\dots,y_{\ell-1})$ be a tuple of integers. Then the formula
$\delta_{\ell-1}^{d}$ expresses that there are $d$ many ways to extend the
tuple $(y_{1},\dots,y_{\ell-1})$ to a tuple satisfying $\varphi$ (all counts
in this paragraph are understood modulo $p$). Next let
$(y_{1},\dots,y_{\ell-2})$ be a tuple of integers. Then the conjunction in the
formula $\delta_{\ell-2}^{d}$ expresses that, for all
$i\in\\{1,2,\dots,p-1\\}$, there are $d_{i}$ many values for $y_{\ell-1}$ that
satisfy $\delta^{i}_{\ell-1}(y_{1},\dots,y_{\ell-1})$, i.e., that can be
extended in $i$ many ways to a tuple satisfying $\varphi$. Thus, the formula
$\delta_{\ell-2}^{d}$ expresses that the tuple $(y_{1},\dots,y_{\ell-2})$ can
be extended in $d$ many ways to a tuple satisfying $\varphi$. Arguing
inductively, the formula $\delta_{0}^{d}$ expresses that there are $d$ many
tuples satisfying $\varphi$.

Setting

$\psi:=\eta_{0}\land\bigvee_{0\leqslant
r<p}\bigl{(}r\equiv_{p}t\land\delta_{0}^{r}\bigr{)}$

we consequently get
$\alpha\Leftrightarrow\beta\Leftrightarrow\psi\in\mathrm{FO}\bigl{[}\exists^{(q,p)}x]$.

Note that the construction of $\eta_{0}$ and $\delta_{0}$ leaves the sets
$\textsc{Coeff}(.)$, $\textsc{Mod}(.)$, and $\textsc{Const}(.)$ and the
quantifier-depth unchanged.

It remains to bound the time needed to construct the formula $\psi$. First,
$\eta_{0}$ can be constructed in time $O(\ell\cdot p\cdot|\alpha|)$ since the
formula $\eta_{n+1}$ appears only once in $\eta_{n}$. Next, any of the
formulas $\delta_{\ell-1}^{d}$ can be constructed in time $O(|\alpha|)$. We
now consider the construction of $\delta_{n}^{d}$ from the formulas
$\delta_{n+1}^{i}$. Note that the tuple $(d_{1},\dots,d_{p-2})$ together with
equation (1) completely determines the value of $d_{p-1}\in\\{0,\dots,p-1\\}$.
Hence the disjunction $(*)$ extends over at most $p^{p-2}$ tuples.
Consequently, the formula $\delta_{n}^{d}$ contains at most
$p^{p-2}\cdot(p-1)\leqslant p^{p-1}$ many subformulas $\delta_{n+1}^{i}$. By
induction, we obtain that $\delta_{0}^{r}$ can be constructed in time
$O\bigl{(}p^{(p-1)\cdot\ell}\cdot|\alpha|\bigr{)}$. Since the construction of
$\psi$ requires this to be done for all $r\in\\{0,1,\dots,p-1\\}$ and
furthermore $r\equiv_{p}t$ has to be added, the formula $\psi$ can be
constructed in time $O\bigl{(}p\cdot\log(p)\cdot
p^{(p-1)\cdot\ell}\cdot|\alpha|\bigr{)}$ which is in
$O\bigl{(}p^{p\cdot\ell}\cdot|\alpha|\bigr{)}$ as $\ell>1$.

The above lemma allows to reduce the number of non-unary modulo-counting
quantifiers by one, hence an inductive application eliminates all of them. The
algorithmic cost and the form of the resulting formula is analysed in the
following proof.

######  Proposition 7.

From a formula $\varphi\in\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x}]$,
one can construct in time doubly exponential in $|\varphi|$ an equivalent
formula $\gamma\in\mathrm{FO}\bigl{[}\exists^{(q,p)}x]$.

In addition, we have $\textsc{Coeff}(\gamma)\subseteq\textsc{Coeff}(\varphi)$,
$\textsc{Const}(\gamma)\subseteq\textsc{Const}(\varphi)$,
$\textsc{Mod}(\gamma)\subseteq\textsc{Mod}(\varphi)$, and
$\mathrm{qd}(\gamma)\leqslant\mathrm{qd}(\varphi)$.

######  Proof 3.5.

Let $P$ be the maximal value such that some modulo-counting quantifier
$\exists^{(t,P)}$ appears in the formula $\varphi$ and let $L$ be the maximal
arity of any modulo-counting quantifier in $\varphi$. Finally, let $n$ be the
number of non-unary modulo-counting quantifiers in $\varphi$.

Let $\varphi_{0}=\varphi$. To inductively construct $\varphi_{i+1}$ from
$\varphi_{i}$, we chose some subformula
$\exists^{(t,p)}(y_{1},\dots,y_{\ell})\colon\alpha$ with $\ell>1$ and
$\alpha\in\mathrm{FO}\bigl{[}\exists^{(q,p)}x]$. This subformula is replaced
by an equivalent formula from $\mathrm{FO}\bigl{[}\exists^{(q,p)}x]$ that we
obtain from Lemma 6. This reduces the number of non-unary modulo-counting
quantifiers by one so that $\gamma:=\varphi_{n}$ is a formula from
$\mathrm{FO}\bigl{[}\exists^{(q,p)}x]$.

From Lemma 6, we get $\gamma\iff\varphi$,
$\textsc{Const}(\gamma)=\textsc{Const}(\varphi)$,
$\textsc{Coeff}(\gamma)=\textsc{Coeff}(\varphi)$,
$\textsc{Mod}(\gamma)=\textsc{Mod}(\varphi)$, and
$\mathrm{qd}(\gamma)=\mathrm{qd}(\varphi)$.

Also from Lemma 6, we get that $\varphi_{i+1}$ can be constructed from
$\varphi_{i}$ in time $O(P^{P\cdot L}\cdot|\varphi_{i}|)$ and is therefore of
size at most $O(P^{P\cdot L}\cdot|\varphi_{i}|)$. Consequently, $\gamma$ can
be constructed from $\varphi_{0}$ in time $O(\bigl{(}P^{P\cdot
L}\bigr{)}^{n}\cdot|\varphi|)$. Since the binary encoding of $P$ appears in
$\varphi$, we get $P\leqslant 2^{|\varphi|}$. Furthermore,
$L,n\leqslant|\varphi|$. Consequently, the construction of $\gamma$ from
$\varphi$ can be carried out in doubly exponential time.

The above two Propositions 4 and 7 imply the following.

######  Theorem 8.

From a formula
$\varphi\in\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x},\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}\bigr{]}$, one can construct in time
doubly exponential in $|\varphi|$ an equivalent formula
$\gamma\in\mathrm{FO}\bigl{[}\exists^{(q,p)}x]$.

In addition, we have $\textsc{Coeff}(\gamma)\subseteq\textsc{Coeff}(\varphi)$,
$\textsc{Const}(\gamma)\subseteq\textsc{Const}(\varphi)$, and
$\textsc{Mod}(\gamma)\subseteq\textsc{Mod}(\varphi)$.

In addition, the quantifier depth $\mathrm{qd}(\gamma)$ is polynomial in the
size of $\varphi$.

######  Proof 3.6.

Using Proposition 4, one first constructs in polynomial time an equivalent
formula $\psi$ from $\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x}]$. This
formula is then, using Proposition 7, translated into an equivalent formula
$\gamma$ from $\mathrm{FO}\bigl{[}\exists^{(q,p)}x]$.

Since $|\psi|$ is polynomial in the size of $\varphi$, its quantifier depth is
also polynomial in $|\varphi|$. Hence, the same holds for the quantifier depth
of $\gamma$.

##  4\. Quantifier elimination

This section provides a quantifier elimination procedure for the logic
$\mathrm{FO}\bigl{[}\exists^{(q,p)}x]$ where, differently from the full logic
$\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x},\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}\bigr{]}$, only unary quantifications
$\exists y$ and $\exists^{(q,p)}y$ with $q\in{\mathbb{N}}$ are allowed.

As usual with quantifier elimination procedures, we first demonstrate how to
eliminate a single quantifier in front of a Boolean combination of atomic
formulas. Since the classical existential quantifier and the modulo-counting
quantifier behave rather differently, we handle them in separate Lemmas 10 and
11. The main point in both these lemmas is

  1. (1)

properties of the form $\exists/\exists^{(q,p)}x\colon\beta$ where $\beta$ is
quantifier-free can be expressed without quantification and

  2. (2)

the sets of coefficients, constants, and moduli vary in this process, but
these sets can be controlled.

Our quantifier elimination is effective, but we do not concentrate on this
fact. We do, in particular, not aim at a fast elimination algorithm nor at
small resulting formulas. All we need for our later decision procedure is a
bound on the size of the coefficients, constants, and moduli appearing in the
resulting formula.

For this bound, suppose $\beta$ is a quantifier-free formula and $E$ is a
quantifier $\exists$ or $\exists^{(q,p)}$. We will prove that $Ex\colon\beta$
is equivalent to some quantifier-free formula $\gamma$ whose sets of
coefficients etc. are contained in the following sets (with $p=1$ in case
$E=\exists$):

$\displaystyle\textsc{Coeff}_{p}(\beta)$
$\displaystyle=\bigl{\\{}a_{1}a_{2}-a_{3}a_{4}\bigm{|}a_{1},a_{2},a_{3},a_{4}\in\textsc{Coeff}(\beta)\bigr{\\}}$
$\displaystyle\textsc{Const}_{p}(\beta)$
$\displaystyle=\left\\{a_{1}c_{1}-a_{2}(c_{2}+c)\,\left|\,\begin{array}[]{l}a_{1},a_{2}\in\textsc{Coeff}(\beta),c_{1},c_{2}\in\textsc{Const}(\beta)\\\
|c|\leqslant\max\textsc{Coeff}(\beta)\cdot
p\cdot\mathop{\mathrm{lcm}}\textsc{Mod}(\beta)\end{array}\right\\}\right.$
$\displaystyle\textsc{Mod}_{p}(\beta)$
$\displaystyle=\bigl{\\{}a_{1}a_{2}k_{1}k_{2}\bigm{|}a_{1}a_{2}\in\textsc{Coeff}(\beta),k_{1},k_{2}\in\textsc{Mod}(\beta)\cup\\{p\\}\bigr{\\}}$

Note that the first set does not depend on the number $p$ and that
$\textsc{Const}_{p}(\beta)\subseteq\textsc{Const}_{p_{1}}(\beta)$ for all
$1\leqslant p<p_{1}$.

Using these sets, we formulate the following condition on the triple
$(\beta,\gamma,p)$ where $\beta$ and $\gamma$ are formulas and $p\geqslant 1$
is a positive integer:

$\textsc{Coeff}(\gamma)\subseteq\textsc{Coeff}_{p}(\beta)\,,\
\textsc{Const}(\gamma)\subseteq\textsc{Const}_{p}(\beta)\,,\textsc{Mod}(\gamma)\subseteq\textsc{Mod}_{p}(\beta)$
(2)

Let $\beta$ be a quantifier-free formula and $x=t$ an equation (with $t$ an
$x$-free term). Write $\beta^{\prime}$ for the formula obtained from $\beta$
by replacing all occurrences of $x$ by $t$ so that $\beta^{\prime}$ is a
Boolean combination of $x$-free atomic formulas. Then the formulas
$x=t\land\beta$ and $x=t\land\beta^{\prime}$ are equivalent. The following
lemma, whose statement will be used repeatedly, demonstrates the analogous
fact for equations of the form $ax=t$ (with $a\neq 0$), i.e., constructs an
$x$-free quantifier-free formula $\beta^{\prime}$ so that $ax=t\land\beta$ and
$ax=t\land\beta^{\prime}$ are equivalent. The main point here is that, under a
specific condition on $a$, $t$, and $c$, the triple $(\beta,\beta^{\prime},p)$
satisfies the above Condition (2).

######  Lemma 9.

Let $\beta$ be a Boolean combination of $x$-separated atomic formulas, $ax<t$
or $t<ax$ some atomic formula from $\beta$ with $a>0$, $p\geqslant 1$ a
positive integer, and $c\in{\mathbb{Z}}$ with $|c|\leqslant a\cdot
p\cdot\mathop{\mathrm{lcm}}\textsc{Mod}(\beta)$. There exists a Boolean
combination $\beta_{a,t+c}$ of $x$-free atomic formulas such that the triple
$(\beta,\beta_{a,t+c},p)$ satisfies Condition (2) and, for all assignments
$f$,

$f(ax)=f(t+c)\text{ implies }f(\beta)=f(\beta_{a,t+c})\,.$

Note that in particular

$ax=t+c\land\beta\Longleftrightarrow ax=t+c\land\beta_{a,t+c}\,.$

######  Proof 4.1.

The formula $\beta_{a,t+c}$ is obtained from $\beta$ by the following
replacements (where $s$ is some $x$-free term, $a^{\prime}\geqslant 0$, and
$k\geqslant 2$):

$a^{\prime}x<s$ | is replaced by | $a^{\prime}t+a^{\prime}c<as$
---|---|---
$s<a^{\prime}x$ | is replaced by | $as<a^{\prime}t+a^{\prime}c$
$a^{\prime}x\equiv_{k}s$ | is replaced by | $a^{\prime}t+a^{\prime}c\equiv_{ak}as$

Let $f$ be some assignment with $f(ax)=f(t+c)$. Then we have

$\displaystyle f(a^{\prime}x<s)$ $\displaystyle=f(a^{\prime}ax<as)$
$\displaystyle\text{since }a>0$
$\displaystyle=f\bigl{(}a^{\prime}(t+c)<as\bigr{)}$ $\displaystyle\text{since
}f(ax)=f(t+c)$ $\displaystyle=f(a^{\prime}t+a^{\prime}c<as)$ and similarly
$\displaystyle f(s<a^{\prime}x)$ $\displaystyle=f(as<a^{\prime}t+a^{\prime}c)$
as well as $\displaystyle f(a^{\prime}x\equiv_{k}s)$
$\displaystyle=f(a^{\prime}ax\equiv_{ak}as)$
$\displaystyle=f\bigl{(}a^{\prime}(t+c)\equiv_{ak}as\bigr{)}$
$\displaystyle=f(a^{\prime}t+a^{\prime}c\equiv_{ak}as)\,.$

This completes the proof that $f(ax)=f(t+c)$ implies
$f(\beta)=f(\beta_{a,t+c})$.

It remains to verify Condition (2). First note that
$a\in\textsc{Coeff}(\beta)$ since $ax<t$ or $ax>t$ appears in $\beta$ and
since $t$ is $x$-free.

Now, let $b\in\textsc{Coeff}(\beta_{a,t+c)}$. If $b\in\textsc{Coeff}(\beta)$,
we get $b=1b-0b$ implying $b\in\textsc{Coeff}_{p}(\beta)$ since
$1,0\in\textsc{Coeff}(\beta)$. So let $b\notin\textsc{Coeff}(\beta)$. Then
there exists some atomic formula $a^{\prime}x<s$ or $s<a^{\prime}x$ in $\beta$
such that $b$ is some coefficient in the term $as-a^{\prime}(t+c)$.
Consequently, there exists a variable $y$ with coefficient $a_{2}$ in $s$ and
with coefficient $a_{4}$ in $t$ such that $b=aa_{2}-a^{\prime}a_{4}$. Since
$a^{\prime}x<s$ or $s<a^{\prime}x$ is an atomic formula in $\beta$ and since
$s$ is $x$-free, we have $a^{\prime}\in\textsc{Coeff}(\beta)$. Hence, also in
this case, $b\in\textsc{Coeff}_{p}(\beta)$.

Next let $d\in\textsc{Const}(\beta_{a,t+c})$. If $d\in\textsc{Const}(\beta)$,
we have $d=1d-0(0+c)\in\textsc{Const}_{p}(\beta)$. So suppose
$d\notin\textsc{Const}(\beta)$. Then, as above, there exists some atomic
formula $a^{\prime}x<s$ or $s<a^{\prime}x$ in $\beta$ such that $\pm d$ is the
constant term in $as-a^{\prime}(t+c)$. Consequently, $\pm
d=ac_{1}-a^{\prime}(c_{2}+c)$ where $c_{1}$ and $c_{2}$ are the constant terms
of $s$ and $t$, resp. Since $a,a^{\prime}\in\textsc{Coeff}(\beta)$ (see above)
and since $|c|\leqslant a\cdot
p\cdot\mathop{\mathrm{lcm}}\textsc{Mod}(\beta)$, we get
$d\in\textsc{Const}_{p}(\beta)$.

Finally, let $\ell\in\textsc{Mod}(\beta_{a,t+c})$. If
$\ell\in\textsc{Mod}(\beta)$, then $\ell=1\cdot 1\cdot\ell\cdot
1\in\textsc{Mod}_{p}(\beta)$ since $1\in\textsc{Coeff}(\beta)$. Otherwise,
there exists an atomic formula $a^{\prime}x\equiv_{k}s$ in $\beta$ with
$\ell=ak$. Hence, also in this case, $\ell=1\cdot ak\cdot
1\in\textsc{Mod}_{p}(\beta)$.

We now come to the elimination of the classical existential quantifier.
Neither the result nor its proof are new, we present them here to be able to
also verify Condition (2).

######  Lemma 10.

Let $x$ be a variable and $\beta$ a Boolean combination of $x$-separated
atomic formulas. Then there exists a Boolean combination $\gamma$ of $x$-free
atomic formulas such that the triple $(\beta,\gamma,1)$ satisfies Condition
(2) and $(\exists x\colon\beta)\Longleftrightarrow\gamma$.

######  Proof 4.2.

Let $T$ be the set of all pairs $(a,t)$ such that $\beta$ contains an atomic
formula of the form $ax<t$ or $t<ax$ with $a>0$. We first assume that this set
$T$ is not empty. Let furthermore
$N=\mathop{\mathrm{lcm}}\bigl{(}\textsc{Mod}(\beta)\bigr{)}$. In particular,
$N$ is a multiple of every integer $k$ such that the atomic formula
$ax\equiv_{k}t$ appears in $\beta$ for some term $t$ and some
$a\in{\mathbb{Z}}$. Then we set

$\gamma:=\bigvee(\beta_{a,t+c}\land 0\equiv_{a}t+c)$

where the disjunction extends over all triples $(a,t,c)$ with $(a,t)\in T$ and
$-aN\leqslant c\leqslant aN$ (since $T\neq\emptyset$, this disjunction is not
empty). We prove $(\exists x\colon\beta)\Longleftrightarrow\gamma$. So let $f$
be an assignment with $f(\exists x\colon\beta)=\mathrm{t\\!t}$. Then there is
$b\in{\mathbb{Z}}$ with $f_{x/b}(\beta)=\mathrm{t\\!t}$. Let $g=f_{x/b}$.
Since the values $\frac{f(t)}{a}$ for $(a,t)\in T$ divide ${\mathbb{Z}}$ into
intervals, there exists $(a,t)\in T$ such that

  1. (1)

$b=\frac{f(t)}{a}$ or

  2. (2)

$\frac{f(t)}{a}<b$ and for all $(a^{\prime},t^{\prime})\in T$ with
$\frac{f(t^{\prime})}{a^{\prime}}<b$, we have
$\frac{f(t^{\prime})}{a^{\prime}}\leqslant\frac{f(t)}{a}$ or

  3. (3)

$b<\frac{f(t)}{a}$ and for all $(a^{\prime},t^{\prime})\in T$ with
$b<\frac{f(t^{\prime})}{a^{\prime}}$, we have
$\frac{f(t)}{a}\leqslant\frac{f(t^{\prime})}{a^{\prime}}$.

(The 2nd and 3rd cases are not exclusive, but if $b<\frac{f(t)}{a}$ for all
$(a,t)\in T$, then only the third case applies and symmetrically in case
$b>\frac{f(t)}{a}$.) Assume the first case. Then $g(ax)=ab=f(t)=g(t)$ where
the last equality holds since $t$ is $x$-free. Hence, by Lemma 9, we get
$\mathrm{t\\!t}=g(\beta)=g(\beta_{a,t})=f(\beta_{a,t})$ and, since
$\frac{f(t)}{a}=b\in{\mathbb{Z}}$, also $f(0\equiv_{a}t)=\mathrm{t\\!t}$.
Hence, using the triple $(a,t,0)$, we have $f(\gamma)=\mathrm{t\\!t}$.

Next consider the second case. There exists $k\in{\mathbb{N}}$ with
$0<(b-kN)-\frac{f(t)}{a}\leqslant N$ or, equivalently,
$0<a(b-kN)-f(t)\leqslant aN$. We set $c=a(b-kN)-f(t)$ so that $-aN\leqslant
c\leqslant aN$.

Since $N$ is a multiple of all moduli appearing in $\beta$, we get
$f_{x/b-kN}(\beta)=\mathrm{t\\!t}$ from $f_{x/b}(\beta)=\mathrm{t\\!t}$ and
the choice of $(a,t)$ and of $k$. Set $g^{\prime}=f_{x/b-kN}$. Then
$g^{\prime}(ax)=a(b-kN)=f(t+c)=g^{\prime}(t+c)$ since the term $t+c$ is
$x$-free. Hence, by Lemma 9, we get
$\mathrm{t\\!t}=f_{x/b-kN}(\beta)=g^{\prime}(\beta)=g^{\prime}(\beta_{a,t+c})=f(\beta_{a,t+c})$.
Furthermore, $f(t)+c=a(b-kN)$ is divisible by $a$ so that
$f(0\equiv_{a}t+c)=\mathrm{t\\!t}$. Using the triple $(a,t,c)$, we obtain
$f(\gamma)=\mathrm{t\\!t}$ also in the second case.

The third case is symmetric to the second, i.e., we showed $f(\exists
x\colon\beta)=\mathrm{t\\!t}\Longrightarrow f(\gamma)=\mathrm{t\\!t}$.

For the converse implication, suppose $f(\gamma)=\mathrm{t\\!t}$. Then there
is a triple $(a,t,c)$ with $(a,t)\in T$ and $-aN\leqslant c\leqslant aN$ such
that $f(\beta_{a,t+c}\land 0\equiv_{a}t+c)=\mathrm{t\\!t}$. Because of
$0\equiv_{a}f(t)+c$, there exists $b\in{\mathbb{Z}}$ with $ab=f(t+c)$. Let
$g=f_{x/b}$. Then $g(ax)=ab=f(t+c)=g(t+c)$ since $t$ is $x$-free. Hence, by
Lemma 9, we have $g(\beta)=g(\beta_{a,t+c})=f(\beta_{a,t+c})=\mathrm{t\\!t}$.
Since $g=f_{x/b}$, this implies $f(\exists x\colon\beta)=\mathrm{t\\!t}$ and
therefore the remaining implication.

Finally, we have to verify Condition (2). Recall that $(a,t)\in T$ means that
$ax<t$ or $t<ax$ is a subformula of $\beta$ (or $a=1$ and $t=0$). Hence
$\textsc{Coeff}(\gamma)\subseteq\textsc{Coeff}_{1}(\beta)$ and
$\textsc{Const}(\gamma)\subseteq\textsc{Const}_{1}(\beta)$ follow immediately
from Lemma 9 since these sets only refer to atomic formulas of the form
$a^{\prime}x<s$ or $a^{\prime}x>s$. Next let $\ell\in\textsc{Mod}(\gamma)$.
Then $\ell\in\textsc{Mod}(\beta_{a,t+c})$ or $\ell=a$ for some $(a,t)\in T$
and $|c|\leqslant aN$. In the first case, $\ell\in\textsc{Mod}_{1}(\beta)$
follows from Lemma 9, in the latter case note that
$a,1\in\textsc{Coeff}(\beta)$ and $1\in\textsc{Mod}(\beta)$ so that
$\ell=a=1\cdot a\cdot 1\cdot 1\in\textsc{Mod}_{1}(\beta)$.

Thus, we proved the lemma in case $T\neq\emptyset$. Now assume $T=\emptyset$.
Note that the formulas $\beta$ and $\beta\land(x<0\lor\lnot x<0)$ are
equivalent, agree on the sets of coefficients etc., and that the latter
contains some atomic formula of the form $ax<t$. Thus, by the above arguments,
we find the Boolean combination $\gamma$ with the desired properties also in
this case.

Having shown how to eliminate a single existential quantifier, we now come to
the analogous result for modulo-counting quantifiers.

######  Lemma 11.

Let $x$ be a variable, $\beta$ a Boolean combination of $x$-separated atomic
formulas, and $0\leqslant q<p$ natural numbers. Then there exists a Boolean
combination of $x$-free atomic formulas $\gamma$ such that the triple
$(\beta,\gamma,p)$ satisfies Condition (2) and
$(\exists^{(q,p)}x\colon\beta)\Longleftrightarrow\gamma$.

The proof of this lemma requires several claims and definitions that we
demonstrate first, the actual proof of Lemma 11 can be found on page 4.6. Its
idea is to split the integers into finitely many intervals (depending on the
set of terms that appear in $\beta$) and to express the number (modulo $p$) of
witnesses for $\beta$ in any such interval by a quantifier-free formula. The
claims below consider different types of such intervals.

Let $N=\mathop{\mathrm{lcm}}\bigl{(}\textsc{Mod}(\beta)\bigr{)}$. Let $T$ be
the set of all pairs $(a,t)$ such that $\beta$ contains an atomic formula of
the form $ax<t$ or $t<ax$ with $a>0$ (if no such formula exists, set
$T=\bigl{\\{}(1,0)\bigr{\\}}$).

Let $S$ be some non-empty subset of $T$ and let $\prec$ be a strict linear
order on $S$. We call an assignment $f$ _consistent with $(S,\prec)$_ if the
following hold:

  * •

$\frac{f(s_{1})}{a_{1}}<\frac{f(s_{2})}{a_{2}}\iff(a_{1},s_{1})\prec(a_{2},s_{2})$
for all $(a_{1},s_{1}),(a_{2},s_{2})\in S$

  * •

for all $(a_{1},t_{1})\in T$, there exists $(a_{2},s_{2})\in S$ with
$\frac{f(t_{1})}{a_{1}}=\frac{f(s_{2})}{a_{2}}$.

In the following, let
$S=\bigl{\\{}(a_{1},s_{1}),(a_{2},s_{2}),\dots,(a_{n},s_{n})\bigr{\\}}$ with
$(a_{1},s_{1})\prec(a_{2},s_{2})\prec\dots\prec(a_{n},s_{n})$. Then any
assignment $f$ that is consistent with $(S,\prec)$ divides ${\mathbb{Z}}$ into
the open intervals444Of course, these intervals are considered as sets of
integers so that the terms “open” and “closed” are to be understood as
“excluding / including the given bounds if they happen to be integers”.
$\left(-\infty,\frac{f(s_{1})}{a_{1}}\right)$,
$\left(\frac{f(s_{i})}{a_{i}},\frac{f(s_{i+1})}{a_{i+1}}\right)$ for
$1\leqslant i<n$, and $\left(\frac{f(s_{n})}{a_{n}},\infty\right)$, and the
(singleton) closed intervals
$\left[\frac{f(s_{j})}{a_{j}},\frac{f(s_{j})}{a_{j}}\right]$ for $1\leqslant
j\leqslant n$. The following formulas describe (modulo $p$) the number of
witnesses for $\beta$ in these intervals (for $0\leqslant r<p$):

$\displaystyle\beta_{0,r}$
$\displaystyle=\exists^{(r,p)}x\colon(a_{1}x<s_{1}\land\beta)$
$\displaystyle\beta_{n,r}$
$\displaystyle=\exists^{(r,p)}x\colon(s_{n}<a_{n}x\land\beta)$
$\displaystyle\beta_{i,r}$
$\displaystyle=\exists^{(r,p)}x\colon(s_{i}<a_{i}x\land
a_{i+1}x<s_{i+1}\land\beta)$ $\displaystyle\beta^{\prime}_{j,r}$
$\displaystyle=\exists^{(r,p)}x\colon(a_{j}x=s_{j}\land\beta)$

Now consider the formula

$\varphi^{\prec}=\bigvee\left(\bigwedge_{0\leqslant i\leqslant
n}\beta_{i,r_{i}}\\\ \land\displaystyle\bigwedge_{1\leqslant i\leqslant
n}\beta^{\prime}_{i,r_{i}^{\prime}}\right)$

where the disjunction extends over all tuples
$(r_{0},r_{1},\dots,r_{n},r_{1}^{\prime},r_{2}^{\prime}\dots,r_{n}^{\prime})$
of integers from the set $\\{0,1,\dots,p-1\\}$ that, modulo $p$, sum up to
$q$. For any assignment $f$ consistent with $(S,\prec)$, we get
$f\bigl{(}\exists^{(q,p)}x\colon\beta\bigr{)}=f\bigl{(}\varphi^{\prec}\bigr{)}$.
In order to construct $\gamma$ as claimed in Lemma 11, we next eliminate the
counting quantifiers from the formulas $\beta_{0,r}$, $\beta_{i,r}$,
$\beta_{n,r}$, and $\beta^{\prime}_{j,r}$. In this elimination procedure
(detailed in the following claims), we will assume the assignment $f$ to be
consistent with $(S,\prec)$.

Let $0\leqslant r<p$. There exists a Boolean combination
$\gamma^{\prec}_{0,r}$ of $x$-free atomic formulas such that the triple
$(\beta,\gamma^{\prec}_{0,r},p)$ satisfies Condition (2) and
$f(\beta_{0,r})=f(\gamma^{\prec}_{0,r})$ for all assignments $f$ that are
consistent with $(S,\prec)$.

######  Proof 4.3.

Let $f$ be an assignment that is consistent with $(S,\prec)$. Let
$b\in{\mathbb{Z}}$ with $a_{1}b<f(s_{1})$. For all $(a,t)\in T$, we have
$b<\frac{f(s_{1})}{a_{1}}\leqslant\frac{f(t)}{a}$ and therefore
$a(b-N)<ab<f(t)$. Consequently, $b$ and $b-N$ satisfy the same inequalities
from $\beta$. Since $N$ is a multiple of all moduli appearing in $\beta$, the
same holds for all modulo constraints. Hence we obtain

$f_{x/b}(\beta)=f_{x/b-N}(\beta)\,.$

Consequently, there are infinitely many $b\in{\mathbb{Z}}$ satisfying
$f_{x/b}(a_{1}x<s_{1}\land\beta)=\mathrm{t\\!t}$ or none. For $r\neq 0$, we
can therefore set $\gamma^{\prec}_{0,r}=(0<0)$ ensuring Condition (2) for the
triple $(\beta,\gamma_{0,r}^{\prec},p)$. It remains to consider the case
$r=0$. Note that

$f(\beta_{0,0})=f\bigl{(}\exists^{(0,p)}x\colon(a_{1}x<s_{1}\land\beta)\bigr{)}=f\bigl{(}\neg\exists
x\colon(a_{1}x<s_{1}\land\beta)\bigr{)}$

since, if any, infinitely many integers $b<\frac{f(s_{1})}{a_{1}}$ satisfy
$f_{x/b}(\beta)=\mathrm{t\\!t}$. Let $\alpha$ be the formula obtained by Lemma
10 from the formula $\exists x\colon(a_{1}x<s_{1}\land\beta)$ and set
$\gamma_{0,0}^{\prec}=\lnot\alpha$. Since $a_{1}x<s_{1}$ or $s_{1}<a_{1}x$ is
an atomic formula from $\beta$, we get
$\textsc{Coeff}(\beta)=\textsc{Coeff}(a_{1}x<s_{1}\land\beta)$ and similarly
for Const and Mod. Hence the triple $(\beta,\alpha,p)$ and therefore
$(\beta,\gamma^{\prec}_{0,0},p)$ satisfies Condition (2).

Symmetrically, we also get the following:

Let $0\leqslant r<p$. There exists a Boolean combination
$\gamma^{\prec}_{n,r}$ of $x$-free atomic formulas such that the triple
$(\beta,\gamma^{\prec}_{n,r},p)$ satisfies Condition (2) and
$f(\beta_{n,r})=f(\gamma^{\prec}_{n,r})$ for all assignments $f$ that are
consistent with $(S,\prec)$.

We next want to eliminate the initial quantifier $\exists^{(r,p)}$ from
$\beta_{i,r}$ for $1\leqslant i<n$, i.e., we consider the integers in the open
interval $\left(\frac{f(s_{i})}{a_{i}},\frac{f(s_{i+1})}{a_{i+1}}\right)$. To
get the idea of the rather long proof, consider the formula

$\exists^{(0,2)}x\colon y<x<z\land x\equiv_{3}y+z$

and assume that the assignment $f$ satisfies $f(y)<f(z)$. Then the witnesses
for $\varphi:=(x\equiv_{3}y+z)$ in the interval $\bigl{(}f(y),f(z)\bigr{)}$
are $3$-periodic. Consequently, any subinterval of length $6=3\cdot 2$
contains an even number of witnesses for $\varphi$. It follows that we only
need to count the number of witnesses of $\varphi$ in the interval
$\bigl{(}f(y),f(y)+b\bigr{)}$ where $1\leqslant b\leqslant 6$ is the unique
number satisfying $6\mid f(z)-b$ (since then the length of the interval
$\bigl{[}f(y)+b,f(z)\bigr{)}$ is a multiple of $6$).

The main additional difficulty in the following proof is based on the
occurrence of subformulas of the form $ax<t$ for $a>0$.

Let $1\leqslant i<n$ and $0\leqslant r<p$. There exists a Boolean combination
$\gamma^{\prec}_{i,r}$ of $x$-free atomic formulas such that the triple
$(\beta,\gamma^{\prec}_{i,r},p)$ satisfies Condition (2) and
$f(\beta_{i,r})=f(\gamma^{\prec}_{i,r})$ for all assignments $f$ consistent
with $(S,\prec)$.

######  Proof 4.4.

Let $f$ be any assignment that is consistent with $(S,\prec)$ and let
$W\subseteq{\mathbb{Z}}$ be the set of witnesses for $\beta$, i.e.,

$W=\\{w\in{\mathbb{Z}}\mid f_{x/w}(\beta)=\mathrm{t\\!t}\\}\,.$

Furthermore, we write $I$ for the interval
$\left(\frac{f(s_{i})}{a_{i}},\frac{f(s_{i+1})}{a_{i+1}}\right)$. Our task is
to express, by a quantifier-free formula and irrespective of the concrete
$(S,\prec)$-consistent assignment $f$, that $|I\cap W|\equiv_{p}r$ holds.

We first split the interval $I$ into an initial segment of length $\leqslant
pN$ and subsequent subintervals of length $pN$ each. To this aim, let $b$ be
the unique integer from the set $\\{1,2,\dots,a_{i}a_{i+1}pN\\}$ with

$b\equiv_{a_{i}a_{i+1}pN}a_{i}f(s_{i+1})-a_{i+1}f(s_{i})\,.$

Since $N$ is the least common multiple of $\textsc{Mod}(\beta)$, this is
equivalent to requiring that the formula

$\bigwedge_{m\in\textsc{Mod}(\beta)}b\equiv_{a_{i}a_{i+1}pm}a_{i}s_{i+1}-a_{i+1}s_{i}$

evaluates to $\mathrm{t\\!t}$ under the assignment $f$. Note that
$a_{i}a_{i+1}pN$ divides $a_{i}f(s_{i+1})-a_{i+1}f(s_{i})-b$, hence

$K:=\frac{a_{i}f(s_{i+1})-a_{i+1}f(s_{i})-b}{a_{i}a_{i+1}pN}$

is an integer. Even more, $\frac{f(s_{i})}{a_{i}}<\frac{f(s_{i+1})}{a_{i+1}}$
implies $b\leqslant a_{i}f(s_{i+1})-a_{i+1}f(s_{i})$ and therefore
$K\in{\mathbb{N}}$. Now we define the following intervals:

  * •

$I_{0}=\left(\frac{f(s_{i})}{a_{i}},\frac{f(s_{i})}{a_{i}}+\frac{b}{a_{i}a_{i+1}}\right)$

  * •

$J_{k}=\left[\frac{f(s_{i})}{a_{i}}+\frac{b}{a_{i}a_{i+1}}+k\cdot
pN,\frac{f(s_{i})}{a_{i}}+\frac{b}{a_{i}a_{i+1}}+(k+1)\cdot pN\right)$ for
$0\leqslant k<K$

Note that these intervals form a partition of the interval $I$.

Let $c\in{\mathbb{Z}}$ with
$\frac{f(s_{i})}{a_{i}}<c<c+N<\frac{f(s_{i+1})}{a_{i+1}}$, i.e., $c,c+N\in I$.
Since $f$ is consistent with $(S,\prec)$, for any $(a,t)\in T$, we have
$\frac{f(t)}{a}\leqslant\frac{f(s_{i})}{a_{i}}<c<c+N$ or
$c<c+N<\frac{f(s_{i+1})}{a_{i+1}}\leqslant\frac{f(t)}{a}$. Hence $c$ and $c+N$
satisfy the same inequalities from $\beta$. Since $N$ is a multiple of all
moduli appearing in $\beta$, it follows that $c$ and $c+N$ also satisfy the
same modulo constraints from $\beta$. Hence we get

$f_{x/c}(\beta)=f_{x/c+N}(\beta)\,.$

It follows that the set $W$ of witnesses for $\beta$ within the interval $I$
is $N$-periodic. Since the interval $J_{k}\subseteq I$ is of length $pN$, it
follows that $|J_{k}\cap W|\equiv_{p}0$ for all $0\leqslant k<K$.
Consequently,

$\displaystyle|I\cap W|$ $\displaystyle=|I_{0}\cap W|+\sum_{0\leqslant
k<K}|J_{k}\cap W|$ $\displaystyle\equiv_{p}|I_{0}\cap W|\,.$

It remains to construct a formula expressing that the interval $I_{0}$ has,
modulo $p$, $r$ witnesses for $\beta$.

To characterise the elements of $I_{0}$, let $e\in{\mathbb{Z}}$ be arbitrary.
By the definition of $I_{0}$, we have $e\in I_{0}$ iff
$a_{i+1}f(s_{i})<a_{i}a_{i+1}e<a_{i+1}f(s_{i})+b$. This is clearly equivalent
to $0<a_{i}e-f(s_{i})<\frac{b}{a_{i+1}}$. Equivalently, there exists an
integer $d$ with

$0<d\leqslant\left\lfloor\frac{b-1}{a_{i+1}}\right\rfloor\text{ and
}e=\frac{f(s_{i})+d}{a_{i}}\,.$

Set
$M=\Bigl{\\{}1,2,\dots,\bigl{\lfloor}\frac{b-1}{a_{i+1}}\bigr{\rfloor}\Bigr{\\}}$.
Then we showed

$I_{0}=\left\\{\left.\frac{f(s_{i})+d}{a_{i}}\ \right|d\in
M,f(s_{i})+d\equiv_{a_{i}}0\right\\}\,.$

Now let $d\in M$ with $f(s_{i}+d)\equiv_{a_{i}}0$ be arbitrary and set
$e=\frac{f(s_{i}+d)}{a_{i}}$. Then we have

$f_{x/e}(a_{i}x)=a_{i}e=f_{x/e}(s_{i}+d)\,.$

Hence, by Lemma 9, we get

$f_{x/e}(\beta)=f_{x/e}(\beta_{a_{i},s_{i}+d})=f(\beta_{a_{i},s_{i}+d})$

where the last equality holds since $\beta_{a_{i},s_{i}+d}$ is $x$-free. It
follows that $e\in W$ iff $f(\beta_{a_{i},s_{i}+d})=\mathrm{t\\!t}$. Hence we
showed that $I_{0}\cap W$ is the set of fractions $\frac{f(s_{i}+d)}{a_{i}}$
for $d\in M$ with $f(s_{i}+d)\equiv_{a_{i}}0$ and
$f(\beta_{a_{i},s_{i}+d})=\mathrm{t\\!t}$. We consequently get

$\displaystyle|I_{0}\cap W|$
$\displaystyle=\Biggl{|}\biggl{\\{}\frac{f(s_{i}+d)}{a_{i}}\colon d\in
M,f(s_{i}+d)\equiv_{a_{i}}0,f(\beta_{a_{i},s_{i}+d})=\mathrm{t\\!t}\biggr{\\}}\Biggr{|}$
$\displaystyle=\biggl{|}\Bigl{\\{}d\in M\colon
f\bigl{(}s_{i}+d\equiv_{a_{i}}0\land\beta_{a_{i},s_{i}+d}\bigr{)}=\mathrm{t\\!t}\Bigr{\\}}\biggr{|}\,.$

It follows that $|I_{0}\cap W|\equiv_{p}r$ iff the following formula
$\gamma_{i,r}^{\prec}$ holds under the assignment $f$:

$\bigvee_{1\leqslant b\leqslant
a_{i}a_{i+1}pN}\left(\begin{array}[]{ll}&\displaystyle\bigwedge_{m\in\textsc{Mod}(\beta)}b\equiv_{a_{i}a_{i+1}pm}a_{i}s_{i+1}-a_{i+1}s_{i}\\\
\land&\displaystyle\bigvee_{\genfrac{}{}{0.0pt}{}{W_{0}\subseteq
M}{|W_{0}|\equiv_{p}r}}\left(\begin{array}[]{ll}&\displaystyle\bigwedge_{d\in
W_{0}}\bigl{(}s_{i}+d\equiv_{a_{i}}0\land\beta_{a_{i},s_{i}+d}\bigr{)}\\\
\land&\displaystyle\bigwedge_{d\in M\setminus
W_{0}}\lnot\bigl{(}s_{i}+d\equiv_{a_{i}}0\land\beta_{a_{i},s_{i}+d}\bigr{)}\end{array}\right)\end{array}\right)$

We finally verify Condition (2) for the triple
$(\beta,\gamma_{i,r}^{\prec},p)$. Note that any element of
$\textsc{Coeff}(\gamma_{i,r}^{\prec})$ or
$\textsc{Const}(\gamma_{i,r}^{\prec})$ appears in a subformula of the form
$\beta_{a_{i},s_{i}+d}$ for some integer $d\in M$ and therefore $1\leqslant
d\leqslant\frac{b-1}{a_{i+1}}<a_{i}pN$. Hence
$\textsc{Coeff}(\gamma_{i,r}^{\prec})\subseteq\textsc{Coeff}_{p}(\beta)$ and
$\textsc{Const}(\gamma_{i,r}^{\prec})\subseteq\textsc{Const}_{p}(\beta)$
follow from Lemma 9.

Now let $p_{1}\in\textsc{Mod}(\gamma_{i,r}^{\prec})$. There are three cases to
be considered:

  * •

$p_{1}=a_{i}a_{i+1}pm$ for some $m\in\textsc{Mod}(\beta)$. Then
$p_{1}\in\textsc{Mod}_{p}(\beta)$.

  * •

$p_{1}=a_{i}$. Then
$p_{1}\in\textsc{Coeff}(\beta)\subseteq\textsc{Mod}_{p}(\beta)$

  * •

$p_{1}\in\textsc{Mod}(\beta_{a_{i},s_{i}+d})$ for some integer $d$ with

$1\leqslant d\leqslant a_{i}pN\,.$

Then, by Lemma 9, $p_{1}\in\textsc{Mod}_{p}(\beta)$.

Thus, indeed,
$\textsc{Mod}(\gamma_{i,r}^{\prec})\subseteq\textsc{Mod}_{p}(\beta)$ which
finishes the proof of Claim 4.

Let $1\leqslant j\leqslant n$ and $0\leqslant r<p$. There exists a Boolean
combination $\delta^{\prec}_{j,r}$ of $x$-free atomic formulas such that
$(\beta,\delta^{\prec}_{j,r},p)$ satisfies Condition (2) and, for all
assignments $f$ (even those that are not consistent with $(S,\prec)$),
$f(\beta^{\prime}_{j,r})=f(\delta^{\prec}_{j,r})$.

######  Proof 4.5.

Since the term $s_{j}$ is $x$-free, there can be at most one witness for the
formula $a_{j}x=s_{j}\land\beta$ (which is the quantifier-free part of the
formula $\beta^{\prime}_{j,r}$). For $r>1$, we therefore set
$\delta_{j,r}^{\prec}=(0<0)$.

For the same reason, we obtain

$\exists^{(1,p)}x\colon(a_{j}x=s_{j}\land\beta)\iff\exists
x\colon(a_{j}x=s_{j}\land\beta)\,.$

Hence, we obtain the formula $\delta_{j,1}^{\prec}$ from Lemma 10. Since
precisely one of the formulas $\delta_{j,r}^{\prec}$ must hold, we can set
$\delta_{j,0}^{\prec}=\bigwedge_{0<r<p}\lnot\delta_{j,r}^{\prec}$ (which is
equivalent to $\lnot\delta_{j,1}^{\prec}$).

Having shown all these claims, we can now use them to finally prove Lemma 11.

######  Proof 4.6 (Proof of Lemma 11).

Let $S\subseteq T$ be some non-empty subset of $T$ and let $\prec$ be a strict
linear order on $S$. As above, we let
$S=\bigl{\\{}(a_{1},s_{1}),\dots,(a_{n},s_{n})\bigl{\\}}$ with
$(a_{1},s_{1})\prec(a_{2},s_{2})\prec\dots\prec(a_{n},s_{n})$. Then set

$\displaystyle\gamma^{\prec}=\bigvee\left(\bigwedge_{0\leqslant i\leqslant
n+1}\gamma_{i,r_{i}}^{\prec}\land\bigwedge_{1\leqslant j\leqslant
n}\delta_{j,r_{i}^{\prime}}^{\prec}\right)$

where the disjunction extends over all tuples
$(r_{0},r_{1},\dots,r_{n+1},r_{1}^{\prime},r_{2}^{\prime}\dots,r_{n}^{\prime})$
of natural numbers from $\\{0,1,\dots,p-1\\}$ with $\sum_{0\leqslant
i\leqslant n+1}r_{i}+\sum_{1\leqslant i\leqslant n}r_{i}^{\prime}\equiv_{p}q$.
The above claims imply $f(\varphi^{\prec})=f(\gamma^{\prec})$ for all
assignments $f$ that are consistent with $(S,\prec)$. Furthermore,
$\gamma^{\prec}$ is a Boolean combination of atomic formulas and the triple
$(\beta,\gamma^{\prec},p)$ satisfies Condition (2).

Next consider the formula

$\alpha^{\prec}=\bigwedge_{1\leqslant
i<n}a_{i+1}s_{i}<a_{i}s_{i+1}\land\bigwedge_{(a,t)\in T}\bigvee_{1\leqslant
i\leqslant n}a_{i}t=as_{i}\,.$

Then, for any assignment $f$, we have $f(\alpha^{\prec})=\mathrm{t\\!t}$ if
and only if $f$ is consistent with $(S,\prec)$. Since $\alpha^{\prec}$ is a
Boolean combination of formulas of the form $a^{\prime}s<at$555Write $\lnot
a_{i}t<as_{i}\land\lnot a_{i}t>as_{i}$ for $a_{i}t=as_{i}$. with
$(a,s),(a^{\prime},t)\in T$, the triple $(\beta,\alpha^{\prec},p)$ satisfies
Condition (2).

Finally, let

$\gamma=\bigvee_{(*)}(\alpha^{\prec}\land\gamma^{\prec})$

where the disjunction $(*)$ extends over all strict linear orders $\prec$ on
some non-empty subset of $T$.

Lemmas 10 and 11 above show how to eliminate a quantifier in front of a
quantifier-free formula and analyses the sets of coefficients, constants, and
moduli appearing in this process. The following proposition summarises these
results and provides bounds on the maximal coefficients etc. Recall that
$\mathbf{P}(\varphi)=\textsc{Coeff}(\varphi)\cup\textsc{Mod}(\varphi)$.

######  Proposition 12.

Let $x$ be a variable and $\alpha$ a Boolean combination of atomic formulas.
Let furthermore $E=\exists$ or $E=\exists^{(q,p)}$ for some $0\leqslant q<p$
and $2\leqslant p$. Then there exists a Boolean combination $\gamma$ of
$x$-free atomic formulas such that
$(Ex\colon\alpha)\Longleftrightarrow\gamma$. Furthermore, we have the
following:

$\displaystyle\max\mathbf{P}(\gamma)$
$\displaystyle\leqslant\max\mathbf{P}(Ex\colon\alpha)^{4}$
$\displaystyle\max\textsc{Const}(\gamma)$
$\displaystyle\leqslant\max\textsc{Const}(Ex\colon\alpha)\cdot
16^{\max\mathbf{P}(Ex\colon\alpha)}$

######  Proof 4.7.

If $E=\exists$, set $p=1$. Without changing the sets of coefficients etc., we
can transform $\alpha$ into an equivalent Boolean combination $\beta$ of
$x$-separated atomic formulas. By Lemma 10 or 11, there exists a Boolean
combination $\gamma$ of $x$-free atomic formulas with
$(Ex\colon\alpha)\Longleftrightarrow\gamma$ such that the triple
$(\alpha,\gamma,p)$ satisfies Condition (2).

Note that
$\max\textsc{Coeff}(\alpha),\max\textsc{Mod}(\alpha)\leqslant\max\mathbf{P}(\alpha)$.
From $\textsc{Coeff}(\gamma)\subseteq\textsc{Coeff}_{p}(\alpha)$ and
$\textsc{Mod}(\gamma)\subseteq\textsc{Mod}_{p}(\alpha)$, we can therefore
infer

$\displaystyle\max\textsc{Coeff}(\gamma)$
$\displaystyle\leqslant\max\textsc{Coeff}_{p}(\alpha)\leqslant
2\cdot\max\textsc{Coeff}(\alpha)^{2}$
$\displaystyle\leqslant\max\textsc{Coeff}(\alpha)^{3}$
$\displaystyle\leqslant\max\mathbf{P}(Ex\colon\alpha)^{4}$ and
$\displaystyle\max\textsc{Mod}(\gamma)$
$\displaystyle\leqslant\max\textsc{Mod}_{p}(\alpha)$
$\displaystyle\leqslant\max\textsc{Coeff}(\alpha)^{2}\cdot\max\textsc{Mod}(Ex\colon\alpha)^{2}$
$\displaystyle\leqslant\max\mathbf{P}(Ex\colon\alpha)^{4}\,.$

Consequently,
$\max\mathbf{P}(\gamma)\leqslant\max\mathbf{P}(Ex\colon\alpha)^{4}$.

From $\textsc{Const}(\gamma)\subseteq\textsc{Const}_{p}(\alpha)$, we can infer

$\displaystyle\max\textsc{Const}(\gamma)$ $\displaystyle\leqslant
2\cdot\max\textsc{Coeff}(\alpha)\cdot\max\textsc{Const}(\alpha)+\max\textsc{Coeff}(\alpha)^{2}\cdot
p\cdot\mathop{\mathrm{lcm}}\bigl{(}\textsc{Mod}(\alpha)\bigr{)}$
$\displaystyle\leqslant\max\mathbf{P}(\alpha)^{2}\cdot(\max\textsc{Const}(\alpha)+p\cdot\mathop{\mathrm{lcm}}\\{1,2,\dots,\max\textsc{Mod}(\alpha)\\})\,.$
Since $\mathop{\mathrm{lcm}}\\{1,2,\dots,n\\}\leqslant 4^{n-1}$ by [Nai82], we
can continue
$\displaystyle\leqslant\max\mathbf{P}(\alpha)^{2}\cdot(\max\textsc{Const}(\alpha)+p\cdot
4^{\max\mathbf{P}(\alpha)})$ $\displaystyle\leqslant
2^{\max\mathbf{P}(\alpha)}\cdot(\max\textsc{Const}(\alpha)+2^{p+2\cdot\max\mathbf{P}(\alpha)})\
(\text{provided }\max\mathbf{P}(\alpha)\neq 3)$
$\displaystyle\leqslant\max\textsc{Const}(\alpha)\cdot
2^{p+3\cdot\max\mathbf{P}(\alpha)}$
$\displaystyle\leqslant\max\textsc{Const}(\alpha)\cdot
2^{4\cdot\max\mathbf{P}(Ex\colon\alpha)}$
$\displaystyle=\max\textsc{Const}(Ex\colon\alpha)\cdot
16^{\max\mathbf{P}(Ex\colon\alpha)}\,.$

If $\max\mathbf{P}(\alpha)=3$, we get
$\max\mathbf{P}(\alpha)^{2}\cdot(\max\textsc{Const}(\alpha)+p\cdot
4^{\max\mathbf{P}(\alpha)})\leqslant\max\textsc{Const}(\alpha)\cdot
2^{p+3\cdot\max\mathbf{P}(\alpha)}$ as well since $2p\leqslant 2^{p}$ so that
the desired estimation holds in this case, too.

Now, by induction on the quantifier depth we can obtain the following theorem.

######  Theorem 13.

Let $\varphi\in\mathrm{FO}\bigl{[}\exists^{(q,p)}x]$ be a formula of
quantifier-depth $d$. There exists an equivalent Boolean combination $\gamma$
of atomic formulas with

$\displaystyle\max\mathbf{P}(\gamma)$
$\displaystyle\leqslant\max\mathbf{P}(\varphi)^{4^{d}}\,,\text{ and }$
$\displaystyle\max\textsc{Const}(\gamma)$ $\displaystyle\leqslant
2^{(\max\mathbf{P}(\varphi))^{4^{d}}}\cdot\max\textsc{Const}(\varphi)\,.$

######  Proof 4.8.

The proof proceeds by induction on $d$. For $d=0$, the claim is trivial since
then, we can set $\gamma=\varphi$. Now suppose the theorem has been shown for
formulas of quantifier-depth $<d$.

So let $\varphi=Ex\colon\psi$ where $E=\exists$ or $E=\exists^{(q,p)}$ for
some $0\leqslant q<p$ and the formula $\psi$ has quantifier-rank $<d$. If
$E=\exists$, set $p=1$. Then, by the induction hypothesis, there exists a
Boolean combination $\alpha$ of atomic formulas such that
$\psi\Longleftrightarrow\alpha$,

$\displaystyle\max\mathbf{P}(\alpha)$
$\displaystyle\leqslant(\max\mathbf{P}(\psi))^{4^{d-1}}\text{ and}$
$\displaystyle\max\textsc{Const}(\alpha)$ $\displaystyle\leqslant
2^{(\max\mathbf{P}(\psi))^{4^{d-1}}}\cdot\max\textsc{Const}(\psi)\,.$

By Prop. 12, we find a Boolean combination $\gamma$ of atomic formulas such
that the following hold:

  * •

$\gamma\Longleftrightarrow Ex\colon\alpha\Longleftrightarrow
Ex\colon\psi=\varphi$

  * •

$\max\mathbf{P}(\gamma)\leqslant\max\mathbf{P}(Ex\colon\alpha)^{4}$

  * •

$\max\textsc{Const}(\gamma)\leqslant\max\textsc{Const}(Ex\colon\alpha)\cdot
16^{\max\mathbf{P}(Ex\colon\alpha)}$

Note that $\max\mathbf{P}(Ex\colon\alpha)$ is the maximum of $p\leqslant
p^{4^{d-1}}$ and
$\max\mathbf{P}(\alpha)\leqslant\max\mathbf{P}(\psi)^{4^{d-1}}$. Similarly,
the maximum of $p$ and $\max\mathbf{P}(\psi)$ is equal to
$\max\mathbf{P}(Ex\colon\psi)$. Therefore we get
$\max\mathbf{P}(Ex\colon\alpha)\leqslant\max\mathbf{P}(Ex\colon\psi)^{4^{d-1}}$.
Hence

$\displaystyle\max\mathbf{P}(\gamma)$
$\displaystyle\leqslant\max\mathbf{P}(Ex\colon\alpha)^{4}$
$\displaystyle\leqslant(\max\mathbf{P}(Ex\colon\psi)^{4^{d-1}})^{4}$
$\displaystyle=\max\mathbf{P}(\varphi)^{4^{d}}\,.$

Before we prove the desired upper bound for $\max\textsc{Const}(\gamma)$, note
the following for all $n\geqslant 2$ and $d\geqslant 1$:

$\displaystyle\log_{2}\bigl{(}16^{n^{4^{d-1}}}\cdot 2^{n^{4^{d-1}}}\bigr{)}$
$\displaystyle=4\cdot n^{4^{d-1}}+n^{4^{d-1}}$ $\displaystyle\leqslant
n^{3}\cdot n^{4^{d-1}}$ $\displaystyle=n^{3+4^{d-1}}$ $\displaystyle\leqslant
n^{4^{d}}\,.$

With $n=\max\mathbf{P}(\varphi)$, we therefore obtain

$\displaystyle\max\textsc{Const}(\gamma)$ $\displaystyle\leqslant
16^{\max\mathbf{P}(Ex\colon\alpha)}\cdot\max\textsc{Const}(Ex\colon\alpha)$
$\displaystyle\leqslant 16^{\max\mathbf{P}(\varphi)^{4^{d-1}}}\cdot
2^{\max\mathbf{P}(\varphi)^{4^{d-1}}}\cdot\max\textsc{Const}(\varphi)$
$\displaystyle\leqslant
2^{\max\mathbf{P}(\varphi)^{4^{d}}}\cdot\max\textsc{Const}(\varphi)\,.$

Using Proposition 7, the extension of the above result to the larger logic
$\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x}]$ follows immediately.

######  Corollary 14.

Let $\varphi\in\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x}]$ be a formula
of quantifier-depth $d$. There exists an equivalent Boolean combination
$\gamma$ of atomic formulas with

$\displaystyle\max\mathbf{P}(\gamma)$
$\displaystyle\leqslant\max\mathbf{P}(\varphi)^{4^{d}}\text{ and }$
$\displaystyle\max\textsc{Const}(\gamma)$ $\displaystyle\leqslant
2^{(\max\mathbf{P}(\varphi))^{4^{d}}}\cdot\max\textsc{Const}(\varphi)\,.$

If we allow the threshold counting quantifiers $\exists^{\geqslant c}$ and
$\exists^{=c}$, the result gets a bit weaker since we have to replace the
exponent $d$ in the above bounds by a polynomial in the size of $\varphi$. To
see this, let
$\varphi\in\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x},\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}\bigr{]}$. Then, by Proposition 4, it
can be transformed in polynomial time into an equivalent formula
$\varphi^{\prime}$ from $\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x}]$. The
quantifier depth $d^{\prime}$ of $\varphi^{\prime}$ is bounded by the size of
$\varphi^{\prime}$ and therefore polynomial in the size of $\varphi$. Now we
can resort to the above corollary and obtain

######  Corollary 15.

Let
$\varphi\in\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x},\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}\bigr{]}$ be a formula. There exists an
equivalent Boolean combination $\gamma$ of atomic formulas with

$\displaystyle\max\mathbf{P}(\gamma)$
$\displaystyle\leqslant\max\mathbf{P}(\varphi)^{4^{\mathrm{poly}(|\varphi|)}}\text{
and }$ $\displaystyle\max\textsc{Const}(\gamma)$ $\displaystyle\leqslant
2^{(\max\mathbf{P}(\varphi))^{4^{\mathrm{poly}(|\varphi|)}}}\cdot\max\textsc{Const}(\varphi)\,.$

##  5\. An efficient decision procedure

Let $\varphi(x)$ be a Boolean combination of formulas with a single free
variable. To determine validity of the formula $\exists x\colon\varphi$, one
has to check, for all integers $n\in{\mathbb{Z}}$, whether $\varphi(n)$ holds.
The following lemma reduces this infinite search space to a finite one that is
exponential in the coefficients and moduli as well as linear in the constants
from $\varphi$.

######  Lemma 16.

Let $A\geqslant 6$ and $B\geqslant 0$. Let $x$ be a variable and $\gamma$ a
Boolean combination of atomic formulas of the form $ax>b$, $ax<b$, and
$cx\equiv_{h}d$ with $a,b,c,d\in{\mathbb{Z}}$, $h\geqslant 2$, $|a|,h<A$, and
$|b|<B$. Then $\exists x\colon\gamma$ is equivalent to $\exists
x\colon\bigl{(}|x|\leqslant A^{A^{5}}\cdot B\land\gamma\bigr{)}$.

######  Proof 5.1.

Since $h<A$, we can assume that $0\leqslant c,d<A$ for all formulas of the
form $cx\equiv_{h}d$. We can also assume that $\gamma$ is in negation normal
form, i.e., only atomic formulas are negated. We make the following
replacements:

$\neg(ax>b)$ | is replaced by | $ax<b+1$
---|---|---
$\neg(cx\equiv_{h}d)$ | is replaced by | $\bigvee_{0\leqslant d^{\prime}<h,d\neq d^{\prime}}cx\equiv_{h}d^{\prime}$
$ax>b$ | is replaced by | $-ax<-b$

As a result, $\gamma$ is equivalent to a formula in disjunctive normal form,
without negations, and with atomic formulas of the form $ax<b$ and
$cx\equiv_{h}d$ with $0\leqslant c,d,|a|,h<A$ and $|b|\leqslant B$. Hence
$\gamma\Longleftrightarrow\bigvee_{1\leqslant i\leqslant n}\delta_{i}$ where
each of the formulas $\delta_{i}$ is a conjunction of atomic formulas of the
allowed form. Consequently, $\exists x\colon\gamma$ is equivalent to
$\bigvee_{1\leqslant i\leqslant n}\exists x\colon\delta_{i}$.

Consider one such conjunction $\delta_{i}$. Note that it contains at most
$A^{3}$ many atomic formulas of the form $cx\equiv_{h}d$ since $0\leqslant
c,d,h<A$. For any such atomic formula, introduce a new variable $y$ and
replace $cx\equiv_{h}d$ by $cx-hy=d$. Then $\delta_{i}$ is equivalent to
$\exists\overline{y}\colon\delta^{\prime}_{i}$ where $\delta^{\prime}_{i}$ is
a conjunction of formulas of the form $cx-hy=d$ and $ax<b$ with $0\leqslant
c,h,d,|a|<A$ and $|b|\leqslant B$ and $\overline{y}$ is a sequence of at most
$A^{3}$ variables.

Let $M$ be the maximal absolute value of the determinant of an $(m\times
m)$-matrix with $m\leqslant A^{3}+2$, where the first $m-1$ columns contain
entries of absolute value at most $A$ and the entries in the last column have
absolute value at most $B$. Then it is not hard to determine that

$M\leqslant(A^{3}+2)!\cdot A^{A^{3}+1}\cdot B\,.$

Now the main theorem of [VS78] implies that the formula $\exists
x,\overline{y}\colon\delta^{\prime}$ is equivalent to the existence of a
solution $(x,\overline{y})$ of $\delta^{\prime}$ where the absolute value of
every entry is at most

$\displaystyle(A^{3}+2)\cdot M$ $\displaystyle\leqslant
A^{4}\cdot(A^{4})!\cdot A^{A^{4}}\cdot B$ $\displaystyle\leqslant
A^{4}\cdot(A^{4})^{A^{4}}\cdot A^{A^{4}}\cdot B$ $\displaystyle\leqslant
A^{4+5\cdot A^{4}}\cdot B\leqslant A^{A^{5}}\cdot B\,.$

In summary, we get

$\displaystyle\exists x\colon\gamma$
$\displaystyle\Longleftrightarrow\bigvee\exists x\colon\delta_{i}$
$\displaystyle\Longleftrightarrow\bigvee\exists
x\exists\overline{y}\colon\delta_{i}^{\prime}$
$\displaystyle\Longleftrightarrow\bigvee\exists x\colon\bigl{(}|x|\leqslant
A^{A^{5}}\cdot B\land\exists\overline{y}\colon\delta_{i}^{\prime}\bigr{)}$
$\displaystyle\Longleftrightarrow\exists x\colon\bigl{(}|x|\leqslant
A^{A^{5}}\cdot B\land\bigvee\delta_{i}\bigr{)}$
$\displaystyle\Longleftrightarrow\exists x\colon\bigl{(}|x|\leqslant
A^{A^{5}}\cdot B\land\gamma\bigr{)}$

where all disjunctions extend over $1\leqslant i\leqslant n$.

The core of the above lemma is the reduction of the search space for closed
formulas of the form $\exists x\colon\varphi(x)$ with $\varphi$ quantifier-
free. The following corollary provides an analogous reduction for arbitrary
formulas $\varphi(x)$. In addition, we allow the formula $\varphi$ to have
further free variables $y_{1},\dots,y_{\ell}$ that are handled as parameters.

######  Corollary 17.

There exists $\kappa\geqslant 2$ with the following property. Let $d\geqslant
1$ and consider a formula $\varphi(x,y_{1},\dots,y_{\ell})$ from
$\mathrm{FO}\bigl{[}\exists^{(q,p)}x]$ of quantifier-depth at most $d$. Let
$n_{1},\dots,n_{\ell}\in{\mathbb{Z}}$ with $|n_{i}|\leqslant N$. Then the
closed formula $\exists x\colon\varphi(x,n_{1},\dots,n_{\ell})$ holds if and
only if there exists $n\in{\mathbb{Z}}$ such that
$\varphi(n,n_{1},\dots,n_{\ell})$ holds with

$\displaystyle|n|\leqslant
2^{\max\mathbf{P}(\varphi)^{\kappa^{d}}}\cdot\max\textsc{Const}(\varphi)\cdot
N\cdot\max\\{1,\ell\\}\,.$

######  Proof 5.2.

The implication “$\Leftarrow$” is trivial since, if there is a small $n$
satisfying $\varphi(x,n_{1},\dots,n_{\ell})$, then $\exists
x\colon\varphi(x,n_{1},\dots,n_{\ell})$ holds.

Conversely suppose $\exists x\colon\varphi(x,n_{1},\dots,n_{\ell})$ holds. Let
$\varphi_{\overline{n}}=\varphi_{\overline{n}}(x)$ be the formula obtained
from $\varphi$ by substituting $n_{i}$ for $y_{i}$. For any inequality $s<t$
in $\varphi$, the term $s-t$ contains at most $\ell$ of the variables $y_{i}$,
each with a coefficient from
$\textsc{Coeff}(\varphi)\subseteq\mathbf{P}(\varphi)$. Hence these
substitutions at most eliminate coefficients, do not change moduli, but can
increase constants by $N\cdot\ell\cdot\max\mathbf{P}(\varphi)$. Hence we get

$\displaystyle\max\mathbf{P}(\varphi_{\overline{n}})$
$\displaystyle\leqslant\max\mathbf{P}(\varphi)\ \text{and}$
$\displaystyle\max\textsc{Const}(\varphi_{\overline{n}})$
$\displaystyle\leqslant\max\textsc{Const}(\varphi)+N\cdot\ell\cdot\max\mathbf{P}(\varphi)\,.$

By Theorem 13, there exists an equivalent Boolean combination
$\gamma_{\overline{n}}$ of atomic formulas with

$\displaystyle\max\mathbf{P}(\gamma_{\overline{n}})$
$\displaystyle\leqslant\max\mathbf{P}(\varphi)^{4^{d}}=:A\ \text{and }$
$\displaystyle\max\textsc{Const}(\gamma_{\overline{n}})$
$\displaystyle\leqslant
2^{\max\mathbf{P}(\varphi)^{4^{d}}}\cdot(\max\textsc{Const}(\varphi)+N\cdot\ell\cdot\max\mathbf{P}(\varphi))$
$\displaystyle\leqslant
2^{\max\mathbf{P}(\varphi)^{5^{d}}}\cdot\max\textsc{Const}(\varphi)\cdot
N\cdot\max\\{1,\ell\\}=:B\,.$

From Lemma 16, we obtain that there is some $n\in{\mathbb{Z}}$ with
$|n|\leqslant A^{A^{5}}\cdot B$ such that $\gamma_{\overline{n}}(n)$ holds.
Hence, for this $n$, also $\varphi(n,n_{1},\dots,n_{\ell})$ holds. Note that
we have (with $p=\max\mathbf{P}(\varphi)$)

$A^{A^{5}}\leqslant\left(p^{4^{d}}\right)^{\left(p^{4^{d}}\right)^{5}}=p^{4^{d}\cdot
p^{5\cdot 4^{d}}}\leqslant p^{p^{5\cdot 4^{d}+2d}}\leqslant
2^{p^{c^{d}}}=2^{\max\mathbf{P}(\varphi)^{c^{d}}}$

for some $c\geqslant 1$ and therefore

$\displaystyle|n|$ $\displaystyle\leqslant
2^{\max\mathbf{P}(\varphi)^{c^{d}}}\cdot
2^{\max\mathbf{P}(\varphi)^{5^{d}}}\cdot\max\textsc{Const}(\varphi)\cdot
N\cdot\max\\{1,\ell\\}$ $\displaystyle\leqslant
2^{\max\mathbf{P}(\varphi)^{\kappa^{d}}}\cdot\max\textsc{Const}(\varphi)\cdot
N\cdot\max\\{1,\ell\\}$

for some $\kappa\geqslant 2$.

In the following, we want to prove a similar result for the modulo-counting
quantifier. Recall that $\exists^{(q,p)}x\colon\varphi(x)$ can only be true if
$\varphi$ has only finitely many witnesses, i.e., if the formula $\exists
y\forall x\colon\bigl{(}\varphi(x)\to|x|\leqslant y\bigr{)}$ is true. Applying
the above corollary, one finds a finite interval such that $\varphi$ has
infinitely many witnesses iff it has at least one witness in this interval. In
case $\varphi$ has only finitely many witnesses, then all of them are of
bounded absolute value. More precisely, we get the following.

######  Lemma 18.

Let $d\geqslant 1$ and $\kappa\geqslant 2$ be the constant from Corollary 17.
Furthermore, let
$\varphi=\varphi(x,y_{1},\dots,y_{\ell})\in\mathrm{FO}\bigl{[}\exists^{(q,p)}x]$
be a formula of quantifier-depth at most $d$, let
$n_{1},\dots,n_{\ell}\in{\mathbb{Z}}$ with $|n_{i}|\leqslant N$. Suppose there
exist only finitely many $n\in{\mathbb{Z}}$ such that
$\varphi(n,n_{1},\dots,n_{\ell})$ holds. Then all $n\in{\mathbb{Z}}$ such that
$\varphi(n,n_{1},\dots,n_{\ell})$ holds satisfy

$|n|\leqslant
2^{\max\mathbf{P}(\varphi)^{\kappa^{d+1}}}\cdot\max\textsc{Const}(\varphi)\cdot
N\cdot\max\\{1,\ell\\}\,.$

######  Proof 5.3.

Since there are only finitely many $n\in{\mathbb{Z}}$ such that
$\varphi(n,n_{1},\dots,n_{\ell})$ holds, the closed formula

$\exists y\forall
x\colon\bigl{(}\varphi(x,n_{1},\dots,n_{\ell})\to|x|\leqslant y\bigr{)}$ (3)

holds. Let $\varphi^{\prime}$ denote the subformula starting with $\forall x$.
Note that its quantifier-depth equals $d+1$,
$\mathbf{P}(\varphi)=\mathbf{P}(\varphi^{\prime})$, and
$\textsc{Const}(\varphi)=\textsc{Const}(\varphi^{\prime})$. Hence, by
Corollary 17, the above formula (3) is equivalent to

$\exists y\colon\bigl{(}|y|\leqslant
2^{\max\mathbf{P}(\varphi)^{\kappa^{d+1}}}\cdot\max\textsc{Const}(\varphi)\cdot
N\cdot\max\\{1,\ell\\}\land\varphi^{\prime}\bigr{)}$

and therefore to

$\forall x\colon\bigl{(}\varphi(x,n_{1},\dots,n_{\ell})\to|x|\leqslant
2^{\max\mathbf{P}(\varphi)^{\kappa^{d+1}}}\cdot\max\textsc{Const}(\varphi)\cdot
N\cdot\max\\{1,\ell\\}\bigr{)}\,.$

Now the claim follows since the formula (3) and therefore this formula holds.

######  Corollary 19.

Let $d\geqslant 1$ and $\kappa$ be the constant from Corollary 17 and

$C=2^{\max\mathbf{P}(\varphi)^{\kappa^{d+1}}}\cdot\max\textsc{Const}(\varphi)\cdot
N\cdot\max\\{1,\ell\\}\,.$

Let
$\varphi=\varphi(x,y_{1},\dots,y_{\ell})\in\mathrm{FO}\bigl{[}\exists^{(q,p)}x]$
be a formula of quantifier-depth at most $d$, let
$n_{1},\dots,n_{\ell}\in{\mathbb{Z}}$ with $|n_{i}|\leqslant N$. Then
$\exists^{(q,p)}x\colon\varphi(x,n_{1},\dots,n_{\ell})$ is true if and only if
the following hold:

  1. (1)

no integer $n$ with $C<|n|\leqslant C^{2}$ makes
$\varphi(n,n_{1},\dots,n_{\ell})$ true and

  2. (2)

$\bigl{|}\\{n\in{\mathbb{Z}}\colon|n|\leqslant C\text{ and
}\varphi(n,n_{1},\dots,n_{\ell})\text{ is true}\\}\bigr{|}\equiv_{p}q$ .

######  Proof 5.4.

We first show that $\exists^{(q,p)}x\colon\varphi(x,n_{1},\dots,n_{\ell})$ is
true if and only if

  1. (a′)

$\forall x\colon\bigl{(}\varphi(x,n_{1},\dots,n_{\ell})\to|x|\leqslant
C\bigr{)}$ is true and

  2. (b)

$\bigl{|}\\{n\in{\mathbb{Z}}\colon|n|\leqslant C\text{ and
}\varphi(n,n_{1},\dots,n_{\ell})\text{ is true}\\}\bigr{|}\equiv_{p}q$ .

Suppose there are infinitely many integers $n$ such that
$\varphi(n,n_{1},\dots,n_{\ell})$ holds. Then the formula
$\exists^{(q,p)}x\colon\varphi$ does not hold. Furthermore, statement (a′) is
false since there are only finitely many integers $x$ with $|x|\leqslant C$.
Hence, in this case, the equivalence holds.

So it remains to consider the case that there are only finitely many integers
$n$ such that $\varphi(n,n_{1},\dots,n_{\ell})$ holds. Then, by Lemma 18, all
these integers satisfy $|n|\leqslant C$. Consequently, statement (a′) is true
and

$\bigl{\\{}n\in{\mathbb{Z}}\bigm{|}\varphi(n,n_{1},\dots,n_{\ell})\text{
holds}\bigr{\\}}=\bigl{\\{}n\in{\mathbb{Z}}\colon|n|\leqslant C\text{ and
}\varphi(n,n_{1},\dots,n_{\ell})\text{ holds}\bigr{\\}}\,.$

Hence, in this case, $\exists^{(q,p)}x\colon\varphi$ is equivalent to
statement (b). Since (a′) is true in this case, we have the equivalence.

We complete the proof of this corollary by showing that (a) and (a′) are
equivalent. Consider the formula

$\varphi^{\prime}=\bigl{(}\varphi(x,x_{1},\dots,x_{\ell})\land|x|>C\bigr{)}\,.$

Then $\mathbf{P}(\varphi^{\prime})=\mathbf{P}(\varphi)$ and
$\textsc{Const}(\varphi^{\prime})=\textsc{Const}(\varphi)\cup\\{\pm C\\}$
implying $\max\textsc{Const}(\varphi^{\prime})=C$. Hence, by Corollary 17,
$\exists x\colon\varphi^{\prime}$ is equivalent to the existence of
$n\in{\mathbb{Z}}$ satisfying $\varphi(x,n_{1},\dots,n_{\ell})$ with $C<|n|$
and

$\displaystyle|n|$ $\displaystyle\leqslant
2^{\max\mathbf{P}(\varphi^{\prime})^{\kappa^{d}}}\cdot\max\textsc{Const}(\varphi^{\prime})\cdot
N\cdot\max\\{1,\ell\\}$
$\displaystyle=2^{\max\mathbf{P}(\varphi)^{\kappa^{d}}}\cdot C\cdot
N\cdot\max\\{1,\ell\\}$ $\displaystyle\leqslant C^{2}\,.$

Hence, statement (a′), i.e., $\neg\exists x\colon\varphi^{\prime}$, is
equivalent to statement (a).

Corollaries 17 and 19 allow to compute the truth value of a closed formula
$\varphi$ from $\mathrm{FO}\bigl{[}\exists^{(q,p)}x]$ by, recursively,
computing the truth value of subformulas $\psi$ of $\varphi$ with arguments of
bounded size. More precisely, let $d$ be the quantifier depth of $\varphi$ and
set

$D=2^{\max\mathbf{P}(\varphi)^{\kappa^{d+2}}}\cdot\max\textsc{Const}(\varphi)\,.$
(4)

Note that $\max\mathbf{P}(\varphi),\kappa\geqslant 2$ implying $D\geqslant d$.

Now suppose $\exists x\colon\psi(x,y_{1},\dots,y_{\ell})$ is a subformula of
$\varphi$, $d^{\prime}$ is the quantifier depth of $\psi$, and
$n_{1},\dots,n_{\ell}$ are integers. Then to determine the truth of $\exists
x\colon\psi(x,n_{1},\dots,n_{\ell})$, it suffices by Corollary 17 to verify
the truth of $\psi(n,n_{1},\dots,n_{\ell})$ for all integers $n$ with

$\displaystyle|n|$ $\displaystyle\leqslant
2^{\max\mathbf{P}(\psi)^{\kappa^{d^{\prime}}}}\cdot\max\textsc{Const}(\psi)\cdot\max\\{|n_{1}|,\dots,|n_{\ell}|\\}\cdot\max\\{1,\ell\\}$
$\displaystyle\leqslant
2^{\max\mathbf{P}(\varphi)^{\kappa^{d}}}\cdot\max\textsc{Const}(\varphi)\cdot\max\\{|n_{1}|,\dots,|n_{\ell}|\\}\cdot
d$ $\displaystyle\leqslant D\cdot\max\\{|n_{1}|,\dots,|n_{\ell}|\\}\,,$ which,
for later purposes, can be bounded by $\displaystyle\leqslant
D^{2}\cdot\max\\{|n_{1}|,\dots,|n_{\ell}|\\}^{2}\,.$

Similarly, suppose $\exists^{(q,p)}x\colon\psi(x,y_{1},\dots,y_{\ell})$ is a
subformula of $\varphi$, $d^{\prime}$ is the quantifier depth of $\psi$, and
$n_{1},\dots,n_{\ell}$ are integers. Then to determine the truth of
$\exists^{(q,p)}x\colon\psi(x,n_{1},\dots,n_{\ell})$, it suffices by Corollary
19 to verify the truth of $\psi(n,n_{1},\dots,n_{\ell})$ for all integers $n$
with

$\displaystyle|n|$
$\displaystyle\leqslant\bigl{(}2^{\max\mathbf{P}(\psi)^{\kappa^{d^{\prime}+1}}}\cdot\max\textsc{Const}(\psi)\cdot\max\\{|n_{1}|,\dots,|n_{\ell}|\\}\cdot\max\\{1,\ell\\}\bigr{)}^{2}$
$\displaystyle\leqslant\bigl{(}2^{\max\mathbf{P}(\varphi)^{\kappa^{d+1}}}\cdot\max\textsc{Const}(\varphi)\cdot\max\\{|n_{1}|,\dots,|n_{\ell}|\\}\cdot
d\bigr{)}^{2}$ $\displaystyle\leqslant
D^{2}\cdot\max\\{|n_{1}|,\dots,|n_{\ell}|\\}^{2}\,.$

By induction, we obtain that all recursive calls of the evaluation procedure
use integers of size at most

$\displaystyle D^{4^{d}}$
$\displaystyle=\left(2^{\max\mathbf{P}(\varphi)^{\kappa^{d+2}}}\cdot\max\textsc{Const}(\varphi)\right)^{4^{d}}$
$\displaystyle\leqslant
2^{\max\mathbf{P}(\varphi)^{\kappa^{cd}}}\cdot\max\textsc{Const}(\varphi)^{4^{d}}\,,$

where $c$ is some constant. To store any such integer, one needs space
$4^{d}\log D$. When evaluating a closed formula of quantifier depth $d$, one
has to store at most $d$ variables at once. Therefore we get the following.

######  Proposition 20.

Satisfaction of a closed formula
$\varphi\in\mathrm{FO}\bigl{[}\exists^{(q,p)}x]$ of quantifier-depth $d$ can
be decided in space $O(4^{d}\cdot\log D)$ with $D$ given by Equation (4).

Let $\varphi\in\mathrm{FO}\bigl{[}\exists^{(q,p)}x]$. Then the quantifier
depth $d$ is at most $|\varphi|$. Since coefficients etc. are written in
binary, $\max\mathbf{P}(\varphi)$ and $\max\textsc{Const}(\varphi)$ are
bounded by $2^{|\varphi|}$. Consequently, the proposition shows that
satisfaction of closed formulas
$\varphi\in\mathrm{FO}\bigl{[}\exists^{(q,p)}x]$ can be decided in space
doubly exponential in $|\varphi|$.

Recall that for formulas from $\mathrm{FO}\bigl{[}\exists^{(q,p)}x]$ we
require modulo-counting quantifiers of the form
$\exists^{(t,p)}(y_{1},\dots,y_{\ell})$ to satisfy $t\in{\mathbb{N}}$ and
$\ell=1$. We now show that also without this restriction, the doubly
exponential space bound remains true.

######  Theorem 21.

Satisfaction of a closed formula
$\varphi\in\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x}]$ can be decided in
space doubly exponential in $|\varphi|$.

######  Proof 5.5.

Let $\varphi\in\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x}]$ be a closed
formula. By Proposition 7, we can compute in doubly exponential time an
equivalent closed formula $\gamma\in\mathrm{FO}\bigl{[}\exists^{(q,p)}x]$
without changing the sets of coefficients, moduli, or constants and without
increasing the quantifier depth. Because of the time bound, this construction
requires at most doubly exponential space and $|\gamma|$ is at most doubly
exponential in $|\varphi|$.

By Proposition 20, validity of $\gamma$ can be decided using space
$O(4^{\mathrm{qd}(\gamma)}\cdot\log D)$ with $D$ given by Equation (4). Since
$\gamma$ and $\varphi$ agree on the sets of coefficients etc. and on the
quantifier depth, this value is doubly exponential in the size of $\varphi$.

Since Proposition 4 allows to translate formulas from
$\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x},\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}\bigr{]}$ into equivalent formulas from
$\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x}]$ in polynomial time, we also
get the corresponding result for the logic
$\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x},\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}\bigr{]}$.

######  Corollary 22.

Satisfaction of a closed formula
$\varphi\in\mathrm{FO}\bigl{[}\exists^{(t,p)}\overline{x},\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}\bigr{]}$ can be decided in space
doubly exponential in $|\varphi|$.

Note that this complexity matches the best known upper space bound for
Presburger arithmetic without modulo-counting quantifiers from [FR79]. From
[Ber80], we know that Presburger arithmetic can be decided in alternating
doubly exponential time with linearly many alternations (and our Corollary 5
extends this to the logic $\mathrm{FO}[\exists^{\geqslant
c}\overline{x},\exists^{=c}\overline{x}]$). Our handling of the modulo-
counting quantifier requires us to count witnesses of bounded size. As the
number of potential witnesses is triply exponential, we do not see how to do
this using an alternating Turing machine in only doubly exponential time.

## References

  * [Ape66] H. Apelt.  Axiomatische Untersuchungen über einige mit der Presburgerschen Arithmetik verwandten Systeme.  Zeitschr. f. math. Logik und Grundlagen d. Math., 12:131–168, 1966\.  doi:10.1002/malq.19660120111.
  * [Ber80] L. Berman.  The complexity of logical theories.  Theoretical Computer Science, 11:71–77, 1980.  doi:10.1016/0304-3975(80)90037-7.
  * [CHM21] D. Chistikov, C. Haase, and A. Mansutti.  Presburger arithmetic with threshold counting quantifiers is easy, 2021\.  doi:10.48550/arXiv.2103.05087.
  * [CHM22] D. Chistikov, C. Haase, and A. Mansutti.  Quantifier elimination for counting extensions of Presburger arithmetic.  In FoSSaCS’22, volume 13242 of Lecture Notes in Comp. Science, pages 225–243. Springer, 2022.  doi:10.1007/978-3-030-99253-8_12.
  * [FR74] M.J. Fischer and M.O. Rabin.  Super-exponential complexity of Presburger arithmetic.  In Complexity of Computation, SIAM-AMS Proc. Vol. VII, pages 27–41. AMS, 1974.
  * [FR79] J. Ferrante and C. W. Rackoff.  The computational complexity of logical theories.  Lecture Notes in Mathematics vol 718. Springer-Verlag Berlin Heidelberg, 1979.  doi:10.1007/BFb0062837.
  * [Grä88] E. Grädel.  Subclasses of Presburger arithmetic and the polynomial-time hierarchy.  Theoretical Computer Science, 56:289–301, 1988.  doi:10.1016/0304-3975(88)90136-3.
  * [Haa14] C. Haase.  Subclasses of Presburger arithmetic and the weak EXP hierarchy.  In CSL-LICS ’14. ACM, 2014.  doi:10.1145/2603088.2603092.
  * [Här62] K. Härtig.  Über einen Quantifikator mit zwei Wirkungsbereichen.  In L. Kalmár, editor, Colloquium on the foundations of mathematics, mathematical machines and their applications, pages 31–36. Akadémiai Kiadó, Budapest, 1962.
  * [HK15] P. Habermehl and D. Kuske.  On Presburger arithmetic extended with modulo counting quantifiers.  In FoSSaCS’15, Lecture Notes in Comp. Science vol. 9034, pages 375–389. Springer, 2015.  doi:10.1007/978-3-662-46678-0_24.
  * [HKPV91] H. Herre, M. Krynicki, A. Pinus, and J. Väänänen.  The Härtig quantifier: A survey.  The Journal of Sybmolic Logic, 56(4):1153–1183, 1991.  doi:10.2307/2275466.
  * [Kla08] F. Klaedtke.  Bounds on the Automata Size for Presburger Arithmetic.  ACM Trans. Comput. Logic, 9(2):1–34, 2008.  doi:10.1145/1342991.1342995.
  * [Nai82] M. Nair.  On Chebyshev-type inequalities for primes.  The American Mathematical Monthly, 89(2):126–129, 1982.  doi:10.2307/2320934.
  * [Opp78] D. C. Oppen.  A $2^{2^{2^{pn}}}$ upper bound on the complexity of Presburger arithmetic.  J. Comput. Syst. Sci., 16(3):323–332, 1978.  doi:10.1016/0022-0000(78)90021-1.
  * [Pre30] M. Presburger.  Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt.  In Sprawozdanie z 1 Kongresu Matematyków Krajow Slowiańskich, Ksiaznica Atlas, pages 92–101. Warzaw, 1930.  For an English translation see [Pre91].
  * [Pre91] M. Presburger.  On the completeness of a certain system of arithmetic of whole numbers in which addition occurs as the only operation.  Hist. Philos. Logic, 12:225–233, 1991.  English translation of [Pre30].  doi:10.1080/014453409108837187.
  * [RL78] C. R. Reddy and D. W. Loveland.  Presburger arithmetic with bounded quantifier alternation.  In ACM Symposium on Theory of Computing, pages 320–325, 1978\.  doi:10.1145/800133.804361.
  * [Sch97] U. Schöning.  Complexity of Presburger arithmetic with fixed quantifier dimension.  Theory Comput. Syst., 30(4):423–428, 1997.  doi:10.1007/BF02679468.
  * [Sch05] N. Schweikardt.  Arithmetic, first-order logic, and counting quantifiers.  ACM Trans. Comput. Log., 6(3):634–671, 2005.  doi:10.1145/1071596.1071602.
  * [VS78] J. Von Zur Gathen and M. Sieveking.  A bound on solutions of linear integer equalities and inequalities.  Proc. AMS, 72:155–158, 1978.  doi:10.2307/2042554.