Problem Statement
I'm reading the second edition of Kock's Synthetic Differential Geometry and encountered some trouble in exercise 3.2. To cite,
If $R$ satisfies Axiom $1'$ and contains $\mathbb{Q}$ as a subring, prove that if $f:D_k\to R$ satisfies $$\forall(d_1,\cdots,d_k)\in D^k : f(d_1+\cdots+d_k)=0$$ then $f\equiv 0$
And they say this property is sometimes expressed as "$R$ believes that $\Sigma:D^k\to D_k$ is surjective". I get that if we knew that $\Sigma$ is indeed surjective, then this proof would be immediate, but since it's not we have to work a little harder.
Attempt
My attempt was through induction on $k$ but to keep things simple here I will demonstrate the idea for $k=2$. Consider some $f:D_2\to R$ such that $f(d_1+d_2)=0$ for all $(d_1,d_2)\in D^2$. We take its restriction $g = f|_D:D\to R$. By fixing $d_2=0$ we get $$f(d_1+d_2)=f(d_1)=0$$ and since $d_1+0\in D$ then also $g(d_1)=0$ (In my full proof this means $g$ satisfies the induction hypothesis). Hence we conclude $g \equiv 0$.
Next using axiom $1'$ we can write $$ \forall d\in D_2: f(d) = b_0 + b_1d + b_2d^2 \quad\quad\quad \forall d\in D_1: g(d) = c_0 + c_1d $$ Now the parts I'm not certain about are: can we conclude from $g \equiv 0$ that $c_0=c_1=0$? And from $g$ being a restriction of $f$ that $c_0=b_0, c_1=b_1$? I believe the former is a special case of the latter when $g$ is a restriction of the constant $0$. I tried proving those by repeatedly substituting $d\in D_k$ for increasing $k$s but couldn't quite get all the details, on top of not being sure if my argument accidentally uses LEM behind the scenes.
If this is true we get to the end as follows: for every $d\in D_2$, $$ f(d) = b_2d^2 \Longrightarrow d\cdot f(d) = d\cdot 0 $$ and by cancelling the universally quantified $d$ we get $f(d) = 0$.
$\mathbb{Q}$ as a subring of $R$
So my question is, is the proof valid?
I feel like it's not since I haven't even used the fact that $\mathbb{Q}$ is a subring of $R$, though it seems like a pretty big assumption to ignore. I also feel like I'm not fully appreciating this fact. Seems like it would allow me to get the inverse of any rational number in $R$, but I can't see any place where rationals pop up in this problem at all. (e.g. from axiom $1'$ we get unique coefficients $b_0,\cdots,b_k\in R$ but these are not guaranteed to be rational)
I believe I found the problem: in the very end, I don't think I'm able to cancel the universally quantified $d$ because the remaining expression still depends on it (so it reaches a power not covered by the polynomial in axiom $1'$). But here's how to do it correctly:
In general we end up with $\forall d\in D_k: f(d)=b_kd^k$. By the assumption on $f$, we get $$\forall (d_1,\cdots,d_k)\in D^k: f(d_1+\cdots+d_k)=0=b_k(d_1+\cdots+d_k)^k$$ By (Ex3.1) in the book, $$0=b_kk!\sigma_k(d_1,\cdots,d_k) = b_kk!d_1\cdots d_k$$ where $\sigma_k$ denotes the elementary symmetric polynomial of degree $k$. Those $d_i$s are cancellable as usual, so the only thing we need to cancel is $k!$ which is an integer, and has an inverse thanks to the $\mathbb{Q}$ subring! $\square$