According to Marker's "Model Theory: An Introduction", the real exponential field has a $\forall\exists$ axiomatization (because it is model complete) but no-one has any idea what such an axiomatization might look like. Has any progress been made on this since the early 2000s when Marker wrote this?
1 Answer
$\begingroup$
$\endgroup$
In her PhD thesis ``On the First Order Theory of Real Exponentiation'', Tamara Servi, has given a recursive subtheory $T$ of $T_{exp}$ and has shown that if Schanuel's conjecture holds, then $T$ is complete and hence provides a recursive axiomatization of $T_{exp}$. There are some related results.
See section 4.7 of the above mentioned paper.