Consistency and consistency strength of certain special cuts in $I\Delta_0$ Recall that $I\Delta_0$ is the theory in the language of arithmetic that consists of the axioms of $\mathsf{PA}$ with induction restricted to $\Delta_0$ formulas (i.e., formulas where all quantifiers are bounded).
It is not too difficult to build a model $M$ of $I\Delta_0$ with a proper cut $N \subset M$ such that $M \equiv N$. Moreover, we can ensure that $2^n$ exists for every $n \in N$ and that $2^x$ is not a total function on $N$ (and therefore not a total function on $M$ either). It is also a standard fact that the set $\{ x \in M : (\exists y \in N) x < 2^y\}$ is a cut that models $I\Delta_0$ (this follows from the fact that it is downwards closed and closed under addition and multiplication). My question is about this last cut actually being all of $M$.
Let $C$ be a unary predicate symbol, and let $T$ be the theory in the language of arithmetic augmented with $C$ that contains $I\Delta_0$ and says that

*

*$C$ is downwards closed,


*$C$ is not all of the structure,


*$2^x$ is not a total function,


*$2^x$ is total on $C$,


*the induced structure on $C$ has the same theory as the full structure (in particular, it is a model of $I\Delta_0$), and


*for every $x$, there exists a $y \in C$ such that $x < 2^y$.
Obviously, the fifth bullet point must be stated as an axiom scheme.

Question 1. Is $T$ consistent?


Question 2. Does $I\Delta_0$ interpret $T$?


Question 3. Does $T$ interpret $I\Delta_0 + \mathrm{Exp}$ (where $\mathrm{Exp}$ is the statement that $2^x$ is a total function)?

Note that since $I\Delta_0$ does not interpret $I\Delta_0 + \mathrm{Exp}$, these last two questions cannot both have a positive answer.
 A: $T$ is inconsistent. The argument below is due to Robert Solovay (it is attributed to a letter from Solovay to Nelson in Visser’s Peano Basso and Peano Corto, see Lemma 3.7).
Let $2^x_n$ denote the iterated exponential function $2^x_0=x$, $2^x_{n+1}=2^{2^x_n}$. It is well known that the graph of $2^x_n$ has a well-behaved $\Delta_0$ definition in $I\Delta_0$.

Lemma (Solovay): $I\Delta_0+\neg\mathrm{Exp}$ proves that there exists a unique number $n$ such that $2^0_n$ exists, but $2^0_{n+1}$ does not.

Proof: Take $x$ such that $2^x$ does not exist, and let $n$ be maximal such that $2^0_n\le x$. Then $2^0_{n+1}$ either does not exist, or satisfies $2^0_{n+1}>x$, hence $2^0_{n+2}$ does not exist. Thus, $n$ or $n+1$ satisfies the conclusion of the Lemma. QED
Let us call the $n$ from the Lemma as Solovay’s number.
Now, observe that the axioms of $T$ imply that $C=\{x:2^x\text{ exists}\}$. Thus, working in $T$ (which includes $I\Delta_0+\neg\mathrm{Exp}$), if $n$ is Solovay’s number, then $n-1$ is Solovay’s number in $C$. In particular, the universe and $C$ disagree on the truth of the sentence “Solovay’s number is even”, contradicting the elementary equivalence axiom.
