Q.E.D.Undecidability of Q: Proving Godel's First Incompleteness Theorem

[andrewkirk]

Undecidability of Q

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 S, define:
Cn(S) = {#(θ) : Sentence(θ) ⋀ (S⊢ θ)}
where #(F) denotes the Godel number of formula F and Sentence(ψ) means that ψ is a well-formed sentence in formal language 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):
(#(θ)∈Cn(T⋃Q)) ⇒ (Q⊢Bew_T⋃Q[c:=#(θ)] and
(#(θ)∉Cn(T⋃Q)) ⇒ (Q⊢¬Bew_T⋃Q[c:=#(θ)]).
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)]) [by definition of Bew_T⋃Q]
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)] [by definition of Bew_T⋃Q]
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.