Does axiom schema of specification in ZFC states that any sub-set of any set exist?

Question

According to axiom schema of specification in ZFC:

$\forall z \forall w_1 \forall w_2\ldots \forall w_n \exists y \forall x [x \in y \Leftrightarrow (( x \in z )\land \phi )]$,

where $\phi$ can be any formula in the language of ZFC with all free variables among $x,z,w_{1},\ldots ,w_{n}$ ($y$ is not free in $\phi$ ).

Informally, the axiom states (as far as I understand) that for any set $z$ there is (exist) a sub-set $y$, if $y$ is constructed in the way described by the axiom schema of specification.

However, couldn't we just say that any subset of set $z$ exist? It looks to me that a set construction provided by the axiom schema of specification works like this: Loop over all elements of the set $z$ check if the current element satisfy condition $\phi$ and, if it is the case, include this element into $y$.

So, couldn't we just write the following?

$\forall z [\forall x ((x \in y) \Rightarrow (x \in z)) \Rightarrow \exists y]$

Moreover, for me it is not clear how this axiom is related to the Power Set Axiom, which states that for any set $A$ there is a set that contains all the subsets of $A$. Shouldn't this axiom (making a statement about a set of all sub-sets) first "prove" that those sub-sets exist?

Answer 1

In standard first-order logic all elements of the universe "exist", so the axiom you've written doesn't really make sense: "$\exists y$" all on its own is not a formula: quantifiers have to govern a predicate, as in $\exists y(y \neq x)$.

However, it is possible to formalise a theory of classes, in which sets like those in ZF feature as a special kind of class. One of the best known systems of this kind is called NBG. In such a system, being a set is a definable property, sets are the things that are elements of some class. So you can define the notion of set-hood thus: $$ M(x) \equiv \exists y(x \in y) $$ ("M" for "Menge" - German for set.) In such a framework, it is meaningful to write $$ \forall z\forall y (M(z) \land (\forall x(x \in y \Rightarrow x \in z)) \Rightarrow M(y)) $$ which says that any class $y$ that is contained in a set $z$ is itself a set. This statement or some equivalent statement is one of the axioms of NBG.

Answer 2

The purpose of the axiom schema of specification is to give us a way of writing down (specifying) subsets of a set $z$. That is, for every formula $\phi(x)$, we can construct a subset $\{x\in z\ |\ \phi(x)\}$. In particular every subset of $z$ can be specified by a specific formula.

Without this axiom schema we have no way of knowing how to construct subsets of $z$, let alone showing that they exist. The powerset axiom does not help us either in constructing subsets. The best we could do if we know how to construct a finite number of elements $x_1,\ldots,x_n\in z$ is to construct the finite subset $\{x_1,\ldots,x_n\}\subset z$ with the pairing axiom.

Note that the formula you write is not well formed because you refer to $y$ before it is quantified.

The following question is related: Is the Subset Axiom Schema in ZF necessary?

Answer 3

The string you wrote is not a well-formed string, $$\forall z [\forall x ((x \in y) \Rightarrow (x \in z)) \Rightarrow \exists y]$$

For one, quantifiers can be added to existing formulae, they are not atomic. The goal is to bound a variable into a context. So $\exists y$ on its own is a syntax error. The range of the quantifier is also mishandled, since it leaves the $y$ in the first part free, so you're not even writing an axiom, but rather a formula which requires the assignment to say something meaningful about $y$ in advance.

But maybe it will be clearer if we clarify the terminology. Sets are exactly the things that exist, in the context of $\sf ZFC$, so talking about a sub-set is kind of funny, since it seems to presume the existence from the get go. Every subset of a set $x$ exists, since it's a set by definition. So what's the catch here, why do we even need this axiom?

The axiom of specification is saying that every subclass of a set is a set. In other words, given a set, and given a property, the collection of elements which correspond to the property inside the set will also form a set.