I am reading Enderton's A Mathematical Introduction to Logic, section 2.4 on logical deductions. I am finding it unclear on how the Existence of Alphabetical Variants theorem works to find deductions. I think the notation for substitution is tripping me up here.
Existence of Alphabetical Variants: Let $\phi$ be a formula, t a term, x a variable, then we can find a formula $\psi$ that differs from $\phi$ only in the choice of quantified variables such that $\phi \vdash \psi$ and $\psi \vdash \phi$, and t is substitutable for x in $\psi$.
If I understand correctly, this is merely a way to circumvent the restrictions on the Generalization theorem, though Enderton is never very clear or linear about explaining it.
In particular, say x is free in $\Gamma$ and I want to deduce $\forall x\varphi$, where x is free in $\varphi$. From what I understand, if I can show for some $w$ not occuring in $\Gamma$ or $\varphi$, that $\Gamma \vdash \forall w \varphi ^x_w$, then it follows by EAV that $\Gamma \vdash \forall x \varphi$. The finiteness of formulas ensures that there is always such a $w$.
So, for example, if I want to show $\Gamma \vdash \forall x\phi(x)$, I need to show $\Gamma \vdash \forall w \phi(w)$, where $w$ does not occur anywhere.
Is this a correct interpretation? In particular, in a proof, do I need to prove or cite anything other than EAV that $\vdash \forall w \psi(w) \rightarrow \forall x \phi(x)$? Can my $w$ occur bounded in $\Gamma$?