Vtyjkyuk

I'll try to make this as short as I can. I'm just beginning to read Thomas Jech's Set Theory (3rd Millenium Edition) where he starts with the axioms of ZFC. Pardon the naivete of my question that follows, but some of these axioms sound vague to me. Take the Axiom of Separation: If $P$ is a property with parameter $p$, then for any $X$, there exists a set $Y$ $= u in X : P(u,p)$.

The same with Axiom of Power Sets: For any $X$, there exists a set $Y$ of the subsets of $X$.

The key thing I have an issue with is that this "any $X$" is vague and does not help the reader make sense of the axioms. What is $X$ to be? It's not a trivial question when you consider the assertions these axioms make: namely, that the objects $Y$ in my two examples above are actually sets (and thus do not belong to the cesspool of proper classes that tend to breed those Russell-type paradoxes).

For example, in the power set axiom, since there are no restrictions on $X$, can I take $X$ to be a proper class? If so, this axiom tells me that the power set of $X$ (which has strictly larger cardinality than $X$ itself) is a set and not a proper class. How is that to be?

In ZFC the domain of discourse is all sets. So when we say 'for all $X$' we mean for all sets $X$. So the power set axiom can be written in more detail as "for every set $X$ there is a set $P(X),$ whose elements are all sets that are subsets of $X.$"

(What 'all' sets means is a different can of worms and varies from model to model. But in any event, proper classes are not sets by definition, so are not included. In fact they can't be directly expressed as objects in ZFC's language. Rather, they are talked about indirectly, via formulas. So a class is just a formula, whose extension may or may not correspond to a set.)

Edit (In response to your comments)

It is wrong to think of the ZFC axioms as 'defining what a set is' although I can see why you might be under that impression since most of the axioms essentially tell you how to define new sets from previously defined ones. Rather, the ZFC axioms define what a set theoretical universe is, in that a set theoretical universe is a collection of objects and a membership relation $in$ on those objects for which the axioms hold.

Although we certainly want such a theory to be consistent, and paradox avoidance is what motivated the restricted form of comprehension that ZFC has, it's also important to realize that ZFC makes some 'arbitrary' choices that have nothing to do with paradox avoidance. For instance, the axiom of extensionality implies that everything in our universe is a set and, for instance, there are no 'pure elements' (usually called urelements) that are not set-like in nature. (It does so by implying that the empty set is the only thing that doesn't contain anything else.) Also, the axiom of foundation guarantees that there are no strange sets that contain themselves, e.g. so-called Quine atoms obeying an equation like $x=x,$ which are not inherently paradoxical despite not being as natural as urelements and superficially smelling like Russell's paradox. It is useful since it implies that the universe of sets is arranged in a Von Neumann hierarchy The other axioms (including perhaps choice) are less arbitrary, in the sense that they formalize our intuition from naive set theory of what kinds of sets we should be able to define based on others.

It is also important to note that ZFC is not a full characterization of a unique universe of sets. For instance, you have probably heard that the continuum hypothesis is independent of ZFC and that the axiom of choice is independent of ZF. This means that there are models of ZF/C that differ on these questions, and thus we haven't uniquely specified a universe of sets.

(In fact we could have never hoped to do anything close to this in a first order theory, with results like Lowenheim-Skolem. And yet if we try to move to a second order theory we run into another problem that we need set theory in our metatheory so set theoretical questions our theory 'answers' may well depend on what the answer is in the metatheory.)

As other have noted in the comments, this is not a lot different from how we usually proceed in axiomatizing math. The group axioms don't 'define what a group element is', they tell you the properties all groups have (and note there are many groups just as there are many models of ZFC). Same goes for the axiomatization of any type of mathematical object. Sometimes, as in the second order Peano axioms, there is only one model (up to isomorphism) obeying them, but that is a rare case.

This issue of circularity that you bring up is called impredicativity and a lot has been written about it. In fact it was originally thought to be a big part of what leads to Russell's paradox, and something to avoid, though this has fallen out of favor. Essentially, it is when one defines an object by quantifying over a universe containing that object. So for instance, when you define the empty set as 'the set that doesn't contain anything,' this definition includes an implicit clause that the empty set doesn't contain the empty set, and thus seems to require we know what the empty set is prior to our defining the empty set. Of course this is a silly example since it's reasonably clear that the notion of the empty set is self-consistent (see also the example of 'the tallest person in the room' from the Wikipedia page), so not all impredicative definitions are paradoxical.

I'm not very knowledgable on this issue in general, but my understanding is that some systems were built that tried to keep predicativity paramount, but it was simply too constraining to work well (see the examples on the wikipedia page of common mathematial definitions that are impredicative). Modern day constuctivists still sometimes have predicativity as a desideratum and for instance Martin-Lof's intuitionistic type theory is predicative. ZFC is decidedly not, but it does not seem to lead to any problems. Again, it is clear that it is not inherently paradoxical since things defined in such a way can still be perfectly self-consistent.

But I think that maybe takes us a little far afield of your misconception here. The way most set theorists think about ZFC is that we have a collection $V$ of objects related by the membership relation $in$ that obey the ZFC axioms. This universe is fixed (though we don't necessarily specify it fully other than that it obeys the ZFC axioms). Then it makes sense that the axioms say 'for all sets, yada yada'. They are true statements about this universe of sets. They do tell us some that sets with certain properties have to exist and for certain properties (like $forall x (x=x)$ by Cantor's paradox) there can't be a set with that extension, but again, this is a description of the universe.

Edit 2
This is already overlong and a bit unfocused (though I think the commenters-- including a few professional logicians in case authority makes a difference-- have done a really good job of hammering home the main take-aways) but I thought it would be useful to actually spell out how the definition of the power set should be thought of here.

First of all, there is the subset property $ysubseteq x$ which is an abbreviation for $forall z (zin y to zin x),$ which hopefully already seemed sharp and unproblematic here. We don't even really quantify over 'all sets', just the elements of $y.$ Then, the power set axiom says $$forall x exists!z forall u (uin z leftrightarrow u subseteq x)$$ which informs us we are assuming that a set theoretical universe has, for any set $x,$ a unique power set $z$ whose elements are exactly those sets $u$ that obey the relation $usubseteq x$ (just as we assume a group has an identity element with certain properties).

(Note we don't actually have to put all this in the axiom... for instance extensionality already guarantees the uniqueness part, and if we wish, we can weaken the $leftrightarrow$ to a $leftarrow$ and use subset comprehension to pick up the slack.)

Now, since we know there is a unique set with this property, we can define an operation $mathcal P:Vto V$ such that given a set $x,$ $mathcal P(x)$ is the unique set with this property. So we have argued that within any set-theortical universe, that this operation is well-defined and thus we have a power set for every set.

If you are a bit unsatisfied and think it's tautoglogical and we rigged that to happen, well, that's the point of the power set axiom. It's a thing that guarantees the existence of a power set for every set.