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](http://jdh.hamkins.org/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](http://jdh.hamkins.org/the-real-numbers-are-not-interpretable-in-the-complex-field/#comment-10799) 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](http://jdh.hamkins.org/the-real-numbers-are-not-interpretable-in-the-complex-field/#comment-11161) 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.



Can one show that the real field is not interpretable in the complex field without the axiom of choice?
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.


