Whitehead and Russell’s Principia rewritten in Coq

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

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...

https://github.com/LogicalAtomist/principia/blob/master/PL.v

Well, tons of math books have been typeset before digital typesetting and/or TeX, they had the knack of it by the time.

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.

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.

Probably because of constructive math, category theory and theorem provers have got more publicity lately.

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.

Now making the Latex infra and formalizing can be parallelized, but they are already doing that!