A question about the axiom schema of separation

Question

I am currently studying axiomatic set theory and I am struggle to answer some questions regarding the axiom schema of separation. First, let me introduce some context. It is usual to state the axiom schema of separation as

$$\vdash \forall y \exists x \forall z (z \in x) \leftrightarrow (z \in y \wedge \phi(z))$$

regarded that $z$ is a free variable in $\phi$ and that $x$ is not a free variable in $\phi$.

In the presence of the logical axioms concerning universal quantification, one can deduce a more general version of this axioms, for example

$$\vdash \forall w_1 \forall w_2 \cdots \forall w_n \forall y \exists x \forall z (z \in x) \leftrightarrow (z \in y \wedge \phi(z,w_1,w_2, \dots, w_n)).$$

One may even allow the variable $y$ to occur in the formula $\phi$ as a free variable and we obtain something similar to the previous one, which $\phi(z,y,w_1,\dots,w_n)$ in the place of $\phi(z,w_1,w_2,\dots,w_n)$.

Now, just a couple of things concerning the presented until now. When I ask if something is correct or true, I am actually asking if the reasons that I am giving are the ones that motivates the formulation of this axiom schema.

1. I believe that the reason that we do not allow $x$ to be a free variable in the formula $\phi$ is because otherwise we would be defining the set $x$ in terms of the set $x$ (informally, it happens self referencing). Is this correct? Also, I think that we do not state anything about the possibility of $x$ being a bound variable in $\phi$ since we cal always change the bound occurrences of a variable for another variable which do not appear in the formula. Is it true?

2. Regarding the variable $z$. We do not worry abound the bound occurrences since, as it was said in the last paragraph, we can always change them for some other variable which do not occur in the formula. The fact that $z$ must occur free in $\phi$ sounds intuitively plausible, since we are “testing” the elements that came from why to see if they satisfy the formula $\phi$ so we can gather them together. Right?

3. About allowing $y$ to be also a free variable in $\phi$. Well I must say that his one I can’t figure it out. I mean, we can check a few examples and intuitively they seem sound, but I wonder why would someone use this an instance of this axiom schema, while letting the variable $y$ to be free in $\phi$.

This are my main questions. I must say that (obviously) I am not trying to prove the axiom schema, I am just trying to get a feel for it and to come up with an informal justification of how it was formulated.

Also, when dealing axiomatically, one observes that the variables play the roles of sets in the language of set theory, meaning, a variable is used to denote sets. But is it right to say, for example, “$x$ is a set which do not occur free in $\phi$“? In other words, variables and sets are different things (I guess?)

Thank you in advance!

Answer 1

I believe that the reason that we do not allow $x$ to be a free variable in the formula $\phi$ is because otherwise we would be defining the set $x$ in terms of the set $x$ (informally, it happens self referencing). Is this correct? Also, I think that we do not state anything about the possibility of $x$ being a bound variable in $\phi$ since we cal always change the bound occurrences of a variable for another variable which do not appear in the formula. Is it true?

In addition to the conceptual problem, allowing $x$ free would result in inconsistency: for instance we could let $\phi$ be $z\notin x$ and consider the case where $y$ is nonempty. You're right about the bound occurrences.

Regarding the variable $z$. We do not worry abound the bound occurrences since, as it was said in the last paragraph, we can always change them for some other variable which do not occur in the formula. The fact that $z$ must occur free in $\phi$ sounds intuitively plausible, since we are “testing” the elements that came from why to see if they satisfy the formula $\phi$ so we can gather them together. Right?

Ditto on bound occurrences. Actually, there's no reason to require $z$ to occur free. The absence of $z$ is just an unproblematic trivial case where either $x=y$ (if $\phi$ is true) or $x=\emptyset$ (if $\phi$ is false). On the other hand, if for some reason you wanted to get rid of this triviality, disallowing $\phi$ where $z$ doesn't occur free wouldn't help, since the occurrence could be trivial, like $\phi(z) := (z=z)\land \sigma,$ where $\sigma$ doesn't depend on $z.$

About allowing $y$ to be also a free variable in $\phi$. Well I must say that his one I can’t figure it out. I mean, we can check a few examples and intuitively they seem sound, but I wonder why would someone use this an instance of this axiom schema, while letting the variable $y$ to be free in $\phi$.

This is a non-issue. If the variable $y$ weren't allowed to occur free in $\phi,$ but your argument required that the condition $\phi$ to depend on $y$, you could nonetheless obtain this by assigning one of the parameters $w_i$ to the same set as $y$ is assigned to.

Also, when dealing axiomatically, one observes that the variables play the roles of sets in the language of set theory, meaning, a variable is used to denote sets. But is it right to say, for example, “$x$ is a set which do not occur free in $\phi$“? In other words, variables and sets are different things (I guess?)

Yes, variables and sets are different things, and it is wrong to say that a set occurs in a formula. But things get blurry, because the intended meaning is that the variables are sets, so when we reason informally we often refer to "the set $x$", etc. (And by the completeness theorem, these informal arguments can be converted into formal proofs only involving syntactical rules of deduction in first order logic, and making no mention of "sets".)

Answer 2

but I wonder why would someone use this an instance of this axiom schema, while letting the variable $y$ to be free in $\phi$.

There are some situations where it is obviously more convenient to use an instance of Separation with $y$ free in $\phi$, because you may want to apply Separation not to a concrete $y$, but to many different values of $y$, or even an arbitrary $y$, and the "membership test" you want to use may depend on $y$. For example, if you want to prove the sentence "the minimal elements of every poset $(P, \preceq)$ form a set", you would want to use the instance $$\forall P\ \exists x\ \forall z\ (z\in x \Leftrightarrow (z\in P \wedge \forall z'\ (z'\in P \Rightarrow \neg (z' \preceq z))))$$ where $\phi(z)$ is $\forall z'\ (z'\in P \Rightarrow \neg (z' \preceq z))$, a formula where $P$ does occur free.

Of course, like the other answer has noted, this is nothing more than a convenience issue. Even if your formulation of the axiom schema does not allow $y$ to occur free in $\phi$, the rules of logic would allow you to prove the same thing by using a free variable $w_i$ in place of $y$ in $\phi$, and then assign the value $y$ to the free variable $w_i$.