Impact of the axiom of replacement on finite sets 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
 A: I claim that replacement is provable in the theory S+"every set is finite". One proves any instance by induction on the size of the domain of the function. That is, a given instance of replacement says that if $A$ is a set and we have for every $a\in A$ a unique $b$ such that $\varphi(a,b)$, then the set $\{b\mid \exists a\in A\, \varphi(a,b)\}$ is a set. Suppose this is true for all sets smaller than $A$. Now, remove one element from $A$, apply the induction hypothesis, and then add in the missing $b$.
So the answer to your first question is yes.
A: In his paper "Finite-to-one maps" [ Journal of Symbolic Logic 68 (4):1251-1253 (2003) ], Thomas Forster proves the following result:
If there exists a surjection from the power set of $X$ to $X$ with all fibres finite then $X$ is itself finite. 
Forster proves this result in ${\bf ZF}$, by an argument which makes manifest use of Replacement. He poses the question as to whether or not this is in fact a theorem of $\bf Z$. 
A: I am definitely not an expert in the relevant areas, so I hope this answer is critiqued by experts in the comments, but my impression is that this question may have implicitly been answered by this excellent answer to a related question: https://mathoverflow.net/a/323034/93694
First, let me assume (following that answer and the comments above) that the theories $\mathsf{S}$ and $\mathsf{SF}$ as defined in this question use the axiom schema of $\in$-induction, rather than the typical foundation/regularity axiom. (If not, then redefine them.) So to be explicit
$$\mathsf{SF}  = \mathsf{Empty} +\mathsf{Ext}+\mathsf{Pair}+\mathsf{Union}+\in\mbox{-}\mathsf{Ind}+\mathsf{Sep}+\mathsf{Rep}+ \mathsf{Power},$$
$$\mathsf{S} = \mathsf{Empty} +\mathsf{Ext}+\mathsf{Pair}+\mathsf{Union}+\in\mbox{-}\mathsf{Ind}+\mathsf{Sep} + \mathsf{Power}.$$
Cf. also this answer to a related question. (Actually some care is needed here, because replacement might be needed for power set? But maybe that’s only in the absence of epsilon induction?)
As mentioned in the other answer, the power set axiom is a theorem of either $\mathsf{S} + \lnot \mathsf{Inf}$ or $\mathsf{SF}+ \lnot \mathsf{Inf}$, so
$$\mathsf{SF} + \neg \mathsf{Inf} = \mathsf{Empty} +\mathsf{Ext}+\mathsf{Pair}+\mathsf{Union}+\in\mbox{-}\mathsf{Ind}+\mathsf{Sep}+\mathsf{Rep} + \neg \mathsf{Inf},$$
$$\mathsf{S} + \neg \mathsf{Inf} = \mathsf{Empty} +\mathsf{Ext}+\mathsf{Pair}+\mathsf{Union}+\in\mbox{-}\mathsf{Ind}+\mathsf{Sep} + \neg \mathsf{Inf}.$$
I.e. $\mathsf{SF} + \lnot \mathsf{Inf}$ is the same as what the other answer refers to as $\mathsf{ZFfin}$, which in turn is the same as $\mathsf{ZFCfin}$ because the axiom of choice also becomes a theorem with $\lnot \mathsf{Inf}$.
Although technically what is meant by negating the axiom of infinity also requires some care, cf. this comment. Assume for the sake of simplicity that we’ve made the same choice as in the Kaye and Wong paper [KW], i.e. a choice that works.
So then the question is basically whether $\mathsf{Rep}$ is a theorem of $\mathsf{S} + \neg \mathsf{Inf}$, so that $\mathsf{SF} + \neg \mathsf{Inf} = \mathsf{S} + \neg \mathsf{Inf}$. Clearly $\mathsf{Rep}$ is not a theorem of $\mathsf{S}$, e.g. given a model of ZFC the set $V_{\omega+\omega}$ is a model of $\mathsf{S}$ but not of $\mathsf{SF}$.
Both the comments to this question and that other answer mention the "folklore" result that $\mathsf{SF} + \lnot \mathsf{Inf}$ is bi-interpretable with first-order Peano arithmetic $\mathsf{PA}$.
The answer gives an even stronger result involving finite fragments of these theories, namely for any $n$
$$\mathsf{SF}_n + \neg \mathsf{Inf} = \mathsf{Empty} +\mathsf{Ext}+\mathsf{Pair}+\mathsf{Union}+\in\mbox{-}\mathsf{Ind}+ \Sigma_n \mbox{-}\mathsf{Sep}+ \Sigma_n \mbox{-}\mathsf{Rep} + \neg \mathsf{Inf},$$
$$\mathsf{S}_n + \neg \mathsf{Inf} = \mathsf{Empty} +\mathsf{Ext}+\mathsf{Pair}+\mathsf{Union}+\in\mbox{-}\mathsf{Ind}+\Sigma_n \mbox{-}\mathsf{Sep} + \neg \mathsf{Inf}.$$
Here $\Sigma_n \mbox{-}\mathsf{Sep}$ denotes the separation axiom schema restricted to $\Sigma_n$ formulas in the Levy hierarchy, and completely analogously $\Sigma_n \mbox{-}\mathsf{Rep}$ denotes the replacement axiom schema restricted to $\Sigma_n$ formulas in the Levy hierarchy.
The TL;DR is that it seems to be the case that when assuming $\mathsf{S}_1 + \neg \mathsf{Inf}$, then for every n, $\Sigma_n \mbox{-} \mathsf{Rep} \implies \Sigma_n \mbox{-} \mathsf{Sep}$ and $\Sigma_{n+1} \mbox{-} \mathsf{Sep} \implies \Sigma_n \mbox{-} \mathsf{Rep}$, i.e. that for all $n \ge 1$ we have that $\mathsf{SF}_n + \neg \mathsf{Inf} \implies \mathsf{S}_n + \neg \mathsf{Inf}$ and $\mathsf{S}_{n+1} + \neg \mathsf{Inf} \implies \mathsf{SF}_n + \neg \mathsf{Inf}$.
Hence any model of $\mathsf{S}_n + \neg \mathsf{Inf}$ for all $n$ must also be a model of $\mathsf{SF}_n + \neg \mathsf{Inf}$ for all $n$, i.e. (by compactness) any model of $\mathsf{S} + \neg \mathsf{Inf}$ must also be a model of $\mathsf{SF} + \neg \mathsf{Inf}$ and so (by the Godel completeness theorem) $\mathsf{Rep}$ is a theorem of $\mathsf{S} + \neg \mathsf{Inf}$, i.e. $\mathsf{S}+ \neg \mathsf{Inf}$ = $\mathsf{SF} + \neg \mathsf{Inf}$.
At least heuristically speaking, this basically says that the fact that the induction schema $\mathsf{I}$ in $\mathsf{PA}$ proves the boundedness schema $\mathsf{B}$ in $\mathsf{PA}$ can be used to show that the separation schema $\mathsf{Sep}$ in $\mathsf{SF} + \lnot\mathsf{Inf}$ proves the replacement schema $\mathsf{Rep}$ in $\mathsf{SF} + \lnot\mathsf{Inf}$, and hence that $\mathsf{SF} + \lnot\mathsf{Inf}$ = $\mathsf{S} + \lnot\mathsf{Inf}$.
So basically it seems the answer to that other question can maybe be understood as making extremely precise the solution proposed in the comment and answer to this question. In other words, the fact that the proof is inductive is probably not a coincidence, and the answer explains one reason why.
Of course, this is not a proof, but intuitively the result at least seems plausible, given that $V_{\omega + \omega}$ already suffices to model $\mathsf{ZFC} - \mathsf{Rep} + \mathsf{Sep}$, it would be highly surprising if $\mathsf{S} + \lnot \mathsf{Inf} = \mathsf{ZFCfin} - \mathsf{Rep}$ which is already modeled by $V_{\omega}$ would gain any new models by adding $\mathsf{Rep}$ as an axiom scheme. Again though that is just a heuristic plausibility argument for the result, not even remotely a proof.

