General exponential inequality?

The theory $Th_{\exp,\mathrm{fields}}$ of exponential ordered fields is the first-order theory over $\left\langle +,\cdot,0,1,<,\exp\right\rangle$ whose axioms state that the model is an ordered field and $\exp$ is an isomorphism of its ordered additive group to its ordered multiplicative group of strictly positive elements.

edit: I corrected my question to see if counter-examples still exist. ANd I corrected it yet again with some context to explain.

Do you know if $\exists a \forall x(\exp(x) \geq a + x)$ is provable from $Th_{\exp,\mathrm{fields}}$?

This is true when the field is archimedean, because then it is a sub-ordered field of $\mathbb{R}$, the exponential map is uniformly continuous over bounded intervals so it can be extended to an exponential map over $\mathbb{R}$, which needs be some $x \mapsto a^x$, for which $\forall x (a^x \geq x + \frac{\ln(\ln(a)) + 1}{\ln(a)})$ holds.

For non archimedean fields, even if one can generalize the concept of derivative, one lacks the mean value theorem (or the intermediate value theorem) without which the relations between monotonicity and the sign of the derivative disappear. (moreover, I am not sure one can prove the exponential map is differentiable) So this is a totally different problem, and I wonder if there are different ways to prove the result anyway.

• You probably want to ask whether $\text{exp}(x) \geq 1+x$ only for $x \geq 0$... Also, including some motivation for why you're asking the question could help you get a better answer. For example, maybe you're really wondering about the growth rate of exp in general? Commented Oct 7, 2015 at 20:36
• Why only for positive $x$? The context is that of exponential fields, and I am interested in non-archimedean fields in particular. For archimedean fields, the exponential function $E$ satisfies $E(x) \geq x + b$ for some $b$ ($b = \frac{\ln(\ln(E(1)) + 1}{\ln(E(1))}$ where $\ln$ is the Neperian logarithm). It is the general way to prove such inequalities without the classical theorems I am interested in. (I think it is more likely that there are counter-examples) Commented Oct 7, 2015 at 22:45
• Because the sentence in your first edit, $\text{exp}(1) \geq 3 \rightarrow (\forall x\, \text{exp}(x) \geq 1 + x)$, is already false in $\mathbb{R}$ if we interpret $\text{exp}(x) = 4^x$ ($4^{-1/4} < 3/4$) Commented Oct 7, 2015 at 23:40
• I don't have a copy, but I suspect you can find an answer to your question in Salma Kuhlman's book Ordered Exponential Fields. Commented Oct 9, 2015 at 4:26
• Yes you're right, the formulation where the variable is $a$ is a better one. I have been looking for the book of Salma Kulman for some time but it is hard to find. I know someone who has it though. Commented Oct 9, 2015 at 9:01

There is nothing in your axioms that says that your $\operatorname{exp}$ function has to be natural exponentiation (i.e., exponentiation with base $e$). In particular, $(\mathbb{R},+,\cdot,0,1,<,x \mapsto (1.00001)^x) \models T_{\operatorname{exp},fields}$ as you defined it. However, $1.00001^1 = 1.00001 < 1 + 1 = 2$, showing that your sentence is not a consequence of $T_{\operatorname{exp},fields}$ as you defined it.
(BTW, Wikipedia's definition for exponential field is the same as yours, and that article also confirms that $a^x$ works as the exponential map, for arbitrary positive $a$.)