[FOM] Has Principia Mathematica been formally verified?

[Alasdair Urquhart]

It is well known that Principia Mathematica does not even come
close to being a formal system in the modern sense.  The first
fully rigorous versions of simple type theory are those of Goedel and
Tarski.  (F.P. Ramsey's version of simple type theory is also
lacking in rigour.)

As for ramified type theory, formalizations have
been given by Church, Myhill and Schutte, but people continue
to argue whether these versions are a correct formalization of
the "system" of PM.  Goedel's remark in "Russell's mathematical
logic":

 	It is to be regretted that this first comprehensive
 	and thorough-going presentation of a mathematical
 	logic and the derivation of mathematics from it
 	is so greatly lacking in formal precision in the
 	foundations (contained in *1-*21 of Principia) that
 	it presents in this respect a considerable step
 	backwards as compared with Frege (Collected Works,
 	Volume II, p. 120)

is completely accurate, and even perhaps charitable.

As for formal verifications of PM, the only work that I know
of in this direction is that of Daniel J. O'Leary, reported
in "Russell: the Journal of the Bertrand Russell archives",
Vol. 8 (1988), pp. 92-115.  O'Leary verified only the propositional
part, which is, from the point of view of rigour, one of the
least problematic parts of PM.