Gödel’s incompleteness theorems
Foundations and logic
Two results of Kurt Gödel (1931). First: any consistent, effectively axiomatised formal system strong enough to express basic arithmetic contains statements true of the natural numbers that it cannot prove. Second: no such system can prove its own consistency.
What is usually left out
Every condition is load-bearing. Consistency is required because an inconsistent system proves everything. Effective axiomatisation is required because true arithmetic — the set of all true statements about the naturals — is complete but has no algorithmically listable axioms. And the system must express enough arithmetic; simpler theories such as Presburger arithmetic are complete and decidable.