Selon Colin McLarty <colin.mclarty@case.edu>: CM: Andre.Rodin@ens.fr Suggests a better take on CCAF than the one he has been taking. That would be a take based more on Bill's published work on CCAF, and less on the philosophical objection that Geoff Hellman used to make about CCAF. Geoff himself has given up this objection. AR: I don't know about Hellman's objection about CCAF and would be grateful for the reference. Talking about CCAF I mean first of all Bill's 1966 paper (leaving aside the problem noticed by Isbell as irrelevant to my story), rather than later versions of CCAF. I don't quite understand what does it mean a "better take" but if this means my argument then this argument is based on its own (as, in my understanding, any philosophical argument should be) but not on works of other people. CM: This is the Hilbert conception where axioms are not asserted as true but offered as implicit definition; and so they are not about any specific subject matter but may be applied to whatever satisfies them. Lawvere from 1963 on has always been clear that his first order axioms ETCS and CCAF can be taken this way for metamathematical study -- but that he does assert them as true specifically of actual sets and categories. (Now Bill is not talking about any idealist truth or objects. He takes a dialectical view. But that is another topic.) AR: This is an interesting aspect of the issue, about which I didn't think earlier. It might have a bearing on what I'm saying but so far I cannot see that it does. I am saying this: the axiomatic method in its modern form - which has been pioneered by Hilbert (among other people including Dedikind, et al. ) and then further developed by Zermelo, Tarski et al.) - involves a preformal notion of set or collection. Whatever first-order theory is built by this method objects of such a theory form preformal sets. In particular, when this method is used for building ETC then primitive objects of this theory called "morphisms" form preformal sets called "categories". In THIS sense the preformal notion of set remains a foundation of ETC. As far as I can see this situation doesn't depend on whether one thinks about axioms of ETC (or any other first-order theory) as assertive or as implicit definitions. CM: But even take the interpretation corresponding to any one object A of CCAF. That amounts to specifying X as A in the parametrized interpretation. This interpretation does not deal with "the collection of objects of A" and "the collection of morphism of A". It never refers to any such collections. It deals with categories A,1,2,3, and functors among them. AR: Right. This is exactly the reason why I say that CCAF has two well-distinguishable foundational "layers". At the first layer (ETC) a category is a collection of morphisms; at the second layer (i.e., in the core fragment of CCAF called in 1966 paper "basic theory" ), as you rightly notice, a category is no longer a collection. My problem with this is actually twofold. (1) The second layer depends on the first but not the other way round. Formally speaking, this simply amounts to the fact that axioms of ETC are axioms of BT but not the other way round. In THIS sense, once again preformal sets remain a foundation of CCAF. (2) The joint between the two layers remains for me unclear. From a formal viewpoint this looks trivial: CCAF is ETC plus some other axioms. But this doesn't explain the switch from thinking about categories as collections to thinking about categories as identity functors. In Bill's 1966 paper this switch is described as a new terminological convention made in the middle of the paper (that cancels the earlier convention). This change of notation points to but doesn't really addresse the issue, as far as I can see. CM: you would do better to notice the novelty of these parametrized and single-category interpretations of ETC in CCAF and take this as the kind of major change that you expect to see. AR: I do see this as a great novelty. But I claim that this novel approach in the given setting (i.e. in CCAF) doesn't work *independently* of the older approach; moreover there is a sense in which the older approach remains basic while the new one is a "superstructure". CM: This different axiomatic method is explicit in CCAF, and does work independently there. Specifically what is supposed to "not work" about it? AR: To sum up. ETC is built with the older Hilbert-Tarski's method. CCAF as a whole involves a genuinely new idea of how to build mathematical theories , I agree with you on this point. But since ETC is indispensible in CCAF - and morever since ETC is a starting point of CCAF the new categorical axiomatic method in the context of CCAF does not work *independently* (I am not saying that it doesn't work at all.) This is why I say that CCAF is only a half-way to genuinely categorical foundations of mathematics (that is only natural in case of such a pioneering work as Bill's 1966's paper). For a possible development of CCAF into a better categorical foundation my hopes are for developing the diagrammatic reasoning of the second layer of CCAF into a genuine logico-mathematical synatax, which could serve independently of the usual first-order syntax. I'm particularly interested in this respect in recent work of Charles Wells, Zinovy Diskin, Dominique Duval, René Guitart and other people. Actually I would be quite interested to hear from these people what they think about a possible relevance of their work to foundations of mathematics and, more specifically, to CCAF. A more general point: in my understanding, a dialectical attitude to foundations amounts to looking at them as a subject of further rebuilding - rather than looking at them as what is accomplished in principle and needs only working out some further technical details. best, andrei [For admin and other information see: http://www.mta.ca/~cat-dist/ ]