Real exponential field with restricted analytic functions: $\mathbb R_{an,\exp,\log}$ has quantifier elimination, but $\mathbb R_{an,\exp}$ does not.

Question

At a talk sometime ago a result was presented, which I believe originates from:

van den Dries, Lou; Miller, Chris, On the real exponential field with restricted analytic functions, Isr. J. Math. 85, No. 1-3, 19-56 (1994). ZBL0823.03017.

At some point it was mentioned that $\mathbb R_{an,\exp,\log}$ admits quantifier elimination while $\mathbb R_{an,\exp}$ does not. Here $\mathbb R_{an,\exp}$ is the theory of the (ordered) real exponential field with function symbols for all restricted analytic functions. Then of course $\mathbb R_{an,\exp,\log}$ is just adding a function symbol for logarithms.

Someone in the audience remarked that $\log(x)$ (or more precisely, its graph) is quantifier-free definable by $x = \exp(y)$. Then a fairly simple formula was presented to show why you really need $\log$ as a function symbol for quantifier elimination, and there is my question: I just cannot remember or reconstruct that formula. So what would be a simple example of some formula in this setting that is not equivalent to a quantifier-free formula in $\mathbb R_{an,\exp}$?

I am probably missing something obvious here, but now it's haunting me.

Answer 1

By pure coincidence I happened to come across an answer to this question while browsing David Marker's homepage. In his note A failure of quantifier elimination (with A. Macintyre), he answers exactly this question for different languages (see his homepage for a download of that file).

The short answer is that $$ \exists z (\exp(\exp(z)) = x \land y = z \exp(z)) $$ is not equivalent to a quantifier-free formula. So this is somewhat similar to one of the formulas suggested in the comments. This is even in a bigger language, but then it certainly works for my question. Just a sanity check, if we allow $\log(x)$ in our language, then this formula is equivalent to $$ x > 1 \land y = \log(x) \log(\log(x)). $$

Some more examples are mentioned in that note. It also contains a proof of why the above mentioned formula is not equivalent to a quantifier-free formula. This proof is not trivial at all, so I will not repeat it here.