When does renaming bound variables require a fresh variable?

849 Views Asked by At

Suppose that $E_1$ and $E_2$ are two $\alpha$-equivalent first-order logic formulas (or $\lambda$-terms), and let $V$ be the set of all variables (free and bound) used in $E_1$ or $E_2$. Is it possible that $E_1$ cannot be converted into $E_2$ by renaming bound variables if only variables from $V$ are used in the renaming? In other words, is it possible that $\alpha$-conversion of one expression into another requires a fresh variable, not encountered in the original expressions?