I get to André Rodin's comments, and the redoubtable John Mayberry, below. 2009/11/12 Joyal, André <joyal.andre@uqam.ca>: Writes what I entirely agree with:
I am convinced that categorical logic, which was wholly invented by Lawvere, is the most important development of logic during the second half of the 20th century. I find the notion of elementary topos absolutely extraordinary, almost magical.
I only mean it is not extraordinary that with enough time the developments become generally known.
Like every important mathematical discovery, it stands out as a colorful gem on a bed of grey stones.
This imagery makes perfect sense to me, for many great examples such as the complex numbers as André described. But I don't know if I could convey it to many philosophers of mathematics even in the most general terms -- let alone convince them anything to do with category theory is an example. Most philosophers, so far as I know, still consider the complex numbers far-fetched and "impossible to visualize" (which I find incredible).
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.
Yes. And I agree with what André said earlier that there is room here for possible further insights into what remain profound mysteries about the hierarchy of infinite cardinals. (I do not claim to currently have those insights!)
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.
I am not happy to call it "magic" -- I collected rocks as a teenager and once did catch a "gem" (a thick tuft of pink-grading-to-green byssolite hairs with bright pyrite crystals suspended in them, 4 feet down a gray rock crevice that I could barely crawl into) but I do not call that "magic" either. Perhaps this is mostly a difference over words. 2009/11/12 <Andre.Rodin@ens.fr>: writes
I do NOT believe that ETCS and CCAF "work perfectly well". Each of these involve two foundational "layers", namely, the classical "bottom" and a categorical "superstructure". By the classical bottom I mean NOT an underlying Set theory but the "Elementary theory of categories" (ETC), i.e. a theory of categories using the usual First-Order Logic (FOL) and relying on the standard Hilbert-Tarski-style axiomatic method. I agree with John Mayberry and some other people who argue that this aximatic method alone assumes a basic notion of set or collection.
Mayberry says two things about this. The first, which has taught me a lot, is his stress that no formalization can be the basis of our actual knowledge of mathematics. This applies to all formalized foundations. Mayberry's point is precisely the reason why I say that ETCS and CCAF " work perfectly well, in formal terms." It is a plain fact that these axioms work as well as the formal ZFC axioms --- while Mayberry is right that formalized axioms cannot be the real basis of our knowledge. I believe John has underrated the dialectical relation between formalization and "the real basis of our knowledge." I have often discussed this with him and I am not sure exactly what he thinks about it now. Formal investigation of ZFC has changed our actual beliefs about sets. Category theory has further changed our actual beliefs about mathematics, and formal investigation of ETCS and CCAF has been part of this. But the key point is that ETCS and CCAF are not only formal axioms, any more than ZFC is. All are formalizations *of* our real beliefs about sets and categories. These real beliefs do not "assume a basic notion of set or collection" but rather *include* or *express* a basic notion. The next thing John says is that our basic notion of collection is best captured by ZFC. (Or, rather, he used to say that prior to developing his finitary set theory as an alternative foundation.) I say ETCS formalizes almost the same idea of set, but better than ZFC. The ETCS formalization is rather like the ZFC one, but omitting a lot of irrelevancies about transfinitely iterated membership. Zermelo and then Fraenkel and Skolem found these in the first attempts at axiomatization and I don't say i could have done better in 1908 or 1922. I say Eilenberg and MacLane's work of 1945 enabled Lawvere to do better in 1963. But even before Bill did that he had already seen that our basic notion of collection is not so much like that. It is typified by, say, the continuum, or the collection of Euclidean motions of the plane, and such. Our basic notion of the continuum is not that the discrete collection of points on it is equinumerous with the powerset of the natural numbers, and it is equipped with a lattice of open subsets -- our "basic notion" of it is rather a somewhat open-ended notion of continuous translation. The basic notions are in fact not very articulate in themselves, and throughout the history of mathematics it has taken further ideas to articulate them. Bill saw how to articulate these and many more, quite directly, in categorical terms not assuming any prior set theory. That articulation works even if you do not take it as foundational. But it gets a natural foundational character in the framework of the category of categories -- thus CCAF, the axiomatic theory of the category of categories as a foundation. best, Colin Unlike Mayberry I don't think that this fact implies that
the project of categorical foundations, as a alternative to and replacement for set-theoretic foundations, is futile. Recall that the axiomatic method we are talking about (which is, of cause, quite different from Euclid's method and other earlier versions of axiomatic method) emerged together with Set theory. In order to make categorical foundations into a viable alternative of set-theoretic foundations we still need to provide Category theory with a new axiomatic method rather than use the older axiomatic method as do ETCS and CCAF. Elements of this prospective axiomatic method are found in what I just called the "categorical superstructure" of ETCS and CCAF but as far as these theories are concerned the classical background (FOL+ETC) is indispensable. This is why I say that ETCS and CCAF do NOT work perfectly weel as categorical foundations. Building of "purely categorical" foundations remains an open problem. It is not a matter of a ideological purity but a matter of complete "rebuilding" (Manin's word) of foundations: in my view, such a rebuilding is healthy and refreshing in any circumstances (unless it clashes severely with practice).
best, Andre
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]