Can one show that the real field is not interpretable in the complex field without the axiom of choice? We all know that the complex field structure $\langle\mathbb{C},+,\cdot,0,1\rangle$ is interpretable in the real field $\langle\mathbb{R},+,\cdot,0,1\rangle$, by encoding $a+bi$ with the real-number pair $(a,b)$. The corresponding complex field operations are expressible entirely within the real field.
Meanwhile, many mathematicians are surprised to learn that the converse is not true — we cannot define a copy of the real field inside the complex field. (Of course, the reals $\mathbb{R}$ are a subfield of $\mathbb{C}$, but this subfield is not a definable subset of $\mathbb{C}$, and the surprising fact is that there is no definable copy of $\mathbb{R}$ in $\mathbb{C}$.)  Model theorists often prove this using the core ideas of stability theory, but I made a blog post last year providing a comparatively accessible argument:

*

*The real numbers are not interpretable in the complex field.

The argument there makes use in part of the abundance of automorphisms of the complex field.
In a comment on that blog post, Ali Enayat pointed out that the argument therefore uses the axiom of choice, since one requires AC to get these automorphisms of the complex field. I pointed out in a reply comment that the conclusion can be made in ZF+DC, simply by going to a forcing extension, without adding reals, where the real numbers are well-orderable.
My question is whether one can eliminate all choice principles, getting it all the way down to ZF.
Question. Does ZF prove that the real field is not interpretable in the complex field?
I would find it incredible if the answer were negative, for then there would be a model of ZF in which the real number field was interpretable in its complex numbers.
 A: An interpretation of $(\mathbb R,+,\cdot)$ in $(\mathbb C,+,\cdot)$ in particular provides an interpretation of $\DeclareMathOperator\Th{Th}\Th(\mathbb R,+,\cdot)$ in $\Th(\mathbb C,+,\cdot)$. To see that the latter cannot exist in ZF:

*

*The completeness of the theory $\def\rcf{\mathrm{RCF}}\rcf$ of real-closed fields is an arithmetical ($\Pi_2$) statement, and provable in ZFC, hence provable in ZF. Its axioms are clearly true in $(\mathbb R,+,\cdot)$, hence $\Th(\mathbb R,+,\cdot)=\rcf$.


*Similarly, ZF proves completeness of the theory $\def\acfo{\mathrm{ACF_0}}\acfo$ of algebraically closed fields of characteristic $0$, hence $\Th(\mathbb C,+,\cdot)=\acfo$.


*The non-interpretability of $\rcf$ in $\acfo$ is again an arithmetical statement ($\Pi_2$, using the completeness of $\acfo$), hence its provability in ZFC automatically implies its provability in ZF.
Of course, common proofs of some or all the results above may already work directly in ZF (e.g., if you take syntactic proofs of completeness, or if you make it work using countable models, etc.). My point is that it is not necessary to check the proofs, as the results transfer from ZFC to ZF automatically due to their low complexity.
A: (1) $\mathbb{C}$ is stable, (2) $\mathbb{R}$ is unstable, and (3) stability is preserved under interpretations. Of course the usual development of stability uses a lot of choice, but (2) and (3) are elementary. (1) follows from QE for algebraically closed fields. One of the reasons why model theorists care about the whole alphabet soup of classification-theoretic properties is that they enable this kind of argument.
Furthermore we have a complete understanding of fields interpretable in $\mathbb{C}$: If $K$ is an algebraically closed field then any infinite field interpretable in $K$ is definably isomorphic to $K$. This is in Poizat's book on stable groups, but I forget who it is due to. I don't think this proof requires choice either.
Edit: I just read Joel's post more carefully and realized that it contains "Model theorists often prove this using the core ideas of stability theory". But I think it's still worth pointing out that this argument does not require choice.
Another edit: I thought about this a bit more today and I think that the following is the simplest argument I can think of. It uses ideas from stability, but no actual stability theory, just elementary model theory and algebra. Recall that a theory $T$ is $\omega$-stable if for any $M \models T$ and countable $A \subseteq M$, there are only countably many types in $M$ over $A$. It's easy to see that $\omega$-stability is preserved under interpretations - if $N$ is interpretable in $M$ then a witness of non-$\omega$-stability in $N$ lifts to one in $M$. It's also easy to see that a real closed field is not $\omega$-stable - there are uncountably many types over $\mathbb{Q}$. So it comes down to showing that algebraically closed fields are $\omega$-stable. Quantifier elimination for algebraically closed fields gives a bijection between $n$ types over $A \subseteq \mathbb{C}$ and prime ideals in $K [x_1,\ldots,x_n]$ where $K$ is the subfield generated by $A$, and every prime ideal in $K[x_1,\ldots,x_n]$ is finitely generated, so there are only countably many prime ideals.
Yet another edit: Emil pointed out that the argument above actually uses choice - in the proof of preservation of $\omega$-stability under interpretations. He suggests replacing $\omega$-stability with the following property: there are only countably many types over any finite set of parameters. When you do that you only need to make finitely many choices in the preservation argument.
Yet another another edit It turns out that this whole question had already been asked and answered on stack exchange. In particular Alex gave a worked out elementary version of the stability argument.
