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.

  • 1
    $\begingroup$ 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. $\endgroup$ – CopyPasteIt Jun 11 at 14:53
  • $\begingroup$ @CopyPasteIt Thank you for your advice, but I'm currently on a holiday so I can't see my tutor for now. $\endgroup$ – 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)$.


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.