- 3,770

- 1,384

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.

There is a step that the wiki proof just takes for granted, perhaps because it

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.

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

There is a step that the wiki proof just takes for granted, perhaps because it

*looks*obvious. 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.

Last edited: