Proof that a set of axioms axiomatizes the complex field along with the real numbers

Question

This is a follow-up to this question: What is an explicit axiomatization of the complex field along with the real numbers?. In that question, Noah Schweber gave a set of axioms for the theory of the structure $(\mathbb{C};+,-,*,0,1,R)$, where $R$ is a predicate that picks out the real numbers. Now, following his suggestion, I am asking for a fuller proof that those axioms generate the theory of that structure.

Answer 1

There are a couple ways to prove this. I'll use Ehrenfeucht-Fraisse games. For simplicity I'll use the "tuple versions" where players play finite tuples rather than individual elements; recall that the win condition for Duplicator is that the tuples built agree on all atomic formulas not involving nested function symbols. Additionally, I'll want the notion of a depth-$q$ winning strategy for Duplicator (this terminology is not standard); this is a strategy such that, in any play where it is followed, the resulting tuples of elements agree on all atomic formulas involving at most $q$ nested functions. A winning strategy for Duplicator in the usual sense is just a depth-$1$ winning strategy. It should be clear that Duplicator having a depth-$q$ winning strategy in $EF_n(\mathcal{X},\mathcal{Y})$ follows from their having a winning strategy in the usual sense in $EF_{n+q-1}(\mathcal{X},\mathcal{Y})$, so in particular if $\mathcal{X}\equiv\mathcal{Y}$ then we can find a depth-$q$ winning strategy for Duplicator in $EF_n(\mathcal{X},\mathcal{Y})$ for every $q,n$.

---

Suppose $$\mathcal{A}=(A; +_\mathcal{A},-_\mathcal{A}, \times_\mathcal{A},0_\mathcal{A}, 1_\mathcal{A}, R_\mathcal{A}), \quad\mathcal{B}=(B; +_\mathcal{B}, -_\mathcal{B}, \times_\mathcal{B}, 0_\mathcal{B}, 1_\mathcal{B}, R_\mathcal{B})$$ are models of the theory from my answer. I want to show that Duplicator has a winning strategy in the Ehrenfeucht-Fraisse game of length $n$ for each $n$. So fix some $n$. Additionally, fix some square roots of negative one $i_\mathcal{A},i_\mathcal{B}$ in the sense of $\mathcal{A},\mathcal{B}$ respectively; note that by the axioms I wrote down, every element $z$ of $\mathcal{A}$ can be uniquely represented as $x+_\mathcal{A}y\times_\mathcal{A}i_\mathcal{A}$ for $x,y\in R^\mathcal{A}$, and similarly for $\mathcal{B}$.

The "$R$-parts" of the two structures are elementarily equivalent by the completeness of $\mathsf{RCF}$, so I can pick some strategy $\Sigma$ which is depth-$2$ winning for Duplicator in $EF_n(R^\mathcal{A},R^\mathcal{B})$. The need for depth-$2$ winning will become clear at the end of the argument; for now, just think of $\Sigma$ as being "as good as needed."

Now the strategy $\Sigma$ translates to a strategy $\hat{\Sigma}$ for Duplicator in $EF_n(\mathcal{A},\mathcal{B})$ itself via a kind of "simulation." We start by translating between tuples in $\mathcal{A}/\mathcal{B}$ and tuples in $R^\mathcal{A}/R^\mathcal{B}$. There are two directions to this:

• Each tuple $t$ of elements of $\mathcal{A}$ of length $k$ has a corresponding tuple $\overline{t}$ of elements of $R^\mathcal{A}$ of length $2k$ by replacing each term $x+_\mathcal{A}yi_\mathcal{A}$ with the tuple $(x,y)$ and then concatenating everything; and similarly for $\mathcal{B}$. Note that this operation is well-defined per the "unique representation" point above.

• The above map is injective, and so given a $2k$-tuple $t$ of elements of $R^\mathcal{A}$ we let $\underline{t}$ be the unique $k$-tuple of elements of $\mathcal{A}$ satisfying $\overline{(\underline{t})}=t$.

