What Made Gödel’s Incompleteness Theorem Hard to Prove

https://algorithmsoup.wordpress.com/2018/10/01/what-made-godels-incompleteness-theorem-hard-to-prove-its-about-how-you-say-it-not-just-what-you-say/

by williamkuszmaul • 8 years ago

126 99 8 years ago

algorithmsoup.wordpress.com

7dare• 8 years ago

I feel like the further you go in maths, the less attention is given to details, which are "left as exercise to the reader".

dan-robertson• 8 years ago

This depends a lot on the branch of maths: eg topology has much more of a reputation for being wishy-washy than analysis.

It also depends what the context is. A paper is not meant to prove things sufficiently for a layperson but for the author’s peers and so an omitted proof means one of “proven elsewhere;” “follows in a straightforward way from the definitions;” “follows in a straightforward way from an earlier proposition;” or “follows from a well-known pattern in the subfield.” And here “follows in a straightforward way” typically means something between “just look at;” “at each step there is only one reasonable thing to do so just do that;” and “apply all the standard tricks from the subfield and see what sticks.”

It is not true that advanced mathematics is less rigorous than more elementary maths, it’s just that materials for advanced topics require more domain knowledge, and provide less hand-holding.

SolarNet• 8 years ago

And I feel like this is where better hyperlinking of papers could be used. Like not just citations, but the ability to click through to the "proven elsewhere" perhaps with a short paragraph of how the given citation proves it.

Avshalom• 8 years ago

"you must understand when I say it's trivial I just mean that I can do it "

fredgrott3• 8 years ago

true..how many understand no really know Graph Theory at the level we use it to analyze code object coupling, RTTI, etc

QML• 8 years ago

I feel small things like that, or professors not understanding their students’ perspectives — apparently this is a known cognitive bias called “curse of knowledge” — unnecessarily restricts access to field.

lixtra• 8 years ago

I know some authors who write out all such proofs and then remove or shorten them for publication. What may seem incredibly hard for you may be just tedious to read for someone else. A math paper is more than just proofs. It’s also a story.

technocratius• 8 years ago

For those interested, Hoffstadter's Godel Escher Bach gives a great introduction into formal systems and Godels incompleteness theorem. Highly recommended.

afthonos• 8 years ago

I read it cover to cover out of a sense of obligation but came away very disappointed. The Achilles-Turtle-Random Other Creature allegories got very tiresome, and the content took a very long time to get to the point. For anyone interested in the proof, I recommend Gödel’s Proof by Nagel instead. It covers the same material in about a tenth the space.

(GEB has other philosophical discourses that are interesting, if only as an example of how people can very reasonably mispredict the future. In Hofstader’s case, he posited that chess would only be played at a human level by an AGI.)

manifestsilence• 8 years ago

I agree that it's way over-long and rambling, but it was my introduction to the topic. Where it really shines is his interesting and controversial thesis that connects Godel's proof with the Church-Turing thesis and other things to form a theory of consciousness as pattern and make the claim that a sufficiently powerful AI is as sentient and meaningful a consciousness as we are.

I read Godel's Proof after though, and I agree that it is a far clearer introduction to Godel's theorems.

et1337• 8 years ago

Absolutely agree. GEB constantly tries to prove the cleverness of the author, complete with winks and nudges. It stacks so many unintuitive analogies on top of each other that I spent most of the time trying to recall which real-world concepts they all mapped to.

Also, the book is about 98% Gödel and 2% Escher and Bach. Any time it steps outside its wheelhouse of math and into the realm of philosophy or art, you get the distinct sense that it has no idea what it's talking about.

Do yourself a favor and just take discrete math 1 and read a few Wikipedia articles instead.

westoncb• 8 years ago

I found 'Gödel’s Proof' fascinating—surprisingly more so than GEB, which I'd anticipated loving for years before dipping into it (I didn't finish, but the primary reason was loss of interest). It was one of the first things I came across that gave me the sense of something like 'mathematical system architecture'.

misiti37802• 8 years ago

