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)

Regards