Is the order arithmetic of the positive reals o-minimal?

Yes. To see this, first note that we can interpret the positive reals in $(\mathbb{R},0,1,+,-,\times)$ as squares of non-zero real numbers. We can by induction on complexity of formulas define a translation map from formulas in the language of the positive reals to formulas in the language of the reals as follows:

  • For an atomic formula $\phi(x_1,\dots x_k)$ by its translation is $T(\phi)(y_1, \dots, y_k) = \phi(y_1^2, \dots , y_k^2)$

  • $T(\phi \wedge \psi) = T(\phi) \wedge T(\psi)$

  • $T(\neg \phi) = \neg T(\phi)$

  • $T(\exists x \phi(x)) = \exists y (y \neq 0 \wedge T(\phi)(y^2))$

Then the postive reals model $\phi(c)$ for $c > 0$ if and only the reals models $T(\phi)(\sqrt{c})$, for formulas with a single free variable of arbitrary complexity.

But then using o-minimality of the reals, we know $\{y : T(\phi)(y)\}$ is a finite union of points and intervals, so the same is true of $\{c : \phi(c)\} = \{c : T(\phi)(\sqrt{c})\}$


Another way to see o-minimality is to note that $log$ induces an isomorphism $$log : ((0,\infty), 1, +, \times, >) \cong (\mathbb R, 0, \oplus, +, >),$$ where $\oplus$ is the binary operation defined by $\oplus(x,y) = \log(e^x + e^y)$. But $\oplus$ is definable in $\mathbb R_{exp}$. Hence the latter structure is a reduct of $\mathbb R_{exp}$ and therefore is o-minimal.