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).
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.
Dr Robin Knight
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.
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.