Dear Colin, I thank you for your interesting comments and observations. I just realised that ETCS means <Elementary Theory of the Category of Sets> and that CCAF means <Category Theory as a Foundation>. I am convinced that categorical logic, which was wholly invented by Lawvere, is the most important developpement of logic during the second half of the 20th century. I find the notion of elementary topos absolutly extraordinary, almost magical. Like every important mathematical discovery, it stands out as a colorful gem on a bed of grey stones. A classical example of gem is the field of complex numbers. The numbers were introduced by Cardan as a trick for computing the root of third degree equations in a case where his formula was not working. The idea of inventing a square root of -1 to solve the problem was crazy but it worked. The fact that the new system of numbers turns out to be algebraically closed was proved by Lagrange and Gauss but it could not be foreseen by Cardan. Equally unexpected is the role of complex numbers in quantum physics. Similarly, I find astonishing that ETCS should be closely related to topos theory via the notion of an elementary topos. It is also surprising that the internal logic of a topos should be formally identical to intuitionistic set theory. The construction by Hyland of the realizability topos is also extraordinary because of the connection with recursive function theory. One may argue that there is nothing magical in mathematics, since mathematics is rational by nature. I disagree. We are far from understanding completely the natural world, and mathematics is not a pure construction of the rational mind. Mathematicians are probing in the depth of a highly structured unkown. If we are patient and lucky enough we may catch a gem. The gem has a structure of its own and we can learn from it. This is were the magic is. best, Andre -------- Message d'origine-------- De: categories@mta.ca de la part de Colin McLarty Date: mer. 11/11/2009 11:38 À: categories@mta.ca Objet : categories: Re: pragmatic foundation 2009/11/6 Andre Joyal <joyal.andre@uqam.ca>: writes
I invite everyone to read the interesting interview of Yuri Manin published in the November issue of the Notices of the AMS:
Manin is always entertaining but not very careful about what he says. André says:
The foundational framework of Bourbaki is very much in the tradition of Zermelo-Fraenkel, Godel-Bernays and Russell. I am aware that Bourbaki was more interested in the development of mathematics than in its foundation.
I agree. Naturally Bourbaki was in a better situation to make up a system that would work, since they had the others behind them. And still their system did not work in fact. Russell was more concerned with philosophic issues of logic, but his touchstone for logic was that it should work! (He was very clear about this by 1919, in his Principles Of Mathematical Philosophy.) He knew a lot less than Zermelo about what would work for two reasons: Russell got into it much earlier, and Russell studied math as a philosopher at Cambridge while Zermelo studied it as a mathematician with Hilbert in Göttingen and in debates with Poincaré. All these people sought a foundation that would make sense in itself and would work. Naturally they had different emphases, partly shaped by the different resources they could draw on. Russell, Zermelo, and Gödel all read each other (recalling that Russell was 59 years old, and two decades past his work on logic, when Gödel published the incompleteness theorem, and everyone took years absorbing it).
In the interview, Manin also said that:
And so I don't foresee anything extraordinary in the next twenty years.
Of course we do not expect to *foresee* extraordinary things.
Probably, a rebuilding of what I call the "pragmatic foundations of mathematics" will continue.
That is a pretty safe bet.
By this I mean simply a codification of efficient new intuitive tools, such as Feynman path integrals, higher categories, the "brave new algebra" of homotopy theorists, as well as emerging new value systems and accepted forms of presenting results that exist in the minds and research papers of working mathematicians here and now, at each particular time.
Yes, there will be progress on all of these things. I myself am also confident that people will calm down and notice that axiomatic categorical foundations such as ETCS and CCAF work perfectly well, in formal terms, and relate much more directly to practice than any earlier foundations. One hundred and fifty years of explicitly foundational thought has made this progress possible. By now, that can hardly qualify as "extraordinary"! best, Colin [For admin and other information see: http://www.mta.ca/~cat-dist/ ]