# FOM: Harvey's First Questions to Mathematicians

Matt Insall montez at rollanet.org
Thu Sep 21 16:36:35 EDT 2000

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

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.

```