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

• Obvious means: $'$ is successor $x'=x+1$ and $\text{exp}(x)=2^x$? – Joel David Hamkins Jul 26 '18 at 23:15
• If exp were a binary function, $\exp(x,y)=x^y$, then you could define multiplication because $yz=w$ iff $\forall x(\exp(\exp(x,y),z))=\exp(x,w))$. Then you could define addition because $y+z=w$ iff $\forall x(\exp(x,y)\exp(x,z)=\exp(x,w))$. I therefore agree with @JoelDavidHamkins that exp had better be unary with a fixed base, presumably $2$. – Andreas Blass Jul 26 '18 at 23:54
• (Note that $0$ and $'$ are definable from $<$.) Conjecture: the theory is completely axiomatized by axioms of discrete linear order with least element, $x<y\to\exp(x)<\exp(y)$, $\exp(0^{(k)})=0^{(2^k)}$ and $0^{(k)}<x\to x^{(k)}<\exp(x)$ for all standard $k\in\mathbb N$. If true, this would imply the theory has plenty of recursive nonstandard models. – Emil Jeřábek Jul 27 '18 at 6:19
• Sorry, one more schema: $0^{(k)}<x<y\to\exp(x)^{(k)}<\exp(y)$. – Emil Jeřábek Jul 27 '18 at 6:27
• Joel: Thanks for the suggestion! Edited. – Beau Madison Mount Jul 29 '18 at 21:57

$$\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, and $$\forall x>0\,\exists y\,(\exp(y)\le x<\exp(y'))$$;

c. the axioms $$\exp(\overline k)=\overline{2^k}$$ and $$\overline k 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.

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