Suppose I have some characterization of the natural numbers $N$ in a first-order system under ZF. To be precise, I have $N = \lbrace n: \forall w:( w\space is\space inductive) \rightarrow n \in w \rbrace $ and a predicate $P[x]$ such that $P[0]$ and $P[x] \rightarrow P[succ[x]] $.
Therefore, $n \in N \rightarrow n \in P[x]$, but I'd also like to show that $ n \in P[x]\rightarrow n \in N $.
I'm using Von Neumann ordinals ($succ(x) := \lbrace x \rbrace \cup x$), and I believe that the characterization is "sharp": $P[x] \equiv (x=0\vee \exists y:x=succ(y)) \wedge \forall y\in x:(y=0 \vee \exists z \in y : (y=succ(z)\wedge z \in x))$
Noting $x \notin N \wedge \exists y:x=succ(y) \rightarrow y \notin N$, and applying a first order induction "downward" to show some property $\phi$ over the $y : y \in x$ for some $x$ such that $P[x]$, I can construct the set for which $ \neg \phi[x] $, and reach a contradiction under the assumption $\neg \phi[0]$ by showing that set inductive, and therefore $\exists n : (n \in N \wedge \phi[n]) \rightarrow \phi[0]$
Obviously this will not be useful for $\phi[x] := x \in N$, however, since there is no such $n \notin N$!
So, is it possible to do this sort of thing? How does one proceed? Or are there models which have bigger $\lbrace x:P[x]\rbrace$ than $N$?
The alternative is to carry around the "$x \in N$" clause in sets defined by specification, such as the inductive restriction of $N$ by $P[x]$, $\lbrace x : x \in N \wedge P[x] \rbrace$ obtained to reach $n \in N \rightarrow P[n]$ above. Which is not so bad, but $N = \lbrace x : P[x] \rbrace$ is cleaner.
As you note x∉N∧∃y:x=succ(y) → y∉N. P has the stronger property
P[x] → x=0 ∨ ∃y:x=succ(y) ∧ P[y].
Combining these and defining ϕ[x] := x∉N ∧ P[x], we get
ϕ[x] → ∃y:x=succ(y) ∧ ϕ[y]
If there exists x such that ϕ[x], let C = {y ∈ x : ϕ[y] ∧ y ⊂ x}.
C is non-empty as it contains the predecessor of x, but contradicts regularity as
$y \in C$ → ∃z:(y=succ(z) ∧ z ∈ $y \cap C)$
Hence there is no such x, and so P[x] → x∈N