= Solution
Use the <bounded successor characterization of finite ordinals>. Let $\operatorname{Ord}(x)$ assert that $x$ is transitive, each of its members is transitive, and any two members are equal or comparable by membership. This is a bounded <first-order formula>; <foundation> makes its linear membership order well-founded, so it is precisely the <Von Neumann ordinal> predicate. Define
$$
\operatorname{Succ}_0(x)\quad\Longleftrightarrow\quad
x=\varnothing\ \lor\ (\exists y\in x)(\forall z\in x)(z=y\ \lor\ z\in y),
$$
and put
$$
\boxed{\operatorname{Nat}(x)\quad\Longleftrightarrow\quad
\operatorname{Ord}(x)\ \land\ \operatorname{Succ}_0(x)\ \land\
(\forall y\in x)\operatorname{Succ}_0(y).}
$$
For an <ordinal>, having a greatest member $y$ says exactly $x=y\cup\{y\}$. The displayed definition makes no reference to an infinite <inductive set> or to $\omega$; all quantifiers are bounded within the candidate and its members. Occurrences of $x=\varnothing$ can also be expressed as $(\forall u\in x)\,u\ne u$, so no unbounded quantifier is hidden in empty-set notation.
Every usual <natural number> satisfies this predicate, by induction: it is a <finite ordinal>, and every nonzero initial segment is a successor. Conversely, suppose an <ordinal> $x$ is not a usual <natural number>. <Ordinal> comparability gives $x\ge\omega$. If $x=\omega$, it has no greatest member, contradicting $\operatorname{Succ}_0(x)$. If $x>\omega$, then $\omega\in x$ has no greatest member, contradicting the corresponding bounded requirement on members of $x$. Hence $\operatorname{Nat}(x)$ holds exactly for the usual <natural numbers>. The <axiom of infinity> and <separation> therefore collect this class as the usual <set> $\omega$. This is a bounded definition of membership in the natural-number class; it does not claim that the <infinite set> $\omega$ itself can be produced without the <infinity> axiom.
Back to article page
