[FOM] Has Principia Mathematica been formally verified?

[Marcin Mostowski]

The topic is interesting for me. I have thought a lot of it.
So I feel provoked to comment your posting.

1. I do not think that formalizing in any proof checking system the proofs from PM would be reasonable today. Currently we know about foundations of mathematics much more than Russell and Whitehead. We have have much better understanding of proof theory and practice of proving, and - last but not least - we have much better proofs of the relevant theorems. Surely PM was very important step in our understanding mathematical proofs - moreover still you can meet mathematicians which did not pass this lesson - nevertheless currently its significance is mainly historical.

2. In 1980-ties I was strongly engaged in the proof checking system Mizar, in mathematical, metatheoretical and practical programming ways. The system was intended as allowing simulation of usual mathematical practice. When I left Bia\l ystok - the main place of the project - I went deeper into theoretical and philosophical interests. Nevertheless I know that the project is still alive and it is oriented toward organizing the database for mathematics. As far as I know currently it is much richer than PM. Of course it is still much smaller than Bourbaki’s project - which develop the idea of PM - nevertheless it is not only larger than PM but also computer checked. So summarizing the work was done in a much better version than you expected.

3. You suggest that the paper by Newell, Simon, and Shaw was apparently rejected for publication. I agrees with my experience. Currently mathematics is a social game oriented toward obtaining new results. Older problem is solved - better result, more difficult proof - better result. I am not claiming that it is wrong - only a little bit stupid - because it works. It forces young mathematicians to fight, to work strongly, and finally, to find new research areas. According to my experience FOM is the only forum in the world for discussing foundation of mathematics beyond of the mentioned scheme but still in agreement in mathematical standards.

Marcin Mostowski

_______________________________________________________

For reference I am citing the original post by Tim 


"I have a vague recollection that I once saw a paper or perhaps a master's
thesis that attempted to verify all the proofs in Russell and Whitehead's
PM mechanically with a computer.  Does anybody else know of such a
documented effort?

Though I've never made a serious effort to read PM in detail, my
impression is that their approach was not what we would today consider
purely formal, in the sense of providing purely syntactic rules for
everything.  Still, it would seem that formalizing PM and putting it into
a computer should be a relatively straightforward, if tedious, exercise.

If a full verification of PM doesn't exist, then I'm wondering if anyone
has at least programmed up a modern formalist description of the system.

I'm aware that Newell, Simon, and Shaw wrote a program in the 1950's
called Logic Theorist that was designed to *find* proofs of PM theorems.  
Though this isn't exactly what I'm asking about, it's close.  
Unfortunately I haven't been able to find too many details of how Logic
Theorist chose to formalize things, since their paper was apparently
rejected for publication."
_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom