[FOM] FOM: Has Principia Mathematica been formally verified?

[Irving]

Timothy Y. Chow asked: Has Principia Mathematica been formally verified?

If I recall correctly, Hao Wang wrote about his work on this project in 
"Computer Theorem Proving and Artificial Intelligence", W. W. Bledsoe & 
D. W. Loveland (editors), Automated Theorem Proving: After 25 Years, 
Contemporary Mathematics 29 (Providence: American Mathematical Society, 
1984), 49-70, and Daniel J. O'Leary, "Principia Mathematica and the 
Development of Automated Theorem Proving", in Thomas Drucker (editor), 
Perspectives on the History of Mathematical Logic (Boston/Basel/Berlin: 
Birkhäuser), 47-53 wrote about the program written by Newell, Shaw, & 
Simon, discussed in their "Report on a General Problem-solving 
Program", IFIP Congress 1959, 256–264, generating all of the theorems 
in Principia of propositional calculus. In mentioning Newell, Shaw, & 
Simon, you may also be thinking of the exchange, reported on p. 52 in 
O'Leary's article, in which, referring to their program , Simon wrote 
to Russell in 1956 reporting to Russell about this. Russell wrote back 
to Simon: "I am delighted to know that Principia Mathematica can now be 
done by machinery. I wish Whitehead and I had known of this possibility 
before we wasted ten years doing it by hand. I am quite willing to 
believe that everything in deductive logic can be done by machinery."


Irving H. Anellis
Visiting Research Associate
Peirce Edition, Institute for American Thought
902 W. New York St.
Indiana University-Purdue University at Indianapolis
Indianapolis, IN 46202-5159
USA
URL: http://www.irvinganellis.info