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

1 Answer 1

Reset to default
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$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .