Formalizability as a Criterion for Mathematical RigourJohn Harrison <John.Harrison@cl.cam.ac.uk>
To: QED <firstname.lastname@example.org>
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>
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
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 )
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 (email@example.com)
P.S. Since the name Bourbaki is bandied about a lot here, I thought I'd point
out an interesting article by Adrian Mathias  criticizing their attitude to
logical and set theoretic foundations (as distinct from their development of
 A. Mathias, "The Ignorance of Bourbaki".
Math. Intelligencer, a few years ago.
 R. D. Tennant, "Semantics of Programming Languages".
Prentice Hall International Series in Computer Science 1991.