Some burning questions on First-order logic from an amateur I'm currently taking an introductory course in Mathematical logic(prerequisites is only advanced calculus) and my lecture notes are based on Enderton's book 'Mathematical Introduction to Logic'
Suppose $\varphi$ is deducible from $\Gamma$ and we are seeking a proof of this fact. There are several cases, one of the which is $\varphi=\forall x \psi$. According to the book, if $x$ should occur free in $\Gamma,$ there will be a variable $y$ such that $\Gamma \vdash \forall y \ \psi ^{x}_{y}$ and $\forall y \ \psi^{x}_{y} \vdash \forall x \ \psi.$ 
May I know how do we prove that there will be a variable $y$ such that $\Gamma \vdash \forall y \ \psi ^{x}_{y}$ and $\forall y \ \psi^{x}_{y} \vdash \forall x \ \psi \ ?$ The author then refers one to Re-replacement lemma but I can't see how are both related. Could anyone instruct me please?
Thank you. 
 A: I suppose that you are working with Corollary 24G, page 124, of Herbert Enderton, A Mathematical Introduction to Logic (2nd ed Harcourt - 2001) :

Assume that $\Gamma \vdash \varphi^{x}_{c}$, where the constant symbol $c$ does not occur in $\Gamma$ or in $\varphi$. Then $\Gamma \vdash \forall x \varphi$, and there is a deduction of $\forall x \varphi$ from $\Gamma$ in which $c$ does not occur. 

The proof invoks Theorem 24F (Generalization on Constants) [page 123].
The motivation of the Corollary is [page 124] : "We want to apply Theorem 24F in circumstances in which not just any variable will do. In the following version, there is a 
variable $x$ selected in advance."
From the hypotheses $\Gamma \vdash \varphi^{x}_{c}$, where the constant symbol $c$ does not occur in $\Gamma$ or in $\varphi$, Theorem 24F gives us a deduction (without $c$) from $\Gamma$ of $\forall y ((\varphi^{x}_{c})^{c}_{y})$ where $y$ does not occur in $\varphi^{x}_{c}$.
But since $c$ does not occur in $\varphi$,

$((\varphi^{x}_{c})^{c}_{y}) = \varphi^{x}_{y}$.

This substitution works, because there are no occurrences of $c$ in the "original" formula $\varphi$; thus, substituting $c$ in place of $x$, and then $y$ in place of $c$, we do not have "unpleasant effects".
Thus, we may conclude that : 


$\Gamma \vdash \forall y \varphi^{x}_{y}$ --- (a).


The last step in the proof is to show that :

$\forall y \varphi^{x}_{y} \vdash \forall x \varphi$. 

To do this, he invokes Axiom 2 [see page 112] : $\forall y \alpha \rightarrow \alpha^{y}_{t}$.
With $\varphi^{x}_{y}$ in place of $\alpha$ and $x$ in place of $t$, we have as $\alpha^{y}_{t}$ the result $(\varphi^{x}_{y})^{y}_{x}$ , i.e. $\varphi$.

The proof now call for a formal verification through Re-replacement lemma.

Having verified this, we have $\vdash \forall y \varphi^{x}_{y} \rightarrow \varphi$.
Then the following generalization is also an axiom [see page 112] :

$\vdash \forall x (\forall y \varphi^{x}_{y} \rightarrow \varphi )$.

By Axiom 4 ($x$ is not free in $\forall y \varphi^{x}_{y}$), we have :

$\vdash \forall y \varphi^{x}_{y} \rightarrow \forall x \varphi$.

Thus, from (a) above, we may finally conclude :


$\Gamma \vdash \forall x \varphi$.


