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

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.

• How do you add a function symbol for $\log$ when it's not defined everywhere ? Commented Apr 18, 2019 at 22:45
• You just make it 0 everywhere else (same thing happens for the analytic function symbols, they are really only defined on some bounded interval). Unfortunately, $\exists y (exp(y) = x)$ is just equivalent to $0 < x$. Commented Apr 18, 2019 at 22:48
• Ok for $\log$ . Yes, I deleted that bit because I realized it was the ordered field. Perhaps something like $\log (x) \log (y) \geq 1$ ? (I'll stop guessing after that ) Commented Apr 18, 2019 at 22:52
• You mentioned grading based on presentation once. I will deduct 2 points from your grade for not using \exp and \log. Commented Apr 19, 2019 at 0:07
• @Asaf haha, point(s) taken. Commented Apr 19, 2019 at 10:14

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)).$$