Is there a finite or at least recursive axiomatization for the theory of the rational ordered field? Consider the structure $(\mathbb{Q},+,-,*,0,1,<)$ What is an axiomatization for the complete theory of that structure? Is there a finite or at worst recursive axiomatization for the complete theory of that structure?
 A: Perhaps surprisingly, $\mathbb{Z}$ is first-order definable in the ring of rationals! So the latter's theory is exactly as complicated as the former's (interpreting $\mathbb{Q}$ in $\mathbb{Z}$ is an easy exercise), hence not recursively axiomatizable.
The definition of $\mathbb{Z}$ in $\mathbb{Q}$ is however quite complicated; it is open whether the Diophantine theory of $\mathbb{Q}$ is decidable ("Hilbert's $10$th problem for $\mathbb{Q}$"). See this survey of Poonen for general aspects of Diophantine complexity.

That said, we can give a snappy axiomatization of $\mathbb{Q}$ relative to $Th(\mathbb{Z})$.
Let $\zeta(x)$ be a formula defining $\mathbb{Z}$ in $\mathbb{Q}$. Then $Th(\mathbb{Q})$ is axiomatized by:

*

*$Th(\mathbb{Z})^\zeta$, the relativization of each sentence in $Th(\mathbb{Z})$ to $\zeta$.


*The usual ordered field axioms.


*The "generation" axiom that every $x$ is of the form $y\over z$ for some $y,z\in\mathbb{Z}$.
It's not actually quite trivial that the conjunction $T$ of the above sentences axiomatizes $Th(\mathbb{Q})$; while given $M,N\models T$ we have $\zeta^M\equiv\zeta^N$, we still need to check that we don't get any first-order differences when we look beyond their "$\zeta$-parts." In general, two structures "generated" in the same way by elementarily equivalent substructures will themselves be elementarily equivalent; this can be proved by EF-games.
