What incompleteness actually says

The inescapable conclusion seems to be that mathematicians do not use a knowingly sound algorithm to ascertain mathematical truth. We deduce that mathematical understanding—the means whereby mathematicians arrive at their conclusions with respect to mathematical truth—cannot be reduced to blind calculation!

We started from a deliberately simple question: can a machine tell, of every mathematical statement, whether it is true? Hilbert hoped the answer was yes. After following programs and Turing machines all the way into Peano arithmetic, we can say something sharper.

If a theory of arithmetic is consistent, recursively axiomatizable, and strong enough to talk about the halting of programs, then it cannot prove every true statement it can write down. The argument does not float in the abstract. We exhibited a particular Python program, godel_peano.py, whose behaviour translates into a Peano sentence that is true precisely because the program does not halt — and that sentence cannot be a theorem, or the program would halt after all.

The same idea generalizes. Any logical system that can encode “this program halts on the empty input,” and that can enumerate its own theorems, inherits the incompleteness of arithmetic. Soundness (theorems are true) and syntactic consistency (the system does not prove both a sentence and its negation) each yield a version of the result. Completeness, in the semantic sense we used throughout, is the casualty.

Two distinctions did most of the work, and they are easy to blur if one only meets incompleteness as a slogan.

The first is proof versus truth. A formula can be a correct claim about the numbers and still fail to appear at the end of any finite derivation from the axioms. $\textbf{BinarySum}$ made that gap concrete with a toy arithmetic; $\textbf{Peano}$ is the same phenomenon at full strength.

The second is programs versus machines. Once a Python interpreter and a single-tape Turing machine can simulate each other, we are allowed to write the self-referential constructions in ordinary code. That is not a shortcut around rigour: it is the Church–Turing thesis used as a licence to pick the model that humans can actually read.

None of this says that mathematics is broken, or that computers are useless at proving theorems. It says that no single recursively axiomatizable, consistent package of arithmetic axioms will ever be a complete decision procedure for the truths of arithmetic. If you want every true sentence, you cannot also demand a mechanical inventory of the proofs.

There is a natural next question we have not answered here: whether such a system can prove its own consistency (Gödel’s second theorem). The techniques of this series are aimed at that problem as well, but they belong to another story.