If you still have the energy or interest, try I Am A Strange Loop, he wrote in a number of years after and it seemed more approachable

pflats• 8 years ago

The New Turing Omnibus has a good chapter on the Incompleteness Theorem; it covers the basics in 5 or 6 pages, if memory serves.

carlehewitt11• 8 years ago

Chaitin [2007] presented the following analysis:

Godel's proof of inferential undecidability [incompleteness] was too superficial. It didn't get at the real heart of what was going on. It was more tantalizing than anything else. It was not a good reason for something so devastating and fundamental. It was too clever by half. It was too superficial. [It was based on the clever construction] I'm unprovable. So what? This doesn't give any insight how serious the problem is.

raverbashing3• 8 years ago

Yes

And GEB's explanation of it is more complete/exact than the one in the article.

It is also amazingly mind-twisting. Not the explanation per se, but the theorem.

And I think its consequences are under appreciated: no (sufficiently complex) logical system is free from self-contradictions.

wk_end3• 8 years ago

I believe that's a misinterpretation of Goedel; it's an incompleteness theorem, not an unsoundness theorem.

Incompleteness: there exist true statements that lack proofs

Unsoundness: there exist false statements with proofs

If I understand all this correctly, what Goedel demonstrated was that a sufficiently complex logical system could self-reference, and from self-reference unprovable (not contradictory) true statements fall out.

By reductio ad absurdum any self-contradictory logical system is useless as a logic because everything is provable in it, so one wonders if such systems should even be considered "logical systems".

edanm2• 8 years ago

And I think its consequences are under appreciated: no (sufficiently complex) logical system is free from self-contradictions.

That doesn't seem right? Any logical system that has a self-contradiction (which I take to mean can prove a statement and its inverse) will be able to prove everything, which is obviously a pretty big flaw.

What Godel's 2nd incompleteness theorem says is that if a system can prove its own consistency, then it follows that it is unsound.

DyslexicAtheist• 8 years ago

obligatory "I am a Strange Loop" reference here for anyone who wants a more polished introduction into the topic from many years later. He wrote GEB when still very young and had time to refine his points in this later book.

chj• 8 years ago

Unfortunately his style sticks.

orcs• 8 years ago

I felt like the article was just getting going, then it finished.

nielsbot• 8 years ago

i was ready to roll up my sleeves, expecting “and here’s a walkthrough”.... and that’s how i felt.

dajohnson89• 8 years ago

article had no teeth whatsoever.

vyodaiken4• 8 years ago

What made the theorem hard is not the details, which are simple, it's the conceptual leap to thinking about mathematical statements as mathematical objects - something that is much easier for us than for mathematicians of Godel's time because we are familiar with programs and computers. Much of the text is taken up with proving things that were surprising to mathematicians of the era, but are now commonplace: e.g. that we can treat numbers as encoding mathematical propositions so that for every proposition P expressible in some formal logic L, there is a number #P which encodes P in some unambiguous way - as long as L is expressive enough to formalize some basic arithmetic. Then we can start making trouble by asking if we can construct a proposition Q so that Q(#P) is true iff the proposition #P encodes, P, is provable in our system. If so, we should be able to prove Q(#P) or NOT Q(#P) if L is complete, but things don't work out well because it's possible to encode paradoxical statements. In short.

thrmsforbfast4• 8 years ago

thinking about mathematical statements as mathematical objects...

Lock yourself away in a room with nothing but pen and paper (no internet, not books) and try to reproduce Goedel's original proof. Then post the attempt here :)

When I tried this a few years ago I made a mistake in the definition of numbering, got through half the proof, ran into trouble, and gave up before I figured out exactly where the mistake was. And I had already committed the overall outline and the tactical steps for each part to memory...

Even if you remember the entire outline, it'll be really hard to get the details right....

And, more importantly, the outline itself is actually not obvious.

... much easier for us than for mathematicians of Godel's time because we are familiar with programs and computers

Again, it seems unlikely that this was the sticking point.

