Best known theory for proving statements about natural numbers

Gödel's incompleteness theorems imply that there is no consistent theory that can be effectively generated and contains all true statements about the natural numbers.

Well, what known consistent theory with recursively enumerable theorems can prove the most true statements about the natural numbers as defined by true arithmetic (or perhaps some other similar theory)? What's the best we can do?

• The one that contains all of them as axioms. (I guess you want an effectively generated theory too. I don't think there is a "best" theory here in the sense that given any effectively generated consistent theory $T$ that talks about the natural numbers, the theory $T + \text{Con}(T)$ proves strictly more statements about the natural numbers.) – Qiaochu Yuan Aug 7 '11 at 14:41
• ZFC with some large cardinal axioms added. – André Nicolas Aug 7 '11 at 14:52
• To elaborate on Qiaochu Yuan's comment : What do you mean by the natural number. If you mean $\omega$ (or any model of Peano arithmetics), then $Th(\omega)$ can prove everything that is true in the model $\omega$. $Th(\omega)$ is also complete and consistent. However, Peano's Arithmetic (the theory) is not complete in the sense that it can not prove for all statements either the statement or its negation. – William Aug 7 '11 at 15:00
• Or maybe you mean "true statements that we care about." In that case I think PA is expected to be enough for quite a lot already. – Qiaochu Yuan Aug 7 '11 at 16:29
• Do you mean the best known consistent theory which can prove the most true statements about the natural numbers, or the best known theory? The questions differ significantly, since if we have classical logic at work, then any inconsistent theory can prove every true statement about the natural numbers. So, every inconsistent theory (with classical logic at work) qualifies as "the best" by that criterion. – Doug Spoonwood Aug 7 '11 at 16:39

For brevity's sake, say that a theory $T$ is nice if $T$ is a consistent theory that can interpret Peano Arithmetic and admits a recursively enumerable set of axioms. For any such $T$, the statement "$T$ is consistent" can be coded as an arithmetic statement (saying that no number codes a proof of a contradiction from the axioms of $T$). What Gödel's theorem actually shows is that this statement is not provable in $T$.

This shows that there is no "best" theory or one that can do "the most" in the sense you describe, as given any true nice theory $T$ ("true" in the sense that all arithmetic consequences of $T$ are true in the standard model of arithmetic), $T$ +"$T$ is consistent" is also true and nice, and proves more arithmetic statements.

One could think of perhaps iterating this procedure and taking a limit. For any recursively enumerable sequence of true nice theories, however, one can find another theory $T$ that is also nice and true, and proves all the arithmetic statements that the theories in the sequence prove, so we can again go beyond this "limit" as in he previous paragraph.

(A good reference for these topics is "Aspects of Incompleteness" by Per Lindström.)

In fact, note how frustrating (?) the situation is, in that the sentence we found that the theory cannot prove is $\Pi^0_1$, as simple as possible in the natural complexity hierarchy. As explained in the book "Metamathematics of first-order arithmetic" by Petr Hájek and Pavel Pudlák, even adding to PA all its true $\Pi^0_1$ consequences (and therefore losing that it is r.e.) does not give us a complete theory. Many natural (combinatorial) examples of independent statements (on hydra games, Goodstein sequences, etc) are independent of this theory, and are $\Pi^0_2$, as simple as possible.

Gödel proved some very nice speed-up theorems, discussed in detail by Samuel Buss, see the relevant papers on his page: "On Gödel's theorems on lengths of proofs I: Number of lines and speedups for arithmetic", Journal of Symbolic Logic 39 (1994) 737-756; and "On Gödel's theorems on lengths of proofs II: Lower bounds for recognizing k symbol provability", in Feasible Mathematics II, P. Clote and J. Remmel (eds), Birkhauser, 1995, pp. 57-90.

What these theorems say is that not only the theory $T$+"$T$ is consistent" proves more arithmetic statements, but there are proofs in $T$ that require an absurd number of steps and can be proved very quickly in the new theory, so even if we cannot find a "best" theory, there is a point in looking for "better" ones.

In the comments to the question I see that large cardinals are suggested. Any particular large cardinal axiom we adopt beyond ZFC (that does not result in an inconsistent theory) will result in a theory to which Gödel's theorem applies, and so it can be transcended just as before. But there is a point to the program of extending ZFC with large cardinals. For example, we have deep theorems explaining how the arithmetic consequences of a large cardinal axiom $A$ are extended by those of a large cardinal axiom $B$ precisely if $B$ is in "consistency strength" stronger than $A$. These theorems (for the large cardinals studied so far) suggest clear lines along which to continue research on large cardinals (for example, we expect this feature to be continued by all further large cardinal axioms people may suggest in the future). There are much stronger "absoluteness" and "correctness" results associated with large cardinal axioms as well. Some of them are discussed at length in some questions at MO, see for example this one.