From rrosebru@mta.ca Thu Feb 1 14:24:28 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f11HdiO30959 for categories-list; Thu, 1 Feb 2001 13:39:44 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <3.0.5.32.20010201111006.00822860@TESLA.open.ac.uk> X-Sender: sjv22@TESLA.open.ac.uk X-Mailer: QUALCOMM Windows Eudora Light Version 3.0.5 (32) Date: Thu, 01 Feb 2001 11:10:06 +0000 To: categories From: S Vickers Subject: categories: RE: Why binary products are ordered In-Reply-To: <20010131135719.A5824@kamiak.eecs.wsu.edu> References: Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 1 [David Benson asked me: >This looks extremely useful... Where might I read more about this >formulation of limits? > >> The product of f: X -> M is then a universal solution to the problem of >> finding >> >> g: YxM -> X over M >> >> and this is equivalent to the usual characterization once you have chosen >> the isomorphism between M and 2. > Perhaps readers of the list can suggest sources I'd overlooked.] Dear David, The underlying idea is a very broad one, namely to look for limits of internal diagrams. You will find these described in Johnstone's "Topos Theory" and (I think - I haven't got it to hand) Mac Lane and Moerdijk. Suppose, working in a suitable category S (let's say a topos), you have an internal category C. Then you can define a notion of internal diagram over C (C-shaped diagram of S-objects) and they are the objects of an external category S^C, another topos. If D is another internal category in S and F: C -> D is a functor, then there is a functor F^*: S^D -> S^C defined using pullbacks in S and it has both right and left adjoints. In fact it defines an essential (if I remember the right word) geometric morphism from S^C to S^D. Now consider the situation when D is the terminal category, one object and one morphism. S^D is just S. The the right and left adjoints of F^* calculate internal limits and colimits of internal diagrams. This is easy to see, since F^*(X) is just the constant diagram, X everywhere, and a morphism (natural transformation) between an internal diagram D and F^*(X) is just a cone or cocone over D from or to X. The adjunctions then express exactly the universal properties of limits and colimits. I was describing situations where C was a discrete category, so the internal limit is an internal product. I also considered the question of whether the construction of the internal limit was geometric - preserved under inverse image functors of geometric morphisms. I have written about this kind of question in my own work, for instance "Topical Categories of Domains". (See my website, http://mcs.open.ac.uk/sjv22 .) Geometricity in general rules out the use of exponentiation in the topos, but exponentiation Y^X is geometric if X is finite with decidable equality (Johnstone and Wraith, ??"Algebraic theories in a topos"). My proposal is that the record type construction should be seen as a solution to the problem of internal products, but that it relies on finite decidability of the set of field names - hence it's related to geometricity of the internal product. In a different direction, note that internal products make sense in categories other than toposes, even if they don't always exist. For instance, if f: X -> Y is a continuous map of spaces, then the internal product, if it exists, is a space of continuous sections of f. I bet that's explored somewhere in the literature, but I don't know where. Best regards, Steve. From rrosebru@mta.ca Fri Feb 2 12:08:34 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f12FSRT21019 for categories-list; Fri, 2 Feb 2001 11:28:27 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: Todd Wilson MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-ID: <14969.60780.98559.298877@goedel.engr.csufresno.edu> Date: Thu, 1 Feb 2001 15:12:44 -0800 (PST) To: categories@mta.ca Subject: categories: CT vs ST thread X-Mailer: VM 6.75 under 21.1 (patch 3) "Acadia" XEmacs Lucid Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 2 I'd like to thank the contributors to what has turned out to be another Category Theory vs Set Theory thread -- Steve Vickers, Michael Barr, Colin McLarty, Charles Wells, Zinovy Diskin, and John Duskin -- especially Steve and Zinovy for their lengthy replies. My original post was, in a way, meant to be a step in the direction of ending such CT vs ST debates, but there still seems to be some interest in establishing "oppositions" between the two theories. Here is my attempt to frame the debate and to respond to some comments of the contributors in the process. I apologize for the length of this post. Zinovy Diskin observes that the debate involves "methodologically quite different problems whose merging under the same title CTvsST may be misleading", echoing the earlier statement by Bill Lawvere that "[s]o much confusion has been accumulated that an opposition of the form `set-theoretical versus non-set-theoretical' has at least seven wholly distinct meanings." I quite agree, and this was exactly the point of the end of my original post: And, finally, shouldn't "better" really be "better for what"? In other words, aren't the two communities really just arguing past one another, like people arguing over types of automobile? What really is the issue here? Colin McLarty has asked for clarification of these questions. My point was simply that it is pointless to claim that one theory or subject or approach is better than another without specifying what it is supposed to be better *for*. (Is a pick-up truck better than a 2-seater sports-car? Is a Mercedes Benz better than a BMW?) Here is a list of eight possible uses to which CT and ST may be put: 1. Offering an axiomatic foundation upon which all of mathematics may be developed, with a view towards a. establishing or making manifest its consistency b. providing a standard of rigor c. providing a common framework for the cooperation between different mathematical domains 2. Acting as a language in which certain mathematical ideas can be expressed, so that a. better use can be made of them (in applying them to specific instances, seeing connections between them, highlighting their more important features, etc.) b. they can be communicated more effectively to other mathematicians c. they better please our aesthetic sense 3. Providing models for specific phenomena (physical or computational), with a view towards a. informally illuminating their properties and connections b. predicting the outcomes of experiments involving them All of these uses are more or less concrete enough that comparisons between CT and ST could be undertaken empirically using these criteria (although some of them, for example 2a and 2c, are clearly more subjective than the others). My expectation is that CT and ST would each be "winners" on some non-trivial subset of the criteria. In addition to these eight uses for CT and ST, there is another important role that these theories play, namely, as formal theories of pre-mathematical concepts -- "collection" and "membership" in the case of ST, and "transformation" and "comparison" in the case of CT. From this point of view, I am left somewhat mystified by Lawvere's reference to the "totally arbitrary `singleton' operation of Peano with the resulting chains of mathematically spurious rigidified membership". Whatever its other "faults", ST seems to me to be a pretty accurate theory of "recursive collections" (or "classes" or "containers"), that is, collections of collections of .... Indeed, we can easily play with real containers of various sizes, and put them inside each other in various ways, and ST can be seen to be an accurate description of these configurations. The part of our conceptual apparatus that deals with container relations such as these is real and deserves to be modeled by a formal theory, and I find it hard to criticize ST on its appropriateness for this role. (Of course, ST is also about infinite collections, and its role there is more open to debate.) Continuing from this point of view, one feature of ST that I find especially interesting is that, although it is ostensibly a theory of "recursive collections", it nevertheless is quite successful, without any substantial additions, in many other roles -- see the list of eight uses above. It is an interesting philosophical and practical question to ask why this might be so, but one can hardly dispute this success. Thus, I also find it difficult to appreciate claims (such as Lawvere's) that set theory is "ill-suited for mathematics"; doesn't a simple comparison of the mathematical achievements before and after its "arithmetization" by set theory suggest otherwise? Turning to more specific topics, several respondents to my original post realized that my discussion of Cartesian products was a bit muddled, and that my suggestion of an "unordered product" was incoherent. Colin McLarty answered my question about the technical work involved in dealing with the a/the distinction by suggesting that "nothing is involved if we introduce a product operator". However, if we have a category with many non-trivial isomorphisms, then the task of introducing a product operator does involve something: making some arbitrary choices. Without getting into the details, I just wanted to ask whether such choices themselves added a kind of "spurious element" to the construction at least qualitatively similar to those in ST referred to by Lawvere. Steven Vickers nicely spelled out in more detail some of the ideas behind Lawvere's "cohesive and variable sets". However, I didn't mean to suggest in my post that I didn't appreciate the difference in approach (for example, I did my PhD thesis on frame theory, an algebraic underpinning for point-free topology). Rather, I fail to understand the point of criticizing ST for presenting a *particular* view of cohesion. Isn't it interesting that a surprisingly general and mathematically fruitful definition of cohesion/nearness among a set of points can be given in terms of just a single element of the double powerset of those points? The many achievements of "point-set" or "general" topology would suggest so. Now, I certainly agree that this view of cohesion may not be the best one for some, or even many, applications (which is what initially led to my interest in frame theory), but why does that have to turn into a criticism of the set-theoretic framework? We don't criticize the rectangular representation of complex numbers because we also have a polar representation. Vickers also makes the point that set-theoretic topology "does not generalize well to situations where you want to vary the set theory," and also mentions situations where it is fruitful to vary the underlying logic as well. These topics are among my favorites in all of mathematics, and I have been a proselytizer for these ideas in other forums, but the reaction of set theorists is understandable: varying the ST and logic makes it harder to relate what you are doing in the different "universes". A mathematician wanting to take advantage of a shift in ST and logic is faced with the problem of (re-)interpreting the results in the original framework. The extra overhead involved in moving between universes (not to mention the large "start-up costs" involved in learning the framework in the first place) is seldom ever justified by the advantages that ones gains, however real they can be. This is a very practical matter, involving mathematicians' choice of where to invest their time, and, again, I don't see what is to be gained by criticizing them for their choices. CONCLUSION: PLURALISM AND A CHALLENGE To sum up, I think that any debate on CT vs ST should take place in the context of a concrete and particular use of the two theories, where it is possible to investigate, more or less empirically, the advantages and disadvantages of each. In any other context, the debate reduces to a battle over personal preference, artistic sense, working habits, and other such subjective issues, and is unlikely to get anywhere. Second, I think we ought to foster a more pluralistic viewpoint. Each theory has its strengths and weaknesses, and we should choose the most appropriate tool for whatever job it at hand. If someone contends that there is a significant difference in appropriateness between two approaches, then, for this contention to be taken seriously, the difference has to be made clear and concrete for the "worker in the field". I would make the same point to computer scientists who are involved in the endless "Language Wars" over which programming language is the "best". And finally, I would like to offer a challenge (or challenges). For those mathematicians and computer scientists enamored with the vistas opened up by category theory, and topos theory in particular (and I count myself as among these), - Can we build computer-implemented formal systems that make it easier to navigate through several universes, work simultaneously with several logics, and help with re-interpretation when necessary? - Can we write books that help reduce the start-up costs involved in "outsiders" learning and using the framework? - Can we discuss in public places and in detail the importance of the topos-theoretic or category-theoretic outlook in obtaining our mathematical results? - And can we all the while hold off on our criticism of other approaches and instead let the results speak for themselves? -- Todd Wilson A smile is not an individual Computer Science Department product; it is a co-product. California State University, Fresno -- Thich Nhat Hanh From rrosebru@mta.ca Fri Feb 2 12:17:53 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f12FWVM26373 for categories-list; Fri, 2 Feb 2001 11:32:31 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <3A7A8AB4.43B2453@iml.univ-mrs.fr> Date: Fri, 02 Feb 2001 11:23:49 +0100 From: Paul RUET Organization: Institut de =?iso-8859-1?Q?Math=E9matiques?= de Luminy X-Mailer: Mozilla 4.51 [en] (X11; I; Linux 2.2.5-15 i686) X-Accept-Language: fr, it, en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Book on Linear Logic (deadline extension) Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 3 The submission deadline for the Book on Linear Logic is extended to March 1st, 2001. CALL FOR PAPERS Book on Linear Logic On the occasion of its International Summer School http://linear.di.fc.ul.pt/ held in the Azores from August 30 to September 7, 2000, the TMR Linear network http://iml.univ-mrs.fr/ldp/LINEAR/ wishes to edit a book devoted to recent advances in Linear Logic. This book will consist of a few invited papers and some refereed contributions (not necessarily written by people who gave a talk at the School). All submitted contributions will be refereed. They must be in English and may not exceed 25 pages, and the results must be unpublished and not submitted for publication elsewhere, including the proceedings of symposia or workshops. Submissions (in postscript format) must be sent by E-mail to linear-tmr-book@iml.univ-mrs.fr by March 1st, 2001. Suggested, but not exclusive, topics of interest for submissions include: * Proof theory: proof-nets, ludics, non-commutative logic, proof theory of classical logic. * Complexity: polynomial and elementary linear logics, decision problems, feasible arithmetics. * Semantics: phase semantics, categorical semantics, denotational semantics, game semantics, geometry of interaction. * Concurrency: categorical models for concurrency, interaction nets. * Applications: sharing reductions in lambda-calculus and optimality, linear functional programming linear constraint logic programming, proof search and focalisation. New submission deadline: March 1st, 2001. Tentative publisher: Cambridge University Press, in the "London Mathematical Society Lecture Note Series". Editorial board: Thomas Ehrhard Jean-Yves Girard Paul Ruet Phil Scott From rrosebru@mta.ca Fri Feb 2 12:25:56 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f12FVbm19769 for categories-list; Fri, 2 Feb 2001 11:31:37 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <034501c08ccf$21420e70$ad06df80@cs.uoregon.edu> From: "Luciano Baresi" To: categories2mta.ca Subject: categories: GT-VMT'01 Call for papers Date: Thu, 1 Feb 2001 20:17:58 -0800 MIME-Version: 1.0 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 4 Call for Papers Second International Workshop on Graph Transformation and Visual Modeling Techniques Crete, Greece, July 12 and 13, 2001 A Satellite Event of ICALP'2001 SCOPE AND OBJECTIVES OF THE WORKSHOP The growing success of visual modeling techniques in the design and development of complex applications is justified by many reasons. For example, the use of visual representations simplifies the communication both among developers and between developers and their customers; furthermore, visual techniques provide a high-level, yet precise language which allows to express and reason about concepts at their natural level of abstraction; finally, the availability of modern computational resources (like graphical workstations) provides easier access to tools supporting such techniques. However, despite the wide-spread usage of visual modeling techniques, compared to textual languages there is a lack of well-understood (and integrated) methodologies for defining their semantics. For example, there exists no equivalent approach to operational semantics in the SOS style, nor is there a general method for defining denotational semantics. The same applies to concepts like type systems, deductive proof methods, etc. for visual modeling techniques. On the other hand there are a number of individual approaches which exploit formalisms like Graph Transformation Systems, Process Algebra, Abstract State Machines, etc. to solve certain aspects of the overall problem. The workshop aims at bringing together scientists and researchers interested in discussing formal methodologies for the definition of syntax and semantics of visual modeling techniques. In particular contributions exploring the use of the theory of Graph Grammars and Graph Transformation Systems to this aim are welcome, as well as approaches based on other formalisms. Preferably, the contributions should be methodological in nature, rather than focusing on particular technical aspects. CALL FOR CONTRIBUTIONS Authors are invited to submit extended abstracts of up to 5 (five) A4 pages. The contributions should report about ongoing research in the area of graph transformation and visual modeling techniques, especially on the syntax and semantics of visual languages according to the scope and objectives of the workshop. Contributions exploring the use of Graph Grammars and Graph Transformation Systems are particularly welcome, as well as papers which cover several aspects or integrate different formalisms for the definition of visual modeling techniques. Position papers and contributions making methodological statements are strongly encouraged. Submissions should be sent preferably in postscript format to the address baresi@elet.polimi.it (Luciano Baresi) before the submission deadline. In the case electronic submission is not possible, three copies should be sent to the address: Luciano Baresi DEI - Politecnico di Milano Piazza L. da Vinci, 32. I-20133 - MILANO (Italy) IMPORTANT DATES Deadline for submissions: March 5, 2001 Notification of acceptance: April 5, 2001 Final version of accepted extended abstracts: May 2, 2001 PROGRAM COMMITTEE Luciano Baresi (Politecnico di Milano, Italy) [co-chair] Andrea Corradini (University of Pisa, Italy) Gregor Engels (University of Paderborn, Germany) Robert France (Colorado State University, USA) Reiko Heckel (University of Paderborn, Germany) Hans-Joerg Kreowski (University of Bremen, Germany) Francesco Parisi Presicce (Universit=E0 di Roma, Italy) Mauro Pezze' (Universita' di Milano, Bicocca, Italy)[co-chair] Gregor Rozenberg (Universiteit Leiden ,Netherlands) Gabriele Taentzer (TU Berlin, Germany) [co-chair] PROCEEDINGS The abstracts of the contributions accepted for presentation will be published in a volume collecting the contributions to all satellite workshops of ICALP 2001. The volume will be published by Carleton Scientific, and it will be distributed to all ICALP participants. On the basis of the number and quality of the submissions, the Program Committee will consider the possibility of inviting submissions for a special issue of an international journal dedicated to the workshop. INVITED SPEAKERS Hartmut Ehrig (TU Berlin, Germany) Mary Jean Harrold (Georgia Institute of Technology, USA) Andy Schorr (University of the German Federal Armed Forces,Germany) Alex Wolf (University of Colorado at Boulder, USA) FURTHER INFORMATION Please contact: Luciano Baresi DEI - Politecnico di Milano Piazza L. da Vinci, 32. I-20133 - MILANO (Italy) Fax: +39 02 2399 3411 E-mail: baresi@elet.polimi.it Mauro Pezze' DISCO - Universita' di Milano Bicocca Via Bicocca degli Arcimboldi 8 - I-20126 MILANO (Italy) Fax: +39 02 6448 7839 E-mail: pezze@disco.unimib.it Gabriele Taentzer Technical University of Berlin Computer Science Department (FB 13) Sekr. FR 6-1 Franklinstr. 28/29, D-10587 Berlin (Germany) Fax: +49 30 314 23516 Email: gabi@cs.tu-berlin.de From rrosebru@mta.ca Fri Feb 2 15:21:41 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f12ISMX16255 for categories-list; Fri, 2 Feb 2001 14:28:22 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <3.0.6.16.20010202130511.1a27a38a@pop.cwru.edu> X-Sender: cxm7@pop.cwru.edu X-Mailer: QUALCOMM Windows Eudora Light Version 3.0.6 (16) Date: Fri, 02 Feb 2001 13:05:11 To: categories@mta.ca From: Colin McLarty Subject: categories: Re: CT vs ST thread In-Reply-To: <14969.60780.98559.298877@goedel.engr.csufresno.edu> Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 5 Todd Wilson suggested there are many different issues in contrasting CT to ST. He admits he was partly "mystified" by Lawvere's earlier post, which said the same thing and actually advanced the discussion by specifically laying out several different threads. And when I asked Wilson which issues he wanted to discuss he mistook my meaning, and thought I was asking him to explain how there are different issues. This kind of repeatedly starting from scratch is not helpful, though it is regrettably common in the "debate" over ST and CT. Finally though, he gets to some specifics. > Here is a list of eight possible uses to which CT and ST may be put: > >1. Offering an axiomatic foundation upon which all of mathematics may > be developed, with a view towards > > a. establishing or making manifest its consistency > b. providing a standard of rigor > c. providing a common framework for the cooperation between > different mathematical domains Work going back to Osius and Mitchell and others in the 1970s shows that CT can accomplish 1a and 1b in pretty much the same way that ST does, if you want to do it that way. Perhaps the best comprehensive citation now is to Johnstone TOPOS THEORY and its chapter on topos theory and set theory. See also Mac Lane and Moerdijk SHEAVES IN GEOMETRY AND LOGIC and their chapter on topoi and logic. Simpson on the FOM list likes to call this "slavish imitation" of set theory, thus agreeing that CT can do what ST does. It can also accomplish 1a and 1b in its own terms, if you like that. 1c is definitively answered in mathematical practice. Category theory has been the leading common framework for linking domains for half a century. ST is not a candidate on any practical level. >2. Acting as a language in which certain mathematical ideas can be > expressed, so that > > a. better use can be made of them (in applying them to specific > instances, seeing connections between them, highlighting their > more important features, etc.) > b. they can be communicated more effectively to other > mathematicians > c. they better please our aesthetic sense Again, in practice, category theory is the leading framework for 2a and 2b. No one proposes using ZF on that level. As to 2c, anyone may vote as they please. I make no citations on these because they are perfectly obvious. If any result can "speak for itself" surely the categorical methods in topology, geometry, analysis, and arithmetic, can for themselves. >3. Providing models for specific phenomena (physical or > computational), with a view towards > > a. informally illuminating their properties and connections > b. predicting the outcomes of experiments involving them As to physical phenomena, the principled foundations of math don't seem to bear very directly on them as practiced today. Who could seriously argue that Hawking's or Witten's work is "actually" founded on ZF versus the category of sets? On the level of methods, people do propose categorical methods for quantum gravity, quantum groups, and so on. I don't believe anyone is seriously exploring ZF for the same role. People who believe practice would advance better, if foundations were brought closer to practice so that the whole structure of math was more harmonious, will probably favor category theory. Computational phenomena bring us back to the issue that started the thread. Here I think serious discussion is warrented because there is a lot to know. I'm no computer expert but I will reply to: >Turning to more specific topics, several respondents to my original >post realized that my discussion of Cartesian products was a bit >muddled, and that my suggestion of an "unordered product" was >incoherent. Colin McLarty answered my question about the technical >work involved in dealing with the a/the distinction by suggesting that >"nothing is involved if we introduce a product operator". However, if >we have a category with many non-trivial isomorphisms, then the task >of introducing a product operator does involve something: making some >arbitrary choices. No. Look at it this way: If I say in a computer program "x=0" am I making an "arbitrary choice" of how to represent 0 by a set? We know that in CT or ST there are alternative representations of 0. But the computer does not occupy itself with those. It has its internal representation of 0 as a data value (perhaps several) and uses that (or, one of them). Similarly, suppose I have a product operator. That is actually, one binary operator on objects _x_ with object values, and two binary operators on objects p0_,_ and p1_,_ with arrow values. When implementing these I give the machine a way of internally representing these as data values, and the machine uses those representations. Of course, in implementing the categorical product, as in implementing integer arithmetic or anything else, the programmer makes many more or less "arbitrary" choices of details of how the machine will handle them. That has nothing to do with non-identity isomorphisms, and nothing to do with ST versus CT. In principle, or for foundations, the issue here is the difference between choices and operators. There is a huge logical literature on it and it is uncontroversial. best, Colin From rrosebru@mta.ca Sun Feb 4 11:24:57 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f14ESZn31869 for categories-list; Sun, 4 Feb 2001 10:28:35 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Fri, 2 Feb 2001 16:18:48 GMT From: Mark D Ryan Message-Id: <200102021618.QAA17670@gromit.cs.bham.ac.uk> To: categories@mta.ca Subject: categories: job: Research job in model checking application Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 6 Job opportunity * Model checking * flexible balance of theory/applications, to suit applicant * good research environment * ability more important than relevant experience * informal enquiries welcome THE UNIVERSITY OF BIRMINGHAM SCHOOL OF COMPUTER SCIENCE Postdoctoral Research Fellow Applications are invited for a Postdoctoral Research Fellow to work on the project `The Feature Construct in Programming and Specification Languages', funded by EPSRC and British Telecom, coordinated by Dr. Mark Ryan and Dr. Marta Kwiatkowska. Applicants should have a PhD in Computer Science and ideally have knowledge of one or more of the following areas: model checking, temporal logic, and/or program semantics. The successful applicant may be expected to contribute to teaching in the School up to a maximum of two hours per week on average. More information about the project, the research group and the School can be obtained from the URLs: www.cs.bham.ac.uk/~mdr/fc www.cs.bham.ac.uk The starting salary will be up to 19,482 pounds per year. The post is for three years from 1 April 2001 or as soon as possible thereafter. Application forms and further particulars available from: The Director of Personnel Services The University of Birmingham Edgbaston, Birmingham, B15 2TT tel: + 44 (0)121 414 6486 (24 hours) email: h.h.luong@bham.ac.uk Application forms are available from the WWW, at www.bham.ac.uk/personnel/app.htm Please quote reference S35522/01. The closing date for applications is Friday 9th March 2001. Late applications will be considered if the selection process has not advanced too far. Informal enquiries are welcome, and should be addressed to: Mark Ryan, tel: +44 (0)121 414 7361, email: M.D.Ryan@cs.bham.ac.uk. The University of Birmingham is working towards equal opportunities. From rrosebru@mta.ca Sun Feb 4 18:59:30 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f14MH6S16280 for categories-list; Sun, 4 Feb 2001 18:17:06 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Sun, 4 Feb 2001 15:25:01 -0500 (EST) From: Oswald Wyler X-Sender: owyler@localhost To: categories@mta.ca Subject: categories: Complete atomic Boolean algebra: Reference? Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 7 Every reader of this post probably knows that the algebras for the monad on sets induced by the self-adjoint contravariant powerset functor are the complete atomic Boolean algebras, with maps preserving all infima and all suprema as morphisms. I know how to prove this without much trouble, but I have not been able to find a proof of this fact, or even a good reference to such a proof, in the literature available to me at my present location (which is essentially what I have at home). If you know such a reference, please e-mail it to me at owyler@nqi.net. Related question. The functor on sets which assigns to every set X the set of increasing subsets of PX is the functor part of a monad, with completely distributive complete lattices as algebras. Again, I have a proof but no references. From rrosebru@mta.ca Mon Feb 5 10:55:25 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f15EKhD25912 for categories-list; Mon, 5 Feb 2001 10:20:44 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <3A7DE6D8.62497273@sun.iwu.edu> Date: Sun, 04 Feb 2001 17:33:44 -0600 From: Larry Stout X-Mailer: Mozilla 4.75 [en] (X11; U; Linux 2.2.16-22 i686) X-Accept-Language: en MIME-Version: 1.0 To: Categories List Subject: categories: Some infinitesimal analysis questions Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 8 I am teaching a course out of Bell's book "A Primer of Infinitesimal Analysis" to senior mathmajors at my liberal arts college. It is making a nice capstone, since it lets them look at the material they started college with (claculus) from a completely different viewpoint (that of synthetic differential geometry). It also lets me teach some of a topos theoretic view on mathematics. I am left with some questions in my own mind about what one can and cannot do in a smoth world. Specifically, 1. The usual inverse function theorem uses monotonicity to guarantee the existence of an inverse function, a monotonicity obtained from the mean value theorem. It seems unlikely to me that the mean value theorem holds in synthetic differential geometry, so how does one guarantee the existence of an inverse for a function with strictly positive derivative? 2. In a smooth world must the image of a closed interval be a closed interval? Can one characterize closed intervals without knowing what their endpoints are purported to be? (Since closed intervals are microstable you can't actually know those endpoints uniquely). 3. How do you justify the leap from stationary points to maxima and minima? Have any of the other readers of this list tried teaching a course out of this book? -- Lawrence Neff Stout Professor of Mathematics Illinois Wesleyan University http://www.iwu.edu/~lstout "Fiddling is a viol habit." Anon? "Dancing is necessary in a well ordered society." Thoinot Arbeau From rrosebru@mta.ca Mon Feb 5 11:00:26 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f15ELhf19775 for categories-list; Mon, 5 Feb 2001 10:21:43 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <200102051312.AA13037@menthe.ens.fr> Content-Type: text/plain Mime-Version: 1.0 (NeXT Mail 4.2mach_patches v148.2) From: Giuseppe Longo Date: Mon, 5 Feb 2001 14:12:31 +0100 To: categories@mta.ca Subject: categories: ST vs CT Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 9 The key issues raised by Bill Lawvere may be further specified if we try to make explicit the different "philosophical projects" which underlie the Set Theory vs Category Theory debate. ST is "newtonian": it proposes a fixed-absolute universe (ZF or alike) where all of present (and future!) mathematics should be embedded (described). Its perspective is (basically) "laplacian": given the (current) axioms of set-theory (or arithmetic) we can prove/decide/predict all future states of affairs (theorems of mathematics). CT originates from a rather different perspective. Riemann first proposed to found mathematics (geometry) on key regularities of the world to be turned into conceptual invariants, as "hypothesis" about the structure of physical space (connectivity, continuity, isotropy ... ; H. Weyl added symmetries to this). Then, one had to single out the "invariant preserving transformations" (Kleine, Clifford, Poincare' ...). The objects, as structural invariants, and the morphisms of CT, as transformations (including isomorphisms ...; functors; natural transformations ...), came out directly from this tradition; that is, CT followed the riemannian project who had replaced the absolute axioms/universe of euclidean geometry by the "relativizable" notions of invariant and transformation (as founding manifolds). In CT, the unity of mathematics, not as an absolute pre-fixed universe, but as an open world of ongoing new concepts and structures, is constantly re-constructed, by (interpretation) functors, which relate new categories to old ones (moreover, natural transformations (adjunctions ...) help to correlate these functors). Clearly, Newton and Laplace were immense scientific personalities, but ..., since then, many things have happened. In Physics, of course, but also within ... ST or in the proof-theory of Arithmetic, such as the independence theorems or the remarquable results on the "unremovability of machinery", which, even if within ST, force us outside the "rational mechanics" of PA .... More on this may be found in a two pages note of mine on "Laplace (vs Hilbert)" (or, reflections on rational mechanics and incompleteness), an item inserted in the Dictionary at the end of JY Girard's paper "Locus Solum" (MSCS, n. 11.3, to appear) and in a paper on "The reasonable effectiveness of Mathematics ..." (both downloadable from my web page). Giuseppe Longo Lab. et Dept. d'Informatique CNRS et Ecole Normale Superieure (Postal addr.: LIENS 45, Rue D'Ulm 75005 Paris (France) ) http://www.dmi.ens.fr/users/longo et : CENtre d'Etude des systemes Complexes et de la Cognition de l'ENS (CENECC) http://www.cenecc.ens.fr/ e-mail: longo@dmi.ens.fr (tel. ++33-1-4432-3328; fax -2151) From rrosebru@mta.ca Mon Feb 5 11:10:12 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f15ELJ301616 for categories-list; Mon, 5 Feb 2001 10:21:19 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Mon, 5 Feb 2001 12:29:23 +0100 (MET) From: Message-Id: <200102051129.MAA23214@kodder.math.uu.nl> To: categories@mta.ca Subject: categories: Re: Complete atomic Boolean algebra: Reference? X-Sun-Charset: US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 10 This is of course folklore. I believe there is a proof (essentially) in Johnstone's Stone Spaces. I have written out a proof for students in chapter 1 of my "Basic Category Theory" notes; see http://www.math.uu.nl/people/jvoosten/onderwijs.html Jaap van Oosten From rrosebru@mta.ca Mon Feb 5 22:32:21 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f161hHP23726 for categories-list; Mon, 5 Feb 2001 21:43:17 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <3A7EFDEC.72B06928@kestrel.edu> Date: Mon, 05 Feb 2001 11:24:28 -0800 From: Dusko Pavlovic X-Mailer: Mozilla 4.5 [en] (Win98; U) X-Accept-Language: en,nl MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Re: Complete atomic Boolean algebra: Reference? References: <200102051129.MAA23214@kodder.math.uu.nl> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 11 isn't the correspondence of sets and caBa the "discrete part" of the stone duality? the other monad prof wyler mentions appears, i think, in e. manes' thesis, and in his 1976 book "algebraic theories", perhaps as a step towards deriving the monad for compact hausdorff spaces. all the best, -- dusko pavlovic jvoosten@math.uu.nl wrote: > This is of course folklore. I believe > there is a proof (essentially) in > Johnstone's Stone Spaces. > > I have written out a proof for students in > chapter 1 of my "Basic Category Theory" > notes; see > > http://www.math.uu.nl/people/jvoosten/onderwijs.html > > Jaap van Oosten From rrosebru@mta.ca Tue Feb 6 10:19:28 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f16DWAW19851 for categories-list; Tue, 6 Feb 2001 09:32:10 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Tue, 6 Feb 2001 08:21:29 -0500 (EST) From: Marta BUNGE To: categories@mta.ca Subject: categories: Re: complete atomic Boolean algebras Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 12 For an "upgraded" version of the correspondence see the newly appeared M.Bunge, J. Funk, M. Jibladze, T. Streicher "Distribution Algebras and Duality" Advances in Mathematics 156, 133-155 (2000) This is done for a bounded topos E--->S, replacing S = Coc_S(S,S) by Dist(E) = Coc_S(E,S) and caBA(S) by "distribution algebras". Identifying E with S gives the correspondence in question. For just that one, it may be worthwhile to consult directly Mikkelsen's thesis combined with Pare's Theorem. Marta Bunge From rrosebru@mta.ca Tue Feb 6 10:27:46 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f16DUPX23611 for categories-list; Tue, 6 Feb 2001 09:30:25 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <3A7F3792.5D0A3D7D@yorku.ca> Date: Mon, 05 Feb 2001 18:30:41 -0500 From: jwpell X-Mailer: Mozilla 4.7 (Macintosh; U; PPC) X-Accept-Language: en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: preprint: Quantisation of Spaces Content-Type: text/plain; charset=us-ascii; x-mac-type="54455854"; x-mac-creator="4D4F5353" Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 13 We wish to announce the availability of our new paper, "On the Quantisation of Spaces," which has been submitted to the JPAA volume in honour of the 70th birthday of Max Kelly. It can be accessed in either pdf or ps format as follows: http://www.maths.sussex.ac.uk/Staff/CJM/research/pdf/quanspce.pdf http://www.maths.sussex.ac.uk/Staff/CJM/research/ps/quanspce.ps The paper applies the concept of point introduced in our previous paper, "On the Quantisation of Points," http://www.maths.sussex.ac.uk/Staff/CJM/research/pdf/quanpts.pdf http://www.maths.sussex.ac.uk/Staff/CJM/research/ps/quanpts.ps to establish a concept of space within the context of involutive unital quantales. C. J. Mulvey J Wick Pelletier -- Dr. Joan Wick Pelletier Department of Mathematics and Statistics York University From rrosebru@mta.ca Wed Feb 7 12:01:44 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f17F3PX28334 for categories-list; Wed, 7 Feb 2001 11:03:25 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Wed, 7 Feb 2001 11:07:56 +0100 (CET) From: Tobias Schroeder X-Sender: tschroed@pc12394 To: Category Mailing List Subject: categories: field and Galois theory Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from QUOTED-PRINTABLE to 8bit by mailserv.mta.ca id f17A7wg10232 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 14 Hello, all introductions to field and Galois theory I've found are written in a "classical" way, i.e. making not much use of categorical notions. A lot of computation is done where someone who is "categorical minded" has the feeling that the results could be established in a more comprehensible and clear way by category theory. -- Does somebody have a reference to a short and good introduction to field and Galois theory from a categorical viewpoint? Thanks Tobias Schroeder -------------------------------------------------------------- Tobias Schröder FB Mathematik und Informatik Philipps-Universität Marburg WWW: http://www.mathematik.uni-marburg.de/~tschroed email: tschroed@mathematik.uni-marburg.de From rrosebru@mta.ca Wed Feb 7 15:17:17 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f17ITWQ30701 for categories-list; Wed, 7 Feb 2001 14:29:32 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Authentication-Warning: muppet44.cs.chalmers.se: reiner owned process doing -bs Date: Wed, 7 Feb 2001 17:07:30 +0100 (MET) From: Reiner Haehnle To: Subject: categories: New PhD Positions in Computing Science, Gothenburg, Sweden Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 15 Please pass on to interested students. Apologies for multiple copies. --------------------------------------------------------------------- New PhD Positions (DEADLINE 1 March 2001! See "How to apply" below.) Department of Computing Science, Chalmers University of Technology & University of Gothenburg Sweden The Department has about 70 researchers, half being faculty members and half PhD students. Our focus is on programming logic, type theory, functional programming, formal methods, distributed and concurrent systems, security, algorithms, bioinformatics, human computer interaction, and computational linguistics, but research is not restricted to these topics. For more information, see http://www.cs.chalmers.se/Cs/Research. PhD positions are for 5 years. There is no tuition fee. A PhD position is a regular job with social benefits; the salary amounts currently to about 16700 SEK per month in the first year (the exact amount depends on teaching duties, usually 20% of your time). Knowledge of Swedish is not a prerequisite for application. English is our working language for research. Both Swedish and English are used in undergraduate courses. Half of our researchers and PhD students are native Swedes; the rest come from more than 20 different countries. Applicants must have a very good undergraduate degree in Computing Science or in a related subject with a strong Computing Science component. They must also have a strong interest in doing research. You may also apply if you have not yet completed your degree, but expect to do so by September 2001. You are also invited to apply for our new International Master's Programme in Dependable Computer Systems, which can help you to obtain the necessary qualification (see http://www.cs.chalmers.se/Cs/Education/dcs/) The School especially welcomes female applicants. How to apply ------------ First, immediately register your intention to apply using the electronic application form on the WWW via http://www.md.chalmers.se/Jobs/PhD/phd-01-en.thtml The full application should contain 1 A letter of application, listing specific research interests 2 A curriculum vitae 3 Attested copies of degrees and other certificates 4 Copies of relevant work, for example dissertations or articles, that you have authored or co-authored 5 A description of: a previous teaching experience, documented, if any b previous PhD studies, also in other subjects. State financial support for these, if any c previous work experience 6 Letters of recommendation from your teachers or employers If you have financial support of your own (industry job, grant, etc.), please state this fact clearly. It will increase your chances to be accepted considerably, because you need not compete for the limited number of fully financed positions. Send your application (paper mail) to Section for Mathematics and Computer Science Chalmers University of Technology 412 96 Gothenburg Sweden to arrive by 1 March 2000. You will know the result of your application by 1 May 2000. From rrosebru@mta.ca Thu Feb 8 09:55:59 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f18DIxX08319 for categories-list; Thu, 8 Feb 2001 09:18:59 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <200102080117.RAA13130@coraki.Stanford.EDU> To: categories@mta.ca Subject: categories: Re: Why binary products are ordered In-reply-to: Your message of "Mon, 29 Jan 2001 10:18:52 PST." <4.1.20010129101330.00ad8560@mail.oberlin.net> Date: Wed, 07 Feb 2001 17:17:19 -0800 From: Vaughan Pratt Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 16 (Just back from Australia, where I was able to combine my mum's 90th birthday with the annual Australian Computer Society meeting which by pure luck turned out to be only a 20 minute drive away, in the process running into Bob Walters and Mike Johnson as well as some other friends I hadn't seen for ages. The following arrived right on Mum's birthday.) >From: Charles Wells > >One might say that the ordering of binary products, with a first projection >and a second projection, is spurious but inevitable. > >The two components of a binary product must be distinguished, as Colin >McLarty explained, but they must be allowed to be isomorphic. The usual >way we handle a situation like this in mathematics is to index them, in >this case by a two-element set. One could use {red,blue}. As far as I >know, in Western culture, this set has no canonical ordering, but >nevertheless one knows that there is a redth component and a blueth >component and they might or might not be different objects. > >However, in practice the index set is {0,1}, {1,2} or {x,y} (the latter in >analytic geometry). All of these are canonically totally ordered in our >culture, so inevitably binary products do have an order in practice. I confess to some confusion as to what Charles is insisting is inevitable here. A binary product in C is a limit of a diagram 1+1->C (1+1 the two-object discrete category), and 1+1 has two automorphisms. This much and its mathematical consequences are surely inevitable. But woven into Charles' argument is what Bill has called the "totally arbitrary singleton operation of Peano." It appears implicitly at the beginning when Charles names the projections, and then (after an indirect reference to the automorphisms of the binary product) more explicitly when he collects the names as a set. Surely anyone insisting on names like 1 and 2 or red and blue for the projections of binary product is backsliding into the ZFvN tarpit of spurious rigidified membership. If this backsliding really is inevitable as Charles seems to be saying, how does one reconcile this with Bill's view of "rigidified membership" as "mathematically spurious"? Must mathematics accept the spurious, in this or any other case? Vaughan From rrosebru@mta.ca Fri Feb 9 15:18:16 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f19IdwF30454 for categories-list; Fri, 9 Feb 2001 14:39:58 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <200102091836.TAA07095@irmast2.u-strasbg.fr> Date: Fri, 9 Feb 2001 19:36:33 +0100 (MET) From: Philippe Gaucher Reply-To: Philippe Gaucher Subject: categories: technical question about omega-categories To: categories@mta.ca MIME-Version: 1.0 Content-Type: TEXT/plain; charset=us-ascii Content-MD5: shbGAGcLjrmlBTk82w0Syw== X-Mailer: dtmail 1.3.0 @(#)CDE Version 1.3.5 SunOS 5.7 sun4u sparc Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 17 Dear all, Let C be an omega-category (strict, globular). Let U be the forgetful functor from strict globular omega-categories to globular sets. And let F be its left adjoint. Let us suppose that we are considering an equivalence relation R on UC (the underlying globular set of C) such that the source and target maps pass to the quotient : i.e. one can deal with the quotient globular set UC/R. The canonical morphism of globular sets UC --> UC/R induces a morphism of omega-categories F(UC) --> F(UC/R) by functoriality of F. Consider the following push-out in the category of omega-categories : F(UC) -----> F(UC/R) | | | | | | v v C ---------> D The morphism F(UC)-->C (the counit of the adjonction) is surjective on the underlying sets. The morphism F(UC)-->F(UC/R) is generally not surjective on the underlying sets : because by taking the quotient by R, one may add composites in F(UC/R) which do not exist in F(UC). However the intuition tells (me) that the morphism F(UC/R)-->D is surjective on the underlying sets : this morphism only adds in F(UC/R) the calculation rules of C : this is precisely what I want by introducing D. But I cannot see why with a rigorous mathematical argument. Thanks in advance. pg. From rrosebru@mta.ca Fri Feb 9 15:18:24 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f19Id7O30380 for categories-list; Fri, 9 Feb 2001 14:39:07 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Fri, 9 Feb 2001 11:02:52 +0000 (GMT) From: Marco Mackaay To: categories@mta.ca Subject: categories: reference: normal categorical subgroup? Message-ID: MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 18 To all category theorists, I'm looking for a reference to the definition of a normal categorical subgroup, i.e. the right kind of subgroupoid of a categorical group for taking the quotient. I know the definition, but I have no reference. Does anyone know a published origin of the definition? Best wishes, Marco Mackaay From rrosebru@mta.ca Fri Feb 9 15:20:20 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f19Iac129963 for categories-list; Fri, 9 Feb 2001 14:36:38 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Authentication-Warning: triples.math.mcgill.ca: barr owned process doing -bs Date: Thu, 8 Feb 2001 12:44:59 -0500 (EST) From: Michael Barr X-Sender: barr@triples.math.mcgill.ca To: categories@mta.ca Subject: categories: Re: Why binary products are ordered In-Reply-To: <200102080117.RAA13130@coraki.Stanford.EDU> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 19 As I said in an earlier post, the whole thing is a figment of the linear way we write (and speak, for that matter). Products are over unordered sets and any ordering is purely irrelevant. On Wed, 7 Feb 2001, Vaughan Pratt wrote: ... > I confess to some confusion as to what Charles is insisting is inevitable > here. A binary product in C is a limit of a diagram 1+1->C (1+1 the > two-object discrete category), and 1+1 has two automorphisms. This much > and its mathematical consequences are surely inevitable. > > But woven into Charles' argument is what Bill has called the "totally > arbitrary singleton operation of Peano." It appears implicitly at the > beginning when Charles names the projections, and then (after an indirect > reference to the automorphisms of the binary product) more explicitly > when he collects the names as a set. > > Surely anyone insisting on names like 1 and 2 or red and blue for the > projections of binary product is backsliding into the ZFvN tarpit of > spurious rigidified membership. If this backsliding really is inevitable > as Charles seems to be saying, how does one reconcile this with Bill's > view of "rigidified membership" as "mathematically spurious"? > > Must mathematics accept the spurious, in this or any other case? > > Vaughan > From rrosebru@mta.ca Fri Feb 9 15:29:26 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f19Ic7v30442 for categories-list; Fri, 9 Feb 2001 14:38:07 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <3.0.5.32.20010209120209.00925c10@mail.math.ucl.ac.be> X-Sender: borceux@mail.math.ucl.ac.be X-Mailer: QUALCOMM Windows Eudora Light Version 3.0.5 (32) Date: Fri, 09 Feb 2001 12:02:09 +0100 To: categories@mta.ca From: BORCEUX Francis Subject: categories: Re: field and Galois theory Mime-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by mailserv.mta.ca id f19B1tH13832 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 20 As possible answer to the following message of Tobias Schroeder to this list >all introductions to field and Galois theory I've found are written in a >"classical" way, i.e. making not much use of categorical notions. A lot of >computation is done where someone who is "categorical minded" has the >feeling that the results could be established in a more comprehensible and >clear way by category theory. -- Does somebody have a reference to a short >and good introduction to field and Galois theory from a categorical >viewpoint? let me mention the book Galois theories Francis Borceux & George Janelidze Cambridge Studies in Advanced Mathematics, volume 72 Cambridge University Press (2001), 341 pages ISBN 0 521 80309 8 which will be available from February 20. This is probably not an as "short" introduction as Tobias wants ... and I let you decide if it is a "good" one. References at the end of the book, in particular to various papers of George Janelidze on a categorical approach of Galois theory, will provide alternative answers to Tobias'question. Here is the table of contents of the book. 1. Classical Galois theory 2. Galois theory of Grothendieck 3. Infinitary Galois theory 4. Categorical Galois theory of commutative rings 5. Categorical Galois theorem and factorization systems 6. Covering maps 7. Non-galoisian Galois theory For further information, contact WWW: http://www.cambridge.org Francis Borceux %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Francis Borceux doyen de la faculté des Sciences, Université Catholique de Louvain 2 place des Sciences, 1348 Louvain-la-neuve (Belgique) tél. 32 10 473170 fax 32 10 472837 secrétaire 32 10 478679 From rrosebru@mta.ca Sat Feb 10 17:21:23 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1AKeIS07453 for categories-list; Sat, 10 Feb 2001 16:40:18 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <3.0.6.16.20010208101428.44872230@pop.cwru.edu> X-Sender: cxm7@pop.cwru.edu X-Mailer: QUALCOMM Windows Eudora Light Version 3.0.6 (16) Date: Thu, 08 Feb 2001 10:14:28 To: categories@mta.ca From: Colin McLarty Subject: categories: Re: Why binary products are ordered In-Reply-To: <200102080117.RAA13130@coraki.Stanford.EDU> References: Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 21 Charles Wells and Steve Vickers both made the point that, for example, in a record of type (height in inches age, in years) you have to be able to identify the height entry, and the age entry, but you do not have to identify either one as the "first" entry or the "second". Yet, as Charles points out, the usual ways of identifying the two entries all carry a culturally-canonical ordering--as we say "one, two" usually in that order and "left, right" most often in that order. As he puts it: >>However, in practice the index set is {0,1}, {1,2} or {x,y} (the latter in >>analytic geometry). All of these are canonically totally ordered in our >>culture, so inevitably binary products do have an order in practice. Then Vaughan Pratt weighs in, in his rhinocerean way. (For those who do not read FOM, or at least Ionesco, Vaughan had a terrific post on FOM about categorists as kind of rhinoceros, and by the end he began transforming into one.) >But woven into Charles' argument is what Bill has called the "totally >arbitrary singleton operation of Peano." It appears implicitly at the >beginning when Charles names the projections, and then (after an indirect >reference to the automorphisms of the binary product) more explicitly >when he collects the names as a set. > >Surely anyone insisting on names like 1 and 2 or red and blue for the >projections of binary product is backsliding into the ZFvN tarpit of >spurious rigidified membership. If this backsliding really is inevitable >as Charles seems to be saying, how does one reconcile this with Bill's >view of "rigidified membership" as "mathematically spurious"? I think Charles is not tarred by this pit. The Peano/ZFvN idea is to say that, given 0 and 1, and some one among all the two-element sets is actually the set {0,1}. Charles is merely saying that when we pick a two element set, and name its elements, we tend to use names with specific (helpful or spurious) connotations. The naming here is "local", a choice of how to talk about two objects we assme we have. It involves no idea that the two element set has any objective features making it the set of 0 and 1. best, Colin From rrosebru@mta.ca Sat Feb 10 17:21:35 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1AKckU06779 for categories-list; Sat, 10 Feb 2001 16:38:46 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Thu, 8 Feb 2001 08:29:53 -0500 (EST) From: Peter Freyd Message-Id: <200102081329.f18DTrG10893@saul.cis.upenn.edu> To: categories@mta.ca Subject: categories: Robin Milner Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 22 Copyright 2001 TSL Education Limited The Times Higher Education Supplement February 2, 2001 SECTION: COMPUTING; BOOKS; No.1472; Pg.26 LENGTH: 1616 words HEADLINE: Honouring The Master Of Logical Languages BYLINE: Jonathan Bowen BODY: Proof, Language and Interaction Edited by Gordon Plotkin, Colin Stirling and Mads Tofte MIT Press, 722pp, Pounds 48.50 ISBN 0 262 16188 5 THES Bookshop Pounds 44.50 Tel: 020 8324 5104 This Festschrift, or celebratory publication, honours an important contributor to the fundamentals of computer science. Robin Milner, to whom this volume is dedicated, has been a cornerstone of the theoretical computer science world for the past three decades or so. The book begins with an enlightening biography of Milner's professional achievements that helps set the context for the rest of the book. As is usual in a Festschrift, the volume mainly consists of contributions from Milner's immediate colleagues and those working in the same field on related topics. All the contributions are of international stature and are largely technical in nature. Thus, this book provides an important in-depth snapshot of the work of some of the best minds in the area of theoretical computer science. Milner had an excellent education. He won a scholarship to King's College, Cambridge, in 1952 - the same college where Alan Turing had won a similar scholarship about 20 years earlier. He studied mathematics, the underpinning of computer science, and, for a while, Cambridge's "moral sciences", or philosophy in normal parlance. The early professional experiences of Milner were as a schoolteacher and as a programmer at Ferranti, both useful grounding for a computer science academic. He then worked at City University in London, Swansea University, Stanford University in California and, from 1973, at Edinburgh University, where his most important work was undertaken. In 1995 he moved back to Cambridge, where he now heads the Computer Laboratory. He has received the highest awards, including a fellowship of the Royal Society in 1988 and the annual ACM Turing Award in 1991, computer science's nearest equivalent to a Nobel prize. Milner's contributions to theoretical computer science have been in the areas of programming language semantics using domain theory, computer-assisted theorem proving, the programming language ML (standing for "Metalanguage") and, perhaps most significantly, concurrency. His early influences included Christopher Strachey (leader of the Programming Research Group at Oxford and originator of denotational semantics), Rod Burstall (also at Edinburgh), Peter Landin (a free-spirit pioneer of computing), Dana Scott (who worked with Strachey at Oxford on the foundations of programming languages) and John McCarthy (of artificial intelligence fame at Stanford, who coined the term AI). At Stanford, Milner developed the Stanford LCF (logic of computable functions) while working within McCarthy's AI group, based on a logic developed by Scott using a typed l-calculus (the essential underlying theoretical basis for the functional programming paradigm). This subsequently developed into Edinburgh LCF, with its own programming language Edinburgh ML that was designed to aid in the discovery and construction of proofs, an inspired idea for the time. This became Standard ML that, because of its carefully designed and well- understood formal semantics, has proved to be an excellent, more general programming language. If the above efforts are not enough, probably Milner's most important contribution concerns the formal underpinning for concurrency, starting with his calculus of communicating systems (CCS). This introduced the notion of bisimulation for comparing the equivalence of processes. Although an influential concept, some researchers have considered bisimulation too restrictive in practice (for example, in strong bisimulation, both processes must execute the same number of steps) and Milner himself proposed a more forgiving weak bisimulation. CCS has always been somewhat in competition with Tony Hoare's communicating sequential processes (CSP) in terms of influencing the field, with the usual camps of researchers expert in each. However, more recently Milner has developed his ideas further with a newer p-calculus for mobile computing that is increasingly important in practical terms with the development of the internet. Milner remains active in this area. Milner's influence on his field is significant, as the contributions in this book attest. Many subsequent theorem provers produced by other researchers have been inspired by Milner's original LCF, including the development of Cambridge LCF, and the related HOL (higher order logic) by Mike Gordon, as well as Isabelle by his colleague Larry Paulson (both contributors to this book). ML has also been developed further and other theorem-proving systems like Coq, Lego and NuPrl owe much to Milner's ideas. Proof, Language and Interaction is divided into five sections: "Semantic foundations", "Programming logic", "Programming languages" and "Concurrency and mobility". These successfully reflect the developing interests of Milner through his professional career. "Semantic foundations" includes contributions on the linking of different types of semantics. Full abstraction, a term coined by Milner, is developed further by Samson Abramsky, a colleague at Edinburgh who has since moved on to join the Programming Research Group (PRG) at Oxford within the Oxford University Computing Laboratory. Hoare, who recently moved from the PRG to join Microsoft Research in Cambridge, is closely associated with the Computing Laboratory there. He presents his and his colleagues' work on deriving an operational semantics algebraically. The linking of semantics and concurrency is also explored. In "Programming logic", Gordon (like Milner, of Edinburgh and Cambridge) gives a helpful and less technical historical view of the development of the original LCF into his own important contribution to computer science, HOL, one of the most widely used theorem provers. Paulson, colleague at Cambridge, gives a related but much more technical account of a fixed-point approach to induction. Robert Constable, developer of the NuPrl theorem prover, and his colleagues at Cornell University in the United States, present the formalisation of automata theory. The "Programming languages" section naturally includes work on Milner's ML as well as a programming language based on the p-calculus. Gerard Berry, who is based in Paris, presents a useful introduction to the important synchronous language Esterel, whose design was highly influenced by Milner's work on process calculi and bisimulation. The section on concurrency, as expected, includes developments of Milner's CCS. The final mobility section presents advances with respect to the p-calculus, which is where Milner's most recent research interests and contributions lie. All of these essays build on concepts that Milner originated or promulgated himself, either directly or indirectly. This unifying force helps to provide structure to the book, especially because Milner's own work, although it is varied in application, has a consistency in elegance of style that is a feature of work by all top-class theoreticians. The book finishes with a list of contributors, but does not include an index. This would have been a useful addition for those wishing to use it as a reference work. Some abbreviations (for example PCF, a programming language development of LCF) are introduced without expansion or comprehensive explanation. An index might have made some of these omissions clear to the editors. Alternatively, or in addition, a glossary of terms, especially those coined by Milner himself, would have been an interesting supplement. However, these are minor quibbles in an otherwise well-edited and presented volume. The majority of the material is highly technical in nature and is only suitable for those acquainted with the field. The introductory biography is naturally approachable to a wider readership and is a useful historical record, but its 17 pages, out of a voluminous 722 in total, would not alone justify acquisition of the book. Ultimately, this collection will be at home in any good computer-science library, and this will probably be its main destination. It will also be of interest to theoretical computer scientists wanting a book that provides a range of invited papers all of which are of international journal class. Most computer scientists with an interest in the theoretical developments of the subject would be only too happy to have this book on their shelves if they could afford it. In 1999, as head of the Computer Laboratory at Cambridge, Milner officiated during the celebrations for the 50th anniversary of the early Edsac computer, developed by Maurice Wilkes and his team, which first ran a program successfully in 1949. Indeed, in 1956, Milner himself attended a computing course at Cambridge using the Edsac. Wilkes was a important leader of the Cambridge University Computer Laboratory. His expertise on the pioneering practical development of computers counterpoints Milner's contribution in the mathematical underpinning of computer science. The balance of theory and practice has been a key feature of work undertaken at Cambridge that continues under Milner's direction to this day and is the basis for all significant computer-science research. Milner has always ensured that his research contributions have been relevant as well as fundamental. This book is a fitting "thank you" from those who have benefited most directly from Milner's insights. In turn, it should help others to appreciate his influential contribution to theoretical computer science. Jonathan Bowen is professor of computing, South Bank University. From rrosebru@mta.ca Sat Feb 10 17:24:16 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1AKfXj07102 for categories-list; Sat, 10 Feb 2001 16:41:33 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <4.1.20010208103452.00af4d30@mail.oberlin.net> X-Sender: cwells@mail.oberlin.net X-Mailer: QUALCOMM Windows Eudora Pro Version 4.1 Date: Thu, 08 Feb 2001 10:48:43 -0800 To: categories@mta.ca From: Charles Wells Subject: categories: Inevitability of ordering products Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 23 Vaughn Pratt made some valid points about my earlier remarks on the inevitably of binary product projections being ordered. For the most part, I agree with him (but see below), since my (unclearly made) point was that it is inevitable in our current mathematical culture, not that it was mathematically inevitable. However, I am stuck on one point: Sometimes one needs to refer to one of the projections, and that involves giving the projections names. I mentioned "red" and "blue" as examples of names that do not introduce a spurious ordering. But in practice, we must occasionally give names. This is not only for computation, either. For example, one sometimes needs to assume that an n-ary operation factors through one of the projections, and then deduce consequences from that (Peter Johnstone did something like that in his study of varieties that are ccc's). In the proof one must give a name to the projection it factors through. So I argue that naming the projections is sometimes a practical necessity, and given current mathematical habits the names are likely to have some intrinsic (culturally intrinsic!) ordering. But we could use red and blue. Or vanilla and chocolate. Charles Wells, 105 South Cedar St., Oberlin, Ohio 44074, USA. email: charles@freude.com. home phone: 440 774 1926. professional website: http://www.cwru.edu/artsci/math/wells/home.html personal website: http://www.oberlin.net/~cwells/index.html NE Ohio Sacred Harp website: http://www.oberlin.net/~cwells/sh.htm From rrosebru@mta.ca Sun Feb 11 17:48:55 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1BKr9P12402 for categories-list; Sun, 11 Feb 2001 16:53:09 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <3A85D882.CF0F0EE9@kestrel.edu> Date: Sat, 10 Feb 2001 16:10:42 -0800 From: Dusko Pavlovic X-Mailer: Mozilla 4.72 [en] (X11; U; SunOS 5.5.1 sun4u) X-Accept-Language: en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Re: Why binary products are ordered References: <200102080117.RAA13130@coraki.Stanford.EDU> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 24 Hi. I am also trying to catch up, perhaps belatedly, with the "spurious ingredients" thread, but I am quite lost in some parts. > But woven into Charles' argument is what Bill has called the "totally > arbitrary singleton operation of Peano." To begin embarassing myself --- I am not sure what Peano's singleton operation is. Is it the map x|-->{x}? If it is --- why is this operation totally arbitrary, like Bill says? In particular, why is it more arbitrary than the successor operation in arithmetic (which Peano used)? It comes about as a part of the initial algebra structure on Godel's cumulative hierarchy, just like the successor comes about in NNO. Aren't all our inductive constructions based on such operations, including the software we are using to run this conversation? I would really appreciate help with this. Also, I somehow came to think of set theory as *tree representations of abstract sets*, much like vector spaces are used for group representations. Is this wrong? It seems to me that introducing the external, "spurious" elements (eg vectors) is the whole point of representations. And more than that, the essence of our thinking: Isn't every metaphor, as a deviation from the abstract view, built of spurious elements? Isn't every novel a bunch of lies, things that never happened, put together to tell some truth? Can we really define cartesian product without the spurious elements? I am sure we can, but it would be good to know more precisely how to distinguish the spurious from the authentic elements. Otherwise, we may end up "slinging back and forth ill-defined epithets", like i am probably doing now. With apologies, and best wishes, -- Dusko > Surely anyone insisting on names like 1 and 2 or red and blue for the > projections of binary product is backsliding into the ZFvN tarpit of > spurious rigidified membership. If this backsliding really is inevitable > as Charles seems to be saying, how does one reconcile this with Bill's > view of "rigidified membership" as "mathematically spurious"? > > Must mathematics accept the spurious, in this or any other case? > > Vaughan From rrosebru@mta.ca Sun Feb 11 17:48:55 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1BKrcJ12595 for categories-list; Sun, 11 Feb 2001 16:53:38 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <001001c09462$a3363b00$1349393f@cpu> From: "zdiskin" To: References: <3.0.6.16.20010208101428.44872230@pop.cwru.edu> Subject: categories: Re: Why binary products are ordered Date: Sun, 11 Feb 2001 11:40:37 -0800 MIME-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: 8bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 25 OOPS! In my previous posting i've made some mixed-up and talked mainly about notation for diagrams while the actual question is whether product is commutative (symmetric) operation in Sets. Below is a sketch of possible solution. First of all, product is a diagram operation and explicit presentation of their syntax would be useful; so, let me present a bit of technicalities. Let G be some base category (think of the category of graphs). The arity of a diagram operation F (think of products, push-outs...) is a G-morphism s: S^in --> S with S the shape of the operation and S^in the input shape. For example, for binary products, S is the graph [x] <--p-- [u] --q--> [y] where [ ]'s denote nodes and arrows' names are written right on the arrows, S^in is the two-node discrete graph [x] [y], and morphism s is its embedding into S. A G-object C (think of a category) is an F-algebra if for any diagram d: S^in --> C there is a unique diagram F^C(d): S-->C such that s;F^C(d) = d (input data are preserved); below i'll write just F for F^C. Well, categorically we normally have many isomorphic F(d)'s, let's skip this for a while. And as for products of sets (ie, F is Prod, C is Sets), by using names p and q that are already given in the shape, we really have a canonical choice. Namely, for any d: [x] [y] --> Sets with x.d=A, y.d=B, we define u.Prod(d) = { t: {p,q} --> A \cup B | p.t \in A, q.t \in B } with evident p.Prod(d) and q.Prod(d). F is called commutative on algebra C if any isomorphism i: S^in --> S^in has an isomorphic extension i+: S --> S with s;i+ = i;s s.t. for any d: S^in --> C, F(i;d) = i+ ; F(d) Now it is seen that Prod is commutative in Sets because any isomorphism i: S^in --> S^in has an evident required extension i+, i+(u) = u and i+ acts on the arrows p,q, . exactly like i acts on their targets x,y,.. The illusion of non-commutativity of products in Sets arises because of disregarding the diagrammatic nature of the operation: isomorphism i on the nodes in the shape acts on d but the corresponding i+ acting on the arrows is not taken into consideration. A peculiarity of what was described above is that names of items in the shape are used in the definition of the operation. So, for example, the following two shapes [x] <-- weight -- [u] -- height --> [y] and [x] <-- red -- [u] - blue -->[y] though isomorphic yet different and determine the two different product operations producing isomorphic yet different results from the same input. Thus, what we usually call the product operation is something like operation schema parameterized by pairs of names. Then expressions like Prod[weight:A, height:B] denote a concrete instance of the shape schema and, simultaneously, a diagram d in Sets with weight.codom.d = A and height.codom.d = B. Now back to AxB vs. BxA. The writing AxB is normally unambiguous, it means [1st:A] x [2nd:B] and encodes (i) the standard shape instance [x] <-- 1st -- [u] -- 2nd --> [y] and (ii) the diagram d: [x] [y] --> Sets, x.d = A, y.d=B. In contrast, the writing BxA is really ambiguous: it may mean either (a) [1st:B] x [2nd:A] that encodes the same standard shape instance [x] <-- 1st -- [u] -- 2nd --> [y] but now the diagram is x.d = B, y.d=A; or it may mean (b) [2nd:A] x [1st:B] that encodes the non-standard shape instance [x] <-- 2nd-- [u] -- 1st --> [y] and again the diagram x.d = B, y.d=A. It seems that thinking naïvely-set-theoretically people tend to see in writing BxA the case (a) and then, of course, BxA is not equal to AxB. And thinking categorically, people tend to see in writing BxA the case (b) and then BxA is the same as AxB. So, the problem 'ordered vs. unordered products ' is a problem of poor notation for product operation like BxA while the operation itself is a *commutative* diagram operation as defined above. Actually it was already said in early postings but now it became more transparent. Finally, some speculation. It seems that parameterization of (shapes of ) operations by names, and use of these names in operation's definitions, is applicable to other standard categorical operations and can be considered in a general setting. Probably, it could be made precise by some kind of internalization ...? Zinovy Diskin From rrosebru@mta.ca Sun Feb 11 17:50:12 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1BKqeg12064 for categories-list; Sun, 11 Feb 2001 16:52:40 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <003201c093cd$c9a89020$cc49393f@cpu> From: "zdiskin" To: References: Subject: categories: Re: Why binary products are ordered Date: Sat, 10 Feb 2001 17:54:58 -0800 MIME-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 26 Michael Barr wrote: > As I said in an earlier post, the whole thing is a figment of the linear > way we write (and speak, for that matter). Products are over unordered > sets and any ordering is purely irrelevant. > It's right of course but maybe some explanation of what is meant would be useful. Even if we work in naive set theory, products are defined for diagrams d: I -> Set and thus expressions Prod(A,B,C) or AxBxC are, strictly speaking, incorrect because we don't see diagrams. When we use such expressions we actually use the following convention: (i) the source of any diagram is an initinal fragment of natural numbers, I={1,2,3,...n} (ii) the very mapping d is defined by the correspondence of the natural ordering I={1,2,...} and the list of sets in the expressions above in their reading from left to right, eg, AxBxC encodes the diagram d1=A, d2=B, d3=C. Quite similarly, we may use colored inks for writing AxBxC... and state another convention: (i)' the source of any diagram is a set of colors, I={red, yellow, blue,...} (ii)' the very mapping d is defined by correspondence between semantic meaning of these labels 'red', 'yellow', .... and colors of inks with which symbols 'A', 'B', 'C' are written, eg, A(written in yellow) x B(in greeen) x C(in red) encodes the diagram d: {yellow, green, red} --> Set with yellow.d=A, green.d=B, red.d =C. Does it mean that pdoducts are colored? :) So, back to the "problem of ordered vs. unordered products": ordering is not more than a notational tip for encoding diagrams having nothing to do with the construct of product as such. In applications, where we need to deal with semantically meaningful indexes -- elements of I, the convention of having I={1,2,..} is irrelevant and another notational tip was invented. To designate the product of diagram d: {red, blue}-> Set with red.d=A, blue.d=B, we write Prod(red:A, blue:B) or (red:A) x (blue:B) or just [red:A, blue:B] and it's really convenient. Thus, expression AxB denotes Prod(1:A, 2:B) while BxA denotes Prod(1:B, 2:A) which are different just becausse these are products of the *different* diagrams. So, heavy use of convention (i),(ii) and the corresponding notation in classical math may be misleading (notational peculiarity is attributed to the notion as such) and thus, as Mike Barr wrote in his early posting, is its disadvantage. It became an *annoying* disadvantage when you start to work in applications (say, relational database theory) with your old habit to consider relations as sets of ordered tuples. ================ Actually, a similar problem we have in categorical products and other categroical operations producing multiple items and so we need a convention how to name/denote them. For example, having a diagram d: I--> C, we need to agree how to denote (name) projections. There is no such a problem with usual operations over sets because there is a single result and we usually denote it by the very term built with the symbol of the operation, say, 8+3. Let's imagine now that we have a binary operation * on integers producing two results: their difference and product, so that 8*3=(5,24). Of course, the latter notation is ambiguous and actually we need to write say [1st:8] * [2nd:3] = [1ST: 5, 2ND:24]. Thus, a really unambiguous format for writing arity-coarity shape of the operation * is [1st:_] * [2nd:_] = [1ST:_ , 2ND:_ ] where _'s denote placeholders. Well, this notation is still using, though inesentially, some ordering flavor and so let's suppose that the two operands of our operation are distingusihed by some meaningful (semantic) roles they play, say, one operand is considered to be 'principal' while the other is 'auxiliary'; as for the two results, we may use the underlying procedures for naming them. Then the arity-coarity shape might be written as [princ:_ ] * [aux:_ ] = [diff:_ , prod:_ ] and no any ordeirng used. Note, names of the results are included in the syntax of the operation from the very beginning and not taken on the sky. Probably, Colin McLarty wrote about the same. ======================= After all, it seems that in this (indeed somewhat figment) debate (initiated, i remind, by a Todd Wilson's question about comparative pluses and minuses of the two ways of treating products w.r.t. applications) the actual principle difference between them, that really matters for applications, was lost, i mean not articulated explicitly and hence lost by the applied domains part of the audience. I will sketch it for the case of relations because in application we normally deal with relations rather than products. In ST, you first define tuples (actually, as we've seen, mappings defined on unordered sets) and *then* a relation is a set of tuples of the corresponding type. In CT, you *first* define a relation as a set equipped with a jointly monic family of outgoing mappings (that is, in fact, declare a special predicate for the corresponding diagram of arrows with common source) and then, if you need, define a tuple as an element of that set. The CT-way is a really abstract specification applicable in any context where objects of interest are organized into a category (say, we may define what is a relation between the two database schemas). In ST-way, we have just a particular specification, in fact, an elementwise implementation of the categorical specification. In sofware engineering terms, one might say that the CT-way is object-oriented (though actually it's arrow orineted) since relation appears as a set of objects while the ST-way is value-oriented since relation is just a table of values. Also, these two ways induce the two different logics. In the CT-treatment, relations appear as new (derived) sorts to which basic sorts of other theories can be mapped when we deal with interpretaions of theories. In applications (say, consider the famous ER-diagrams), this phenomenon is not exotics and well known under the name of 'semantic relativism' (what is an entity -- basic sort -- for one user, may be a relationship for another user). In the logic naturally induced by the ST-treatment (Tarsky's first-order structures), a theory interpretation can map a basic relation to a derived relation but mapping a basic sort to relation (either basic or derived) is not legitimate. An essential difference! Zinovy Diskin From rrosebru@mta.ca Sun Feb 11 17:50:14 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1BKq7w12147 for categories-list; Sun, 11 Feb 2001 16:52:07 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f To: categories@mta.ca Subject: categories: TACS 2001 -- call for papers Reply-to: bcpierce@cis.upenn.edu Date: Sat, 10 Feb 2001 11:20:35 -0500 Message-ID: <17144.981822035@silvercomet.emperorlinux.com> From: bcpierce@cis.upenn.edu Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 27 Call For Papers Fourth International Symposium on Theoretical Aspects of Computer Science (TACS 2001) October 29-31, 2001 Tohoku University, Sendai, Japan http://tacs2001.ito.ecei.tohoku.ac.jp/tacs2001/ The TACS Symposium will focus on the theoretical foundations of programming and their applications. The topics of interest include... Theoretical aspects of the design, semantics, analysis, and implementation of programming languages and systems; logics of programs; calculi and models of concurrency and parallel computation; theories of mobile computation and system security; categories and types in computer science; formalisms, methods, and systems for program specification, verification, synthesis, and optimization; constructive, linear, and modal logics in computer science. The scientific program will consist of invited lectures, contributed talks, and demo sessions. A proceedings containing the full papers of the invited and contributed talks will be published by Springer-Verlag as a volume of Lecture Notes in Computer Science. IMPORTANT DATES Submission deadline: April 1, 2001 Notification to authors: June 15, 2001 Deadline for final versions: July 20, 2001 INVITED SPEAKERS Luca Cardelli Microsoft Research Daniel Jackson Massachusetts Institute of Technology Christine Paulin-Mohring Universite Paris Sud & INRIA Andrew Pitts University of Cambridge Jon Riecke Lucent Technologies Kazunori Ueda Waseda University CONFERENCE CHAIR: Takayasu Ito Tohoku University PROGRAM CO-CHAIRS: Naoki Kobayashi Tokyo Institute of Technology kobayasi@cs.titech.ac.jp Benjamin Pierce University of Pennsylvania bcpierce@cis.upenn.edu PROGRAM COMMITTEE: Zena Ariola University of Oregon Cedric Fournet Microsoft Research Jacques Garrigue Kyoto University Masami Hagiya University of Tokyo Robert Harper Carnegie Mellon University Masahito Hasegawa Kyoto University Nevin Heintze Lucent Technologies Martin Hofmann Edinburgh University Zhenjiang Hu University of Tokyo Naoki Kobayashi Tokyo Institute of Technology Martin Odersky Ecole Polytechnique Federale de Lausanne Catuscia Palamidessi Pennsylvania State University Benjamin Pierce University of Pennsylvania Francois Pottier INRIA Andre Scedrov University of Pennsylvania Natarajan Shankar SRI International Ian Stark Edinburgh University Makoto Tatsuta Kyoto University SUBMISSION INFORMATION Authors are invited to submit full papers (up to 6000 words, including figures and bibliographies). Papers must be unpublished and not submitted for publication elsewhere. Submissions should be in Postscript format, on A4 or US letter pages. They must be printable on common printers and viewable with ghostview. The first page of each submission should include the email address, telephone, and fax numbers of the corresponding author. Accepted papers must be presented at the symposium, and the final manuscript must be prepared in the LNCS format. All submissions should be done electronically through the TACS submission page http://saul.cis.upenn.edu:8086/. From rrosebru@mta.ca Sun Feb 11 17:57:25 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1BL1fJ13973 for categories-list; Sun, 11 Feb 2001 17:01:41 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Mime-Version: 1.0 X-Sender: duskin@mail.buffnet.net Message-Id: Date: Sun, 11 Feb 2001 15:19:50 -0500 To: categories@mta.ca From: John Duskin Subject: categories: Inevitability of ordering products Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 28 I guess that the point I was trying to make in my post was missed in my telegraphic submission. I'll try to make what I was trying to say clearer. If you take the "representable functor" definition of a product of a object A with an object B, you say that an object P together with an ordered pair of arrows (p_A:P--->A,p_B:P-->B) is a product of A with B if for all objects T , the mapping Hom(T,P)--->Hom(T,A)xHom(T,B), defined by f |---> (p_A.f,p_B.f) is a bijection. This makes it clear that P together with (p_A,p_B) represents the product of A with B and P together with (p_B,p_A) represents the product B with A and that these are not representations of the same functor but that there is a natural isomorphism of such an object with itself which "interchanges the two projections". Note also that this distinction remains even for a product of A with itself which leads a pr_1 and pr_2 notation for the two "projections". Now, as with all such bijections, one can eliminate all reference to sets of morphisms by a "for all x there exists a unique y such that..." statement which here becomes: for all ordered pairs of arrows of the form (x:T--->A,y:T--->B) , there exists a unique arrow f:T--->P, such that (p_A.x,p_B.y)=(x,y), and the distinction made in in set theory between AxB and BxA," that they are not equal, but there is a 'canonical' bijection between them", is perfectly maintained entirely within category theory... or is it? The use of the ordered pair term "(x,y)" still appears in the replacement first order statement, and if the only way that one can use "ordered pair" is through von Neumann's clever but rather grotesque (x,y)={x,{x,y}}, one has to pull in "Peano's entirely spurious singletons" , as Bill Lawvere referred to them. Now if the purpose of an "underlying logic" us to "codify by making explicit the normal habits of reasoning that all mathematicians will accept" and that "an object P and arrows p_A:P--->A and p_B:P--->B" is equivalent to "an object P and arrows p_B:P-->B and p_A:P-->A", or more starkly, the logical equivalence of,"p_A and p_B" and "p_B and p_A". Then there would seem to be no way that a purely first order category theory could make the distinctions that we teach in every elementary math course about the distinction between (x,y) and (y,x), unless we appeal to informal aspects of everyday language where "and" is sometimes commutative and sometimes not, and thus in this case rely on "everybody's having met (x,y) long before they have ever heard of a 'category' ". Apparently this subtlety has surfaced before: In the beginning of Bourbaki's Theorie des Ensembles,\footnote{which, remember, was written by "working mathematicians" who did not consider themselves "professional logicians or professional set-theorists", and may even have had some contempt for them (among others) if we are to judge from a certain fronts piece photograph inserted by Andre Weil into the Fascicule de Resultats.} they introduced as "specific signs", in addition to those of equality and membership, another sign of weight 2, \couple xy, ultimately written as (x,y) together with the Axiom (A3) : (for all x)(for all y)(for all x')(for all y' ) (x,y)=(x',y') implies x=x' and y=y'. They then define "z is an ordered pair (couple)" by "(there exists x)(there exists y)(z=(x,y))", which then gives (x,y) its first and second projections because of the way that "there exists " is constructed (using their "\tau operator"). The existence of the cartesian product of the set A with the set B then follows, as usual, as the set of ordered pairs,since the presence of (x,y) allows them to describe formal "relations" R|x,y| as properties of the ordered pair z=(x,y). Only later do they observe, in an exercise, that the little von Neumann nest of singletons has the property of the axiom A3, but they use this only to show that \couple xy together with A3 is relatively consistent with their other axioms for set theory. It is clear, however, that \couple xy and A3 could have been introduced immediately after they had done quantification and long before any of the axioms for \epsilon were introduced. But, after all, they were trying to use their "Theory of Sets" as a foundation for all of mathematics, so most people have considered this whole business of adding \couple xy and A3 at so fundamental a level an eccentric and superfluous curiosity, and it has all but been completely forgotten. My point is not to pull category theorists back into the intricacies of Bourbaki 's treatment of logic, but rather to point out that the idea of an ordered pair has at least once before been considered a notion that properly belongs somewhere anterior to set theory and can be used in category theory without fear of the latter suffering from any "set-theoretic contamination". In any case, to my eyes, the use of "lists and addresses" with their attendant ordering seems to be pretty fundamental in computer science. Amusingly, Grothendieck "pushed" representability in the forlorn hope that it would convince working mathematicians that they did not have to give up their Cantorian Paradise of " set-theory" in order to make use of the unique insights provided by "category theory", but then had to (re-)invent "universes" when the old paradoxes of set-theory and the category of all sets, all groups, etc. carpingly resurfaced. Bill Lawvere, in contrast, noticed that when the working axioms of set-theory were rephrased in purely "category-theoretic" terms, that they, amazingly, all became "first order" statements , thereby raising the question of an entirely new way to look at foundational questions in which the pesky membership paradoxes could not arise nor even be formally expressible. He, in contrast to Grothendieck, "pushed" the much more radical move of, effectively, "banning all use of Hom-sets" and thereby made the divide crystal clear. From rrosebru@mta.ca Mon Feb 12 19:58:27 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1CNF4Y16963 for categories-list; Mon, 12 Feb 2001 19:15:04 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <3.0.6.16.20010211182455.133f94ae@pop.cwru.edu> X-Sender: cxm7@pop.cwru.edu X-Mailer: QUALCOMM Windows Eudora Light Version 3.0.6 (16) Date: Sun, 11 Feb 2001 18:24:55 To: categories@mta.ca From: Colin McLarty Subject: categories: Singleton as arbitrary In-Reply-To: <3A85D882.CF0F0EE9@kestrel.edu> References: <200102080117.RAA13130@coraki.Stanford.EDU> Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 29 Dusko Pavlovic wrote: >To begin embarassing myself --- I am not sure what Peano's singleton operation >is. Is it the map x|-->{x}? > >If it is --- why is this operation totally arbitrary, like Bill says? In >particular, why is it more arbitrary than the successor operation in arithmetic >(which Peano used)? It comes about as a part of the initial algebra structure >on Godel's cumulative hierarchy, just like the successor comes about in NNO. Well, something *like* Peano's operation occurs in that initial algebra structure, but that is not much to the point. The point is: successor did not have to wait for NNOs to be defined. It occurs throughout arithmetic for nearly as long as we have records of systematic thought. And it is central to all uses of arithmetic today. The *singleton subset* idea is also very old: A geometric condition can define a subset of points in the plane, and perhaps a singleton subset. And singleton subsets are all over math today for the same reason. It is a recent idea that given any set x there is some set {x}. Bill traces it to Peano. It plays no role in ordinary mathematical practice, and is unnecessary in set theory. It does not exist in categorical set theory. >Also, I somehow came to think of set theory as *tree representations of >abstract sets*, much like vector spaces are used for group representations. Is >this wrong? It seems to me that introducing the external, "spurious" elements >(eg vectors) is the whole point of representations. The whole point of group representations is that each group has many of them. The classical Lie groups are given as groups of linear transformations in the first place. The power of representation theory is to relate these with *other* representations of the same groups. Each ZF set has exactly one membership tree. Thus the "representation" cannot do anything like what group representations do. And obviously it plays no role in ordinary math practice. I hope no one believes that singletons, or trees, or vectors are "spurious" per se. Some uses of the ideas are "arbitrary", and some claims about them are "spurious". best, Colin From rrosebru@mta.ca Mon Feb 12 22:20:55 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1D1p5619933 for categories-list; Mon, 12 Feb 2001 21:51:05 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: Eduardo Dubuc Message-Id: <200102122027.PAA28404@cogito.math.uqam.ca> Subject: categories: Re: Inevitability of ordering products To: categories@mta.ca Date: Mon, 12 Feb 2001 15:27:42 -0500 (EST) In-Reply-To: <4.1.20010208103452.00af4d30@mail.oberlin.net> from "Charles Wells" at Feb 08, 2001 10:48:43 AM X-Mailer: ELM [version 2.5 PL2] MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 30 ordering is not inevitable naming is inevitable how do you refer to a proyection withot naming it ? of course naming a proyection by the object it proyects is the mother of all evil have you delt with actions of the symetric group, say, on polynomials on several variables ? There is a related (if not the same) confusion here. what sense has the concept of unlabeled graph ? try to put an unlabeled graph inside a computer ? well, unlabeled graph has to be a quotient by an equivalent relation ... and so on ... From rrosebru@mta.ca Tue Feb 13 21:22:21 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1E0nfO16599 for categories-list; Tue, 13 Feb 2001 20:49:41 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <3A88BE0C.C3CA8E04@kestrel.edu> Date: Mon, 12 Feb 2001 20:54:36 -0800 From: Dusko Pavlovic X-Mailer: Mozilla 4.72 [en] (X11; U; SunOS 5.5.1 sun4u) X-Accept-Language: en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Re: Inevitability of ordering products References: <200102122027.PAA28404@cogito.math.uqam.ca> Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 31 Eduardo Dubuc wrote: > what sense has the concept of unlabeled graph ? > > try to put an unlabeled graph inside a computer ? you mean unordered? i would implement it as an ordered graph, with an additional involutive map on the edges, ie Edges <--inv-- Edges ==dom,cod==> Nodes dom.inv = cod inv.inv = id --- which, in a way, confirms that > well, unlabeled graph has to be a quotient by an equivalent relation ... isn't the "ordering" of the components of a product AxB (by the names, colors A and B), in a similar way, "factored out" by the canonical isomorphism with BxA? isn't coherence theory the way we can always factor out such arbitrary annotations on objects? (SORRY i am posting too much.) -- dusko From rrosebru@mta.ca Tue Feb 13 21:22:31 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1E0mYS16698 for categories-list; Tue, 13 Feb 2001 20:48:34 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <3A88B95D.D0243A3E@kestrel.edu> Date: Mon, 12 Feb 2001 20:34:37 -0800 From: Dusko Pavlovic X-Mailer: Mozilla 4.72 [en] (X11; U; SunOS 5.5.1 sun4u) X-Accept-Language: en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Re: Singleton as arbitrary References: <200102080117.RAA13130@coraki.Stanford.EDU> <3.0.6.16.20010211182455.133f94ae@pop.cwru.edu> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 32 Colin McLarty wrote: > >It comes about as a part of the initial algebra structure > >on Godel's cumulative hierarchy, just like the successor comes about in NNO. > > Well, something *like* Peano's operation occurs in that initial algebra > structure, but that is not much to the point. [snip] > It is a recent idea that given any set x there is some set {x}. Bill > traces it to Peano. It plays no role in ordinary mathematical practice, and > is unnecessary in set theory. It does not exist in categorical set theory. but didn't joyal and moerdijk actually write a book about it? i think they call it successor, but the standard model is x|-->{x}. (or did i mix it all up?) > >Also, I somehow came to think of set theory as *tree representations of > >abstract sets*, much like vector spaces are used for group > >representations. > > The whole point of group representations is that each group has many of > them. The classical Lie groups are given as groups of linear > transformations in the first place. The power of representation theory is > to relate these with *other* representations of the same groups. > > Each ZF set has exactly one membership tree. Thus the "representation" > cannot do anything like what group representations do. i didn't say that set theory provides tree representations of ZF sets; ZF sets *are* trees (or acyclic rooted graphs). i said that set theory provides tree representation of *abstract* sets. think of lazy natural numbers, flat natural numbers, finite chains, all of them different *and useful* representations of the same abstract set. > And obviously it > plays no role in ordinary math practice. the words "obviously" and "practice" don't go together well. 20 years ago, it seemed obvious that complexity theory was mostly an academic whim. nowadays, the security infrastructure built upon it is a critical part of the engineering practices, and the very life of the net. large cardinals may still find unexpected applications, say in establishing the new tax policies =;0 all the best, -- dusko From rrosebru@mta.ca Tue Feb 13 21:22:42 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1E0lED16650 for categories-list; Tue, 13 Feb 2001 20:47:14 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Mon, 12 Feb 2001 19:39:40 -0500 (EST) From: James Borger X-X-Sender: To: Subject: categories: Re: Inevitability of ordering products In-Reply-To: Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 33 On Sun, 11 Feb 2001, John Duskin wrote: > Bill Lawvere, in contrast, noticed that when the working axioms of > set-theory were rephrased in purely "category-theoretic" terms, that > they, amazingly, all became "first order" statements , thereby > raising the question of an entirely new way to look at foundational > questions in which the pesky membership paradoxes could not arise nor > even be formally expressible. He, in contrast to Grothendieck, > "pushed" the much more radical move of, effectively, "banning all use > of Hom-sets" and thereby made the divide crystal clear. Can someone give a reference to an elaboration of this point of view? Since I am not a real category theorist and have at best a weak understanding of foundations, something written for the mainstream mathematician would be even better. Thanks in advance. Jim Borger From rrosebru@mta.ca Wed Feb 14 12:53:03 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1EG2Qq18955 for categories-list; Wed, 14 Feb 2001 12:02:26 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: "Christopher R A Gilmour" Organization: University of Cape Town To: categories@mta.ca Date: Wed, 14 Feb 2001 17:53:21 +0200 Subject: categories: Tragic news of Japie Vermeulen X-mailer: Pegasus Mail for Windows (v2.33) Message-Id: Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 34 Dear colleagues It is with great sadness and pain that I tell you that Japie Vermeulen died tragically on the night of Sunday 11 February. He was on his way back from visiting family in Ceres, about a two-hour journey from Cape Town. He had taken a route through Bain's Kloof, a spectacular pass over the mountains between Ceres and Wellington. It was established that his car was overheating, the radiator was found to be empty and there was a hole in a water pipe. He had taken a container and attempted to descend a steep path to fetch water from a stream. He slipped and fell 10 to 15 metres, hitting his head and fracturing his skull. He died instantly. His body was eventually found, after a search, at 5pm on Monday. All who knew Japie will mourn a wonderful human being and a brilliant mind. ______________________________________________________________________ Prof Christopher Gilmour, E-mail: CRAG@maths.uct.ac.za Department of Mathematics Phone: +27-(0) 21-650-4065 and Applied Mathematics, or 650-3192 University of Cape Town, Fax: +27-(0) 21-650-2334 Rondebosch 7701, South Africa From rrosebru@mta.ca Thu Feb 15 16:08:27 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1FJZ8N06247 for categories-list; Thu, 15 Feb 2001 15:35:08 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: Eduardo Dubuc Message-Id: <200102141840.NAA09452@cogito.math.uqam.ca> Subject: categories: Re: Inevitability of ordering products To: categories@mta.ca Date: Wed, 14 Feb 2001 13:40:08 -0500 (EST) In-Reply-To: <3A88BE0C.C3CA8E04@kestrel.edu> from "Dusko Pavlovic" at Feb 12, 2001 08:54:36 PM X-Mailer: ELM [version 2.5 PL2] MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 35 This is concerning the mail of Dusko in reply to my mail: > > Eduardo Dubuc wrote: > > > what sense has the concept of unlabeled graph ? > > > > try to put an unlabeled graph inside a computer ? > > you mean unordered? i would implement it as an ordered graph, with an > additional involutive map on the edges, ie > > Edges <--inv-- Edges ==dom,cod==> Nodes > dom.inv = cod > inv.inv = id > > --- which, in a way, confirms that > yours is not an answer to my question, which I shall explain now (I thought that it needed no explanations) by an unlabeled graph i mean the drawing of a graph, in paper, say, or a graph buildt in space, the skeleton of a building for example. It has vertices and edges, and everybody knows what it is. Mathematically you could say a symetric relation on its (finete) set of vertices. But not quite so ... If you have n vertices, you have n! different labeling. Each labeling gives you a different labeled graph. The minute you have a set (in the mathematical sense) of vertices, you have a labeling. Namely, the elements of that set are the labels!. So, with a symetric relation (in the mathematical sense) what you got is a labeled graph. Not an unlabeled graph !. And you become well aware of this fact when you want to put a concrete unlabeled graph (say, the skeleton of a building) inside a computer !! REMEMBER I rise the question on unlabeled graph related to the question that we were discussing: INEVITABILITY OF NAMING (IN MATHEMATICS) (naming is not the same as labeling ?) >> well, unlabeled graph has to be a quotient by an equivalent relation ... I said that. It seems possible. I explain now the ... Given two graphs R, S (symetric relations) on a finite set X (of vertices), consider the natural action of the symetric group of X on the power set of X x X. Then, R =~ S iff they are in the same orbit. The elements of the quotient set are the unlabeled graphs. e.d. From rrosebru@mta.ca Thu Feb 15 16:08:27 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1FJXim04849 for categories-list; Thu, 15 Feb 2001 15:33:44 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <3.0.6.16.20010214093148.46276cdc@pop.cwru.edu> X-Sender: cxm7@pop.cwru.edu X-Mailer: QUALCOMM Windows Eudora Light Version 3.0.6 (16) Date: Wed, 14 Feb 2001 09:31:48 To: categories@mta.ca From: Colin McLarty Subject: categories: Re: Singleton as arbitrary Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 36 Dusko Pavlovic points out that various data types representing the natural numbers by posets are useful. That is true but hardly related to tree representations in set theory. (For example, these posets are generally not "extensional" in the sense of membership trees.) When I remarked that the operation x|--> {x} has no role in mathematical practice and does not exist in categorical set theory, Dusko replied: >but didn't joyal and moerdijk actually write a book about it? Joyal and Moerdijk wrote a book on algebraic characterization of models of ZF. They use an operation with formal properties like Peano's singleton. So I have to admit the singleton operation does figure in practice, when the "practice" is to describe ZF and related set theories. Not otherwise. When I said membership trees "obviously play no role in ordinary math practice" he replied >the words "obviously" and "practice" don't go together well. 20 years ago, it >seemed obvious that complexity theory was mostly an academic whim. nowadays, the >security infrastructure built upon it is a critical part of the engineering >practices, and the very life of the net. large cardinals may still find unexpected >applications, say in establishing the new tax policies =;0 Membership trees are hardly the same as the study of large cardinals. The large cardinals I know of are all described by isomorphism invariant properties (measurable: an uncountable set k which admits a non-principle k-complete ultrafilter). So the definitions that ZF set theorists give do not rely on membership, they are already definitions in categorical set theory. As to "obvious", we might wish that everything about practice was obscure. It would free up 'debate' wonderfully. But it is obvious right now that membership trees in set theory are used only for a handful of technical theorems in the foundations of set theory. Categorical set theorists also use them, for equiconsistency results with ZF. I don't claim to *prove* they will never have any other use. Perhaps one day they will be central to work in PDEs. Perhaps one day (as Philip Johnson predicts) Bible based biology will produce far greater advances than materialist science as practiced in recent centuries. I only say such claims are arbitrary. best regards, Colin From rrosebru@mta.ca Thu Feb 15 16:08:28 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1FJWCQ01198 for categories-list; Thu, 15 Feb 2001 15:32:12 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <4.3.1.1.20010213112222.00b612e0@popin.ncl.ac.uk> X-Sender: nbnr@popin.ncl.ac.uk X-Mailer: QUALCOMM Windows Eudora Version 4.3.1 Date: Tue, 13 Feb 2001 18:17:59 +0000 To: categories@mta.ca From: Nick Rossiter Subject: categories: Re: Why binary products are ordered In-Reply-To: <003201c093cd$c9a89020$cc49393f@cpu> References: Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii"; format=flowed X-Filter-Version: 2.0 (cheviot3) Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 37 At 05:54 PM 2/10/01 -0800, Zinovy Diskin wrote: > It became an *annoying* disadvantage when you start to >work in applications (say, relational database theory) with your old habit >to consider relations as sets of ordered tuples. Relational database theory is actually more subtle than this. The extension indeed is a set of ordered n-tuples but this is linked to an intension specifying attribute names and types. The extension is effectively indexed by names in the intension so that ordering of columns is immaterial. Since the ordering of tuples in the extension is also immateial, the model is very flexible. The indexing is in effect from another level. >In ST, you first define tuples (actually, as we've seen, mappings defined >on unordered sets) and *then* a relation is a set of tuples of the >corresponding type. In CT, you *first* define a relation as a set equipped >with a jointly monic family of outgoing mappings (that is, in fact, declare >a special predicate for the corresponding diagram of arrows with common >source) and then, if you need, define a tuple as an element of that set. Cannot such relations be better represented as pullbacks? Limits and colimits then appear to emerge naturally as keys (product thereof) and non-keys (sums) respectively. >The CT-way is a really abstract specification applicable in any context >where objects of interest are organized into a category (say, we may define >what is a relation between the two database schemas). In ST-way, we have >just a particular specification, in fact, an elementwise implementation of >the categorical specification. In sofware engineering terms, one might say >that the CT-way is object-oriented (though actually it's arrow orineted) >since relation appears as a set of objects while the ST-way is >value-oriented since relation is just a table of values. CT certainly appears more powerful at handling object modelling than ST. But I am not sure the relational model is simply value-oriented. The user view is such but the underlying theory (dependencies, normalization, intension-extension mapping, integrity rules) is very much arrow-based and hence also amenable to CT. Regards ... Nick http://www.cs.ncl.ac.uk/people/b.n.rossiter/home.informal/ From rrosebru@mta.ca Thu Feb 15 16:08:29 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1FJX2s05167 for categories-list; Thu, 15 Feb 2001 15:33:02 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: Amiguet Matthieu To: categories@mta.ca Message-ID: <3A8A8F1F.E49648BE@info.unine.ch> Date: Wed, 14 Feb 2001 14:58:54 +0100 X-Mailer: Mozilla 4.6 (Macintosh; I; PPC) X-Accept-Language: fr-CH,fr,en MIME-Version: 1.0 Subject: categories: statecharts and categories Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 38 Dear Categoricians, I'm wondering if there has been any work in formalizing statecharts [1] in categorical terms. If not, do you know of an other algebraic description of this specification language? Also, it seems to me that the operationnal semantic STATEMATE of Statecharts as described in [2] is very coalgebraic in nature. Did anybody write something about this? Thank you for any information or pointer, Matthieu REFERENCES: [1] Harel, D. (1987) Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8(3), 231--274. [2] Harel, D. and Naamad, A. (1996) The STATEMATE Semantics of Statecharts. ACM Transactions on Software Engineering and Methodology, 5(4), 293--333 From rrosebru@mta.ca Thu Feb 15 16:08:38 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1FJSg202726 for categories-list; Thu, 15 Feb 2001 15:28:42 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Tue, 13 Feb 2001 11:17:34 GMT Message-Id: <200102131117.LAA25831@brittle.dcs.ed.ac.uk> From: Martin Hofmann To: categories@mta.ca Subject: categories: 2nd CFP: WS on Implicit Computational Complexity Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 39 Third international workshop on Implicit Computational Complexity-2001 (ICC'01) ------------------------------------------------------------------------------- (affiliated with PADO and MFPS) The Implicit Complexity Workshop (ICC'01) will be held on Sunday, 20 May 2001 in Aarhus as part of the joint PADO/MFPS 2000 conferences. Topics of Interest: ------------------- The synergy between Logic, Computational Complexity and Programming Language Theory has gained importance and vigour in recent years, cutting across areas such as Proof Theory, Computation Theory, Applicative Programming, and Philosophical Logic. Several machine-independent approaches to computational complexity have been developed, which characterize complexity classes by conceptual measures borrowed primarily from mathematical logic. Collectively these approaches might be dubbed IMPLICIT COMPUTATIONAL COMPLEXITY. Practically, implicit computational complexity provides a framework for a streamlined incorporation of computational complexity into areas such as formal methods in software development, programming language theory. In addition to research reports on theoretical advances in implicit computational complexity, practical contributions bridging the gap between Computational Complexity and Programming Language Theory are therefore of particular interest. Previous Workshops ------------------ have been held in Indianapolis 1994, Baltimore 1998, Trento 1999, Santa Barbara 2000. Programme committee ------------------- Samson Abramsky (University of Oxford, UK) Martin Hofmann (University of Edinburgh, UK) (Chair) Bruce Kapron (University of Victoria, Canada) Harry Mairson (Brandeis University) Jean-Yves Marion (Loria, Nancy, France) So/ren Riis (Queen Mary and Westfield College, London) Helmut Schwichtenberg (University of Munich, Germany) Steering committee ------------------ Daniel Leivant (University of Indiana at Bloomington) Jean-Yves Marion (Loria, Nancy, France) Submission procedure -------------------- E-mail your contribution as a PostScript file to the programme chair (mxh@dcs.ed.ac.uk) to bereceived by 16 March 2001. Alternatively, you can send 5 hardcopies by air mail to the program chair. Authors with restricted copying facilities may also send a single hardcopy. Important dates --------------- 16 March 2001 Submission deadline (late submissions may be accepted after consultation with the PC chair) 10 April 2001 Notification of authors of accepted papers 20 May 2001 Workshop Workshop WWW-page ----------------- http://www.dcs.ed.ac.uk/home/mxh/ICC01.html Contact information ------------------- Martin Hofmann Division of Informatics University of Edinburgh JCMB, KB Mayfield Road Edinburgh EH9 3JZ UK tel : (44) 131 650 5187 fax : (44) 131 667 7209 mxh@dcs.ed.ac.uk From rrosebru@mta.ca Thu Feb 15 16:30:31 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1FK3RD05686 for categories-list; Thu, 15 Feb 2001 16:03:27 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <3A8BFFA9.C5A6AE37@email.unc.edu> Date: Thu, 15 Feb 2001 11:11:21 -0500 From: jim stasheff X-Mailer: Mozilla 4.7 [en] (WinNT; I) X-Accept-Language: en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: queries Content-Type: text/plain; charset=iso-8859-1 X-MIME-Autoconverted: from 8bit to quoted-printable by smtpsrv0.isis.unc.edu id LAA24256 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by mailserv.mta.ca id f1FGBPb30649 Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 40 Erdal Ulualan wrote: > > >From: jim stasheff > >To: Erdal Ulualan > >Subject: Re: categories > >Date: Fri, 26 Jan 2001 10:09:26 -0500 > > > >Erdal Ulualan wrote: > > > > > > Mr. Stasheff; > > > > > > I am a research assistant in Dumlupýnar University. I am studing > > > category theory. > > > I have some problems If you help me about following questions I > will > > > be very grateful to you. > > > > > > 1- If a category C has pullbacs no terminal object, then has C > finite > > > product? > > > > > > 2- How can be Simplicial crossed module of groups defined? > > > > > > 3- Is there crossed module of topological groups ? > > > > > > 4- How can be defined "pullback profinite crossed modules" > > > Sincerely > > > > > > Thank you for everything you have done and you will do. > > > Good days > > > > > > > > > >Dear Erdal, > > > > I am forwarding your question to some friends. Where is > >Dumlupýnar University? > > > >jim stasheff > > > > Dear stasheff > > Thank you for everything. Dumlupinar University is in Turkey. I > am waiting your advices. > > Sincerely > From rrosebru@mta.ca Thu Feb 15 22:30:53 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1G231F00023 for categories-list; Thu, 15 Feb 2001 22:03:01 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Thu, 15 Feb 2001 15:16:22 -0500 (EST) From: Peter Freyd Message-Id: <200102152016.f1FKGMQ13139@saul.cis.upenn.edu> To: categories@mta.ca Subject: categories: Question from Erdal Ulualan Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 41 If a category C has pullbacs no terminal object, then has C finite product? No. The simplest counterexample is the discrete category with two objects. From rrosebru@mta.ca Thu Feb 15 22:30:54 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1G23uZ00736 for categories-list; Thu, 15 Feb 2001 22:03:56 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <4.1.20010215151228.009f0500@mail.oberlin.net> X-Sender: cwells@mail.oberlin.net X-Mailer: QUALCOMM Windows Eudora Pro Version 4.1 Date: Thu, 15 Feb 2001 15:31:44 -0500 To: categories@mta.ca From: Charles Wells Subject: categories: Re: Unlabeled graphs In-Reply-To: <200102141840.NAA09452@cogito.math.uqam.ca> References: <3A88BE0C.C3CA8E04@kestrel.edu> Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 42 This is in reply to Eduardo Dubuc (quoted after the reply). I have a major point and a minor point. Minor point: The phrase "labeled graph" usually allows different nodes to have the same label. Eduardo clearly intends, however, that the labeling be injective. (In the usual sense there are n^n labels, not n!). This is only a matter of terminology. My answer refers to injective labeling as he intended. (Better terminology for his purposes would be to call them NAMED nodes.) Major point: Any way you store an unlabeled graph in a computer will involve a memory location for each node, and so introduces a labeling, indeed a total ordering, on the nodes. However, a high level language with pointers such as C can be used to describe the structure without any names being given explicitly. The structure head will point to a node, which will have a pointer to another node, etc, and the program text will not mention all the nodes directly. For the purpose of computing with the graph, you can have the program traverse the nodes without naming them. This is a commonly used technique. (There will have to be pointer structures for the edges with pointers to the two nodes each is incident on.) When the program is compiled, the nodes are made to correspond to memory locations but the locations are hidden from the user. It seems to me that this preserves the psychology of a drawing with no labels on the nodes. You can respond that each node has an implicit label, essentially an integer, which is the number of pointers you have to dereference to get to the node. But that is just like saying that in the drawing of the graph on a piece of paper, each node has an implicit label, namely its location on the paper. If you allow implicit labels like this the drawing has them and so does the graph in the computer. If you don't allow them then neither has labels. Let me forestall someone bringing up a red herring: The coordinates of the node on the paper depend on an arbitrary choice of coordinate system, unlike the number of pointers you need to get to the stored node in the computer. This argument, if someone makes it, is based on a misreading of what I said. I said each node is labeled by its location on the paper. I didn't say the coordinates of the location. The location itself is the label. (But how do you talk about it? You POINT to it!) --Charles Wells >by an unlabeled graph i mean the drawing of a graph, in paper, say, or a >graph buildt in space, the skeleton of a building for example. It has >vertices and edges, and everybody knows what it is. Mathematically you >could say a symetric relation on its (finete) set of vertices. But not >quite so ... > >If you have n vertices, you have n! different labeling. Each labeling >gives you a different labeled graph. > >The minute you have a set (in the mathematical sense) of vertices, you >have a labeling. Namely, the elements of that set are the labels!. So, >with a symetric relation (in the mathematical sense) what you got is a >labeled graph. Not an unlabeled graph !. > >And you become well aware of this fact when you want to put a concrete >unlabeled graph (say, the skeleton of a building) inside a computer !! > >REMEMBER I rise the question on unlabeled graph related to the question >that we were discussing: > >INEVITABILITY OF NAMING (IN MATHEMATICS) > (naming is not the same as labeling ?) > >>> well, unlabeled graph has to be a quotient by an equivalent relation >... > >I said that. It seems possible. I explain now the ... > > Given two graphs R, S (symetric relations) on a finite set X (of >vertices), consider the natural action of the symetric group of X on the >power set of X x X. Then, R =~ S iff they are in the same orbit. The >elements of the quotient set are the unlabeled graphs. > > e.d. > > > > > > Charles Wells, 105 South Cedar St., Oberlin, Ohio 44074, USA. email: charles@freude.com. home phone: 440 774 1926. professional website: http://www.cwru.edu/artsci/math/wells/home.html personal website: http://www.oberlin.net/~cwells/index.html NE Ohio Sacred Harp website: http://www.oberlin.net/~cwells/sh.htm From rrosebru@mta.ca Fri Feb 16 12:41:49 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1GG7CR09025 for categories-list; Fri, 16 Feb 2001 12:07:12 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <000001c09846$d8a1f800$175188c1@mat.ua.pt> Reply-To: "George Janelidze" From: "George Janelidze" To: Subject: categories: field and Galois theory Date: Fri, 16 Feb 2001 18:27:24 -0000 MIME-Version: 1.0 Status: RO X-Status: X-Keywords: X-UID: 43 Dear All, The following recent message of Tobias Schroeder >Hello, >all introductions to field and Galois theory I've found are written in a >"classical" way, i.e. making not much use of categorical notions. A lot of >computation is done where someone who is "categorical minded" has the >feeling that the results could be established in a more comprehensible and >clear way by category theory. -- Does somebody have a reference to a short >and good introduction to field and Galois theory from a categorical >viewpoint? > >Thanks > >Tobias Schroeder was already answered by Francis Borceux, who has beautifully written most of the book "Galois theories". I would like to add: I would say, "Field and Galois theory" sounds too general. For instance any such introduction should include a lot of Group theory and polynomials, which of course would look much nicer if various parts of Category theory were involved - but this is a very long story! So, let me replace "Field and Galois theory" by just "The fundamental theorem of Galois theory" - and call it GFT for short. The standard formulation of GFT includes the following assertions about a finite Galois extension E/K with the Galois group G = Gal(E/K): GFT1: The opposite lattice of subextensions of E/K is isomorphic to the lattice of subgroups of G; under this isomorphism a subextension F/K corresponds to the subgroup Gal(E/F) = {g in G: ga = a for all a in F}, and therefore a subgroup H in G corresponds to {a in E: ga = a for all g in H}. GFT2: A subextension F/K of E/K is normal (equivalently, Galois) if and only if its corresponding subgroup Gal(E/F) is normal, and if this is the case, then Gal(F/K) is canonically isomorphic to the quotient group. Moreover, every K-homomorphism of subextensions of E/K extends to a K-automorphism of E. Unfortunately even today all books in Algebra give only this kind of formulation. I think actually the right name for it is not "standard" but "prehistoric" - since more than 40 years ago Chevalley and Grothendieck understood that it is a straightforward consequence of the following simple and nice formulation: Grothendieck's GFT restricted: The category of subextensions of E/K (with morphisms all K-homomorphisms) is equivalent to the category of transitive G-sets, where E/K and G are as above. Moreover, one does not really want what I called "restricted", and then the right formulation becomes: Grothendieck's GFT: The category of K-algebras split over E/K is equivalent to the category of finite G-sets. Here a K-algebra A is said to be split over E/K if its tensor product over K with E is isomorphic to the Cartesian product of a finite number of copies of E; note that A is split over E/K if and only if it is itself isomorphic to the Cartesian product of a finite number of subextensions of E/K. There are many theorems similar or more general then this, proved by Chevalley and Grothendieck themselves, by A. R. Magid, M. Barr and R. Diaconescu, and others. In 1984 I realized that there is a purely categorical formulation and a purely categorical proof - before that the topos-theoretic level was considered as the most general, although there was no topos-theoretic extension of Magid's theorem. And what I call now Categorical Galois theory - let us say CGT for short - has important examples very far from Grothendieck and topos theory. One of them, studied in joint work with G. M. Kelly is of what we called generalized central extensions in universal algebra. CGT actually uses very simple category theory (pullbacks, adjoint functors, monadicity, internal category actions), but after many attempts I found it very difficult to explain it to "non-category-theorists" - I would say, simply because most of them do not believe that General Category theory can have non-trivial applications! A further generalization of CGT to so-called variable categories was developed in joint work with D. Schumacher and R. H. Street. In some sense it includes Street's theory of torsors, Joyal - Tierney's theorem on geometric morphisms of toposes, and Tannaka duality. George Janelidze From rrosebru@mta.ca Fri Feb 16 13:49:16 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1GHJGk31009 for categories-list; Fri, 16 Feb 2001 13:19:16 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Fri, 16 Feb 2001 08:43:56 -0500 (EST) From: Peter Freyd Message-Id: <200102161343.f1GDhuo24693@saul.cis.upenn.edu> To: categories@mta.ca Subject: categories: Which is the simplest example? Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 44 I said that the simplest example of a category with pullbacks but not products is the discrete category with two objects. Come to think of it, any category with exactly two morphisms is an example. From rrosebru@mta.ca Sat Feb 17 15:04:29 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1HIU7u14568 for categories-list; Sat, 17 Feb 2001 14:30:07 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Authentication-Warning: beta.namesys.com: god set sender to NikitaDanilov@Yahoo.COM using -f From: Danilov Nikita MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-ID: <14989.28420.518530.766264@beta.namesys.com> Date: Fri, 16 Feb 2001 21:18:44 +0300 To: categories@mta.ca Subject: categories: Re: Which is the simplest example? In-Reply-To: <200102161343.f1GDhuo24693@saul.cis.upenn.edu> References: <200102161343.f1GDhuo24693@saul.cis.upenn.edu> X-Mailer: VM 6.89 under 21.1 (patch 8) "Bryce Canyon" XEmacs Lucid Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 45 Peter Freyd writes: > I said that the simplest example of a category with pullbacks but not > products is the discrete category with two objects. Come to think of > it, any category with exactly two morphisms is an example. Initial question was If a category C has pullbacs no terminal object, then has C finite product? Now, think of empty category (one without objects and morphisms): (*) it doesn't contain terminal object (*) it does have pullbacks of all pairs of objects (because there are none) (*) it doesn't contain all finite products (as it doesn't contain limit of empty diagram---terminal object) Now, simplify _this_ counter-example. :) Actually, if terminal object is considered as product of zero multipliers (as it's usually does), then initial question contains answer in itself. Nikita. From rrosebru@mta.ca Sat Feb 17 15:04:37 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1HIRhw14559 for categories-list; Sat, 17 Feb 2001 14:27:43 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Fri, 16 Feb 2001 14:11:33 +0100 (MET) From: Elke Tetzner Message-Id: <200102161311.OAA28531@titus.informatik.uni-rostock.de> To: categories@mta.ca Subject: categories: job: Postdoctoral Position Cc: tetzner@informatik.uni-rostock.de, wlohmann@informatik.uni-rostock.de X-Sun-Charset: US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 46 Please pass on to interested Post doctorants. Apologies for multiple copies. ---------------------------------------------------------------------------- New Postdoctoral Position (DEADLINE 1 April 2001) Department of Computer Science, University of Rostock Germany Vacancy for an assistant professor Responsibilities: education and research in programming languages and compiler construction research in implementation techniques in different areas of computer science cooperation in academic self-administration Qualifications: PhD in computer science interests in programming languages and compiler constructions priorities: declarative programming, attribute grammars and applications, semantics of programming languages and compiler construction further interests: aspect-oriented programming, specification technics, real-time programming and other educational skills a good knowledge of german language engagement: 1st April 2001 (permanent) salary: BAT-O Ib (special in Germany), full time further information: Prof. Dr. G. Riedewald (http://www.informatik.uni-rostock.de/FB/Praktik/psuet/griedew.html) Dr. W. Mahrhold phone: (+49 381)498-3397 Qualified women are emphatically invited for application. Severely handicapped person with same qualification is prefered. From rrosebru@mta.ca Sat Feb 17 15:04:43 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1HITHu17102 for categories-list; Sat, 17 Feb 2001 14:29:17 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Fri, 16 Feb 2001 17:30:54 GMT From: Marta Z Kwiatkowska Message-Id: <200102161730.RAA13390@chip.cs.bham.ac.uk> To: categories@mta.ca Subject: categories: job: Research studentships available at Birmingham X-Sun-Charset: US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 47 [Please forward to anyone interested. Apologies for multiple mailing.] ========================================================================= The University of Birmingham School of Computer Science Research studentships in Computer Science and Artificial Intelligence ========================================================================= The School of Computer Science has research strengths in the areas of Theoretical Computer Science, Artificial Intelligence and Cognitive Science, and Software Engineering. The Theory of Computation group concentrates on the development of logics and semantics for programming languages. The overall aim is to provide intuitive conceptual tools for the everyday practice of programming. Within this framework, the activities range from abstract mathematics to issues of implementation and software development. For an overview of past research activities of the group, including funded research projects and publications, see the URL: http://www.cs.bham.ac.uk/research/research.html Current academic and research members of the Theory group are: Dr Martin Escardo Dr Carsten Fuhrman Dr Mateja Jamnik Professor Achim Jung Dr Manfred Kerber Dr Marta Kwiatkowska Dr Gethin Norman Professor Uday Reddy Dr Eike Ritter Dr Mark Ryan Dr Jeremy Sproston Dr Hayo Thielecke There are also 11 PhD students associated with the group, of the total of 40 in the School. Possible topics for research include, but are not restricted to: Verification and model checking Feature interactions in reactive systems Abstraction and decomposition in model checking Verification of probabilistic systems (theory and implementation) Verification of real-time systems (theory and implementation) Probabilistic and stochastic calculi Semantics for concurrency Temporal and modal logics Domain theory Topological methods in computer science Exact real number computation Constructive mathematics Extensions to the relational database model (theory and implementation) Parametricity and foundations of data abstraction Semantics and formal methods for OO programming Continuations and control Semantics and reasoning for computational effects Categorical models of programming languages Linear logic, type theory and corresponding categorical semantics Linear abstract machines Agent-based mathematical reasoning Machine-assisted reasoning Diagrammatic reasoning Theorem proving and proof planning Applicants must have or be about to gain at least an upper second class honours degree or an overseas equivalent in Computer Science or a related subject. Successful applicants will be offerred an opportunity to join The Midlands Graduate School in the Foundations of Computing Science, a recent initiative between the Universities of Birmingham, Leicester, Nottingham and Warwick aiming to provide broader educational experience for doctoral students. For more information see URL: http://www.cs.nott.ac.uk/MGS/ The School has a number of studentships and teaching assistantships. The teaching assistantships are available to UK and EU applicants while a range of studentships are available to all applicants. Details are given in: http://www.cs.bham.ac.uk/~pjh/prospectus/funding/research.html The School's research student prospectus and application form are available from: http://www.cs.bham.ac.uk/studentinfo/form_mailer.html Informal enquiries can be directed to any member of the group (see URL http://www.cs.bham.ac.uk/system/auto-gen/staff.html http://www.cs.bham.ac.uk for contact information), or *in the first instance* to Marta Kwiatkowska Email M.Z.Kwiatkowska@cs.bham.ac.uk Tel +44 121 414 7264 FAX +44 121 414 4281 ========================================================================= From rrosebru@mta.ca Mon Feb 19 11:52:43 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1JF3Ij21534 for categories-list; Mon, 19 Feb 2001 11:03:18 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: Konstantinos Tourlas MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-ID: <14993.2133.143263.322554@april.dcs.ed.ac.uk> Date: Mon, 19 Feb 2001 11:49:41 +0000 (GMT) To: categories@mta.ca Subject: categories: Re: statecharts and categories In-Reply-To: <3A8A8F1F.E49648BE@info.unine.ch> References: <3A8A8F1F.E49648BE@info.unine.ch> X-Mailer: VM 6.72 under 21.1 (patch 14) "Cuyahoga Valley" XEmacs Lucid Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 48 Amiguet Matthieu writes: > I'm wondering if there has been any work in formalizing statecharts [1] > in categorical terms. Currently John Power and myself are involved in providing an algebraic foundation (in category-theoretic terms) of higraphs, the "visual formalism" [1] which underlie Statecharts. On this basis, we are adding more features in an attempt to study a large subset of the Statecharts language. In brief, our approach is to regard higraphs as graphs in Poset, the category of partially ordered sets and monotone functions. Our main results so far pertain to operations underpinning the semantics of Statecharts and the concept of zooming described by Harel in [1]. Technical details will appear soon in my web page: http://www.dcs.ed.ac.uk/~kxt More generally, our interests are in studying domain-specific programming and specification languages which have a strong diagrammatic component. Statecharts present a most interesting case for study, as they contain a multitude of interacting diagrammatic features and support practically important operations such as zooming. Part of our objective is to evaluate how the different features blend together, in an attempt to research good design principles for the kind of diagrammatic languages used in computing. > If not, do you know of an other algebraic > description of this specification language? I know of a paper by Uselton and Smolka, but which does not use categories: "A Compositional Semantics for Statecharts using Labeled Transition Systems", by A. Uselton, S. Smolka, available online at: http://www.di.ufpe.br/~lrl/statecharts_js.html > Also, it seems to me that the operationnal semantic STATEMATE of > Statecharts as described in [2] is very coalgebraic in nature. Did > anybody write something about this? I'm afraid I do not know of any such work. However, your view of STATEMATE semantics seems most interesting. Please feel free to email me (kxt@dcs.ed.ac.uk) or John (ajp@dcs.ed.ac.uk) for a more detailed techical discussion on this subject or any of the above. [1] D. Harel, On Visual Formalisms, Communications of the ACM, 31(5), 1988. -- Konstantinos Tourlas Tel. : 0131-650-5162 Rm 1404, JCMB, The University of Edinburgh, e-mail : kxt@dcs.ed.ac.uk King's Buildings, Edinburgh, EH9 3JZ UK From rrosebru@mta.ca Mon Feb 19 11:54:24 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1JF2IP22661 for categories-list; Mon, 19 Feb 2001 11:02:18 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: Eduardo Dubuc Message-Id: <200102182338.SAA11720@cogito.math.uqam.ca> Subject: categories: Re: Unlabeled graphs To: categories@mta.ca Date: Sun, 18 Feb 2001 18:38:52 -0500 (EST) In-Reply-To: <4.1.20010215151228.009f0500@mail.oberlin.net> from "Charles Wells" at Feb 15, 2001 03:31:44 PM X-Mailer: ELM [version 2.5 PL2] MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 49 this is in reply to Charles Wells, I quote in between ' " ' " Major point: Any way you store an unlabeled graph in a computer will involve a memory location for each node, and so introduces a labeling, indeed a total ordering, on the nodes. However, a high level language with pointers such as C can be used to describe the structure without any names being given explicitly. The structure head will point to a node, which will have a pointer to another node, etc, and the program text will not mention all the nodes directly. For the purpose of computing with the graph, you can have the program traverse the nodes without naming them. This is a commonly used technique. (There will have to be pointer structures for the edges with pointers to the two nodes each is incident on.) When the program is compiled, the nodes are made to correspond to memory locations but the locations are hidden from the user. It seems to me that this preserves the psychology of a drawing with no labels on the nodes. " quite wright, i agree that the technique you describe "preserves the psychology of a drawing with no labels on the nodes. ". i had no thought about the pointer technique !!! but then, try to put an unlabeled graph in a computer using assembler languge ! is what i should have said ! " You can respond that each node has an implicit label, essentially an integer, which is the number of pointers you have to dereference to get to the node. But that is just like saying that in the drawing of the graph on a piece of paper, each node has an implicit label, namely its location on the paper. If you allow implicit labels like this the drawing has them and so does the graph in the computer. If you don't allow them then neither has labels. Let me forestall someone bringing up a red herring: The coordinates of the node on the paper depend on an arbitrary choice of coordinate system, unlike the number of pointers you need to get to the stored node in the computer. This argument, if someone makes it, is based on a misreading of what I said. I said each node is labeled by its location on the paper. I didn't say the coordinates of the location. The location itself is the label. " the final conclusion of your arguing : " The location itself is the label" means that there is no such a thing as an unlabeled graph. interesting . . . but what about permutation of the labels ? en fin ! we should perhaps leave this problem to the philosophers, if they would be able to understand it e.d. From rrosebru@mta.ca Mon Feb 19 13:31:36 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1JGgOq18610 for categories-list; Mon, 19 Feb 2001 12:42:24 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: Thomas Streicher Message-Id: <200102191546.QAA14750@fb04209.mathematik.tu-darmstadt.de> Subject: categories: toposes vs. sets - another aspect To: categories@mta.ca Date: Mon, 19 Feb 2001 16:46:40 +0100 (CET) X-Mailer: ELM [version 2.4ME+ PL66 (25)] Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 50 I want to take up the discussion on ``toposes vs. sets'' from another point of view. Over the years a few questions have accumulated and I'd be interested in the opinion of the experts. As Bill Lawvere has pointed out in his reply to the original question there are several meanings in which one can understand the relation ``toposes vs. set theory''. One such distinction is static sets vs. variable sets and one can hardly deny that the latter are of enormous importance for understanding modern mathematics from a conceptual point of view. That's probably what most categorists have in mind when they defend categories as superior to traditional set theory. Another argument probably is that the official language of axiomatic set theory is most inconvenient for actual formalisation of mathematics. One knows that in principle one always can eliminate function symbols in favour of relation symbols but that leads to an explosion of length of formulas and ends in something fairly uncomprehensible.Thus, categorists and also quite a few logicians are in favour of formal systems based function application and predication instead of using just one single relation \epsilon besides equality because function application and predication are the basic constitutents of actual mathematical statements and, moreover, appear most naturally from the categorical notion of topos. In the end this amounts to the point of view that HAH (Higher Order Arithmetic), the internal language of the free topos with NNO, is the formal system which is most suitable for formalizing mathematics (if one wants to embark on such an endeavour at all). Well, but there are some reasons why HAH may be considered as non-sufficient at least from a logical point of view. As Zermelo-Fraenkel set theory ZF(C) and, actually, already Zermelo's Set Theory Z(C) prove the consistency of HAH and accordingly they are non-conservative extensions of HAH. Well, one might argue that this lack of conservativity only affects "meta-statements" and not ``real mathematical statements''. Even hard boiled set theorists would admit that "99% of modern mathematics can be formalised in HAH" (such a statement for Zermelo's Z(C) instead of HAH can be found e.g. in Kunen's monograph on set theory). However, there do exists natural mathematical statements which can be formulated in the language of HAH but proved only in ZF though they are fairly different in character from ``meta-statements''. A typical such example is Borel Determinacy (BD) saying that for every Borel set X in Baire space either player or opponent has a winning strategy for the game G_X where in each step each player plays a natural number and in the end (after \omega steps) player has won if and only if the resulting sequence of numbers lies in X. >From this point of view I think one can hardly insist that HAH is the ultima ratio as it prevents us from proving meaningful statements which can be formulated in HAH. Of course, one might still have in mind an open-ended axiomatization of HAH where one adopts an axiom, as e.g. BD, whenever convenient. This seems to be the attitude for example in SDG where one postulates by need axioms ensuring the existence of particular functions such as cos and sin instead of constructing them via some series. It seems to me that such an attitude is absolutely ok as long as one is interested only in appropriate formalism for expressing mathematical facts and not in the strength of axiomatizations. However, if one wants to arrive at a formal system which allows one to derive (in principle) "all current mathematics" then I think one has to accept that HAH is not satisfactory simply because it is too weak. On the other hand it still is the case that traditional syntax of ZF is not very convenient as a formalisation of mathematical practice. Therefore, it might be worthwhile to look for formal systems of a type-theoretic character equiconsistent to ZF(C) and including ZF(C) via translation. Well, such a language is available, namely the so-called "Calculus of Inductive Constructions" an impredicative type theory with an infinite hierarchy of universes. This is described in Werner, Benjamin Sets in types, types in sets. Theoretical aspects of computer software (Sendai, 1997), 530--546, Lecture Notes in Comput. Sci., 1281, Springer, Berlin, 1997. ftp://ftp.inria.fr/INRIA/Projects/coq/Benjamin.Werner/zfc.ps.gz where one also can find (sketches of) proofs of the meta-theoretic properties mentioned above. The reason why systems like the "Calculus of Inductive Constructions" are as strong as ZF(C) is that they allow one to define FAMILIES of TYPES by structural recursion. which is precisely what the set theoretic axiom of replacement is good for. However, type theoretic language does bring this to the point more clearly than the set-theoretic axiom of replacement which is often used in mathematical practice to formulate the image of a function f : A -> B namely as { f(a) | a \in A} which certainly has to be considered as sort of an overkill because this can be formulated in HAH as well. The real strength of the axiom of replacement is used when defining `images of functions without a codomain' as e.g. families of sets indexed by some inductive type (e.g. an ordinal). The very purpose of type-theoretic universes is to provide a codomain for such `functions without codomain'. According to these observations I get the impression that what topos logic is missing is a concept of universe which allows one to define by recursion not only families of objects but also families of types. I want to conclude my remarks with a pointer to a recent paper by Alex Simpson on Solving Domain Equations in Models of Intuitionistic Set Theory (to be found at http://www.dcs.ed.ac.uk/home/als/Research/rde.ps.gz) where in the last paragraph of section 5 (p.12) he gives a counterexample to the claim that in a topos satisfying the usual axioms of SDT (Synthetic Domain Theory) one always can solve domain equations. The reason is that the topos considered there doesn't allow one to construct certain N-indexed families. (This is a style of argument well-known from the usual proofs in set theory showing that Z(C) is weaker than ZF(C)!) I hope that it has got clear from my formulations that I am not at all ``anti-category''. However, I always found it most confusing when in some texts on toposes I read the statement that the logic of toposes coincides with intuitionistic set theory. I think that most classically trained logicians get immediately puzzled by such statements because they know very well that set theory is stronger than type theory and, therefore, feel sort of repelled by such oversimplifying statements. Moreover, during the 90ies there have been developed fascinating categorical accounts of constructive set theory by Joyal, Moerdijk, Simpson, Butz and Palmgren. I think it would be an interesting question to clarify the relation between this account and the one by universes. Thomas Streicher From rrosebru@mta.ca Mon Feb 19 13:31:36 2001 -0400 X-UIDL: 5TJ!!*nQ!!oYl"!N!("! Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1JGgOq18610 for categories-list; Mon, 19 Feb 2001 12:42:24 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: Thomas Streicher Message-Id: <200102191546.QAA14750@fb04209.mathematik.tu-darmstadt.de> Subject: categories: toposes vs. sets - another aspect To: categories@mta.ca Date: Mon, 19 Feb 2001 16:46:40 +0100 (CET) X-Mailer: ELM [version 2.4ME+ PL66 (25)] Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 51 I want to take up the discussion on ``toposes vs. sets'' from another point of view. Over the years a few questions have accumulated and I'd be interested in the opinion of the experts. As Bill Lawvere has pointed out in his reply to the original question there are several meanings in which one can understand the relation ``toposes vs. set theory''. One such distinction is static sets vs. variable sets and one can hardly deny that the latter are of enormous importance for understanding modern mathematics from a conceptual point of view. That's probably what most categorists have in mind when they defend categories as superior to traditional set theory. Another argument probably is that the official language of axiomatic set theory is most inconvenient for actual formalisation of mathematics. One knows that in principle one always can eliminate function symbols in favour of relation symbols but that leads to an explosion of length of formulas and ends in something fairly uncomprehensible.Thus, categorists and also quite a few logicians are in favour of formal systems based function application and predication instead of using just one single relation \epsilon besides equality because function application and predication are the basic constitutents of actual mathematical statements and, moreover, appear most naturally from the categorical notion of topos. In the end this amounts to the point of view that HAH (Higher Order Arithmetic), the internal language of the free topos with NNO, is the formal system which is most suitable for formalizing mathematics (if one wants to embark on such an endeavour at all). Well, but there are some reasons why HAH may be considered as non-sufficient at least from a logical point of view. As Zermelo-Fraenkel set theory ZF(C) and, actually, already Zermelo's Set Theory Z(C) prove the consistency of HAH and accordingly they are non-conservative extensions of HAH. Well, one might argue that this lack of conservativity only affects "meta-statements" and not ``real mathematical statements''. Even hard boiled set theorists would admit that "99% of modern mathematics can be formalised in HAH" (such a statement for Zermelo's Z(C) instead of HAH can be found e.g. in Kunen's monograph on set theory). However, there do exists natural mathematical statements which can be formulated in the language of HAH but proved only in ZF though they are fairly different in character from ``meta-statements''. A typical such example is Borel Determinacy (BD) saying that for every Borel set X in Baire space either player or opponent has a winning strategy for the game G_X where in each step each player plays a natural number and in the end (after \omega steps) player has won if and only if the resulting sequence of numbers lies in X. >From this point of view I think one can hardly insist that HAH is the ultima ratio as it prevents us from proving meaningful statements which can be formulated in HAH. Of course, one might still have in mind an open-ended axiomatization of HAH where one adopts an axiom, as e.g. BD, whenever convenient. This seems to be the attitude for example in SDG where one postulates by need axioms ensuring the existence of particular functions such as cos and sin instead of constructing them via some series. It seems to me that such an attitude is absolutely ok as long as one is interested only in appropriate formalism for expressing mathematical facts and not in the strength of axiomatizations. However, if one wants to arrive at a formal system which allows one to derive (in principle) "all current mathematics" then I think one has to accept that HAH is not satisfactory simply because it is too weak. On the other hand it still is the case that traditional syntax of ZF is not very convenient as a formalisation of mathematical practice. Therefore, it might be worthwhile to look for formal systems of a type-theoretic character equiconsistent to ZF(C) and including ZF(C) via translation. Well, such a language is available, namely the so-called "Calculus of Inductive Constructions" an impredicative type theory with an infinite hierarchy of universes. This is described in Werner, Benjamin Sets in types, types in sets. Theoretical aspects of computer software (Sendai, 1997), 530--546, Lecture Notes in Comput. Sci., 1281, Springer, Berlin, 1997. ftp://ftp.inria.fr/INRIA/Projects/coq/Benjamin.Werner/zfc.ps.gz where one also can find (sketches of) proofs of the meta-theoretic properties mentioned above. The reason why systems like the "Calculus of Inductive Constructions" are as strong as ZF(C) is that they allow one to define FAMILIES of TYPES by structural recursion. which is precisely what the set theoretic axiom of replacement is good for. However, type theoretic language does bring this to the point more clearly than the set-theoretic axiom of replacement which is often used in mathematical practice to formulate the image of a function f : A -> B namely as { f(a) | a \in A} which certainly has to be considered as sort of an overkill because this can be formulated in HAH as well. The real strength of the axiom of replacement is used when defining `images of functions without a codomain' as e.g. families of sets indexed by some inductive type (e.g. an ordinal). The very purpose of type-theoretic universes is to provide a codomain for such `functions without codomain'. According to these observations I get the impression that what topos logic is missing is a concept of universe which allows one to define by recursion not only families of objects but also families of types. I want to conclude my remarks with a pointer to a recent paper by Alex Simpson on Solving Domain Equations in Models of Intuitionistic Set Theory (to be found at http://www.dcs.ed.ac.uk/home/als/Research/rde.ps.gz) where in the last paragraph of section 5 (p.12) he gives a counterexample to the claim that in a topos satisfying the usual axioms of SDT (Synthetic Domain Theory) one always can solve domain equations. The reason is that the topos considered there doesn't allow one to construct certain N-indexed families. (This is a style of argument well-known from the usual proofs in set theory showing that Z(C) is weaker than ZF(C)!) I hope that it has got clear from my formulations that I am not at all ``anti-category''. However, I always found it most confusing when in some texts on toposes I read the statement that the logic of toposes coincides with intuitionistic set theory. I think that most classically trained logicians get immediately puzzled by such statements because they know very well that set theory is stronger than type theory and, therefore, feel sort of repelled by such oversimplifying statements. Moreover, during the 90ies there have been developed fascinating categorical accounts of constructive set theory by Joyal, Moerdijk, Simpson, Butz and Palmgren. I think it would be an interesting question to clarify the relation between this account and the one by universes. Thomas Streicher From rrosebru@mta.ca Tue Feb 20 20:36:47 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1KNtGj16031 for categories-list; Tue, 20 Feb 2001 19:55:16 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Authentication-Warning: triples.math.mcgill.ca: barr owned process doing -bs Date: Tue, 20 Feb 2001 10:58:23 -0500 (EST) From: Michael Barr X-Sender: barr@triples.math.mcgill.ca To: Categories list Subject: categories: Jon Beck's thesis Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 52 Does anyone have a copy of Jon Beck's thesis? I have received a request from a Georgian mathematician (the editor and founder of Homology, Homotopy and Applications) who has no access to foreign exchange for a copy. I have looked and I do not have one, although I must have once. Actually, I don't have a copy of my own thesis (and they have disappeared from the Penn library). Michael From rrosebru@mta.ca Tue Feb 20 20:37:03 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1KNvIR14958 for categories-list; Tue, 20 Feb 2001 19:57:18 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: 21 Feb 2001 00:48:20 -0800 Message-ID: <918077649csiddiqi@qmny.cup.org> From: Cathy Siddiqi Subject: categories: Book Announcement: Galois Theories To: X-Mailer: QuickMail Pro 2.1 (Mac) X-Priority: 3 MIME-Version: 1.0 Reply-To: Cathy Siddiqi Content-Type: text/plain; charset="US-Ascii" Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by mailserv.mta.ca id f1KHmRb13400 Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 53 I would like to post the following annoucement for your category theorists. Galois Theories by Francis Borceux and George Janeldize Starting from the classical finite-dimensional Galois theory of fields, this book develops Galois theory in a much more general context. The authors first formalize the categorical context in which a general Galois theorem holds, and then give applications to Galois theory for commutative rings, central extensions of groups, the topological theory of covering maps and a Galois theorem for toposes. The book is a hardback, 360 pages, and costs $74.95 (50.00 in UK). For more information about the book, or to order a copy, please visit www.cambridge.org. Please let me know if you need additional information from me Thanks, Cathy -- Cathy Siddiqi Marketing Associate Cambridge University Press 40 West 20th Street New York, NY 10011 212-924-3900 x323 212-691-3239 fax From rrosebru@mta.ca Fri Feb 23 12:39:37 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1NFmSI24702 for categories-list; Fri, 23 Feb 2001 11:48:28 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Thu, 22 Feb 2001 02:06:54 GMT From: Mark D Ryan Message-Id: <200102220206.CAA24424@gromit.cs.bham.ac.uk> To: categories@mta.ca Subject: categories: job: Research job in model checking application Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 54 [apologies for multi-post] Job opportunity * Model checking * flexible balance of theory/applications, to suit applicant * good research environment * informal enquiries welcome THE UNIVERSITY OF BIRMINGHAM SCHOOL OF COMPUTER SCIENCE Postdoctoral Research Fellow Applications are invited for a Postdoctoral Research Fellow to work on the project `The Feature Construct in Programming and Specification Languages', funded by EPSRC and British Telecom, coordinated by Dr. Mark Ryan and Dr. Marta Kwiatkowska. Applicants should have a PhD in Computer Science and ideally have knowledge of one or more of the following areas: model checking, temporal logic, and/or program semantics. The successful applicant may be expected to contribute to teaching in the School up to a maximum of two hours per week on average. More information about the project, the research group and the School can be obtained from the URLs: www.cs.bham.ac.uk/~mdr/fc www.cs.bham.ac.uk The starting salary will be up to 19,482 pounds per year. The post is for three years from 1 April 2001 or as soon as possible thereafter. Application forms and further particulars available from: The Director of Personnel Services The University of Birmingham Edgbaston, Birmingham, B15 2TT tel: + 44 (0)121 414 6486 (24 hours) email: h.h.luong@bham.ac.uk Application forms are available from the WWW, at www.bham.ac.uk/personnel/app.htm Please quote reference S35522/01. The closing date for applications is Friday 9th March 2001. Late applications will be considered if the selection process has not advanced too far. Informal enquiries are welcome, and should be addressed to: Mark Ryan, tel: +44 (0)121 414 7361, email: M.D.Ryan@cs.bham.ac.uk. The University of Birmingham is working towards equal opportunities. ------- end ------- From rrosebru@mta.ca Wed Feb 28 11:51:52 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1SEuV300644 for categories-list; Wed, 28 Feb 2001 10:56:31 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Tue, 27 Feb 2001 08:37:54 GMT From: Mark D Ryan Message-Id: <200102270837.IAA27286@gromit.cs.bham.ac.uk> To: catgeries2mta.cak Subject: categories: job: Postdoc available Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 55 [apologies for multi-post] Dear Colleague, I would be very grateful if you would forward this email to finishing or recently-finished PhD students. The University of Birmingham, UK, has a post-doctoral position to offer involving Applications of formal logic, in particular temporal logic, to problems in telecommunication systems. The job would suit someone with a PhD in formal methods or logic, who is interested in developing and applying verification techniques in a setting of industrial relevance and importance. We offer a good research environment, and the job can be moulded to suit your preference in terms of theory vs applications. Informal enquiries welcome. ===== THE UNIVERSITY OF BIRMINGHAM SCHOOL OF COMPUTER SCIENCE Postdoctoral Research Fellow Applications are invited for a Postdoctoral Research Fellow to work on the project `The Feature Construct in Programming and Specification Languages', funded by EPSRC and British Telecom, coordinated by Dr. Mark Ryan and Dr. Marta Kwiatkowska. Applicants should have a PhD in Computer Science and ideally have some knowledge of one or more of the following areas: model checking, temporal logic, and/or program semantics. The successful applicant may be expected to contribute to teaching in the School up to a maximum of two hours per week on average. More information about the project, the research group and the School can be obtained from the URLs: www.cs.bham.ac.uk/~mdr/fc www.cs.bham.ac.uk The starting salary will be up to 19,482 pounds per year. The post is for three years from 1 April 2001 or as soon as possible thereafter. Application forms and further particulars available from: The Director of Personnel Services The University of Birmingham Edgbaston, Birmingham, B15 2TT tel: + 44 (0)121 414 6486 (24 hours) email: h.h.luong@bham.ac.uk Application forms are available from the WWW, at www.bham.ac.uk/personnel/app.htm Please quote reference S35522/01. The closing date for applications is Monday 19th March 2001. Late applications will be considered if the selection process has not advanced too far. Informal enquiries are welcome, and should be addressed to: Mark Ryan, tel: +44 (0)121 414 7361, email: M.D.Ryan@cs.bham.ac.uk. The University of Birmingham is working towards equal opportunities. ------- end ------- From rrosebru@mta.ca Wed Feb 28 12:17:46 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1SFdfo10111 for categories-list; Wed, 28 Feb 2001 11:39:41 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Authentication-Warning: sirppi.helsinki.fi: ess_lli owned process doing -bs Date: Tue, 27 Feb 2001 14:46:33 +0200 (EET) From: Ahti Pietarinen To: categories@mta.ca Subject: categories: CALL FOR REGISTRATION: ESSLLI 2001 (Helsinki, Finland) Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from QUOTED-PRINTABLE to 8bit by mailserv.mta.ca id f1RDGGb06656 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 56 - Apologies for multiple copies - If you want to receive detailed information including the ESSLLI 2001 poster please send us (esslli@helsinki.fi) your complete address. !!!!!!!!!!!!!!!!!!!!!!!!!! CALL FOR REGISTRATION !!!!!!!!!!!!!!!!!!!!!!!! 13th European Summer School in Logic, Language and Information ESSLLI 2001 University of Helsinki FINLAND August 13-24, 2001 http://www.helsinki.fi/esslli ** Early registration deadline: 30 April 2001 ** GENERAL INFORMATION The 13th European Summer School in Logic, Language and Information (ESSLLI'01) will take place at the University of Helsinki, Helsinki, Finland, during two weeks in August, from August 13 until 24. The ESSLLI Summer Schools are organised under the auspices of FoLLI (http://www.folli.uva.nl), the European Association for Logic, Language and Information. The main focus of the European Summer Schools is the interface between linguistics, logic and computation. Foundational, introductory and advanced courses, workshops and special events cover a wide variety of topics within six areas of interest: * Logic * Language * Computation * Logic and Language * Logic and Computation * Language and Computation The number of courses offered is over 50. Previous summer schools have been highly successful, attracting around 500 students from Europe and elsewhere. The school has developed into an important meeting place and forum for discussion for students, researchers and IT professionals interested in the interdisciplinary study of Logic, Language and Information. In addition to courses, workshops and evening lectures there will be a Student Session and a social program. COURSE PROGRAM The full scientific program can be found at our home page. Evening Lectures are given by * Edward L. Keenan "Spinoza Lecture" (UCLA) * Yannis Moschovakis "Vienna Circle Lecture" (UCLA) * Keith Devlin (Saint Mary's College, California) * Jaakko Hintikka (Boston & Helsinki) * Bonnie Webber (Edinburgh) WORKSHOPS There are currently several Calls for Workshop Papers. Please visit our home page for detailed information. TRAVEL AND LOCAL INFORMATION By plane to Helsinki airport and then a 30-minute nonstop coach or taxi service to the main railway station. From the railway station 5-minute walk to the university. A gateway between East and West, the city of Helsinki (population 1M) is the capital of Finland and one of the nine European Cities of Culture for the millennium. It is located at the warm and sunny south coast of Finland, within an easy reach from the main airports worldwide, or inside Europe by car or regular train services, or using the ferry services operating within the Baltic region. The scientific program of ESSLLI'01 will be held in the University Main Building, located on the University city campus at the very centre of Helsinki. The accommodation will be arranged at the University Summer Hotel close to the city campus. The accommodation includes sauna and breakfast. REGISTRATION ESSLLI 2001 is now open for registration. The registration fee for students is just ECU 190, for scholars ECU 350, and for industrial affiliates ECU 600. Please visit our home page for the on-line registration form and detailed instructions. ** Early registration deadline: 30 April 2001 ** All participants will get a letter of invitation to facilitate the procedure of getting a visa. GRANTS There will be a limited number of grants available, to partially support travel, registration and accommodation for ESSLLI'01. Instructions for grant applications are found at our home page. ** Deadline for grant applications: 31 May 2001 ** SPEACIAL EVENTS During ESSLLI, special "Finnish for Foreigners" language courses will be organised, as well as various excursions and other social events. Helsinki Summer School (http://summerschool.helsinki.fi) will offer special deals for ESSLLI participants who want to choose some of their courses and earn credits. SATELLITE EVENTS The Association for the Mathematics of Language will stage its annual meeting (MoL7) in conjunction with ESSLLI'01 in Helsinki, in the weekend preceding ESSLLI in August 10-12, and the affiliated Formal Grammar Conference will be held in conjunction with the Mathematics of Language Conference. ESSLLI participants are entitled to reduced registration fees. PROGRAM COMMITTEE Marcus Kracht (Chair) Jouko Väänänen (Logic) Bonnie Webber (Language) Claude Kirchner (Computation) Michael Moortgat (Logic and Language) Steffen Hölldobler (Computation and Logic) Claire Gardent (Language and Computation) CONTACT ADDRESSES Please visit ESSLLI'01 Home Page http://www.helsinki.fi/esslli for updated information concerning the scientific program, registration fees and procedures, grants, accommodation, satellite events, and other practical information. For further enquiries concerning ESSLLI'01, please contact the Organising Committee at , or write to ESSLLI 2001 Secretariat C/o Department of Philosophy P.O. Box 24 00014 Helsinki University Finland ESSLLI'01 is organised by the Department of Philosophy (coordinator), the Department of Mathematics, the Department of General Linguistics, and the Department of Computer Science at the University of Helsinki. ORGANISING COMMITTEE Gabriel Sandu (Chair, Philosophy) Jouko Väänänen (Mathematics) Fred Karlsson (General Linguistics) Ilkka Niiniluoto (Philosophy) Martti Tienari (Computer Science) Ahti Pietarinen (Philosophy, secretariat) ================================================================================ From rrosebru@mta.ca Wed Feb 28 12:20:09 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1SFmMA11068 for categories-list; Wed, 28 Feb 2001 11:48:22 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <004501c09f90$cedeaa60$be35183f@cpu> From: "zdiskin" To: "Categories" Subject: categories: Re: Mike Healy's question about AI and math Date: Sun, 25 Feb 2001 17:09:40 -0800 MIME-Version: 1.0 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 57 The discussion around the question in Re:above is expired but it seems not too much was said that might be directly related to problems in the applied domains in question and, thus, be really understood and appreciated by the corresponding part of the audience. Bill Lawvere is of course right in his << strong advice to actually learn some category theory, rather than resting content with slinging back and forth ill-defined epithets like "set theory", "contingency", etc >> but still there are no King's ways in math, and learning CT, as any other rich math discipline, needs efforts and time. Well, efforts and time is not a problem for students but a working specialist will reasonably require a certain motivation and justification for investing his resources into CT-studies. No doubts, the best justification is a host of examples of real successful applications ("success stories"), and in a discussion in this list in 1997 few were described. However, the NCDoms (Newly Created Domains as Lawvere called them) is an enormous territory and a few discrete example in particular areas do not set enough motivation/justification for the entire region. What is needed is a representative net of examples but still we have no it. So, for a while, a discrete set of new examples, and substantial conceptual / theoretical considerations too, would not be useless and a few were presented in the discussion. I'm afraid however that for a non-CT-part of the audience the arguments may seem far too general and/or too abstract, and we again come to the same issue at the beginning of the posting... There is a general problem of applying math to engineering domains and, correspondingly, of interaction between mathematicians and engineers. The former must respect a lot of formal details (in order to exist, the construction has to be formally consistent) and hence must go into the depth of consistent formalization. The latter must respect a lot of obstacles of the real world (to exist, the construction has to work) and hence must go into the width of functioning in the real world. Amalgamation of math depth with engineering width is a non-trivial task that needs working out a spacious array of details (every mathematician who ever tried to work in an industrial environment knows it) but at the end you have some kind of 3D vision beneficial for the both sides. (This general opposition "depth vs. width" in the case of "Math vs. NSDs" has some quite concrete technical aspects, see below). In these terms, an overall picture appeared in the discussion so far is somewhat like a discrete collection of bore-pits (well, they are connected at a depth, but it's hardly visible from the surface). To get a presentation more relevant for NCDs, I've tried to write a text integrating these pits into something wider ("a foundation pit" :). That is, I've tried (i) to trace some of the lines appeared in the discussion and add a bit of engineering width to them, (ii) to integrate them into an observable picture, (iii) to make some details a bit more understandable for the "foreign" part of the audience (and probably annoying for the "native" part so that my head is on the two platters simultaneously), and finally (iv), to explain something for myself. The resulting text turned out very bulky and can be found on http://www.cs.kuleuven.ac.be/~frank/Diskin.ps (thanks to Frank Piessens for hospitality). Below is a brief summary of the text and the table of contents to look thru before starting, or not starting, the tour. Regards, --Zinovy Diskin BRIEF SUMMARY (I) OBSERVATION. In many newly created domains (NCDs) they deal with a stuff in much similar to that managed in mathematics. Like a mathematician, an NCD-specialist deals with design (definition), presentation and reasoning about structures modeling a piece of reality (material, informational, "computeral") in an abstract way, suppressing some details (irrelevant for the model) and explicating others (important but often residing in intuition / default assumptions and therefore implicit). Hence, to look for a suitable math framework(s) for NCDs, one should look at *meta*mathematics -- a part of mathematics aimed at modeling mathematics by mathematical means. (II) OBSERVATION. Category theory (CT) is, in essence, a consistent *meta*mathematical framework where relations, manipulations and transformations of / between math structures are considered in an abstract and precise way. In a sense, CT is a discipline and framework for mathematical structure engineering. It is abstract enough to provide an extreme flexibility and simultaneously concrete enough to discover CT- structures in applications in a quite immediate way. In addition, this framework is essentially algebraic (and in some precise sense too), well structured itself and hence is quite manageable and effective. (III) It follows from (I) and (II) that CT appears to be a good candidate for an integral math framework, and effective machinery too, for applications in NCDs. Of course, in each particular context suitable CT-patterns should be found and adjusted, and their match with NCDs-structures to be managed should be checked. An example (rough sketch) of such an activity for the case of software engineering is presented below. (IV) OBSERVATION: CT vs. SE (software engineering in a wide sense including business modeling and knowledge representation). It appears that some of major mechanisms invented (and implemented!) in SE to manage the complexity of structures involved -- object orientation, set orientation, graphic notations, multi-level system architectures -- are based on ideas very close to those developed in CT. To wit: object and set orientations together appear as a kind of SE-realization of the arrow thinking underlying CT, and graph-based syntax and multi-level organization of the CT-stuff are evident and speak for themselves. (V) SPECULATION. While the theoretical part of the NCDs community is discussing whether CT is relevant or not, the (software) engineering part is already using categorical, in essence, ideas in a implicit way. Nothing surprising: the same goal of building a framework where complex structures (computational and specificational) could be managed in a systematic and effective way has led engineers and mathematicians to close results. Making this implicit partnership explicit would benefit the both sides. END OF SUMMARY CT as a mathematical framework for software engineering, AI, cognitive science, and other newly created domains (NCDoms). http://www.cs.kuleuven.ac.be/~frank/Diskin.ps Table of contents. 1 About NCDoms. 1.1 NCDoms as mathematics. 1.2. Peculiarities of NCDoms' mathematics: length and width vs. depth. 1.3 SE's mechanisms to manage complex structures. 2 CT in a SE-View: Object-Oriented, Setwise And Graph-Based Mathematics with Multi-Level Architecture. 2.1 CT as OO-language: Math structures via arrows. 2.2 CT as a setwise language. Toposes. 2.3 CT as a graphic language. Sketches. 2.4 CT as a language for multi-level specifying architectures. 3 CT vs. SE. 3.1 Graphic notation and sketches. 3.2 CT as an integral specification framework. 3.3 Three final remarks. REFERENCES Appendix O. MODELING AND MATHEMATICAL MODELING O.1 General schema of modeling (something by something) O.2 Examples O.3 Some peculiarities of applying math to natural sciences O.3.1. Semi-formal deduction. O.3.2 "Unreasonable effectiveness". Appendix A. MECHANISMS FOR MANAGING NCDs' STRUCTURES A.1 Object orientation. A.2 Set orientation. A.3 Graphic syntax of specification languages: Notational Babylon A.4 Multi - level specification architectures. A.5 The challenge of integration. Appendix B. ABOUT METAMATHEMATICS B.0 "Business structure" of meta-mathematics. B.1 Metamath I: CatST vs. FrmST. B.2 Metamath II: CatLogic vs. Tarskian MetaMath. B.3 Metamath III: abstract mathematical structures engineering. B.A(ppendix): Bourbakian way of setting math structures and CT. Appendix C. CT vs. SE: EXAMPLES C.1 Relations: Categorical vs. Element-oriented treatment C.2. Semantic database theory: Toposes and Database design. C.3 Whether schema integration is an associative operation? From rrosebru@mta.ca Wed Feb 28 12:20:29 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f1SFn7S02270 for categories-list; Wed, 28 Feb 2001 11:49:07 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Tue, 27 Feb 2001 22:31:30 +0000 (GMT) From: paolo torrini X-Sender: paolot@csun-gps To: categories@mta.ca Subject: categories: connectedness/intuitionistic logic Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 58 I am looking for information about work on the representation of topological properties (esp. connectedness) using intuitionistic logic. I presently know about definitions of connectedness in "Sheaves and Logic" (Fourman-Scott 79) and "Formal spaces" (Fourman-Grayson 82). I would be interested in knowing whether there has been more work, esp. whether there is something that may have some relation with discrete geometry. Thank you for your help, Paolo -- Paolo Torrini School of Computing Leeds 0113 233 5684