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.


1 Answer 1


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 (improved to models of $IE_1$ by Wilmers), and then using the cofinality assumption, $(M,L,+,{\le})$ is recursively saturated using a variant of Theorem 5.3 in this paper of mine.

  • $\begingroup$ Thanks for your answer. I was interested in the second variant, and after your first answer, I noticed that I should have added (5) in the original statement, so this extension is really interesting. $\endgroup$
    – M Carl
    Apr 23, 2012 at 13:30
  • $\begingroup$ I realized the argument does not really give the axiom (7) $E(x,y)\to x< y$. While I am confident that the zig-zag construction of the isomorphism $f$ can be modified to yield $f(x)>\lfloor\log_2x\rfloor$ which guarantees (7), the proof gets messy, so I just deleted the axiom from the answer. $\endgroup$ Apr 24, 2012 at 9:30
  • 1
    $\begingroup$ The argument in Theorem 6.4 of arxiv.org/abs/2209.01197 does, in fact, give the axiom $E(x,y)\to x<y$. $\endgroup$ Sep 5, 2022 at 8:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.