I 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.
What'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".
First 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.
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.
> ... 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
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 , 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
I am somewhat a type theory partisan, but I appreciate Metamath leading the way, especially on the social side of things. (I would say it is technically primitive, but socially advanced, as opposed to say Coq which is more technically advanced but has a very poor track record of fostering wide-scale many-person projects.)
Best of luck! The importance is not there is one way that wins out (that would be bad) but that each project seeks to be all-encompassing. We want many maps over all the land, not divvying up the land into unoverlapping fiefdoms, or forcing everyone to be in one big fiefdom.
I 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 :)
All 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?
You'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.
Oh, 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?
I 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.
Yes, generally the mathematician would write the manuscript & others would turn it into a printable form. IIRC, some people (typographers) created moveable type with math symbols that would then be set in place by a typesetter; if that wouldn't work, a plate for a page would be created. Very expensive & laborious.
I believe that the "backward-E" and later the "upside-down-A" are that way because then you did NOT need to create a new metal symbol; you could simply reuse a capital E and A and put them in upside down. I can't find a citation for this. There's other history here: https://jeff560.tripod.com/set.html
> 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.
There'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.
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.
>Either way, this was literally Gödel's first paper (published in 1944: "Russell’s Mathematical Logic") and he never mentioned Principia Mathematica again.
I'm not sure what you're trying to say here. That paper was nowhere near Godel's first, nor was it the only time he mentioned Principia.
The title of the first of his works on the incompleteness theorem was "On Formally Undecidable Propositions of Principia Mathematica and Related Systems" in 1931.
You 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).
In 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.
Indeed, 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
There are two schools of thought: pronunciation as per the Catholic church, where the sound has evolved (to "ch") over hundreds of years of Latin being used as a working language, and pronunciation as per the Romans, for whom "c" was pronounced "k" (and "v" was pronounced "w").
Neither is really right or wrong, certainly neither is 'anachronistic'. Latin can be regarded as a classical, dead language, or as an ecclesiastical, priestly language, or as something else.
In practice, different pronunciations are used by people with different educational, cultural and religious backgrounds. In many cases the 'accepted' pronunciation is used to signify 'belonging' to a particular tribe (eg academic archeologists vs theologians educated at seminaries). In Scotland it was a sectarian marker (one of about a million obscure indicators of community allegiance) back in the days when Latin was widely taught in grammar schools.
FWIW, I have only ever heard mathematicians refer to the Russell book with a hard C.
I 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.
That'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!
Why 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.
>I ask honestly and earnestly, how would the Homo sapiens and the cosmos progress and advance if more people understood Principia Mathmatica?
Not much, I'd say.
For one, it bears no moral significance. You can be a net negative scumbag and understand Principia Mathmatica.
Second, it's a formalization of mathematics. It doesn't necessarily yield relevant new insight to advance homo sapiens beyond it's (quite narrow) scope. Understanding Principia Mathmatica doesn't mean you'll know how to make penicillin, for example.
Third, even for pure mathematical work, it's not that interesting in the end. Tons of great math work is being done that has no relation to it.
Several of them are getting pretty far, and none of them are directly using PM notation (although all of them ultimately owe something to PM). You can learn more math, or contribute more to math, nowadays by learning one or more of these systems. To my knowledge, all of them are eager for new volunteers to continue formalizing theorems in their respective databases.
Agree, and I suspect only a tiny percentage of mathematicians have read it (I certainly did a degree and doctorate in maths at Oxford and sat the logic and set theory paper in my finals and it never went through my mind to read it). I get the impression that it's one of those books that was very influential in certain ways (Godel read it!) but is more a historical artefact now.
> how would the Homo sapiens and the cosmos progress and advance if more people understood Principia Mathmatica?
It's important to separate historical importance from importance to understanding by most people.
The presence of Whitehead & Russell's Principia Mathematica (PM) in history is a very important historical event. In at least one list, it's one of the most important books in the 20th century. PM shattered any argument that mathematics couldn't have rigorous foundations. PM instead showed that it was possible to start from relatively simple axioms and really prove all the way up to a higher level.
PM is NOT, however, important to read or understand itself in detail, as it's been superseded by later works. Syntactically, PM uses a dotted notation instead of parentheses that most people find hard to read & generally undesirable. From a deeper point-of-view, PM uses a set of axioms built on a hierarchy of types. This hierarchy of types was an early effort to avoid various paradoxes. Almost no one uses a hierarchy of types like this today; it's far more common to use Zermelo-Fraenkel set theory with the axiom of choice (ZFC). Even if you wanted to use a hierarchy of types, which is rare, you're probably more likely to use Quine's "New Foundations" which provides a much simpler foundation for mathematics.
It's not important to understand PM in detail, but knowing that it's possible has inspired many more recent efforts, and that is more important.
I argue in my video "Metamath Proof Explorer: A Modern Principia Mathematica" that the Metamath Proof Explorer (MPE) is a successor to PM. MPE uses modern notation (e.g., parentheses) and ZFC set theory combined with classical logic, so it uses modern conventions, but it also tries to prove "everything" from a very few axioms. Thankfully, we can now use computers to verify every last step (with multiple independent implementations), so we can have much more confidence in the proofs. Here's my video, I think you might like it: https://www.youtube.com/watch?v=8WH4Rd4UKGE
That video focuses on MPE, but of course there are several efforts inspired by PM. Understanding the impact that PM had on mathematics is, to me, the important thing.
I 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.
Also 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.
Does 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.
Interactive 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.
I 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!
I 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.
I 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.
66 comments
[ 2.8 ms ] story [ 128 ms ] threadNow making the Latex infra and formalizing can be parallelized, but they are already doing that!
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.
https://github.com/LogicalAtomist/principia/blob/master/PL.v
I am a big fan or the sort of thinking in 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-... 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.
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
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 , 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
Best of luck! The importance is not there is one way that wins out (that would be bad) but that each project seeks to be all-encompassing. We want many maps over all the land, not divvying up the land into unoverlapping fiefdoms, or forcing everyone to be in one big fiefdom.
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?
I'm not a historian but this seems like the only plausible process given the technology around at the time.
I believe that the "backward-E" and later the "upside-down-A" are that way because then you did NOT need to create a new metal symbol; you could simply reuse a capital E and A and put them in upside down. I can't find a citation for this. There's other history here: https://jeff560.tripod.com/set.html
Well, tons of math books have been typeset before digital typesetting and/or TeX, they had the knack of it by the time.
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/fr...
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.
???
This paper contains a nice summary of Gödel's interactions with Russell. 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.
I'm not sure what you're trying to say here. That paper was nowhere near Godel's first, nor was it the only time he mentioned Principia.
The title of the first of his works on the incompleteness theorem was "On Formally Undecidable Propositions of Principia Mathematica and Related Systems" in 1931.
https://en.wikipedia.org/wiki/On_Formally_Undecidable_Propos...
More common for post latin spoken languages would be ʧ ("ch·eese"). (You missed the foremost contender.)
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.
Well, latin are anachronistic themselves - so the classical pronunciation would still matter.
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
Neither is really right or wrong, certainly neither is 'anachronistic'. Latin can be regarded as a classical, dead language, or as an ecclesiastical, priestly language, or as something else.
In practice, different pronunciations are used by people with different educational, cultural and religious backgrounds. In many cases the 'accepted' pronunciation is used to signify 'belonging' to a particular tribe (eg academic archeologists vs theologians educated at seminaries). In Scotland it was a sectarian marker (one of about a million obscure indicators of community allegiance) back in the days when Latin was widely taught in grammar schools.
FWIW, I have only ever heard mathematicians refer to the Russell book with a hard C.
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!
>* mathematics
>* formalized mathematics
>* mathematical research
Yeah, none of them are based on or rely in any way on PM.
Not much, I'd say.
For one, it bears no moral significance. You can be a net negative scumbag and understand Principia Mathmatica.
Second, it's a formalization of mathematics. It doesn't necessarily yield relevant new insight to advance homo sapiens beyond it's (quite narrow) scope. Understanding Principia Mathmatica doesn't mean you'll know how to make penicillin, for example.
Third, even for pure mathematical work, it's not that interesting in the end. Tons of great math work is being done that has no relation to it.
https://news.ycombinator.com/item?id=25118372
Several of them are getting pretty far, and none of them are directly using PM notation (although all of them ultimately owe something to PM). You can learn more math, or contribute more to math, nowadays by learning one or more of these systems. To my knowledge, all of them are eager for new volunteers to continue formalizing theorems in their respective databases.
It's important to separate historical importance from importance to understanding by most people.
The presence of Whitehead & Russell's Principia Mathematica (PM) in history is a very important historical event. In at least one list, it's one of the most important books in the 20th century. PM shattered any argument that mathematics couldn't have rigorous foundations. PM instead showed that it was possible to start from relatively simple axioms and really prove all the way up to a higher level.
PM is NOT, however, important to read or understand itself in detail, as it's been superseded by later works. Syntactically, PM uses a dotted notation instead of parentheses that most people find hard to read & generally undesirable. From a deeper point-of-view, PM uses a set of axioms built on a hierarchy of types. This hierarchy of types was an early effort to avoid various paradoxes. Almost no one uses a hierarchy of types like this today; it's far more common to use Zermelo-Fraenkel set theory with the axiom of choice (ZFC). Even if you wanted to use a hierarchy of types, which is rare, you're probably more likely to use Quine's "New Foundations" which provides a much simpler foundation for mathematics.
It's not important to understand PM in detail, but knowing that it's possible has inspired many more recent efforts, and that is more important.
I argue in my video "Metamath Proof Explorer: A Modern Principia Mathematica" that the Metamath Proof Explorer (MPE) is a successor to PM. MPE uses modern notation (e.g., parentheses) and ZFC set theory combined with classical logic, so it uses modern conventions, but it also tries to prove "everything" from a very few axioms. Thankfully, we can now use computers to verify every last step (with multiple independent implementations), so we can have much more confidence in the proofs. Here's my video, I think you might like it: https://www.youtube.com/watch?v=8WH4Rd4UKGE
That video focuses on MPE, but of course there are several efforts inspired by PM. Understanding the impact that PM had on mathematics is, to me, the important thing.
> 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.
Probably because of constructive math, category theory and theorem provers have got more publicity lately.
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!
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.