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 ?

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.
