# The complexity of the first-order theory of pure equality111Mathematics
Subject Classification. 03C40, 03C07, 03D15.

Ivan V<EMAIL_ADDRESS>
###### Abstract

We will find a lower bound on the recognition complexity of the theories that
are nontrivial relative to equality (or equational-nontrivial), namely, each
of these theories is consistent with the formula, whose sense is that there
exist two various elements at least. However, at first, we will obtain a lower
bound on the computational complexity for the first-order theory of Boolean
algebra that has only two elements. For this purpose, we will code the long-
continued deterministic Turing machine computations by the relatively short-
length quantified Boolean formulae; the modified Stockmeyer and Meyer method
will appreciably be used for this simulation. Then, we will construct a
polynomial reduction of the theory of this Boolean algebra to the first-order
theory of the pure equality.

Key words: Computational complexity, the theory of equality, the coding of
computations, simulation by means formulae, polynomial time, polynomial space,
lower complexity bound

##  1 Introduction

At the beginning, we recall some designations. A function $\exp_{k}(n)$ is
called $k$-iterated or $k$-story exponential, if, for every natural $k$, it is
calculated in the following way: $\exp_{0}(n)\\!=\\!2^{n}$,
$\exp_{k+1}(n)\\!=\\!2^{\exp_{k}(n)}$ [19]. The length of a word $X$ is
denoted by $|X|$, i.e., $|X|$ is the number of symbols in $X$. If $A$ is a
set, then $|A|$ denotes its cardinality; ”$A\rightleftharpoons\mathcal{A}$”
means ”$A$ is a designation for $\mathcal{A}$”; and
$\exp(n)\rightleftharpoons\exp_{1}(n)$.

###  1.1 Problem statement

The results on the complexity of recognition (or computational complexity) for
many of the decidable theories are well-known [7, 12, 13, 14, 15, 16, 17]. We
recall only some of these results concerning first-order theories.

Any decision procedure has more than an exponential complexity for the theory
$ThRLC$ of the field $\mathbb{R}$ of real numbers, and even for
$Th(\mathbb{R},+)$ [7], namely, there exists a rational constant $d_{1}>0$,
such that if $P$ is a deterministic Turing machine which recognizes the theory
$ThRLC$ (or $Th((\mathbb{R},+))$), then the $P$ runs for at least
$2^{d_{1}|\varphi|}$ steps when started on input $\varphi$, for infinitely
many sentences $\varphi$; and so, the complexity of recognition for these
theories (which corresponds to the concept of inner complexity as defined in
[15]) is more than $\exp(d_{1}n)$, here and below, the variable $n$ is the
length of the input string; and the letter $d$ with subscripts denotes a
suitable constant. In other words, $ThRLC$ and $Th(R,+)$ do not belong to
$DTIME(\exp(d_{1}n))$. For Presburger arithmetic $PAR$ (the theory of natural
numbers with addition) and for Skolem arithmetic $SAR$ (the theory of natural
numbers with multiplication), the recognition complexity is more than a double
exponential: $PAR,SAR\\!\notin\\!DTIME(\exp_{2}(d_{2}n))$. For the theory of
linearly ordered sets $ThOR$, the computational complexity is very great [13]:
$ThOR\\!\notin\\!DTIME(\exp_{\lfloor d_{3}n\rfloor}(n))$, where $\lfloor
y\rfloor$ is the integer part of a number $y$.

It is quite natural to expect that if we go beyond the confines of logical
theories of the first order, then we can see more impressive lower bounds on
the recognition complexity of theories. An example of such an estimate is the
lower bound for the weak monadic second-order theory of one successor $WSIS$,
other examples can be found in [4, 12, 15, 17]. However, according to the
author, the most impressive estimate of this kind was obtained by Vorobyev
S.G. [19] for the type theory $\Omega$, which is a rudimentary fragment of the
theory of propositional types due to Henkin:
$\Omega\\!\notin\\!DSPACE(\exp_{\infty}(\exp(d_{4}n)))$, hence
$\Omega\\!\notin\\!DTIME(\exp_{\infty}(\exp(d_{4}n)))$, where the function
$\exp_{\infty}$ is recursively defined by $\exp_{\infty}(0)\\!=\\!1$ and
$\exp_{\infty}(k\\!+\\!1)\\!=\\!2^{\exp_{\infty}(k)}$, i.e., this lower bound
has the exponentially growing stack of twos.

And what is the recognition complexity of the simplest (in the semantic and
syntactical sense), but non-trivial theories? Should it be polynomial? In
other words, shall such theories be quickly decidable?

It is clear that one of the simplest theory is the first-order theory of the
algebraic structure of two elements with a unique equality predicate. We will
see in Section 7 that even this theory does not have a polynomial upper bound
of computational complexity. We will in passing obtain the lower bounds on the
recognition complexity of the theories that are nontrivial relatively to some
equivalence relation $\backsim$, namely, these theories have models with at
least two elements that are not $\backsim$-equivalent. Obvious examples of
such theories are the theories of pure equality and of one equivalence
relation.

Since the lower bound on the computational complexity of these theories is not
polynomial, we obtain that the class $\mathbf{P}$ is a proper subclass of
$\mathbf{PSPACE}$.

###  1.2 Used methods and the main idea

The lower bounds on the computational complexity for the theories mentioned in
previous subsection and some others were yielded by the techniques of the
efficient reducibility of the machines to the formulae in [7, 12, 13, 14, 15,
16, 17, 19], or more precisely, by methods of the immediate codings of the
machine actions. The essence of these methods 333We will call it the Rabin and
Fischer method or the technique for modeling of computations by means formulae
is as follows [15]. Let $T$ be the theory, under study, written in the
signature (or underlying language [15]) $\sigma$. Assume that, for any input
string $X$ and every program $P$ of the Turing machine, one can write a
sentence $S(P,X)$, of the $\sigma$, satisfying the following conditions. There
exist a constant $d\\!>\\!0$ and a function $f$ such that: (i)
$|S(P,X)|\\!<\\!d(|X|\\!+\\!|P|)$; (ii) $S(P,X)\\!\in\\!T$ if and only if a
computation by the program $P$ accepts the input $X$ in fewer than $f(|X|)$
steps; (iii) the formula $S(P,X)$ can be effectively constructed from $X$ and
$P$ in fewer than $g(|X|\\!+\\!|P|)$ steps, where $g(k)$ is a fixed
polynomial. If $f(k)$ is a function growing at least at exponential rate, then
under the above conditions, there exist a constant $C\\!>\\!0$ and infinitely
many sentences $\varphi$ of $\sigma$, for which every Turing machine requires
at least $f(C|\varphi|)$ steps to decide whether $\varphi\\!\in\\!T$, i.e.,
$T\\!\notin\\!DTIME(f(Cn))$.

The proof of the last statement is based on a well-known diagonal argument,
though we will below scrutinize this method in more detail and in a somewhat
more general form than this was done in the previous paragraph or in
Subsection 4.1 in [15]. We need the more general form of this technique for
the following reason.

Our main purpose is to evaluate the computational complexity of an equality
theory $Th\mathcal{E}$ (Section 7). However, at first, we will obtain a lower
bound on recognition complexity for the first-order theory of Boolean algebra
$\mathcal{B}$ that has only two elements, using the Rabin and Fischer method.
Then, we will construct a polynomial reduction of the $Th\mathcal{B}$ to
$Th\mathcal{E}$. In Subsection 8.1, we will explain why such a succession of
actions is applied.

But the first-order theory of two-element Boolean algebra has a very weak
expressive ability. Therefore, the modeling sentence for this theory, i.e.,
the formula possessing property (ii) from the method described above, does not
turn out to be very short, it may have not a linear restriction on its length
(see Subsection 6.4 for more details). Furthermore, the $Th\mathcal{B}$ is so
poor and meager that there can, in general, be a doubt about the very
possibility of the simulation of the sufficiently long computations by means
of the relatively short formulae of this theory.

Nevertheless, such a modeling was well-known a long time ago. Stockmeyer L.J.
and Meyer A.R. showed in 1973 that a language $TQBF$444The problem
corresponding to this language is designated as $QBF$, or sometimes $QSAT$.
consisting of the true quantified Boolean formulae is polynomially complete in
the class $\mathbf{PSPACE}$ [9, 18]. This implies in particular that for every
language $\mathcal{L}$ in this class, there is an algorithm, which produces a
quantified Boolean formula for any input string in polynomial time; and all
these sentences model the computations that recognize the $\mathcal{L}$ and
use the polynomial amount of space. Namely, each of theirs is true if and only
if the given input string belongs to the language under study; at that, the
long enough computations are simulated, seeing that the polynomial constraint
on memory allows the machine to run during the exponential-long time [1, 2,
9].

Stockmeyer L.J. and Meyer A.R. have employed the highly ingenious technique
for the implementation of this simulation (see the proof of Theorem 4.3 in
[18]). Their approach permits writing down a polynomially bounded formula for
the modeling of the exponential quantity of the Turing machine steps provided
that one step is described by the formula, the length of which is polynomially
bounded. One running step of machine is described in [18] by the Cook’s method
formula; this is a formula of the propositional calculus, and one can
construct it just as the sentences, which were applied for the modeling of the
polynomial quantity of steps of the nondeterministic Turing machine in the
proof of $\mathbf{NP}$-completeness of the problem SAT [5], (see also the
proof of Theorem 10.3 in [1]). There exists a Boolean $\exists$-formula, which
corresponds to the Cook’s method formula. We will also name this
$\exists$-formula as Cook’s formula.

We intend to modernize the elegant construct of Stockmeyer and Meyer and to
bring it into play for the obtaining our purpose. But we will model the
running steps of a machine by the more complicated formulae that have an
alternation of quantifiers. This complication is caused due to the fact that
the Cook’s method formula is very long — it is far longer than an amount of
the used memory. Really, it has a subformula that consists of one
propositional variable $C_{i,j,t}$ (see, for instance, the proof of Theorem
10.3 in [1] and also Section 8). This variable is true if the $i$th cell
contains symbol $X_{j}$ of the tape alphabet at the instant of time $t$. But
suppose that each of the first $T+1$ squares of tape contains the symbol
$X_{0}$ at time $t$, the remaining part of the tape is empty. This simple tape
configuration (or _instantaneous description_ [1, 18]) is described by the
formula that has a fragment $C_{0,0,t}\wedge C_{1,0,t}\wedge\ldots\wedge
C_{T,0,t}$, and this subformula is $2T+1$ in length without taking the indices
into account. It is impossible to abridge this record, even if we try to use
the universal quantifier since its application to the indices is not allowed
within the confines of the first-order theory. Thus, in order to describe the
machine actions using the exponential amount of space, we need Cook’s formula,
whose length is no less than exponential.

We propose to encode the binary notation of the cell number by a value set of
special variables $x_{t,0},\ldots,x_{t,n}$, where
$n\\!+\\!1\\!\geqslant\\!\log_{2}T$ (see Subsections 4.1, 6.2, and 8.2 for
further details). So we need $\mathcal{O}(n)$ symbols for the describing of
one cell, and $\mathcal{O}(n^{2})$ ones for the assignment of the whole input
string $X$, if $n\\!=\\!|X|$. But then we can describe one running step of the
machine, which uses $T\\!\rightleftharpoons\\!\exp(|X|)$ memory cells on input
$X$, with the aid a formula that is $\mathcal{O}(n^{3})$ in length. The main
idea of so brief a describing consists of the following: merely one tape
square can change on each of the running steps, although the whole computation
can use the exponential amount of memory. 555The denoted locality of the
actions of deterministic machines has long been used in the modeling of the
machine computation with the help of formulae, see, for example, Lemma 2.14 in
[17] or Lemma 7 in [19]. Therefore, it is enough for us to describe the
changes in the only cell, and the contents of the remaining ones can be
”copied” by applying the universal quantifier (see the construction of the
formula $\Delta^{\textit{cop}}(\widehat{u})$ in Subsection 4.1).

At the beginning, we will introduce all variables in great abundance in order
to facilitate the proof, namely, the variables will have the first indices $t$
from 0 to $T$. Next, we will eliminate many of the variables using the
modified method of Stockmeyer and Meyer — see Subsections 4.3.2, 6.2, 8.2 for
further details. A final modeling formula will only contain those of variables
for which $0\\!\leqslant\\!t\\!\leqslant\\!n$ or $t\\!=\\!T$ hold.

The description of the initial configuration and the condition of the
successful termination of computations have a length of $\mathcal{O}(n^{3})$,
if we anew use the quantifiers; hence the entire formula, which simulates the
first $\exp(n)$ steps of the computation of the machine $P$, will be
$\mathcal{O}(|P|\cdot n^{3})$ in length (taking into account the indices).

Therefore, we need to slightly strengthen the Rabin and Fischer method, so
that it can also be applied in the case of a non-linear estimate for the
length of the modeling formula.

###  1.3 The paper structure

The generalized Fisher and Rabin method is adduced in Section 2. The degree of
its usefulness and novelty is discussed in Remark 1. Section 3 contains an
exact formulation of the main theorem (Theorem 1), its primary corollaries,
and some preparation for that and for the proof of this theorem. Sections 4–6
are devoted to the proof of the main theorem. The lower bound on the
computational complexity of the theories, which are nontrivial relatively to
some equivalence relation, in particular, equational-nontrivial, will be
yielded in Section 7. In Section 8, we will discuss the obtained results and
consider the used methods in greater detail, comparing theirs with other
approaches to the simulation of computation.

##  2 The generalized Fischer and Rabin method

We will describe this method in the most general form.

###  2.1 Auxiliary notions

We will need some new concepts.

######  Definition 1.

Let $P$ be a program of the Turing machine; $k$ be a number of its tapes; and
$q_{b}\alpha_{1}\alpha_{2}\ldots\alpha_{k}\to
q_{j}\beta_{1}\beta_{2}\ldots\beta_{k}$ be an instruction of this program. We
will call this instruction explicitly non-executable and the internal state
$b$ inaccessible (for the $P$), if the program $P$ does not contain the
instructions of the form $q_{l}\gamma_{1}\gamma_{2}\ldots\gamma_{k}\to
q_{b}\delta_{1}\delta_{2}\ldots\delta_{k}$.

It is clear that one can write such machine program that it contains some non-
executable instructions, but all its internal states are accessible. It is
evident too that one can easily find the explicitly non-executable
instructions in any program, most precisely, all such instructions can be
found in polynomial time on the program length. However, the detection of the
non-executable instructions, whose internal states are accessible, maybe is
the very difficult task in some cases.

Let us assume that we have removed all the explicitly non-executable
instructions from a program $P$. The elimination has resulted in some program
$P_{1}$. This $P_{1}$ may again contain some explicitly non-executable
instructions, for instance, if the instructions
$q_{l}\gamma_{1}\gamma_{2}\ldots\gamma_{k}\to
q_{b}\delta_{1}\delta_{2}\ldots\delta_{k}$ and
$q_{b}\alpha_{1}\alpha_{2}\ldots\alpha_{k}\to
q_{j}\beta_{1}\beta_{2}\ldots\beta_{k}$ belong to $P$, the first of them is
explicitly non-executable for the $P$, and the state $b$ is not included in
other instructions, then the second instruction is not such in full, although
it is non-executable for the $P$. However, it already is explicitly non-
executable for the program $P_{1}$. We can continue this removing process of
the explicitly non-executable instructions until we obtain the irreducible
program $r(P)$ that does not contain such instructions.

We name the programs $T$ and $P$ monoclonal if $r(T)\\!=\\!r(P)$; at that the
$P$, $T$, and $r(P)$ are called the clones of each other. As usual, a Turing
machine and its program are designated by a uniform sign. Therefore we will
say that two Turing machines are monoclonal if their programs are so.

######  Lemma 1.

(i) There exists a polynomial $h(n)$ such that one can write the code of
irreducible clone $r(P)$ within $h(|P|)$ steps for every program $P$;

(ii) the question about the monoclonality of any two programs $P$ and $T$ is
solvable in polynomial time from $|P|$ and $|T|$;

(iii) all the tape actions of monoclonal machines are identical with each
other on the same inputs.

###### Proof.

It straightforwardly follows from definitions. ∎

######  Definition 2.

Let $F(n)$ be a function that is monotone increasing on all sufficiently large
$n$. The function $F$ is called a limit upper bound for the class of all
polynomials (LUBP) if, for any polynomial $p$, there is a number $n$ such that
the inequality $F(m)\\!>\\!p(m)$ holds for $m\\!\geqslant\\!n$, i.e., each
polynomial is asymptotically smaller than $F$.

