proof theory
Gödel's Incompleteness Theorems
You should know: soundness and completeness
Overview
Gödel's two incompleteness theorems (1931) are among the most significant results in mathematical logic. The first incompleteness theorem states that any consistent formal system F that is recursively axiomatizable (its axioms can be listed by an algorithm) and strong enough to express basic arithmetic (e.g. Peano arithmetic or anything encoding it) contains true statements about the natural numbers that F cannot prove or disprove. The second incompleteness theorem, a corollary of the first's proof method, states that such a system F cannot prove its own consistency (a statement 'Con(F)' expressible within F itself) unless F is actually inconsistent. These theorems apply specifically to sufficiently powerful, recursively axiomatizable, consistent formal systems — not to every conceivable formal or informal system, and not to logic in general (they do not contradict Gödel's own 1930 completeness theorem for first-order logic, which is a separate, different-scope result).
Intuition
Gödel's trick was to build, using a technique now called Gödel numbering, a statement G_F inside arithmetic itself that effectively says 'I am not provable in F' — a mathematical cousin of the liar paradox ('this sentence is false'), but carefully engineered to be a legitimate, meaningful arithmetic claim rather than a paradox. If F could prove G_F, then F would be proving something false (since G_F asserts its own unprovability), breaking soundness; if F could disprove G_F (prove ¬G_F), then F would be proving something false in the other direction. So a consistent F can do neither — meaning G_F sits there, true (we can see this from outside the system) but forever unprovable from within it. This isn't a flaw specific to one clumsy system; it's a structural limit on any system rich enough to talk about its own arithmetic, which is why it applies broadly to ZFC, Peano arithmetic, and any similarly powerful, honestly-axiomatized theory — but not to weaker systems (like Presburger arithmetic, which lacks multiplication and is actually complete) or to systems that are inconsistent to begin with.
Formal Definition
For a consistent, recursively axiomatizable formal system F capable of expressing arithmetic:
Worked Examples
G_F is constructed to assert (via Gödel numbering) 'G_F is not provable in F.'
Suppose F ⊢ G_F. Then F proves a statement that itself claims to be unprovable in F — meaning F proves something false about itself (since it just proved it), which contradicts F's soundness/consistency.
Answer: If F is consistent (and sound with respect to arithmetic truth), F cannot prove G_F, since doing so would falsify what G_F itself asserts.
Practice Problems
Does Gödel's first incompleteness theorem apply to every formal system whatsoever, including trivial or very weak ones?
Why can't a system F use the second incompleteness theorem to conclude it is inconsistent by 'proving' Con(F) is unprovable and treating that as evidence?
Explain why Gödel's incompleteness theorems do not contradict his own 1930 completeness theorem for first-order logic.
Quiz
Summary
- The first incompleteness theorem: any consistent, recursively axiomatizable system expressive enough for arithmetic has true statements it cannot prove or disprove.
- The second incompleteness theorem: such a system cannot prove its own consistency from within itself, unless it is actually inconsistent.
- These results apply specifically to sufficiently powerful, honestly-axiomatized systems like Peano arithmetic or ZFC — not to every formal system, and they do not contradict Gödel's separate 1930 completeness theorem for first-order logic.
Mathematics