Does ZF prove that the real number field is not interpretable in the complex number field? I recently saw a proof that the real number field is not interpretable in the complex number field. But this required the axiom of choice, namely the existence of wild automorphisms of the complex numbers. Is there a way to prove it in ZF alone?
 A: In the comments, I mentioned the following argument that $\mathbb{R}$ is not interpretable in $\mathbb{C}$: $\mathbb{C}$ is stable,  $\mathbb{R}$ is unstable, and stability is preserved under interpretations.
The word "stable" may look a bit scary here - indeed, stability theory is a rather technical subject - but the argument above actually doesn't need any complicated ideas from stability theory. It just boils down to this: the order on the real field is definable, but no infinite linear order is interpretable in the complex field. 
I'm taking your question as a challenge to produce as elementary a proof of this as possible, in particular without using the word "stable" and without using any choice. For those in the know, I'm trading in the order property (a theory is stable if it does not have the order property) for the strict order property, to make the argument a bit more transparent. 
Suppose for contradiction that the real field $\mathbb{R}$ is interpretable in the complex field $\mathbb{C}$. 


*

*First, note that the standard order $x \leq y$ on $\mathbb{R}$ is definable by the formula $\varphi(x,y): \exists z\, (x+ z^2 = y)$. 

*Since the complex field interprets the real field, and the real field interprets the real order, we can compose these interpretations to conclude that the complex field interprets the real order. More precisely: As part of the data of the given interpretation, we have a definable set $X\subseteq \mathbb{C}^n$ and a surjective map $\pi\colon X\to \mathbb{R}$. Each real number $r\in \mathbb{R}$ is represented by an equivalence class $X_r = \pi^{-1}(\{r\})$ for a definable equivalence relation on $X$. Pulling back the formula $\varphi$ to $\mathbb{C}$, there is a formula $\psi(x,y)$ (where now $x$ and $y$ are tuples of length $n$) such that for all $a\in X_r$ and $b\in X_s$, $\mathbb{C}\models \psi(a,b)$ if and only if $r\leq s$. 

*In particular, if we write $Y_b$ for the subset of $X$ defined by $\psi(x,b)$, then $(Y_b)_{b\in X}$ is a family of definable sets which is linearly preordered by $\subseteq$, and such that the quotient linear order is isomorphic to the standard order on $\mathbb{R}$. To get a contradiction, we would like to show that the complex field does not admit any such family of definable sets. 

*To understand the definable sets in $\mathbb{C}$, we use quantifier elimination. Now the easiest proofs of quantifier elimination for the complex field use the compactness theorem, which might get you worried that we're using choice. But don't worry: quantifier elimination for $\mathbb{C}$ can be proven constructively. 
Now there are probably many ways to see that the complex field does not admit any quantifier-free definable family of definable sets which is linearly preordered by $\subseteq$ with the order type of $\mathbb{R}$. Here's the most elementary way that occurred to me - remember, I'm trying to avoid appealing to any more advanced results in algebraic geometry or model theory.  


*First, let's assume $X\subseteq \mathbb{C}^1$, i.e. $x$ is a single variable, not a tuple of variables. Let $\psi(x,y)$ be the formula defining the family of definable sets. By quantifier elimination, we may assume $\psi$ is quantifier-free. Then for any $b$, $\psi(x,b)$ is equivalent to a Boolean combination of polynomial equations $p(x) = 0$ and inequations $p(x)\neq 0$, with each $p\in \mathbb{C}[x]$. When $p\neq 0$, the formula $p(x) = 0$ defines a finite set of size at most $\deg(p)$, and $p(x)\neq 0$ defines a cofinite set whose complement has size at most $\deg(p)$, so letting $N$ be the sum of the degrees (in $x$) of all the polynomials involved in $\psi(x,y)$, we have that $\psi(x,b)$ defines a finite set of size at most $N$ or a cofinite set whose complement has size at most $N$. Hence, a $\subseteq$-chain of definable sets defined by instances of $\psi$ can have length at most $2N+2$, and in particular every such chain has a $\subseteq$-minimal element. 

