FOM: Harvey's First Questions to Mathematicians

[Matt Insall]

I am trying to take some time to go through the archives of messages I've 
missed for one reason or another.  In the first place, I did not join FOM 
until late 1999, so I start with the beginning.  Back in 1997, Harvey 
started the list with some questions.  He first made a statement that he 
seemed to think several mathematicians ``find attractive sometimes''.  I'll 
quote it here, for reference:

"I don't care about what can be proved in what formal system. I only care if
the knowledge of that fact gives, as a consequence, something interesting
about the mathematics itself."

I myself frequently have heard statements that seem to follow these 
lines.  However, in my own interests, the question of what formal system 
can be used for what mathematics has been of interest all along, even when 
I have not formulated conjectures or theorems and/or proved theorems about 
such formal systems.

Harvey also asked some questions relating to ``what may be behind this 
disinterest''.  One of these was a question about whether the formal 
systems appear to be artificial or ad hoc.  Personally, I have no problem 
with this aspect, except when it seems to me that something just as 
effective can be obtained in a ``less artificial'' or ``less ad hoc'' 
manner.  First, let me say why ``artificiality'' does not bother me.  As a 
student of mathematics, I found that one of the most interesting things I 
could imagine was the concept of an isomorphism, and how it can be used in 
mathematics.  In linear algebra, we describe various structures to our 
students and then prove that they are isomorphic.  Now, when I have done 
so, I have always thought of isomorphism as ``totally free'', in the sense 
that I am allowed to specify the image set and operations so that the 
function between the spaces (or groups or rings or models [in model 
theory]) is an isomorphism.  This of course is only possible when the 
function is one-to-one and onto.  However, in almost all the reading I did 
before I learned anything about formal systems, a one-to-one function could 
be quite arbitrary and ad hoc.  One can even teach this extreme 
arbitrariness to students of linear algebra, by taking, for example, the 
positive real numbers and some fairly nonlinear bijective function from the 
reals onto the positive reals, and using it to define a vector space 
structure on the positive reals.  I have done this so often I can hardly 
count the number of times.  When I have more advanced students, I ask them 
to consider an arbitrary bijection from the reals onto some other set.  An 
example I do not yet recall using is the plane, but the fact in ZFC (the 
underlying formal system in my advanced linear algebra class), that the 
line and plane are in one-to-one correspondence, is fairly well known to 
the students, so I tell them how to make R^2 into a one-dimensional vector 
space using any given bijection between the two sets.  This amounts to an 
injection of a taste of model theory in an otherwise fairly pedestrian 
course.  (The little bit of model theory that is included is fairly 
pedestrian as well.)  I think that it is quite natural to mathematicians to 
accept the concept of an arbitrary bijection, even when the bijection is 
somehow arbitrary or ad hoc, and this forms a basis for communicating to 
them that the artificiality or ad hoc character of a formal system should 
not be a deterrent for them in deciding what is useful about the results 
derived in such systems.


Another of the questions raised by Harvey involved the statement by some 
mathematicians that mathematics should not be judged by what can be proved 
in what formal systems.  After stating that he responded that since we are 
in a University, we should be judged by the criteria of intrinsic 
intellectual interest, Harvey asked ``what do you think?''  Well, I guess I 
agree with Harvey on this score, to an extent.  Personally, I find certain 
topics interesting and others less so.  But I do not deny the potential 
usefulness of topics outside my sphere of interest or outside my area of 
study.  There are many different worthy pursuits on a University campus, 
and I feel that a good mathematics department will involve itself in those 
pursuits.  One of these is the formalization of as much of mathematics as 
possible, even if we do not believe formalization of all of mathematics is 
possible.  Many mathematicians now use programs like Mathematica, MathCad, 
GAP, MAPLE, etc., and, as I understand it, those programs take advantage of 
various foundational results.  Thus, for these mathematicians, it is 
imperative that the formal systems research be carried on, and that it be 
done well.