Let $L\_{E}$ be the language of discretely ordered rings together with an extra predicate symbol $E$. The system $A$ consists of the axioms of $I\Delta\_{0}$ (basic arithmetic plus induction for bounded formulas) together with the statements:


(1) $E(0,1)$


(2) $\forall{x}\exists{y}E(x,y)$


(3) $\forall{x>0,y,z}E(x+1,y)\wedge E(x,z)\rightarrow y\geq 2z$


Is it then provable in $A$ that exponentiation (with base $2$) is total? (In any of the formulations as a bounded formula.)


This might be well-known, but I couldn't find a reference so far.



Is there exponentiation in "sufficiently large" models of $I\Delta_{0}$?
Do you intend system $A$ to include only $I\Delta\_0$, or actually $I\Delta\_0(E)$? That is, do you allow induction for formulas involving $E$?


If you do allow it, then then you can prove easily
$$\forall x,y\le w\,(E(x,y)\to x=y=0\lor\exists z\le y\,(z=2^x))$$
by induction on $w$, hence the theory proves exponentiation to be total.


If you only allow induction for $\Delta\_0$ formulas without $E$, then the answer is negative, and in fact, $A$ is a conservative extension of $I\Delta\_0$. This can be seen as follows: take any model $M\models I\Delta\_0$, we’ll expand it to a model of $A$. For $n\in\mathbb N$, put $E(n,2^n)$. For nonstandard $x,y\in M$, let $x\sim y$ iff $x-y\in\mathbb Z$. For any equivalence class $C$ of $\sim$, choose its representative $a$ so that $C=a+\mathbb Z$, and choose an arbitrary nonstandard $b\in M$. Then for any $n\in\mathbb N$, put $E(a+n,b2^n)$ and $E(a-n,\lfloor b/2^n\rfloor)$.


One can do even better: for example, let $A^+$ be the extension of $A$ by the following axioms:


(4) $E(x,y)\land E(x,y')\to y=y'$


(5) $E(x,y)\land E(x',y')\to E(x+x',yy')$


(6) $E(x,y)\land E(x',y')\land x< y\to x'< y'$


(this would be more readable if we had a unary function symbol instead of $E$). Then $A^+$ is still a conservative extension of $I\Delta\_0$. One way to prove this is as follows: take any countable recursively saturated model $M\models I\Delta\_0$, and let $L=\{a\in M:M\models\exists y\,(y=2^a)\}$. The countable structures $(M,+,\le)$ and $(L,+,\le)$ are elementarily equivalent (as they are both models of Presburger arithmetic), and the joint model $(M,L,+,\le)$ is recursively saturated, hence there exists an isomorphism $f\colon(M,+,\le)\simeq(L,+,\le)$. Then putting $E(x,2^{f(x)})$ defines a model of $A^+$.


In fact, one does not need $M$ to be recursively saturated for this argument to work: it is enough if $M$ has no cofinal set of the form $\{a^n:n\in\mathbb N\}$. Then $(M,+,{\le})$ is recursively saturated by [Cégielski, McAloon & Wilmers](https://doi.org/10.1016/S0049-237X(09)70503-8) (improved to models of $IE\_1$ by [Wilmers](https://doi.org/10.2307/2273790)), and then using the cofinality assumption, $(M,L,+,{\le})$ is recursively saturated using a variant of Theorem 5.3 in [this paper](https://arxiv.org/abs/2209.01197) of mine.