Anyway let me explain the details (as far as I understand them) of how the answer to the related question seems to provide the above solution to this question.
Let $\mathsf{Q}_{\le}$ denote Robinson arithmetic $\mathsf{Q}$ augmented with two symbols and two definitional axioms, one for each of $\le$ and $<$. Then recall that the induction axiom schema in the language of $\mathsf{Q}$ is:
$$ \forall \bar{p} \left( (\varphi(0, \bar{p}) \land \forall n (\varphi(n, \bar{p}) \rightarrow \varphi(S(n), \bar{p})) ) \rightarrow \forall n (\varphi(n, \bar{p})    \right)  \tag{$\mathsf{I}$} $$
Note that first-order Peano arithmetic $\mathsf{PA}$ is equivalent (under closure of deduction) to $\mathsf{Q} + \mathsf{I}$.
The following boundedness schema $\mathsf{B}$ in the language of $\mathsf{Q}_{\le}$ is a theorem of $\mathsf{PA}$ (i.e. when assuming the full induction axiom schema $\mathsf{I}$) in the language of $\mathsf{Q}_{\le}$:
$$\forall \bar{p} \left( \forall m (     
(\forall \mu \le m)(  \exists n (  \varphi(\mu, n, \bar{p}) ) \rightarrow
\exists n (  (\forall \mu \le m)( (\exists \nu \le n) ( \varphi (\mu, \nu, \bar{p}) )     )   )
  )   )
 )   \right)  \tag{$\mathsf{B}$} \,. $$
