Are integers conservatively embedded in the field of complex numbers?

Question

I am looking for a reference to the fact that $\mathbb{Z}$ is conservatively embedded into the field $\mathbb{C}$ of complex numbers, that is anything in $\mathbb{Z}$ which is definable in $(\mathbb{C},\mathbb{Z},+,\times)$ is already definable in $(\mathbb{Z},+,\times)$.

Answer 1

I don't know a reference, but here's a (slightly overkill) proof:

It's known that $(\mathbb{Z};+,\times)$ interprets an algebraically closed field $K$ of infinite transcendence degree and characteristic zero, and it's not hard to show that additionally the inclusion $\mathbb{Z}\hookrightarrow K$ is also definable in $(\mathbb{Z};+,\times)$. This means that for every logic $\mathcal{L}$ which is at least as strong as first-order logic, every $\mathcal{L}$-definable set of integers in $(K;\mathbb{Z},+,\times)$ is already $\mathcal{L}$-definable in $(\mathbb{Z};+,\times)$. But $(K;\mathbb{Z},+,\times)\equiv_{\infty,\omega}(\mathbb{C};\mathbb{Z},+,\times)$ since e.g. they become isomorphic after forcing with $Col(\omega,2^{\omega})$. Consequently, letting $\mathit{Def}_\mathcal{L}(\mathfrak{M})$ be the set of relations on the structure $\mathfrak{M}$ which are definable in the logic $\mathcal{L}$ and letting $\mathit{Def}_\mathcal{L}^A(\mathfrak{M})$ be the subset of the above consisting of relations contained in a finite power of $A\subseteq\mathfrak{M}$, we have:

If $\mathcal{L}$ is a logic between $\mathsf{FOL}$ and $\mathcal{L}_{\infty,\omega}$, then $$\mathit{Def}_\mathcal{L}^\mathbb{Z}(\mathbb{C};\mathbb{Z},+,\times)=\mathit{Def}_\mathcal{L}(\mathbb{Z};+,\times).$$

In particular, taking $\mathcal{L}=\mathsf{FOL}$ answers the question.

This is a bit overkill though! (That said, it's interesting to note that in $\mathsf{ZF+AD}$ there is a subset of $\mathbb{Z}$ which is second-order-definable over $(\mathbb{C};\mathbb{Z},+,\times)$ but is not second-order-definable over $(\mathbb{Z};+,\times)$: using $\mathsf{AD}$ we get a second-order definition of $\mathbb{R}$ in $(\mathbb{C};+,\times)$, and from there we can define the set of integers coding the full second-order theory of $(\mathbb{Z};+,\times)$, at which point we invoke Tarski.)

---

Here's a possibly interesting follow-up question which tests the idea that this is in fact "tricky to prove" (which is now asked separately):

Replace $+$ and $\times$ with their relational versions $+_R$ and $\times_R$ (e.g. $+_R=\{(a,b,c)\in\mathbb{C}^3: a+b=c\}$). In the resulting language, consider the substructure with underlying set $X=\{2^n:n\in\mathbb{N}\}$ of $\mathbb{C}$. Every element of $X$ is definable in $\mathbb{C}$ so the way it sits inside $\mathbb{C}$ seems plausibly as tame as that for $\mathbb{Z}$. But the interpretation argument above doesn't work since $X$ is "informationally" just $(\mathbb{N};+)$.

Is there a definable relation on $(\mathbb{C};X,+_R,\times_R)$ which lives on $X$ (= is contained in some finite power of $X$) but is not definable in $(X;+_R,\times_R)$ (which is of course just $(X;\times_R)$)?