What is an explicit axiomatization of the complex field along with the real numbers? 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.
 A: 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.
