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 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.
