Can all theorems of $\sf ZFC$ about the natural numbers be proven in $\sf ZF$?

Question

I know a proof of Hindman's theorem that uses ultrafilters on the natural numbers, and ultimately, the axiom of choice. But the theorem itself is essentially a combinatorial property of the natural numbers, so somehow I expect that there should be a proof which doesn't need choice, especially since it can be written in a totally "finitistic" form. My question is not about Hindman's theorem itself though; I am interested to know if we have a general method of reduction of proof from $\sf ZFC$ to $\sf ZF$, for theorems that can be stated in the language of $\sf PA$.

Answer 1

Turning my comment into an answer:

Any arithmetic statement provable in $\mathsf{ZFC}$ is provable in $\mathsf{ZF}$. The point is that if $\mathsf{ZFC}$ proves that $\mathbb N\models\phi$, then $\mathsf{ZF}$ proves that $L$ models that $\mathbb N\models\phi$. To see this, note that the $\mathsf{ZFC}$ proof uses only finitely many axioms of $\mathsf{ZFC}$, and it is a theorem of $\mathsf{ZF}$ that $L$ satisfies these axioms.

We conclude by noting that if $L\models \mathbb N\models\phi$, then $\mathbb N\models \phi$.

The argument can be pushed a bit. The Shoenfield absoluteness theorem gives us that the same holds not just for arithmetic statements ($\Sigma^0_n$ for some $n$), but even for $\Sigma^1_2$ statements. (Kanamori's book on large cardinals has a careful discussion of this result.) And this is not the end of the story: Leaving the arithmetic hierarchy, we can still find traces of absoluteness; for instance, see here.