1
$\begingroup$

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$?

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

$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}

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.