An inquiry on the proof of CF6 in Bourbaki's Theory of Sets

Question

Regarding the assembly $\tau_{z}((y|x)A)$ ($y$ does not appear in $A$) in the case $z=x$. I do understand the method if we apply CS3 to simplify that, but if I try to simplify it from first principles, something wrong happens, here is how I did it. "The operation replaces all $x$ in (A with all $x$ replaced by $y$) with $\square$, since there is no $x$ in the bracket, the operation is identical with $(y|x)A$. But if we apply CS3 we would get $\tau_{y}((y|x)A)$, which essentially replace all x with $\square$. The two different outcomes confuse me, could you help please? Thank you very much.

Answer 1

The author is proving the rule for substitution of a varibale in a formula $A$.

The substitution is written as $(y|x)A$.

The propositional cases are striaghtforward; the only issue is with the quantifier $\tau_z$.

If $A$ is $\tau_z (A')$, we have three sub-cases :

(i) $z$ is different form both $x$ and $y$: thus, we can freely subst $y$ in place of $x$ and the result is : $(y|x)A := \tau_z [(y|x)A']$. This is CS4.

Example: $A$ is $\tau_z(x \in z)$. The result of the substitution will be $(y|x)A := \tau_z(y \in z)$.

(ii) $z$ is identical $x$. In modern terms, this means that $x$ is not free in $A$, and thus we cannot subst it with $y$. Thus, the result is the original formula $\tau_z(A) := \tau_x(A)$.

But a quantfied variable can be renamed, provided that we use a new variable; thus, due to the fact that $y$ does not occur into $A$, we have that $\tau_x(A) := \tau_y(A')$. This is CS3.

Example: in this case, let $A$ is $\tau_x(x \in w)$. In "formal" notation [see page 17], this is $\tau (\square \in z)$ where $\square$ is a "place-holder".

As you can see, there is no $x$ to be replaced, and thus $(y|x)[\tau (\square \in z)$ will be $\tau (\square \in z)$, that can be re-written as $\tau_y(y \in z)$.

(iii) $z$ is identical with $y$. In this case, we cannot put $y$ in place of $x$, because if we do so, the new occurrence of $y$ into $A$ will be "captured" by the quantifier $\tau_y$.

Thus, we have to rename the quantified variable with a new variable $u$ to get : $\tau_u(A)$ and then subst $y$ in place of $x$ to get : $(y|x)[\tau_u(A)] := \tau_u(A')$.

Example: $A$ is $\tau_z(x \in z)$. The result of the substitution will be $(y|x)A := (y|x)[\tau_y(x \in y)] := (y|x)[\tau_u(x \in u)] := \tau_u(y \in u)$.