# Questions about godel's first incompleteness theorem

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, 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.

• The theorem can be proved within quite a weak theory, but I do not consider that particularly interesting. If it were a result about partial differential equations, everybody would understand that all mathematical tools are permitted. It happens to be a theorem about certain kinds of formal theories. Again, all mathematical tools are permitted. – André Nicolas Oct 30 '14 at 19:16
• I guess my question is... is the theory from within which godel's incompleteness theorem is being stated and proved... totally different from these "effectively generated theories" that the theorem is talking about? Or is it incorrect to say that godel's incompleteness theorem is being proved from within a theory? When humans prove things are they operating from within a theory... – Ameet Sharma Oct 30 '14 at 19:37
• In principle the theorem has a "finitary" proof. Some people with finitary leanings consider that a good thing. When humans prove things they are usually not operating within a formal theory. However, it is well-known that almost all of mathematics can be done within ZFC. – André Nicolas Oct 30 '14 at 20:54