An obvious example of the limit upper bound for all polynomials is a
$s$-iterated exponential for every $s\\!\geqslant\\!1$. It is easy to see that
if $F(x)$ is a LUBP, then the functions $F(x^{m})$ and $F(rx)$ are LUBPs also
for positive constants $m$ and $r$, moreover, the function $F(x)\\!-\\!F(dx)$
is a LUBP for every constant $d$ such that $0\\!<\\!d\\!<\\!1$. It follows
from this that if $T(n)$ is a LUBP, then it grows at least exponentially in
the sense that is considered in [4], namely, $T(dn)/T(n)$ tends to 0 as $n$
tends to $\infty$. Inverse assertion seemingly is valid too.

###  2.2 The generalization

Let us suppose that we want to find a lower bound on the recognition
complexity of a language $\mathcal{L}$ over alphabet $\sigma$. We, first of
all, fix a finite tape alphabet $A$ of Turing machines and the number $k$ of
their tapes. We also fix a certain polynomial encoding of the strings over the
alphabet $\sigma$ and of the programs of Turing machines by finite strings of
symbols (words) over the alphabet $A$, i.e., it is implied that the encoding
and unique decoding are realized in a polynomial time from the length of an
object in a natural language.666This language consists of all words over the
alphabet $\sigma$ and all the Turing machines programs with $k$ the tapes and
the tape alphabet $A$. An example of such natural language will be described
in Subsection 3.1. It is implied here and below that the numbers of the
internal states and other indices are written in decimal notation. We presume
also that the used encoding is composite, namely, the code of each instruction
in any program is the constituent of the program code. The code of an object
$E$ is denoted by $c_{O}E$, i.e., $c_{O}E\\!\in\\!A^{\ast}$, if
$E\\!\in\\!\sigma^{\ast}$ or $E$ is a program.

######  Proposition 1.

Let $F$ be a limit upper bound for all polynomials and $\mathcal{L}$ be a
language over some alphabet $\sigma$. Suppose that for any given program $P$
of a deterministic Turing machine and every string $X$ on the input tape of
this machine, one can effectively construct a word $S(P,X)$ over the alphabet
$\sigma$ with the following properties:

(i) a code for $S(P,X)$ can be built within time $g(|X|\\!+\\!|c_{O}P|)$,
where $g$ is a polynomial fixed for all $X$ and $P$;

(ii) the word $S(P,X)$ belongs to $\mathcal{L}$ if and only if the Turing
machine $P$ accepts input $X$ within $F(|X|)$ steps;

(iii) there exist constants $D,b,s\\!>\\!0$ such that either the inequalities

$(a)\qquad|X|\\!\leqslant\\!|c_{O}S(P,X)|\\!\leqslant\\!D\cdot|c_{O}P|^{b}\cdot|X|^{s}$

or the inequalities

$(b)\qquad|X|\\!\leqslant\\!|c_{O}S(P,X)|\\!\leqslant\\!D\cdot(|c_{O}P|\\!+\\!|X|)$

hold true for all sufficiently long $X$, and these constants do not depend on
$P$, but they depend on the applied encoding.

Then (1) for every constant $\delta\\!>\\!0$ and any program $P$, there is a
number $t_{0}$ such that the inequality
$|c_{O}S(P,X)|\\!\leqslant\\!D_{1}\cdot|X|^{s_{1}}$ holds true for all of the
strings $X$, which are longer than $t_{0}$, where $D_{1}\\!=\\!D$ and
$s_{1}\\!=\\!s\\!+\\!\delta$ in case (a) or $D_{1}\\!=\\!(D\\!+\\!\delta)$ and
$s_{1}\\!=\\!1$ in case (b);
(2) for each $a\\!>\\!1$ and every deterministic Turing machine $M$, which
recognizes the language $\mathcal{L}$, there exist infinitely many words $Y$,
on which $M$ runs for more than $F(D_{2}\cdot|c_{O}Y|^{\rho})$ steps for
$D_{2}\\!=\\!(aD_{1})^{-\rho}$ and $\rho\\!=\\!(s_{1})^{-1}$.

###### Proof.

(1). It is easy to see that the $t_{0}$ is equal to $|c_{O}P|^{b/\delta}$ in
case (a); and it equals to $(D/\delta)\cdot|c_{O}P|$ in case (b).

(2) In accordance with condition (i), one can assume that a code for $S(P,X)$
can be written by some machine $M_{1}$ for all given strings $X$ and $c_{O}P$.

Let us suppose that there exist numbers $a,t_{1}$ and a machine $M_{2}$ such
that the $M_{2}$ determines whether $Y\\!\in\\!\mathcal{L}$ within
$F(D_{2}\cdot|c_{O}Y|^{\rho})$ steps for any string $Y$ over the $\sigma$,
provided that $|c_{O}Y|\\!>\\!t_{1}$ and $a\\!>\\!1$.

To proceed to an ordinary diagonal argument, we stage-by-stage construct the
Turing machine $M$. At the first stage, we write a machine $M_{0}$, which for
a given input $X$, determines whether the string $X$ is the code $c_{O}P$ of
some program $P$. If not, then the $M_{0}$, as well as the whole machine $M$,
rejects the $X$; else it writes the code $c_{O}r(P)$ of the irreducible clone
$r(P)$.

At the second stage, the $M_{1}$ joins the running process and writes a word
$c_{O}S(r(P),c_{O}P)$. At the next stage, the procedure $M_{2}$ determines
whether the string $S(r(P),c_{O}P)$ belongs to the language $\mathcal{L}$. If
it does not, then the $M$ accepts the input $X\\!=\\!c_{O}P$. When the $M_{2}$
gives an affirmative answer, then $M$ rejects the $X$.

We estimate the running time of $M$ on input $X\\!=\\!c_{O}P$. Since $c_{O}$
is a polynomial encoding and Lemma 1(i) is valid, there exists a polynomial
$h_{1}$ such that the running time of $M_{0}$ does not exceed $h_{1}(|X|)$.
The machine $M_{1}$ builds $c_{O}S(r(P),X)$ within
$g(|X|\\!+\\!|c_{O}r(P)|)\\!\leqslant\\!g(2|c_{O}P|)$ steps, since
$|c_{O}r(P)|\\!\leqslant\\!|c_{O}P|$; the stage $M_{2}$ lasts no longer than
$F(D_{2}\cdot|c_{O}S(r(P),c_{O}P)|^{\rho})\\!\leqslant\\!F((D_{1}\cdot|c_{O}P|^{s_{1}})^{\rho}/(aD_{1})^{\rho})\\!=\\!F(|c_{O}P|/a^{\rho})$
steps for $|c_{O}S(r(P),c_{O}P)|\\!\geqslant\\!|c_{O}P|\\!>\\!t_{1}$ by our
assumption. Hence, the entire $M$ will execute its work no more than
$T(P)\\!=\\!h_{1}(|c_{O}P|)+g(2|c_{O}P|)+F(|c_{O}P|/a^{\rho})\\!<\\!F(|c_{O}P|)$
steps for all sufficiently large $|c_{O}P|$.

Let us look at the situation that obtains if as $X$ we take the code of so
lengthy a clone $\widehat{M}$ of the machine $M$ that the inequalities
$|c_{O}\widehat{M}|\\!>\\!\max\\{t_{0},t_{1}\\}$ and
$T(\widehat{M})\\!<\\!F(|c_{O}\widehat{M}|)$ hold true.

If the $M$ rejects the input $c_{O}\widehat{M}$, then the $M_{2}$ answers
affirmatively, i.e., the string $S(r(\widehat{M}),c_{O}\widehat{M})$ belongs
to the language $\mathcal{L}$. According to the condition (ii), this means
that the $r(\widehat{M})$ accepts the input $c_{O}\widehat{M}$ within
$F(|c_{O}\widehat{M}|)$ steps. Since the machines $M$, $\widehat{M}$, and
$r(\widehat{M})$ are monoclonal, the $M$ does it too. There is a
contradiction.

If the $M$ accepts the $c_{O}\widehat{M}$ as its input, then the procedure
$M_{2}$ answers negatively. In accordance with the sense of the formula
$S(r(\widehat{M}),c_{O}\widehat{M})$, this signifies that the machine
$r(\widehat{M})$ either rejects the $c_{O}\widehat{M}$ or its running time on
this input is more than $F(|c_{O}\widehat{M}|)$. By construction and our
assumption, the clone $r(\widehat{M})$ cannot operate so long. We have again
arrived at a contradiction. ∎

######  Remark 1.

Apparently, the generalization of Rabin and Fischer’s method has been in
essence known in an implicit form for a long time. For example, it is said in
the penultimate paragraph of the introduction of the article [19] (before the
paragraph ”Paper outline”) that the quadratic increase in the length of the
modeling formulae implies a lowering of the lower bound with $F(n)$ to
$F(\sqrt{n})$ (in our notation), when Compton and Henson’s method is applied.
But the author could not find an explicit formulation of the statement similar
to Proposition 1 for a reference, although its analog for the space complexity
is Lemma 3 in [19]. The proof of the proposition is given only for the sake of
completeness of the proof of Corollary 3. In addition, Proposition 1 in such
form is clearly redundant for the proof of this corollary. However, the author
hopes to apply it in further researches.

######  Corollary 1.

Under the conditions of the proposition
$\mathcal{L}\\!\notin\\!DTIME(F(D^{-\zeta}\cdot n^{\zeta}))$, where
$\zeta\\!=\\!s^{-1}$ ($s\\!=\\!1$ in case (b)).

###### Proof.

Really, $s_{1}\\!=\\!s\\!+\\!\delta$ and $aD_{1}\\!=\\!a(D\\!+\\!\delta)$ tend
to $s$ and $D$ respectively, when $a$ tends to one and $\delta$ tends to zero.
Hence, $\rho\\!=\\!(s\\!+\\!\delta)^{-1}$, $n^{\rho}$, and $D_{1}^{-\rho}$
accordingly tend to $s^{-1}$, $n^{s^{-1}}$, and $D^{-s^{-1}}$ in this case. ∎

##  3 Necessary agreements and the main result

In this section, we specify the restrictions on the used Turing machines, the
characteristics of their actions, and the methods of recording their
instructions and Boolean formulae. These agreements are very important in
proving the main theorem. Although any of these restrictions can be omitted at
the cost of a complication of proofs.

###  3.1 On the Turing machines and recording of Boolean formulae

We reserve the following alphabet for the formulae of the signature of the
two-element Boolean algebra $\mathcal{B}$:
a) signature symbols $\cap,\cup,C,0,1$ and equality sign $\approx$; b) Latin
letters for the indication of the types of the object variables; c) Arabic
numerals and comma for the writing of indices; d) Logical connectives
$\neg,\wedge,\vee,\rightarrow$; e) the signs of quantifiers $\forall,\exists$;
f) auxiliary symbols: (,). All these symbols constitute the first part of a
natural language.

######  Remark 2.

Let us pay attention to that we use three different symbols for the denotation
of equality. The first is the signature symbol ”$\approx$”. It applies only
inside the formulae of a logical theory. The second is the ordinary sign
”$=$”. It denotes the real or assumed equality and is used in our discussions
on the formal logical system. The third sign ”$\rightleftharpoons$” designates
the equality in accordance with a definition.

The priority of connectives and operations or its absence is inessential, as a
difference in length of formulae is linear in these cases.

Hereinafter we consider only deterministic machines with the fixed tape
alphabet $A$, which contains at least four symbols: the first of them is a
designated ”blank” symbol, denoted $\Lambda$; the second is a designated
”start” symbol, denoted $\rhd$; and the last two are the numerals 0,1 (almost
as in Section 1.2 of [2]). As usual, the machine cannot write or erase $\rhd$
symbol.

It is implied that the simulated machines have an only tape, seeing that the
transformation of the machine program from a multi-tape variant to a single-
tape version is feasible in the polynomial time on the length of the program,
at that the running time increases polynomially too [1, 2, 9]. Although the
auxiliary machines may be multi-tape.

The machine tape is infinite only to the right, because the Turing machines
are often considered in this manner (e.g., [1, 2, 4, 5, 7, 9, 11, 12, 13, 14,
15, 16, 17, 18, 19]). Moreover, such machines can simulate the computations,
which is $T$ steps in length on the two-sided tape machine, in linear time of
$T$ [2]. The tape contains initially the start symbol $\rhd$ in the leftmost
square, a finite non-blank input string $X$, and the blank symbol $\Lambda$ on
the rest of its cells. The head is aimed at the left end of the tape, and the
machine is in the special starting state $q_{start}\\!=\\!q_{0}$. When machine
recognizes an input, it enters the accepting state $q_{1}\\!=\\!q_{acc}$ or
the rejecting state $q_{2}\\!=\\!q_{rej}$.

Our machines have the single-operand instructions of a kind
$q_{i}\alpha\\!\rightarrow\\!q_{j}\beta$ as in [11], which differ from double-
operand instructions of a form $q_{i}\alpha\\!\rightarrow\\!q_{j}\beta\gamma$,
where $\alpha\\!\in\\!A;\ \beta,\gamma\\!\in\\!A\cup\\!\\{R,L\\}$. Even if we
regard the execution of a double-operand instruction as one step of
computation, then the difference in length of the running time will be linear.

The Turing machines do not fall into a situation when the machine stopped, but
its answer remained undefined. Namely, they do not try to go beyond the left
edge of the tape; and besides, they do not contain the hanging (or pending)
internal states $q_{j}$, for which $j\\!\neq\\!0,1,2$, and there exist
instructions of a kind $\ldots\rightarrow q_{j}\beta$, but there are no
instructions beginning with $q_{j}\alpha\rightarrow\ldots$ at least for one
$\alpha\\!\in\\!A$. The attempts to go beyond the left edge of the tape are
blocked by the replacement of the instructions of a form
$q_{i}\rhd\\!\rightarrow\\!q_{k}L$ by $q_{i}\rhd\\!\rightarrow\\!q_{i}\rhd$.
The hanging states are eliminated by adding the instructions of a kind
$q_{j}\alpha\\!\rightarrow\\!q_{j}\alpha$ for each of the missing alphabet
symbol $\alpha$.

The programs of the single-tape Turing machines with the tape alphabet $A$ are
written by the symbols of this alphabet, as well with the application of the
symbols $q,R,L,\rightarrow$, Arabic numerals, and comma. This is the second,
last part of a natural language.

###  3.2 The main theorem and its corollary

Let $c_{O}M$ be a chosen polynomial code of an object $M$ by a string over a
tape alphabet $A$ — see the beginning of Subsection 2.2. We suppose that for
this encoding, there exists a linear function $l$ such that the inequalities
$|M|\\!\leqslant\\!|c_{O}M|\\!\leqslant\\!l(|M|)$ hold for any object $M$ of
the natural language described in the previous subsection.

######  Theorem 1.

For each deterministic Turing machine $P$ and every input string $X$, one can
write a closed formula (sentence) $\Omega(X,P)$ of the signature of the two-
element Boolean algebra $\mathcal{B}$ with the following properties:

(i) there exists a polynomial $g$ such that the code $c_{O}\,\Omega(X,P)$ is
written within time $g(|X|,|c_{O}P|)$ for all $X$ and $P$;

(ii) $Th(\mathcal{B})\vdash\Omega(X,P)$ if and only if the Turing machine $P$
accepts input $X$ within time $\exp(|X|)$;

(iii) for every $\varepsilon\\!>\\!0$, there is a constant $D\\!>\\!0$
(depending on the used encoding) such that the inequalities

$|X|\\!<\\!|c_{O}\,\Omega(X,P)|\\!\leqslant\\!D\cdot|c_{O}P|\cdot|X|^{2+\varepsilon}$

hold true for all sufficiently long $X$.

###### Proof.

See Sections 4–6. Now we just note that according to the agreement in the
beginning of this subsection, the calculation of the lengths of all components
of the modeling formulae will be based on the estimate of the quantity of all
the symbols, of the natural language of Subsection 3.1, involved in their
recording.

At first, we will construct the very long formulae that simulate the
computations. These formulae will have the huge number of the ”redundant”
variables. We will take care of the brief record of the constructed formulae
after we ascertain the correctness of our modeling (see Propositions 2 (ii),
3, and 4(ii) below). The modified Stockmeyer and Meyer method is substantially
used at that.∎

######  Corollary 2.

