How Gödel's Proof Works (2020)

ttzury about 3 hours ago 32 commentsRead Article on quantamagazine.org

⚡ Community Insights

Discussion Sentiment

78% Positive

Analyzed from 1175 words in the discussion.

Discussion (32 Comments)Read Original on HackerNews

reliablereason•9 minutes ago

Gödels incompleteness is just an example of the fact that you cant determine the outcome of infinite regression (in the general case).

The same as me asking you to give me the last digit of pi.

I am a bit annoyed by pop science always twisting it to sound so convoluted.

erichocean•5 minutes ago

I thought it was sorting an infinite set of infinite strings that seemed sketchy.

It's definitely not a "constructive" proof, even though it pretends to be....

That said, it's far less well-known that the workaround is trivially easy (from Alfred Tarski), making it kind of a useless theorem in practice.

gregfjohnson•32 minutes ago

Show HN: I recently gave a talk on the incompleteness theorem, specifically expressed in the language of software. It starts with a bit of historical background and a discussion of some of the philosophical context in which he carried out his work. The second half of the talk is my attempt to show the beautiful essential idea at the core of Godel's idea, pitched to a technically knowledgeable general audience. These are the slides from the talk, not translated into web pages; YMMV. Link: https://www.gregfjohnson.com/godel_incompleteness/

gavinsyancey•about 3 hours ago

If you find this interesting, I highly recommend reading "Gödel, Escher, Bach: an Eternal Golden Braid"

andyjohnson0•about 3 hours ago

GEB is a great book, and I've probably read it at least 3.33333333... times over the years. As a late teen it blew my mind. But I'm not sure I'd recommend it as a route into Gödel's proofs [1]. The book covers a lot of other ground too, and is notoriously digressive and quirky (looking at you, dialogues).

Instead I'd recommend Gödel's Proof by Nagel and Newman for a conceptual intro.

[1] I'm not a mathematician, so my understanding is necessarily informal.

gus_massa•about 1 hour ago

I really like GEB.

