How arithmetical is algebraic exponentiation? 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.).
 A: The answer to both questions is negative. Every countable model $\def\sM{\mathfrak M}\sM$ of $\mathit{VTC}^0$ (a very weak fragment of $I\Delta_0+\Omega_1$) is an exponential integer part of a real-closed exponential field by [1,2], hence if this property has any first-order consequences besides $\mathit{IOpen}$ at all, they are included in $\mathit{VTC}^0$.
The basic idea is to take for $K$ the completion $\mathbf R^\sM$ of the fraction field $\mathbf Q^\sM$ of $\sM$. This is a real-closed field as $\sM\models\mathit{IOpen}$, and with some effort, one can show that the usual exponential function $2^n\colon\mathbf L^\sM\to\sM$ (where its domain $\mathbf L^\sM$ is the set of logarithmic natural numbers of $\sM$) extends to an isomorphism $2^x\colon(\mathbf R_{\mathbf L}^\sM,+,{<})\simeq(\mathbf R_{>0}^\sM,\cdot,{<})$, where $\mathbf R_{\mathbf L}^\sM=\{x\in\mathbf R^\sM:\exists n\in\mathbf L^\sM\,|x|\le n\}$ is the set of logarithmically bounded reals of $\sM$. Moreover, if $\sM$ is nonstandard, then $(\mathbf Q^\sM,\mathbf Z^\sM,\mathbf Q_{\mathbf L}^\sM,+,{<})$ is recursively saturated, where $\mathbf Z^\sM$ is the extension of $\sM$ with negative numbers. If $\sM$ is countable,  one can use this to construct an isomorphism $(\mathbf R^\sM,\mathbf Z^\sM,+,{<})\simeq(\mathbf R_{\mathbf L}^\sM,\mathbf Z_{\mathbf L}^\sM,+,{<})$, whose composition with $2^x$ yields the desired exponential on $\mathbf R^\sM$.
References
[1] Emil Jeřábek: Elementary analytic functions in $\mathit{VTC}^0$, arXiv:2206.12164 [cs.CC], 55 pp., 2022.
[2] Emil Jeřábek: Models of $\mathit{VTC^0}$ as exponential integer parts, arXiv:2209.01197 [math.LO], 21 pp., 2022.