*Now let's prove by induction on $n$, where $n$ is the length of the tuple of variables $x$, that for any formula $\psi(x,y)$, there is no family $(X_b)_{b\in Y}$ of definable sets defined by $\psi$ which is linearly preordered by $\subseteq$ and has no minimal element. We've established the base case $n = 1$. So let $x = (x_1,\dots,x_n,x_{n+1})$. Let's write $b\leq b'$ when $X_b\subseteq X_{b'}$, and note that this relation is definable (by $\forall x\, (\psi(x,b)\rightarrow \psi(x,b'))$). For any $b$ and any $a\in \mathbb{C}^n$, we can look at the set $Z_{a,b}$ defined by $\psi(a,x_{n+1},b)$. Since $Z_{a,b}\subseteq \mathbb{C}^1$ is the fiber over $a$ of $X_b$, we have $Z_{a,b}\subseteq Z_{a,b'}$ whenever $b\leq b'$. For fixed $a$, since $(Z_{a,b})_{b\in Y}$ is a definable family of subsets of  $\mathbb{C}^1$, it has a $\subseteq$-least element, i.e. $Z_{a,b}$ is constant for a downwards-closed set of $b$s. Let's call this downwards-closed set $Y_a$. We can use this observation to definably linearly preorder the $n$-tuples $a$: $a \leq a'$ if $Y_a \subseteq Y_{a'}$. Applying induction to the family of downwards-closed sets in this order, by induction the order has a minimal element $a^*$. But now for any $b\in Y_{a^*}$, I claim that $X_b$ is minimal in the original family of sets. Indeed, if $b'$ such that that $X_{b'}\subsetneq X_b$, then there is some $a$ such that $Z_{a,b'}\subsetneq Z_{a,b}$. But then $b\notin Y_a$, so $Y_a\subsetneq Y_{a^*}$, contradicting minimality of $a^*$. 
A: Here's a rather silly computability-based argument:
Suppose $\Phi$ were an interpretation of $\mathbb{R}$ in $\mathbb{C}$. Fix a non-arithmetical real $r\in\mathbb{R}$ and some $a_1,...,a_k\in\mathbb{C}$ such that $\Phi(a_1,...,a_k)=r$; let $F=\overline{\mathbb{Q}(a_1,...,a_k)}$.
By standard considerations we have $F\preccurlyeq\mathbb{C}$ and so $\Phi^F$ is (isomorphic to) a real closed subfield of $\mathbb{R}$ containing $r$. But $F$ has a computable copy (since every countable algebraically closed field has a computable copy), so $\Phi^F$ must have an arithmetic copy since it's interpretable in $F$. But $r$ is computable in any copy of $\Phi^F$, and $r$ is not arithmetical, so we're done.

We've used some basic model- and computability-theory here for which choice is clearly irrelevant. The choicily-nontrivial point was that every finite tuple of complex numbers is contained in some countable elementary substructure of $\mathbb{C}$. Since choice fails this need not be generally true (consider an infinite Dedekind-finite linear order), but for $\mathbb{C}$ specifically we're saved by the explicitness of the algebraic closure operation, but in general this can be an issue.

And to round the picture out, here's a set-theoretic proof of a stronger result: that $\mathbb{R}$ is not $\mathcal{L}_{\infty,\omega}$-interpretable in $\mathbb{C}$. This is based on the same combinatorial intuition, that $\mathbb{R}$ has lots of information coded into its elements while $\mathbb{C}$ doesn't.
The key point is that $\mathsf{ZF}$ proves that there is exactly one structure up to isomorphism which is $\mathcal{L}_{\infty,\omega}$-equivalent to $\mathbb{C}$, namely the algebraically closed field of characteristic zero and transcendence degree $\aleph_0$ which I'll call $F^0_{\aleph_0}$. This isn't hard to prove. Clearly it's the only candidate since we can rule out finite transcendence dimension in $\mathcal{L}_{\infty,\omega}$, so we just need to show $F^0_{\aleph_0}\equiv_{\infty,\omega}\mathbb{C}$. We can prove this by a messy explicit argument, or the more general result that potentially isomorphic structures are $\mathcal{L}_{\infty,\omega}$-equivalent.


*

*Actually, the real subtlty here is around the right definition of $\models_{\infty,\omega}$ in the absence of choice (and really this was already an issue with FOL). The right definition is the existence of a family of multivalued Skolem functions, or of an appropriate subtree of the syntax tree for the sentence in the structure in question, or something morally equivalent. Once we explicitly write out the correct choiceless definition of $\models_{\infty,\omega}$, though, the above result about potential isomorphisms becomes basically trivial.


Any $\mathcal{L}_{\infty,\omega}$-interpretation $\Phi$ of $\mathcal{A}$ in $\mathbb{C}$ therefore yields an $\mathcal{L}_{\infty,\omega}$-interpretation in $F^0_{\aleph_0}$ of some necessarily countable structure $\mathcal{A}'\equiv_{\infty,\omega}\mathcal{A}$. But it's easy to prove that there is no countable structure which is $\equiv_{\infty,\omega}\mathbb{R}$, basically for the same reason that the computability-theoretic argument above worked: for each real $r$ there is an $\mathcal{L}_{\infty,\omega}$-sentence $\psi_r$ asserting that $r$'s Dedekind cut is filled.
(Meanwhile, note that if $\mathbb{C}$ has no automorphisms other than the identity and conjugation then $\mathbb{R}$ is interpretable in $\mathbb{C}$ via second-order logic: this is because we can define the real part of $z$ as "one-half of the sum of the two (possibly equal) images of $z$ under automorphisms of the universe," and the set of numbers which are their own real parts is just $\mathbb{R}$. This is ruled out if $\mathsf{AC}$ holds, of course.)
