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

[Stephen G Simpson]

Martin Davis 28 May 1999 10:46:08

 > 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 certainly agree, if by ``knowledgeable person'' you means someone
who is familiar with 20th century f.o.m. research.  But I have found
that many contemporary mathematicians do not fall into this category.

Perhaps you think that Conway is in this category.  I am not so sure.
I don't know Conway personally, but I do know that Conway in his book
does not mention or cite any f.o.m. research.  (The only exception is
that he mentions nonstandard analysis briefly, in order to assert that
it is irrelevant to his concerns.)  He seems to know what
formalization is, but he dismisses it by saying ``it seems to us
... that mathematics has now reached the stage where formalisation
within some particular axiomatic set theory is irrelevant'' and
calling on mathematicians to liberate themselves from the alleged
tyrrany of formalization.

I guess we could debate endlessly about what Conway meant, but I'm not
sure there is much point.  It's a shame that Conway apparently never
clarified or amplified his anti-formalization views.

-- Steve