[FOM] Has Principia Mathematica been formally verified?

[Richard Zach]

What's wrong with Carnap's simple type theory in the /Abriss der
Logistik/?  I thought that's where Gödel got it from?

-R

On Fri, 2011-07-29 at 11:27 -0400, Alasdair Urquhart wrote:
> 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.
> 
> 
> 
>