Maybe It Is True — But You Can't Prove It!
2 min read
Core idea
David Hilbert's program aimed to put mathematics on a perfectly secure footing: axiomatize all of it, then prove the axiom system consistent. Kurt Gödel showed, in 1931, that the first step is impossible — not even arithmetic (the truths about the natural numbers 0, 1, 2, ...) can be fully axiomatized.
What an axiom system is
An axiom system has a set of axioms (accepted without proof) and rules of deduction. A proof is a sequence of statements, each an axiom or deducible from earlier ones; its theorems are what the proofs end with. The system is complete if it can prove every true sentence of its language.
Gödel's verdict
Priest's argument: Though there may be axiom systems capturing some truths of arithmetic, there is no axiom system capturing all of them — any such system must be incomplete.
The self-referential sentence
Statements, programs, and proofs are all sequences of symbols, so all can be coded as numbers. The relation "x is the code of a proof of the statement coded y" is itself expressible inside arithmetic. By an ingenious construction, Gödel built a sentence G whose meaning is, in effect: this very sentence is not provable in the system. If G were provable it would be false, making the system inconsistent. So, assuming consistency, G is unprovable — and therefore true, exactly as it says.
Why it matters
Incompleteness drew a permanent boundary around the axiomatic method. It killed Hilbert's program: arithmetic cannot be captured by any complete axiom system, and Gödel's second incompleteness theorem adds that a consistent system cannot even prove its own consistency. The result follows directly from the halting theorem — if arithmetic were completely axiomatizable, you could decide the halting problem, which is impossible. G is a close cousin of the liar paradox, a reminder that self-reference lurks near the foundations of mathematics.
Key takeaways
Mental model
Practical application
Example
Picture a "complete rulebook" for a board game that claims to settle every possible position as a win, loss, or draw. Gödel's lesson is that you could construct a legal position the rulebook describes but never adjudicates — a position whose verdict is determinate yet outside the rulebook's reach. Bolting that one verdict on as a new rule does not close the loophole: the enlarged rulebook admits a new position it cannot decide. Provability inside a system always trails truth.
Related lessons
Related concepts
- Incompletenesslinked concept
- Godel Incompletenesslinked concept
- Provabilitylinked concept
- Formal Systemlinked concept