[FOM] Has Principia Mathematica been formally verified?
Timothy Y. Chow
tchow at alum.mit.edu
Thu Jul 28 11:45:54 EDT 2011
Thanks to all those who replied to my query, including some who sent me
email but whose replies may not appear on FOM.
I should clarify that my interest is primarily historical. I don't care
about the actual theorems in PM for their own sake, or even so much about
automating the process of finding proofs of those theorems. What I wanted
to know was how much "updating" needed to be done to shoehorn PM into a
modern formalist viewpoint, and, assuming that the answer to that question
was "relatively little," how much correcting and gap-filling would be
needed to get PM to meet the standards of a computer program. I thought
that PM would serve as an interesting benchmark in this regard.
The most relevant work seems to be that of Randall Holmes (pointed out to
me by Peter Smith) and the paper by Kamareddine, Laan, and Nederpelt
(Bull. Symb. Logic 8 (2002), 185-245). They discuss at great length the
issues involved in formalizing PM, and in particular the type theory in
PM, which plays a central role but which is not formalized in PM itself.
It's still not clear to me, though, whether anyone has bothered to go
through PM theorem by theorem and enter everything in the computer (or
have students do so).
More information about the FOM