FOM: role of formalization in f.o.m.; coordinate systems

[Stephen G Simpson]

Holmes 1 Jun 1999 11:57:21

 > I suggest that Simpson should carefully consider the possibility
 > that he is misunderstanding Conway's intentions

But obviously I have considered it.  I don't think I am
misunderstanding Conway.

 > 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 still think that term is consistent with and justified
by Conway's own remarks.  One of Conway's relevant remarks is:

  It seems to us, however, that mathematics has now reached the stage
  where formalisation within some particular axiomatic set theory is
  irrelevant, even for foundational studies.

The surrounding passage is reproduced in full in my posting of 24 May
1999 19:25:58.

It's too bad Conway never took the trouble to clarify or amplify his
anti-formalization remarks, so that we might understand their context
and meaning in Conway's mind.

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
too charitable.  Perhaps their enjoyment of the mathematical content
of Conway's book has blinded them to the poor quality of Conway's
foundational remarks.

 > neither, I think, do many other respondents in the discussion thus
 > far.

Shipman 19 May 1999 14:25:44 says he agrees with me that Conway should
not have said ``even for foundational studies''.  But he offers no
explanation of why Conway *did* say that.  Neither does Holmes.

 > 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?

 > There is nothing in this which suggests that Conway is opposed to
 > formalization per se or does not recognize that it is important;

On the contrary, Conway's remark that ``formalisation within some
particular axiomatic set theory is irrelevant, even for foundational
studies'' tends to show that Conway thinks formalization is
irrelevant, even for foundational studies.

The truth of the matter is that formalization is *very relevant*,
especially for foundational studies, as f.o.m. professionals well
know.  Therefore, I characterize Conway's view as one of opposition to
formalization.  I don't know why Holmes thinks this is unreasonable on
my part.

 > Using an analogy which Conway makes in his discussion in ONAG,
 > formalizations can be regarded as analogous to coordinate systems.

In my opinion this is a very bad analogy.  It is inappropriate and
misleading.

In geometry, there is a well known distinction between analytic and
synthetic geometry.  Synthetic geometry goes back to the ancient
Greeks and is coordinate-free, in the sense that coordinate systems
are never mentioned or used.  Analytic geometry on the other hand is a
modern development and makes essential use of coordinate systems.
Historically, analytic geometry grew out of synthetic geometry by the
introduction of coordinate systems.  Each of the two kinds of geometry
can stand on its own, but there are also some interesting theorems
such as Desargues' theorem which elucidate the close relationship
between them.

In f.o.m., formalization of one kind or another is an important part
of the fabric of virtually all ancient and modern f.o.m. research.
(The Elements of Euclid are an attempt formalize synthetic geometry in
an axiomatic framework.)  Indeed, formalization is of the essence in
f.o.m.  There is no ``formalization-free'' approach to f.o.m.  The
idea of ``formalization-free'' f.o.m. is vacuous.  The idea of trying
to ``liberate'' f.o.m. from formalization is absurd.

Thus the Conway/Holmes analogy between formalization and coordinate
systems breaks down completely.

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.

-- Steve

PS.

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.

However, this line of research is not actually formalization-free,
because the formal theories are still there.  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.  Indeed, he didn't
refer to any f.o.m. research or literature at all.