Welcome to our community

Be a part of something great, join today!

[SOLVED] A question on "Change of bound variables" Theorem (predicate logic)

Mathelogician

Member
Aug 6, 2012
35
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.
 

Attachments

Evgeny.Makarov

Well-known member
MHB Math Scholar
Jan 30, 2012
2,492
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

Member
Aug 6, 2012
35
Perfect!
As always...