11
$\begingroup$

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*?

Improve this question
$\endgroup$
7
  • 1
    $\begingroup$ If $F$ is a field containing at least $n+1$ distinct elements (and "distinct" means "you know the inverses of their pairwise differences"), then every polynomial of degree $\leq n$ that is identically zero on $F$ must be zero coefficient-wise. The proof is absolutely constructive (pure computation - look up "Lagrange interpolation"). I am pretty sure that in every reasonable logical system, "infinite" implies that you CAN pick $n+1$ distinct elements of the field, because otherwise the notion of infinity would be ottally useless. $\endgroup$
    – darij grinberg
    Commented Dec 15, 2010 at 21:26
  • 1
    $\begingroup$ I've looked up Lagrange interpolation, and the only uniqueness proofs I've seen use the fundamental theorem of algebra. Also, even if the proof was "absolutely constructive", that's not what I'm asking for. (unless you define "absolutely constructive" as "formalizable in RCA0*") $\endgroup$
    – user5810
    Commented Dec 16, 2010 at 3:18
  • 1
    $\begingroup$ Where do they use the fundamental theorem of algebra? $\endgroup$
    – darij grinberg
    Commented Dec 16, 2010 at 9:33
  • 1
    $\begingroup$ BTW here is an easier proof (not mathematically easier, but easier to explain): en.wikipedia.org/wiki/Polynomial_interpolation . All we need is that the Vandermonde determinant is nonzero (= you can divide by it), but this is clear from the formula for the Vandermonde determinant. I don't understand the definition of RCA0*, but if you have any logical framework that allows you to do ANYTHING reasonable with fields (such as: divide by an element that is not zero), and ANYTHING reasonable with infinite sets (such as, picking $m$ pairwise distinct elements for any $m\in\mathbb N$), ... $\endgroup$
    – darij grinberg
    Commented Dec 16, 2010 at 9:37
  • 1
    $\begingroup$ ... then you can prove the uniqueness of polynomial interpolation in this framework. $\endgroup$
    – darij grinberg
    Commented Dec 16, 2010 at 9:37

0

Reset to default

You must log in to answer this question.