Return to Question

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).

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).

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-Shishikurs bound on nonrepelling cycles.

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.

For a concrete example of what I am driving at, consider polynomials of degree 2 or more over $\mathbb{C}$. Recall that $\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 assertions:

Note that each assertion is actually a (primitive recursive) family of first order sentences, one for each natural number degree.

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}$:

Note that each assertion is actually a (primitive recursive) family of first order sentences, one for each positive integer degree.