According to wikipedia, the statement "every polynomial over a countable field that is not the zero polynomial has only finitely many roots" is equivalent to RCA0 over RCA0* (which is called ERCA-0 in this answer). I've been interested in reverse math for 1-2 years, so when I got to working with polynomial rings, I got curious as to the strength of the equivalence of their representations as functions and formal polynomials. Let izizp (identically zero implies zero polynomial) be the following statement:

For all (countably) infinite fields $F$, for all members $c_0,...,c_n$ of $F$, if $\; \displaystyle\sum_{m=0}^n \; \; c_m\cdot x^m \;$ is identically zero, then $c_0,...,c_n$ are all zero.

Is izizp a theorem of RCA0*?

Is izizp equivalent to RCA0 over RCA0*?

define"absolutely constructive" as "formalizable in RCA0*") – Ricky Demer Dec 16 '10 at 3:18