4 ms·

Yes, it was a tad tendentious, but I don’t think anyone really buys the logicist program anymore. Don’t get me wrong, PM is marvelous and there’s no gainsaying

Yes, it was a tad tendentious, but I don’t think anyone really buys the logicist program anymore. Don’t get me wrong, PM is marvelous and there’s no gainsaying its enormous historical impact. If your characterization of Metamath is correct, I don’t think that’s in the spirit of PM at all. One of the major problems PM had was the rejection of (what later became) the Axiom of Choice in favor of Russell’s convoluted theory of types. Indeed, that set theory (ZFC) is needed to get the rest of the way R&W were trying to go is one of the signal failures of the logicist program behind PM.

dwheeler 3y ago
If you believe the big advantage of Principia Mathematica was that it starts with a very few axioms and then manages to formally and exactly prove many things, then MPE is a worthy successor. I'm in that camp. However, if you think the main point of Principia Mathematica was the very specific set of axioms that they chose, then that's different. The PM authors chose to use a "ramified" theory of types, which is complex. It does have sets, it's just not ZFC sets. Few like its complexities. Later on Quine found a simplification of their approach and explained it in "New Foundations for Mathematical Logic". There's a Metamath database for that "New Foundations" axiom set as well (it's not as popular, but it certainly exists): https://us.metamath.org/index.html https://us.metamath.org/index.html More Metamath databases are listed here, along with some other info: https://us.metamath.org/index.html https://us.metamath.org/index.html
- dmvdoug 3y ago
  Although N.B.: it’s still an open question whether NF is consistent.
  - dwheeler 3y ago
    Strictly speaking that's true for any system that can handle arithmetic (as proved by Goedel). You can show an inconsistency, but you can't prove consistency. No one's found an inconsistency. There are pros and cons for both systems.
    - dmvdoug 3y ago
      Yes, I was too loose with me words again. I was gesturing at relative consistency (especially, at least, when compared to the lack of serious doubt about ZF/C’s consistency), as well as the work of folks like RB Jensen and Randall Holmes. The biggest problem NF has is, as usual, a social one: there just ain’t a lot of people working on, or interested in working on, NF compared to other set theories.

dwheeler 3y ago

If you believe the big advantage of Principia Mathematica was that it starts with a very few axioms and then manages to formally and exactly prove many things, then MPE is a worthy successor. I'm in that camp. However, if you think the main point of Principia Mathematica was the very specific set of axioms that they chose, then that's different. The PM authors chose to use a "ramified" theory of types, which is complex. It does have sets, it's just not ZFC sets. Few like its complexities. Later on Quine found a simplification of their approach and explained it in "New Foundations for Mathematical Logic". There's a Metamath database for that "New Foundations" axiom set as well (it's not as popular, but it certainly exists): https://us.metamath.org/index.html https://us.metamath.org/index.html More Metamath databases are listed here, along with some other info: https://us.metamath.org/index.html https://us.metamath.org/index.html

dmvdoug 3y ago
Although N.B.: it’s still an open question whether NF is consistent.
- dwheeler 3y ago
  Strictly speaking that's true for any system that can handle arithmetic (as proved by Goedel). You can show an inconsistency, but you can't prove consistency. No one's found an inconsistency. There are pros and cons for both systems.
  - dmvdoug 3y ago
    Yes, I was too loose with me words again. I was gesturing at relative consistency (especially, at least, when compared to the lack of serious doubt about ZF/C’s consistency), as well as the work of folks like RB Jensen and Randall Holmes. The biggest problem NF has is, as usual, a social one: there just ain’t a lot of people working on, or interested in working on, NF compared to other set theories.