Formalizability as a Criterion for Mathematical Rigour

• Mail folder: QED
• Next message: Phil Windley: "Re: a multilingual approach "
• Previous message: guttman@linus.mitre.org: "Re: a multilingual approach "

To: QED <qed@mcs.anl.gov>
Subject: Formalizability as a Criterion for Mathematical Rigour
Date: Tue, 13 Apr 93 22:40:18 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-id: <"swan.cl.ca.893:13.04.93.21.40.32"@cl.cam.ac.uk>
Sender: qed-owner
Precedence: bulk

The influence of Bourbaki on the accepted structure of mathematics surely goes
beyond a few bits of arcane terminology like "quasi-compact", and has
substantially altered the emphasis placed on certain areas, e.g. uniform spaces
and  filters. I suggest that a project of formalization like QED might effect
similar changes.

If certain areas seem hard to formalize in the QED system, it may not point to
a flaw in QED (whatever it turns out to be), but rather indicate that the
mathematical notions concerned have not been established with sufficient rigour
and clarity, and should be redeveloped in a careful way, or subsumed in a more
abstract, and therefore simpler, theory. (Perhaps the development of algebraic
geometry this century is a good example.) It is a commonplace in Computer
Science that formal semantics of programming languages should be used in
language design, e.g.

  "The hitch is that defining a language a posteriori, i.e. after its
   design has been frozen by the existence of implementations and users,
   can hardly improve it. To create a good programming language,
   semantics must be used a priori, as a design tool that embodies and
   extends the intuitive notion of uniformity."

    (John C. Reynolds in [2])

Is it stretching an analogy too far to hope for a similar attitude to the
formalization of mathematics?

Of course this is not to deny that a dogmatic faith in a particular
foundational system is much worse than a dogmatic faith in existing
mathematics. Indeed, various foundational programmes have had to modify their
original goals a little in order to formalize actual mathematics. For example,
the logicists Russell and Whitehead stretched the notion of `logical' to
incorporate the Axiom of Infinity; the formalist Gentzen stretched the concept
of `finitary' to attain a consistency proof for arithmetic. Intuitionists
tended to be less flexible, but they were intent not on codifying existing
mathematics, but with creating a new mathematics.

John Harrison (jrh@cl.cam.ac.uk)

P.S. Since the name Bourbaki is bandied about a lot here, I thought I'd point
out an interesting article by Adrian Mathias [1] criticizing their attitude to
logical and set theoretic foundations (as distinct from their development of
mathematical structures).


[1] A. Mathias, "The Ignorance of Bourbaki".
Math. Intelligencer, a few years ago.

[2] R. D. Tennant, "Semantics of Programming Languages".
Prentice Hall International Series in Computer Science 1991.