6
$\begingroup$

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.

$\endgroup$
7
  • $\begingroup$ How do you add a function symbol for $ \log $ when it's not defined everywhere ? $\endgroup$ Commented Apr 18, 2019 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$ Commented Apr 18, 2019 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$ Commented Apr 18, 2019 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
    Commented Apr 19, 2019 at 0:07
  • $\begingroup$ @Asaf haha, point(s) taken. $\endgroup$ Commented Apr 19, 2019 at 10:14

1 Answer 1

4
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .