"The most comprehensive formal systems that have been set up hitherto are the system of Principia Mathematica(PM) on the one hand and the Zermelo-Fraenkel axiom system of set theory (further developed by J. von Neumann) on the other. These two systems are so comprehensive that in them all methods of proof today used in mathematics are formalized, that is, reduced to a few axioms and rules of inference. One might therefore conjecture that these axioms and rules of inference are sufficient to decide any mathematical question that can at all be formally expressed in these systems. It will be shown below that this is not the case ...This situation is not in any way due to the special nature of the systems that have been set up but holds for a wide class of formal systems..."
On Formally Undecidable Propositions of Principia Mathematica and Related Systems I
It was with these words that Goedel announced what he was going to demonstrate. As if by magic, Goedel maps statements within formal system to statemens ABOUT statements within formal systems. Thus, Goedel demonstrates that certain true propositions in the language map to true assertions that they are unprovable -- assuming, of course, the formal system is consistent. Goedel begins by giving a sketch of the main idea of the proof. In the below, we will use Principia Mathematica (PM) as the formal system.
The basic signs of PM are mapped onto numbers in an ingenious way, so that proposiions, like, "2+2=4", are mapped to a number. A more complicated expression, like "If x and y are bigger than z and w, then x+y is bigger than z+w" is also mapped to a number, and is mapped in such a way that the number, as well as it decomposition into factors, expresses important facts about the proposition, most relevantly for our purposes the fact that the proposition is provable within PM. What Goedel demonstrates is that there are some propositions that map to numbers in such a way that these numerical relationships reveal the unprovability of the proposition within PM.
Goedel expresses this in his sketch of the main proof by defining a class K of natural numbers defined in such a way that the natural number n is in the class K if and only if the statement identified by that number is unprovable. The way we get an unprovable proposition is to define a proposition S, interpreted in PM to mean that its corresponding number, call it q, belongs to the class K. Now, suppose S is provable, then it would be true, which would mean that q belongs to K, which means that S is unprovable. On the other hand, if the negation of S is provable, then q does not belong to K, in which case S is provable. So, if S is provable it is unprovable, a contradiction; if negation S is provable, then S is provable, a contradiction. Thus, S is undecidable.
Here we can see the sort of thing Hofstadter is going to make a big deal of: from statements about numbers in PM we are able to get layers of meaning about statements, including proofs that statements themselves are unprovable. These "meta" statements are seen to emerge out of the strange loop structure.
In future posts I will work carefully through Goedel's proof of undecidable propositions and also the fact that these systems cannot prove their own consistency.