The recognition complexity of decidable theories

We will find a lower bound on the recognition complexity of the decidable theories that are nontrivial relative to equality, namely, each of these theories is consistent with the formula, whose sense is that there exist at least two distinct elements. However, at first, we will obtain a lower bound on the computational complexity for the first-order theory of the Boolean algebra that contains 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 this theory to the first-order theory of pure equality.