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

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

-
It is a theorem of ZF that any two complete (in the order sense) ordered fields are isomorphic. In particular, the complete ordered fields constructed by the Dedekind and Cauchy methods are isomorphic. AC is not needed for any of this. – Gerald Edgar Jun 21 '12 at 21:35
Gerald, that's an interesting remark. I believe that this fact is also intuitionistically valid. In fact, in a topos, the Cauchy and Dedekind reals are the same precisely when the Cauchy reals are ordered... – François G. Dorais Jun 21 '12 at 23:03

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.

-

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 RCA0 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].

-
Another clarification, by "comparing a real with a rational," I mean comparison in the weak sense, $a \leq b \lor a \geq b$; strong comparison, $a \lt b \lor a = b \lor a \gt b$, is equivalent to the stronger Limited Principle of Omniscience (LPO). – François G. Dorais Jun 21 '12 at 22:42

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.

-
I was looking for a reference for this result of Ernst Specker, here it is: MR0256880 ams.org/mathscinet-getitem?mr=256880 Note that the result is peculiar: For each $m \geq 1$ there is a continuous function that returns the $m$-element multiset of the roots of the (not necessarily irreducible) polynomial of degree $m$, but there is no continuous function that picks just one element from that multiset except in the case $m = 1$! – François G. Dorais Jun 21 '12 at 22:29