About the axiom of choice, the fundamental theorem of algebra, and real numbers - MathOverflow most recent 30 from http://mathoverflow.net2013-06-18T21:04:30Zhttp://mathoverflow.net/feeds/question/100289http://www.creativecommons.org/licenses/by-nc/2.5/rdfhttp://mathoverflow.net/questions/100289/about-the-axiom-of-choice-the-fundamental-theorem-of-algebra-and-real-numbersAbout the axiom of choice, the fundamental theorem of algebra, and real numbersBuschi Sergio2012-06-21T20:39:45Z2012-06-21T23:09:50Z
<p>About fundamental theorem of algebra, there is a large collection different demonstrations.</p>
<p>I ask: is there some proof that avoids AC (choice axiom)?</p>
<p>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. </p>
<p>In ZF theory, are the Dedekind and Cauchy constructions different? (In the "Cauchy" reals, operates on a real number $r$ through a <em>choice</em> of a Cauchy sequence converging to $r$.)</p>
http://mathoverflow.net/questions/100289/about-the-axiom-of-choice-the-fundamental-theorem-of-algebra-and-real-numbers/100293#100293Answer by Andreas Blass for About the axiom of choice, the fundamental theorem of algebra, and real numbersAndreas Blass2012-06-21T21:14:25Z2012-06-21T21:14:25Z<p>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.</p>
<p>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. </p>
<p>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.</p>
http://mathoverflow.net/questions/100289/about-the-axiom-of-choice-the-fundamental-theorem-of-algebra-and-real-numbers/100294#100294Answer by François G. Dorais for About the axiom of choice, the fundamental theorem of algebra, and real numbersFrançois G. Dorais2012-06-21T21:15:03Z2012-06-21T22:12:55Z<p>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 <a href="http://en.wikipedia.org/wiki/K%C3%B6nig%27s_lemma" rel="nofollow">Weak König Lemma</a> (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.</p>
<p>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 <em>every</em> 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.</p>
<hr>
<p>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<sub>0</sub> 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 [<a href="http://mathsci2.appstate.edu/~jlh/bib/pdf/rrepsproof.pdf" rel="nofollow"><em>Representations of reals in reverse mathematics</em></a>, Bull. Pol. Acad. Sci. Math. 55 (2007), 303–316; <a href="http://www.ams.org/mathscinet-getitem?mr=2369116" rel="nofollow">MR2369116</a>].</p>
http://mathoverflow.net/questions/100289/about-the-axiom-of-choice-the-fundamental-theorem-of-algebra-and-real-numbers/100295#100295Answer by Goldstern for About the axiom of choice, the fundamental theorem of algebra, and real numbersGoldstern2012-06-21T21:15:59Z2012-06-21T22:27:20Z<p>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)$. </p>
<p>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. </p>
<p>In constructive mathematics or intuitionistic logic, the story is different, as Francois Dorais explains in his answer. </p>