What is an explicit axiomatization of the complex field along with the real numbers?

Question

Consider the structure $(\mathbb{C};+,-,*,0,1,R)$ where $R$ is a predicate that picks out the real numbers. I would be very interested in an explicit axiomatization of the complete theory of that structure. There probably isn't a finite axiomatization of it, but I would be interested in some recursive axiomatization of it, if one exists. I think what you need is the axioms for algebraically closed fields, plus some more axioms. I would be interested in what these "more axioms" are.

Answer 1

Rather than thinking about this as "$\mathbb{C}$ but more," we should really just think of it as "$\mathbb{R}$ with more made explicit:" the complex numbers are interpretable in the reals via the usual construction of complex numbers as ordered pairs of reals. So all we have to do is $(i)$ write down axioms saying that the $R$-part of our structure is $\mathbb{R}$-like (= the real closed field axioms) and $(ii)$ make sure that the usual interpretation of $\mathbb{C}$ in $\mathbb{R}$, applied to the $R$-part of our structure, gives the whole structure itself

This amounts, ultimately, to the following axioms (thanks to Alex Kruckman for improving this):

• The field axioms for the whole structure.

• The real closed field axioms for the $R$-part.

• An axiom saying that in the whole structure there is a square root of $-1$.

• An axiom saying that, if $i$ is a square root of $-1$, then every $z$ can be written uniquely in the form $a+bi$ for $a,b$ in the $R$-part.

This is a computable axiomatization, but not a finite one due to the role of real closedness. And indeed no finite axiomatization exists, since $Th(\mathbb{R};+,*,0,1)$ itself is not finitely axiomatizable.

---

Elaborating on the first paragraph a bit:

Suppose we have a bi-interpretable pair of structures $\mathcal{A},\mathcal{B}$ - that is, we have an interpretation $\Phi$ of $\mathcal{B}$ in $\mathcal{A}$, an interpretation $\Psi$ of $\mathcal{A}$ in $\mathcal{B}$, a formula $\varphi$ defining in $\mathcal{A}$ an isomorphism $\mathcal{A}\cong\Psi^{\Phi^\mathcal{A}}$, and a formula $\psi$ defining in $\mathcal{B}$ an isomorphism $\mathcal{B}\cong\Phi^{\Psi^{\mathcal{A}}}$. In our case:

• $\mathcal{A}$ is the field of real numbers,

• $\mathcal{B}$ is the field of complex numbers together with a predicate naming the reals,

• $\Phi$ is the usual ordered pair construction of the complex numbers (keeping track of the reals along the way),

• $\Psi$ is "restrict to the $R$-part,"

• and $\varphi$ and $\psi$ are left as exercises.

Then we have a general process for turning axiomatizations of $Th(\mathcal{A})$ into axiomatizations of $Th(\mathcal{B})$:

Suppose $T$ axiomatizes $Th(\mathcal{A})$. Then the following axiomatizes $Th(\mathcal{B})$:

• $T^\Psi$, the theory saying that $T$ holds not in the structure being considered but rather in the related $\Psi^-$ = that structure's $\Psi$-construction (if we're looking at $\mathcal{B}$, this is just $\mathcal{A}$), and

• sentences saying that $\psi$ is in fact an isomorphism between $\Phi^{\Psi^-}$ and the structure under consideration.

The point is that if $\mathcal{B}\not\equiv\mathcal{B}'$ this must be reflected by a first-order difference in $\Psi^\mathcal{B}$ vs. $\Psi^{\mathcal{B}'}$ since the latter recover the former via $\Phi$.

The axiomatization given above, while not literally fitting this form, does exactly this.