# [FOM] Has Principia Mathematica been formally verified?

Haim Gaifman hg17 at columbia.edu
Tue Aug 9 11:47:27 EDT 2011

```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>
```