Dismiss Notice
Join Physics Forums Today!
The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

Proof of Godel's 1st Theorem missing ω-consistency requirement. What's wrong?

  1. Oct 25, 2012 #1


    User Avatar
    Science Advisor
    Homework Helper
    Gold Member

    Below is a proof of one of the key steps in Godel's first incompleteness theorem. It appears to prove the theorem. However, it doesn't assume that T⋃Q is ω-consistent, which I have read is necessary for the proof to work. The alternative is to use Rosser's Trick to avoid needing to assume ω-consistency. But the proof doesn't do that either.

    This leads me to believe that my proof must have an invalid step in it, that requires ω-consistency to validate it. But I cannot see where that would be required. That's probably because my grasp of the concept of ω-consistency is very new and very tenuous.

    I think my omission is probably in the part of the proof I've laid out in detail below. But it's possible that it lies somewhere else, like in the Representability Theorem or the couple of steps at the end.

    If anybody can help me identify where I have gone wrong, I would appreciate it.

    Strong Undecidability of Q
    For a collection S of sentences in formal language L, define:
    Cn(S) = {#(θ) : Sentence(θ) ⋀ (S⊢ θ)}
    where #(F) denotes the Godel number of formula F and Sentence(ψ) means that ψ is a well-formed sentence in L.
    The strong undecidability of Q theorem states that for any L-theory T, if T⋃Q is consistent in L, then T is undecidable, by which we mean that Cn(T) is not recursive.
    Here Q denotes Robinson Arithmetic.

    Assume T⋃Q is consistent in L and Cn(T⋃Q) is recursive (meaning that the relation that defines it as a subset of ω is recursive, aka μ-recursive).
    Because of the recursivity of Cn(T⋃Q), the Representability Theorem tells us that the relation it defines must be representable in Q, which means there must exist a formula BewT⋃Q in wff(LN) with one free variable, say c, such that, for any θ in wff(LN):

    A. (#(θ)∈Cn(T⋃Q)) ⇒ (Q⊢BewT⋃Q[c:=#(θ)] and
    B. (#(θ)∉Cn(T⋃Q)) ⇒ (Q⊢¬BewT⋃Q[c:=#(θ)]).

    Bew is short for the German word beweisbar, meaning provable.
    Note that representability of Cn(T⋃Q) is a bigger requirement than it might at first seem, as any wff must have finite length and, since both sets Cn(T⋃Q) and ω - Cn(T⋃Q) are infinite, this precludes BewT⋃Q from being a simple infinite list of all numbers in Cn(T⋃Q). BewT⋃Q doesn't have to be recursive, but it must be concise.

    Now by the Diagonal Lemma, applied to the wff (¬BewT⋃Q), we know there exists a sentence G in wff(LN) such that:

    1. Q ⊢ (G↔¬BewT⋃Q[c:=#(G)])

    This appears to be a theorem saying that G is true in T iff it is not provable in T, which immediately arouses suspicion. Let us examine this formally:

    2. T ⊢G [Hypothesis]
    3. #(G)∈Cn(T) [from previous line, by definition of Cn(T)]
    4. #(G)∈Cn(T⋃Q) [as Cn(T)⊂Cn(T⋃Q)]
    5. Q ⊢BewT⋃Q[c:=#(G)]) [from A. above]
    6. Q ⊢¬G [from lines 1 and 5, via Modus Ponens]
    7. T⋃Q ⊢¬G [as Q⊂T⋃Q]
    8. T⋃Q ⊢¬G [from line 2, as Q⊂T⋃Q]

    Hence T⋃Q⊢(G→(G⋀¬G)), so if T⋃Q is consistent, we must have:

    9. T⋃Q⊬G

    However it then follows that:

    10. #(G)∉Cn(T⋃Q) [from previous line, by definition of Cn(T⋃Q)]
    11. Q ⊢¬BewT⋃Q[c:=#(G)] [from B. above]
    12. Q ⊢G [by lines 1 and 11, via Modus Ponens]
    13. T⋃Q ⊢G [from previous line, as Q⊂T⋃Q]

    So we have (T⋃Q⊢G)⋀¬(T⋃Q⊢G), which is a contradiction outside T.

    Hence we must conclude that one of the assumptions we have made is false. If we insist on retaining the assumption of consistency then the only other available assumption is the one that Cn(T⋃Q) is recursive, so we must reject that assumption.

    A bit more argument, which I've omitted here, shows that if Cn(T⋃Q) is not recursive then neither is Cn(T).

    That means that T is undecidable and if we assume T is axiomatisable then it follows that T is not complete.
  2. jcsd
  3. Oct 26, 2012 #2
    Maybe it would be easier if you just put your questions concerning the proof of Godel's theorem in a single thread?

    Anyway, Rosser's trick is used in the proof of the Representability Theorem. Without Rosser's trick, you would get the Representability Theorem in the following form:

    #(θ)∈Cn(T⋃Q)) ⇒ (Q⊢BewT⋃Q[c:=#(θ)]
    #(θ)∉Cn(T⋃Q)) ⇒ ¬ (Q⊢BewT⋃Q[c:=#(θ)]

    rather than in the form that you use:

    #(θ)∈Cn(T⋃Q)) ⇒ (Q⊢BewT⋃Q[c:=#(θ)]
    #(θ)∉Cn(T⋃Q)) ⇒ (Q⊢¬BewT⋃Q[c:=#(θ)]
  4. Oct 27, 2012 #3


    User Avatar
    Science Advisor
    Homework Helper
    Gold Member

    Thanks Preno. I thought it might be in the Representability Theorem. I'll go and work through the version of the proof of that that I have, now, to see if I can find where either omega-consistency is used or Rosser's Trick is built in.

    If I have more questions I'll just start a thread called "Questions about Godel's Incompleteness Theorem" and put them there. I'd rename this thread to that but the OP is already locked. They lock posts quickly around here.
Share this great discussion with others via Reddit, Google+, Twitter, or Facebook