For every $\varepsilon\\!>\\!0$,
$Th(\mathcal{B})\\!\notin\\!DTIME(\exp(D^{-\rho}\cdot n^{\rho}))$, where
$\rho\\!=\\!(2\\!+\\!\varepsilon)^{-1}$

###### Proof.

It straightforwardly follows from the theorem and Corollary 1. ∎

######  Corollary 3.

The class $\mathbf{P}$ is a proper subclass of the class $\mathbf{PSPACE}$.

###### Proof.

Really, the theory $Th(\mathcal{B})$ does not belong to the class $\mathbf{P}$
in accordance with the previous corollary, and this theory is equivalent to
the language $TQBF$ relatively polynomial reduction. But the second language
belongs to the class $\mathbf{PSPACE}$, moreover, it is polynomially complete
for this class [18]. ∎

######  Remark 3.

This result is quite natural and expected for a long time. Its proof is
yielded by one of the few possible ways. Indeed, since the language $TQBF$ is
polynomially complete for the class $\mathbf{PSPASE}$, the inequality
$\mathbf{P}\neq\mathbf{PSPASE}$ implies the impossibility of the inclusion
$Th(\mathcal{B})\in\mathbf{P}$ that is almost equivalent to
$Th(\mathcal{B})\notin DTIME(\exp(dn^{\delta}))$ for suitable
$d,\delta\\!>\\!0$, as it is clear that $Th(\mathcal{B})\in
DTIME(\exp(d_{1}n))$ for some $d_{1}\\!>\\!0$.

###  3.3 Supplementary denotations and arrangements

We introduce the following abbreviations and arrangements for the improvement
in perception (recall that ”$A\rightleftharpoons\mathcal{A}$” means ”$A$ is a
designation for $\mathcal{A}$”):
(1) the square brackets and (curly) braces are equally applied with the
ordinary parentheses in long formulae; (2) the connective $\wedge$ is
sometimes written as $\&$; (3) $\cap$ and $\wedge$ (&) connect more closely
than $\cup$ and $\vee,\rightarrow$; (4) $x\\!<\\!y\rightleftharpoons
x\\!\approx\\!0\wedge y\\!\approx\\!1$; (5)
$\langle\alpha_{0},\ldots,\alpha_{n}\rangle\\!<\\!\langle\beta_{0},\ldots,\beta_{n}\rangle$
is the comparison of tuples in lexicographic ordering, i.e., it is the formula

$\alpha_{0}\\!<\\!\beta_{0}\vee\Bigl{\\{}\alpha_{0}\\!\approx\\!\beta_{0}\wedge\bigl{[}\alpha_{1}\\!<\\!\beta_{1}\vee\bigl{(}\alpha_{1}\\!\approx\\!\beta_{1}\wedge\\{\alpha_{2}\\!<\\!\beta_{2}\vee[\alpha_{2}\\!\approx\\!\beta_{2}\wedge(\alpha_{3}\\!<\\!\beta_{3}\ldots)]\\}\bigr{)}\bigr{]}\Bigr{\\}}.$

The symbol $\widehat{x}$ signifies an ordered set $\langle
x_{0},\ldots,x_{n}\rangle$, whose length is fixed. It is natural that ”the
formula” $\widehat{x}\\!\approx\\!\widehat{\alpha}$ denotes the system of
equations $x_{0}\\!\approx\\!\alpha_{0}\\!\wedge\ldots\wedge
x_{n}\\!\approx\\!\alpha_{n}$. The tuples of variables with two subscripts
will occur only in the form where the first of these indices is fixed, for
instance, $\langle u_{k,0},\ldots,u_{k,n}\rangle$, and we will denote it by
$\widehat{u}_{k}$.

Counting the length of a formula in the natural language, we are guided by the
rule: a tuple $\widehat{x}$ has a length of $n\\!+\\!1$ plus $M$, which is the
quantity of symbols involved in a record of the indices $0,\ldots,n$. The
inequality
$|\widehat{x}\\!\approx\\!\widehat{\alpha}|\\!\leqslant\\!M\\!+\\!3n\\!+\\!3$
will hold, if the $\widehat{\alpha}$ is a tuple of constants; and
$|\widehat{x}\\!\approx\\!\widehat{\alpha}|\\!\leqslant\\!2M\\!+\\!3n\\!+\\!3$,
when it consists of variables.

A binary representation of a natural number $t$ is denoted by $(t)_{2}$.

It is known that if
$t\\!=\\!(\widehat{\gamma})\\!=\\!\langle\gamma_{0},\ldots,\gamma_{n}\rangle_{2}$
is a binary representation of a natural number $t\\!\leqslant\\!\exp(2,n)$,
then the numbers $t\\!+\\!1$ and $t\\!-\\!1$ will be expressed as
$((\widehat{\gamma})\\!+\\!1)_{2}\\!=\\!\langle\gamma_{0}\\!\oplus\gamma_{1}\\!\cdot\\!...\\!\cdot\gamma_{n-1}\\!\cdot\gamma_{n},\,\ldots,\,\gamma_{n-2}\\!\oplus\gamma_{n-1}\\!\cdot\gamma_{n},\,\gamma_{n-1}\\!\oplus\gamma_{n},\,\gamma_{n}\\!\oplus\\!1\rangle_{2}$
and
$((\widehat{\gamma})\\!-\\!1)_{2}=\langle\gamma_{0}\\!\oplus\\!C\gamma_{1}\\!\cdot\\!\ldots\\!\cdot\\!C\gamma_{n-1}\\!\cdot\\!C\gamma_{n},\,\ldots,\,\gamma_{n-2}\\!\oplus\\!C\gamma_{n-1}\\!\cdot\\!C\gamma_{n},\,\gamma_{n-1}\\!\oplus\\!C\gamma_{n},\,\gamma_{n}\\!\oplus\\!1\rangle_{2},$
respectively, where the operation $\cap$ is written in the form of
multiplication $x\cap y\\!=\\!x\cdot y$; and $x\oplus
y\\!\rightleftharpoons\\!x\cdot Co(y)\cup Co(x)\cdot y$.

######  Lemma 2.

(i)
$|\langle\alpha_{0},\ldots,\alpha_{n}\rangle\\!<\\!\langle\beta_{0},\ldots,\beta_{n}\rangle|=\mathcal{O}(\max\\{|\langle\alpha_{0},\ldots,\alpha_{n}\rangle|,$
$|\langle\beta_{0},\ldots,\beta_{n}\rangle|\\})$.

(ii) If a tuple $(t)_{2}$ (together with the indices) is $l$ symbols in
length, then the binary representation of the numbers $t\\!\pm\\!1$ will take
up $\mathcal{O}(l^{2})$ symbols.

###### Proof.

It is obtained by direct calculation. ∎

##  4 The beginning of the proof of Theorem 1

Prior to the writing of a formula $\Omega(X,P)$, we add $2|A|$ the
instructions of the idle run to a program $P$, these instructions have the
form $q_{k}\alpha\to q_{k}\alpha$, where $k\\!\in\\!\\{1(accept),$
$2(reject)\\},\ \alpha\\!\in\\!A$. While the machine executes them, the tape
configuration does not change.

###  4.1 The primary and auxiliary variables

In order to simulate the operations of a Turing machine $P$ on an input $X$
within the first $T\\!=\\!\exp(|X|)$ steps, it is enough to describe its
actions on a zone, which is $T\\!+\\!1$ squares in width, since if the $P$
starts its run in the zeroth cell, then it can finish a computation at most in
the $T$th square. Because the record of the number $(T)_{2}$ has the
$n\\!+\\!1\\!=\\!|X|\\!+\\!1$ bit, the cell numbers are encoded by the values
of the ordered sets of the variables of a kind ”$x$”:
$\widehat{x}_{t}\\!=\\!\langle x_{t,0},\ldots,x_{t,n}\rangle$, which have a
length of $n\\!+\\!1$. The first index $t$, i.e., the color of the record,
denotes the step number, after which there appeared a configuration under
study on the tape. So the formula
$\widehat{x}_{t}\\!\approx\\!\widehat{\alpha}\rightleftharpoons
x_{t,0}\\!\approx\\!\alpha_{0}\wedge\ldots\wedge
x_{t,n}\\!\approx\\!\alpha_{n}$ assigns the number $(\widehat{\alpha})$ of the
required tape cell in binary notation at the instant $t$.

Let us select so great a number $r$ in order that one can write down all the
state numbers of the $P$ and encode all the symbols of the alphabet $A$ by
means of the bit combinations of the same length $r\\!+\\!1$ at one time.
Thus, $\exp(r\\!+\\!1)\\!\geqslant\\!|A|\\!+\\!U$, where $U$ is the maximal
number of the internal states of the $P$, and if $\beta\\!\in\\!A$, then
$c\beta\rightleftharpoons\langle c\beta_{0},\ldots,c\beta_{r}\rangle$ will be
the $(r\\!+\\!1)$-tuple, which codes the $\beta$. So, the encoding $c_{O}$
applied in Sections 2 and 3 is ”outside” (inherent a machine being simulated),
and the encoding $c$ is ”inner” (inherent a modeling formula).

The formula $\widehat{f}_{t}\\!\approx\\!c\varepsilon$ represents an entry of
symbol $\varepsilon$ in some cell after step $t$, where $\widehat{f}_{t}$ is
the $(r\\!+\\!1)$-tuple of variables. When the cell, whose number is
$(\widehat{\mu})$, i.e. the $(\mu)$th cell, contains the symbol $\varepsilon$
after step $t$, then this fact is associated with the quasi-equation (or the
clause) of color $t$:

$\displaystyle\psi_{t}(\widehat{\mu}\\!\rightarrow\\!\varepsilon)\
\rightleftharpoons\
\widehat{x}_{t}\\!\approx\\!\widehat{\mu}\rightarrow\widehat{f}_{t}\\!\approx\\!c\varepsilon\
\rightleftharpoons\ (x_{t,0}\\!\approx\\!\mu_{0}\wedge\ldots\wedge
x_{t,n}\\!\approx\\!\mu_{n})\to$
$\displaystyle\\!\rightarrow(f_{t,0}\\!\approx\\!c\varepsilon_{0}\wedge\ldots\wedge
f_{t,r}\\!\approx\\!c\varepsilon_{r}).$

The tuples of variables $\widehat{q}_{t}$ and $\widehat{d}_{t}$ are
accordingly used to indicate the number of the machine’s internal state and
the code of the symbol scanned by the head at the instant $t$. For every step
$t$, a number $i\\!=\\!(\widehat{\delta})$ of the machine state $q_{i}$ and a
scanned square’s number $(\widehat{\xi})$ together with a symbol $\alpha$,
which is contained there, are represented by a united _$\pi$ -formula_ of
color $t$:

$\displaystyle\pi_{t}(\alpha,(i)_{2},\widehat{\xi})\ \rightleftharpoons\
\widehat{d}_{t}\\!\approx\\!c\alpha\wedge\widehat{q_{t}}\\!\approx\\!\widehat{\delta}\wedge\widehat{z_{t}}\\!\approx\\!\widehat{\xi}\
\rightleftharpoons\ (d_{t,0}\\!\approx\\!c\alpha_{0}\wedge\ldots\wedge
d_{t,r}\\!\approx\\!c\alpha_{r})\wedge$
$\displaystyle\wedge(q_{t,0}\\!\approx\\!\delta_{0}\wedge\ldots\wedge
q_{t,r}\\!\approx\\!\delta_{r})\wedge(z_{t,0}\\!\approx\\!\xi_{0}\wedge\ldots\wedge
z_{t,n}\\!\approx\\!\xi_{n}),$

where the ordered sets of variables $\widehat{d}_{t}$ and $\widehat{q}_{t}$
have a length of $r\\!+\\!1$; and $\widehat{z}_{t}$ is the $(n\\!+\\!1)$-tuple
of variables and is assigned for the storage of the scanned cell’s number. The
formula expresses a condition for the applicability of instruction
$q_{i}\alpha\\!\rightarrow\\!\ldots$; in other words, this is a timer that
activates exactly this instruction, provided that the head scans the
$(\widehat{\xi})$th cell.

The basic variables $\widehat{x}_{t},\widehat{z}_{t}$, and
$\widehat{q}_{t},\widehat{f}_{t},\widehat{d}_{t}$ are introduced in great
abundance in order to facilitate the proof. But a final modeling formula will
only contain those of them for which $t\\!=\\!0,\ldots,n$ or
$t\\!=\\!T\rightleftharpoons\exp(n)$ holds. The sets of the basic variables
have the different lengths. However, this will not lead to confusion, since
the tuples of the first two types will always be $n\\!+\\!1$ in length,
whereas the last ones will have a length of $r\\!+\\!1$. The sets of constants
or other variables may also be different in length, but such tuple will always
be identically associated to some of the above mentioned ones.

The other variables are auxiliary. They will be described as needed. Their
task consists in a determination of the values of the basic variables of the
color $t+\\!1$ provided that the primary ones of the color $t$ have the
”correct” values. Moreover, this transfer has to adequately correspond to that
instruction which is employed at the step $t\\!+\\!1$.

######  Lemma 3.

If the indices are left out of account, then a clause
$\psi_{t}(\widehat{u}\\!\rightarrow\\!\beta)$ and a timer ($\pi$-formula) will
be $\mathcal{O}(n\\!+\\!r)$ in length.

###### Proof.

It is obtained by direct calculation. ∎

###  4.2 The description of an instruction action

The following formula $\varphi(k)$ describes an action of the $k$th
instruction $M(k)\\!=\\!q_{i}\alpha\\!\rightarrow\\!q_{j}\beta$ (including the
idle run’s instructions; see the beginning of this section) at some step,
where $\alpha\\!\in\\!A$, $\beta\\!\in\\!A\cup\\{R,L\\}$:

$\displaystyle\varphi(k)\ \rightleftharpoons\ \forall\,\widehat{u}_{k}\
\bigl{\\{}\pi_{t}(\alpha,(i)_{2},\widehat{u}_{k})\ \rightarrow\
\bigl{[}\Delta^{cop}(\widehat{u}_{k}(\beta))\ \&\
\forall\widehat{h}_{k}\bigl{(}\Gamma^{ret}(\beta)\ \rightarrow$
$\displaystyle\to\ [\Delta^{wr}(\beta)\ \&\
\pi_{t+1}(h_{k},(j)_{2},\widehat{u}_{k}(\beta))]\bigr{)}\bigr{]}\bigr{\\}}.$

For the sake of concreteness, we regard that this step has a number
$t\\!+\\!1$, so we have placed such subscripts on both $\pi$-formulae. Now we
will describe the subformulae of the $\varphi(k)$ with the free basic
variables
$\widehat{x}_{t},\widehat{q}_{t},\widehat{z}_{t},\widehat{d}_{t},\widehat{f}_{t},\widehat{x}_{t+1},\widehat{q}_{t+1},\\\
\widehat{z}_{t+1},\widehat{d}_{t+1}$, and $\widehat{f}_{t+1}$.

The first $\pi$-formula of color $t$ plays a role of _a timer_. It starts up
the fulfillment of the instruction with the prefix
$q_{i}\alpha\\!\rightarrow\\!\ldots$ provided that a head scans the
$(\widehat{u})_{k}$th square. For every $(n\\!+\\!1)$-tuple $\widehat{u}_{k}$
and a given meta-symbol $\beta\\!\in\\!\\{R,L\\}\cup A$, the number of the
cell that will be scanned by the head after the execution of the instruction
$M(k)$ is specified as follows:
$\widehat{u}_{k}(R)\\!\rightleftharpoons\\!((\widehat{u}_{k})\\!+\\!1)_{2};\quad\widehat{u}_{k}(L)\\!\rightleftharpoons\\!((\widehat{u}_{k})\\!-\\!1)_{2}$;
and $\widehat{u}_{k}(\beta)\\!\rightleftharpoons\\!\widehat{u}_{k}$ for
$\beta\\!\in\\!A$.

The formula $\Delta^{cop}(\widehat{u}_{k}(\beta))$ changes the color of
records in all the cells, whose numbers are different from
$(\widehat{u}_{k}(\beta))$; in other words, it ”copies” the majority of
records:

$\displaystyle\Delta^{cop}(\widehat{u}_{k}(\beta))\rightleftharpoons\forall\,\widehat{w}_{k}\,[\neg\widehat{w}_{k}\\!\approx\\!\widehat{u}_{k}(\beta)\rightarrow\exists\,\widehat{g}_{k}(\psi_{t}(\widehat{w}_{k}\\!\rightarrow\\!\widehat{g}_{k})\
\wedge\ \psi_{t+1}(\widehat{w}_{k}\\!\rightarrow\\!\widehat{g}_{k}))].$

