21–30 of 38 posts
Earlier quoted context omitted.
TLDW: Godel's incompleteness theorem is at odds with the goals of Principia.
Which is weird because he used the formalism of principia to actually state the theorem, or at least part of it
This is useful to anyone who wants to reason through the proofs constructively and tinker with the approaches. Thank you!
Earlier quoted context omitted.
Thanks. It appears, however, that Dyson considers the whole approach a failure (referring to Gödel as a demolisher of it). So while he is saying it about a book, ironically, it seems hardly applicable in this context anymore. Because with this reasoning, any program in Lean (and the Lean programming language itself) should be seen as "a monumental failure".
This is just my opinion, but reading about Bertrand Russell my impression is that he dedicated his life to Pincipia Mathematica partially because he expected to find God in the foundations of the mathematics, and when that didn't happen it drove him rather insane. And then Gödel shows up and basically knifes him on stage with the Incompleteness Theorm.
Earlier quoted context omitted.
TLDW: Godel's incompleteness theorem is at odds with the goals of Principia.
I remember my Java IDE in undergrad warned me about an infinite loop, and this was before I learned about the diagonalization proof of the non-computability of the halting problem, one of my favourite proofs ever. The fact that not all programs and inputs can be shown to halt did not stop the engineer who wrote that guardrail for the IDE. Surely the principia and similar efforts will still yield useful results even i…
So the Java IDE had been able to recognize an infinite loop of the kind you wrote by an algorithm, that can be proven to be correct for a limited class.
On the other hand, you can loop infinitely deciding to exit on the return value of opaque calls to some entity external to your analyzer, and your IDE shouldn't be able to catch that.
Sorry if this is obvious in one of the links, but does there exist a high quality “OCR-ed” version of the original text?
I recently completed the natural number lean game and found it pretty fun, and would like to learn more about the differences between the two. Thanks!
What is the real difference between rocq vs lean? Alternatively, what is your motivation to do this in lean as compared to playing around with the rocq one if it exists? I recently completed the natural number lean game and found it pretty fun, and would like to learn more about the differences between the two. Thanks!
Lean is also a lot faster.
> Although the Principia is thought to be “a monumental failure”, as said by Prof. Freeman Dyson I'd like some elaboration on that. I failed to find a source.
Earlier quoted context omitted.
I remember my Java IDE in undergrad warned me about an infinite loop, and this was before I learned about the diagonalization proof of the non-computability of the halting problem, one of my favourite proofs ever. The fact that not all programs and inputs can be shown to halt did not stop the engineer who wrote that guardrail for the IDE. Surely the principia and similar efforts will still yield useful results even i…
Yes, you can't prove important properties of the class of all programs, but you can prove properties of smaller, limited classes of programs that you are interested in. So the Java IDE had been able to recognize an infinite loop of the kind you wrote by an algorithm, that can be proven to be correct for a limited class. On the other hand, you can loop infinitely deciding to exit on the return value of opaque calls to…