I am trying to fill in some of the gaps in wikipedia's proof of Godel's diagonal lemma, which is a crucial step in proving his first incompleteness theorem.(adsbygoogle = window.adsbygoogle || []).push({});

There is a step that the wiki proof just takes for granted, perhaps because itlooksobvious. But I am unable to find a formal proof of the step (which is the sentence "Then the final formula in (*) must be true" in the very last paragraph of the "Proof" section of the wiki page).

What is needed is to prove that, in a Hilbert System:

[tex]\phi[x:=m] \rightarrow\forall y((y=m)\rightarrow\phi[x:=y])[/tex]

where [itex]\phi[/itex] is a formula, [itex]y, x[/itex] are variables and [itex]m[/itex] is a constant.

[itex]\phi[a:=b][/itex] denotes the formula obtained by substituting [itex]b[/itex] for [itex]a[/itex] in [itex]\phi[/itex]

The axioms of a Hilbert system are standard, as set out in http://en.wikipedia.org/wiki/Hilbert_system. I reproduce them here:

$$ P1.\ \ \phi \to \phi \\

P2.\ \ \phi \to \left( \psi \to \phi \right) \\

P3. \ \ \left ( \phi \to ( \psi \rightarrow \xi \right)) \to \left( \left( \phi \to \psi \right) \to \left( \phi \to \xi \right) \right)\\

P4. \ \ \left ( \lnot \phi \to \lnot \psi \right) \to \left( \psi \to \phi \right) \\

Q5.\ \ \forall x \left( \phi \right) \to \phi[x:=t] \text{ where t may be substituted for x in }\,\!\phi\\

Q6. \ \ \forall x \left( \phi \to \psi \right) \to \left( \forall x \left( \phi \right) \to \forall x \left( \psi \right) \right)\\

Q7. \ \ \phi \to \forall x \left( \phi \right) \text{ where x is not a free variable of }\,\!\phi. \\

I8. \ \ x = x \text{ for every variable }x.\\

I9. \ \ \left( x = y \right) \to \left( \phi[z:=x] \to \phi[z:=y] \right)

$$

The only other logical tools available are Generalisation of any of these axioms by universally quantifying any variables over them, and Modus Ponens.

The Deduction Theorem has already been proved, so is also available.

I was able to almost get the result, as follows:

\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. By Axiom I9 above (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 [itex]\forall y[/itex] and I can't use Q7 above to add it because y is free in this formula. Also, I'm suspicious of step 3, which substitutes a variable for a constant, which I don't think is allowed.

I tried a different approach that gave me the quantifier where I needed it, but it didn't have the right form.

Any suggestions gratefully received.:-)

PS the second set of equations above is horribly aligned. Any suggestions about how to better align them in LaTeX would be appreciated too.

**Physics Forums | Science Articles, Homework Help, Discussion**

Join Physics Forums Today!

The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

# Logic puzzle - trying to justify a step in proof of Godel's theorem

**Physics Forums | Science Articles, Homework Help, Discussion**