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

[andrewkirk]

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.

Proof
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 Bew_T⋃Q in wff(L_N) with one free variable, say c, such that, for any θ in wff(L_N):

A. (#(θ)∈Cn(T⋃Q)) ⇒ (Q⊢Bew_T⋃Q[c:=#(θ)] and
B. (#(θ)∉Cn(T⋃Q)) ⇒ (Q⊢¬Bew_T⋃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 Bew_T⋃Q from being a simple infinite list of all numbers in Cn(T⋃Q). Bew_T⋃Q doesn't have to be recursive, but it must be concise.

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

1. Q ⊢ (G↔¬Bew_T⋃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 ⊢Bew_T⋃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 ⊢¬Bew_T⋃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.

 

[Preno]

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:=#(θ)]

 

[andrewkirk]

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.