alt Hacker NewsThis blog post gets way too caught up in Gödel numbers, which are merely a technical detail (specifically how the encoding is done is irrelevant). A clever detail, but a detail nonetheless. Author gets lost in the sauce and kind of misses the forest for the trees. In class, we used Löb's Theorem[1] to prove Gödel, which is much more grokkable (and arguably even more clever). If you truly get Löb, it'll kind of blow your mind.
[1] https://inference-review.com/article/loebs-theorem-and-curry...
Replies
annie511266728 • today at 7:04 AM
Yeah, I think that's the tradeoff.
Löb gets you to the main idea faster, but Gödel numbering is the part that makes it feel like the system is actually doing it itself.
Without that step, it can start to feel a bit too close to the liar paradox.
➕ show 1 reply
Yeah, I think it would be better to first explain the liar's paradox to give the broad brush strokes, and then go into the details of Gôdel numbering.
It seems like most expositions of Gödel's incompleteness theorem go into a surprising amount of detail about Gödel numbering. In a way it's nice though, because you see that the proof is actually pretty elementary and doesn't require fancy math as a prerequisite.