# Hilbert-calculus, formal proof

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.

• What are your axioms? Have you tried to apply directly the axiom schemes Q5 and Q6 here? – Bruno Bentzen May 5 '15 at 12:42
• Excuse me, I do not know where to start. Yes, I have to use the axiom schemes, but I cant really imagine how I have to combine them to get this result. – user105916 May 5 '15 at 12:56

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].