Let $\mathbb R$ denote the ordered field of the reals. A well-known theorem of Wilkie [1] states that the structure $(\mathbb R,\exp)$ is model-complete (every formula is equivalent to an existential formula). Wilkie deals exclusively with the natural base-$e$ exponential function, but I’ve seen in other paper the result being applied liberally to exponentiation with other bases, in particular $(\mathbb R,2^x)$, without further elaboration. My question is whether this is warranted.

The closest I came to a published source for such a generalization is Ressayre [2], who outlines an alternative proof of Wilkie’s result, working with base-$2$ exponentiation. However, Ressayre’s argument is an incomplete sketch rather than a detailed proof, and I’m afraid that at this level of granularity, it might easily slip that a pesky extra constant is needed to make it go through. Thus I’m not really comfortable to take it at face value.

Let me disentangle what the question is really about. Recall that a function $f(\vec x)$ is existentially definable in a structure $A$ if its graph $f(\vec x)=z$ is expressible in $A$ by an existential formula. Any existentially definable function is also universally definable as $f(\vec x)=z\iff\forall z'\,(f(\vec x)=z'\to z=z')$, which easily implies that every existential formula of $(A,f)$ is equivalent to an existential formula of $A$. Let $x^y$ denote the binary exponentiation function for $x>0$, extended by, say, $x^y=0$ for $x\le 0$ to make it total. Below, definable always means definable without parameters.

Observation 1. For any $b>0$, $b\ne1$, the structures $(\mathbb R,b^x)$ and $(\mathbb R,x^y,b)$ have the same existentially definable predicates.

Proof: $b=b^1$, and $x^y=z$ is existentially definable by $(x\le0\land z=0)\lor\exists w\,(b^w=x\land b^{wy}=z)$.

Observation 2. The constant $e$ is universally definable in $(\mathbb R,x^y)$.

Proof: For example, $e=z$ iff $\forall x\,z^x\ge1+x$.

Corollary 3. The following are equivalent:

1. $(\mathbb R,2^x)$ is model-complete.
2. $(\mathbb R,b^x)$ is model-complete for every $b>0$.
3. $e$ is existentially definable in $(\mathbb R,2^x)$, or equivalently, in $(\mathbb R,x^y)$.

Proof: $2\to1$ is trivial. $3\to2$: By Wilkie’s result and Observation 1, $(\mathbb R,x^y,e)$ is model-complete. Thus, if $e$ is existentially definable in $(\mathbb R,x^y)$, then $(\mathbb R,x^y)$ is model-complete, whence $(\mathbb R,x^y,b)$ is model-complete for any $b$. $1\to3$: Since $e$ is definable in $(\mathbb R,2^x)$, it is existentially definable if this structure is model-complete.

Question. Is any of the equivalent conditions in Corollary 3 true, and if so, is there a published proof?

Of course, if someone convinces me that Ressayre’s argument actually does prove this result, such as by extracting from it an existential definition of $e$, I’ll take that.

References:

[1] Alex J. Wilkie: Model completeness results for expansions of the ordered field of real numbers by restricted Pfaffian functions and the exponential function, Journal of the American Mathematical Society 9 (1996), no. 4, pp. 1051–1094, doi 10.1090/S0894-0347-96-00216-0.

[2] Jean-Pierre Ressayre: Integer parts of real closed exponential fields, in: Arithmetic, proof theory, and computational complexity (P. Clote, J. Krajíček, eds.), Oxford University Press, 1993, pp. 278–288.