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

[andrewkirk]

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 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:
$$\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$

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 $\forall y$ 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.

 

[Preno]

This is almost what's required, except it's missing the universal quantifier $\forall y$ and I can't use Q7 above to add it because y is free in this formula.

You're forgetting that the Generalization rule is available.

Also, I'm suspicious of step 3, which substitutes a variable for a constant, which I don't think is allowed.

Step 3 is okay.

 

[andrewkirk]

Thank you for your reply Preno. It's good to know that I'm on the right track.
I am uncertain about what rule of Generalization can be applied.
The two descriptions of Hilbert's system I am principally using include a generalisation rule that the generalisation of any of the nine axioms (meaning universally quantifying them over any collection of variables) above is a theorem. But I can't use that because my last line is not an axiom.

The wikipedia article refers to a metatheorem of generalisation:

Generalization: If $\Gamma\vdash\phi$, and x does not occur free in any formula of $\Gamma$, then $\Gamma\vdash\forall x\phi$ .
​

My guess is that this theorem is derivable from the more limited generalisation rule above, which only applies to axioms.

However I have been unable to find a proof of this metatheorem, despite a moderate search. I tried to prove something along those lines by induction on the three methods of composition ( $\neg, \to, \forall$) starting from the above rule of generalisation for axioms. I could do the steps for $\neg$ and $\to$ but got stuck when I tried $\forall$.

Also I don't really understand what is meant by "x does not occur free in any formula of $\Gamma$". If $\Gamma$ refers to all axioms used to derive $\phi$ then the restriction will never be satisfied because every variable occurs in every axiom group that mentions a variable (the fifth to ninth axiom groups).
Is $\Gamma$ intended to refer only to the non-logical axioms (eg the Peano axioms if that is what we are working with)?

I expect that if I could find a proof of the metatheorem, all would become clear, but I can't find one.

 

[Preno]

The theorem (Generalization limited to axioms + the axiom schemas Q6 & Q7 yield the above generalization of Generalization) is easy to prove, but you're using the wrong kind of induction. What you want to prove is: if there is a proof of kind A, then there is a proof of kind B. Thus you need to use induction on the length of the proof of phi from Gamma.

Gamma does not refer to axioms used to derive phi, it refers to the hypotheses used to derive phi. A proof in a Hilbert system from the assumptions Gamma is a sequence of formulas such that each formula in the sequence is either a member of Gamma, or an axiom, or is derived from some previous formulas in the sequence by means of a rule of derivation.

Note that Hilbert calculi are in general rather awkward to work with. Some syntactic bureaucracy is necessary in proof theory, but Hilbert calculi tend to obscure rather than clarify the structure of formal proofs, hence I am constantly baffled by the fact that logical results are presented to non-logicians in terms of Hilbert calculi. Perhaps you would find working with in Gentzen calculi or in natural deduction more convenient? In particular, the above theorem on generalization is a primitive rule in the usual Gentzen calculus for classical logic.

 

[andrewkirk]

Thank you again Preno. Induction on proof length was just the hint I needed. I should have guessed, as that's the same technique as is used to prove the Deduction Theorem.

Mostly for my own benefit, here is my proof of the Universal Generalisation Theorem

Universal Generalisation Theorem
If Γ⊢φ and y does not appear free in any of the formulas in Γ, then Γ⊢φ'≡∀y:φ
Proof
Let the proof of φ be the sequence of formulas T1, T2, ….Tn. Each of these formulas must be either a logical axiom, a formula in Γ, or the result of applying modus ponens to two earlier members of the sequence. We prove the result by induction on n.
Let Tk' denote ∀y:Tk if the variable y is not already universally quantified in Tk, otherwise Tk' denotes Tk.

The base case is n=1. Then T1 is either a logical axiom or a formula in Γ. If T1 is a logical axiom then Γ⊢T1'≡∀y:T1, as any generalisation of a logical axiom is in the theory generated by those axioms. Alternatively, if T1 is in Γ then y is not free in T1 by assumption so we can insert the following proof steps:

• T1''≡T1→∀y:T1 by the axiom schema of generalisation.
• T1'≡∀y:T1, which follows from modus ponens on T1 and T1'.

So the theorem is true for proofs of length 1 (prior to the transformations necessary to insert universal quantification, which will lengthen them by inserting additional steps).

Now assume the result is true for all proofs of length k<n prior to transformation. Then for a given proof T1, …, Tn, we can also prove T1', …, T(n-1)'. What about Tn? If Tn is a logical axiom or in Γ then Tn' can be proven by the same argument as we used for T1. The remaining alternative is that Tn is derived by modus ponens from Ti and Tj≡Ti→Tn. Then we proceed as follows:

• Γ⊢Ti' by our inductive hypothesis, as i<n,
• Γ⊢Tj', by our inductive hypothesis, as j<n,
• ⊢Tn'''≡∀y:(Ti→Tn)→(∀y:Ti→∀y:Tn)≡Tj'→(Ti'→Tn'), which is an instance of the axiom schema 7
• Γ⊢Tn''≡Ti'→Tn' is obtained by modus ponens on Tj' and T'''
• Γ⊢Tn' is obtained by modus ponens on Ti' and T''.

Hence the result is also true for n, hence it is true for proofs of all lengths.
----------------------------------------------------------------------------------------------------------
I have also managed to shore up my step 3. You were right, it is valid, but it just needs another couple of steps to make that clear.
$$\forall z ((y=z)\rightarrow(\phi[x:=z]\rightarrow\phi[x:=y]))\ \ \ \ \ \ \text{3a. By Axiom I9 above (substitution of equal variables), generalised by universal quantification over z}\\
\forall z ((y=z)\rightarrow(\phi[x:=z]\rightarrow\phi[x:=y]))\to((y=m)\rightarrow(\phi[x:=m]\rightarrow\phi[x:=y]))\ \ \ \ \ \ \text{3b. By Axiom Q5 above (substituting constant m for variable z)}\\
((y=m)\rightarrow(\phi[x:=m]\rightarrow\phi[x:=y]))\ \ \ \ \ \ \text{3. by Modus Ponens on 3a and 3b}\\
$$

 

[Preno]

Yes, the proof seems to be correct. Note, however, that there is no need to distinguish two cases (if the variable y is "not already universally quantified in Tk" - meaning, presumably, if it is free in Tk - and if it is not), as the argument works just the same in both cases. Even if y is "already universally quantified in Tk", nothing prevents you from adding another universal quantifier ∀y.