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.

  • 2
    $\begingroup$ Obvious means: $'$ is successor $x'=x+1$ and $\text{exp}(x)=2^x$? $\endgroup$ – Joel David Hamkins Jul 26 '18 at 23:15
  • 5
    $\begingroup$ 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$. $\endgroup$ – Andreas Blass Jul 26 '18 at 23:54
  • 2
    $\begingroup$ (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. $\endgroup$ – Emil Jeřábek Jul 27 '18 at 6:19
  • 1
    $\begingroup$ Sorry, one more schema: $0^{(k)}<x<y\to\exp(x)^{(k)}<\exp(y)$. $\endgroup$ – Emil Jeřábek Jul 27 '18 at 6:27
  • 1
    $\begingroup$ Joel: Thanks for the suggestion! Edited. $\endgroup$ – 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.


  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.

| cite | improve this 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}$.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.