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

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?

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.

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.

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?