Synopsis for Gödel's Incompleteness Theorems

Recommended Prerequisites

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

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.

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. -completeness and -completeness. The arithmetical hierarchy. -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 -completeness. Provability logic; the fixed point theorem. The -rule. The Bernays arithmetized completeness theorem; formally undecidable -sentences of arithmetic.

1. Lecture notes for the course.

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), pp. 44-49.