However, fragments of $\mathsf{B}$ become relevant when discussing fragments of $\mathsf{PA}$, as discussed below.
In what follows, for the sake of brevity I will assume that the reader understands the arithmetic hierarchy of formulas in the language of $\mathsf{Q}_{\le}$ and the basic nuances associated with it. (Even though I admittedly don’t yet fully understand them myself.) I will also assume familiarity with the Levy hierarchy from set theory, which is an analogous idea.
However the main facts about the arithmetic hierarchy that are relevant for what follows is that $\Delta_0$ formulas are the same (by definition) as $\Sigma_0$ formulas, and that for every $n \ge 0$ there is a strict inclusion $\Sigma_n \hookrightarrow \Sigma_{n+1}$ of $\Sigma_n$ formulas inside of $\Sigma_{n+1}$ formulas, i.e. every $\Sigma_n$ formula is $\Sigma_{n+1}$, but not vice versa, i.e. there exists $\Sigma_{n+1}$ formulas that are not $\Sigma_n$.
From this it follows that the induction axiom schema restricted to $\Delta_0$ formulas, denoted $\mathsf{I\Delta}_0$, is a weaker axiom schema than the induction axiom schema restricted to $\Sigma_n$ formulas, denoted $\mathsf{I\Sigma}_n$, for all $n\ge 1$. More generally, we always have that the induction axiom schema restricted to $\Sigma_{n+1}$ formulas, $\mathsf{I\Sigma}_{n+1}$, always implies the induction axiom schema restricted to $\Sigma_n$ formulas, $\mathsf{I\Sigma}_n$, for every $n$. Completely analogously, the boundedness schema restricted to $\Sigma_{n+1}$ formulas, $\mathsf{B\Sigma}_{n+1}$, implies the boundedness schema restricted to $\Sigma_n$ formulas, $\mathsf{B\Sigma}_n$, for every $n$.
The base theory we work with is $\mathsf{Q}_{\le}$ together with the weakest possible form of induction, $\mathsf{I \Delta}_0$. Now it is a theorem that, when assuming $\mathsf{Q}_{\le} + \mathsf{I\Delta}_0$, we have for all $n \ge 0$ that $\mathsf{B\Sigma}_n \implies \mathsf{I\Sigma}_n$ and that $\mathsf{I\Sigma}_{n+1} \implies \mathsf{B\Sigma}_n$. Cf. Theorem A of [PK] or section 1.2.4 of [Bu]. Neither of the two implications can be reversed.
Now the big result, mentioned in the other answer, and which appears to be discussed in detail in the Kaye and Wong paper (cf. Section 7 and in particular Theorem 21), is that for every $n \ge 1$ (the assumption $n \ge 1$ is crucial, see below), we have that $\mathsf{S}_1 + \neg \mathsf{Inf} + \Sigma_n \mbox{-} \mathsf{Sep} + \Sigma_m \mbox{-} \mathsf{Rep}$ is bi-interpretable with $\mathsf{Q}_{\le} + \mathsf{I\Sigma}_1 + \mathsf{I\Sigma}_n + \mathsf{B\Sigma}_m$.
Because bi-interpretability appears to effectively mean that theorems from one theory can be transported to the other theory and vice versa unproblematically, this bi-interpretability result combined with result that $\mathsf{B\Sigma}_n \implies \mathsf{I\Sigma}_n$ seems to mean that $\mathsf{S}_1 + \lnot \mathsf{Inf} + \Sigma_n \mbox{-} \mathsf{Rep} \implies \mathsf{S}_1 + \lnot \mathsf{Inf} + \Sigma_n \mbox{-} \mathsf{Sep}$, which by a simple inductive argument would mean that $\mathsf{SF}_n + \lnot \mathsf{Inf} \implies \mathsf{S}_n + \lnot \mathsf{Inf}$. (Although  phrased that way this isn’t interesting / surprising because by definition $\mathsf{SF}_n$ contains a superset of the assumptions of $\mathsf{S}_n$.)
More importantly and interestingly to us, the bi-interpretability result appears to mean that $\mathsf{Q}_{\le} + \mathsf{I\Delta}_0 + \mathsf{I\Sigma}_{n+1} \implies \mathsf{Q}_{\le} + \mathsf{I\Delta}_0 + \mathsf{B\Sigma}_{n}$ in turn implies that $\mathsf{S}_{n+1} + \lnot \mathsf{Inf} \implies \mathsf{SF}_n + \lnot \mathsf{Inf}$. And so anyway as argued above this latter result is sufficient to imply that $\mathsf{SF} + \lnot \mathsf{Inf}$ and $\mathsf{S} + \lnot \mathsf{Inf}$ are the same theory.
The interpretation of “set theory inside of arithmetic” used for these bi-interpretability results is the Ackermann encoding of sets as natural numbers. In order for this encoding to succeed, the exponential function in the natural numbers needs to be defined, but this is only possible with induction on formulas of $\Sigma_1$ complexity or higher. More explicitly, $\mathsf{Q}_{\le} + \mathsf{I \Sigma_1} \implies \mathsf{Q}_{\le} + \mathsf{I\Delta}_0 + \mathsf{Exp} \implies \mathsf{Q}_{\le} + \mathsf{I\Delta}_0$, with none of the implications possible to reverse, and $ \mathsf{Exp}$ referring to the fragment of induction needed to define exponentiation. This is discussed in the answer to the other question, relevant background on $\mathsf{Exp}$ is given in section 2 of [Sv] and section 4 of [Bu], and the issues related to the Ackermann interpretation and $\mathsf{Exp}$ are described in the most detail in section 7 of the Kaye and Wong paper.
The above is mostly based on my understanding of the following sources:

*

*the answer to the other question,

*[Sv] On Strong Fragments of Peano Arithmetic by Vitezslav Svejdar, see here (archived)

*[Bu] First-Order Proof Theory of Arithmetic by Samuel Buss, see here (archived)

*[PK] $\Sigma_n$-Collection Schemas in Arithmetic by J.B. Paris and L.A.S. Kirby (1978) Studies in Logic and the Foundations of Mathematics, 199–209. doi:10.1016/s0049-237x(08)72003-2

*[KW] On interpretations of arithmetic and set theory by Richard Kaye and Tin Lok Wong (2006), see here (archived)

Obviously any errors are my own original work.
