ZF minus Axiom of Infinity $\vdash$ If there exists a set that is not finite then $\Bbb N$ exists

Question

There are elementary definitions of a finite set that do not involve the natural numbers; see this wikipedia link or this stackexchange post. To be exact, take the definition to be

Paul Stäckel: The set $S$ is said to be finite if it can be given a total ordering which is well-ordered both forwards and backwards. That is, every non-empty subset of S has both a least and a greatest element in the subset.

With this context,

If there exists a set that is not finite then $\Bbb N$ exists

My work

I do not have the tools to answer this question, but my guess is that it is true.

Answer 1

Here's a proof that doesn't use the von-Neumann hierarchy (and therefore works even if you additionally remove the axiom of foundation):

Be $I$ your infinite set, and $P$ its power set (which according to the axiom of power set is also a set). Then according to the axiom of specification, the set $F$ of all finite subsets of $I$ is also a set (it's the set of all finite members of $P$).

Now you can define a class function that maps every finite set to its cardinality. Note that we don't care about what it does to infinite sets, as we'll apply it to $F$, which by definition only has sets of finite cardinality. We might e.g. map all infinite sets to the empty set. Therefore we don't need to bother with generally defining cardinality (which with neither choice nor foundation would be a problem); having a representation of each natural number is enough. The finite von-Neuman ordinals work fine for that.

According to the axiom of replacement, since we have a class function that maps each finite set to its cardinality, the set $N=\{|x|:x\in F\}$ exists as well. In words, $N$ is the set of cardinalities of finite subsets of $I$.

Clearly $N$ only contains natural numbers (because the cardinality of a finite set is a natural number).

Now assume that there exists a natural number that is not in $N$. Then because the natural numbers are well-ordered, there is a minimum natural number $n$ that is not in $N$. Clearly $n>0$ because the empty subset is subset of every set, in particular of $I$. Therefore by definition of $n$, $I$ has a subset $S$ of cardinality $n-1$.

Obviously $S\ne I$, because $S$ is by definition finite, while $I$ is by assumption infinite. Thus $S$ is a proper subset of $I$. But then there exists an element $x\in I\setminus S$, and therefore the set $S\cup\{x\}$ is also a finite subset of $I$, with cardinality $n$, in contradiction to the assumption that $I$ had no subset of cardinality $n$.

But if $N$ is a set that contains all natural numbers, and only natural numbers, then $N$ is the set of natural numbers. And we have previously shown that the set $N$ exists

Therefore the set of natural numbers exists. $\square$

Answer 2

Proposition. If $x$ is finite, then every subset of $x$ is finite.

Proof. Trivial using the given definition. $\square$

Proposition. If $x$ is finite, its power set is finite as well.

Proof. Fix a well-ordering on $x$ witnessing its finiteness, and define a linear ordering on $\mathcal P(x)$. Now show that this linear ordering is in fact well-ordered and co-well-ordered. $\square$

Now, even in $\sf ZF-Infinity$ we can prove that the von Neumann hierarchy exists and exhausts the universe. So $\omega$, and $V_\omega$ as a consequence, are definable classes, and we just don't know yet if they are sets.

Claim. If $x\in V_\omega$, then $x$ is finite.

Proof. By induction, $V_n$ is finite for every $n<\omega$, so every $x\in V_\omega$ is a subset of a finite set. $\square$

Theorem. If there is an infinite set, then $\omega$ is a set.

Proof. By the claim, an infinite set cannot be in $V_\omega$. Therefore it lies in some $V_\alpha$ for $\alpha>\omega$, and therefore $\omega$ is a set. $\square$