In 1931, the great German logician Kurt Gödel published his paper "On Formally Undecidable Propositions of Principia Mathematica and Related Systems I". This paper contained the proof of Gödel's celebrated incompleteness theorems. The first of these stated that, in any axiomatic theory of sufficient strength, there will always be a statement that is undecidable by the theory, in the sense that the theory neither proves nor refutes this statement. The second states that no axiomatic theory of sufficient strength proves its own consistency.
These two results, and the techniques used in their proof, have had a major influence on the development of mathematical logic. Part of our purpose in this course will be simply to understand them.
The first incompleteness theorem underwent significant refinement in the years following Gödel's original publication. What is now its standard statement did not really emerge, however, until work by Tarski, Mostowski, and Robinson in the 1950s. We will read their book, in part as a way of becoming familiar with the important notion of interpretation.
Our main focus, though, will be on the second incompleteness theorem: the one concerned with consistency. This result is, in some ways, puzzling. For it turns out that it is extremely sensitive to questions about how notions like proof and theory are formulated. There are ways of formalizing these notions that are extensionally correct, in the sense that they get the set of proofs and theorems right, but that seem to allow theories to prove their own consistency that are not supposed to be able to do so. We will look at early work on this issue and then at some more recent work that seeks to refine our understanding of the insight the theorem seems to give us.