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?
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.