Gödel, Escher, Bach: an in-depth explainer

But at the same time, when it really gets going I can't help but being swept away and entertained by the unfiltered enthusiasm he displays and the work he has done to put it to paper. It's like a conversation with a very exhausting but at the same time very interesting person. It's like trying to put that tingling in the back of the brain when some kind of insight looms in words.

I feel like it's probably best read as a curious psychograph of a nerd in the seventies who is deeply interested in theoretical computer science and its implications on awareness and (artificial) intelligence. Not as a scientific non-fiction-book which is trying to educate the reader or trying to make a strong argument for something

Yet Godel's theorem is entirely formal and understandable by a computer, which can draw the same conclusions about any such statement as a human.

One of the things it inspired was Turing's work on uncomputable numbers. It turns out that computability and incompleteness are intertwined, which at least I find interesting. And without the "uncomputable numbers" malarkey, I wonder if the Turing Machine formalism would exist (answer, "probably, but maybe looking different and with another name"). And, well, the Halting Problem is essentially Gödel Incompleteness (imagine handwaving here).

As for proof systems, again, the answer is "probably". Knowing that there are true, unprovable, statements in a formalism is something that informs how you approach it, you need to put a limit on how far to go before you say "I don't know" and taht is in and of itself important.

The proof of Gödel's result uses the paradoxical statement "This statement is false", but that's being used to prove this very general result about all systems. So the hunt is then on to find "natural" statements that are True but Unprovable.

But the "unprovable" bit should more completely be stated as "unprovable in a specific axiomatic proof system". If we want to prove that statement S is "True but Unprovable" then we must actually prove that it's true. So if we've proved it's true, what does it mean to say it's unprovable? We just proved it! What's going on?

So let's take a specific example.

Peano Arithmetic (PA)[0] is an axiomatic proof system intended to capture Natural Numbers and their behaviour.

The "Goodstein Sequence" G(m) of a number m is a sequence of natural numbers ... you can find the definition here[1]. It's not hard, but it's longer than I want to reproduce here.

Goodstein's Theorem (GT) says that for every integer m greater than 0, G(m) is eventually zero.

It has been proven that GT cannot be proved in PA, but it can be proved in stronger systems, such as second-order arithmetic.

So the statement of GT is not self-referential, along the lines of "This Statement Is False" sort of thing. It's an actual statement about the behaviour of integers, so it's not a self-referential trick.

Your question now is: What's the point? How is this useful or relevant?

Much of modern (pure) mathematics is chasing things because the mathematicians find them interesting. The vast, vast majority will never, of themselves, be useful by (what I expect are) your standards.

But it was once thought that factoring integers was of no practical use, and only pursued or investigated by cranks. Imaginary Numbers were thought to be bizarre, useless, and dangerous. Non-Euclidean Geometry was thought to be utter nonsense, and held up as part of the "proof" that the fifth postulate was unnecessary and was deducible from the other four. All three of these now form critical components in modern technology.

Even more, to the average person on the street, anything to do with algebra is completely pointless.

For you, Gödel's theorem is completely pointless and useless and probably of no interest at all, but it helps us understand the limitations of formal systems. The techniques that have been developed in the time since it was proved have helped us understand more about what computer verification systems might or might not be able to accomplish.

Of itself, Gödel's theorem might not be of direct, immediate, and practical use, but the work it has inspired has tangentially been useful, and may yet be moreso.

But not for everyone. After all, some people don't care about the Mona Lisa, or Beethoven's Fifth Symphony, or Michaelangelo's David, or the fact that people have walked on the Moon, so why should people care about results in Pure Mathematics?

That's the thing about Pure Mathematics. Sometimes it ends up being useful in ways we never expected.

[0] https://en.wikipedia.org/wiki/Peano_axioms

[1] https://en.wikipedia.org/wiki/Goodstein's_theorem#Goodstein_...

That's precisely what it is. And what makes it valuable too: such works of blatant self-indulgence are not very common in mathematics (at least, while remaining enjoyable to read).

> than a profound intellectual achievement in itself

Sure. I would call the book an artistic achievement in the intellectual realm: it talks about ideas, but is art. To put it another way: everyone knows "mathematics is not a spectator sport" — this is usually said in the sense of "you can't learn mathematics unless you do it yourself", which is true enough, but it's also a loss in the sense that there's no equivalent of sitting back and watching a game, watching someone play with ideas and do mathematics. This book comes close. How good the quality of the game is, and whether you'll learn anything from watching the game, is debatable (probably not much), but the experience itself is unusual, which makes the existence of this book a happy circumstance.