It is well-known that the first order theory of algebraically closed fields admits quantifier elimination, whence the theory $ACF_p$ of algebraically closed fields of given characteristic $p$ is complete. In particular, for any formula $\phi$ in the language of rings,
$\hspace{1 in}$ $ACF_0\vdash \phi\;\;\;$ if and only if $\;\;\;\overline{\mathbb{Q}}\models \phi\;\;\;$ if and only if $\;\;\;{\mathbb{C}}\models \phi$
where $\overline{\mathbb{Q}}$ is the algebraic closure of $\mathbb{Q}$ in $\mathbb{C}$. The above equivalence is itself elementary, provable within the system $RCA_0$ of weak second order arithmetic. In particular, no metatheoretical appeal to Choice is required: thus, theorems of $ACF_0$ also hold for Lauchli's algebraic closure of $\mathbb{Q}$ which canmot be embedded in $\mathbb{C}$ (see http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=2076124).
Similarly, the first order theory $RCF$ of real closed fields is complete: for any formula $\phi$ in the language of rings,
$\hspace{1 in}$ $RCF\vdash \phi\;\;\;$ if and only if $\;\;\mathcal{R}\models \phi\;\;\;$ if and only if $\;\;\;{\mathbb{R}}\models \phi$
where $\mathcal{R}$ is the real closure of $\mathbb{Q}$ in $\mathbb{R}$.
The theories $RCF$ and $ACF_0$ are closely related. For any model $R$ of $RCF$, the degree 2 field extension $R(i)$ is a model of $ACF_0$. Conversely, any well-orderable model of $ACF_0$ thereby arises from a real closed subfield.
Evidently, the theory obtained by augmenting $ACF_0$ with a constant symbol for $i$ and a predicate symbol for real, and with axioms asserting that the real elements form a real closed subfield, is a conservative extension of $ACF_0$, this even in the absence of Choice. In practice, this means we can establish theorems of $ACF_0$ indirectly, for example by transcendental methods from complex analysis. In many cases (standard applications of the Residue Theorem, for example) such excursions from first order reasoning within $ACF_0$ are largely a matter of presentation. I am interested in cases where it appears otherwise, at least given current understanding.
Are there perhaps well-known examples of theorems in $ACF_0$ whose only known proof requires such a detour through $RCF$? Can it be helpful to assume without loss of generality that consideration of real and imaginary parts is allowed, even if models like Lauchli's do not allow this? I grant that for any given sentence, such a proof might only require ordering a finite extension of $\mathbb{Q}$, this possible in the absence of Choice but still not canonical. Moreover, assertions of interest might arise in families, with a natural number complexity parameter - for example, degree, dimension, etc. For families of assertions, a unified proof by real-variable methods (whether algebraic or transcendental) might not specialize coherently to a family of proofs within $ACF_0$. If this is an a priori possibility, how sharply can such phenomena be delineated? (Such questions motivated my previous post finite dimensional real division algebras).
I have an actual example motivating these queries, namely Thurston's Rigidity Theorem in one dimensional holomorphic dynamics. One version of this result asserts that (except for the well-known "Lattes examples") for maps with finite postcritical orbit, the combinatorics of that orbit determine the Mobius conjugacy class up to finite ambiguity. In fact, the latter statement can deduced by an elementary argument from a algebraic assertion concerning the eigenvalues of an induced cohomology action. The latter assertion (actually a family with natural complexity parameters) admits an easy proof which makes essential reference to real and imaginary parts: the key fact that 1 cannot be an eigenvalue is deduced indirectly from the fact that 1 lies outside the open unit disk and similarly, the fact that $1-\sqrt{2}$ cannot be an eigenvalue is shown (via Galois theory) strictly after it is shown that $1+\sqrt{2}$ cannot be. For many years now I have found this state of affairs very puzzling. I would like to imagine that some as yet unexploited considerations from algebraic number theory might lend insight.
For a concrete example of what I am driving at, consider polynomials over a given ring. Say that a ring element $\zeta$ is a critical point of $f$ if $f'(\zeta)=0$, a critical value if $\zeta=f(\xi)$ for some critical point $\xi$.
Here are two true assertions about nonconstant polynomials over $\mathbb{C}$:
- Some fixed point is not a critical point.
- Some fixed point is not a critical value.
Note that each assertion is actually a (primitive recursive) family of first order sentences, one for each positive integer degree.
Assertion 1 has a straightforward proof: a degree $D$ polynomial has $D$ fixed points (counted with multiplicity) and has derivative 1 at every multiple fixed point, but there are (at most) $D-1$ critical points. On the other hand, colleagues and I do not currently see how to prove Statement 2 without invoking transcendental arguments from complex analysis, such as Fatou's Theorem (infinite critical orbits in parabolic basins) or my own extension of Thurston Rigidity which recovers and sharpens the Farou-Shishikura bound on nonrepelling cycles.
