HN

Comments (13)

• Menu

  dvt
  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.[1] https://inference-review.com/article/loebs-theorem-and-curry...
• Menu

  WhitneyLand
  Saying his name like “girdle”, is the closest English pronunciation I’ve seen.The actual German ö is hard for me to figure out without having a native speaker around to practice with.
• bazoom42
  I’m confused by this jump to the natural world:> could you encode in pure logic how a dog behavesAssuming we knew enough about how a dog behaves (or less ambitiously, a more primitive organism) I would assume this could be described in a formal language. But why would Principia be needed for this? Math have been used to model natural phenomena a long time before Principia.
• Menu

  qnleigh
  I feel like it's nice to get the gist before diving into the gory details. The proof works by showing that just within the axioms of arithmetic, you can formally state the sentence "this sentence is unprovable." This has some very strange consequences:- It can't be false, because if it's false then it is provable, and 'provable' means ' can be proven to be true.' That would be a contraction.- So therefore it must be true, implying that it can't be proven. Consequently there are statements that are true but unprovable, even just within the axioms of arithmetic.This is Gödel's incompleteness theorem in a nutshell. Most of the proof is spent developing machinery for doing logic, talking about provability, and ultimately getting a statement to refer to itself all using integers and their properties. It's quite satisfying because it doesn't require any super-advanced math, and yet the result is very deep.
• txhwind
  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.