The axiom of replacement is usually used to prove the existence of large sets, to provide a reflection principle, for transfinite recursion… However, I am wondering how it affects finite sets. Let me give two concrete questions (let S be ZF without replacement and without infinity, SF=S+replacement, Z=S+infinity):

- Are there theorems in SF+“every set is finite” which cannot be proved in S+“every set is finite”? In an alternative formulation: Does S+“every set is finite” imply the axiom of replacement? If not: Is there some instructive construction which fails?
- Assume we are working in Z or ZF and consider the set $HF$ of all hereditarily finite sets: Are there “natural” statements about $HF$ which can be proved in $ZF$ but not in $Z$? (of course there are such statements, namely in $ZF$ we can prove that $HF$ is a model of some first-order statements expressing that $Z$ plus any given finite fragment of $ZF$ is consistent (and some similar statements), but I am looking for different properties)

“Finite” should be defined using natural numbers, which are Dedekind finite ordinals. Feel free to use strong versions of foundation for the first question. If something interesting happens with the negation of such an axiom, it would be interesting, too.

Regards