5 ms·
I’m a mathematician who spent many hours thinking about Goedel theorem and adjacent topics. The author in a self-deprecating way says that he’s not a mathemati
by xyzzyz 6y ago
I’m a mathematician who spent many hours thinking about Goedel theorem and adjacent topics. The author in a self-deprecating way says that he’s not a mathematician, but just a programmer. Bear no mind to that: this is one of the best popular expositions of Goedel theorem I’ve seen. Everything is very accurately explained, there are no silly mistakes and untruths one often sees mentioned in context of Goedel theorem, and even the original proof is sketched in a very approachable manner, striking a very good balance between getting across all crucial ideas, and skipping most of the distracting technical aspects (which are important and interesting, but I think only to mathematicians, haha). Great job all around.
- phaemon 6y agoWhat an excellent recommendation to the article. Thank you!
- stopachka 6y agoThis brought a big smile to read, thank you :)
- sillysaurusx 6y agoThere is an extraordinarily minor typo: “PM-LIsp” I point it out only because your work here is so good that it feels wrong not to smooth out any small splinters. Thank you for making this!
- stopachka 6y agoOi, thanks for the kind words and the catch! Updated (should take a few minutes to show up)
- marv3lls 6y agoI think I maybe noticed another typo... The last two axioms don't have matching parentheses? It looks like one more is opened than closed if I counted right.
- deleted 6y ago[deleted]
- ProfHewitt 6y agoDear xyzzy, Unfortunately, you missed that the author's proof does not actually prove inferential undecidability (sometimes called "inferential incompleteness") of Russell's Principia Mathematica for the following reason: The [Gödel 1931] proposition *I'mUnprovable* does **not** exist in Principia Mathematica because it violates restrictions on orders of propositions that are necessary to avoid paradoxes (such as Russell's Paradox). Gödel numbers (and in the author's case Lisp expressions) leave out the order of a proposition with the consequence that the Diagonal Lemma **cannot** be used to construct the proposition *I'mUnprovable*. Furthermore, existence of the proposition I'mUnprovable contradicts the following fundamental theorem of provability that goes all the way back to Euclid: A theorem can be used in other proofs. See the following article for further details: https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021
- derangedHorse 6y agoSo in layman's terms you're saying the system the author tries to prove incomplete by definition removed the parts that would prove it's inconsistent?
- greatquux 6y agoI'm going to need someone to come along and write up a layman's summary of this article. :) Does it change the end result of Gödel? Or is it basically the equivalent of saying what some restricted programming languages are doing, that we can get "good enough" results and not have these problems by restricting what we can do in the language?
- ProfHewitt 6y agoHi GreatQuux! The article linked below explains why [Gödel 1931] did not prove inferential undecidability of Russell's Principia Mathematica and likewise why the formalization of [Gödel 1931] in Lisp proof being discussed is also invalid: https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021 However, the article linked above does have a correct proof of inferential undecidability (also known as "inferential incompleteness"). Would be happy to respond to any questions that you might have.