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

-
Just to be certain, by IOpen you mean induction for "open" formulas in the language including exp? And what exactly is the sentence EXP? The statement that exp is an isomorphism? And if the answers are yes and yes, then doesn't Shepherdson's proof for plain old IOpen work here? If I remember right, it just uses the fact that K is o-minimal. –  SJR Oct 29 '12 at 15:02
Yes, that is what I meant. I have added a clarification to my addmitedly not very self-contained post. –  M Carl Oct 29 '12 at 15:28
Sorry, I misread your first question. 'exp' is not supposed to be included in the language. –  M Carl Oct 29 '12 at 15:30
I’m afraid your definition of EXP is not specific enough. There are many possible definitions of exponentiation; in the context of $I\Delta_0$, any two $\Delta_0$ definitions which provably satisfy some basic recurrence axioms will be provably equivalent, hence it is not necessary to specify the axiom exactly, but these definitions will be no longer equivalent in IOpen. (E.g., in your proposed wording, different coding schemes for sequences may lead to different definitions.) –  Emil Jeřábek Oct 29 '12 at 16:33
Having said that, since exp is not necessarily definable in $Z$, I would expect the answer to be negative due to phenomena like mathoverflow.net/questions/94928, but I’m not sure (the situation here is more delicate). –  Emil Jeřábek Oct 29 '12 at 16:37
show 1 more comment