I am learning the axioms of Zermelo-Fraenkel (ZF) set theory.
One axiom schema basically says that given any set S and any formula phi(x), there is a set T consisting of all those elements x of S such that phi(x).
I find this axiom schema unsatisfying because it only guarantees that subsets of S definable by a formula are really sets. It's like saying that a function from X to Y only exists if you can write down a formula for it rather than just allowing arbitrary single-valued subsets of X cross Y. Is there a way in the language of ZF to say "given a set S, if T is a subset of S then T is a set?"
Related is the power set axiom. Given a set S, there is a set P(S) consisting of exactly all the subsets of S. But in ZF the objects of the theory are sets (no urelements). Everything is a set. So, the elements of P(S) are all sets. Doesn't this mean that every subset of a given set S is a set? If so, why the need for the subset axioms?
I can anticipate some difficulty. I want to say that "if x is a member of P(S) then x is a set," but I cannot express the predicate "is a set" in the language of set theory, and strangely enough there is no need to since everything is a set! I attempted:
"(for all S)(for all x)[x subset S --> (there exists y)(x = y)]"
where "x subset S" is an abbreviation for "(for all z)[z in x --> z in S]."
But this attempt is silly because when I say "for all x," x is automatically a set and there is no need to say it is a set.
I'm confused.
- Are the subset axioms necessary?
- Is there a way to remove reference to a defining formula so that every subset of a given set is a set?
- If the answer to 1 is "yes" and the answer to 2 is "no" then why is set theory so weird as to allow only definable subsets on the one hand and yet allow for a set of all subsets on the other?