On Formally Undecidable Propositions of Principia Mathematica and Related Systems
In any rich enough system of arithmetic, there are true statements it can never prove.
Gödel proved that any rulebook big enough to do ordinary arithmetic must leave some true facts forever unprovable — and that it can never vouch for itself.
The idea, unpacked
For decades, mathematicians chased a beautiful dream — often called Hilbert's programme: write down a set of starting rules so airtight that, in principle, every true statement about numbers could be reached just by grinding through them. Gödel proved the dream impossible. Any system strong enough to handle ordinary arithmetic must contain statements that are true but unprovable inside it.
His method was as startling as his conclusion. He found a way to turn every formula and every proof into a number — so a sentence about numbers could secretly be a sentence about what the system can prove. With that, he built a sentence that, decoded, says “This sentence cannot be proved here.” If the system proves it, the system has proved a falsehood. If it can't, the sentence is true but out of reach. Either way there is a gap — and patching it by adding rules only opens a new one.
Where it came from
In 1930, at a conference in Königsberg, the 24-year-old Kurt Gödel quietly announced a result that upended the foundations of mathematics — just as David Hilbert was restating his confident programme to put all of it on certain ground. Gödel's paper appeared the next year in a Vienna journal, dense with a new technique for making arithmetic talk about itself. The field took years to absorb it; today it is regarded as one of the most important theorems in the history of logic.
Why it mattered
Gödel drew a permanent line around what proof can do. No formal system can be at once complete, consistent, and able to certify itself — a humbling limit that reshaped mathematics and philosophy alike. And the very trick at its heart, self-reference made rigorous, became the seed of computer science: the same idea shows there are problems no program can ever solve.
A sentence that trips itself
Think of the old paradox “This sentence is false.” If it's true it's false, and if it's false it's true — it spins forever. Gödel's genius was to swap one word: instead of “false,” his sentence says “not provable.” That small change turns a useless paradox into a precise theorem — the sentence ends up true, yet unprovable. Build it yourself below and watch the trap close.
Where you'll meet it again
Gödel's self-reference echoes far beyond logic. It is the direct ancestor of Alan Turing's proof that no program can decide, in general, whether another program will halt — the bedrock result of theoretical computer science — and it surfaces whenever a task turns out to be provably impossible to automate. It's also why no single system of rules, however clever, can be the final word on mathematical truth.
The formalization of mathematics
Theorem VI — the undecidable proposition
To every ω-consistent recursive class κ of formulae there correspond recursive class-signs r, such that neither v Gen r nor Neg (v Gen r) belongs to Flg(κ) (where v is the free variable of r).
A proposition that asserts its own unprovability
The analogy of this argument with the Richard antinomy leaps to the eye. It is closely related to the “Liar” too; for the undecidable proposition [R(q); q] states that q belongs to K, i.e. … that [R(q); q] is not provable. We are therefore confronted with a proposition which asserts its own unprovability.