[FOM] Has Principia Mathematica been formally verified?

Stephen Cook sacook at cs.toronto.edu
Tue Jul 26 14:48:37 EDT 2011


Tim,
    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.

Stephen Cook


On Tue, 26 Jul 2011, Timothy Y. Chow wrote:

> 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.
>
> Tim
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>


More information about the FOM mailing list