\documentclass[12pt]{article} 
\begin{document} 

We review the model theory of quantifier elimination (QE). In particular I 
shall prove that, for countable theories, the Strong Shoenfield QE-test is 
equivalent to the van den Dries QE-test. Using this latter test van den 
Dries showed that the theory of the reals with a predicate for the powers 
of two admits quantifier elimination in an expanded language, and is hence 
decidable. He gave a model-theoretic argument, which provides no apparent 
bounds on the complexity of a decision procedure. We provide a syntactic 
argument that yields a procedure that is primitive recursive, although not 
elementary. In particular, we show that it is possible to eliminate a 
single block of existential quantifiers in time $2^0_{O(n)}$, where $n$ is 
the length of the input formula and $2_k^x$ denotes $k$-fold iterated 
exponentiation. Some immediate consequences on decidable
recurrent relations will also be discussed, if time permits.

\end{document} 

