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.

  • $\begingroup$ How do you add a function symbol for $ \log $ when it's not defined everywhere ? $\endgroup$ – Max Apr 18 at 22:45
  • $\begingroup$ 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$. $\endgroup$ – Mark Kamsma Apr 18 at 22:48
  • $\begingroup$ 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 ) $\endgroup$ – Max Apr 18 at 22:52
  • $\begingroup$ You mentioned grading based on presentation once. I will deduct 2 points from your grade for not using \exp and \log. $\endgroup$ – Asaf Karagila Apr 19 at 0:07
  • $\begingroup$ @Asaf haha, point(s) taken. $\endgroup$ – Mark Kamsma Apr 19 at 10:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.