**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.