# I don't understand the axiom schema of separation.

I understand that the axiom schema of separation should assert the existence of a set $y$, subset of a set $z$, where $y=\{x\in z:\varphi \,x\}$ (with $\varphi$ some formula).

In the book I'm reading, it's written as follows

Any formulae of the form $$(\exists v)\,((\exists w_1) (w_1\in v\, \vee v =0)\, \wedge\,(\forall\, w)(w\in v\iff w\in u \wedge \varphi))$$ Is an axiom.

Where $0$ stands for the empty set, $v$ is distinct from $u$ and $w_1$ and is not free in $\varphi$.

So, here $v$ would place the role of my $y$ above, and $u$ of my $z$. However, I don't understand the part about $w_1$ not being free in $\varphi$. Shouldn't we require that $\varphi$'s only free variable be $w$?

• Admittedly, I am also not sure what the $(\exists w_1)(w_1\in v\lor v=0)$ part is supposed to gain. - Isn't that tautologic? – Hagen von Eitzen Apr 29 '16 at 16:28
• Additionally, it doesn't make much sense to require that $w_1$ is not free in $\varphi$, since $\varphi$ doesn't appear in the formula in a context where $w_1$ is bound at all. On the other hand we do need to require that $v$ is not free in $\varphi$; otherwise taking $\varphi$ to be $w\notin v$ would lead to a contradiction whenever $u$ is nonempty. – hmakholm left over Monica Apr 29 '16 at 17:24
• Yes, it's pretty weird. This comes from Suppes' book Axiomatic Set Theory, if that helps... – YoTengoUnLCD Apr 29 '16 at 17:31
• Based on this sample you probably shouldn't put too much trust in the technical details of formulae in that book ... – hmakholm left over Monica Apr 29 '16 at 17:33
• Oh I'm sorry!! It appears I misunderstood the paragraph and copied it wrongly. Please see the edit. It looks like $v$ is supposed to be the not free variable in $\varphi$. Althought I still don't see the need for the first part of the $\wedge$. – YoTengoUnLCD Apr 29 '16 at 17:37

With regard to the $\exists w_1(w_1\in v \vee v=0)$ clause, it's important to keep in mind that Suppes allows non-sets (also called urelements) into the universe. Now imagine we omit this clause. As I mention in the comments, it means that there could be extensionally equivalent abstracts whose identity we would be unable to prove, such as $\{x\in A: x\neq x\}$ and $\{x\in A: \forall y(y\in x)\}$.
This starts to get hairy when we look at powersets. Do we define the powerset of $A$ as $\{x: \forall y(y\in x\Rightarrow y\in A)\}$? Then every urelement would be included, and we'd have some very uncomfortable cardinal arithmetic. Or do we define it as $\{x:x\textrm{ is a set }\wedge\forall y(y\in x\Rightarrow y\in A)\}$? In which case given an example of an object that satisfies an instance of the separation scheme, we can't necessarily prove that it's a member of the power set.
Of course, the $\exists w_1(w_1\in v \vee v=0)$ clause just saves you a little bit of work, and isn't strictly necessary. The good notion of the powerset is obviously the latter, and we can show that the empty set will also satisfy any instance of separation that an urelement does, and use it instead, but having it packaged into the separation scheme saves proving that extra step repeatedly.
You may need additional free variables in applications. For example in order to define $$a\cap b:=\{\,x\in a:x\in b\,\}$$ you would want $\varphi$ to be $w\in b$, where both $w$ and $b$ are free.