Bxdty

The axioms of ZF define what a set is by:

1. 
   $omega$ is a set


2. If $x$ and $y$ are sets, then ${x, y}$ is a set


3. If $x$ is a set, then $bigcup x$ is a set


4. If $x$ is a set, then $mathcal{P}(x)$ is a set


5. If $x, y_1, ..., y_n$ are sets and $P$ is a statement free variables $x, y, z_1, ..., z_n$, then ${z in x : P}$ is a set

and also defines equality between sets by the axiom of extensionality.

But I don't understand why we can't just add "nothing else is a set" as an axiom to the list, as we usually do when defining a certain mathematical object.

Wouldn't adding that axiom solve the problem of some statements being independent? If we can't prove a set exists, then it means it can't be produced using the rules listed above, so it's not a set.

It's not clear why we need to. One reason we "can't" has to do with a technicality. ZF is a theory in "first-order logic". Saying that nothing is a set except that which the axioms imply is a set is not a "first-order" statement, so if we tried to add it we'd no longer have a first-order theory. That would be too bad, because first-order logic works out a lot nicer than higher-order logics.

There's no way to say "nothing is a set except things that the axioms imply are sets" using just $forall$, $exists$ and $in$.

(In fact, the axioms don't quite say what you say they say! There's no mention of "is a set" in the actual axioms. What you say is maybe how one thinks off what the axioms mean, but in fact, for example the actual axiom (2) is $$forall xforall yexists z(forall t(tin ziff (t= xlor t= y))).$$The axioms talk about sets, not about what is or is not a set; adding "is a set" to the formalism makes it a totally different sort of thing.)

The approach of defining a recursive data structure $S$ by giving some rules for constructing members of $S$ and saying "anything constructed by these rules is an $S$ and nothing else is an $S$" is a shorthand for saying that $S$ is the intersection of all sets that are closed under the rules. This approach is usually used in contexts where the candidates for membership of $S$ are already known, so the intersection is over a well-defined set. E.g., if the rules are given by a grammar over some set of symbols, $S$ will be a subset of the set of all strings of symbols.

To apply this approach to a first-order axiomatization of set theory, you'd need some mechanism allowing the language of set theory to talk about itself, so that you could say in the language of set theory that the only sets are those that can described following your rules. This isn't impossible, but it would be technically tricky: the axiomatization would depend on something equivalent to a Gödel numbering of the language and you would have to presuppose some notion of the satisfaction relation in order to give meaning to the set comprehensions in your rule 5.

The end result is going to be unsatisfactory. In ZF, we can prove (1) that uncountable sets exist and (2) that the language of ZF is countable. Hence your modification of ZF in which all the sets are expressible by formulas in the language would be inconsistent. To regain consistency, you would have to weaken ZF. There is no obvious weakening that would achieve consistency and would respect the underlying intuitions behind ZF.