Is there a first-order formula ϕ(x) with exactly one free variable $x$ in the language of fields together with the unary function symbol $\exp$ such that in the standard interpretation of this language in $\Bbb C$ (where $\exp$ is interpreted as the exponential function $x \mapsto e^x$), $ϕ(x)$ holds iff $x \in \Bbb R$?
My thoughts: If one takes the algebraic theory of the complex field without the exponential function, then $\Bbb R$ is not definable because there are isomorphisms of $\Bbb C$ mapping reals to non-real numbers. Does a similar approach work in this case? In particular, is there any other isomorphism of the exponential $\Bbb C$ structure besides the identity and complex conjugation?
This is a major open problem in model theory. Recent attempts to study ${\mathbb C}_{\exp}$ have been centred around Zilber's pseudo-exponentiation, which is a nice structure and module some (very serious) algebraic conjectures coincides with ${\mathbb C}_{\exp}$. Zilber's pseudo-exponential field is quasiminimal (i.e. every definable set is countable or co-countable) and hence $\mathbb R$ is not definable there. Have a look at Marker's paper for an introduction.