Stating Goedel's Theorem with Less Confusion

Here are Gödel's incompleteness theorems, according to Wikipedia:

The first incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an effective procedure (i.e., an algorithm) is capable of proving all truths about the arithmetic of natural numbers. For any such consistent formal system, there will always be statements about natural numbers that are true, but that are unprovable within the system. The second incompleteness theorem, an extension of the first, shows that the system cannot demonstrate its own consistency.

This is often summarized as saying that there are mathematical truths that cannot be proved.

The obvious implication is that logical proof from axioms is inadequate, as apparently there are other truths, and someone found them to be true somehow.

I think this is confusing. How do we know those truths are true, if no one can prove them?

Maybe it would be better to say: If an arithmetic system has a computable set of axioms, then there will be statements that are true in some models of the axioms, and false in others.

It is called "incompleteness", because a complete theory would be able to prove or disprove every statement from the axioms.

The point is that statements are true or false in some model, and the axioms allow many possible models.

You might think that arithmetic could be given a set of axioms such that only one model is possible. But you cannot, and that was known before Goedel.

Some say that Goedel proved that the axiomatic method does not work. But that is incorrect. The axioms do let you prove all the statements that are true in all the models.

This is an important point, that is worth repeating. The axiomatic method would be defective if there were some statements that were true in all the models, but still could not be proved from the axioms. Goedel proved that was not possible.

Here is a typical account, from a new paper:

In 1931 Kurt G ̈odel shook mathematics (literally) to its foundations with his incompleteness theorems:

I) No consistent finite set of axioms and rules11 can be used to prove all true theorems about the integers.

Even worse:
II) No consistent finite set of axioms and rules can prove itself to be consistent!

(1I am avoiding necessary subtleties. To be more precise, G ̈odel’s theorem can be stated as: The set of provable statements, although not recursive, is recursively enumerable, whereas the set of true statements is not.)

This absolutely contradicts Hilbert’s dream that one could axiomatize so as to prove or disprove any given mathematical claim. The first is frustrating, while the second unveils inescapable limitations in the possible formulation of axiomatic theories and indeed mathematical foundations:

Formal, axiomatic set theory ... cannot be a final foundational theory for mathematics, [yet] nothing else [can] be. Hallett [30]

Or as von Neumann put it in 1930:

There can be no rigorous justification for classical mathematics.

So how do mathematicians deal with this existential crisis in their subject? The only answer is that they learn to live with it.12

A theorem is a proved statement. So I do not agree that not all true theorems can be proved. The theorems can be proved, by definition.

Nothing can prove itself consistent, because inconsistent theories can prove anything. Goedel adds a subtle twist to that, but proving self-consistency was hopeless anyway.

I tried to find the source of the von Neumann quote, but failed. He did some excellent work on axiomatizing mathematics, and justifying modern mathematics, so I doubt that he was saying that his own work was not rigorous.

This paper has a very nice summary of the recent history of mathematical proofs, including computer-assisted proofs and wrong proofs that got published. He even mentions a famous mathematician who thought that the foundation of math might be inconsistent!