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:

1.  In any formal system, change the rules to rules of arithmetic.  (DH did this in Chapter 9).
1. Express a derivation of a theorem in arithmetic (this will be a VERY LONG number, but it doesn't matter).
1. 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
and
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.

1. means (a + a) = SSSS0

2
SS0 + SS0 = SSSS0

that is, the following derivation:
a + a = 4
a = 2
2 + 2 = 4

1. means  ~(a*a)=a'

1
~(S0*S0) = a'
that is
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.

#### Tags

EMAIL TO A FRIEND X
You must add at least one tag to this diary before publishing it.

Add keywords that describe this diary. Separate multiple keywords with commas.
Tagging tips - Search For Tags - Browse For Tags

?

More Tagging tips:

A tag is a way to search for this diary. If someone is searching for "Barack Obama," is this a diary they'd be trying to find?

Use a person's full name, without any title. Senator Obama may become President Obama, and Michelle Obama might run for office.

If your diary covers an election or elected official, use election tags, which are generally the state abbreviation followed by the office. CA-01 is the first district House seat. CA-Sen covers both senate races. NY-GOV covers the New York governor's race.

Tags do not compound: that is, "education reform" is a completely different tag from "education". A tag like "reform" alone is probably not meaningful.

Consider if one or more of these tags fits your diary: Civil Rights, Community, Congress, Culture, Economy, Education, Elections, Energy, Environment, Health Care, International, Labor, Law, Media, Meta, National Security, Science, Transportation, or White House. If your diary is specific to a state, consider adding the state (California, Texas, etc). Keep in mind, though, that there are many wonderful and important diaries that don't fit in any of these tags. Don't worry if yours doesn't.

You can add a private note to this diary when hotlisting it:
Are you sure you want to remove this diary from your hotlist?
Are you sure you want to remove your recommendation? You can only recommend a diary once, so you will not be able to re-recommend it afterwards.
Rescue this diary, and add a note:
Are you sure you want to remove this diary from Rescue?
Choose where to republish this diary. The diary will be added to the queue for that group. Publish it from the queue to make it appear.

You must be a member of a group to use this feature.

Add a quick update to your diary without changing the diary itself:
Are you sure you want to remove this diary?
 Unpublish Diary (The diary will be removed from the site and returned to your drafts for further editing.) Delete Diary (The diary will be removed.)
Are you sure you want to save these changes to the published diary?

#### Comment Preferences

• ##### Things are getting heavy(18+ / 0-)

Let's see what happens in the comments.

What are you reading will be moving to Wednesday mornings. Come and read!

• ##### I'm still not following, but thanks(5+ / 0-)

Well, GEB remains on my shelf, bookmark somewhere in the middle.  I dip into it between books, but at the moment I'm still on Macroscope.  Then some number theory, oy.

I may have to go back to your analysis of the chapter I'm on when I get there.

"What doesn't have credibility today is the truth." -- Bill Moyers, The Daily Show 6/22/05

• ##### It will be very hard, if not impossible,(4+ / 0-)

to follow these diaries without having read the book ... sorry.  Not sure what to do about that.

I liked Macroscope.

Are you studying number theory in school, or on your own?

Godel, Escher, Bach

is now open

[ Parent ]

• ##### I'm decades out of school but still learning(3+ / 0-)
Recommended by:

Oh, GEB is all the Number Theory I'm dealing with at the moment.  I find it amusing to go from hard science fiction to soft science:  Exercising the mind via fiction vs. coming to grips with Reality (tm).  Still, sometimes I need a cheat sheet for both.

"What doesn't have credibility today is the truth." -- Bill Moyers, The Daily Show 6/22/05

[ Parent ]

• ##### So, Bertrand Russell blew up Gottlob Frege's(11+ / 0-)

… big project that he had invested a lot of time in, and then Kurt Gödel blew up Bertrand Russell's big project that he had invested a lot of time in (Principia Mathematica)?

And, just around the time we humans invent machines that can do arithmetic at enormous speed, we also discover that this really ambitious and meaningful thing that philosophers always hoped we would be able to do with such machines isn't possible and never will be?

In other words, Gödel proved the mathematical equivalent of

No, you can't have a pony.

?

The Dutch kids' chorus Kinderen voor Kinderen wishes all the world's children freedom from hunger, ignorance, and war.

• ##### Yeah, you've summarized it neatly(8+ / 0-)

:-)!

But maybe the box quote should be

