[FOM] Has Principia Mathematica been formally verified?

[Haim Gaifman]

The trouble with PM is that it is a hybrid system, based on a partially 
specified intensional theory
of propositions. On top of this an extensional theory of classes is 
constructed,within which a large chunk of mathematics can be carried 
out. The goal is to vindicate some version of the logicist thesis that 
mathematics is  reducible to logic.  In principle the classes can be 
eliminated by translating everything to the intensional level. That 
level is however not fully specified;  for the purposes of doing 
mathematics many crucial details can be left open; for example, it is 
sufficient to base everything on logical equivalence of propositions 
(and propositional functions), without having to specify the identity 
conditions for them.   The language of PM uses freely the notions of a 
variable , or constant, "occurring in a proposition", which remain 
undefined and which do not match exactly the linguistic notions of 
occurrence in a wff, since the propositions are not linguistic entities. 
Every formalization of PM is therefore an interpretative project that 
requires philosophical  and mathematical work, and  which involves 
judgements about what is more important or essential in the system.

In a talk I gave at the VIG conference at UCLA, this last February ("On 
The Mathematical Content of /Principia Mathematica")/  I presented a 
semantic modeling of PM, which I hope, brings out clearly its main 
structure and some alternatives of interpretation. If we assume the 
axiom of infinity and the predicative principle that underlies the 
ramified system (thus rejecting the axiom of reducibility), then it can 
be shown that the extensional theory is equivalent to a theory whose 
intended interpretation is //*_*_**///L/*_? *_+*?* (/X/)//**_**_**//, 
where /X/is an infinite set of ur-elements. I hope to have the paper 
ready in a couple of months.

On 7/29/2011 11:27 AM, 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.
>
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20110809/bfc6ff23/attachment-0001.html>