# When does renaming bound variables require a fresh variable?

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?

• I think so : consider $\forall x \forall y A(x,y)$; it is equivalent to $\forall y \forall x A(y,x)$, but to do so, we have to use : $\forall x \forall y A(x,y) \to \forall y A(z,y) \to A(z,x) \to \forall x A(z,x) \to \forall y \forall x A(y,x)$. – Mauro ALLEGRANZA Mar 18 '15 at 15:30