About the axiom of choice, the fundamental theorem of algebra, and real numbers

Question

About fundamental theorem of algebra, there is a large collection different demonstrations.

I ask: is there some proof that avoids AC (choice axiom)?

In a general topos (with natural number object) there are the two constructions of real numbers (generalizations of the classical Dedekind and Cauchy constructions) that are different.

In ZF theory, are the Dedekind and Cauchy constructions different? (In the "Cauchy" reals, operates on a real number $r$ through a choice of a Cauchy sequence converging to $r$.)

Answer 1

The fundamental theorem of algebra is, unless I miscounted quantifiers, a $\Pi^1_2$ sentence of second-order arithmetic and therefore absolute between the full universe and Gödel's constructible universe by the Shoenfield absoluteness theorem. So, since it's provable in ZFC, it is necessarily provable in ZF as well.

I believe, though, that this metamathematical argument can be avoided, because I don't see any serious use of the axiom of choice in usual proofs by methods of analysis and (plane) topology.

The Dedekind and Cauchy constructions of the reals are equivalent in ZF; no choice is needed. Although AC is often involved when one wants to prove general results about sequences of reals, in the present situation one only needs to consider sequences of rationals. So one can fix an enumeration of the rationals and thereafter, whenever a rational needs to be chosen, taking the first suitable one in the enumeration.

Answer 2

Regarding Cauchy and Dedekind reals. The fact that every Dedekind real has a Cauchy representation is provable in very weak systems of intuitionistic analysis. The converse fact that every Cauchy real has a Dedekind representation is equivalent to the Weak König Lemma (WKL) — that every infinite tree of $\lbrace0,1\rbrace$-sequences has an infinite path. (See note.) This very weak form of König's lemma is provable in ZF, so there is no difference between Cauchy reals and Dedekind reals in ZF.

Breaking this down further, the ability to compare a Cauchy real to a given rational number is equivalent to the Lesser Limited Principle of Omniscience (LLPO), which can be formulated as follows $$\lnot(\exists n A(n) \land \exists n B(n)) \rightarrow (\forall n \lnot A(n) \lor \forall n \lnot B(n)),$$ where $A(n)$ and $B(n)$ are simple decidable statements (e.g., primitive recursive predicates). Note that LLPO is a consequence of the Law of Excluded Middle, and therefore true in every classical system such as ZF, but not necessarily in intuitionistic systems such as topoi. To extract a Dedekind cut from a Cauchy real, it is necessary to simultaneously compare a real with every rational number, so we need to repeat LLPO countably many times. WKL is precisely equivalent to countably many repetitions of LLPO. In set theory and topos theory, such repetitions come for free through comprehension. So the only thing that can prevent every Cauchy real to have a Dedekind cut in a topos is the failure of LLPO.

---

This is not quite true as I originally stated it. It is the existence of a "uniform method" for converting Cauchy reals into Dedekind reals which is equivalent to WKL. In classical systems, one can get around the uniformity requirement through clever use of the Law of Excluded Middle. In weak classical systems such as RCA₀ one can prove that every Cauchy real has a Dedekind cut by providing separate methods for rational and irrational numbers, thus sweeping a lot of the computation cost in deciding whether a real is rational or not. The equivalence with WKL is recovered when one asks to simultaneously find Dedekind cuts for an infinite sequence of Cauchy reals, as demonstrated by Hirst [Representations of reals in reverse mathematics, Bull. Pol. Acad. Sci. Math. 55 (2007), 303–316; MR2369116].

Answer 3

In classical logic, using the ZF axioms, one can show that there is an isomorphism between the Dedekind cuts in the rationals, and the equivalence classes of Cauchy sequences. One can also (without AC) choose a representative from each equivalence class of Cauchy sequences. (EDIT: In high school one might chose decimal fractions, and represent $\pi$ by the sequence $(3, 3.1, 3.14,\ldots)$; a more sophisticated approach might choose continued fractions and represent $\pi$ by the sequence $(3, 22/7, 333/106,\ldots)$.

The fundamental theorem of algebra (every non-constant polynomial with real or complex coefficients has a zero in the complex numbers) can be proved without AC. In fact, there is a quite explicit algorithm that computes, for each irreducible polynomial (with leading coefficient 1, to be on the safe side), the roots of this polynomial continuously from the coefficients.

In constructive mathematics or intuitionistic logic, the story is different, as Francois Dorais explains in his answer.

Answer 4

In an intuitionistic setting, the exact choice principles that it requires does indeed depend on the definition of the reals that you start with. If your complex numbers are defined as some sequence of approximations (by the rationals or some other system), the existence of complex roots of arbitrary complex numbers is equivalent to being able to consistently choose a branch of the roots for each approximation.

The axiom of weak countable choice (WCC) which follows both from countable choice and from LEM is often introduced as a sufficient choice principle to prove the fundamental theorem of algebra. It is just the restriction of countable choice to the case where at most one of the sets is not a singleton so that only one choice needs to be made (but where you can't tell for which of the countable number of sets you need to make a choice).

If you have omniscience you can just reduce it to a single choice, so in classical logic this requires no choice principle, and so the FTA holds in ZF (and much weaker systems). On the other hand, weak countable choice, fails for Sh(X) where X is any locally connected Tychonoff space though, and for smooth topoi where it is false that every number that squares to 0 is zero and where nilpotent infinitesimals are important, roots will behave fairly differently from in Set.

So there are plenty of very natural models where key theorems like the FTA may need to be rephrased in some way. One approach in those cases is to avoid choice entirely by rephrasing it in terms of (something that is classically equivalent to) multisets of roots.