Return to Question

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.

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).$$

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.

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 $+$.

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.

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.

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)$.

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.

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 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.

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.

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)$.

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 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)$.

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$, 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.

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.