Model-completeness of real exponential fields

Question

Let $\mathbb R$ denote the ordered field of the reals (in a language with $+$, $\cdot$, and possibly $<$, $0$, $1$, or $-$; these are all existentially definable in terms of $+$ and $\cdot$ alone).

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 papers 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 $M$ if its graph $f(\vec x)=z$ is expressible in $M$ 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 $(M,f)$ is equivalent to an existential formula of $M$. 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. 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 1. Is any of the equivalent conditions in the Corollary 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.

Following up on Matt F.’s comment, every existential formula is in $(\mathbb R,2^x)$ equivalent to an existentially quantified equality of two terms in the language $(+,\cdot,2^x)$, thus $e$ is existentially definable in $(\mathbb R,2^x)$ iff there are $(+,\cdot,2^x)$-terms $t(z,\vec x)$ and $s(z,\vec x)$ such that for all $z\in\mathbb R$, $$z=e\iff\exists\vec x\in\mathbb R\:t(z,\vec x)=s(z,\vec x).$$ Another normal form is that every existential formula is in $(\mathbb R,2^x)$ equivalent to a disjunction of unnested primitive positive formulas in the language $(+,2^x)$. Moreover, if $e$ is defined by such a disjunction, it is already definable by one of the disjuncts. That is, $e$ is existentially definable in $(\mathbb R,2^x)$ iff it has a definition of the form $$e=x_0\iff\exists x_1,\dots,x_n\:\Bigl(\bigwedge_{(i,j,k)\in I}x_i+x_j=x_k\land\bigwedge_{(i,j)\in J}2^{x_i}=x_j\Bigr)$$ for some $n\in\mathbb N$, $I\subseteq\{0,\dots,n\}^3$, and $J\subseteq\{0,\dots,n\}^2$. Alternatively, one can do the same thing with $\cdot$ in place of $+$.

Another angle on the question is that all model-complete theories are axiomatizable by $\forall\exists$ sentences. The theory of $(\mathbb R,2^x)$ can be axiomatized by its $\forall\exists$ consequences together with one $\exists\forall$ sentence, such as $$\exists z\,\forall x\,2^x\ge1+zx.$$ [In general, if $c$ is definable in a structure $M$ by a universal formula $\psi(z)$, and $(M,c)$ is model-complete, then $\mathrm{Th}(M)$ is axiomatizable by its $\forall\exists$ consequences plus the $\exists\forall$-sentence $\exists z\,\psi(z)$. To see this, any sentence in the language of $M$ implied by a $\forall\exists$ sentence $\forall\vec x\,\exists\vec y\,\theta(\vec x,\vec y,c)$ of $(M,c)$ follows from $\exists z\,\psi(z)$ and the $\forall\exists$ sentence $\forall\vec x\,\forall z\,(\psi(z)\to\exists\vec y\,\theta(\vec x,\vec y,z))$.]

Question 2. Is $\mathrm{Th}(\mathbb R,2^x)$ $\forall\exists$-axiomatizable?

Following up on James Hanson’s comment, here are some examples:

• Dense linear order with one end-point: let $M=([0,+\infty),<)$ and $c=0$. Then $0$ is universally definable in $M$, and $\mathrm{Th}(M,0)$ has full quantifier elimination, but $\mathrm{Th}(M)$ is not model-complete, and not $\forall\exists$-axiomatizable. Indeed, the union of the chain of structures $[-n,+\infty)$, $n\in\mathbb N$, which are isomorphic to $M$, has no least element, and thus is not a model of $\mathrm{Th}(M)$.

• Presburger arithmetic: let $M=(\mathbb Z,+,<)$ and $c=1$. Then $\mathrm{Th}(M,1)$ is model-complete, and $1$ is universally definable in $M$, but $\mathrm{Th}(M)$ is not model-complete and not $\forall\exists$-axiomatizable, as $(n^{-1}\mathbb Z,+,<)\simeq(\mathbb Z,+,<)$ for any $n\in\mathbb N$, but $\bigcup_n(n!^{-1}\mathbb Z,+,<)=(\mathbb Q,+,<)$ is not a model of $\mathrm{Th}(M)$.

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.

