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$ – Maxime Ramzi Apr 18 '19 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 '19 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$ – Maxime Ramzi Apr 18 '19 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 '19 at 0:07
  • $\begingroup$ @Asaf haha, point(s) taken. $\endgroup$ – Mark Kamsma Apr 19 '19 at 10:14

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.

| cite | improve this answer | |

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.