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

[holmes@catseye.idbsu.edu]

Simpson said in reply to quoted remarks of mine:

 > I see no "anti-foundational views" in this passage;

Both Holmes and Shipman accuse me of accusing Conway of
anti-foundationalism, but I never did so.  I did however use the term
*anti-formalization* to describe Conway's view that formalization is
irrelevant.

I reply:

You are correct.  I should have said "anti-formalization".  But I clarify
this below, where I say that in my opinion Conway appears to oppose
"formalization in a specific system", with the emphasis not on
_formalization_ but on the insistence on a specific formal system.

Simpson said:

I think it was somewhat irresponsible of Conway to make his
anti-formalization remarks without a full, detailed explanation.

I don't think Holmes and Shipman realize how much damage this kind of
irresponsibility can cause.  I think their attitude toward Conway is
much too charitable.

I reply:

This is a good point, though I don't think Conway is being all that
obscure.  I would have appreciated seeing at least a hint as to what a
formalization of his principles i and ii would look like.

For the record, I do know that figures with public reputations can
do damage by making statements which are open to unfortunate interpretations.
However, I don't think that any of us can avoid making such statements:
even if we qualify everything we say carefully so as to avoid this,
the malicious will always be able to take some remark we make out of
context (and those with public reputations can expect to be treated
in this way).

Simpson says:

 > I think that Conway can be understood as objecting to views which
 > regarded some specific system (say ZFC) as the indispensible core
 > of foundations of mathematics: of course, Simpson either holds or
 > appears to hold views of exactly this kind, ...

I don't hold views of this kind.  I do however hold that formalization
is an essential part of modern f.o.m. research.  Does anyone dispute
this?

I reply:

I'm delighted to hear that you do not hold views of the sort I tentatively
ascribed to you above :-)  I certainly agree that formalization
is an essential part of modern f.o.m. research; it is not clear that
Conway disagrees (and in fact (as you point out below) the program he
suggests cannot be carried out without the tools of formalization).

Simpson says:

Conway bluffed about having a metatheorem which would provide a
formalization-free approach to f.o.m.  However, he never stated the
metatheorem, and if he ever does state it, I bet it will involve
formalization anyway.

I reply:

I'm not sure that Conway claims to have such a metatheorem; I think he
suggests that it might be fruitful to look for one.  As I observed
above, it would have helped if he had outlined his formalization of
principles i and ii (he does claim to be able to formalize them!); one
could then tell exactly what he is talking about.  I agree that it
would involve formalization anyway (I think I said that in the post
Simpson is responding to).  In fact, I suggested that an adequate description
of invariant features of formal theories that would allow interpretability
in ZFC would probably itself be a formalization of mathematics :-)

Simpson says:

I can think of at least one serious line of research which might
suggest (to some people) the existence a formalization-free approach
to f.o.m.  Namely, there is the well known and extremely important
f.o.m. idea of classifying foundational formal theories into
hierarchies according to relative interpretability or relative
consistency strength.

I reply:

The context strongly suggests that this _is_ what Conway is talking
about (that he is proposing to look for a metatheorem which would allow
one to verify that broad classes of formal theories are interpretable
in ZFC-like theories without actually carrying out the formalizations).

Simpson says:

However, this line of research is not actually formalization-free,
because the formal theories are still there.  

Holmes replies:

This I agree with (but I think that Conway might agree as well; the
advantage he appears to see in pursuing such a metatheorem is freedom
from the accidental details of particular formal theories).

Simpson says:

And I don't think this is what Conway had in mind, because he didn't
mention anything like this, and he dismisses formalization as
irrelevant.

Holmes replies:

Charity still forbids me from agreeing that Conway dismisses formalization
per se as irrelevant; it is in fact fairly clear that he does not (or he
wouldn't care about proving the metatheorem that he proposes).  I might
agree that the phrasing he uses is unfortunate, but it is permissible
to be deliberately provocative in informal contexts (Simpson is perfectly
capable of being deliberately provocative himself).  

Any manifesto which is short and pithy enough to command attention 
will be short enough to admit the danger of unintended and unfortunate
interpretations.  If a manifesto does not command attention, it does
not fulfil the function of a manifesto.  But it is also the case that
the author of a manifesto should follow it up with a detailed program!

And God posted an angel with a flaming sword at | Sincerely, M. Randall Holmes
the gates of Cantor's paradise, that the       | Boise State U. (disavows all) 
slow-witted and the deliberately obtuse might | holmes at math.idbsu.edu
not glimpse the wonders therein. | http://math.idbsu.edu/~holmes