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