FOM: this and that

[holmes@catseye.idbsu.edu]

Happy Holidays to everyone, and enjoy the Millennium Bug (and
next year the Millennium :-)

Re the proper definition of mathematics:

Mathematics is the study of abstract data types, specifiable in the
language of second-order logic (there is no requirement here that the
mathematician actually specify them this way :-), without qualms about
the possibility of implementation (the last clause indicates why
mathematics is not subsumed by theoretical computer science).

Re things which ought to happen in the future in FOM (I'm not
going to say what _will_ happen):

I hope that the hypnotic influence of the truly marvellous and useful
theorems about first-order logic lifts enough for more mathematicians
to recognize that second-order logic is also ... logic.  First-order
logic is vitally important as the basic machine of inference, but
second-order logic is needed for the (equally "logical") purpose of
enabling the precise definition of mathematical concepts.  It is of
course inconvenient that second-order logic does not admit complete
rules of inference (but it inherits perfectly adequate partial rules
of inference from first-order logic, with rules for quantification
extended to second-order quantifiers).  Higher order logics are
interpretable as second-order logic with extra non-logical
assumptions.

I hope that philosophy of mathematics and general philosophy begin
talking to each other, particularly about "ontological commitments".
The effect of this will probably be to cast some doubt on the wisdom
of relying on a system as strong as ZFC (or even as strong as the
theory of types or NFU with infinity), since these systems talk about
very large worlds!  I certainly hope that the former beautiful systems
(and even stronger ones) continue to be studied (I decline to be
driven out of Cantor's paradise :-), but I would guess that the right
level of strength for a foundational system is somewhere around the
level of third order arithmetic (the strength of the second-order
theory of real numbers).  Of course, if one thinks that the world is
finite or that the world is infinite but discrete then one might
prefer still weaker systems.  (Nothing here is intended to discourage
investigations of assertions about small structures which have high
consistency strength; in fact the viewpoint suggested here should
encourage such investigations as demonstrating the applicability of
strong systems whose ontological commitments are dubious.)

I hope that truly user-friendly systems for computer-assisted
reasoning come into general use; I think that we are just short of the
threshold for such systems to be of practical use to at least some
mathematicians (I would not suggest my own theorem prover for this
purpose; I'm thinking of something like an extension of Mizar).
Certainly the demands of theoretical computer science will continue to
act strongly on the foundations of mathematics (for one thing,
computer scientists are often more conscious of their foundational
needs than mathematicians: witness my borrowing of the term "abstract
data type" for the purposes of a definition of mathematics above),
so we ought to get something in return!

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.boisestate.edu
not glimpse the wonders therein. | http://math.boisestate.edu/~holmes