Suppose $K$ is an exponential real closed field, i.e. there is an isomorphism, say exp, between the additive group of $K$ and the multiplicative group of its positive elements. Assume further that $Z$ is an integer part of $K$ whose positive cone $Z^{\geq 0}$ is closed under exp.
(1) Does it follow (for any of the standard phrasings of $EXP$) that $Z^{\geq 0}\models IOpen+EXP$?
(2) What if we further assume that $I\models I\Delta_{0}$ (so that the possible dependence on the choice of phrasing is eliminated)?
Edit: $IOpen$ refers to the axiom system of arithmetic with induction restricted to quantifier-free formulas. EXP denotes the arithmetical statement that exponentiation is total. (In the language of arithmetic, exponentiation can e.g. be expressed by stating that $x^{y}=z$ iff there is a number coding a sequence $s$ such that $s_{0}=1$, $s_{y}=z$ and, for all integers $i$ strictly less than $y$, we have $s_{i+1}=xs_{i}$.) Shepherdson's result shows that the positive cone of an $IP$ of an $RCF$ will always be a model of $IOpen$, but $IOpen$ does not prove $EXP$ (nor does even $I\Delta_{0}$). The existence of exp for $K$ ensures that, for some $a\in I$, there is a function $f:I\rightarrow I$ such that $f(0)=1$ and $f(k+1)=af(k)$ for all $k\in I$, but that does not make it obvious (at least to me) that $I$ is 'aware' of this fact (e.g. contains the coding sequences etc.).
