Models of arithmetic in a signature with exponentiation but not addition and multiplication

Question

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.

Answer 1

$\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:

1. $\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$.

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

3. 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.

Answer 2

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}$.