MHB A question on "Change of bound variables" Theorem (predicate logic)

[Mathelogician]

Hi all;
I need some clarification in red part; in how it is deduced from the theorem 2.5.6!
I know how the blue is deduced from the theorem but don't even know how to get blue form red in practice!(No algorithm is suggested...)
Anyway, any explanation is thanked...
Regards.

 

[Evgeny.Makarov]

Given a formula $\varphi$, we have two sets of variables: those that occur free in $\varphi$ and those that occur bound in $\varphi$. These two sets may have a nonempty intersection. We cannot do anything with free variables, but we can rename bound ones. So, for each bound variable $x$ select a new name that does not occur free and is free for $x$ and replace the variable with this name. It is often easier to select a completely new (called "fresh") variable name that does not occur in the original formula.

For example, let $\psi$ be \[x=0\lor\forall x\exists u\,f(x)=g(u,v)\] Then $FV(\psi)=\{x,v\}$ and $BV(\psi)=\{x,u\}$, so $FV(\psi)\cap BV(\psi)=\{x\}$. We would like to rename the bound $x$ by applying Theorem 2.5.6 to the right disjunct of $\psi$, i.e., to $\forall x\,\varphi[x/z]$ where $\varphi$ is $\exists u\,f(z)=g(u,v)$. We choose a new name for $x$, e.g., $y$, which is different from all variables in $\psi$. Then $x,y$ are free for $z$ in $\varphi$ and $x,y\notin FV(\varphi)$. Therefore, we can apply Theorem 2.5.6 to get $\models \forall x\,\varphi[x/z] \leftrightarrow \forall y\,\varphi[y/z]$, i.e., \[\models(\forall x\exists u\,f(x)=g(u,v)) \leftrightarrow (\forall y\exists u\,f(y)=g(u,v))\tag{*}\]By replacing the left-hand side of (*) with the right-hand side in $\psi$, we get an equivalent formula $x=0\lor\forall y\exists u\,f(y)=g(u,v)$.

It probably takes longer to read than to understand this. The idea is simple: choose a fresh variable name and replace a bound variable with this new name; you'll get an equivalent formula. If the old bound variable also occurred free, then you have one less variable that occurred both free and bound.

 

[Mathelogician]

Perfect!
As always...