Is the Subset Axiom Schema in ZF necessary?

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.

1. Are the subset axioms necessary?
2. Is there a way to remove reference to a defining formula so that every subset of a given set is a set?
3. 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?
-
"Subset of" is an abbreviation for "is a set and each of its elements is an element of". So the Subset Schema is really about what subcollections are sets; "if T is a subset then it is a set" is a tautology. The point of the Power Set axiom is not that the elements of P(S) are sets, but that there is a set whose elements are exactly the subsets of S. –  Arturo Magidin Aug 13 '10 at 17:51
In response to 3. The subset axiom schema says we can make sets by finding all elements of another set that satisfy a predicate. It doesn't "allow only" these subsets because it doesn't say that there aren't other types of subset as well. –  Dan Piponi Aug 13 '10 at 18:14
The subset axioms do require the subsets to be definable by a formula. I know it is not an "if and only if" statement. I know that there may be other subsets. –  L. Blackburn Aug 15 '10 at 15:57

The subtle point you are speaking about is exactly the difference between first order logic and second order logic. In first order logic, we quantify only over objects in the universe. In second order logic, we can quantify also over subcollections of the universe. ZFC is a first order theory.

Note that the ZFC subset axiom is not saying that every subset of a set is describable in the way you mention. Rather, it is making the much milder claim that if we can describe a subset, then it is a set. And this seems totally unobjectionable.

You evidently want to consider a stronger version of the axiom, which says somehow that all the subcollections that exist anywhere are also sets. This is a second order assertion, since it is quantifying over subsets of the universe. This second order subset axiom, however, is not expressible in first order logic. The reason is that any model with an infinite set, satisfying the second-order subset axiom would have to uncountable, since it would truly contain all the subsets of its sets. Thus, there could be no countable models of your theory, which would violate the Lowenheim Skolem theorem if the axiom were expressible in first order logic.

Nevertheless, it is natural to look into the possibilities of second order ZFC, and this is studied in set theory. It turns out that the models of your second order ZFC (using second order Replacement also) are exactly the same as the universes known as $H_\kappa$ for an inaccessible cardinal $\kappa$, one of the large cardinal notions. These models are also known as the Grothendieck universes, and are used throughout category theory as a convenient way of formalizing the large/small distinction.

It might be a good exercise for a beginner in this area to prove that if $\kappa$ is a (strongly) inaccessible cardinal, then the collection $H_\kappa$ of sets whose transitive closure has size less than $\kappa$ is a model of second order ZFC. When $\kappa$ is inaccessible, then this universe $H_\kappa$ is the same as $V_\kappa$ in the Levy cumulative hierarchy.

Finally, let me remark that some might find it to be somewhat incoherent to propose a second-order theory as the main axiomatization of set theory. The purpose of the axiomatization, after all, is to set forth certain minimal bedrock principles that the set concept should obey, but if we make these principles second-order, then we would seem to need a prior concept of set to interpret them. That is, a second order logic only makes sense in the context of a larger set-theoretic background. So it wouldn't seem to work foundationally to provide such an axiomatization as the principal axiomatization of set theory.

-
Thank you for the excellent response. I'm particularly intersted in the idea that second-order axioms would need a prior concept of set to interpret them. But doesn't the notion of a model (as a set with a binary predicate) of the first-order axioms also require a prior concept of set? When you talk about a countable model of ZFC aren't you assuming a prior concept of set? –  L. Blackburn Aug 15 '10 at 16:02
Yes, but we undertake model theory only inside a set-theoretic background. That is, once having founded our set theory (in first order), we can now use it to analyze other theories, including both first and second order theories. –  JDH Aug 15 '10 at 19:33
@L. Blackburn: I think that it is important to understand that Gödel's completeness theorem works for first order logic, but not for higher order logic. There is no associated proof theory for second order logic. –  George Lowther Oct 9 '11 at 21:38
When you say that in $\kappa$ is inaccessible then $H_\kappa$ is the same as $V_\kappa$, you mean the von Neumann hierarchy, not Levy's hierarchy. Right? –  Asaf Karagila Feb 29 '12 at 11:45
Yes, it should say von Neumann hierarchy. –  JDH Feb 29 '12 at 14:54

So, maybe I should write this as a response. So, let's take the notions in order. First, I will reserve the word "set" for objects in the theory, and use "collection" for the more intuitive notion.

Note that "$A$ is a subset of $B$" is an abbreviation for two statements: (i) $A$ is a set; and (ii) for every $x$, if $x\in A$ then $x\in B$. So "if $A$ is a subset of $B$ then $A$ is a set" is a tautology of the form $P\wedge Q\Rightarrow P$.

