This 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.
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.
txhwind•31m ago
The proof will be more friendly to nowadays programmers if we treat all "Gödel numbers" as bytecode of a programming language.
It's trivial that functions like "prove" and "subst" can be implemented based on abilities like bytecode parsing and expression tree manipulation.
dvt•53m ago
[1] https://inference-review.com/article/loebs-theorem-and-curry...
qnleigh•4m ago
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.