What is the reverse mathematical strength of the fundamental theorem of algebra? 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.
 A: 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.
A: Bjørn Kjos-Hanssen has answered the stated question but I think it would help to make a few clarifying comments.
Let BWQ denote the statement, "Every bounded infinite sequence from $\mathbb Q$ has an infinite Cauchy subsequence."  What Friedman has shown is not that BWQ implies Con(PA).  (I've gotten confused on this point myself in the past.)  Instead, what he has shown is that Con(RCA_0 + BWQ) implies Con(PA).  See Friedman's posts here and here for example.
If you're looking for other mundane-looking statements whose consistency implies the consistency of PA, then Simpson's book contains a number of candidates, e.g., 


*

*Every countable field is isomorphic to a subfield of a countable algebraically closed field.

*Every countable vector space over $\mathbb Q$ has a basis.

*Every countable commutative ring has a maximal ideal.


Note: One has to be a bit careful about what exactly "countable objects" are in the context of subsystems of second-order arithmetic (as opposed to straight set theory); this fine print is discussed in Simpson's book.
A: It is perhaps instructive to see how Todd's proof of the FTA steps outside of $\mathsf{RCA}_0$ and how it could be modified to fit into $\mathsf{RCA}_0$.
First, let's review some aspects of compactness in subsystems of second-order arithmetic.


*

*Totally bounded complete metric spaces can be formalized in $\mathsf{RCA}_0$ and it is straightforward to show in $\mathsf{RCA}_0$ that $[0,1]$, closed balls in $\mathbb{R}^n$ and closed discs in $\mathbb{C}$ are totally bounded complete metric spaces. [Simpson Definition III.2.3 and following examples. Somewhat confusingly, Simpson uses "compact metric space" for totally bounded complete metric spaces.]

*The system $\mathsf{ACA}_0$ is equivalent over $\mathsf{RCA}_0$ to the statement that every totally bounded complete metric space is sequentially compact [Simpson Theorem III.2.7]. The Bolzano-Weierstrass Theorem is a special case of this and the further special case of $[0,1]$ is already equivalent to $\mathsf{ACA}_0$ over $\mathsf{RCA}_0$ [Simpson Theorem III.2.2].

*The system $\mathsf{WKL}_0$ is equivalent over $\mathsf{RCA}_0$ to the statement that every totally bounded complete metric space is compact [Simpson Theorem IV.1.5]. The Heine-Borel Theorem is a special case of this and the further special case of $[0,1]$ is already equivalent to $\mathsf{WKL}_0$ over $\mathsf{RCA}_0$ [Simpson Theorem IV.1.2].
$\mathsf{WKL}_0$ is strictly stronger than $\mathsf{RCA}_0$ and $\mathsf{ACA}_0$ is strictly stronger than $\mathsf{WKL}_0$. The first-order fragment of $\mathsf{ACA}_0$ is $\mathsf{PA}$ and every model of $\mathsf{PA}$ can be expanded to a model of $\mathsf{ACA}_0$; the $\mathsf{RCA}_0$ and $\mathsf{WKL}_0$ have the same first-order fragment, $\mathsf{PA}$ with induction restricted to $\Sigma_1$-formulas, and likewise any first-order model of that theory can be expanded to a model of $\mathsf{WKL}_0$ (and hence of $\mathsf{RCA}_0$).
Now back to Todd's proof. As in Todd's proof, let $f(z)$ be a nonconstant polynomial over $\mathbb{C}$.
Todd first step uses the Bolzano-Weierstrass Theorem (BWT) for closed discs in $\mathbb{C}$. At first sight, this requires $\mathsf{ACA}_0$ but the point is to show that $|f(z)|$ attains a minimum value. The weaker subsystem $\mathsf{WKL}_0$ already proves that every continuous real-valued function on a totally bounded complete metric space attains a minimum value [Simpson Theorem IV.2.2]. The remaining parts of Todd's proof are direct computations, so now we have a proof in $\mathsf{WKL}_0$. Since the Extreme Value Theorem is equivalent to $\mathsf{WKL}_0$ over $\mathsf{RCA}_0$ [Simpson Theorem IV.2.3] it seems that we can't do much better. This would be the case if $f(z)$ were an arbitrary continuous function, but polynomials aren't arbitrary at all!
The first key fact about polynomials is that they have computable modulus of uniform continuity. In fact, for every closed disc $D$, we can use the coefficients of $f(z)$ to compute a constant $C_D$ such that $|f(x)-f(y)| \leq C_D|x-y|$ for all $x, y \in D$. This can be carried out in $\mathsf{RCA}_0$ and this is enough to show that $\inf\{|f(z)| : z \in D\}$ exists. However, the modulus of uniform continuity alone is not enough to show that this infimum is attained.
The second key fact about polynomials is that they can only have finitely many roots and we can calculate exactly how many there should be: the degree of $f(z)$ minus the degree of the gcd of $f(z)$ and $f'(z)$. Let's call this number $n$. This allows us to home in on a root in a deterministic fashion rather than using Bolzano-Weierstrass. Given disjoint closed  disks $D_1,\ldots,D_n$ such that $\inf\{|f(z)|: z \in D_i\} = 0$ for $i = 1,\dots,n$, we can effectively compute rapidly convergent Cauchy sequence for the unique roots $r_1 \in D_1,\ldots,r_n \in D_n$. To find an element of $D_i$ within $\varepsilon \gt 0$ of the purported $r_i$, find a small $\delta \gt 0$ and a cover of $D_i$ with open balls $B(z_1,\delta),\ldots,B(z_k,\delta)$ such that the elements of $\{z_j : |f(z_j)| \lt C_{D_i}\delta\}$ are all within $\varepsilon$ of each other and pick any element of that set.
I don't see how to adapt Todd's proof to show that $\inf\{|f(z)| : z \in \mathbb{C}\}$ must be $0$ without showing first that the infimum is attained. However, the two key facts above do explain how to circumvent Bolzano-Weierstrass when working with polynomials rather than arbitrary functions.
