Gödel's Third Incompleteness Theorem

In a note appended to the translation of "On consistency and completeness" (), Gödel reexamined the problem of the unprovability of consistency. Gödel here focuses on an alternative means of expressing the consistency of a formal system, in terms of what would now be called a 'reflection principle', roughly, the assertion that a formula of a certain class is provable in the system only if it is true. Gödel suggests that it is this alternative means of expressing consistency that we should be interested in from a foundational point of view, and he gives a result that shows certain reflection principles to be underivable in extensions of elementary number theory under conditions significantly weaker than the Hilbert-Bernays derivability conditions. In this paper I shall discuss the background to Gödel's result and the foundational significance he claims for it. Along the way, I shall present a new proof of the result which places it in an even more general context than the one considered by Gödel in the 1960s.