Questions about godel's first incompleteness theorem

Question

I'd rather not get into the formal proof of godel's first incompleteness theorem. But I have 2 general questions. Looking at the statement from wikipedia:

http://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems#First_incompleteness_theorem

"Any effectively generated theory capable of expressing elementary arithmetic cannot be both consistent and complete. In particular, for any consistent, effectively generated formal theory that proves certain basic arithmetic truths, there is an arithmetical statement that is true,[1] but not provable in the theory (Kleene 1967, p. 250)."

My first question is this... is "any consistent, effectively generated formal theory" something that can be defined and referred to? This seems problematic to me... because then we'd have self-reference wouldn't we... what about the theory from which the theorem is being stated? Meaning isn't the godel incompleteness theorem stated and proved from within a theory capable of expressing elementary arithmetic... and the theorem is referring to the theory within which it is expressed... isn't this a problem.

My second question is related to the first... if I prove godel's incompleteness theorem... it seems I cannot prove it for the very theory within which I state the theorem. Because if I did that, the so-called Godel statement would be proved true within the theory within which I'm operating... which is supposed to be impossible. So it seems to me Godel's incompleteness theorem itself is unprovable except with regards to theories within the theory I'm operating under.

Appreciate any clarification.

Answer 1

For simplicity, I'll treat Rosser's improvement of Godel's original theorem below. In particular, "Godel sentence" should really be "Godel-Rosser sentence." This survey of Beklemishev is also a great source, once you understand the basic distinction between Godel's theorem as a global result about all appropriate theories and each particular instance of Godel's theorem.

---

is "any consistent, effectively generated formal theory" something that can be defined and referred to?

Yes. In particular, "effectively generated" may sound like an informal term, but it's not; more common equivalent phrasings are "computably axiomatizable" and "recursively axiomatizable," and we can talk about computable sets of sentences via Godel numbering and the $T$-predicate. (That's ahistorical, since the $T$-predicate postdates Godel's argument, but from a modern perspective this is the right way to think about things.)

because then we'd have self-reference wouldn't we

Part of the takeaway of Godel is that self-reference isn't inherently problematic. The diagonal lemma (which again was only proved in full generality post-Godel, but whatever) says exactly that a certain amount of self-reference is in fact unavoidable. Not all sets of sentences in the language of arithmetic are definable in the language of arithmetic (see Tarski for a particularly interesting example), but many are - including all computably axiomatizable theories.

isn't the godel incompleteness theorem stated and proved from within a theory capable of expressing elementary arithmetic... and the theorem is referring to the theory within which it is expressed...

Yes. First-order Peano arithmetic, $\mathsf{PA}$, is strong enough to prove Godel's incompleteness theorem (and is in fact massive overkill for this task).

isn't this a problem.

No.

if I prove godel's incompleteness theorem... it seems I cannot prove it for the very theory within which I state the theorem. Because if I did that, the so-called Godel statement would be proved true within the theory within which I'm operating... which is supposed to be impossible.

Godel's incompleteness theorem is the statement "Every computably axiomatizable theory which is consistent fails to decide its Godel sentence." That highlighted bit is fundamental. For example, $\mathsf{PA}$ can prove that statement and so consequently can prove (since it knows it is computably axiomatizable) "If $\mathsf{PA}$ is consistent then $\mathsf{PA}$ doesn't decide its Godel sentence." However, we can't go from that to $\mathsf{PA}$ deciding its Godel sentence without first proving inside $\mathsf{PA}$ that $\mathsf{PA}$ is consistent. In fact, this is how we get the second incompleteness theorem (which similarly is provable, in its general conditional form, in $\mathsf{PA}$)!