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

In summary, the conversation is about filling in gaps in Wikipedia's proof of Godel's diagonal lemma for his first incompleteness theorem. The proof relies on a step that is taken for granted and is unable to be formally proven. The step involves proving that in a Hilbert system, a formula with a substituted variable implies the same formula with a substituted constant. The conversation also discusses the availability of axioms, the use of the Deduction Theorem, and the Generalization rule. The conversation ends with a suggestion to use induction to prove the theorem and a clarification on what Gamma refers to in the proof.
  • #1
andrewkirk
Science Advisor
Homework Helper
Insights Author
Gold Member
4,116
1,712
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:
[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:
Physics news on Phys.org
  • #2
andrewkirk said:
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.
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.
 
  • #3
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 [itex]\Gamma\vdash\phi[/itex], and x does not occur free in any formula of [itex]\Gamma[/itex], then [itex]\Gamma\vdash\forall x\phi[/itex] .
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 ( [itex]\neg, \to, \forall[/itex]) starting from the above rule of generalisation for axioms. I could do the steps for [itex]\neg[/itex] and [itex]\to[/itex] but got stuck when I tried [itex]\forall[/itex].

Also I don't really understand what is meant by "x does not occur free in any formula of [itex]\Gamma[/itex]". If [itex]\Gamma[/itex] refers to all axioms used to derive [itex]\phi[/itex] 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 [itex]\Gamma[/itex] 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.
 
  • #4
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.
 
Last edited:
  • #5
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}\\
$$
 
  • #6
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.
 

1. What is Godel's theorem and why is it important in logic puzzles?

Godel's theorem, also known as Godel's incompleteness theorem, is a mathematical proof that states any formal system of logic will contain statements that cannot be proven or disproven within that system. This is important in logic puzzles because it shows that there will always be limitations to what can be proven using a set of rules or axioms.

2. Can you give a brief overview of the proof of Godel's theorem?

The proof of Godel's theorem involves using a statement called the "Godel sentence" which essentially says "this statement cannot be proven within the system." This sentence is then shown to be both true and not provable, therefore demonstrating the limitations of the system.

3. How does Godel's theorem relate to the concept of self-reference?

Godel's theorem relies on the concept of self-reference, as the Godel sentence is a statement that is referring to itself. This self-referential aspect highlights the limitations of a system trying to prove its own consistency.

4. Are there any real-world applications of Godel's theorem?

Yes, Godel's theorem has been applied in fields such as computer science and artificial intelligence to show the limitations of these systems and the importance of human intuition and creativity. It has also been used in philosophy to explore the nature of truth and knowledge.

5. Is Godel's theorem widely accepted by the scientific community?

Yes, Godel's theorem is widely accepted by the scientific community and is considered one of the most significant mathematical proofs of the 20th century. It has been extensively studied and verified by mathematicians and logicians, and its implications continue to be explored in various fields of study.

Similar threads

  • Advanced Physics Homework Help
Replies
3
Views
287
  • Set Theory, Logic, Probability, Statistics
Replies
6
Views
2K
  • Set Theory, Logic, Probability, Statistics
Replies
2
Views
2K
  • Set Theory, Logic, Probability, Statistics
Replies
3
Views
2K
  • Set Theory, Logic, Probability, Statistics
Replies
1
Views
2K
  • Calculus and Beyond Homework Help
Replies
4
Views
955
  • Introductory Physics Homework Help
Replies
2
Views
1K
  • Topology and Analysis
Replies
2
Views
2K
  • Set Theory, Logic, Probability, Statistics
Replies
1
Views
1K
  • Advanced Physics Homework Help
Replies
1
Views
1K
Back
Top