[FOM] Has Principia Mathematica been formally verified?
Timothy Y. Chow
tchow at alum.mit.edu
Tue Jul 26 10:41:57 EDT 2011
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
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.
More information about the FOM