[FOM] Has Principia Mathematica been formally verified?

[Martin Davis]

On July 26, 2011, Stephen Cook wrote:

>    Hao Wang followed up on the work of Newell, Shaw, and Simon in
>"Toward Mechanical Mathematics" [IBM Journal of Res. and Dev. 4, 1960].
>His program on the IBM 704 proved all 220 theorems of the propositional
>calculus in PM, as well as proving over 100 theorems in the predicate
>calculus with equality.

It's worth noting that Hao's program (for which he received an award) 
did not attempt to verify the correctness of the proofs as given by 
Whitehead and Russell, or indeed to provide proofs in their style. 
The inputs to his general-purpose theorem-prover were just the 
statements of the theorems.

This was quite different from Newell, Shaw, and Simon's program which 
did provide proofs in Principia style from the axioms. Wang was quite 
critical of their approach.

                                                         Martin


Martin Davis
Professor Emeritus, Courant-NYU
Visiting Scholar, UC Berkeley
eipye + 1 = 0