Dedekind infinite set implies axiom of infinity in Kripke-Platek set theory

70 Views Asked by At

I'm referring to this version of Kripke-Platek set theory minus axiom of infinity. Let $S$ be a Dedekind infinite set, and $f\colon S \to S$ be an injection with $f(S) \neq S$. A proof I know picks $s \in S \setminus f(S)$ and constructs function $g(n) = f^n(s)$ by recursion, and use replacement to obtain $\omega = g^{-1}(S)$.

Recursion is available in $\mathsf{KP}$, and the resulting function is $\Delta_1$. $\mathsf{KP}$ can prove $\Sigma_1$-collection and $\Delta_1$-separation. If $\mathsf{KP}$ had $\Sigma_1$-separation, $\operatorname{ran}(g)$ would be a set hence $\omega$ could be obtained by $\Sigma_1$-collection. But $\Delta_1$-separation doesn't seem enough to prove $\operatorname{ran}(g) \subset S$ is actually a set. How could I prove that Dedekind infinite set implies axiom of infinity?