### C1.2 Gödel's Incompleteness Theorems (2023-24)

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: Hilary
Course Lecture Information: 16 lectures.
Course Weight: 1
Course Level: M
Assessment Type: Written Examination
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.