# Axiom Schema of Specification

According to Wikipedia

In the formal language of set theory, the axiom schema is: $$\forall w_1,\ldots ,w_n\forall A\exists B\forall x(x\in B\Leftrightarrow [x\in A\wedge \varphi(x,w_1,\ldots ,w_n,A)]).$$

It also emphasises that

... $$B$$ is not free in $$\varphi$$.

Questions: How to incorporate the above in the formalisation? And why does $$A$$ have to be free in $$\varphi$$?

• The side condition that $B$ is not free in $\varphi$ is part of the formalization. It is already incorporated... not sure what you’re going for here. – spaceisdarkgreen Jun 26 '19 at 18:55
• @spaceisdarkgreen Can you please show how it is a part of the formalisation? – Atom Jun 27 '19 at 3:59
• Could you explain to me why you suspect it isn't? It is part of the definition of what an instance of the axiom scheme of specification is. – spaceisdarkgreen Jun 27 '19 at 4:01
• @spaceisdarkgreen Don't we need to mention that none of $w_1,\ldots ,w_n$ can be $B$? – Atom Jun 27 '19 at 4:03
• We don't. It is a statement about the formula, not a statement in the formal language. (We could formalize the language we use to talk about formulas, but that's another thing entirely.) – spaceisdarkgreen Jun 27 '19 at 4:10

$$A$$ does not have to be free in $$\varphi$$, but it is allowed to be free in $$\varphi$$. The notation $$\varphi(x)$$ means that $$x$$ is a variable that could occur freely in $$\varphi$$, but does not necessarily have to.
The better question is why $$B$$ is not allowed to be free in $$\varphi$$. This is to avoid the following contradiction: \begin{align} \forall A\exists B\forall x(x\in B\leftrightarrow(x\in A\land x\notin B)) \end{align}