Models of arithmetic in a signature with exponentiation but not addition and multiplication Let $\mathcal{L}_{\mathrm{exp}}$ be the language with signature $(0, ^\prime, <, \mathrm{exp})$ (with $0$ interpreted as zero, $^\prime$ as successor, and $\mathrm{exp}(x)$ as $2^x$) and let $\mathsf{TA}_{\mathrm{exp}}$ be true arithmetic in this signature; i.e. $\{ \phi \in \mathsf{Sent}(\mathcal{L}_{\mathrm{exp}}): \mathbb{N} \vDash \phi \}$.  
What is known about the models of $\mathsf{TA}_{\mathrm{exp}}$? Does the analogue of Tennenbaum's theorem hold? I've loooked around a bit, but haven't been able to find anything; pointers to the literature would be greatly appreciated.  
 A: $\mathsf{TA}_{\exp}$ does have recursive nonstandard models. In fact, even the considerably stronger theory $\mathrm{Th}(\mathbb N,+,2^x)$ (Presburger arithmetic with exponentiation) has recursive nonstandard models. This follows from results of Semënov, elaborated in this paper by Point: the theory is decidable (with an explicitly given axiom set), and it has elimination of quantifiers in a language expanded with $<$, congruence predicates, and the logarithm function $\ell(x)=\lfloor\log_2(x)\rfloor$.
It is a general fact that any decidable theory has a recursive model, and even a model with decidable satisfaction predicate. Now here we have the minor problem that this construction may happen to produce the standard recursive model; thus, we apply it to the theory expanded with a new constant $c$, along with axioms making $c$ nonstandard. We need to make sure the theory is still decidable, and one way to do that is to use the quantifier elimination result to exhibit a recursively axiomatized complete type. I didn’t check this in detail, but I believe it is possible.
Alternatively, one may do something similar directly for the theory of $\mathsf{TA}_{\exp}=\mathrm{Th}(\mathbb N,<,2^x)$. I did verify the details, but unfortunately, the full proof is too long to present here, so I will only state the results with a few hints.

Theorem:

*

*$\mathrm{Th}(\mathbb N,0,{}',<,2^x)$ is decidable, and it can be explicitly axiomatized by
a. the axioms of a discrete linear order with a least element and no largest element;
b. the axioms $x<\exp(x)$, $x<y\to\exp(x)<\exp(y)$, and $\forall x>0\,\exists y\,(\exp(y)\le x<\exp(y'))$;
c. the axioms $\exp(\overline k)=\overline{2^k}$ and $\overline k<x\to\exp(x)+k<\exp(x')$ for all $k\in\mathbb N$, where $x+0:=x$, $x+(k+1):=(x+k)'$, and $\overline k:=0+k$.


*The theory has quantifier elimination in the language $L_\ell=(0,{}',x\mathbin{\dot{\smash-}}1,<,\ell)$ (note: $\exp$ not needed).


*Every formula in one variable is equivalent to a Boolean combination of formulas of the form $x=\overline k$ and $P(\ell(\dots(\ell(x))\dots)+k)$ (possibly with negative $k$, defined in the obvious way), where $P(x)$ denotes $x=\exp(\ell(x))$ (i.e., “$x$ is a power of $2$”).

The proof is syntactic: one first proves that any quantifier-free formula of $L_{\ell,\exp}:=L_\ell\cup\{\exp\}$ is equivalent to a quantifier-free formula of $L_\ell$ of a suitable form, and that such a quantifier-free formula in one variable is equivalent to one of the form 3. Using this, we show that any $L_{\ell,\exp}$-formula with one quantifier is equivalent to a quantifier-free formula.
We can then produce a recursive nonstandard model by the general result above. In particular, the quantifier elimination result implies that the theory expanded with a new constant $c$ with the sequence of axioms $P(\ell(\dots(\ell(c))\dots))$ is complete, hence decidable, hence it has a recursive model.
Note that the theory is universally axiomatizable in $L_{\ell,\exp}$, hence any $L_{\ell,\exp}$-submodel of a model of the theory is elementary. Thus, we may take the model generated by $c$, which can be explicitly described by giving a normal form for terms in one variable, and I believe it is equivalent to the model given in Matt F.’s current answer.
A: A third try, with thanks to Emil Jerabek for correcting the previous two:
The following $\mathcal{M}=(S,0,',<,\exp)$ is a recursive non-standard model for the language, and I conjecture that it is a model for the theory:
The sequence $(a,b,c;k)$ is intended to represent
\begin{align}
&a + \exp(b+\exp(c+\omega) &\text{ if }k=0 \\
&a + \exp(b+\exp(c+\exp\cdots\exp\omega) &\text{ if }k>0 \\
&a + \exp(b+\exp(c+\log\cdots\log\omega) &\text{ if }k<0
\end{align}
with $|k|$ operations of $\exp$ or $\log$ on a non-standard $\omega$.
Formally, let $S$ be the union of $\mathbf{N}$ and
$$\{(z_1,\ldots,z_n;k)\}\ /\ ((z_1,\ldots,z_n;k) \sim (z_1,\ldots,z_n,0;k-1))$$
where $z_i,n,k\in \mathbf{Z}$ and $n>1$.  Note that $n+k$ is well-defined, and given any sequence, we can choose a representative of its equivalence class which has arbitrarily high $n$ and low $k$.
Let the $0$ for $S$ be the usual $0$ in $\mathbf{N}$.  Let $'$ and $\exp$ be defined in the standard way on $\mathbf{N}$, and by
$$(z_1,\ldots,z_n;k)'=(z_1+1,z_2,\ldots,z_n;k),$$
$$\exp(z_1,\ldots,z_n;k)=(0,z_1,z_2,\ldots,z_n;k).$$
Let $<$ be defined such that $\mathbf{N}$ is less than all the sequences, with the standard order on $\mathbf{N}$ and $x<x'$ iff $x$ and $x'$ have representatives 
$$x = (z_1,\ldots,z_n;k),\,\ x'=(z'_1,\ldots,z'_{n'};k')$$
with either $n+k <n'+k'$, or $n=n'$, $k=k'$ and $z_j<z'_j$ for the last $j$ where $z$ and $z'$ differ.
Now define $\lfloor \log(x) \rfloor$ for $x=(z_1,\ldots,z_n;k)$, $n \ge 3$, by
$$y=
\begin{cases}
(\phantom{-1+}z_2,z_3,\ldots,z_n;k) \text{ if } \ z_1 \ge 0\\
(-1+z_2,z_3,\ldots,z_n;k) \text{ if } \ z_1 < 0\\
\end{cases}
$$
and this satisfies $\exp(y) \le x < \exp(y')$.
I'm interested in any suggestions of sentences in $Th(\mathbf{N},0,',<,\exp)$ which might not be true in $\mathcal{M}$.
