Does all formula defines a set? A formula is a prediction. ZF system says that any formula defines a subset in a set. But the truth value of a formula is gotten by a proof not by a calculation. That means there doesn't exist a algorithm (a determined steps) that is able to get the truth value of a formula. So, the truth value of some formula could be unknown, at least at the moment the formula is talked about. Does such a formula defines always a set ?
For example, the Goldbach's conjecture G that says any even number bigger than 2 can be the sum of 2 primes. G is neither proved TRUE nor proved FALSE. So, its truth value is unknown till now. G can be written as a formula in ZF system (easier if +, * are defined in ZF before). The Fermat's grand theorem F was proved recently (less than 20 years). F can also be written as a formula in ZF. Now, considering the following formula:
P(x) = ((x=1)⋀(G))⋁((x=2)⋀(F))
P(x) is a formula. But can P(x) define a subset S in N (set of integers) ? If yes, 1∈S ? 2∈S ? 2∈S is known TRUE now but it was unknown 20 years ago.
The real question is perhaps whether it makes sense to define a set for which it's unable to determine an element belongs to it or not ?
 A: Why are you going as far as $\sf ZF$?
Take any incomplete theory $T$ such that there are two formulas $\varphi_a$ and $\varphi_b$ that $T$ proves define unique elements ($a$ and $b$ respectively), and that they define distinct elements.
Let $\psi$ be a statement which is neither provable nor refutable from $T$ and a now consider the element definable by $(\varphi_a\land\psi)\lor(\varphi_b\land\lnot\psi)$. Certainly it is either $a$ or $b$, but which one? We cannot say.
And such $T$ are abundant throughout mathematics. Most arithmetical theories like $\sf PA$ (Peano arithmetic), $\sf Q$ (Robinson arithmetic), all sort of weakening and strengthening of these and so on and so forth. If they prove that $0\neq1$, then you can always define an element which is $0$ if $\psi$ holds and $1$ otherwise.
Moreover, this has nothing to do with being able to determine if something is provable or not. Even if $T$ has some codification of first-order logic, and $T$ proves that $\psi$ is independent of $T$, the only thing that really matters is that $T$ does not prove or disprove $\psi$ for this to work.
So why is this fine? It's fine because first-order logic separates syntax (proofs, definitions) from semantics (truth values in a given model). So we can write things and later find out that we are having a hard time evaluating them. It's not as bad as it sounds, really.
A: It's normal that for a set S and some object b, b∈S could not be decided. So, all formula defines a set leads to this situation has no problem.
If for any object b, b∈S can be decided, S is called a recursive set or decidable set. All set is not recursive (otherwise, set theory covers too narrow area).
Sometimes, the content of a set S is generated by a function (it could be say also that it's enumerated or listed by the function). For example, the serial produced by a pseudo random number generator f(n) with the same seed: S={f(0),f(1),f(2),...,f(n),...}, to decide, for a specific number k, k∈S is sometime impossible (depends on f(x), and assume f(n) is not limited by the number of digits it can have). This kind of set is called recursively enumerable.
