13 ms·
Whitehead and Russell’s Principia rewritten in Coq
- amw-zero 5y agoDoes anyone notice an uptick in the number of posts about interactive theorem provers? Or is it just something I’ve been paying more attention to recently.
- deterministic 5y agoInteractive Theorem Provers are getting productive enough to be useful for real projects. The CompCert project was a real eye opener/motivator for people who want to develop proven correct software.
- trenchgun 5y agoThere is an uptick. Probably because of constructive math, category theory and theorem provers have got more publicity lately.
- huitzitziltzin 5y agoNot obviously any crazier than climbing Mount Everest, but surely much less likely to result in anyone’s untimely death.
- potiuper 5y agoSeems simpler to put the LATEX or HTML version (https://people.umass.edu/klement/pom/ https://people.umass.edu/klement/pom/) through an inversion of that pipeline. In https://news.ycombinator.com/item?id=21185624 https://news.ycombinator.com/item?id=21185624 joycian pointed out Naproche-SAD.
- Ericson2314 5y agoI don't think a Latex write-up would be much easier to formalize than raster scan. Now making the Latex infra and formalizing can be parallelized, but they are already doing that!
- hcs 5y agoI had assumed this had already been done, if not in Coq then in some machine formalization, interesting to see it being tackled. Is there a decent chance they'll find some of the later proofs not just missing a step but actually wrong? Or has this happened already? Edit: I may have been thinking of various attempts to prove the theorems by other (usually AI) means, as mentioned on the page: > This improves significantly on the earlier computer verification work of Allen Newell et al., Hao Wang, and Daniel O’Leary. In all three cases, either some theorems were not verified or their proofs were not reconstructed according to Principia’s proof sketches.
- Palomides 5y agoif I'm reading correctly, they've already done the Coq and it verifies. https://github.com/LogicalAtomist/principia/blob/master/PL.v https://github.com/LogicalAtomist/principia/blob/master/PL.v
- hcs 5y agoWhat's up there now is "only" up to *5. They announced that back in February and it sounds like there's been a lot more work since (though perhaps mostly reorganization and typesetting). Volume I goes up to *97, and the fragment that's commonly printed is "Principia Mathematica to *56".
- Ericson2314 5y agoFirst https://xenaproject.wordpress.com/ https://xenaproject.wordpress.com/, now this? I am very excited to see this sort of "codification" work become a legitimate academic enterprise. People I tend to trust are in that Frege > Russel camp, but that certainly doesn't make me less enthusiastic to see this sort of work undertaken. I am a big fan or the sort of thinking in https://hapgood.us/2015/10/17/the-garden-and-the-stream-a-technopastoral/ https://hapgood.us/2015/10/17/the-garden-and-the-stream-a-te... and https://blog.khinsen.net/posts/2020/07/08/the-landscapes-of-digital-scientific-knowledge/ https://blog.khinsen.net/posts/2020/07/08/the-landscapes-of-... that we need fewer "write an move on" works (e.g. academic papers), and more long-term living documents (e.g. wikis, but not just). The calculus analogy (surprisingly not in the origin) of going directly working on the integral, rather than the thing to be integrated, is good to keep in mind.
- dwheeler 5y ago> ... I am very excited to see this sort of "codification" work become a legitimate academic enterprise. ... I am a big fan or the sort of thinking ... that we need fewer "write an move on" works (e.g. academic papers), and more long-term living documents (e.g. wikis, but not just). You might find the Metamath databases to be very interesting (full disclosure: I participate). In particular, the "Metamath Proof Explorer" (MPE) database uses conventional classical logic + ZFC and proves all sorts of things. It is constantly updated as a collection, and every change is verified by multiple independently-implemented verifiers: http://us.metamath.org/mpeuni/mmset.html http://us.metamath.org/mpeuni/mmset.html Metamath doesn't embed any particular logic or other axioms, so you can choose the axioms you wish. There are other Metamath databases, as shown here at http://us.metamath.org/index.html http://us.metamath.org/index.html , such as the Intuitionistic Logic Explorer (it uses intuitionistic logic instead of classical logic) and the New Foundations Explorer (it constructs mathematics from scratch starting from Quine's NF set theory axioms). Most people have decided to not follow Russell's Typed Set Theory, as his hierarchy of types seems complex to many. If you want to use a more Russell-type system, I think Quine's NF set theory is an elegant simplification of it. You can see more of its Metamath representation here: http://us.metamath.org/nfeuni/mmnf.html http://us.metamath.org/nfeuni/mmnf.html
- dhanna 5y agoI just purchased copies of the Principia as part of my pandemic library after reading up on Allen Newell and Herbert Simons original AI programs. It’s exciting to see other people still interested in this old stuff :)
- lisper 5y agoAll this got me to thinking: how did Russel and Whitehead originally compose PM, and how was it typeset? They obviously didn't use TeX. Whatever they did, it must have been a truly staggering amount of work. For that matter, what is the source material for PM-RW and how is it being processed? Is there a manual translation process from a printed copy of PM, or are they using OCR?
- coldtea 5y ago>They obviously didn't use TeX. Whatever they did, it must have been a truly staggering amount of work. Well, tons of math books have been typeset before digital typesetting and/or TeX, they had the knack of it by the time.
- SavantIdiot 5y agoYou're not gonna believe this, back in the "old days" people cut fonts out of metal. :) People still do it for fun and profit. The Blue Ox Mill in Oregon has classes on fontcutting.
- lisper 5y agoOh, I was well aware of that, but that is just a small part of the story. What I was wondering is the details of the process by which R&W got the ideas out of their heads and into the metal. Surely they didn't carve the typeface by hand themselves?
- coldtea 5y agoWhy would they? There would have been any number of typographers handling such work, and several already working for Cambridge and Oxford books...
- pseudonymcoward 5y agoI believe that they would have written the manuscript, probably by hand but possibly aided by a typewriter, and then given it to a typographer (probably one with experience working on mathematical material) who would have typeset it, cutting any new symbols required. I'm not a historian but this seems like the only plausible process given the technology around at the time.
- dvt 5y ago> Principia has been criticized by famous logicians like Kurt Gödel as being a “step backwards” from Frege Kind of a weird dig here towards Gödel, but I don't think typesetting the whole thing's going to do anything to alleviate his points, as he was mainly criticizing the syntax. Logicians were in love with Frege's Begriffschrift for a long while (first seen in the late 1870s[1]). Either way, this was literally Gödel's first paper (published in 1944: "Russell’s Mathematical Logic") and he never mentioned Principia Mathematica again. [1] https://www.math.uwaterloo.ca/~snburris/htdocs/scav/frege/frege.html https://www.math.uwaterloo.ca/~snburris/htdocs/scav/frege/fr...
- drdeca 5y agotypesetting? huh? edit : oh, they also procedurally produce typeset text in the original syntax from the code in coq
- Rerarom 5y agoHe mentioned it in the title of the incompleteness paper.
- woolion 5y agoThere's a tendency in proof theory circle to dismiss set theory and related foundational work, yet it is ultimately the basis that is used (other foundational programs with 'better properties' tend to have worse issues). So it's not necessarily a dig towards Gödel, but to show that the book would be dismissed, without any dig to living logicians. But the reason would be that you find better and easier introductions to the material, where you don't have to internally translate to their more idiosyncratic syntax. Such a project is not going to give it mass appeal, but make it a tad more approachable for highly motivated people.
- bees_buzz 5y ago> he never mentioned Principia Mathematica again. ??? This paper contains a nice summary of Gödel's interactions with Russell. https://www.cambridge.org/core/services/aop-cambridge-core/content/view/0C347F171985A54395CDA89D31C4A59A/S1079898616000354a.pdf/russell_and_godel.pdf https://www.cambridge.org/core/services/aop-cambridge-core/c... Gödel's future work on constructible hierarchies and the dialectica interpretation were directly inspired by Principia Mathematica. I agree that characterizing Gödel's view on Principia as a "step backwards" is overly simplistic, but he certainly mentions and takes inspiration form the work throughout his career. > as he was mainly criticizing the syntax If you mean to say that Gödel's criticisms of Principia were just about syntax - that is also incorrect. Gödel had substantial complaints about the truthfulness of the axiom of reducibility that (IIRC) Russell himself thought posed a valid attack on the system in Principia.
- SavantIdiot 5y agoYou know I always mixed up Newton's Principia Mathematic with W&R's. Didn't realize for years they were different books. Also didn't know how to pronounce the "C" for even longer (this was pre internet days and I wasn't in college yet).
- jhanschoo 5y agoPronounce the c?
- x3n0ph3n3 5y agoYes, as an "s" or "k". The "correct" way to pronounce it is prinkipia.
- mdp2021 5y ago> "s" or "k" More common for post latin spoken languages would be ʧ ("ch·eese"). (You missed the foremost contender.)
- Soundwave_ 5y agoIn classical Latin a C is always hard, so Principia would not sound as "principle" does in English. Whether this means that this is "correct" is debatable. Cs in Latin have been universally soft for several hundred years so using the classical pronunciation is anachronistic. Perhaps appropriate for a English book with a Latin title. Pronounce it however you fancy, really.
- coldtea 5y ago>Cs in Latin have been universally soft for several hundred years so using the classical pronunciation is anachronistic. Well, latin are anachronistic themselves - so the classical pronunciation would still matter.
- jhanschoo 5y agoIndeed, I doubt that Newton would have pronounced Principia with a hard 'c'; Allen observes that in England, schoolmasters only started to observe meter and the hard 'c' and 'g' starting from the mid-nineteenth, and only in parts. I wanted the commenter to elaborate, since it seems to me that the most likely reason they remarked on its pronunciation would be that they discovered the reconstructed pronunciation of it and thought that it was correct to the point of being knowledge of how it ought to be pronounced, rather than as one of several ways of pronouncing it to communicate it. Ranieri contends that many casual speakers end up observing only partly observing the hard 'c' and 'g' and little of the other differences and end up with a hybrid "not even worthy of importing". https://www.youtube.com/watch?v=IjcX3MVSdyA https://www.youtube.com/watch?v=IjcX3MVSdyA
- for_i_in_range 5y agoI don’t mean to derail this contribution, but I want to chat about Principia. I ask honestly and earnestly, how would the Homo sapiens and the cosmos progress and advance if more people understood Principia Mathmatica? I bought the book two years ago but find it terribly difficult to penetrate and understand. I’m looking for motivation on why I should invest time and life energy in the ~6 months it would take me to read and understand it.
- lgessler 5y agoWhy do you feel as though you ought to read it? Best to think of PM like any other academic text, I reckon: primarily in conversation with contemporary issues/works, brimming with presuppositions of shared knowledge because of this, and unlikely to be of any great interest to a non-specialist. PM of course is no ordinary academic text, but I don't think it's an exception here.
- LudwigNagasena 5y agoGodel proved the whole endeavor to be futile. Really no point in reading it beyond curiousness.
- schoen 5y agoThat's not right! Gödel proved that PM couldn't do what people like Hilbert (or PM's authors) hoped it could do. However, we still have * mathematics * formalized mathematics * mathematical research despite the incompleteness phenomenon. All of them are still making progress, even often using approaches that are no more powerful than PM's approach. There are still interesting and important conjectures that can be resolved by a PM-like system, but haven't been resolved yet. I'm sure lots of mathematicians were deeply disappointed when they understood Gödel's result, but it didn't persuade anyone that mathematics was over or that we should no longer work within formal systems!
- LudwigNagasena 5y ago> However, we still have >* mathematics >* formalized mathematics >* mathematical research Yeah, none of them are based on or rely in any way on PM.
- sadfev 5y agoThis something that excites me immensely! I always had trouble following Principia’s notations!
- cormacrelf 5y agoI can't for the life of me find the actual PDF they say they made, with the whole typesetting pipeline in action. I don't think I've missed anything obvious, the website has this (without a link) > a pleasingly typeset edition of Principia’s first 131 pages in LaTeX, going from its introduction through the end of its propositional logic (up to *5). It has a link to a 113-page PDF that's just the Coq source rendered with syntax highlighting. So that's not it. The remaining PDFs in the GitHub repo are only samples of two of the propositions.
- gopiandcode 5y agoAlso nice to see that this project is licensed under the GPL - very much in keeping with the spirit of open access to knowledge and information; this way future generations will also be able to benefit from these efforts, and malicious evil companies won't be able to steal this work and deprive their customers of the 4 computing freedoms.
- eggy 5y agoI have copies of Newton's PM, W&R's Pricipia and The Elements for post-apocalyptic reading ;) For someone with little computational theorem proving, but not new to real analysis, would it be best to start with Lean vs. Coq? I have heard that HoTT has put Coq up front for this, but that Lean is much easier to get started with as someone with a mathematical background vs. a computational mathematics background, and that Lean tops out after you really dig in. Any tips would be much appreciated! Thanks!
- ocschwar 5y agoI had no experience with proof assistants until this year, and no real interest in formal proofs except as a QA method for statistical analysis code, so I started from a blank slate with almost no prior art to walk through. Lean is way the hell easier to deal with than Coq, and the video walkthroughs from the Xena project are amazingly good for understanding this stuff.
- ocschwar 5y agoAlso, VS Code for Lean is beyond awesome. And the Emacs package is not bad either.
- eggy 5y agoI am going to have to try Lean. I find I sometimes fall into the trap of wanting the ideal tool or solution when good enough will get me further. The little I've looked at Lean so far, has been encouraging from when I tried to play with Coq several years ago.