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

[Stephen G Simpson]

Holmes 1 Jun 1999 14:48:48

 > Conway appears to oppose "formalization in a specific system", with
 > the emphasis not on _formalization_ but on the insistence on a
 > specific formal system.

But all formalization *is* formalization in some specific formal
system.  So it seems to me you are making a distinction without a
difference.

 > I'm not sure that Conway claims to have such a metatheorem; 

I think he is claiming it, because he says: ``It can be shown that any
theory satisfying the corresponding restrictions can be formalised in
ZF together with sufficiently many axioms of infinity.''  Which axioms
of infinity?  No answer.  Is this pure bluff?  There's no way to be
sure, but so far as I can tell, Conway never followed up with a more
detailed explanation.

 > the author of a manifesto should follow it up with a detailed
 > program!

And Conway never did that.

Shipman 01 Jun 1999 18:26:38

 > it is more accurate to accuse Conway of being against formalization
 > (in certain contexts) than against foundationalism.

Maybe so.  But formalization is essential to f.o.m.  If a prominent
Establishment mathematician dismisses formalization as irrelevant (as
Conway does), then it seems to me that person is in effect attacking
and undercutting huge swaths of contemporary f.o.m. research.

 > ONAG is quite rigorously formal for a mathematics book; but the
 > formal system involved is not ZFC ...

There is no good reason not to formalize it in ZFC, or at worst VNBG
plus global choice, which is conservative over ZFC.  In this sense,
Conway's anti-formalization remarks (including the dramatic rhetoric
about a Mathematicians' Liberation Movement) are making a mountain out
of a molehill.

-- Steve