Completeness of real closed fields within ZFC

Question

Tarski proved that the theory of real closed fields (RCF) is complete. But does this theory stay complete when interpreted within ZFC? We know that ZFC can't be complete because it can interpret arithmetic. My guess is that RCF within ZFC becomes incomplete since we can define a predicate which picks out the set-theoretic natural numbers among the set-theoretic real numbers. According to Peter Smith, this is $\textsf{Nat}()$ predicate is essential to showing that a theory is incomplete (or has he puts it, incompleteable).

More formally, let $T$ be a complete theory within some language $L_T$ and let $S$ be a theory within some langauge $L_S$ which can interpret arithmetic. Suppose we can map every unique element of $T$'s domain to a unique element of $S$'s domain and that every function symbol, constant symbol, relation symbol, and quantifier (to pick out only the S-elements which correspond to T-elements) in $L_T$ can be defined as some wff of $L_S$ . Then is $S$ negation complete w.r.t to sentences constructed from these wffs?

If my guess is correct, can someone provide an example of a statement within RCF for which it and its negation are not provable when interpreted in ZFC? Originally I was thinking the continuum hypothesis but on second thought this requires more than what the language of RCF can talk about.

Answer 1

Your guess is incorrect: $\mathsf{RCF}$ remains complete even when we restrict to what $\mathsf{ZFC}$ itself can prove. To make this precise:

For every sentence $\sigma$ in the language of $\mathsf{RCF}$, either $\mathsf{ZFC}\vdash(\mathsf{RCF}\vdash\sigma)$ or $\mathsf{ZFC}\vdash(\mathsf{RCF}\vdash\neg\sigma)$. Moreover, this statement itself is provable inside $\mathsf{ZFC}$.

This doesn't immediately follow from the statement of Tarski's theorem, but it does follow from the proof: the proof that $\mathsf{RCF}$ is complete is entirely constructive, giving a specific algorithm for checking whether or not a sentence is a theorem of $\mathsf{RCF}$, and $\mathsf{ZFC}$ can prove that this algorithm is correct and always terminates.

---

To see that the OP (and the answer above) is not actually trivial, consider the case of true arithmetic $\mathsf{TA}$. This is definable in set theory, and so the following question makes sense:

"Is it the case that, for every sentence $\varphi$ in the language of arithmetic, either $\mathsf{ZFC}\vdash(\mathsf{TA}\vdash\varphi)$ or $\mathsf{ZFC}\vdash(\mathsf{TA}\vdash\neg\varphi)$ hold?"

But this time, in contrast with the $\mathsf{RCF}$ example, the answer is negative: if we take $\varphi$ to be the Rosser sentence for $\mathsf{ZFC}$, then (unless $\mathsf{ZFC}$ is inconsistent of course!) $\mathsf{ZFC}$ cannot tell whether $\varphi$ is true (remember that "provable from $\mathsf{TA}$" is synonymous with "true," literally by definition, for sentences of arithmetic).