[FOM] mathematics as formal
pratt at cs.stanford.edu
Thu Mar 6 20:08:39 EST 2008
catarina dutilh wrote:
> There are two related but independent issues here: one issue is when
> mathematics became formal in OUR sense(s) of formal (e.g. mechanically
> checkable proofs, among others); the other issue, and the one I'm
> interested in at the moment, is when mathematics began to be seen
> as formal, in THEIR (i.e. past mathematicians and philosophers of
> mathematics) sense(s) of formal.
A third issue (or issues 3-5 depending on how one counts) that seems to
me to be separate from the above two is the extent to which formality
bears on each of the nature, practice, and foundations of mathematics.
My impressions are as follows.
Nature. To my thinking the nature of mathematics is abstraction of our
experience sufficient to give the abstraction an independent existence
in a mental or conceptual world. More important than formality is
simplicity of specification of the abstraction, without restriction
however on the complexity of the attendant issues and questions it
raises. Formality can serve mathematics by clarifying and
disambiguating it, and by providing a basis for the mechanization of
mathematics. These roles make formality less an intrinsic component of
the nature of mathematics than a source of ancillary services.
Practice. Formality works strongly against both the discovery and the
dissemination of mathematical results. When working out ideas on a
sheet of paper or solving problems during a boring movie, my notes and
thought processes are jumbles of ideas having little discernible formal
content and yet I still manage somehow to come up with theorems. Then
there's those of us who wake up in the morning with the previous night's
problem magically solved with no idea how it happened. Perhaps our
subconscious pushed formal symbols around diligently while we slept, but
I don't find that hypothesis terribly plausible, despite not having a
better one to replace it with. For all I know there is some geometrical
modeling program at work that tries assembling various shapes until
things fit together. Or perhaps my subconscious taps into a wormhole to
an astral plane where the answers are lying scattered around waiting to
be picked up. Neither of these hypotheses are any more compelling than
the formal symbol manipulation hypothesis.
Regarding dissemination, I'm quite good at, and even enjoy, translating
mathematics into various formal systems including ZFC, various
equational logics, and category theory, having done a fair bit of that
sort of thing in the 1970's while working on theorem provers for program
verification. So if I thought it would help dissemination at all I
would gladly oblige journal editors by presenting my theorems formally.
I don't do so because I fear the audience for my papers would be even
smaller than it already is, and moreover I don't particularly want to
reach that very small minority for whom a Principia Mathematica-like
formalism makes more sense than natural mathematical discourse of the
kind standardly published as I find such people a little scary.
Foundations. This is where formality is most commonly found. However
foundations is no more mathematics than a boiler room is an office,
though the more high tech boiler rooms stand to benefit from the
applicable mathematical, scientific, and technological advances.
Offices are where one gets work done, for which boiler rooms perform a
valuable service by supplying certain kinds of resources. How one
organizes boiler rooms and foundations is very much a cultural thing,
there are multiple ways of going about it all serving the same end of
making the workspace habitable. Formality in foundations is like steam
in a boiler room: part of how it works, but having little bearing on the
nature of the work done in the office.
However to say that formality is found mainly in the foundations rather
than in the nature or practice of mathematics is not to identify
formality with foundations or even to say it is the greater part of it.
Just as the infrastructure for a building is much more than the steam
it manages, so is foundations much more than mere formality. The
present discussion aside, it would seem that very little of what is
discussed on FOM is driven by any sort of concern for formality. Most
threads on FOM seem more intimately coupled to the practice of
mathematics, regarding formality as a tuxedo one could put on if the
occasion demanded it, but rarely finding any need to do so. Not to say
never---I recall a drawn-out discussion on FOM with Steve Simpson a
decade ago where our disagreement as to whether a Boolean algebra was
the same thing as a Boolean ring might have been settled more quickly
had we defined "is" formally from the outset (shades of Bill Clinton!).
More information about the FOM