You can't prove if you have a pony

:-)

Also, some mathematician/philosopher types seem rather happy that no computer will ever be able to prove all of math.

Godel, Escher, Bach

is now open

[ Parent ]

• ##### Also, the "quining" business is tricky, but neat.(5+ / 0-)
Recommended by:
Ahianne, Dave in RI, plf515, linkage, Jimdotz

It seems related to what used to be a standard assignment in first-year computer science, namely to write a program that prints out an exact copy of itself.

The Dutch kids' chorus Kinderen voor Kinderen wishes all the world's children freedom from hunger, ignorance, and war.

[ Parent ]

• ##### Or, "I am not a pony in formal system F." n/t(5+ / 0-)
Recommended by:
Ahianne, Wee Mama, plf515, linkage, Jimdotz

The Dutch kids' chorus Kinderen voor Kinderen wishes all the world's children freedom from hunger, ignorance, and war.

[ Parent ]

• ##### Are we at the end of the line?(2+ / 0-)
Recommended by:

Godel had a great insight. Does that settle it? Could there be another?

In physics, we've thought we were at the end of the line a number of times. Now we're at uncertainty as a basic fact of life. But could there be a next?

Many things in the past were unimaginable .. until...

• ##### There's a big difference between(4+ / 0-)
Recommended by:
theran, Dave in RI, lotlizard, linkage

Newton and Godel ... and between Physics and Math.

Newton came up with a theory of gravitation that elegantly explained the facts at his disposal.  He didn't prove it, certainly not in the sense of the word that mathematicians use.  Godel, OTOH, did prove his theorem.

There will be further developments in mathematical logic and philosophy, but they won't disprove Godel; just as no one has disproved ancient proofs of the irrationality of the square root of 2.

Godel, Escher, Bach

is now open

[ Parent ]

• ##### I suppose ...(2+ / 0-)
Recommended by:

... I was thinking of an extension or another way of thinking about formal systems.