Here's how these tuple translations let us build a strategy $\hat{\Sigma}$ for Duplicator in $EF_n(\mathcal{A},\mathcal{B})$. Duplicator will look at the play so far, apply the $\overline{\cdot}$-transformation to all tuples involved to get an imagined play in $EF_n(R^\mathcal{A},R^\mathcal{B})$, and now ask $\Sigma$ what it would do in this situation. $\Sigma$ responds with some length-$2n$ tuple $s$; now in the actual game, Duplicator will play $\underline{s}$.

We want to check that a possible loss for Duplicator in the actual game if they follow this strategy would correspond to a possible loss for Duplicator in $EF_n(R^\mathcal{A},R^\mathcal{B})$ where they followed $\Sigma$, which by assumption on $\Sigma$ can't happen. The key is to show that inequalities in the "big" structures $\mathcal{A},\mathcal{B}$ are reflected by inequalities in the "small" structures $R^\mathcal{A},R^\mathcal{B}$; the loss condition for Duplicator in an EF-game corresponding to one of a set of equalities failing, this will give the desired result.

Suppose we have a play $\pi$ of $EF_n(\mathcal{A},\mathcal{B})$ in which Duplicator plays as above. Let $t=(a_l)_{1\le l\le k}$, $s=(b_l)_{1\le l\le k}$ be the tuples of elements of $\mathcal{A}$,$\mathcal{B}$ built during this play, and let $\overline{t}=(c_l)_{1\le l\le 2k}, \overline{s}=(d_l)_{1\le l\le 2k}$ be the corresponding tuples of elements of $R^\mathcal{A},R^\mathcal{B}$ built in the "simulated play" $\pi'$ of $EF_n(R^\mathcal{A},R^\mathcal{B})$ in which Duplicator played according to $\Sigma$. To show that Duplicator wins in $\pi$ we need to show:

• For each constant symbol $v$ in our language and each $j$, we have $a_j=v$ in $\mathcal{A}$ iff $b_j=v$ in $\mathcal{B}$.

• For each $m$-ary function symbol $f$ in our language and each $l_1,...,l_m, j$, we have $f(a_{l_1},...,a_{l_m})=a_j$ in $\mathcal{A}$ iff $f(b_{l_1},...,b_{l_m})=b_j$ in $\mathcal{B}$.

• For each $m$-ary relation symbol $U$ in our language $l_1,...,l_m$, we have $U(a_{l_1},...,a_{l_m})$ in $\mathcal{A}$ iff $U(b_{l_1},...,b_{l_m})$ in $\mathcal{B}$.

I'll give one of the nontrivial cases (with some abbreviation for brevity), and leave the rest as an exercise.

Suppose $a_1 a_2=a_3$. We can "reflect this down" to a relationship between $c_1,c_2,c_3,c_4,c_5,c_6$ in $R^\mathcal{A}$: specifically, we have $$c_1c_3-c_2c_4=c_5\quad\mbox{and}\quad c_1c_4+c_2c_3=c_6$$ in $R^\mathcal{A}$. Now since in $\pi'$ Duplicator played according to $\Sigma$, these equations must hold "on the $R^\mathcal{B}$-side" as well: that is, we have $$d_1d_3-d_2d_4=d_5\quad\mbox{and}\quad d_1d_4+d_2d_3=d_6$$ in $R^\mathcal{B}$. But now we "pull up to $\mathcal{B}$" and get $b_1b_2=b_3$ as desired. Note that we need to involve a high-complexity term here; this is why we wanted $\Sigma$ to be a more-than-standardly-winning strategy (and since this is in fact the most complicated that things get, it's clear that $\Sigma$ just needs to be depth-$2$ winning).

---

Note that all we really used is that $\mathbb{C}$ is "built straightforwardly" from $\mathbb{R}$; this provided the necessary transformation of EF-strategies. My above-cited answer stated a very general result codifying this; the proof is basically the same as the above argument, so I'll leave it as an exercise.