Hilbert-calculus, formal proof

Question

I have to give a formal proof in the Hilbert calculus for

$(\forall x\,\,\phi)\rightarrow (\forall y\,\, \phi\frac{y}{x})$, if $x$ is free for $y$ in $\phi$ and $y$ is not free in $\phi$.

Unfortunately I have no idea how this proof could be done.

I would be very grateful, if someone could give a hint, or maybe show an example proof, using the Hilbert-calculus.

Answer 1

See :

• Herbert Enderton, A Mathematical Introduction to Logic (2nd ed - 2001), page 112 :

1) $\forall x \phi$ --- assumption

2) $\forall x \phi \to \phi^y_x$ --- Ax.2 : $x$ is free for $y$ in $\phi$

3) $\phi^y_x$ --- from 1) and 2) by modus ponens

4) $\forall y \phi ^y_x$ --- from 3) by Generalization Th [page 117 : $y$ not free in $\forall x \phi$]

5) $\forall x \phi \to \forall y \phi ^y_x$ --- from 1) and 4) by Deduction Th [page 118].