ZF: Difference between POW and SEP?
In ZF, the Power Set Axiom (POW) says that given any set $A$, there exists a set $\mathcal{P}(A)$ such that $$ \forall a(a\in\mathcal{P}(A)\leftrightarrow a\subseteq A)\tag{1} $$
Questions:
On many occasions, I've seen POW stated like this: "For any set $A$ there is a set consisting of all subsets of $A$."
Would a more precise formulation be: "For any set $A$ which is known to exist there exists a set containing all subsets of $A$ which are known to exist."?
An instance of the Axiom Schema of Separation (SEP) essentially gives the existence of a subset of a given set. So, why doesn't POW imply SEP? Is it because POW doesn't give the existence of the individual subsets but only the set containing them all?
Conversely, does SEP and the remaining ZF axioms imply POW?
Solution 1:
1: Axioms do not have any sense of time or knowledge. They can't speak about whether sets or other elements exist prior to (or as a consequence of) other sets -- at least not then in standard first-order logic that axiomatic set theory is usually done within.
It may be intuitively instructive to imagine all of the sets of set theory to come into being in some particular order sequence, guided by "when" axioms say they ought to exist, but that is not what the axioms say.
What the axioms say is just "Let's imagine we have a universe of sets, and such-and-such claims happen to be true about the universe of sets we have". The axiom of power sets does not create a power set -- it simply asserts that there is a power set of whatever you hold in your hand, and this power set has existed the whole time. It comes together with all of the other sets in your universe, and the entire totality of sets magically happens to make your axioms true.
2: What the power set axiom says is only that for every set $A$ there's a set whose members are those sets in the universe that happen to be subsets of $A$. It doesn't say anything about how many such things exist -- all it tells you that there's a set $\mathcal P(A)$ such that if you manage to find some set $B$ and discover that $B\subseteq A$, the set you have found will also be an element of $\mathcal P(A)$.
On the other hand, the axiom of separation can, in most variants of the formulations, be derived from the axiom of replacement (together with the axiom of the empty set).
3: The axiom of separation lets you know that any subcollection of a set that you can define (in the language of set theory) will exist as a set inside your universe of sets. It does not in itself guarantee that there's a set that contain all of those subsets; for that you need a separate axiom.
For example, if you take a model of ZFC and restrict it to only the hereditarily finite-or-countable sets, you will have something that satisfies all axioms of ZFC except for the power set axiom. Thus, the other axioms cannot (if they are consistent) imply the power set axiom.