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

Join the discussion
Ask a follow-up here, or get your own question answered by working scientists, mathematicians and engineers — people, not an autocomplete.
Real named experts · corrections over time · the nuance an AI answer skips
2 replies · 4K views
Mathelogician
Messages
35
Reaction score
0
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

  • Q1.png
    Q1.png
    20.5 KB · Views: 185
on Phys.org
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.
 
Perfect!
As always...