Construction of natural numbers in ZF/ZFC without class predicates. I'm told by some websites that it's possible to formally construct the naturals in ZF without recourse to either predicates involving classes ("all inductive sets", yuck) or some sort of "intuitive number system" provided outside of the logic.
The basic idea using the Von Neumann ordinal construction is to do get an inductive set (ie. $0\in N_{+} \wedge \forall x:x\in N_{+} \rightarrow (\lbrace x \rbrace \cup x) \in N_{+}:$), via $Infinity$, and then to pick out just $N$ from it  using $Specification$ with the predicate restriction $\forall x: (x=0 \vee \exists r:x=(\lbrace r \rbrace \cup r):) \wedge \forall y:y\in x \rightarrow (y=0 \vee \exists r:y=(\lbrace r \rbrace \cup r) \wedge  y \in x:):$ 
It "makes sense" to me - in my head where the numbers already are I can resort to induction and see that those are exactly the ordinals, and they're all in $N_+$. But, I can't seem to make the proof work with just the objects I already have (the ZF axioms).   It seems clear that it requires $Regularity$, but I can't find a proof online or in any of my books.
Can someone point me to one or provide a rough proof sketch?
 A: The standard route goes something like this:
Let $A$ be the inductive set that the Axiom of Infinity guarantees us. Then using Separation let
$$ \omega=\{n\in A\mid \forall x: x\text{ is inductive} \to n\in x \}$$
One can then easily prove that $\omega$ is inductive and is a subset of every inductive set.
In particular an inductive subset of $\omega$ must be $\omega$ itself, so we have a set of naturals that satisfies the usual second-order induction axiom.
Is this definition what you denounce as "predicates involving classes"? If the unrestricted quantification on $x$ offends you (which it shouldn't) you can replace it by $\forall x\in\mathcal P(A)$. You then need to do slightly more footwork if you still want to prove that $\omega$ is a subset of an arbitrary inductive set $B$, but that's not hard: By definition $\omega$ is a subset of every inductive subset of $A$, and then we can prove that $A\cap B$ is inductive, so $\omega\subseteq A\cap B\subseteq B$).

It looks to me like your your predicate does pick out exactly the naturals once you have an $A$ that contains all of them, assuming Regularity is true (otherwise there are counterexample models). However, you'll need to prove that induction works on the $\mathbb N$ you get. In order to apply Regularity to show this, the natural strategy would be to assume that there's an inductive $B\subsetneq \mathbb N$ and let $x\in\mathbb N\setminus B$ and construct the set $$\bar B=\{x, f(x), f(f(x)), f(f(f(x)),\ldots\}$$ where $f$ is the predecessor function (and this set would then contradict Regularity).
However, constructing $\bar B$ requires Replacement applied to the functional relation $n\mapsto f^n(x)$, with a domain that needs to behave sufficiently much like $\omega$ that we must already have constructed a workable $\omega$ somehow. For example, it would seem that we need to be able to use induction on the domain in order to argue that $\bar B$ and $B$ are disjoint.
The outcome of this is that it is formally possible to go the way you sketch, but it looks like you would have encountered the naturals (or something very much like them) anyway along the way, and the rest of the exercise is then more or less a detour.
A: One can indeed avoid the "Axiom of Infinity" to define the notion of a natural number. One predicate that is satisfied precisely by (von Neumann) natural numbers is $\eta$ defined as follows:
\begin{align*}
    \eta(x) :=
        & (x=\emptyset \vee \exists y(x=S(y))) \\
        & \wedge \forall z(z\in x \rightarrow (z=\emptyset \vee \exists w(w\in x \wedge z=S(w)))) \\
        & \wedge \forall u((u\subset x\wedge u\neq\emptyset)\rightarrow \exists v(v\in u\wedge v\cap u=\emptyset))
\end{align*}
here:

*

*$a\subset b:= \forall p(p\in a\rightarrow p\in b)$

*$a\neq b:=\neg(a=b)$

*$S(x):=x\cup\{x\}$.

This predicate is essentially the same as the one suggested in the question of the OP. The last (added) clause says that the "Axiom of Foundation" holds for subsets of $x$. One may choose to require it to hold for all sets, which is naturally a stronger hypothesis.
One easily shows that:

*

*$\eta(\emptyset)$ holds.

*$\eta(x)\rightarrow\eta(S(x))$ holds.

Suppose $\kappa$ is some predicate for sets such that:

*

*$\kappa(\emptyset)$ holds.

*$\kappa(x)\rightarrow\kappa(S(x))$ holds.

For example, $\kappa(x)$ could be the predicate that says that $x$ is a finite ordinal.
Claim: $\forall x(\eta(x)\rightarrow\kappa(x))$
This shows that $\eta(x)$ is another way of stating that $x$ is a finite ordinal. The following proof shows that $\eta$ provides a way to "pick out" natural numbers without having already proved all their properties. We also do not need to have constructed the set of all naturals.
To prove the claim, we assume $\eta(x)$ and try to prove that $\kappa(x)$ holds. Since $\kappa(\emptyset)$ holds, we also assume $x\neq\emptyset$.
We examine the set $z=\{y\in x:\neg\kappa(y)\}$.
Since $x\neq\emptyset$ the first clause of $\eta(x)$ says that $x=S(y)$; which also means $y\in x$. Thus, if we show that the set $z$ is empty, then $y\in x$ and $\neg(y\in z)$. This means that $\kappa(y)$ holds. Hence, $\kappa(x)=\kappa(S(y))$ holds.
Note that $\neg(\emptyset\in z)$ since $\kappa(\emptyset)$ holds.
If $z\neq\emptyset$, then by the last clause in $\eta(x)$ (or by the "Axiom of Foundation"), there is an element $v\in z$ such that $v\cap z=\emptyset$. Since $v\in z$, we have $v\neq\emptyset$ and $v\in x$. By the second clause in $\eta(x)$ we see that $v=S(u)$ for some $u\in x$. Now, $u\in v$ so $\neg(u\in z)$. Thus, $\kappa(u)$ holds, which means $\kappa(v)=\kappa(S(u))$ also holds which contradicts $v\in z$. The source of this contradiction is our assumption that $z\neq\emptyset$. Thus, we see that $z=\emptyset$.