If $\beta\\!\in\\!\\{R,L\\}$, then $\Gamma^{ret}(\beta)\ \rightleftharpoons\
\psi_{t}(\widehat{u}_{k}(\beta)\\!\rightarrow\\!\widehat{h}_{k})\ =\
\widehat{x}_{t}\\!\approx\\!\widehat{u}_{k}(\beta)\rightarrow\widehat{f}_{t}\\!\approx\\!\widehat{h}_{k}$.
An informal sense of this formula is the following: it ”seeks” a code
$\widehat{h}_{k}$ of the symbol, which will be scanned after the next step
$t\\!+\\!1$ (by this reason it is named ”retrieval”); for this purpose, it
”inspects” the square that is to the right or left of the cell
$(\widehat{u}_{k})$. When $\beta\\!\in\\!A$, there is no need to look for
anything, so the formula $\Gamma^{ret}(\beta)$ will be very simple in this
case: $\widehat{h}_{k}\\!\approx\\!c\beta$.

The formula $\Delta^{wr}(\beta)$ ”puts” the symbol, whose code is
$\widehat{h}_{k}$ and color is $t\\!+\\!1$, in the
$(\widehat{u}_{k}(\beta))$th square:
$\Delta^{wr}(\beta)\rightleftharpoons\psi_{t+1}(\widehat{u}_{k}(\beta)\\!\rightarrow\\!\widehat{h}_{k}))$.

The second $\pi$-formula of the color $t+\\!1$ aims the head at the
$(\widehat{u}_{k}(\beta))$th cell; places the symbol $\widehat{h}_{k}$ in this
location; and changes the number of the machine state for $j$:
$\widehat{z}_{t+1}\\!\approx\\!\widehat{u}_{k}(\beta)\wedge\widehat{d}_{t+1}\\!\approx\\!\widehat{h}_{k}\wedge\widehat{q}_{t+1}\\!\approx\\!(j)_{2}$.

######  Lemma 4.

(i) If $\beta\\!\in\\!A$, then the formulae $\Gamma^{ret}(\beta)$;
$\pi_{t+1}(\widehat{h}_{k},(j)_{2},\widehat{u}_{k}(\beta))$;
$\Delta^{wr}(k,\beta)$; $\Delta^{cop}(\widehat{u}_{k},\beta)$; and
$\varphi(k)$ will be
$\mathcal{O}(|\psi_{t+1}(\widehat{w}_{k}\\!\rightarrow\\!\widehat{g}_{k})|)$
in length.
(ii) For $\beta\\!\in\\!\\{R,L\\}$, each of these formulae is
$\mathcal{O}(n\cdot|\psi_{t+1}(\widehat{w}_{k}\\!\rightarrow\\!\widehat{g}_{k})|)$
in length.

###### Proof.

This follows from Lemmata 2 and 3 by direct calculation. ∎

###  4.3 The description of the running steps and
configurations

At first, we will construct a formula $\Phi^{(0)}(P)$ describing one step of
the machine run, when the $P$ is applied to a configuration that arose after
some step $t$. Next, we will describe by means of the formulae the machine
actions over an exponential period of time; at that, the Stockmeyer and Meyer
method will be used.

####  4.3.1 One step

Let $N$ be a quantity of the instructions of machine $P$ together with $2|A|$
the idle run’s ones (see the beginning of this section). The formula
$\Phi^{(0)}(P)$ that describes one step (whose number is $t\\!+\\!1$) of the
machine $P$ is of the form:

$\Phi^{(0)}(P)(\widehat{y}_{t},\widehat{y}_{t+1})\ \rightleftharpoons\
\bigwedge_{0<\,k\leq\,N}\varphi(k)(\widehat{y}_{t},\widehat{y}_{t+1}),$

where
$\widehat{y}_{t}\rightleftharpoons\langle\widehat{x}_{t},\widehat{q}_{t},\widehat{z}_{t},\widehat{d}_{t},\widehat{f}_{t}\rangle$
and
$\widehat{y}_{t+1}\rightleftharpoons\langle\widehat{x}_{t+1},\widehat{q}_{t+1},\widehat{z}_{t+1},\widehat{d}_{t+1},\widehat{f}_{t+1}\rangle$
are two $(2n\\!+\\!3r\\!+\\!5)$-tuples of its free variables.

Let us denote the quantifier-free part of a formula $\chi$ as
$\langle\chi\rangle$.

######  Lemma 5.

(i) If $\widehat{x}_{t}\\!\neq\\!\widehat{\mu}$, then a clause
$\psi_{t}(\widehat{\mu}\\!\rightarrow\\!\varepsilon)$ will be true
independently of the value of variables $\widehat{f}_{t}$. In particular, a
quasi-equation, which is contained into the record of
$\langle\Delta^{cop}(\widehat{u}_{k})\rangle$, will be true, if its color is
$t$ or $t\\!+\\!1$, and at the same time
$\widehat{x}_{t}\\!\neq\\!\widehat{w}_{k}$ or
$\widehat{x}_{t+1}\\!\neq\\!\widehat{w}_{k}$, respectively.

(ii) For some constant $D_{1}$, the inequality

$|\Phi^{(0)}(P)(\widehat{y}_{t},\widehat{y}_{t+1})|\\!\leqslant\\!D_{1}\cdot|c_{O}P|\cdot|\varphi(N)|$

holds.

###### Proof.

(i) The premises of clauses are false in these cases.

(ii) If the quantity of the program $P$ instructions is not equal to zero,
i.e., $N\\!-\\!2|A|\neq\\!0$, then $N\cdot\lceil\lg
N\rceil\\!<\\!D_{2}\cdot|c_{O}P|$. This implies the assertion of the lemma. ∎

####  4.3.2 The configurations and the exponential quantity of steps

The formulae $\Phi^{(s+1)}(P)(\widehat{y}_{t},\widehat{y}_{t+e(s+1)})$ conform
to the actions of machine $P$ over a period of time
$e(s)\\!\rightleftharpoons\\!\exp(s)$. They are defined by induction:

$\displaystyle\
\Phi^{(s+1)}(P)\rightleftharpoons\exists\,\widehat{v}\,\forall\,\widehat{a}\,\forall\,\widehat{b}\;\bigl{\\{}\bigl{[}(\widehat{y}_{t}\\!\approx\\!\widehat{a}\
\wedge\ \widehat{v}\\!\approx\\!\widehat{b})\ \vee\
(\widehat{v}\\!\approx\\!\widehat{a}\ \wedge\
\widehat{b}\\!\approx\\!\widehat{y}_{t+e(s+1)})\bigr{]}\ \rightarrow$
$\displaystyle\to\qquad\Phi^{(s)}(P)(\widehat{a},\widehat{b})\bigr{\\}},$

where $\widehat{v},\widehat{a},\widehat{b}$ are the
$(2n\\!+\\!3r\\!+\\!5)$-tuples of the new auxiliary variables.

Let $L(t)$ be a configuration, which is recorded on the tape after step $t$
(it may be unrealizable): namely, at the instant $t$, every cell, whose number
is $(\widehat{\mu})$, contains a symbol $\varepsilon(\widehat{\mu})$; the
scanned square has the number $(\widehat{\eta})$; and a machine is ready to
execute an instruction $q_{i}\alpha\\!\rightarrow\\!\ldots$. Then the
following formula corresponds to this configuration (we recall that
$T\\!=\\!\exp(n)$):

$\Psi L(t)(\widehat{y}_{t})\ \rightleftharpoons\
\pi_{t}(\alpha,(i)_{2},\widehat{\eta})\ \&\
\bigwedge_{0\leqslant\,(\widehat{\mu})_{2}\leqslant\,T}\psi_{t}(\widehat{\mu}\\!\rightarrow\\!\varepsilon(\widehat{\mu})).$

It has $2n\\!+\\!3r\\!+\\!5$ free variables
$\widehat{y_{t}}\\!=\\!\langle\widehat{x}_{t},\widehat{q}_{t},$
$\widehat{z}_{t},d_{t},f_{t}\rangle$.

##  5 The simulation of one running step

We simply associated the formulae, which were constructed earlier, with the
certain components of programs or with processes. However one cannot assert
that these formulae simulate something, i.e., they will not always turn true,
when the events, which are described by them, are real.

###  5.1 Simulating formula

Let us definite

$\Omega^{(0)}(X,P)(\widehat{y}_{t},\widehat{y}_{t+1})\rightleftharpoons[\Psi
K(t)(\widehat{y}_{t})\ \&\
\Phi^{(0)}(P)(\widehat{y}_{t},\widehat{y}_{t+1})]\rightarrow\Psi
K(t\\!+\\!1)(\widehat{y}_{t+1}).$

We will prove in this section that the sentence
$\forall\widehat{y}_{t}\forall\widehat{y}_{t+1}\Omega^{(0)}(X,P)(\widehat{y}_{t},\widehat{y}_{t+1})$
is true on the Boolean algebra $\mathcal{B}$ if and only if the machine $P$
transforms the configuration $K(t)$ into $K(t\\!+\\!1)$ in one step. So we can
say that this formula models the machine actions at the step $t\\!+\\!1$.

######  Remark 4.

One can regard that the formula
$\Omega^{(0)}(X,P)(\widehat{y}_{t},\widehat{y}_{t+1})$ is the analog of the
Cook’s method formula $A_{0,m}(\widetilde{U},\widetilde{V})$, which was
applied in the proof of Theorem 4.3 in [18], here $\widetilde{U}$ and
$\widetilde{V}$ are the sequences $(u_{1},\ldots,u_{m})$ and
$(v_{1},\ldots,v_{m})$ of the Boolean variables and $m\\!=\\!q(|X|)$ is the
value of suitable polynomial $q$ on the length of input $X$. Indeed, the
sentence
$\exists\widetilde{U}\exists\widetilde{V}A_{0,m}(\widetilde{U},\widetilde{V})$
is true if and only if the configuration encoded by $v_{1}\ldots v_{m}$
follows from the configuration that corresponds to $u_{1}\ldots u_{m}$ in at
most one step of the $P$ (these $m$ and $P$ are $n$ and $\mathfrak{M}$ in
[18]).

However, there are solid arguments to believe that the real analog of the
formula $A_{0,m}(\widetilde{U},\widetilde{V})$ is the
$\Phi^{(0)}(P)(\widehat{y}_{t},\widehat{y}_{t+e(s+1)})$ nevertheless. We will
return to the discussion of this analogy in Subsection 8.2.

###  5.2 The single-valuedness of modeling and
the special values of variables

Let $K(t\\!+\\!1)$ be a configuration that has arisen from a configuration
$K(t)$ as a result of the machine $P$ action at the step $t\\!+\\!1$.

######  Proposition 2.

(i) There exist special values of variables $\widehat{y}_{t}$ such that the
formula $\Psi K(t)(\widehat{y}_{t})$ is true, and the truth of
$\Phi^{(0)}(P)(\widehat{y}_{t},\widehat{y}_{t+1})$ follows from the truth of
$\Psi K(t\\!+\\!1)(\widehat{y}_{t+1})$ for every $\widehat{y}_{t+1}$.

(ii) If a formula $\Omega^{(0)}(X,P)(\widehat{y}_{t},\widehat{y}_{t+1})$ is
identically true over algebra $\mathcal{B}$, then the machine $P$ cannot
convert the configuration $K(t)$ into the configuration, which differs from
$K(t\\!+\\!1)$, at the step $t+\\!1$.

###### Proof.

We will prove these assertions simultaneously. Namely, we will select the
values variables $\widehat{y}_{t}$ and $\widehat{y}_{t+1}$ such that a formula

$\Upsilon_{t+1}(\widehat{y}_{t},\widehat{y}_{t+1})\\!\rightleftharpoons\\![\Psi
K(t)(\widehat{y}_{t})\,\&\,\Phi^{(0)}(P)(\widehat{y}_{t},\widehat{y}_{t+1})]\\!\rightarrow\\!\Psi
L(t+\\!1)(\widehat{y}_{t+1})$

will be false, if the configuration $L(t+\\!1)$ differs from the real
$K(t+\\!1)$. This implies Item (ii) of the proposition. However, at the
beginning, we will select the special values of the variables of the tuple
$\widehat{y}_{t}$. After that when we pick out the values of the corresponding
variables of the color $t+\\!1$, the formulae $\Psi
K(t+\\!1)(\widehat{y}_{t+1})$ and
$\Phi^{(0)}(P)(\widehat{y}_{t},\widehat{y}_{t+1})$ will become true or false
at the same time depending on the values of the variables $\widehat{y}_{t+1}$.

Let $M(k)\\!=\\!q_{i}\alpha\\!\rightarrow\ldots$ be an instruction that is
applicable to the configuration $K(t)$; and $(\widehat{\eta})$ be a number of
the scanned square. We specify $\widehat{d}_{t}\\!=\\!c\alpha,\
\widehat{q}_{t}\\!=\\!(i)_{2},\ \widehat{z}_{t}\\!=\\!\widehat{\eta}$. Then
$\pi$-formula $\pi_{t}(\alpha,(i)_{2},\widehat{\eta})$, which is in the record
of $\Psi K(t)$, is true.

Let us consider a formula $\varphi(l)$ that conforms to some instruction
$M(l)\\!=\\!q_{b}\theta\\!\rightarrow\ldots$ that differs from the $M(k)$.
This formula has a timer $\pi_{t}(\theta,(b)_{2},\widehat{u}_{l})$ as the
first premise. For the selected values of the variables
$\widehat{d}_{t};\widehat{q}_{t};$ and $\widehat{z}_{t}$, the timer takes the
form of
$c\alpha\\!\approx\\!c\theta\wedge(i)_{2}\\!\approx\\!(b)_{2}\wedge\widehat{\eta}\\!\approx\\!\widehat{u}_{l}$.
It is obvious that if $\alpha\\!\neq\\!\theta$; or $i\\!\neq b$; or
$\widehat{u}_{l}\\!\neq\\!\widehat{\eta}$, then this $\pi$-formula will be
false, and the whole $\varphi(l)$ will be true.

Thus, let $\varphi(k)$ be a formula that correspondents to the instruction
$M(k)\\!=\\!q_{i}\alpha\\!\rightarrow\\!q_{j}\beta$; and
$\widehat{u}_{k}\\!=\\!\widehat{\eta}$. Let us define
$\widehat{d}_{t+1}\\!=\\!c\lambda;\ \widehat{q}_{t+1}\\!=\\!(j)_{2};\
\widehat{z}_{t+1}\\!=\\!\widehat{\eta}(\beta)$, where
$(\widehat{\eta}(\beta))$ is a number of the square, which will be scanned by
the machine head after the fulfillment of the instruction $M(k)$; and
$\lambda$ is the symbol, which the head will see there. For these
$\widehat{u}_{k}$ and selected values of
$\widehat{d}_{t+1},\widehat{q}_{t+1},\widehat{z}_{t+1}$, the $\pi$-formula,
which enters into the record of $\Psi K(t+\\!1)$, becomes true. But the
conclusion of the quantifier-free part $\langle\varphi(k)\rangle$ contains a
slightly different timer
$\pi_{t+1}(\widehat{h}_{k},(j)_{2},\widehat{u}_{k}(\beta))$; in this timer,
the only equality $\widehat{d}_{t+1}\\!\approx\\!\widehat{h}_{k}$ included in
it raises doubts for the time being.

Let us assign $\widehat{x}_{t}\\!=\\!\widehat{\eta}(\beta)$. Since we consider
the case, when $\widehat{u}_{k}\\!=\\!\widehat{\eta}$, the equality
$\widehat{u}_{k}(\beta)\\!=\\!\widehat{\eta}(\beta)$ holds true too. Therefore
the quasi-equation, of the color $t$, which enters into the
$\langle\Delta^{cop}(\widehat{u}_{k}(\beta))\rangle$, is true for all
$\widehat{w}_{k}\\!\neq\\!\widehat{\eta}(\beta)$ and irrespective of the
values of the tuples $\widehat{f}_{t}$ and $\widehat{g}_{k}$ according to
Lemma 5(i). For the same reason, all the clauses that are included in the
$\Psi K(t)$ are true, except the clause
$\psi_{t}(\widehat{\eta}(\beta)\rightarrow\\!\lambda)$ for
$\beta\\!\in\\!\\{R,L\\}$ or $\psi_{t}(\widehat{\eta}\\!\rightarrow\\!\alpha)$
for $\beta\\!\in\\!A$. We set the value of the tuple $\widehat{f}_{t}$ as
$c\lambda$, if $\beta\\!\in\\!\\{R,L\\}$, or as $c\alpha$, if not. Now, the
questionable clause from the $\Psi K(t)$ becomes true, because its premise and
conclusion are true.

