FOM: role of formalization in f.o.m.

[Martin Davis]

At 12:34 PM 5/28/99 -0400, simpson at math.psu.edu wrote:

>Martin Davis 27 May 1999 18:23:18 
>
> > To see what I take Conway to be "dismissing" have a look at
> > Principia Mathematica.  I refer you to proposition *110.643 on p.83
> > of volume 2: 1+1=2
>
>Many mathematicians, e.g. Poincare, have criticized Principia
>Mathematica as allegedly irrelevant on the grounds that 1+1=2 emerges
>only after many pages of formulas.  But I don't think this is what
>Conway was getting at.  Note first that Conway never alludes to
>Principia Mathematica or 1+1=2.  I quoted Conway at length in my
>posting of 24 May 1999 19:25:58.  Conway's words indicate to me that
>he wants to dismiss and undercut the entire issue of formalization as
>such, by making vague claims to the effect that he knows how to avoid
>it, by means of an appropriate metatheorem.  I think this reading is
>strongly suggested by Conway's words.

Steve, I wrote a book on nonstandard analysis, in which formalization (at
least of statement, if not of proof) is crucial. The need to argue that
certain statements and/or proofs can be formalized is so much a part of so
much ongoing and (by now) classic research of the greeatest importance, that
no sensible knowledgeable person could deny it.

I have not read Conway's book. I have experienced competent sympathetic
comment when we were both speakers at a symposium at CUNY. I have read
carefully your excerpts. As  I have said, all he is telling mathematicians
is that the ground is secure and they can go ahead and make whatever
constructions they need without fear. 


                           Martin Davis
                   Visiting Scholar UC Berkeley
                     Professor Emeritus, NYU
                         martin at eipye.com
                         (Add 1 and get 0)
                       http://www.eipye.com