As user80 points out, you are misinterpreting the Subset Axiom schema slightly; it does not state that only those subcollections which you express as ${a\in A: \phi(a)}$ are sets (it is not an "if and only if" statement). It 'merely' states that all those are sets, leaving open that perhaps there may be "other" subcollections that may also be sets. So in your analogy, it would be like saying that if you can write down a formula for a function from $X$ to $Y$ then the result will certainly be a function, but it does not tell you that you get a function only if you can write down a formula: just that writing down a formula is a way of getting a function.

It it "necessary"? Well, it is necessary if you wish to be able to construct new sets by specifying certain elements from something that you already know to be a set. Otherwise, you'll have no warrant for saying that such objects are sets, only that they are collections. The Axiom of Separation/Subset is about one way to take a set, pare it down, and get a set.

As to the axiom of the power set, you are again misinterpreting it. It's not that the axiom of the power set says that subsets of S are sets; that's already in the notion of "subset". Rather, the Power Set Axiom tells you that you have a set whose elements are the subsets of your given set $S$. It guarantees the existence of a set which is "one level up" from $S$, in the sense that its elements are subsets of $S$. From the Axiom of Pairs and other issues it is not hard to show that if you have a finite collection of things that you know are sets, then there is a set whose elements are exactly those in your original collection (that is, it allows you to pull together those things and put them in a set). But what if you have an infinite number of things that you know are subsets of $A$? In order to make sure you have a set that contains all of them as elements, you need something beyond knowing that they are sets; that's where the Axiom of the Power Set comes in: it gives you an overset (which is a set) in which all these objects will be elements.

How does Power Set interact with Separation/Subset? Anything you obtain using Separation will necessarily be an element of the Power Set. It does not say that those are the only things in the power set, just that those are guaranteed to be in the Power Set.

-
Thank you for this clear response. I did not mean to imply that the only subsets are those given by the subset axioms. The main point of my question, which I feel has been partially answered by JDH, is why are not all the elements of the power set of a given set not required to exist as sets? For example, ZFC has a countable model. But the axiom of infinity guarantees an infinite set (like N) and then we have P(N), which we can prove is an uncountable set. So, not every element of P(N) has a corresponding element of the countable model. Seems strange. –  L. Blackburn Aug 15 '10 at 16:13
Okay, again you seem to be confusing the notion of "set" (within the model) and an intuitive notion of what "set" might be; because you are using the same word for both, this leads to confusion. The last part of your comments is related to Skolem's paradox. But "not all elements of the power set of a given set not required to exist as sets" is false. Every element of the power set of S is required to be a set in your model. Again, I think you have the implications backwards. –  Arturo Magidin Aug 15 '10 at 20:37
I don't understand your response. My point is that ZFC guarantees the existence of an infinite set N and then guarantees the existence of P(N), which one can prove has uncountably many elements. But ZFC has a countable model, (A,e), and A isn't big enough so that there is an element of A to play the role of each element of P(N). I know there is no logical contradiction, but this leads me to think that the first order axioms of ZFC are not strong enough to capture what we mean by "set" because they allow these countable models. If I'm being obtuse, I apologize. –  L. Blackburn Aug 24 '10 at 21:15

Once upon a time, mathematicians used "naive set theory": for any logical predicate, there was a set of all objects satisfying that predicate: "unrestricted comprehension". The ability to do this was one of the main features of set theory -- the ability to gather all of the objects in a class up into a set, so that you could reason about the set.

Of course, the famous contradictions were discovered (e.g. Russell's paradox), and that put an end to naive set theory.

Now, comprehension was a rather important feature of set theory, and Zermelo kept it when he came up with his axioms for set theory. The trick was to replace unrestricted comprehension with restricted comprehension. Zermelo set theory uses a limited number of "safe" operations (e.g. pairs, power sets, unions) to build up sets, and then restricts the use of comprehension to merely selecting out elements of sets -- i.e. the axiom (scheme) of subsets -- rather than allowing it to collect elements out of the entire universe.

This turns out to be powerful enough to do mathematics, and so Zermelo set theory (and eventually ZFC) became a foundation of mathematics.

In the very closely related NBG set theory, the axiom of subsets simply becomes "If $\Phi$ is a class, and $S$ is a set satisfying $\Phi \subseteq S$, then $\Phi$ is a set." (or there is a set with the same elements as $\Phi$, depending on technical convention)

-