[FOM] mathematics as formal

[Vaughan Pratt]

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!).

Vaughan Pratt