# Problem in Logic - Hilbert Systems

1. Oct 12, 2012

### andrewkirk

1. The problem statement, all variables and given/known data
In a Hilbert System, prove:
$$\phi[x|m] \rightarrow\forall y((y=m)\rightarrow\phi[x|y])$$
where $\phi$ is a formula, $y, x$ are variables and $m$ is a constant.
$\phi[a|b]$ denotes the formula obtained by substituting $b$ for $a$ in $\phi$
This problem crops up in my attempting to prove Godel's diagonal lemma (aka 'Fixed Point Theorem').

2. Relevant equations
The axioms of a Hilbert system are standard, as set out in http://en.wikipedia.org/wiki/Hilbert_system

3. The attempt at a solution
\begin{align}
\phi[x|m]\ \ \ \ \ \ \text{1. Hypothesis}\\
y=m\ \ \ \ \ \ \text{2. Hypothesis}\\
(y=m)\rightarrow(\phi[x|m]\rightarrow\phi[x|y))\ \ \ \ \ \ \text{3. Axiom Schema 6 (substitution of equal variables)}\\
\phi[x|m]\rightarrow\phi[x|y]))\ \ \ \ \ \ \text{4. Modus Ponens applied to 2 and 3}\\
\phi[x|y]\ \ \ \ \ \ \text{5. Modus Ponens applied to 1 and 4}\\
(y=m)\rightarrow\phi[x|y]\ \ \ \ \ \ \text{6. Deduction Theorem applied to 2 and 5)}\\
\phi[x|m]\rightarrow((y=m)\rightarrow\phi[x|y])\ \ \ \ \ \ \text{7. Deduction Theorem applied to 1 and 6)}\\
\end{align}
This is almost what's required, except it's missing the universal quantifier $\forall y$ and I can't use Axiom Schema 4 of Generalisation to add it because y is free in this formula.
I tried a different approach that gave me the quantifier where I needed it, but it didn't have the right form.