Most proof of the Gödel theorem use the primes encoding that is makes all the operations very unintuitive. But GEB uses just ascii and a lot of the side task get obvious. (It uses base 20 instead of 256, but it's the same idea.)

> is¨notoriously digressive and quirky

It is super mega ultra notoriously digressive and quirky.

bordo•about 3 hours ago

I can second this as a wonderful introduction to the proofs. This is the book that got me into logic and formal methods.

undershirt•about 2 hours ago

I’ll never understand how GEB was using math, art, and music to explain consciousness (and Hofstadter himself still thinks no one understood it), but Nagel and Newman did a great job explaining why logic as a mechanical thing has only a tenuous relationship to concepts we understand, and that helped me crack at least a little bit of the mystery I was after when giving up on GEB.

siddthesquid•about 2 hours ago

I have not read GEB but I thought his second book, I am a Strange Loop, did a pretty good job of connecting the idea of self referential loops (like in godels proof) to consciousness and art and such.

wk_end•about 1 hour ago

> I’ll never understand how GEB was using math, art, and music to explain consciousness

As Flannery O'Connor wrote, "The result of the proper study of a novel should be contemplation of the mystery embodied in it, but this is a contemplation of the mystery in the whole work and not or some proposition or paraphrase. It is not the tracking down of an expressible moral or a statement about life." We don't read literature with the hopes of a book laying out a precise thesis and incontrovertibly demonstrating it.

If you come into GEB expecting a scientific explanation of consciousness (like I did, when I first read it) you walk away confused and maybe disappointed. Hofstadter observed something transcendentally beautiful about self-reference and had a spiritual or religious revelation that, for him, related it to consciousness, and he attempted to convey that beauty and spiritual revelation in - appropriately self-referentially - a book that embodied it. You're meant to and appreciate it in your heart and soul, not (just) in your mind. It's literature, not science.

trescenzi•about 3 hours ago

“Godel’s Proof”[1] is also a great and shorter read if the scale of GEB is intimidating(I know it was for me at first).

https://nyupress.org/9780814758014/godels-proof/

khazhoux•about 2 hours ago

It’s actually an interesting fact that every person who was programming in the 80s owns a copy of GEB, which they flipped through a bit and then put on the bookshelf and never actually read.

zabzonk•about 1 hour ago

> which they put on the bookshelf and never actually read.

Much like the many unread copies of Knuth's TAOCP.

riffraff•about 1 hour ago

I would say "never actually finished", but I think this is quite true.

quaverquaver•about 2 hours ago

while it is a groovy into to recursion and other cool ideas, GEB annoys me in that I feel like the three figures in the title are ill matched. Godel proves a super important result in math, sure... Escher was a skilled draughtsman who had a feel for tesselation. An OK artist IMO but no special insights. Bach on the other hand was an expressive genius who in the volume, power and beauty of his productions just seemed to drop out the sky like a meteor. Escher does not belong in the same breath frankly. if Bach made a crab canon or did other marginally math-y things that is just not the point - the work lives or dies in entirely different terms...

bobson381•about 2 hours ago

the linking thread for all three is self-reference, either in the form of a fugue or in a painting showing its own creation. Doug is a loop guy

Rygian•about 2 hours ago

A Strange Loop guy, to be precise.

(It's the title of his follow up work after GEB.)

matherial•about 2 hours ago

> However, although G is undecidable, it’s clearly true.

That's... not really true; it's surprising to see it in Quanta, of all places.

Godel's (separate) completeness theorem says that in first-order logic, anything that's semantically true in all possible scenarios can be syntactically proved. So, if G is "clearly true", that ought to make it provable.

The theorems don't contradict each other because in FOL, G is not guaranteed to be true. Its truth is independent of the machinery Godel put in place.

It's not something you really need to get into an introductory text, but it actually makes the whole outcome easier to grasp, and leads to many more counterintuitive results, such as Skolem's paradox.

applicative•5 minutes ago

The completeness theorem is basically saying the received rules of logic capture what really follows as a logical consequence, i.e. that ⊢ captures ⊨ , so that all the genuinely logically valid sentences follow from the inference rules, or those and logical axioms, if that's how you formulate your logic.

> anything that's semantically true in all possible scenarios can be syntactically proved.

This means: whatever is true however I interpret the non-logical symbols, is also provable within my logic.

But the symbols of logic do not include `0` and `succ` and what holds about them, or any rules or axioms pertaining just to them, e.g. F 0 & (F n -> F (succ n)) -> \forall n F n.

Moreover given what we do think with `0` and `succ`, we can see that there is no way for us to formulate rules and axioms etc. that are adequate to prove everything true of them.

czgov•about 2 hours ago

It’s clearly true in The Natural Numbers. It’s not provable because in some model it’s false. Being clearly true in one model does not make it provable.

jojomodding•about 1 hour ago

Yes it is true in the unique model of second order PA, aka the computable model, aka the "standard" model.

pfdietz•about 1 hour ago

You can also obtain incompleteness from the unsolvability of the halting problem, by noting that if every statement in (say) Peano arithmetic were provable, one could solve the halting problem. Encode a halting execution of a TM as an integer using Gödel numbers and write a statement that the execution halts. Either that statement or its negation would be provable, so search for proofs for each at the same time.

An additional related theorem is Rogers' recursion theorem, which is how we get programs that, when run, print their own source code (by the theorem this can be done in any Turing complete programming language.)

somethinsfishy•about 2 hours ago

If you like video, supplement your reading with

Joel David Hamkins - Oxford lectures on the philosophy of mathematics "The Gödel incompleteness phenomenon" https://www.youtube.com/watch?v=Y5trjR5aw0k

also, "Gödel's incompleteness theorems: The proof that broke mathematics" | Joel David Hamkins https://www.youtube.com/watch?v=Sza69An_H8o spam-bait title but excellent mid-level talk.

edit: speling

3abiton•about 2 hours ago

Even more videos to binge before the holidays end! Thanks for sharing!

manesioz•about 2 hours ago

Great breakdown: https://stopa.io/post/269

dsego•about 1 hour ago

I am wondering if I'm just not smart enough to understand, but I've managed to slog through GEB and in the end the proof seems contrived, it stands on self reference.

layer8•25 minutes ago

Nagel & Newman is much better if you find GEB a slog (which was also my experience). However, Gödel’s theorem is fundamentally due to self reference. But so is the fact that the power set of countable infinity is uncountable, in a way.

smfjaw•about 2 hours ago

This is my favourite proof in all of maths (that I've been exposed to). Truly unreal feeling proving a statement is unprovable using godel numbering in an exam

Paracompact•about 2 hours ago

I think Godel's theorem is the single most important result in mathematics. At the same time, when the subject comes up, I like to link people to this essay to dispel a lot of the woo surrounding it regarding human exceptionalism, religion, etc:

https://shs.cairn.info/revue-internationale-de-philosophie-2...

bananaflag•about 3 hours ago

(2020)

ChrisArchitect•about 2 hours ago

(2020)

Some previous discussions:

2023 https://news.ycombinator.com/item?id=38391787

2020 https://news.ycombinator.com/item?id=23832087