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

[Stephen G Simpson]

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.

Of course Conway's words are open to interpretation.  Exegesis of
vague accusations and claims accompanied by dramatic rhetoric is
always tricky and difficult.  If Conway were not a prominent and
respected Establishment mathematician with a huge following, we would
not even be bothering with this.  But given that Conway is who he is,
I feel that we f.o.m. professionals need to take him seriously.

Thomas Forster 28 May 1999 12:08:29

 > Which bits of mathematics have the NFistes not yet shown how to
 > implement in NF(U) to your satisfaction?  I hope and trust we will
 > be able to oblige you.

Sorry, I expressed myself poorly.  I haven't read the relevant
literature, but my impression is that NFistes have already shown how
to formalize a substantial part of mathematics in NFU, enough to
convince a reasonable person that almost all of mathematics can be so
formalized.

The point I was trying to make is that, Conway notwithstanding, this
kind of formalization work is an essential, indispensable part of
f.o.m. research.

-- Steve