FOM: misunderstandings

[holmes@catseye.idbsu.edu]

Quoting (with approval!) Friedman thus:

It is not easy to talk about formalization in a clear way. Unless one is
almost unprecedently careful, one is surely going to be misunderstood. I
will attempt to be that careful.

(end quote)

I suggest that Simpson should carefully consider the possibility that
he is misunderstanding Conway's intentions in his "foundational"
remarks in _On Numbers and Games_.  I see no "anti-foundational views"
in this passage; neither, I think, do many other respondents in the
discussion thus far.  

What Conway is opposing (if he can be said to be opposing anything) is
"formalization in some specific system", with the accent on commitment
to some specific system, rather than on formalization.  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, which Conway might be expected to find
objectionable on the basis of the remarks in ONAG.

But it is also clear from Conway's remarks that he regards the
possibility of formalizing mathematical results in specific formal
systems (he mentions ZFC) as an important standard of reliability; he
hopes for results which will allow us (under suitable conditions) to
certify reliability under this standard without actually having to
carry out the formalization, which would not be at all a bad thing, if
it were possible.

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

So much for what I think Conway is saying.

As for what I think (Simpson asked for _my_ views...)

Bodies of mathematical knowledge are prior to formalizations, which are
a retrospective activity.  This is less obvious in the case of set theory
(and very much less obvious in the case of logic) where formalization and
mathematical investigation go hand in hand, but I think that there is truth
in this even there.

Using an analogy which Conway makes in his discussion in ONAG, formalizations
can be regarded as analogous to coordinate systems.  A coordinate system
is a valuable tool for talking about a space; one should note, though, that
the same space admits different coordinate systems, and that one can also
learn things about the space by investigating invariants which are independent
of the coordinate system used.

In an area that I know about, much the same piece of the mathematical
universe is formalized by the following theories:

1.  Russell's theory of types with infinity and choice (as simplified
by Ramsey).

2.  Mac Lane set theory (Zermelo set theory with comprehension restricted
to delta-zero formulas)

3.  NFU + Infinity + Choice

4.  topos theory ("category theoretic foundations") with a natural
    numbers object.

These systems have precisely the same consistency strength (I might
have to specify 4 more precisely to make this true).  Classical
mathematics (outside set theory) can be formalized in any of these
systems (with the same caveat about 4; I'm not sure that just having a
natural numbers object is enough to give the needed consistency
strength; of course one has to do some kind of double negation
interpretation to interpret classical results in the intuitionistic
logic of 4 -- perhaps Colin McLarty could help here?).

I would find any of the systems 1-3 about equally easy to work in (though
1 is notationally awkward).  I would find 4 _extremely_ hard to work in.

As regards mathematical intuition, I find 1 and 2 equally reliable
(bedrock!); I know that 3 is reliable (this relies on mathematical
results (Jensen's consistency proof for NFU) which I would think of
initially as carried out in 1 or 2); I believe that 4 is reliable due
to mathematical work (known to me mostly by reputation) which I would
regard as having been carried out in system 2 or extensions (much
harder than the work needed to certify 3 as reliable!)

The reliability of 1 or 2 for me rests on direct intuition of what the
theories are about (my preformal understanding of set theory, typed or
untyped), plus the fact that extensive work in these systems has
revealed no inconsistency (if a contradiction were found I would
conclude that my preformal intuitions had been incoherent).  I am
willing to regard 3 as similarly resting on a direct intuition, but I
don't regard this intuition as obviously correct (the proof of the
consistency of NFU is needed to firm it up for me, but I do understand
this proof...); however, I can regard 3 as an autonomous foundation,
because 3 is an extension of the system 1 (in a direction unexpected
to a ZF-iste, and only if 1 starts without strong extensionality), and
the consistency proof needed to justify 3 can be carried out in 1.  I
have no intuition at all (or very little) for 4, and find it hard to
understand how 4 can be regarded as an autonomous foundational
proposal (though I can imagine that the intuitive understanding of 4
needed for this could be developed).

I would be willing to use any of the systems 1, 2, or 3 (or extensions
-- note that ZFC is an extension of 2, and my reasons for restricting
to 2 have to do only with the fact that this makes it easier to get
systems with exactly the same strength) as my official (formalized)
foundation for mathematics.  Results in classical mathematics obtained
from any of these formalizations are demonstrably equally reliable.  I
do not think that anything is gained by a fanatical devotion to one of
these systems (even 3 :-) ) as opposed to any of the others.  I would
find it extremely difficult to use 4 as an official foundation, and I
am curious about the mindset that makes this appear possible...as I
suppose some are curious about the mindset that makes it possible to
consider 3...but this does _not_ mean that I regard it as impossible to
sincerely adopt 4 as a foundation.

I have used Conway's analogy in my own thinking: 1,2,3 and perhaps 4
are "coordinate systems" covering essentially the same mathematical
terrain.  Results in any of these systems can be "translated" with
more or less difficulty to any other of these systems (1,2,3 being
quite close to each other and 4 rather distant from the others in
terms of ease of communication).  What I am actually studying is not
any of these formal systems, but the "terrain" itself.  If a program
like what Conway proposes in ONAG were possible, I might have tools
which would allow me to evaluate another proposed formal system 5 and
recognize (under suitable conditions) that 5 was another map of the
same terrain.  No commitment to the existence of "mathematical
terrain" (platonism) is required for such a program to make sense; it
could equally well be expressed in terms of features of formal
theories.  Note that such a program could only be carried out with the
full (and very clever) use of the same kinds of logical tools that
are needed in the formalization of mathematics in a fixed system.

It isn't clear to me that an adequate description of "invariants" of
formal theories that would certify them as being as reliable as (say)
ZFC would not be effectively a formalization of mathematics in its own 
right, usable as an official foundation of mathematics.  (I.e., I think
that a program like Conway's might be formally interesting, but I think
that the result might simply be another formulation of ZFC foundations).

I return to Friedman's quote and reiterate his warning that these things
are extremely hard to talk about!

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