If $\widehat{h}_{k}\\!\neq\\!c\lambda$, then the formula $\Gamma^{ret}(\beta)$
will be false, since it is either
$\psi_{t}(\widehat{\eta}(\beta)\\!\rightarrow\\!\widehat{h}_{k})$ for
$\beta\\!\in\\!\\{R,L\\}$, or $\widehat{h}_{k}\\!\approx\\!c\beta$ for
$\beta\\!\in\\!A$. Hence the whole formula $\langle\varphi(k)\rangle$ will be
true in this case. When $\widehat{h}_{k}\\!=\\!c\lambda$, the terminal
$\pi$-formula in the $\langle\varphi(k)\rangle$ becomes true, since
$\widehat{d}_{t+1}\\!=\\!c\lambda$.

If the ”incorrect” formula $\Psi L(t+\\!1)$ has a mistake in the record of
timer or clause $\psi_{t+1}(\widehat{\eta}(\beta)\rightarrow\\!\lambda)$, we
will define $\widehat{x}_{t+1}\\!=\\!\widehat{\eta}(\beta)$ and
$\widehat{f}_{t+1}\\!=\\!c\lambda$ (we recall that $\lambda\\!=\\!\beta$ for
$\beta\\!\in\\!A$). But when these fragments are that as they should be,
however, there is another ”incorrect” clause
$\psi_{t+1}(\widehat{\mu}\\!\rightarrow\\!\rho)$, where $\rho$ is different
from ”real” $\delta$, we will assign $\widehat{x}_{t+1}\\!=\\!\widehat{\mu}$
and $\widehat{f}_{t+1}\\!=\\!\widehat{g}_{k}\\!=\\!c\delta$.777We note that
this is the only case when we need to set the values of the variables
$\widehat{g}_{k}$. We obtain again that all the quasi-equations of the color
$t\\!+\\!1$ in the formulae
$\langle\Delta^{cop}(\widehat{u}_{k}(\beta))\rangle$ and $\Delta^{wr}(\beta)$
are true in both of these cases on the grounds of Lemma 5(i) or because their
premises and conclusions are true. Therefore the whole formula
$\langle\varphi(k)\rangle$ is true. All the clauses contained in $\Psi
K(t\\!+\\!1)$ are true for the same reasons.

We obtain as a result that any formula $\varphi(l)$ is true for the above
selected values of the primary variables, so the entire conjunction
$\Phi^{(0)}(P)$ is true. Since the premise and conclusion of the
$\Omega^{(0)}(X,P)(\widehat{y}_{t},\widehat{y}_{t+1})$ are true, and the
configurations $K(t+\\!1)$ and $L(t+\\!1)$ are different; the ”incorrect”
formula $\Upsilon_{t+1}$ is false.

In view of the fact that the configuration $L(t\\!+\\!1)$ may differ from the
real $K(t+\\!1)$ in any place, Item (i) is established too. ∎

###  5.3 The sufficiency of modeling

We will now prove a converse to Proposition 2(ii).

######  Proposition 3.

Let $K(t\\!+\\!1)$ be a configuration that has arisen from a configuration
$K(t)$ as a result of an action of the machine $P$ at the step $t\\!+\\!1$.
Then the formula $\Omega^{(0)}(X,P)(\widehat{y}_{t},\widehat{y}_{t+1})$ is
identically true on algebra $\mathcal{B}$.

###### Proof.

Let $M(k)\\!=\\!q_{i}\alpha\\!\rightarrow\\!q_{j}\beta$ be the instruction
that transforms the configuration $K(t)$ into the $K(t\\!+\\!1)$; and
$\varphi(k)(\widehat{y}_{t},\widehat{y}_{t+1})$ be a formula, which is written
for this instruction. This formula is the consequence of the
$\Phi^{(0)}(P)(\widehat{y}_{t},\widehat{y}_{t+1})$.

Let us replace the $\varphi(k)$ by a conjunction of formulae
$\varphi(k)(\widehat{\mu})$, they are each obtained as the result of the
substitution the various values of the universal variables $\widehat{u}_{k}$
for the variables themselves. Every formula $\varphi(k)(\widehat{\mu})$
contains the premise
$\widehat{d}_{t}\\!\approx\\!c\alpha\wedge\widehat{q_{t}}\\!\approx\\!(i)_{2}\wedge\widehat{z}_{t}\\!\approx\\!\widehat{\mu}$,
one of them coincides with the only timer
$\pi_{t}(\alpha,\widehat{\delta},\widehat{\eta})$ included in the $\Psi K(t)$
for $\widehat{u}\\!=\\!\widehat{\mu}\\!=\\!\widehat{\eta}$ and
$i\\!=\\!(\widehat{\delta})$, as the instruction $M(k)$ is applicable to the
configuration $K(t)$. Therefore the formula $\Psi K(t)\ \&\
\Delta^{cop}(\widehat{\eta}(\beta))\ \&\
\forall\,\widehat{h}_{k}\\{\Gamma^{ret}(\beta)(\widehat{\eta})\rightarrow[\Delta^{wr}(\beta)(\widehat{\eta})\
\&\ \pi_{t+1}((\widehat{h}_{k},(j)_{2},$ $\widehat{\eta}(\beta))]\\}$ follows
from the $\Psi K(t)$ and $\varphi(k)(\widehat{\eta})$.

The formula $\Delta^{cop}(\widehat{\eta}(\beta))$ begins with the quantifiers
$\forall\,\widehat{w}_{k}$. Let us replace this formula by a conjunction that
is equivalent to it, we substitute all possible values for the variables
$\widehat{w}_{k}$ to this effect. For every value of $\widehat{w}_{k}$, there
is a unique value of the tuple $\widehat{g}_{k}$ such that the clause
$\psi_{t}(\widehat{w}_{k}\\!\rightarrow\\!\widehat{g}_{k})$ enters into the
formula $\Psi K(t)$. When these values of $\widehat{g}_{k}$ are substituted in
their places, we will obtain all the quasi-equations from the $\Psi
K(t\\!+\\!1)$, except one.

For the appropriate value of $\widehat{h}_{k}$, either the formula
$\Gamma^{ret}(\beta)(\widehat{\eta})$ coincides with some clause existing in
the $\Psi K(t)$, or it becomes true: $\widehat{h}_{k}\\!\approx\\!c\beta$,
owing to the applicability of the instruction $M(k)$ to the configuration
$K(t)$. In any case, the formula $\Delta^{wr}(\beta)(\widehat{\eta})$ in an
explicit form contains the quasi-equation
$\psi_{t+1}(\widehat{\eta}(\beta)\\!\rightarrow\ldots)$, which is missing in
the $\Psi K(t\\!+\\!1)$ so far; and the tuple $\widehat{h}_{k}$ obtains the
concrete value. If we substitute this value in the concluding $\pi$-formula of
the $\varphi(k)$, then we will obtain the necessary timer
$\pi_{t+1}(\widehat{h}_{k},(j)_{2},\widehat{\eta}(\beta))$ from the $\Psi
K(t\\!+\\!1)$. ∎

##  6 The construction of the formula $\Omega(X,P)$

###  6.1 The simulation of the exponential computations

Let us define the formulae
$\Omega^{(s)}(X,P)(\widehat{y}_{t},\widehat{y}_{t+e(s)})$ that model
$e(s)\\!\rightleftharpoons\\!\exp(s)$ running steps of a machine $P$, when it
applies to a configuration $K(t)$:

$\displaystyle\Omega^{(s)}(X,P)(\widehat{y}_{t},\widehat{y}_{t+e(s)})\
\rightleftharpoons\ [\Psi K(t)(\widehat{y}_{t})\ \&\
\Phi^{(s)}(P)(\widehat{y}_{t},\widehat{y}_{t+e(s)})]\to$
$\displaystyle\rightarrow\ \Psi K(t\\!+\\!e(s))(\widehat{y}_{t+e(s)}).$

######  Proposition 4.

Let $t,s\\!\geqslant\\!0$ be the integers such that
$t\\!+\\!e(s)\\!\leqslant\\!T$.

(i) If the machine $P$ transforms the configuration $K(t)$ into the
$K(t\\!+\\!e(s))$ within $e(s)$ steps, then there are special values of
variables $\widehat{y}_{t}$ such that the formula $\Psi K(t)(\widehat{y}_{t})$
is true; and for all $\widehat{y}_{t+e(s)}$, whenever the $\Psi
K(t\\!+\\!e(s))(\widehat{y}_{t+e(s)})$ is true, the
$\Phi^{(s)}(P)(\widehat{y}_{t},\widehat{y}_{t+e(s)})$ is also true.

(ii) The formula $\Omega^{(s)}(X,P)(\widehat{y}_{t},\widehat{y}_{t+e(s)})$ is
identically true over the Boolean algebra $\mathcal{B}$ if and only if the
machine $P$ converts the configuration $K(t)$ into $K(t\\!+\\!e(s))$ within
$e(s)$ steps.

###### Proof.

Induction on the parameter $s$. For $s\\!=\\!0$, Item (i) is a consequence of
Proposition 2(i), and Item (ii) follows from Propositions 2(ii) and 3.

We start the proof of the inductive step by rewriting the formula
$\Phi^{(s+1)}(P)(\widehat{y}_{t},$ $\widehat{y}_{t+e(s+1)})$ in the
equivalent, but longer form:

$\displaystyle\exists\,\widehat{v}\bigl{\\{}\forall\,\widehat{a}\,\forall\,\widehat{b}\bigl{[}(\widehat{y}_{t}\\!\approx\\!\widehat{a}\
\wedge\
\widehat{v}\\!\approx\\!\widehat{b})\rightarrow\Phi^{(s)}(P)(\widehat{a},\widehat{b})\bigr{]}\
\&\
\forall\,\widehat{a}\,\forall\,\widehat{b}\bigl{[}(\widehat{v}\\!\approx\\!\widehat{a}\
\wedge\ \widehat{b}\\!\approx\\!\widehat{y}_{t+e(s+1)})\rightarrow$
$\displaystyle\rightarrow\ \
\Phi^{(s)}(P)(\widehat{a},\widehat{b})\bigr{]}\bigr{\\}}.$

The following formula results from this immediately:

$\Xi_{s+1}\rightleftharpoons\exists\,\widehat{v}\bigl{\\{}\Phi^{(s)}(P)(\widehat{y}_{t},\widehat{v})\
\&\Phi^{(s)}(P)(\widehat{v},\widehat{y}_{t+e(s+1)})\bigr{\\}}.$

On the other hand, each of the two implications which are included in the
equivalent long form of the formula
$\Phi^{(s+1)}(P)(\widehat{y}_{t},\widehat{y}_{t+e(s+1)})$ can be false only
when the equalities existing in its premise are valid. Hence this formula is
equivalent to the $\Xi_{s+1}$.

Let the machine $P$ transforms the configuration $K(t)$ into the
$K(t+\\!e(s))$ within $e(s)$ steps, and it converts the latter into the
$K(t\\!+\\!e(s\\!+\\!1))$ within the same time.

By the inductive hypothesis of Item (ii) (we recall that the induction is
carried out over a single parameter $s$), the formula
$\Omega^{(s)}(P)(\widehat{y}_{t},\widehat{y}_{t+e(s)})$ is identically true
for any $t$ such that $t\\!+\\!e(s)\\!\leqslant\\!T$, and hence it is
identically true for an arbitrarily chosen $t$ and for
$t_{1}\\!=\\!t\\!+\\!e(s)$ provided that
$t\\!+\\!e(s\\!+\\!1)\\!=\\!t_{1}\\!+\\!e(s)\\!\leqslant\\!T$. Thus, the
formulae

$\displaystyle[\Psi K(t)(\widehat{y}_{t})\ \&\
\Phi^{(s)}(P)(\widehat{y}_{t},\widehat{y}_{t+\\!e(s)})]\\!\rightarrow\\!\Psi
K(t\\!+\\!e(s))(\widehat{y}_{t+e(s)})\ \quad\textrm{and}$
$\displaystyle\\{\Psi
K(t\\!+\\!e(s))(\widehat{y}_{t+e(s)})\&\Phi^{(s)}(P)(\widehat{y}_{t+e(s)},\widehat{y}_{t+e(s+1)})\\}\\!\rightarrow\\!\Psi
K(t\\!+\\!e(s\\!+\\!1))(\widehat{y}_{t+e(s+1)})$

are identically true. Therefore, when we change the variables under the sign
of the quantifier, we obtain from this that the following formula

$\displaystyle\forall\widehat{v}\\{[\Psi K(t)(\widehat{y}_{t})\ \&\
\Phi^{(s)}(P)(\widehat{y}_{t},\widehat{v})\ \&\
\Phi^{(s)}(P)(\widehat{v},\widehat{y}_{t+e(s+1)})]\ \rightarrow$
$\displaystyle\rightarrow\ \Psi
K(t\\!+\\!e(s\\!+\\!1))(\widehat{y}_{t+e(s+1)})\\},$

is identically true as well. This formula is equivalent to $[(\Psi K(t)\ \&\
\Xi_{s+1})\\!\rightarrow\\!\Psi
K(t\\!+\\!e(s\\!+\\!1))](\widehat{y}_{t},\widehat{y}_{t+e(s+1)})$, because the
universal quantifiers will be interchanged with the quantifiers of existence,
when they are introduced into the premise of the implication. Since the
premise of the formula
$\Omega^{(s+1)}(X,P)(\widehat{y}_{t},\widehat{y}_{t+e(s+1)})$ is equivalent to
$\Psi K(t)\ \&\ \Xi_{s+1}$ in accordance with the foregoing argument, the
inductive step of Item (ii) is proven in one direction.

Now let the configurations $L(t+\\!e(s+\\!1))$ and $K(t+\\!e(s+\\!1))$ be
different. For some $\widehat{v}_{1},\widehat{y}_{t+e(s+1)}$, the formula

$\\{[\Psi K(t\\!+\\!e(s))\ \&\ \Phi^{(s)}(P)]\rightarrow\Psi
K(t+\\!e(s+\\!1))\\}(\widehat{v}_{1},\widehat{y}_{t+e(s+1)})$

is true, but

$\\{[\Psi K(t\\!+\\!e(s))\ \&\ \Phi^{(s)}(P)]\rightarrow\Psi
L(t+e(s+\\!1))\\}(\widehat{v}_{1},\widehat{y}_{t+e(s+1)})$

is false by the inductive assumption of Item (ii). Therefore, the conclusion
of the second formula is false, and its premise is true, i.e., the $\Psi
L(t+e(s\\!+\\!1))(\widehat{y}_{t+e(s+1)})$ is false, and the
$\Phi^{(s)}(P)(\widehat{v}_{1},\widehat{y}_{t+e(s+1)})$ and the $\Psi
K(t+e(s))(\widehat{v}_{1})$ are true. Since the last formula and the $\Psi
K(t)(\widehat{v}_{0})$ are true for some special $\widehat{v}_{0}$, which
exists due to induction proposition of Item (i), the formula
$\Phi^{(s)}(P)(\widehat{v}_{0},\widehat{v}_{1})$ is true. Thus, the
implication $\\{[\Psi K(t)\ \&\ \Phi^{(s+1)}(P)]\rightarrow\Psi
L(t\\!+\\!e(s\\!+\\!1))\\}(\widehat{v}_{0},$ $\widehat{y}_{t+e(s+1)})$ has a
true premise, and a false conclusion, therefore it is not identically true.
Item (ii) is proven.

Inasmuch as the configuration $L(t\\!+\\!e(s+\\!1))$ may differ from the
current one at any position, to finish the proof of Item (i) we set the values
of the variables $\widehat{v}_{1}$ in a special manner, using the inductive
hypothesis. ∎

###  6.2 The short recording of the initial configuration and
the condition of the successful termination of the machine run

Since we have the instructions for the machine run in the idle mode (see the
beginning of Section 4), the statement that the machine $P$ accepts an input
string $X$ within $T\\!=\\!\exp(n)$ steps can be written rather brief — by
means of one quantifier-free formula of the color $T$:
$\chi(\omega)\rightleftharpoons\widehat{q}\,_{T}\\!\approx\\!(1)_{2}$. This
formula has a length of $4r\\!+\\!3$ symbols nonmetering the indices. The
writing of the first index $T$ occupies $\lfloor\lg T\rfloor\\!+\\!1$ digits
(indices are written in decimal notation, not in binary), where $\lg
m\\!=\\!\log_{10}m$, $\lfloor y\rfloor$ is the integer part of a number $y$.
The maximum length of the second indices is $\lfloor\lg r\rfloor\\!+\\!1$, and
so we have $|\chi(\omega)|\\!<\\!(4r\\!+\\!3)\cdot(\lfloor\lg
T\rfloor\\!+\\!\lfloor\lg r\rfloor\\!+\\!2)$.

The formula $\Psi K(t)$ was introduced in Subsection 4.3.2 to describe a
configuration arising after the step $t$. It is very long — much longer than
$n\cdot\exp(n)$. However, the initial configuration consists of the input
string $X$, which occupies the $|X|$ squares to the right of the edge of a
tape; the head points to this extreme left cell; and the remaining part of the
tape is empty, starting with the cell, whose number is
$|X|\\!+\\!1\\!=\\!(\widehat{\gamma})\\!+\\!1$. Therefore one can describe the
initial tape configuration $K(0)$ by a brief universal formula:

$\chi(0)\rightleftharpoons\pi_{0}(\rhd,\widehat{0},\widehat{0})\
\&\bigwedge_{0\leqslant(\widehat{\eta})_{2}\\!\leqslant|X|}\psi_{0}(\widehat{\eta}\\!\rightarrow\\!\alpha(\eta))\
\&\
\forall\widehat{u}_{0}[\widehat{u}_{0}\\!>\\!\widehat{\gamma}\rightarrow\psi_{0}(\widehat{u}_{0}\\!\rightarrow\\!\Lambda)],$

where $\Lambda$ denotes blank symbol; $\rhd$ is a sign of the left end of the
tape; and $\alpha(\eta)$ is a symbol, which is located in the number
$(\widehat{\eta})$ cell; and the $\pi$-formula of the color 0 signifies that a
mechanism is ready for the execution of the instruction
$q_{0}\rhd\\!\rightarrow\ldots$ at the zeroth instant, and the machine head is
positioned on the extreme left square of tape and scans $\rhd$ symbol.

######  Lemma 6.

(i) The formulae $\chi(0)$ and $\Psi K(0)$ are equivalent to each other.

(ii)
$|\chi(0)(\widehat{y}_{0})|\\!\leq\\!D_{2}\cdot|X|\cdot|\psi_{0}(\widehat{u}_{0}\\!\rightarrow\\!\Lambda)|$
for a proper constant $D_{2}$.

###### Proof.

(i) The quantifier-free part of the formula $\chi(0)$ simply coincides with
the initial fragment of the formula $\Psi K(0)$. If we replace the second part
of formula $\chi(0)$, which begins with the quantifiers
$\forall\widehat{u}_{0}$, with its equally matched conjunction, the rest of
the clauses from $\Psi K(0)$ will appear.

(ii) According to Lemmata 2(i) and 3, the system of inequalities
$\widehat{u}_{0}\\!>\\!\widehat{\gamma}$ has a length of the same order as
$|\psi_{0}(\widehat{u}_{0}\\!\rightarrow\\!\Lambda)|$, a quantifier prefix is
a bit shorter. Hence
$|\forall\widehat{u}_{0}[\widehat{u}_{0}\\!>\\!\widehat{\gamma}\rightarrow\psi_{0}(\widehat{u}_{0}\\!\rightarrow\\!\Lambda)]|\\!=\\!\mathcal{O}(|\psi_{0}(\widehat{u}_{0}\\!\rightarrow\\!\Lambda)|)$.
Since the expression $\chi(0)(\widehat{y}_{0})$ includes $|X|\\!+\\!1$ quasi-
equations of a form $\psi_{0}(\widehat{\eta}\\!\rightarrow\\!\alpha(\eta))$
and the timer, which have a length of the same order as
$|\psi_{0}(\widehat{u}_{0}\\!\rightarrow\\!\Lambda)|$ by Lemma 3, the whole
formula $\chi(0)(\widehat{y}_{0})$ is not more than
$D_{2}\cdot|X|\cdot|\psi_{0}(\widehat{u}_{0}\\!\rightarrow\\!\Lambda)|$ in
length for some constant $D_{2}$. ∎

###  6.3 Simulating formula $\Omega(X,P)$

Let us define

$\displaystyle\Omega(X,P)\quad\rightleftharpoons\quad\forall\widehat{y}_{0},\widehat{y}\,_{T}\
\Bigl{\\{}\ \Bigl{[}\ \chi(0)(\widehat{y}_{0})\quad\&\
\exists\,\widehat{v}_{n}\forall\,\widehat{a}_{n}\forall\,\widehat{b}_{n}\ldots\exists\,\widehat{v}_{1}\forall\,\widehat{a}_{1}\forall\,\widehat{b}_{1}\hphantom{a}$
$\displaystyle\bigl{\\{}\bigwedge\limits_{1\leqslant\,s\leqslant\,n}\bigl{[}(\widehat{a}_{s+1}\\!\approx\\!\widehat{a}_{s}\wedge\widehat{v}_{s}\\!\approx\\!\widehat{b}_{s})\
\vee(\widehat{v}_{s}\\!\approx\\!\widehat{a}_{s}\wedge\widehat{b}_{s}\\!\approx\\!\widehat{b}_{s+1})\bigr{]}\hphantom{aaaaaaa}$
(1) $\displaystyle\rightarrow\
\Phi^{(0)}(P)(\widehat{a}_{1},\widehat{b}_{1})\bigr{\\}}\Bigr{]}\ \rightarrow\
\chi(\omega)(\widehat{y}\,_{T})\Bigr{\\}},\hphantom{aaaa}$

here we designate $\widehat{a}_{n+1}\\!=\\!\widehat{y}_{0},\
\widehat{b}_{n+1}\\!=\\!\widehat{y}\,_{T}$ in the record of the ”big”
conjunction for the sake of brevity.

######  Proposition 5.

The formula $\Omega(X,P)$ has the property (ii) from the statement of Theorem
1. In other words, this sentence is true on the Boolean algebra $\mathcal{B}$
if and only if the machine $P$ accepts the input $X$ within $T$ steps.

###### Proof.

Let
$\Theta_{s}\\!=\\!\Theta_{s}(\widehat{a}_{s},\widehat{a}_{s+1},\widehat{b}_{s},\widehat{b}_{s+1})$
be a denotation for a disjunction of equalities
$(\widehat{a}_{s+1}\\!\approx\\!\widehat{a}_{s}\wedge\widehat{v}_{s}\\!\approx\\!\widehat{b}_{s})\vee(\widehat{v}_{s}\\!\approx\\!\widehat{a}_{s}\wedge\widehat{b}_{s}\\!\approx\\!\widehat{b}_{s+1})$.
If we carry the quantifiers through the subformulae, which do not contain the
corresponding variables (according to the agreement of Subsection 3.3 that a
conjunction connects more intimately than an implication), then we will obtain
that the part of the formula $\Omega(X,P)$, which is located in the big square
brackets in (1), is equivalent to each of the three following formulae:

$\displaystyle 1)\ \chi(0)(\widehat{y}_{0})\ \&\
\exists\,\widehat{v}_{n}\forall\,\widehat{a}_{n}\forall\,\widehat{b}_{n}\ldots\exists\,\widehat{v}_{1}\forall\,\widehat{a}_{1}\forall\,\widehat{b}_{1}\bigl{\\{}\bigwedge\limits_{1\leq\,s\leq\,n}\Theta_{s}\rightarrow\Phi^{(0)}(P)(\widehat{a}_{1},\widehat{b}_{1})\bigr{\\}};\hphantom{aaaaa}$
$\displaystyle 2)\ \Psi K(0)(\widehat{y}_{0})\ \&\
\exists\,\widehat{v}_{n}\forall\,\widehat{a}_{n}\forall\,\widehat{b}_{n}\ldots\exists\,\widehat{v}_{1}\forall\,\widehat{a}_{1}\forall\,\widehat{b}_{1}\bigl{\\{}\Theta_{n}\rightarrow[\Theta_{n-1}\to(\ldots\rightarrow\hphantom{aaaaaaaa}$
$\displaystyle\rightarrow\\{\Theta_{1}\to\Phi^{(0)}(P)(\widehat{a}_{1},\widehat{b}_{1})\\}\ldots)]\bigr{\\}};\hphantom{aaa}$
$\displaystyle 3)\ \Psi K(0)(\widehat{y}_{0})\ \&\
\exists\,\widehat{v}_{n}\forall\,\widehat{a}_{n}\forall\,\widehat{b}_{n}\bigl{\\{}\Theta_{n}\rightarrow\exists\,\widehat{v}_{n-1}\forall\,\widehat{a}_{n-1}\forall\,\widehat{b}_{n-1}[\Theta_{n-1}\to(\ldots\rightarrow\hphantom{aaaaa}$
$\displaystyle\rightarrow\exists\,\widehat{v}_{1}\forall\,\widehat{a}_{1}\forall\,\widehat{b}_{1}\\{\Theta_{1}\to\Phi^{(0)}(P)(\widehat{a}_{1},\widehat{b}_{1})\\})]\ldots\bigr{\\}}.\hphantom{aaaa}$

