Let $T_R$ be the first-order theory of real closed fields. This is precisely the theory over the language $\{0,1,+,\times\}$ such that the theorems are the formulas that hold in $\Bbb R$. It can be effectively axiomatized by saying that it's a field in which every odd-degree polynomial has a root, and that for all $r$ either $r$ or $-r$ has a square root, but that $-1$ is not a square.

Define $T_C$ to be the analogous theory for $\Bbb C$, but where we include complex conjugation in the language. So it's precisely the first-order theory over the language $\{0,1,+,\times,\bar{}\}$ such that a formula is a theorem if and only if it holds in $\Bbb C$. This can be axiomatized by saying that it's an algebraically closed field in which $z\mapsto\bar z$ is a self-inverse automorphism and $z\bar z=-1$ has no solutions.

Then these two theories can interpret each other. The theory $T_R$ is interpretable in $T_C$ by considering the fixed points of $z\mapsto\bar{z}$. In the other direction, and $T_C$ is interpretable in $T_R$ by equipping pairs $(r_0,r_1)$ with operations to make them act like $r_0 + r_1i$.

I'm interested in whether this pair of interpretations rises to the level of biinterpretation, as defined by Joel David Hamkins here. This definition requires that when we compose the two interpretations above (to get interpretations of $T_R$ and $T_C$ in themselves) these composite interpretations are isomorphic to the identity representations, in a way that is definable and provable within the theories themselves.

At first it seemed to me that this would be true, since applying the two interpretations to a model does indeed yield the original model. And Hamkins himself seemingly calls this a biinterpretation here.

What has me doubting is that the nLab says here that biinterpretations of theories induce equivalences between the categories of models. That can't be true here, since the above interpretations send $\Bbb R$ and $\Bbb C$ to each other, and yet $\Bbb R$ has only the trivial automorphism, whereas $\Bbb C$ also has complex conjugation. An equivalence of categories should preserve automorphism groups.

So is this a biinterpretation or not?

I also asked this question over on the category theory Zulip. The answers weren't conclusive, but they lead me to believe the subtlety lies in the interpretation of $T_C$ in itself. If we adjoin a square root of $-1$ to the fixed points of $z\mapsto\bar{z}$ then we would want to define an isomorphism back to the original field by sending this fixed point to $i$. But how do we define $i$ separately from $-i$?

Is this indeed the problem, and is it unavoidable? Does it also prevent $\Bbb R$ and $\Bbb C$ from being biinterpretable as models?

3more comments