This is a series on the book Gödel, Escher, Bach: An eternal golden braid by Douglas Hofstadter.
Earlier diaries are here
Today, we will examine On formally undecidable propositions of TNT and related systems p. 439 - 460.
This chapter isn't very long, but it's very dense, and will take some very slow reading (at least, I had to read it slowly!) But it repays slow, careful reading, as it gets at the key idea of Godel's proof.
From the overview
This Chapter's title is an adaptation of the title of Godel's 1931 article, in which the Incompleteness Theorem was first published. The two major parts of Godel's proof are gone through carefully. It is shown how the consistency of TNT forces one to conclude that TNT (or any similar system) is incomplete. Relations to Euclidean and non-Euclidean geometry are discussed. Implications for the philosophy of mathematics are gone into with some care
On page 438, DH says that this chapter is "more intuitive" than Godel's paper; undoubtedly true. But maybe not quite intuitive enough?
My view of the central idea is as follows:
You can make statements IN number theory that are ABOUT number theory, and one statement you can make is "This string is not a theorem". This brings the paradox of "this statement is false" into any formal system that is sophisticated enough to express it. BOOM.
Then we have to show that each of the parts of this idea are correct:
a) you can make statements about number theory IN number theory
b) you can make a statement "this string is not a theorem".
The first thing DH introduces is proof-pairs. Here's the idea:
- In any formal system, change the rules to rules of arithmetic. (DH did this in Chapter 9).
- Express a derivation of a theorem in arithmetic (this will be a VERY LONG number, but it doesn't matter).
- A proof pair two numbers: The first is that huge number, the second is what we set out to prove.
The next key idea is to distinguish between a proof pair and a proof. Proof pairs can be analyzed in a finite number of steps .... maybe a huge number, but a finite number. Therefore, they can be represented by TNT, and there is a TNT number for PROOFPAIRNESS. But the general concept of proving a theorem can NOT be analyzed in a finite number of steps, there is NO TNT number for this. It's the difference between:
This is a proof of X
X can be proven
On p. 442, one might wonder why 666,111,666 zeroes .... well, by the coding scheme:
666 is 0
111 is =
666 is 0
so, the text
there exists a such thatt TNTPROOFPAIR(a, SSSS....0/a')
is saying what DH has right above "There exists a number a which forms a proof pair with 666,111,666 as its second element" which means that there is a proof of 0 = 0.
On p. 444, near the bottom, here's what I made of the two strings.
- means (a + a) = SSSS0
SS0 + SS0 = SSSS0
that is, the following derivation:
a + a = 4
a = 2
2 + 2 = 4
- means ~(a*a)=a'
~(S0*S0) = a'
a*a does not equal a'
a = 1
1*1 not equal a'
the latter is incorrect - it does not simply substitute 1 for all free variables.
On p. 449, Godel's second theorem - either G or ~G must be correct, but neither is a theorem, so the system is incomplete.
The supernatural numbers are really cool.