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

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.

• I doubt if many people have access to Bourbaki's Theory of Sets. I donated mine to a college library years ago. This question almost needs a new tag, bourbaki-specialized-set-theory-treatment, and it would barely make a blip on this site's radar. To get help with this material (not just this question) you need to find a mentor/professor to work thru it. – CopyPasteIt Jun 11 at 14:53
• @CopyPasteIt Thank you for your advice, but I'm currently on a holiday so I can't see my tutor for now. – Lili Tong Jun 11 at 15:13

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)$$.