# Understanding the Definition of the Axiom Schema of Specification

Consider the Axiom Schema of Separation:

If $P$ is a property (with paramter $p$), then for any $X$ and $p$ there exists a set $Y = \{u \in X : P(u,p)\}$ that contains all those $u \in X$ that have property $P$.

Now consider two potential interpretations of this axiom schema:

(1) If $X$ is a set, and $P$ is any arbitrary property, then we can specify a subset of $X$ in which all of the members of this subset satisfy $P$.

(2) If $X$ is a set, and $P$ is any arbitrary property that can be expressed in terms of a finite number of expressions involving only the relations of $\in$ and $=$ and the logical connectives, then we can specify a subset of $X$ in which all of the members of this subset satisfy $P$ given the constraints in bold.

My question is am I correct in assuming that (2) is the proper way to understand this axiom schema, and that (1) and (2) are strictly distinct from each other?

-
Yes, (2) is the only way to understand this axiom. The first version does not produce an axiom scheme. The axiom scheme was not properly described in the first paragraph, it used the non-syntactic word "property." – André Nicolas Jun 6 '13 at 17:19
And $=$ is not really necessary, since (by the Axiom of Extensionality) it is equivalent to $x \subseteq y$ and $y \subseteq x$ which can be expressed in terms of $\in$. – Pedro M. Jun 6 '13 at 17:20
But $\subseteq$ can't be expressed necessarily in terms of a finite number of $\in$, so that isn't $=$ necessary? – user1770201 Jun 6 '13 at 17:33
$x\subseteq y\iff \forall z\colon z\in x\to z\in y$ – Hagen von Eitzen Jun 6 '13 at 17:34
Of course it can. $x\subseteq y\iff\forall z(z\in x\rightarrow z\in y)$. – Asaf Karagila Jun 6 '13 at 17:34

The magnificent beauty of the axioms of $\sf ZF$ is that they allow us, with only $\in$ to express so much.
When we say an arbitrary property, we mean one that can be expressed in the language of set theory. Otherwise it will be impossible to write the axiom relevant to that property in the language of set theory, which is the language of $\sf ZF$.
You seem to forget that there are quantifiers to be used in the formulas. Not everything is boolean combinations of atomic formulas and their negations. No, we make heavy use of quantification here. For example $\subseteq$ can be defined as $x\subseteq y\iff\forall z(z\in x\rightarrow z\in y)$, and we can define when a set is transitive, $\forall y(y\in x\rightarrow\forall u(u\in y\rightarrow u\in x))$, or in shorter form, $\forall y(y\in x\rightarrow y\subseteq x)$.
We can define $x\cup y$, and $x\cap y$, and more and more. Some of the formulas require us to rely on the axioms in order to prove their correctness, but that's fine. We are allowed to do that. But we can sit and write formulas which quickly become more and more complicated and those express a lot. A lot more than just $x\in y$ or $x=y$.