C1.2 Godel's Incompleteness Theorem (2019-2020)

Dr Robin Knight
General Prerequisites: 

This course presupposes knowledge of first-order predicate logic up to and including soundness and completeness theorems for a formal system of first-order predicate logic (B1.1 Logic).

Course Term: 
Course Lecture Information: 

16 lectures.

Course Weight: 
1.00 unit(s)
Course Level: 

Assessment type:

Course Overview: 

The starting point is Gödel's mathematical sharpening of Hilbert's insight that manipulating symbols and expressions of a formal language has the same formal character as arithmetical operations on natural numbers. This allows the construction for any consistent formal system containing basic arithmetic of a `diagonal' sentence in the language of that system which is true but not provable in the system. By further study we are able to establish the intrinsic meaning of such a sentence. These techniques lead to a mathematical theory of formal provability which generalizes the earlier results. We end with results that further sharpen understanding of formal provability.

Learning Outcomes: 

Understanding of arithmetization of formal syntax and its use to establish incompleteness of formal systems; the meaning of undecidable diagonal sentences; a mathematical theory of formal provability; precise limits to formal provability and ways of knowing that an unprovable sentence is true.

Course Synopsis: 

Gödel numbering of a formal language; the diagonal lemma. Expressibility in a formal language. The arithmetical undefinability of truth in arithmetic. Formal systems of arithmetic; arithmetical proof predicates. $\Sigma_0$-completeness and $\Sigma_1$-completeness. The arithmetical hierarchy. $\omega$-consistency and 1-consistency; the first Gödel incompleteness theorem. Separability; the Rosser incompleteness theorem. Adequacy conditions for a provability predicate. The second Gödel incompleteness theorem; Löb's theorem. Provable $\Sigma_1$-completeness. The $\omega$-rule. The system GL for provability logic. The fixed point theorem for GL. The Bernays arithmetized completeness theorem; undecidable $\Delta_{2}$-sentences of arithmetic.

Reading List: 

Lecture notes for the course.

Please note that e-book versions of many books in the reading lists can be found on SOLO and ORLO.

Further Reading: 
  1. Raymond M. Smullyan, Gödel's Incompleteness Theorems (Oxford University Press, 1992).
  2. George S. Boolos and Richard C. Jeffrey, Computability and Logic (3rd edition, Cambridge University Press, 1989), Chs 15, 16, 27 (pp 170-190, 268-284).
  3. George Boolos, The Logic of Provability (Cambridge University Press, 1993).