TheoremProved

Gödel's first incompleteness theorem

Statement

In any consistent formal system $F$ powerful enough to express basic arithmetic (e.g. containing Peano arithmetic) whose axioms can be listed by an algorithm, there is a sentence $G$ that is true but can neither be proved nor disproved within $F$ .

Why is it true?

Gödel builds a sentence that, via a numbering of formulas and proofs (Gödel numbering) turning statements about provability into statements about numbers, effectively says of itself 'I am not provable in $F$ '. If $F$ could prove $G$ , $F$ would be inconsistent (proving a false statement); if $F$ could prove $\neg G$ , $F$ would again prove something false. So $G$ is true but undecidable inside $F$ .

Proof sketch

Assign every formula and every finite sequence of formulas (candidate proof) a unique natural number (Gödel numbering); express the relation 'the number $y$ codes a proof of the formula coded by $x$ ' as a decidable arithmetic relation $\mathrm{Prf}(y,x)$ ; use a diagonal construction to build a sentence $G$ that, unwound, asserts $\neg\exists y\, \mathrm{Prf}(y,\ulcorner G\urcorner)$ (no number codes a proof of $G$ ); then a case analysis on $F\vdash G$ versus $F\vdash\neg G$ shows the first contradicts consistency and the second contradicts $\omega$ -consistency (weakened to plain consistency by Rosser's refinement), so $F$ proves neither, while $G$ is true.

Proved by

proved 1931Kurt Gödel

Topics that use this theorem

Gödel's incompleteness theorems Predicate logic

Related theorems

Gödel's second incompleteness theorem Gödel's completeness theorem Undecidability of the halting problem

Step-by-step proofs

No step-by-step proof yet for this theorem.

References

Kurt Gödel (1931). Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I · DOI:10.1007/s00605-006-0423-7
Ernest Nagel, James R. Newman (2001). Gödel's Proof