19
$\begingroup$

Russell and Whitehead famously tried to actually create and use a formal system to explicitly develop formal mathematics in their work, "Principia Mathematica."

Much more recently, with the aid of computers, there has been much work done related to the development of proof assistant software, formal verification software, and automated theorem proving software.

However, even though extensive libraries of formal proofs have been developed with all this research, I have not been able to find any attempts made to present the contents of a given library of proofs in an "updated Principia Mathematica," as a formal development of math.

Have I just not done an extensive enough literature search?

Thanks in advance!

$\endgroup$
  • $\begingroup$ Well, some attempts have been made. See for example isa-afp.org and cse.unsw.edu.au/~kleing/top100 $\endgroup$ – mrp May 1 '16 at 18:22
  • 2
    $\begingroup$ Hmm, I am not sure where you get this impression. Proof verification systems like Mizar and coq have had impressive results far exceeding the Principia - proving the Jordan Curve Theorem, for example. $\endgroup$ – Jair Taylor May 1 '16 at 18:23
  • 1
    $\begingroup$ And for instance the Homotopy Type Theory project of Voevodsky et al. is a pretty developped and ambitious project. $\endgroup$ – Captain Lama May 1 '16 at 18:25
  • 1
    $\begingroup$ Right - these are all good points. I have read about coq and some of HoTT. I was just also wondering if anything complete had actually been collected/published which encapsulates a "formal development" of math from axioms, rather than just creating a formal system and then formally proving theorems in that system on an individual basis. $\endgroup$ – JWP_HTX May 1 '16 at 19:29
  • 4
    $\begingroup$ I suggest you revise your question to explain why the libraries for Mizar, Coq, HOL4, etc. fail to meet your expectations. $\endgroup$ – Rob Arthan May 1 '16 at 21:30
14
$\begingroup$

On the one hand, there has been a lot of success recently in creating fully formalized and computer-verified proofs of nontrivial theorems, including Hales' theorem, the prime number theorem, the Jordan curve theorem, and Gödel's incompleteness theorems. The sense I get from experts in the field is that the main challenge is time, not theory. It takes a long time to formalize human-readable proofs into computer-verifiable proofs with the present systems, but there should be no theoretical obstacles to formalizing any theorem one wishes to study.

On the other hand, there are other reasons that nothing explicitly like Principia Mathematica has been developed. The first of these is that Principia is virtually unreadable. As a means of conveying mathematical information from one person to another, fully formal or even mostly formal proofs (the kind that a proof assistant can verify) are not as efficient as ordinary natural-language proofs. This means that few mathematicians have a desire to work with any "new" system of this kind. We already realize that virtually all mathematical theorems can be formalized in ZFC set theory, but instead we write proofs in a way that tries to convey the mathematical insight more than the technical details of a formal system, unless the technical details are somehow important.

There has been a lot of recent work on a different foundational system called "homotopy type theory", which could be used instead of ZFC to formalize theorems. It remains to be seen, however, whether this new system ends up being widely adopted. There other foundational systems, such as second-order arithmetic, which could also be used to fully formalize large parts of mathematics. I believe that a significant number of mathematicians don't really worry much about the foundational system they use, because the objects they deal with are sufficiently concrete that the foundations make little difference.

The other goal of Principia was to support the logicist program that all of mathematics can be reduced to logic. The idea that mathematics can be formalized and presented in full detail is no longer in question, as it might have been at the time. But the idea that the axioms of a foundational theory would all be fully logical is far from clear - in fact, it is generally considered false, because axioms such as the axiom of infinity or the axiom of replacement do not seem purely "logical" to many mathematicians.

$\endgroup$
  • 2
    $\begingroup$ So even though time is an obstacle and the proofs would be hard to read, there's just not a lot of interest in developing math in full formal detail (from say, ZFC) because we basically believe that we can? $\endgroup$ – JWP_HTX May 1 '16 at 19:50
  • 1
    $\begingroup$ Yes, I think that sums it up. Some number of mathematicians would think that developing everything in fully formal detail would take away from time that could be used to "do mathematics", i.e. to prove more theorems in an informally rigorous but not formalized way. $\endgroup$ – Carl Mummert May 1 '16 at 19:56
  • 1
    $\begingroup$ Personally, I wouldn't say that the axioms are illogical unless they are inconsistent. The axioms are just the rules of the game we've agreed to play - you might like them or dislike them, but this is a matter of aesthetics, not logic. $\endgroup$ – Jair Taylor May 1 '16 at 20:04
  • 1
    $\begingroup$ @Jair Taylor: the question is not whether they are logical in that sense; it's about a philosophical distinction between "logical" and "mathematical" axioms that was important to the logicist program. $\endgroup$ – Carl Mummert May 1 '16 at 20:21
  • 3
    $\begingroup$ @Carl: I agree that developing everything in fully formal detail could take away from the actual doing of math, but to me, it seems that there may be a sense in which our mathematical proofs are "better" if the arguments we use are explicitly gap-less. $\endgroup$ – JWP_HTX May 1 '16 at 21:21
1
$\begingroup$

I think that Metamath (list of mirrors) is likely the best candidate for a modern version of Principia Mathematica. The theorem list is broken up into many parts and develops:

  • Propositional calculus
  • ZF, ZFC, and TG (roughly the type of set theory that Mizar uses as well)
  • Real and complex numbers
  • Abstract algebraic structures (including category theory)
  • Topology (a lot of pointset, and some basic definitions for algebraic)
  • Precalculus and Calculus concepts
  • and various other assorted things

Aditionally, Principia Mathematica was an inspiration for Metamath, and a major contributor made a talk on youtube a couple months after the OP's question was posted titled "Metamath Proof Explorer: A Modern Principia Mathematica".


To address @Carl Mummert's point in his answer: "Principia is virtually unreadable...few mathematicians have a desire to work with any "new" system of this kind". I agree. That said, some of those few mathematicians have been working on Metamath, regardless of how it is certainly more difficult to read in some ways than a textbook or paper.

$\endgroup$
0
$\begingroup$

The most promising systems as of 2019

I have talked with people in the area and gone through the description of some of the existing projects, and these seem to be the most promising projects:

I will add more information to this list as I learn more about those systems and try them out myself.

And here are some more interesting links:

One thing which I haven't found yet, but feel is badly missing, is a package register + continuous integration website, a bit like Metamath, but that anyone can contribute to like PyPI, and which runs the proofs and shows them on the web interface. I have described this idea in a bit more detail here.

$\endgroup$
  • $\begingroup$ Lean deserves to be on your list given how much support/drive the people working on it have. $\endgroup$ – Mark S. Jul 20 at 1:10
  • $\begingroup$ @MarkS. thanks! I'll have a look at that one too! $\endgroup$ – Ciro Santilli 新疆改造中心996ICU六四事件 Jul 20 at 8:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.