Within the terms of the system, I'm sure you're right (and I really don't have a good grasp of these things and, therefore, should probably keep my mouth shut). But I'm wondering if maybe there's a Johnson number (named for Ralph Johnson, currently thinking about the problem in a basement somewhere in Ohio who came up with it) or some other unimaginable thing like that that would put a new aha twist on the matter.

• ##### Stephen Wolfram's book "A New Kind of Science" -(1+ / 0-)
Recommended by:
plf515

Has anyone here read it? Is it really an exposition of the foundations of "a new kind of science"?
http://www.wolframscience.com/...

Could something like that, a paradigm shift, qualify as Dave in RI's "new aha twist"? Presumably, a "new kind of science" wouldn't change Gödel's discovery, but it would suggest that science and mathematics could comfort itself with being able to explore the nature of the physical universe from a (relatively) new angle.

Whereby I've heard that Wolfram's "new" angle has to do with cellular automata with discrete states, or some such.

The Dutch kids' chorus Kinderen voor Kinderen wishes all the world's children freedom from hunger, ignorance, and war.

[ Parent ]

• ##### Wolfram's book is pretty interesting(2+ / 0-)
Recommended by:
Dave in RI, lotlizard

but his ego gets in the way.  This is the sort of guy who compares himself to Newton and Einstein.  Wolfram is very smart, but no one is as smart as Wolfram thinks he is.

I think cellular automata are very interesting, but whether they are a revolution in science is another matter, and I don't see them having much to do with mathematical logic.

What are you reading? is moving to Wednesday mornings.

[ Parent ]

• ##### The whiff of ego put me off from reading it. n/t(2+ / 0-)
Recommended by:
Dave in RI, plf515

The Dutch kids' chorus Kinderen voor Kinderen wishes all the world's children freedom from hunger, ignorance, and war.

[ Parent ]

• ##### Whiff, eh? (0+ / 0-)

You're kind.

There is actually a footnote where he says that the reason he uses very simple sentences is that his ideas are so complex that if he used normal syntax, no one would understand them.

jeepers!

What are you reading? is moving to Wednesday mornings.

[ Parent ]

• ##### Good night, nurse! "Stench" then? :o) n/t(1+ / 0-)
Recommended by:
plf515

The Dutch kids' chorus Kinderen voor Kinderen wishes all the world's children freedom from hunger, ignorance, and war.

[ Parent ]

• ##### SS0 + SS0 = …(4+ / 0-)
Recommended by:
Dave in RI, plf515, linkage, Jimdotz

… Quiney S TNT Baby.

The Dutch kids' chorus Kinderen voor Kinderen wishes all the world's children freedom from hunger, ignorance, and war.

• ##### Thank you for(4+ / 0-)
Recommended by:
Dave in RI, plf515, linkage, Jimdotz

The consistency of V=L is provable by inner models but not forcing. Is every abelian group A with Ext1(A, Z) = 0 a free abelian group?

• ##### That's some sig line!(3+ / 0-)
Recommended by:

What does it mean?

Godel, Escher, Bach

is now open

[ Parent ]

• ##### V=L(3+ / 0-)
Recommended by:

is the axiom of constructibility that Godel introduced, althought many think it's false today. It implies the axiom of choice and GCH. It was used by Godel to try to prove choice and GCH. An inner model is a model of the language of set theory which is a class. V=L claims that every set in the Von Neumann universe is constructible according to a certain procedure. If you like that stuff, you'll find a great exposition of all of it and more in Frankael,Bar-Hillel, Levy's book Foundations of Set Theory that you can find in the internet I think.

The second sentence of the sig was an open problem of Whitehead solved by Shelah: it is undecidable in ZFC.

The consistency of V=L is provable by inner models but not forcing. Is every abelian group A with Ext1(A, Z) = 0 a free abelian group?

[ Parent ]

• ##### Absorbing(4+ / 0-)
Recommended by:
Dave in RI, cfk, plf515, linkage

his concepts requires intimate reading like plf said.
But what I came away with from this chapter was how you choose what kind of mathematics to use after discovering the "real world."  So in future as our "real world" changes and the relationship between the two changes we decide which mathematics to apply.

I love the idea of supermathmatics and the "potential" for new formalizations of number theory.  The world continues to "open up".

1+1 does not equal 2.

• ##### I studied Mathematical Logic as a grad student...(5+ / 0-)
Recommended by:
theran, Dave in RI, plf515, linkage, Joffan

including Godel's Incompleteness Theorem, and my only comment about this chapter is the same now as it was then: HUH?

Godel was a genuine madman, for only a madman could have been the first to conceive of these ideas, let alone prove them.

It is the apex of beautiful metamathematics -- Elegance defined.

I know the special interests and lobbyists are gearing up for a fight as we speak.
My message to them is this: So am I -- President Barack Obama

• ##### Who would ever think ...(4+ / 0-)
Recommended by:

... of a Godel number? Had to be Godel.

• ##### Hence the real genius of what Turing did(4+ / 0-)
Recommended by:

Which was to come up with the elegant idea of a program you could write down.  Then the whole mess becomes actually intuitive: there are countably many programs (because they are strings) and uncountably many sets of strings, so some set of strings has no program to recognize it.

"Dream for just a second and then do it!" -- Kolmogorov

[ Parent ]

• ##### Godel was, quite literally, crazy(6+ / 0-)

A paranoid who was convinced people were trying to poison him.  After his wife died, he essentially starved himself to death because he was afraid of eating.

And, while many scientists are wrapped up in their work, Godel took this to extremes that were, well, extreme.

OTOH, toward the end of his life, Einstein said the only reason he went to the office was for the pleasure of walking home with Godel.

Godel, Escher, Bach

is now open

[ Parent ]

• ##### A realization ...(3+ / 0-)
Recommended by:

This week, I spent more time going back to re-read earlier sections than I did on this chapter itself. (I confess I couldn't remember any of the codons, much less exactly how the self-referencing actually works in quining.) If I really want to grasp the ultimate concepts, I'm going to have to re-read the book and really assimilate the building blocks. As it is, I can kind of follow along at the level of, uh, I guess I get it, if you (DRH) say so.

I'm at an interesting point in life. I have plenty of time for satisfying curiosity but it takes a lot longer to do so. By the time I'm thinking about the next step, I've forgotten the last.

• ##### Thank You ...(1+ / 0-)
Recommended by:
plf515

There will always be "truths" beyond any formal system?

"Upward, not Northward" - Flatland, by EA Abbott

• ##### Not exactly(2+ / 0-)
Recommended by:

that makes it sound like you're talking about things like God, or beauty, or such, which are beyond formal systems.

This is more pernicious:

If a formal system is powerful enough to represent number theory, there will be truths in it that cannot be proven in it.

What are you reading? is moving to Wednesday mornings.

[ Parent ]