Answer 1

I think the third condition is false conditional on Schanuel’s conjecture. The algorithm below handles most potential examples, with a bit of uncertainty only about to handle extra algebraic dependencies.

We can use Schanuel’s conjecture to turn potential algebraic relationships into linear relationships, by a version that looks natural constructively, and can be considered a contrapositive of the usual statement.

As an example, we have a preliminary lemma: There is no linear dependence of the form $a\ln 2 + b + c e\ln 2=0$ with rational $a,b,c$. Proof of lemma: We consider the two pairs of expressions $(u=\ln 2,\, e^u=2)$, $(v=1,\, e^v=e)$, and then have three algebraic relations among them: $e^u=2,\, v=1,\, au+b+ce^vu=0$. By Schanuel's conjecture, we must have a rational linear dependence of the form $p \ln 2+q\,1=0$, which is impossible.

Now suppose we have a definition of $e$ as suggested in the post, of minimal complexity, in the sense of using the minimum number of additions, subtractions, multiplications and exponentiations. This will have $m$ equations (that may involve polynomials and powers of two) in $m$ variables $x_1,\ldots,x_m$, jointly implying $x_1=e$. Wherever those equations include a term of the form $2^t$, we replace $t$ with $x_{m+1}$, and add the equation $x_{m+1}=t$; this gives us $m+1$ equations in $m+1$ variables. We continue this until the only powers of two which appear are of the form $2^{x_i}$, and then have $n$ algebraic equations in the $n$ variables $x_i$ and the corresponding terms $2^{x_i}$.

To use Schanuel's conjecture, we consider the $n+2$ pairs of expressions $(u=\ln 2,\, e^u=2)$, $(v=1,\, e^v=e)$, $(w_i=x_i \ln 2,\, e^{w_i}=2^{x_i})$. We can rewrite the $n$ equations above in terms of those expressions, replacing $2^{x_i}$ by $e^{w_i}$ and replacing other instances of $x_i$ by $w_i/u$. This gives $n$ algebraic relationships among the $n+2$ pairs of expressions, and then we add $e^u=2$, $v=1$, $w_1/u=e^v$ to get a total of $n+3$ algebraic relationships.

If these are $n+3$ independent algebraic relationships, then Schanuel's conjecture gives us a rational linear dependence of the form $$a u + b v + \sum c_i w_i=0$$ By the lemma, some $c_i$ must be non-zero with $i>1$. So for that $i$, so we can further transform the equations by $$w_i \to \frac{-1}{c_i}(a u + b v + \sum_{j\neq i}c_j w_j)$$ $$e^{w_i} \to \Big((e^u)^a (e^v)^b \prod_{j\neq i}(e^{w_j})^{c_j}\Big)^{-1/c_i}$$ This eliminates $x_i$ and gives $n+2$ algebraic equations in $n+1$ pairs of variables. We continue using Schanuel's conjecture to eliminate variables until we get $4$ equations in $3$ variables, and a linear dependence as in the lemma. Since this is impossible, it disproves the hypothesis that the original equations implied $x_1=e$.

Alternatively, at some point we might find that the $n+3$ algebraic relationships are not independent. In this case (the only part where I haven't figured out how to write things down in detail) we can find solutions to the equations with $x_1\neq e$, again disproving the initial hypothesis.

For example, we can carry out this process for

• an attempted definition of $e$ by itself: $2^{2^x}-x=93$
• an attempted joint definition of $e$ and $\pi$: $2^x-y/2=5$, $2^y x = 24$
• an attempted definition of $e$ that is too weak, and therefore leads to algebraic dependencies: $2^{x+3}-8 \cdot 2^x=0$

Previous versions of the post give some details for those cases.