# 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. Commented Jun 26, 2019 at 18:55
• @spaceisdarkgreen Can you please show how it is a part of the formalisation?
– Atom
Commented Jun 27, 2019 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. Commented Jun 27, 2019 at 4:01
• @spaceisdarkgreen Don't we need to mention that none of $w_1,\ldots ,w_n$ can be $B$?
– Atom
Commented Jun 27, 2019 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.) Commented Jun 27, 2019 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}