TLDR
- In any consistent formal system that’s strong enough to do basic arithmetic, there are true statements it can’t prove. (First incompleteness)
- Such a system also can’t prove its own consistency. (Second incompleteness)
Gödel numbering: Assign a unique natural number to every symbol, formula, and proof in your system. Now the system can make arithmetic statements that are secretly about itself. Gödel constructs a formula that, when decoded, says “there is no proof of .” If the system proved , it would be inconsistent. If it’s consistent, is true but unprovable.
What counts as “strong enough”? The system needs addition and multiplication on natural numbers. This is enough to encode any finite sequence of symbols as a number (via prime factorization), enabling self-reference. Weaker systems (e.g., Presburger arithmetic with only addition) are complete and decidable because they can’t encode their own syntax.
The halting problem is closely related: if you could decide all arithmetic truths, you could solve the halting problem (encode Turing machines as numbers, encode “this machine halts” as an arithmetic statement). Since halting is undecidable, so is arithmetic truth.
Note: incompleteness is about what’s true in vs provable from axioms. This is different from the completeness theorem, which says every semantic consequence of your axioms is provable. See sequent calculus for how these fit together.