From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/5292 Path: news.gmane.org!not-for-mail From: Andre.Rodin@ens.fr Newsgroups: gmane.science.mathematics.categories Subject: Re: categorical foundations Date: Wed, 18 Nov 2009 13:56:04 +0100 Message-ID: References: Reply-To: Andre.Rodin@ens.fr NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: ger.gmane.org 1258591475 3329 80.91.229.12 (19 Nov 2009 00:44:35 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Thu, 19 Nov 2009 00:44:35 +0000 (UTC) To: Colin McLarty , categories@mta.ca Original-X-From: categories@mta.ca Thu Nov 19 01:44:28 2009 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from mailserv.mta.ca ([138.73.1.1]) by lo.gmane.org with esmtp (Exim 4.50) id 1NAv8N-0000kb-Py for gsmc-categories@m.gmane.org; Thu, 19 Nov 2009 01:44:28 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1NAucX-00052c-Hb for categories-list@mta.ca; Wed, 18 Nov 2009 20:11:33 -0400 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:5292 Archived-At: Selon Colin McLarty : 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 gratef= ul 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 me= ans 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 thin= k earlier. It might have a bearing on what I'm saying but so far I cannot s= ee that it does. I am saying this: the axiomatic method in its modern form = - which has been pioneered by Hilbert (among other people including Dedikin= d, et al. ) and then further developed by Zermelo, Tarski et al.) - involves a preformal notion of set or collection. Whatever first-order theory is bui= lt 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 theor= y 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 a= bout axioms of ETC (or any other first-order theory) as assertive or as implic= it 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 ca= tegory is a collection of morphisms; at the second layer (i.e., in the core frag= ment 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 twof= old. (1) The second layer depends on the first but not the other way round. Fo= rmally speaking, this simply amounts to the fact that axioms of ETC are axioms o= f BT but not the other way round. In THIS sense, once again preformal sets rem= ain a foundation of CCAF. (2) The joint between the two layers remains for me unclear. From a forma= l viewpoint this looks trivial: CCAF is ETC plus some other axioms. But thi= s 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 approa= ch in the given setting (i.e. in CCAF) doesn't work *independently* of the olde= r approach; moreover there is a sense in which the older approach remains b= asic 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 - an= d morever since ETC is a starting point of CCAF the new categorical axioma= tic method in the context of CCAF does not work *independently* (I am not say= ing 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 m= y hopes are for developing the diagrammatic reasoning of the second layer of CCA= F 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 Wel= ls, Zinovy Diskin, Dominique Duval, Ren=E9 Guitart and other people. Actually= I would be quite interested to hear from these people what they think about a pos= sible relevance of their work to foundations of mathematics and, more specifica= lly, to CCAF. A more general point: in my understanding, a dialectical attitude to foun= dations amounts to looking at them as a subject of further rebuilding - rather th= an looking at them as what is accomplished in principle and needs only wor= king out some further technical details. best, andrei [For admin and other information see: http://www.mta.ca/~cat-dist/ ]