According to the definition, the formula
$\exists\,\widehat{v}_{s}\forall\,\widehat{a}_{s}\forall\,\widehat{b}_{s}(\Theta_{s}\to\Phi^{(s-1)}(P)(\widehat{a}_{s},\widehat{b}_{s}))$
contracts into the $\Phi^{(s)}(P)(\widehat{a}_{s+1},\widehat{b}_{s+1})$.
Therefore the whole $\Omega(X,P)$ is equivalent to the
$\forall\widehat{y}_{0},\widehat{y}\,_{T}\bigl{[}\bigl{(}\Psi K(0)\ \&\
\Phi^{(n)}(P)\bigr{)}\to\chi(\omega)\bigr{]}$. Consequently, based on
Proposition 4(ii) and Lemma 6(i), one could say that the formula (1) is the
modeling formula. ∎

###  6.4 The time of writing of $\Omega(X,P)$

The simulating formula $\Omega(X,P)$ is described by the definition (1) in an
explicit form, this notation allows us to design an algorithm for its
construction. It remains only to prove the properties (i) and (iii) of the
statement of Theorem 1. Before we substantiate the polynomiality of the
algorithm, we will make sure that the formula $\Omega(X,P)$ of a form (1) has
a polynomial length. We recall that the length of a formula is calculated in
the natural language — see Subsections 3.1 and 3.2.

######  Lemma 7.

There exists a constant $D\\!>\\!0$ such that it does not depend on the $P$
and $n$ and the inequalities
$|X|\leqslant|\Omega(X,P)|\leqslant\\!D\cdot|P|\cdot|X|^{2+\varepsilon}$ hold
for all the long enough $X$ and any preassigned $\varepsilon\\!>\\!0$.

###### Proof.

Many components of the modeling formula were estimated already during their
description, but their lengths were estimated on the assumption that their
subformulae are written with basic variables
$\langle\widehat{x}_{t},\widehat{q}_{t},\widehat{z}_{t},\widehat{d}_{t},\widehat{f}_{t}\rangle$,
which were denoted in Subsection 4.3 as $\widehat{y}_{t}$. However, they are
not included in the composition of the subformulae of
$\Phi^{(0)}(P)(\widehat{a}_{1},\widehat{b}_{1})$ — we have written the
variables from the tuples $\widehat{a}_{1}$ and $\widehat{b}_{1}$ instead
theirs. Namely, the first $n\\!+\\!1$ variables in the tuple $\widehat{a}_{1}$
serve as $\widehat{x}_{t}$, and they serve as $\widehat{x}_{t+1}$ in the tuple
$\widehat{b}_{1}$; the second $r\\!+\\!1$ variables in $\widehat{a}_{1}$ are
put instead of $\widehat{q}_{t}$, and they are put in place of
$\widehat{q}_{t+1}$ in $\widehat{b}_{1}$ and so on. Certainly, this
replacement has no an influence on a length of those formulae, where the
variables are located, if one disregards a length of indices.

However, the length of the indices has changed markedly. Just because of this
reason, they were earlier taken into account only implicitly for the
estimation of the lengths of the formulae, e.g., see Lemmata 2 and 4, or they
were not counted at all (see Lemma 3).

The first indices of variables of the form $\widehat{a}_{1}$ and
$\widehat{b}_{1}$ are $\lfloor\lg 1\rfloor\\!+\\!1\\!=\\!1$ in length. The
second subscripts of these variables have their lengths restricted from above
by $E\rightleftharpoons\lfloor\lg(2n\\!+\\!3r\\!+\\!5)\rfloor\\!+\\!1$. The
second indices of variables $\widehat{y}_{0}$ are shorter — they are bounded
by $E_{0}\rightleftharpoons\lfloor\max\\{\lg n,\lg(r)\\}\rfloor\\!+\\!1$;
besides, the subscripts are not included in the record of the tuples of
constants. The number $n\\!=\\!|X|$ will grow bigger than $r$, and so the
inequality $E,E_{0}\leqslant\lfloor\lg n\rfloor\\!+\\!2$ holds for the long
enough $X$. Therefore by Lemmata 3 and 4, the quasi-equations and timers of
the subformulae $\chi(0)(\widehat{y}_{0})$ and
$\Phi^{(0)}(P)(\widehat{a}_{1},\widehat{b}_{1})$ from (1), in which the tuples
$\widehat{u}(\beta)$ are not included for $\beta\\!=\\!R,L$, are not greater
than $D_{3}\cdot n\cdot(\lfloor\lg n\rfloor\\!+\\!2)$ in length; the clauses
and timers comprising the $\widehat{u}(\beta)$ have a length not more than
$D_{4}\cdot[n\cdot(\lfloor\lg n\rfloor\\!+\\!2)]^{2}$ for the suitable
constants $D_{3}$ and $D_{4}$. By Lemma 4 we have
$|\varphi(k)|\\!\leqslant\\!D_{5}\cdot[n\cdot(\lfloor\lg
n\rfloor\\!+\\!2)]^{2}$, but with another constant $D_{5}$ and for the long
enough $X$.

The system of equalities, which are under the ”big” conjunction in (1), is
$\mathcal{O}(n\cdot[n\cdot(\lfloor\lg n\rfloor\\!+\\!2)])$ in length; and the
quantifier prefix, which is situated before this conjunction, has
approximately the same length. It is easy to notice that an inequality
$(\lfloor\lg n\rfloor\\!+\\!2)^{2}\leqslant\\!n^{\varepsilon}$ holds for all
$\varepsilon\\!>\\!0$ and the big enough $n$. It follows from this and Lemma
5(ii) that $|\Omega(X,P)|\\!\leqslant\\!D\cdot|P|\cdot|X|^{2+\varepsilon}$ for
some constant $D$.∎

######  Corollary 4.

There is a constant $D_{\varepsilon}$ such that the inequality
$|\Omega(X,P)|\\!\leqslant\\!D_{\varepsilon}\cdot|P|\cdot|X|^{2+\varepsilon}$
holds for all $X$ and $P$.

###### Proof.

For each given $\varepsilon$, there exists only a finite number of the strings
$X$, for which the inequality from the statement of the lemma can be violated.
Therefore the ratio $\lceil|\Omega(X,P)|/(|P|\cdot|X|^{2+\varepsilon})\rceil$
attains its maximum for these $X$. Clearly, it is fit for our
$D_{\varepsilon}$. ∎

######  Corollary 5.

There exists a polynomial $g$ such that for all $X$ and $P$ the construction
time of the sentence $\Omega(X,P)$ is not greater than $g(|X|+|P|)$.

###### Proof.

We will at first estimate the time needed for a multi-tape Turing machine
$P_{1}$ to write down the formula $\Omega(X,P)$. The running alphabet of this
machine contains all symbols of natural language (see Subsection 3.1).

