Reverse Mathematical Strength of the Fundamental Theorem of Algebra – Logic and Reverse Math

lo.logicreverse-math

Reverse mathematics (RM) is that area that tries to pin down exactly which axioms are necessary to prove theorems, given some weak base theory. Harvey Friedman has pointed out several times (on the FOM mailing list) that $Con(PA)$ is equivalent to a variant of Bolzano-Weierstrass over the rationals between 0 and 1 inclusive (something like: every sequence has a subsequence $\{q_i\}$ which is Cauchy, in the that sense $\forall i,j \geq n, |q_i – q_j| < 1/n$). Apparently a very similar result is given in Simpson's book and "it is clear to the experts" how to get to Friedman's claim. (As an aside, I find this such an amazing result it should be written up for the average mathematician, and not buried in a vaguely equivalent form in a book that is hard to get one's hands on.)

The reason I bring up Bolzano-Weierstrass is that Todd Trimble, in a nice answer on Ways to prove the fundamental theorem of algebra, uses B-W to prove (as the key tool among other, elementary considerations) the fundamental theorem of algebra. Todd then had a look to see, at my behest, if the RM strength of FTA was known. He came up blank, so I ask here:

How close in reverse mathematical strength are the Bolzano-Weierstrass statement from Friedman's claim and the fundamental theorem of algebra?

If they are the same, then we find ourselves in the amazing situation that the consistency of PA is equivalent to a theorem that we all would use with no qualms whatsoever. However, I have a vague feeling that FTA is strictly weaker than BW (as used here), but cannot make this precise.

Best Answer

Tanaka and Yamazaki (in the volume Reverse Mathematics 2001, see review) show that a substantial portion of field theory can be done in the weak base theory RCA$_0$, by proving in RCA$_0$ the fundamental theorem of algebra as well as quantifier elimination for the theory of real closed fields.

So the FTA is weaker than BW.