Gödel's incompleteness theorems

前置知识

24 项必需的前置知识（一直追溯到底）

你将学会

• Explain how formulas and proofs are coded by natural numbers and why provability is expressible in arithmetic.
• Prove the diagonal lemma and derive the first incompleteness theorem, in Rosser's form, for consistent recursively axiomatised theories extending Robinson arithmetic Q.
• State the second incompleteness theorem and Tarski's theorem, and explain precisely what they do and do not say.

定义

• A theory is recursively axiomatised if its set of axioms is decidable.
• Robinson arithmetic Q is a weak, finitely axiomatised fragment of Peano arithmetic (PA) without the induction schema.
• Diagonal lemma: for every formula φ(x) there is a sentence G such that the theory proves G ↔ φ(⌜G⌝), where ⌜G⌝ is the numeral of G's code.

定理

• First incompleteness theorem (Gödel 1931; Rosser 1936): every consistent, recursively axiomatised theory extending Q is incomplete.
• Second incompleteness theorem: a consistent, recursively axiomatised theory extending PA does not prove its own (standard) consistency statement.
• Tarski: the set of true sentences of arithmetic is not definable in arithmetic.
• Presburger arithmetic (addition only) and the theory of real closed fields are complete and decidable, so incompleteness needs enough arithmetic.

常见误解

• Claiming Gödel showed that 'some truths can never be known'; the theorems concern provability in a fixed formal theory.
• Applying the theorems to theories that are not recursively axiomatised or cannot interpret enough arithmetic.
• Thinking the second theorem leaves PA's consistency wholly unsupported; it can be proved in stronger systems, for example by Gentzen's method using induction up to ε₀.

通向

可选发现

• Large cardinals If ZFC is consistent it cannot prove that an inaccessible cardinal exists, because such a cardinal κ would give a model V_κ of ZFC and hence prove Con(ZFC).
• ← True, false, and, or, not
• ← Countability and Cantor's diagonal argument

延伸阅读

• Peter Smith, An Introduction to Gödel's Theorems (2007)
• George S. Boolos, John P. Burgess and Richard C. Jeffrey, Computability and Logic
• Herbert B. Enderton, A Mathematical Introduction to Logic (1972)