Let the input tape of the machine comprises a string $X$ and a program $P$,
and $|A|$ be a quantity of different symbols in the record of the $X$ and the
$P$. The machine $P_{1}$ can determine a length $n$ of the input $X$, a
maximal number $U$ of internal states in $P$, and a size of the $|A|$ during
one passage along its input tape. The calculation of the values of
$r\\!\leqslant\\!\log_{2}(U\\!+\\!1\\!+\\!|A|)$ and the decimal notation of it
and $n$ takes a time bounded by a polynomial of the $|P|$ and $|X|$. Further,
the $P_{1}$ moves again along the record of the $X$ and $P$ and writes the
formula $\chi(0)(\widehat{y}_{0})$ at first, after that it writes
$\Phi^{(0)}(P)(\widehat{a}_{1},\widehat{b}_{1}))$, and finally, it designs
$\Omega(X,P)$. It is clear that this process takes the time, which is no
greater than the value of $p(|X|+|P|)$ for some polynomial $p(y)$.

The single-tape variant $P_{2}$ of the machine $P_{1}$ will do the same
actions in the time equal to $g(|X|+|P|)$, which is of the form of
$\mathcal{O}([p(|X|+|P|)]^{2})$ [1, 2]. ∎

##  7 The complexity of the theory of a single equivalence relation

Let $\mathfrak{K}$ be a class of the algebraic systems, whose signature (or
underlying language) $\sigma$ contains the symbol of the binary predicate
$\backsim$, and this predicate is interpreted as an equivalence relation on
every structure of the class, in particular, $\backsim$ may be an equality
relation. We denote these relations by the same symbol.

######  Definition 3.

Let us assume that there exists a _$\backsim$ -nontrivial_ system
$\mathcal{E}$ in a class $\mathfrak{K}$, namely, such structure that contains
at least two $\backsim$-nonequivalent elements. Then the class $\mathfrak{K}$
is also termed _$\backsim$ -nontrivial_. A theory $\mathcal{T}$ is named
_$\backsim$ -nontrivial_ if it has a $\backsim$-nontrivial model. When
$\backsim$ is either the equality relation or there is such formula $N(x,y)$
of the signature $\sigma$ that the sentence $\exists x,yN(x,y)$ is consistent
with the theory $Th(\mathfrak{K})$ (or $\mathcal{T}$, or belongs to
$Th(\mathcal{E})$), and the sense of this formula is that the elements $x$ and
$y$ are not equal, then we will replace the term ”$\backsim$-nontrivial” with
_”equational-nontrivial”_.

######  Theorem 2.

Let $\mathcal{E}$, $\mathfrak{K}$, and $\mathcal{T}$ accordingly be a
$\backsim$-nontrivial system, class, and theory of the signature $\sigma$, in
particular, they may be equational-nontrivial. Then there is an algorithm such
that for every program $P$ and any input string $X$, it builds the sentence
$\Omega^{(T)}(X,P)$ of the signature $\sigma$, where
$T\\!\in\\!\\{Th(\mathcal{E}),Th(\mathfrak{K}),\mathcal{T}\\}$; this formula
possesses the properties (i) and (ii) of the word $S(P,X)$ from the statement
of Proposition 1, where $\mathcal{L}\\!=\\!T$; $F(|X|)\\!=\\!\exp(|X|)$.
Moreover, for each $\varepsilon\\!>\\!0$, there exists a constant
$E_{T,\sigma}$ such that the inequality
$|\Omega^{(T)}(X,P)|\leqslant\\!E_{T,\sigma}\cdot|P|\cdot|X|^{2+\varepsilon}$
holds true for any long enough $X$.

###### Proof.

At first, for given $X$ and $P$, we write a simulating sentence $\Omega(X,P)$
of the theory of the Boolean algebra $\mathcal{B}$ in the signature
$\langle\cap,\cup,C,0,1\rangle$ with the equality symbol $\approx$, applying
Theorem 1. Then, we will transform it in the required formulae
$\Omega^{(T)}(X,P)$ within polynomial time.

For the sake of simplicity of denotations, we assume that the $\backsim$\-
nontrivial structure $\mathcal{E}$ is a model for the theory $\mathcal{T}$,
belongs to the class $\mathfrak{K}$, and has the signature $\sigma$.

Let $\varphi$ be a sentence of Boolean signature. We will construct the closed
formulae $\varphi^{(2.j)}$ so that
$\mathcal{B}\\!\models\\!\varphi\Leftrightarrow\mathcal{E}\\!\models\\!\varphi^{(2.j)}$,
where $j$ can be 0,1, or 2 depending on the signature $\sigma$.

We consider the case, when the $\sigma$ contains the equivalence symbol
$\backsim$ and the two constant symbols $c_{0}$ and $c_{1}$ such that
$\mathcal{E}\\!\models\\!\neg c_{0}\\!\backsim\\!c_{1}$. In the first stage,
we accordingly replace each occurrence of the subformulae of the kind $\exists
y\psi$; $\forall x\psi$; $t\\!\approx\\!s$ with the formulae $\exists
y((y\\!\backsim\\!c_{0}\vee y\\!\backsim\\!c_{1})\wedge\psi)$; $\forall
x((x\\!\backsim\\!c_{0}\vee x\\!\backsim\\!c_{1})\\!\rightarrow\\!\psi)$;
$t\\!\backsim\\!s$, where $t$ and $s$ are the terms.

We carry out the second stage’s transformations during several passages until
the formula ceases to change. In this stage, a) we replace the subformulae of
the kind $C(t)\\!\backsim\\!s$ and $t\\!\backsim\\!C(s)$ with the formula
$\neg\,t\\!\backsim\\!s$; if a term $u$ is not the constant 0 or 1, then we
replace b) the subformulae of the kind
$t_{1}\\!\cup\\!t_{2}\\!\cup\\!\ldots\\!\cup\\!t_{s}\backsim\\!u$ and
$u\backsim\\!t\\!\cup\\!t_{1}\\!\cup\\!t_{2}\\!\cup\\!\ldots\\!\cup\\!t_{s}$
with the formula $[(t_{1}\\!\backsim\\!c_{1}\vee
t_{2}\\!\backsim\\!c_{1}\vee\ldots\vee
t_{s}\\!\backsim\\!c_{1})\\!\rightarrow\\!u\\!\backsim\\!c_{1}]\wedge[(t_{1}\\!\backsim\\!c_{0}\wedge
t_{2}\\!\backsim\\!c_{0}\wedge\ldots\wedge
t_{s}\\!\backsim\\!c_{0})\rightarrow u\\!\backsim\\!c_{0}]$; and c) the
subformulae $t_{1}\\!\cap\\!t_{2}\\!\cap\ldots\\!\cap\\!t_{s}\\!\backsim\\!u$
and $u\\!\backsim\\!t_{1}\\!\cap\\!t_{2}\\!\cap\ldots\\!\cap\\!t_{s}$ with the
formula $[(t_{1}\\!\backsim\\!c_{0}\vee t_{2}\\!\backsim\\!c_{0}\vee\ldots\vee
t_{s}\\!\backsim\\!c_{0})\\!\rightarrow\\!u\\!\backsim\\!c_{0}]\wedge[(t_{1}\\!\backsim\\!c_{1}\wedge
t_{2}\\!\backsim\\!c_{1}\wedge\ldots\wedge
t_{s}\\!\backsim\\!c_{1})\rightarrow u\\!\backsim\\!c_{1}]$.We complete the
second stage by replacing the constants 0 and 1 with the constants $c_{0}$ and
$c_{1}$, respectively.

After the second stage, the resulting record can contain symbols $\cup,\ \cap$
of the signature of Boolean algebras. In the third stage, we replace
accordingly each occurrence of the subformulae of the kind $t_{1}\\!\cup
t_{2}\\!\cup\\!\ldots\\!\cup t_{s}\\!\backsim\\!c_{1}$, $t_{1}\\!\cap
t_{2}\\!\cap\ldots\\!\cap t_{s}\\!\backsim\\!c_{1}$,
$t_{1}\\!\cup\\!t_{2}\\!\cup\\!\ldots\\!\cup\\!t_{s}\\!\backsim\\!c_{0}$,
$t_{1}\\!\cap\\!t_{2}\\!\cap\ldots\\!\cap\\!t_{s}\\!\backsim\\!c_{0}$ with the
formulae $t_{1}\\!\backsim\\!c_{1}\vee t_{2}\\!\backsim\\!c_{1}\vee\ldots\vee
t_{s}\\!\backsim\\!c_{1}$, $t_{1}\\!\backsim\\!c_{1}\wedge
t_{2}\\!\backsim\\!c_{1}\wedge\ldots\wedge t_{s}\\!\backsim\\!c_{1}$,
$t_{1}\\!\backsim\\!c_{0}\wedge t_{2}\\!\backsim\\!c_{0}\wedge\ldots\wedge
t_{s}\\!\backsim\\!c_{0}$, $t_{1}\\!\backsim\\!c_{0}\vee
t_{2}\\!\backsim\\!c_{0}\vee\ldots\vee t_{s}\\!\backsim\\!c_{0}$.

We execute these transformations as long as the record contains at least one
symbol of the signature of Boolean algebras. The number of such symbols is
decreased at least by one on every passage for the second and third stage, and
the first stage can be realized on the only passage. So we need at most $n$
passages, where $n$ is a length of the sentence $\varphi$. The length of the
whole record grows linearly on each pass, since the transformation of the kind
b) or c) of the second stage is longest, but it increases the length no more
than in five times (for $s=2$).

Nevertheless, the length of the resulting record
$\varphi^{(2.0)}\rightleftharpoons\varphi^{\backsim}_{c_{0},c_{1}}$ can
increase non-linearly in common case. For instance, if $\varphi$ contains an
atomic formula of the kind

$\bigcup_{i}\Bigl{\\{}\bigcap_{j}\Bigl{[}\bigcup_{k}\Bigl{(}\ldots\Bigr{)}\Big{]}\Big{\\}}\approx
u,$

where the number of the alternations of the ”big” conjunctions and
disjunctions depends on the $n$.

However, there are not such subformulae in the sentence $\Omega(X,P)$
simulating for the theory of algebra $\mathcal{B}$. Indeed, in accordance with
its definition, the conversion of the subformulae of the kind
$\widehat{x}_{t}\\!\approx\\!\widehat{u}(\beta)$ (this is the system of
equalities) and $\neg\,\widehat{w}\\!\approx\\!\widehat{u}(\beta)$ (this is
the disjunction of inequalities) make the most increase if
$\beta\\!\in\\!\\{R,L\\}$, because they comprise the atomic formulae of the
form $x_{t,j}\\!\approx\\!u_{j}\oplus u_{j+1}^{\beta}\cdot\ldots\cdot
u^{\beta}_{n}$ and $\neg\,w_{j}\\!\approx\\!u_{j}\oplus
u_{j+1}^{\beta}\cdot\ldots\cdot u^{\beta}_{n}$, where $u_{k}^{\beta}$ is
either $u_{k}$ for $\beta\\!=\\!R$ or $Cu_{k}$ for $\beta\\!=\\!L$ — see
Subsection 3.3. We recall that these subformulae are
$x_{t,j}\\!\approx\\![u_{j}\cap C(u_{j+1}^{\beta}\cap\ldots\cap
u^{\beta}_{n})]\cup[Cu_{j}\cap u_{j+1}^{\beta}\cap\ldots\cap u^{\beta}_{n}]$
and $\neg\,w_{j}\\!\approx\\![u_{j}\cap C(u_{j+1}^{\beta}\cap\ldots\cap
u^{\beta}_{n})]\cup[Cu_{j}\cap u_{j+1}^{\beta}\cap\ldots\cap u^{\beta}_{n}]$
by our denotation. So, we need to perform only the three transformations of
the kind b) and c) in order to convert the sentence $\Omega(X,P)$ into the
$\Omega(X,P)^{(2.0)}$. Therefore the estimation
$|\Omega(X,P)^{(2.0)}|\leqslant D_{0}|\Omega(X,P)|$ is valid for appropriate
constant $D_{0}$. Since one can execute every passage of any stage within
$\mathcal{O}(|\Omega(X,P)|^{2})$ steps, the entire transformation takes the
polynomial time.

Let us suppose that the signature of the structure $\mathcal{E}$ has no the
constant symbols. Then we replace the constants $c_{0}$ and $c_{1}$ in the
formula $\varphi^{(2.0)}\rightleftharpoons\varphi^{\backsim}_{c_{0},c_{1}}$
with the new variables $a$ and $b$, respectively. We obtain the formula
$\varphi^{\backsim}_{a,b}$, and write additionally the prefix after that:
$\varphi^{(2.1)}\rightleftharpoons\exists a,b[\neg\,a\\!\backsim\\!b\ \&\
\varphi^{\backsim}_{a,b}]$. It is clear that $|\varphi^{(2.1)}|\leqslant
2|\varphi^{(2.0)}|$ for $|\varphi^{(2.0})|\geqslant 11$, and so
$|\Omega(X,P)^{(2.1)}|\leqslant D_{1}|\Omega(X,P)|$ for appropriate constant
$D_{1}$.

Finally, when the signature $\sigma$ does not contain the equivalence symbol,
but there exists a formula $N(x,y)$, which asserts that the elements $x$ and
$y$ is not equal, then we replace every occurrence of the atomic subformula of
the kind $t\\!\backsim\\!s$ in the $\varphi_{a,b}^{\backsim}$ with the formula
$\neg N(t,s)$ and add the prefix: $\varphi^{(2.2)}\rightleftharpoons\exists
a,b[N(a,b)\ \&\ \varphi_{a,b}^{N}]$. It is obvious that
$|\varphi^{(2.2)}|\leqslant|N(x,y)|\cdot|\varphi^{2.1}|$, hence
$|\Omega(X,P)^{(2.2)}|\leqslant D_{2}|\Omega(X,P)|$ for some constant $D_{2}$.

One can easily prove by induction on the complexity of the formulae that the
condition $\mathcal{B}\models\varphi$ is equally matched to one of the
following conditions (depending on the signature $\sigma$): either
$\mathcal{E}\models\varphi^{(2.0)}$, or $\mathcal{E}\models\varphi^{(2.1)}$,
or $\mathcal{E}\\!\models\\!\varphi^{(2.2)}$. It is clear that if
$\mathfrak{K}$ and $\mathcal{T}$ are the equational-nontrivial class and
theory respectively, then the condition $\mathcal{B}\models\varphi$ is also
equally matched to the conditions $Th(\mathfrak{K})\,\vdash\forall
a,b(N(a,b)\\!\rightarrow\\!\varphi^{N}_{a,b})$ and
$\mathcal{T}\vdash\\!\forall a,b(N(a,b)\\!\rightarrow\\!\varphi^{N}_{a,b})$.∎

######  Corollary 6.

The recognition complexity of each $\backsim$-nontrivial decidable theory
$\mathcal{T}$, in particular, equational-nontrivial, has the non-polynomial
lower bound, more precisely

$\mathcal{T}\notin DTIME(\exp(D_{T,\sigma}\cdot
n^{\delta})),\qquad\textrm{where}\ \ \delta\\!=\\!(2+\varepsilon)^{-1},\ \
D_{T,\sigma}\\!=\\!(E_{T,\sigma})^{-\delta}.$

###### Proof.

It immediately follows from the theorem and Corollary 1. ∎

##  8 Results and Discussion

Let us notice that nearly all of the decidable theories mentioned in the
surveys [6, 15] are nontrivial regarding equality or equivalence. So, if we
regard ”the polynomial algorithm” as a synonym for ”the fast-acting
algorithm”, then the quickly decidable theories are almost completely absent.
Furthermore, the examples given in the introduction and [4, 7, 8, 12, 13, 14,
15, 16, 17, 19] show that the complexity of the recognition procedures can be
perfectly enormous for many natural, and seemingly, relatively simple
theories.

It seems plausible that the estimation obtained in Corollary 2 is precise
enough. One can substantiate this assertion, if firstly, to find the upper
bound on the recognition complexity of theory $Th(\mathcal{B})$ by the
multitape Turing machines; secondly, to obtain the lower bound for this
complexity for the same machines. The author suspects that the inequalities
from Item (iii) of the main theorem are valid as well for the $k$-tape
machines, but the constant $D$ must be about in $k$ times bigger at that.

Let us point out that the number of the alternation of quantifiers depends on
the input length in the modeling formula $\Omega(X,P)$. Therefore this
sentence does not belong to any class of polynomial hierarchy. However, if one
can build the $\Omega(X,P)$ belonging to $\Delta_{k}^{\mathbf{P}}$ for some
$k\\!>\\!1$, then the class $\mathbf{P}$ will be different from this
$\Delta_{k}^{P}$, hence the $\mathbf{P}$ will be not equal to the
$\mathbf{NP}$ [14].

