MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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.

share|cite|improve this question
up vote 12 down vote accepted

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^+$. ${}{}$

share|cite|improve this answer
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. – M Carl Apr 23 '12 at 13:30
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. – Emil Jeřábek Apr 24 '12 at 9:30

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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