E.g. Hilbert understood mathematics as a symbolic game, thought about this exactly question, and didn't come up with Goedel's proof. And Hilbert was definitely no dullard.

gnulinux3• 8 years ago

It's very hard to believe Godel didn't face problems you faced. He probably did mistakes too, and went back periodically to make sure his proofs are sane. He was probably stuck too, many times even, and solved those problems as other mathematicians solve their problems. After all, it took him many years to complete his proof. And even more years until theorems stabilized to today's form (i.e. Rosser's trick etc). People have been practicing formal mathematics long before Godel, and this cycle of being stuck and solving problems is pretty common in mathematics. His coworkers would have had the same sort of issue. This seems to indicate me that GP comment is right that the inciting incident was understanding the correspondence between mathematics and its encoding. Which brings us to:

E.g. Hilbert understood mathematics as a symbolic game

Hilbert had a radically different understanding of the nature of mathematics compared to Godel. Moreover, Hilbert was radical enough that he tried to use his fame to silence people with differing views than him (e.g. Brouwer). Hilbert hardly believed Godel when he published his results, because it was easy to see that it would shake the foundations of "Hilbert's Program" something Hilbert spent half his life on (and logicians still publish papers about the relationship between Godel's Incompleteness theorems and Hilbert's Program). This makes Hilbert orders of magnitude less motivated to think about this issue, probably. On the other hand, Godel had various non-mathematical reasons to prove incompleteness, one being his desire to block materialism; check for Godel's Gibbs Lectures.

repsilat• 8 years ago

It's super easy to prove if you assume the Halting Problem is undecidable. Basically,

1. Assume every either T or ~T is provable for all theorems T, and that our logic is consistent. (The opposite of the incompleteness theorem.)

2. For every Turing machine, there is a proof that it halts or a proof that it doesn't halt.

3. A machine that enumerates and validates proofs will find one of those proofs, so the Halting Problem is decidable -- a contradiction.

Easy peasy. (The proof of the Halting Problem undecidability from the Incompleteness Theorem is similarly straightforward.)

Godel did his work first though, so he didn't have that machinery (hmm) available.

baddox• 8 years ago

Whether you have a thing memorized is fairly unrelated to how complex the thing is.

jonahx• 8 years ago

Lock yourself away in a room with nothing but pen and paper (no internet, not books) and try to reproduce Goedel's original proof. Then post the attempt here :)

We can all agree that would be hard, but your claim that the details are the central thing that makes GP hard is much, much stronger than that.

The relevant question would be: How many people alive right now could succeed at your challenge? My guess would be thousands, maybe tens of thousands.

And compare that to:

The number of people alive who, without any knowledge of GP, could come up with the key insight you describe in your 1 paragraph summary of the proof, and the insight of using godel numbers to label mathematical statements to make that argument rigorous.

The answer to that is "somewhere around 0."

I get that you're impressed by the proof's details -- they're impressive -- but it seems like an odd take to rate those as more difficult than the incredible creative leaps that produced the high-level ideas behind the proof.

vyodaiken4• 8 years ago

Again, it seems unlikely that this was the sticking point.

Look at the proof - page after page of work showing how to encode and decode formal propositions using primitive recursive functions.

E.g. Hilbert understood mathematics as a symbolic game, thought about this exactly question, and didn't come up with Goedel's proof. And Hilbert was definitely no dullard.

Goedel's theorem is exactly that mathematics is not a symbolic game - that Hilbert's program is not possible. The proof relies on reducing logical deduction to arithmetic.

misiti37802• 8 years ago

I just read "I Am a Strange Loop" and he the author a pretty nice job of explaining this -- Unfortunately, I could never get through GEB so I do not know if the explanation in there.

fredgrott3• 8 years ago

its there, about the middle of the book..

arithma2• 8 years ago

Godel Incompleteness Theorem and Turing Halting Problem are two faces to the same coin, I intuited. It is deeper than I thought, especially that I forgot about the two godel's incompleteness theorems (not just one.)

Scott Aaranson "popularizes" Kleene's textbook proof of Godel's theorems using Turing machines in his blog:

