Is there a bounded-quantifier formula in ZF without Foundation that defines the naturals? Does there exist a first-order set-theoretic formula $\phi(x)$ using only bounded quantifiers such that, in ZF without assuming the Axiom of Foundation/Regularity, $\phi(x)$ is true if & only if $x$ is (the von Neumann construction of) a natural number?  The only predicates for defining the naturals that I can find are variations on $\phi(x) := \forall I(\emptyset\in I \land (\forall y\in I)(y\cup\{y\}\in I) \to x\in I)$ (which isn't bounded) and $\phi(x) := x=\emptyset \lor ((\exists k\in x)(k\cup\{k\}=x) \land (\forall y\in x)(y=\emptyset \lor (\exists k\in x)(k\cup\{k\}=y)))$ (which needs not be satisfied by only the naturals in non-well-founded theories; e.g., the Quine atom satisfies this predicate).
 A: I don't think this is possible, for the following reason:
The characteristic property of a formula with bounded quantification $\phi(x)$ is that the truth of $\phi(x)$ for some $x$ in a model $M$ depends only on how the membership relation behaves on the transitive closure of $x$, not on what is in the rest of the model.
Therefore, if we can find two models $M$ and $N$ of $\text{ZF}-\text{Reg}$ with elements $x\in M$ and $y\in N$ such that $x$ is a natural in $M$ but $y$ is not one in $N$, yet the transitive closures of $x$ in $M$ and $y$ in $N$ are isomorphic, then there cannot exist a bounded-quantifier formula that defines the naturals.
Here's a slightly convoluted way to do that (assuming, of course, that ZF is consistent):
Let $N$ be a model of $\text{ZF}-\text{Reg}$ with Aczel's anti-foundation axiom.
Inside $N$, carry out the usual compactness argument that there is a model $M$ of ZF which contains a non-standard integer $x$.
Still working inside $N$, look at the membership structure of the transitive closure of $x$. Because of the anti-foundation axiom, $N$ contains some $y$ whose transitive closure is exactly isomorphic to $x$. But $y$ cannot be a natural in $N$, because $(M,x)$ was explicitly constructed such that $x$ would be a non-standard natural when seen from $N$.
Now, even though $(M,x)$ was constructed inside $N$, we can easily lift it out of $N$ to become a model that lives in our universe side-by-side with $N$. It is still a model of $\text{ZF}-\text{Reg}$ (because everything is first-order, so the conditions for being a model inside $N$ guarantee that the lifted model is a model at our metalevel too), and similarly the isomorphism between $\bar x$ and $\bar y$ that exists in $N$ induces an isomorphism at the metalevel. This completes the proof.
A: The method below fails because we need at least one unbounded quantifier in order to obtain the power set of $x$, however I am keeping this answer here so that others attempting to solve this problem will have a starting point.
To define $\omega$ we either need to find a way to express its minimality as an inductive set, or its minimality as an infinite ordinal; or we need to find a way to define a finite ordinal and write $\omega$ as the set of finite ordinals.


*

*$x$ is transitive, that is every element of an element of $x$ is also an element of $x$.

*$x$ is linearly ordered by $\in$, that is given two distinct elements of $x$, one is the element of the other.

*$x$ is inductive, that is the set with no elements is in $x$, and for every $k$, element of $x$, there is another element of $x$ which is equal to $k\cup\{k\}$.

*$x$ is well-founded, that is for every element of $\mathcal P(x)$ which is non-empty there is a $\in$-minimal member.

*$x$ contains only finite sets, that is every $k$, element of $x$, has the property that every collection of subsets of $k$ is either empty or contains a $\subseteq$-maximal element.


Note that I use the power set twice, once for well-foundedness and one for finiteness. I also use Tarski's definition of finite (Dedekind's definition would also be applicable and would require quantification over elements of $\mathcal P(x\times x)$, so we use power sets again as well as products).
It should be remarked that finite-ness and well-foundedness are both second-order properties, i.e. there are models of ZF in which there are uncountably many [internally] finite sets. Spooky but true. It seems a bit unlikely to find a way to define them without appealing to unbounded quantifiers, or at least bounding the quantifiers at the power set or so.
A: This is too long to write in comments so let me note here that if we can express "$x$ is an ordinal" as a bounded formula $\mbox{ord}(x)$ over ZF-Foundation then we can also express 
"$x$ is a natural number". First define (as in Jech, 3rd ed, p. 164) "$x$ is a limit ordinal" as
$$ \lim(x) \mbox{ iff } \mbox{ord}(x) \wedge (\forall u\in x) (\exists v\in x) u\in v.$$
Now
$$x \mbox{ is a natural number  iff } \mbox{ord}(x) \wedge (\neg \lim(x) \vee x=0) 
\wedge (\forall u\in x) (u=0 \vee \neg\lim(u) ).$$
So if it is the case that "$x$ is a natural number" is not equivalent to a bounded formula over ZF-Foundation then neither
is "$x$ is an ordinal". Since the usual definition of "$x$ is an ordinal" employs "$x$ is well-founded", it also follows 
that "$x$ is well-founded" is not equivalent to a bounded formula over ZF-Foundation.
$$ \mbox{ }$$
Note: If the axiom of foundation holds, then it is easy to define "$x$ is an ordinal" as a bounded formula over ZF. There are different ways to do it:
$$\mbox{ord}(x) \:\: \mbox{ iff } \:\: x \mbox{ is a transitive set } \wedge  x \mbox{ is totally ordered by } \in.$$
Or
$$\mbox{ord}(x)  \:\: \mbox{ iff } \:\:  x \mbox{ is a transitive set } \wedge \: \in \! \mbox{ satisfies trichotomy on }x.$$
Or
$$\mbox{ord}(x)  \:\: \mbox{ iff } \:\:  x \mbox{ is a transitive set } \wedge  (\forall u \in x)(u \mbox{ is a transitive set}).$$
The above equivalences are in Kunen 2011, p.34, p.38, p.39.
