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.