https://www.scottaaronson.com/blog/?p=710

scythe3• 8 years ago

I would say that's a pretty inaccurate analogy. The incompleteness theorem can be considered a consequence of the halting problem, but not the other way around. The incompleteness theorem depends heavily on the properties of Peano arithmetic, as defined by the presence of both addition and multiplication. If you construct a set of numbers with one defined arithmetic operation (Presburger arithmetic), the incompleteness theorem does not hold and all statements can be confirmed or disconfirmed by an algorithm (albeit not efficiently). The halting problem, by contrast, is much more general, and recurs in many settings where self-reference is possible.

arithma2• 8 years ago

It's not an analogy. I thought so too at first, but the connection is material: In the blog it shows a proof of Godel's theorems using the Halting Problem.

johncolanduoni6• 8 years ago

Godel's completeness theorem rests on a system's ability to represent addition and multiplication, not whether they define it. Basically, it recurs where reasoning about addition and multiplication is possible within the internal theory. This is why it applies to e.g. ZF set theory, even though there is no mention of addition, multiplication, or even numbers in ZF's definition.

The role of Peano arithmetic is somewhat analogous to the role of the particular definition of a Turing machine in the proof of the halting problem: you can easily swap it out with something commensurate and get the same result.

edanm2• 8 years ago

From the article:

Here’s another example (known as the Berry paradox):
Define {x} to be the smallest positive integer that cannot be defined in under {100} words.
This might look like a valid mathematical definition. But again it’s nonsensical. And, importantly for the sanity of mathematics, no analogous statement can be made mathematically formal.

I thought it was worth mentioning that the Berry Paradox does show up in a mathematically formal way, and it was fascinating to me. It can be used to prove that a general algorithm to compute the Kolmogorov complexity of a string is uncomputable.

https://en.wikipedia.org/wiki/Berry_paradox#Formal_analogues

carlehewitt11• 8 years ago

See the following for history and limitations of Godel's results:

https://hal.archives-ouvertes.fr/hal-01566393

joker3• 8 years ago

While the Berry paradox isn't strictly speaking mathematically sensible, there are similar ideas that lead to new and less well-known impossibility results. https://arxiv.org/pdf/chao-dyn/9406002.pdf has a transcript of an overview of the idea and main results by the researcher who came up with them, as well as a fairly extensive bibliography.

There's also a version of Russell's paradox lurking in the standard proof of Cantor's theorem (https://en.wikipedia.org/wiki/Cantor%27s_theorem).

undershirt• 8 years ago

I couldn't make it through GEB, but I read a good concise explanation in a book called Godel's Proof: https://www.amazon.com/G%C3%B6dels-Proof-Ernest-Nagel/dp/081...

dandare• 8 years ago

A layperson here, I always wanted to ask this question: Godel proves that not ALL statements that are true can be proven, because here is this one example. I get it, it's a valid mathematical proof. But does it really say anything about other statements, except this one? Does it says anything about statements that are not self-referential? Is it possible that the incompleteness theorem really applies only to self-referential statements and says nothing about non-self-referential statements?

icen• 8 years ago

The proof of the incompleteness theorem only shows you that recursively-enumerable arithmetic systems are always missing something, because the construction always holds. It doesn't make any grand statements about the structure or nature of things that are true and without proof.

The second incompleteness theorem gives an example of something undecidable that's probably more interesting that the uselessly paradoxical statement in the first: it says that no system can consistently prove its own consistency.

svantana• 8 years ago

That's a common technique in math proofs, to disprove a statement by providing a counterexample. But there probably are improvable statements that are not self-referential, e.g. certain statements about infinite sets.

But the grander point, that Hofstadter pushes a lot in GEB, is that any sufficiently powerful symbolic system will be able to self-reference. For example, consider a programming language that is not Turing complete. You will basically need to disallow loops, because with those you can implement a virtual machine to break all your self-reference-banning rules.

What Made Gödel’s Incompleteness Theorem Hard to Prove

Related Stories