Return to Revisions

No. First, let $T'=T+\forall x>0\\,\exists y\\,(xy=1)$, so that $T'$ is the first-order theory of archimedean ordered fields. Let $\phi(x)$ be a formula defining $\mathbb Z$ in $\mathbb Q$, and let $\psi$ be the sentence “$\phi(x)$ defines a discretely ordered ring”. Since the only DOR embeddable in an archimedean field are the integers, $\phi(x)$ provides an interpretation of true arithmetic in the theory $T'+\psi$. Thus, $T'+\psi$ is not recursively enumerable, and a fortiori $T$ is not recursively enumerable either. (In fact, $T$ is not even arithmetical.)