###  8.1 The totality and locality of the simulating methods

The method of Cook’s formulae has arisen for the modeling of the
nondeterministic Turing machine actions within polynomial time, and the
construction of Stockmeyer and Meyer is also applicable for the same
simulation in polynomial space, provided that the running time of the machine
is exponential. This is a significant advantage of these techniques.

However, our method of modeling by means of formulae is ineligible for
nondeterministic machines. More precisely, such modeling formula must be
exponential in length, when the machine runs in exponential space within the
exponential time. Unfortunately, the corresponding example is too cumbersome
for this paper. This example rests on that simple fact that if we set the
values of the basic color $t$ variables, then we can ”see” only at most two
the tape squares (the $\widehat{x}_{t}$th and maybe $\widehat{z}_{t}$th) when
we are situated within the framework of our approach — see the proof of
Proposition 2. So our simulating method is strictly local, pointwise. At the
same time, the techniques of Cook and Stockmeyer and Meyer are total, since
they allow to ”see” all of the tape cells simultaneously at any instant. These
methods are also complete in the sense that we will point in the next
subsection.

The author is sure that the technique of the direct encoding of machines
continues to be a potent tool for investigating the computational complexity
of theories, despite the emergence of other powerful approaches for obtaining
the lower bounds on this complexity such as the Compton and Henson method [4]
or the method of the bounded concatenations of Fleischmann, Mahr, and Siefkes
[8].

Nevertheless, the author agrees with the opinion that the coding of the
machine computations into the models of the theory being studied is the very
difficult task in many cases. Such coding is partly like to the modeling of
the machine actions with the aid the defining relations, when one wants to
prove the insolubility of some algorithmically problem for the finitely
presented algebraical structures of given variety (see, for instance, [3,
10]).

In both cases, we have the strong restrictions, which are dictated by the
necessity to be within the framework of the given signature or variety. But
the case of the algorithmic problem for the finitely presented structures is,
perhaps, somewhat easier than the simulation of computations by means of the
formulae of a certain theory. In the first case, we can apply the suitable
words consisting of the generators of the algebraical system for the
description of tape configurations or their parts. The value of these words
can change depending on the defining relations and the identity of variety.
However, these changes have the local character relatively of the entire
structure; whereas the variables can take on any values inside the system when
we make a simulation in the second case.

The task becomes slightly easier if there are some constants in the theory
signature. Just for this reason, we work with the Boolean algebra having two
elements, but not with the language $TQBF$ consisting of the true quantified
Boolean formulae.

Note also, that the actions simulation of the computational mechanisms, which
is realized in [3] and [10] (these devices are the Minsky machines in the
former, and they are the Minsky operators algorithms in the latter), is total.
On the other hand, this modeling is somewhat like the Compton and Henson
method too. Indeed, in all of these cases, the coding of computations is done
once and for all. In [4], this is made for Turing machines in proving the
inseparability results; then, the authors transfer the obtained lower bounds
from one theory to another, using interpretations. Both in [3] and in [10],
such simulation is made in proving the insolubility of the words problem for
the appropriate module over a certain integral domain; afterward, this module
is embedded (isomorphically in the first article and homomorphically in the
second) in the solvable group under construction.

###  8.2 Complete simultaneous and
conventionally consistent modeling

Let us investigate the modernization of the Stockmeyer and Meyer method that
arose in this paper.

####  8.2.1 A modernization to some extent is present

When we were saying that the formula $A_{0,m}$ (from the proof of Theorem 4.3
in [18]) is the analog of the $\Omega^{(0)}(X,P)$ in Remark 4, we had in mind
that the $A_{0,m}(\widetilde{U},\widetilde{V})$ consists of the conjunction of
the subformulae $u_{1}\ldots u_{m}$, $v_{1}\ldots v_{m}$, which describe the
adjacent configurations, and also of the subformula that describes the
transformation from the former to the latter. One can consider that this
transfer formula has the kind
$A_{t}\&B_{t}\&C_{t}\&D_{t}\&A_{t+1}\&B_{t+1}\&C_{t+1}$
$\&D_{t+1}\&E_{t,t+1}$, where the $A_{t},A_{t+1},B_{t},B_{t+1},C_{t},C_{t+1},$
$D_{t},D_{t+1}$, and $E_{t,t+1}$ are the subformulae of the formulae
$A,B,C,D$, and $E$ respectively from the proof of Theorem 10.3 in [1] and are
obtained from them by means the restriction of the last formulae on the fixed
value of the parameter $t$. One can say that the complete simultaneous
modeling of actions has been applied there. So one can regard the $A_{0,m}$ in
the kind

$configuration(t)\ \&\ configuration(t+1)\ \&\ step(t+1).$

But the formula $\Omega^{(0)}(X,P)(\widehat{y}_{t},\widehat{y}_{t+1})$ is
constructed in another way. It asserts that if the descriptions of the $t$th
step’s configuration (the formula $\Psi K(t)(\widehat{y}_{t})$) and of the
step $t+1$ (the $\Phi^{(0)}(P)(\widehat{y}_{t},\widehat{y}_{t+1})$) are
correct, then the configuration, which appeared after this step, will be
adequately described as well (by the $\Psi K(t\\!+\\!1)(\widehat{y}_{t+1})$).
We call this approach as a conventionally consistent modeling of actions,
i.e., the $\Omega^{(0)}(X,P)$ has such structure:

$configuration(t)\ \&\ step(t+1)\to configuration(t+1).$

Thus, the designs of the formulae
$\Omega^{(0)}(X,P)(\widehat{y}_{t},\widehat{y}_{t+1})$ and
$A_{0,m}(\widetilde{U},\widetilde{V})$ are essentially different, if even one
does not take into consideration the presence of the inner quantifiers in the
former. Furthermore, their free variables ”demand” the quantifiers of the
various kind in order the formulae become true. Seemingly, just this
difference in the external quantifiers dictates the diversity, above
mentioned, in the internal structure of these formulae.

The additional argument for this conclusion is that the conventionally
consistent modeling is also used in [3] and [10]. Recall in this connection
that the investigation of the finitely presented algebraic system, which is
given with the aid of the generators $g_{1},\ldots,g_{k}$ and the defining
relations $R_{1}(g_{1},\ldots,g_{k}),\ldots,$ $R_{m}(g_{1},\ldots,g_{k})$, is
equivalent (in many respects) to the study of the formulae of the kind

$\forall g_{1}\ldots\forall
g_{k}[(R_{1}(g_{1},\ldots,g_{k})\&\ldots\&R_{m}(g_{1},\ldots,g_{k}))\rightarrow
S(g_{1},\ldots,g_{k})].$

Furthermore, we can see in Proposition 2(i) that the $\Omega^{(0)}(X,P)$ can
completely model too, but existential quantifiers are applied at that.

Let us notice that the author applies an internal compression of simulating
formulae when defining the formulae
$\Phi^{(s+1)}(P)(\widehat{y}_{t},\widehat{y}_{t+e(s+1)})$ in Subsection 4.3.2.
The compression is internal, since figuratively speaking, the ”compressing
spring”, which is the subformula
$\exists\,\widehat{v}\,\forall\,\widehat{a}\,\forall\,\widehat{b}\bigl{[}(\widehat{y}_{t}\\!\approx\\!\widehat{a}\
\wedge\
\widehat{v}\\!\approx\\!\widehat{b})\vee(\widehat{v}\\!\approx\\!\widehat{a}\
\wedge\ \widehat{b}\\!\approx\\!\widehat{y}_{t+e(s+1)})\bigr{]}$, is inserted
inside this $\Phi^{(s+1)}(P)$, i.e., this ”spring” is located deep inside the
modeling formula $\Omega^{(s+1)}(X,P)$. From this standpoint, Stockmeyer and
Meyer use the method of an ”external compression”, as their simulating formula
$A_{s+1,m}$ contains similar ”compressing spring” at the its ”surface”, if it
is considered as the analog of the $\Omega^{(0)}(X,P)$.

####  8.2.2 Seemingly, there is almost no modernization

However, the author is inclined to believe nevertheless that the analog of the
formula $A_{0,m}(\widetilde{U},\widetilde{V})$ is the
$\Phi^{(o)}(P)(\widehat{y}_{t},\widehat{y}_{t+1})$. In other words, the former
corresponds to the
$A_{t}\&B_{t}\&C_{t}\&D_{t}\&A_{t+1}\&B_{t+1}\&C_{t+1}\&D_{t+1}\&E_{t,t+1}$
(see the first paragraph of the previous subsubsection), i.e., this formula
simply describes the transformation of one configuration to another, but it
does not contain the descriptions of these configurations (the formulae
$u_{1}\ldots u_{m}$ and $v_{1}\ldots v_{m}$) in explicit form.

This is supported by the fact that the descriptions of intermediate
configurations do not enter into the formula from the proof of Cook’s theorem
(Theorem 10.3) in [1]. Their inclusion will lead to an increase in the length
of the entire modeling formula almost in $2p(n)$ times in the case of Cook’s
theorem, and this increase will be linear in the proof of Theorem 4.3 in [18].
Certainly, that is not essential for the proof of these theorems, but this
inclusion makes the simulating formulae be excessively cumbersome. And what is
more, there is no need for this.

Indeed, one can easily prove by induction in this case that if

$B_{s,m}(\widetilde{U},\widetilde{V})\ \rightleftharpoons\ u_{1}\ldots u_{m}\
\&\ A_{s,m}\ \&\ v_{1}\ldots v_{m},$

then
$\exists\widetilde{U}\exists\widetilde{V}B_{s,m}(\widetilde{U},\widetilde{V})$
is true if and only if the configuration encoded by $v_{1}\ldots v_{m}$
follows from the configuration that corresponds to $u_{1}\ldots u_{m}$ in at
most $\exp(s)$ steps of the $P$. So this
$B_{s,m}(\widetilde{U},\widetilde{V})$ is the simulating formula in [18], and
it is analog of our $\Omega^{(s)}(X,P)(\widehat{y}_{t},\widehat{y}_{t+e(s)})$.

Thus, the Stockmeyer and Meyer method uses, seemingly, the internal
compression of modeling formulae as our one. Nevertheless, this simulating
method does not cease to be complete and simultaneous.

###  8.3 Open problems

It is well known that the theory of two equivalence relations is not
decidable, but the theory of one such relation $\sim$ is decidable [6]. Now it
turns out according to Corollary 6 that although it is decidable, but for a
very long time.

What will happen if we add some unary predicates or functions to the signature
with the only equivalence symbol $\sim$ so that the resulting theory remains
decidable? Will it be possible to find such functions and/or predicates in
order that the recognition complexity ”smoothly” increases? We can formulate
this in a more precise way.

######  Problem 1.

Let $\sigma_{0},\sigma_{1},\ldots$ be a sequence of signatures such that
$\sigma_{0}\\!\supseteq\\!\\{\sim\\}$ or
$\sigma_{0}\\!\supseteq\\!\\{\approx\\}$ and $\sigma_{i}\subset\sigma_{i+1}$
for each natural $i$. Does there exist a sequence of the algebraical
structures $\mathfrak{M}_{0},\mathfrak{M}_{1},\ldots$ such that their
signature accordingly are $\sigma_{0},\sigma_{1},\ldots$ and

$Th(\mathfrak{M}_{j})\\!\in DTIME(\exp_{j+2}(n))\ \setminus\
DTIME(\exp_{j+1}(n))?$

Recall that $Th(\mathfrak{M})$ denotes the first-order theory of the system
$\mathfrak{M}$. It is possible that there already is a candidate for the like
sequence of the higher-order theories with the ”smoothly” increasing
recognition complexity.

######  Problem 2.

Let $\Omega^{(k)}$ be a fragment of the type theory $\Omega$ from [19], which
is obtained with the aid the restriction of the types of variables by level
$k$. Can one point out for each natural $k$ such a number $s$ that
$\Omega^{(k)}\\!\in DTIME(\exp_{k+s+1}(n))\ \setminus\ DTIME(\exp_{k+s}(n))$?

######  Problem 3.

It seems quite plausible that the theory of finite Boolean algebras has a
double exponential as the lower bound on the complexity of recognition.

######  Problem 4.

Let $F(n)$ be a limit upper bound for all polynomials (see Definition 2). What
algebraic and/or model-theoretic properties must be possessed an algebraical
structure $\mathfrak{A}$ in order that $Th(\mathfrak{A})\\!\in\\!DTIME(F(n))$
or $Th(\mathfrak{A})\\!\notin\\!DTIME(F(n))$ holds true?

## References

  * [1] 888We quote from this book and [9] and from review [6] by their versions in Russian. Aho A.V., Hopcroft J.E., and Ullman J.D. The design and analysis of computer algorithms — Massachusetts: Addison-Wesley Publishing Company, Reading, 1976.
  * [2] Arora S. and Barak B. Computational Complexity: A Modern Approach – Published by Cambridge University Press, 2009.
  * [3] Baumslag G., Gildenhuys D., Strebel R. Algorithmically insoluble problems about finitely presented solvable groups, Lie and associative algebras I // J. Pure and Applied Algebra. — 1986. — Vol. 39, No. 1–2. — P. 53–94.
  * [4] Compton K.J. and Henson C.W. A uniform method for proving lower bounds on the computational complexity of logical theories // Ann. Pure Appl. Logic. — 1990. — Vol. 48 — P. 1–79.
  * [5] Cook S.A. The complexity of theorem-proving procedures // in Proc. of the 3rd Annual ACM Symposium on the Theory of Computing — Ohio: Shaker Heights — 1971. — P. 151–159.
  * [6] Ershov Y.L., Lavrov I.A., Taimanov A.D., and Taitslin M.A. Elementary theories // Russian Math, Surveys. — 1965. — Vol. 20\. — P. 35–100 (English translation).
  * [7] Fisher M.J. and Rabin M.O. Super exponential complexity of Presburger’s arithmetic // SIAM, AMS Proceedings. — 1974. Vol. 7. — P. 27–41.
  * [8] Fleischmann K., Mahr B., and Siefkes D. Bounded concatenation theory as a uniform method for proving lower complexity bounds // in: R. Gandy, M. Hyland, eds. — North-Holland, Amsterdam: Logic Colloquium. — 1977\. Vol. 76. — P. 471–490.
  * [9] Garey M.R. and Johnson D.S. Computers and Intractability: A Guide to the Theory of NP-completeness — New York: Freeman, 1979.
  * [10] Latkin I.V. The Occurrence Problem for Subvarieties of the Variety ${\bf N}_{2}{\bf A}$ Revisited // Algebra and Logic. — 2001. — Vol. 40, No 5 — P. 327–333.
  * [11] Malcev A.I. Algorithms and recursive functions — Groningen: Wolters–Noordhoff Pub. Co. — 1970.
  * [12] Meyer A.R. Weak monadic second order theory of successor is not elementary-recursive // Technical Report (Memo 38) Massachusetts Institute of Technology Cambridge, MA, USA, 1973.
  * [13] Meyer A.R. The inherent complexity of the theories of ordered sets // in: International Congress of Mathematians. Vancouver, 1974\. — also in Canadian Math. Congress , 1975. — P. 477–482.
  * [14] Meyer A.R. and Stockmeyer L.J. The equivalence problem for regular expressions with squaring requires exponetial space // in: Proc. Thirteenth Annual IEEE Symposium on Switching and Automata theory, 1972. — P. 125–129.
  * [15] Rabin M.O. Decidable theories // in Handbook of mathematical logic, Part C., Ch III, Ed. J. Barwise, Amsterdam, New York: Elsevier, Eighth impression, 1999. — P. 596–629.
  * [16] Robertson E.L. Structure of complexity in the weakmonadic second-order theories of the natural numbers // Research Report CS-73-31, Dept. of Applied Analysis and Computer Science, kiv. of Waterloo, Dec., 1973; also Proc. 6th ACM Symp. on Theory of Computing, 1974. — P. 161–171.
  * [17] Stockmeyer L.J. The complexity of decision problems in automata theory and logic // PhD thesis, MIT Lab for Computer Science, 1974; also /MIT/LCS TechRep 133.
  * [18] Stockmeyer L.J. and Meyer A.R. Word problems requiring exponential time // in Proc. 5th Ann. ACM Symp. on the Theory of Computing, New York: Association for Computing Machinery, 1973. — P. 1–9.
  * [19] Vorobyov S. The most nonelementary theory // Information and Computation, 2004. — Vol. 190. — P. 196–219.