An ignorant question about the incompleteness theorem

Question

Let me preface this by saying that I have essentially no background in logic, an I apologize in advance if this question is unintelligent. Perhaps the correct answer to my question is "go look it up in a textbook"; the reasons I haven't done so are that I wouldn't know which textbook to look in and I wouldn't know what I'm looking at even if I did.

Anyway, here's the setup. According to my understanding (i.e. Wikipedia), Godel's first incompleteness theorem says that no formal theory whose axioms form a recursively enumerable set and which contain the axioms for the natural numbers can be both complete and consistent. Let $T$ be such a theory, and assume $T$ is consistent. Then there is a "Godel statement" $G$ in $T$ which is true but cannot be proven in $T$. Form a new theory $T'$ obtained from $T$ by adjoining $G$ as an axiom. Though I don't know how to prove anything it seems reasonably likely to me that $T'$ is still consistent, has recursively enumerable axioms, and contains the axioms for the natural numbers. Thus applying the incompleteness theorem again one deduces that there is a Godel statement $G'$ in $T'$.

My question is: can we necessarily take $G'$ to be a statement in $T$? Posed differently, could there be a consistent formal theory with recursively enumerable axioms which contains arithmetic and which can prove every true arithmetic statement, even though it can't prove all of its own true statements? If this is theoretically possible, are there any known examples or candidates?

Thanks in advance!

Answer 1

You are right that $T'=T+G$ must be consistent. If it were not, then we could prove a contradiction from $T$ together with $G$, which would amount to a proof by contradiction of $\neg G$ in $T$. But that contradicts the fact that $G$ is independent of $T$!

On the other hand, when you ask

Posed differently, could there be a consistent formal theory with recursively enumerable axioms which contains arithmetic and which can prove every true arithmetic statement, even though it can't prove all of its own true statements?

that cannot be, because the independent statement $G$ produced by Gödel's construction is always an arithmetic statement. ($G$ is often popularly explained as stating something about provability or not, which is correct so far as it goes -- but the major achievement of Gödel's work is to show how such claims can be expressed as arithmetic statements).

Indeed, if the original theory $T$ was something like Peano Arithmetic, the language of the theory does not allow one to even state any sentence that is not arithmetic -- and no amount of added axioms can change that.

Answer 2

Since the sentence $G$ that is added is a sentence of the language of $T$, the same diagonalization procedure that got you $G$ can be used to produce a sentence $G'$ of the kind you described. The language has not been extended, so $G'$ is definitely "a sentence of $T$." More properly put, it is a sentence of the language of $T$. (To say "sentence of $T$" could be taken to mean is a theorem of $T$, which is definitely not the case.)

As a part answer to your second question, the Incompleteness Theorem applies to any "strong enough" first-order theory. So there is no recursively axiomatized first-order consistent theory that proves all the sentences that are true in the natural numbers. Standard ZFC set theory is recursively axiomatized, so (if consistent) it is not strong enough to prove all sentences that are true in the natural numbers.

Answer 3

If you had a theory, $T$, with a recursively enumerable axiom set, and it completely resolved all arithmetic questions, then, if the set of arithmetic questions was recursively enumerable in $T$, you could recursively enumerate all the arithmetic statements in $T$ which are provable in $T$, and hence you'd have an r.e. enumeration of a set of complete and consistent arithmentical statements.

Therefore, if such a $T$ existed, the map of statements from Peano arithmetic statements to the equivalent statements in $T$ would have to be non-recursive.

One nice thing about having a recursively enumerable set of axioms is that we can enumerate the set of all proofs in our theory, $T$. If we have a recursively enumerable set of statements in such a theory, then the subset of such statements that can be proven is also recursively enumerable.