Do the strongest theories currently known to be unconstrained by Tennenbaum's theorem ($IOpen$ and some modest extensions) remain so when augmented with a definition of exponentiation and axiom $\mathrm{exp}$ stating that it is finite?
As a bonus, can such theories prove some of the core theorems of mathematical logic which typically use exponentiation to encode strings of integers as integers?
Motivation
On the one hand, there is the Reverse Mathematics program, which seeks the weakest natural theories needed to prove theorems of everyday mathematics (which can depend on how these theorems are formulated). Harvey Friedman's "grand conjecture" is that arithmetic results such as Fermat's last theorem can be proven in $I\Delta_0 + \mathrm{exp}$, while Feng Ye in Strict Finitism and the Logic of Mathematical Applications has shown that a theory of essentially the same strength is sufficient for much of the mathematics used in applications to the physical sciences.
The bar is still being pushed lower: Dmytro Taranovsky's Arithmetic with Limited Exponentiation, based on Fernando Ferreira's fesible analysis, argues that for many purposes even exponentiation need not be treated as a total operation, with instead a finite number of types of "integers", each nested within the next, and exponentiation raising the type by 1. The resulting theories can be interpreted in $I\Delta_0$, or even (less directly) within Robinson arithmetic, making them acceptable even to some ultrafinitists.
On the other hand, there is a somewhat related (informal) program to seek the limits of Tennenbaum's theorem, which says that even quite weak theories have no computable nonstandard models. This is known to be true for $I\Delta_0$ and even for the much weaker $IE_1$, but false for $IOpen$ or some modest extensions of it.
The usefulness of such weak theories for everyday mathematics could perhaps be described as "unsettled". For example, Joel Hamkins in this answer points out that the very weakest theories, which are known not to be constrained by Tennenbaum's theorem, are too weak to prove even basic facts about arithmetic and so most of their computable models are quite pathological; he suggests that the theorem may kick in too low to avoid this.
However, some of the aforementioned extensions of $IOpen$, while avoiding Tennenbaum's theorem, do at least enforce some of these basic number-theoretic properties, and so their computable nonstandard models could in some weak sense be thought of as "alternative universes" for doing mathematics. It then seems interesting to ask just how much mathematics one could get away with doing in them.
(I imagine there are also corresponding subsystems of second-order arithmetic, but asking about those would probably make the scope of this question too broad.)
