Do there exist some results on the theory of $\mathbb{C}$ in the language $\{0,1+, \times, \overline{\cdot}\}$, where $\overline{\cdot}$ is the conjugation map $\overline{a+ib} = a - ib$?


I'm wondering in particular if it has QE (or if a sensible expansion of the language has QE), and if it's decidable. But properties like model-completeness, (bi)-interpretability with standard, well-understood structures etc. would be helpful to know too.



Model theory of the complex numbers with conjugation
It is a decidable theory, because it is interpretable in the real-closed field $\langle\mathbb{R},+,\cdot,0,1\rangle$, which has a decidable theory. We can interpret complex numbers $a+bi$ as pairs of real numbers $(a,b)$, and the complex structure, including conjugation, is definable in the reals. (Indeed, this is easily seen to be a bi-interpretation, since we can define $\mathbb{R}$ via conjugation in $\mathbb{C}$.) By [Tarski's theorem on real-closed fields](https://en.wikipedia.org/wiki/Real_closed_field#Decidability_and_quantifier_elimination), that theory is decidable, and so we can decide the complex theory also. 


Basically, for any given statement in the complex field with conjugation, we can translate it to a question in the real-closed field. By Tarski's result, that question is equivalent to a quantifier-free assertion in the real-closed field $\langle\mathbb{R},+,\cdot,<\rangle$, which we can then easily decide. 


Since the interpretation doesn't involve any quantifiers (note that we can clear the use of unary minus in conjugation by moving negatives to the other side of any equation), it follows as Alex Kruckman notes in the comments that we will get model-completeness of the complex field with conjugation. 


My earlier claim that we get full QE for $\mathbb{C}$ stumbles on the fact that $\langle \mathbb{R},+,\cdot\rangle$ doesn't have QE, since you need the order in Tarski's result. As Alex mentions, you can define the positive real line in $\langle\mathbb{C},+,\cdot,\bar{}\rangle$, but this will not be quantifier-free definable. 


If we add the real and imaginary part operators and the order for the real line as a relation on $\mathbb{C}$, however, then we will get QE in the corresponding expansion, and this expansion will also be bi-interpretable with the real-closed field.


