Equivalence of two formulations of the axiom of infinity

Question

I'm introducing Zermelo–Fraenkel axioms in a minimal way: only what is actually needed to introduce real numbers.

In this respect I noticed that I do not need the axiom of foundation nor the axiom of replacement. Instead I define functions as soon as possible, so it is natural to define an infinite set as a set $X$ such that there exists $f\colon X\to X$ injective, but not surjective (Dedekind-infinite) before having natural numbers.

So my statement of the axiom of infinity is: "there exists a (Dedekind-)infinite set". The usual axiom of infinity requires instead the existence of the first infinite ordinal $\omega$. If I have $\omega$ it is not difficult to prove that $\omega$ is Dedekind-infinite.

On the other hand it seems to me that without the replacement axiom it is possible that an infinite set exists even if $\omega$ does not exist. This makes sense to me: why should I suppose the existence of $\omega$ if I don't really need it?

However, this answer states that the equivalence of the two formulations can be obtained only with extensionality, pairs, unions, specification and powers. How can this be achieved?

Answer 1

This is not true. Consider the set $X=\{\emptyset,\{\emptyset\},\{\{\emptyset\}\},\{\{\{\emptyset\}\}\},\dots\}$. Let $M$ be the closure of $X\cup\{X\}$ under the operations of taking subsets, forming pairs, forming power sets, and taking unions. Then $M$ will be a transitive model of the Extensionality, Pairing, Union, Specification, and Powerset axioms (and also Regularity and Choice), as well as your version of Infinity since there is a non-surjective injection $f:X\to X$ given by $f(x)=\{x\}$. However, I claim that $\omega\not\in M$. To prove this, just note that for every $x\in M$, the transitive closure of $x$ contains only finitely many elements of $\omega$ (since this is true of $X\cup\{X\}$ and is preserved by all the operations we close it under to form $M$).

Answer 2

This may be an alternative approach: Let $X=\{\emptyset,\{\emptyset\},\{\{\emptyset\}\},\{\{\{\emptyset\}\}\},\ldots\}$. Define recursively $$ f(x)=\begin{cases}\emptyset&\text{if }x\in X\setminus\{\emptyset,\{\emptyset\}\}\\\{\,f(y)\mid y\in x\,\}&\text{otherwise}\end{cases}$$ and let $M$ be the class of sets $x$ such that $f(x)$ is hereditarily finite. Then $M$ is closed under Pairing, taking subsets (hence under Specification), Union, and Powerset. Clearly $X\in M$ and $\omega\notin M$ and we have the injective non-surjective map $s\colon X\to X$, $x\mapsto \{x\}$.

Incidentally, (using Kuratowksy pairs) its graph $\{\,\langle x,s(x)\rangle \mid x\in X\,\}$ is also $\in M$ because for almost all $x\in X$, we have $$ f(\langle x,s(x)\rangle)=f(\{\{x\},\{x,s(x)\}\})=\{f(\{x\}),f(\{x,s(x)\})\} =\{\emptyset,\{f(x),f(s(x))\}\} =\{\emptyset,\{\emptyset,\emptyset\}\}=\{\emptyset,\{\emptyset\}\}$$