From cat-dist@mta.ca Fri Mar 1 16:22:52 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA14859; Fri, 1 Mar 1996 16:22:51 -0400 Date: Fri, 1 Mar 1996 16:21:50 -0400 (AST) From: categories To: categories Subject: 3rd WoLLIC'96 - Final Call Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Fri, 1 Mar 1996 18:54:34 GMT From: Ruy de Queiroz Deadline: MARCH 8TH 1996 FINAL Call for Contributions 3rd Workshop on Logic, Language, Information and Computation (WoLLIC'96) May 8-10, 1996 Salvador (Bahia), Brazil The `3rd Workshop on Logic, Language, Information and Computation' (WoLLIC'96) will be held in Salvador, Bahia (Brazil), from the 8th to the 10th May 1996. Contributions are invited in the form of two-page (600 words) abstracts in all areas related to logic, language, information and computation, including: pure logical systems, proof theory, model theory, type theory, category theory, constructive mathematics, lambda and combinatorial calculi, program logic and program semantics, nonclassical logics, nonmonotonic logic, logic and language, discourse representation, logic and artificial intelligence, automated deduction, foundations of logic programming, logic and computation, and logic engineering. There will be a number of guest speakers, including: Andreas Blass (Ann Arbor), Nachum Dershowitz (Urbana-Champaign), J. Michael Dunn (Indiana), Peter G"ardenfors (Lund), Jeroen Groenendijk (Amsterdam), Wilfrid Hodges (London), Roger Maddux (Ames, Iowa), Andrew Pitts (Cambridge), Amir Pnueli (Rehovot), Michael Smyth (London). WoLLIC'96 is part of a larger biennial event in computer science being held in the campus of the Federal University of Bahia from the 6th to the 10th of May 1996: the `6th SEMINFO' (6th Informatics Week). The 6th SEMINFO will involve parallel sessions, tutorials, mini-courses, as well as the XI Brazilian Conference on Mathematical Logic (EBL'96), and a Workshop on Distributed Systems (WoSiD'96). The 3rd WoLLIC'96 is under the official auspices of the Interest Group in Pure and Applied Logics (IGPL) and The European Association for Logic, Language and Information (FoLLI). Abstracts will be published in the Journal of the IGPL (ISSN 0945-9103) (up to now produced and distributed by Imperial College, London, and Max-Planck-Institut, Saarbruecken, but soon to be distributed by Oxford University Press) as part of the meeting report. Selected contributed papers will be invited for submission (in full version) to a special issue of the Journal (http://www.mpi-sb.mpg.de/igpl/Journal). The 3rd WoLLIC'96 is also sponsored by the Association for Symbolic Logic (ASL). Submission: Two-page abstracts, preferably by e-mail to *** wollic96@di.ufpe.br *** must be RECEIVED by MARCH 8th, 1996 by the Chair of the Organising Committee. Authors will be notified of acceptance by April 8th, 1996. The location: Salvador, Capital of the Bahia state, the first European settlement of Portuguese America and the first Capital of Brazil, is where all the most important colonial buildings were constructed: churches, convents, palaces, forts and many other monuments. Part of the city historical center has been safekept by UNESCO since 1985. Five hundred years of blending Native American, Portuguese, and African influences have left a rich culture to its people, whichcan be felt on its music, food, and mysticism. Salvador is located on the northeastern coast of Brazil and the sun shines year round with the average temperature of 25 degrees Celsius. It is surrounded by palm trees and beaches with warm water. City population is around 2.5 million and life style is quite relaxed. Programme Committee: W. A. Carnielli (UNICAMP, Campinas), M. Costa (EMBRAPA, Brasilia), V. de Paiva (Cambridge Univ., UK), R. de Queiroz (UFPE, Recife), A. Haeberer (PUC, Rio), T. Pequeno (UFC, Fortaleza), L. C. Pereira (PUC, Rio), K. Segerberg (Uppsala Univ., Sweden), A. M. Sette (UNICAMP, Campinas), P. Veloso (PUC, Rio). Organising Committee: H. Benatti (UFPE), L. S. Baptista (UFPE), A. Duran (UFBA), T. Monteiro (UFPE), A. G. de Oliveira (UFBA), N. Riccio (UFBA). For further information, contact the Chair of Organising Committee: R. de Queiroz, Departamento de Informatica, Universidade Federal de Pernambuco (UFPE) em Recife, Caixa Postal 7851, Recife, PE 50732-970, Brazil, e-mail: ruy@di.ufpe.br, tel.: +55 81 271 8430, fax: +55 81 271 8438. (Co-Chair: T. Pequeno, LIA, UFC, tarcisio@lia.ufc.br, fax +55 85 288 9845) Web homepage: http://www.di.ufpe.br/simposios/wollic.html -------------------------------------------------------------------------------- 3rd Workshop on Logic, Language, Information and Computation (WoLLIC'96) May 8-10, 1996 Salvador (Bahia), Brazil TITLE AND ABSTRACT OF INVITED TALKS -------------------------------------------------------------------------------- Some Semantical Aspects of Linear Logic Andreas Blass I plan to discuss some of the semantics that have been proposed for Girard's linear logic, including different forms of game semantics, de Paiva's Dialectica-like semantics, and perhaps others. I shall describe how these semantics are related to each other, to the intuitions that underlie linear logic, and to some other parts of mathematics. -------------------------------------------------------------------------------- Trees, Ordinals, and Termination Nachum Dershowitz Trees are a natural representation for countable ordinals. We describe natural well-founded orderings of finite binary trees, finite ordered (plane-planted) trees, rational binary trees (finite or infinite binary trees with only finitely many different subtrees), and "supertrees" (trees whose nodes may themselves be supertrees). We relate these orderings to existing ordinal notations, and illustrate their use in various colorful termination problems. -------------------------------------------------------------------------------- Proof Theory and Semantics for Structurally Free Logics J. Michael Dunn This work is joint with R. K. Meyer. The idea is to provide a semantics and proof theory for combinatory logic, extended by a "residual" (implication). The semantics is a variation on the ternary relational (Meyer-Routley) semantics for relevance logic, as extended by Meyer-Routley, and more recently others for the (fusion-implication) fragment of the relevance logic B+ (closely related to the non-associative Lambek calculus). The proof-theory extends some semi-published work of Meyer in the 1970's (following a suggestion of Belnap), wherein Gentzen's structural rules for the intuitionistic implication calculus were replacewith explicit introduction of a combinator licensing the combinatorial manipulations. This is extended so as to make combinators "first-class objects," and a cut theorem can still be proven. This is called "structurally free logic" in analogy with "logic freed of existential presppositions." In this original "free logic," existence presuppositions are made explicit, just as in "combinatorially free logic" combinatorial moves are made explicit by adding the combinators that license them as explicit premisses in the antecedent of the sequent. This allows various logics to be translated into the combinatorially free logic. It also expands the meaning of "substructural logics" beyond the usual ones obtained by considering various subsets of Gentzen's structural rules (plus say associativity). There will also be results about adding other connectives (conjunction and disjunction), with or without distribution. -------------------------------------------------------------------------------- Three Levels of Knowledge Representation Peter G"ardenfors Within logic, AI and early cognitive science, almost all research concerning knowledge representation has been based on symbolic (propositional) models. In the 80's connectionist models became popular as an alternative way of modelling knowledge. I propose that also a third type of knowledge representation based on conceptual models should be studied. In particular, I will discuss conceptual models based on geometrical and topological notions and show their relevance for concept revision and for non-monotonic aspects of concepts. I will argue that conceptual models of knowledge can be seen as a bridge between symbolic and connectionist representations. The three kinds of knowledge representation models should thus not be seen as competitors, but rather as complementary models suitable for different modelling tasks. -------------------------------------------------------------------------------- Update Semantics Meets Discourse Jeroen Groenendijk In update semantics the meaning of a sentence is identified with its potential to change the information state of an agent. In the recursive semantic definition, truth conditions are replaced by update effects. Central notions are not truth and validity, but consistency, support, and coherence. Although update semantics is advertized as addressing itself to the interpretation of discourse, rather than being limited to single sentences, it usually goes no further than interpreting sequences of utterances of a single agent. In the present talk I will study the interpretation of multi-agent discourse. The object language we investigate is the language of modal predicate logic. We concentrate on the role of (epistemic) modalities in discourse, and on anaphoric relations (binding of variables) across utterances of different speakers. The aim is to characterize notions of logical consistency and coherence of multi-agent discourse. The paper reports on joint work with Martin Stokhof and Frank Veltman. -------------------------------------------------------------------------------- TBA Wilfrid Hodges -------------------------------------------------------------------------------- Sequential Algebras Roger Maddux The sequential calculus of von Karger and Hoare ("Sequential Calculus", Inform. Process. Lett. 53(1995), 123-130) is designed for reasoning about sequential phenomena, dynamic or temporal logic, concurrent or reactive systems, and so on. Unlike the classical calculus of relations, it has no operation for forming the converse of a relation. Sequential algebras are defined by von Karger so that sequential calculus turns out to be the equational theory of the class of sequential algebras. A standard example of a sequential algebra is the powerset of a partial ordering (a transitive reflexive relation) with Boolean operations (union, etc.), composition, and two operations that are conjugate to composition. Nonstandard examples arise by relativizing nonrepresentable relation algebras to elements that are transitive and reflexive. The incompleteness and non-finite-axiomatizability of the sequential calculus will be presented through some new constructions of sequential algebras and relation algebras. These algebras improve on previous examples in certain interesting respects and give yet another proof that the classical calculus of relations is not finitely axiomatizable. This is joint work with Peter Jipsen (Cape Town). -------------------------------------------------------------------------------- "Logical" Relations between Syntax and Semantics Andrew Pitts In this talk I will discuss some recent developments in the mathematical foundations of programming language semantics. On the one hand, Freyd's categorical analysis of recursively defined domains has led to simplified techniques for denotational semantics involving such domains. On the other hand, work of Abramsky, Howe and others on co-inductively defined "applicative bisimulations" has provided quite powerful theories of equivalence of functional programs, defined in terms of their operational semantics. I will tie together some of these developments by describing a certain "logical relation" between the syntax and semantics of lambda calculus which can be used to derive extensionality and continuity properties of operationally-defined program equivalences from corresponding properties of recursively defined domains. The logical relation itself goes back to Plotkin. What is new is the recognition that the relation has a certain property (a "universal property", in category-theoretic terms) which both characterises it uniquely and permits the operationally-based properties to be derived. -------------------------------------------------------------------------------- Verifying Timed and Hybrid Systems Amir Pnueli The talk presents new computational models for real-time and hybrid systems. For timed systems we propose a model called A Clocked Transition System (CTSS). The CTSS model is a development of our previous Timed Transition model, where some of the changes are inspired by the model of Timed Automata. The new models lead to a simpler style of temporal specification and verification, requiring no extension of the temporal language. We present verification rules for proving safety properties (including time-bounded response properties) of clocked transition systems, and separate rules for proving (time-unbounded) response properties. To justify the need for time-unbounded resopnse rules, we present a characteristic example of a timed system which terminates but no apriori bound on its termination time can be given All rules are associated with verification diagrams. The verification of RESPONSE properties requires adjustments of the proof rules developed for untimed systems, reflecting the fact that progress in the real time systems is ensured by the progress of time and not by fairness. The style of the verification rules is very close to the verification style of untimed systems which allows the (re)use of verification methods and tools, developed for untimed reactive systems, for proving properties of real-time systems. We conclude with the presentation of a branching-time based approach for verifying that an arbitrary given CTSS is Non-Zeno. This is joint work with Y. Kesten and Z. Manna. -------------------------------------------------------------------------------- TBA Michael Smyth -------------------------------------------------------------------------------- From cat-dist@mta.ca Mon Mar 4 22:51:27 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA29220; Mon, 4 Mar 1996 22:51:27 -0400 Date: Mon, 4 Mar 1996 22:49:46 -0400 (AST) From: categories To: categories Subject: GMK 96 Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Sun, 3 Mar 1996 13:22:14 +1000 From: Ross Street FINAL ANNOUNCEMENT ***** GMK 96 ***** A TWO-DAY SEMINAR IN HONOUR OF MAX KELLY Tuesday 12 and Wednesday 13 March 1996 VENUE The Refectory, The Holme Building, University of Sydney (The Holme Building is on the Parramatta Rd side of the University, to the west of the footbridge.) Coffee will be served in an adjacent room called the Withdrawing Room. DINNER On Tuesday evening, there will be a dinner held at the Art Gallery on the 5th Floor of the Wentworth Building, University of Sydney. (Wentworth Building is on City Rd) Please let Sonia Morr ( or 61-2-351-5809) know if you would like to attend. The charge is $40 per person. PROGRAM TUESDAY 12 MARCH 9:30 - 10:30 George Janelidze "Covering reflections" (joint work with G.M. Kelly) 10:30 - 11:00 Coffee 11:00 - 12:00 Peter Johnstone "A new proof that local operators form a Heyting algebra" 12:00 - 14:00 Lunch (not provided, but available nearby) 14:00 - 15:00 Andre Joyal "The free bicompletion of a category with applications I" 15:00 - 15:30 Coffee 15:30 - 16:30 Ross Street "Developments on monoidal and enriched categories" (joint work with Brian Day) 19:00 - ? Conference Dinner (see above) WEDNESDAY 13 MARCH 9:30 - 10:30 Bob Walters "The Todd-Coxeter Procedure" 10:30 - 11:00 Coffee 11:00 - 12:00 Andre Joyal "The free bicompletion of a category with applications II" 12:00 - 14:00 Lunch (not provided, but available nearby) 14:00 - 15:00 Gus Lehrer "Reflections concerning braids and representation theory" 15:00 - 15:30 Coffee 15:30 - 16:30 Max Kelly "New thoughts on a 2-category of equipments as codomain for such constructions as relE, spanE, parE, profE, and so on" (joint work with A. Carboni, D. Verity and R. Wood) ----------------------------------------------------------------------- Ross Street Bob Walters Mathematics Department School of Mathematics and Statistics Macquarie University University of Sydney NSW 2109 NSW 2006 Australia Australia Phone: -61-2-850-8921 Phone: -61-2-351-2966 Email: Email: Fax: -61-2-850-8114 Fax: -61-2-692-4534 From cat-dist@mta.ca Tue Mar 12 08:32:03 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA27067; Tue, 12 Mar 1996 08:32:02 -0400 Date: Tue, 12 Mar 1996 08:29:35 -0400 (AST) From: categories To: categories Subject: Re: Set membership <-> function composition Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Mon, 11 Mar 1996 17:07:55 -0400 (AST) From: Michael Barr Let me introduce my response by saying that although I was more-or-less familiar with Lawvere's thoughts on the subject, I had never thought too much about them until some years ago, more than 5, less than 10, when I found myself teaching a course in set theory. For the first time, I came to realize what a complex horror set membership really is. In every other type of mathematics I had ever studied, the objects were some kind of sets with some kind of structure and the arrows were the functions (or at worst equivalence classes of such) that preserved them. Mostly, the structure was given by operations, or at least partial operations, although Top was something of an exception, but even there, continuous maps are those that preserve ultrafilter convergence. But of course, Sets are an exception. Here are sets defined in terms of these elaborate epsilon trees and this structure is invariably ignored. It seemed to me intuitively, confirmed by Makkai, that the ONLY arrows between sets that actually preserved all that structure were inclusions of subsets. So that obvious category is just a poset. But of course the truth is that that epsilon structure is invariably ignored. So why is it taken as the basis of mathematics. Much better to simply define sets as the objects of a category and then an element is just a global section, or rather an equivalence class thereof. My whole experience with category theory convinces me that membership and the closely related idea of equality is an intrinsically obscure notion Or rather, not that it itself is obscure, but it obscures anything it touches. Like, the idea of embedding Z into Q by taking the eqivalence classes of fractions and then removing those that include a fraction of the form n/1 and replacing them by the corresponding integer. Yes, it can be done and we certainly want to say that Z is a subring of Q, but it is such a mess and so unnecessary. Some would say, but not I, that you should just work in your favorite topos. I take a platonic view that there really are sets, but membership and equality are not the simple concepts we think they are. In particular, I would like to say that a fraction is a pair of integers m/n, n > 0 and that m/n = p/q when mq = np. I don't know about pointers to the literature. Cheers, Mike From cat-dist@mta.ca Tue Mar 12 14:47:15 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA17419; Tue, 12 Mar 1996 14:47:14 -0400 Date: Tue, 12 Mar 1996 14:46:36 -0400 (AST) From: categories To: categories Subject: 61st PSSL Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Tue, 12 Mar 1996 18:26:31 --100 From: Enrico Vitale PSSL - PRELIMINARY ANNOUNCEMENT The 61st meeting of the PERIPATETIC SEMINAR ON SHEAVES AND LOGIC will be held in Dunkerque over the week-end of 8-9 june 1996. As usual, talks on category theory and related areas are welcomed. If you wish to attend it, please write to Enrico Vitale by e.mail, or by ordinary mail at the home-address below, specifying if you plan to give a talk. Information about hotel accomodation will be forwarded to you as soon as possible. Please, circulate this announcement among your collegues. Dominique Bourn Enrico Vitale Enrico VITALE Laboratoire LANGAL - Faculte de Sciences - Universite du Littoral 1 quai Freycinet - B.P. 5526 - 59379 Dunkerque - FRANCE tel. 0033-28237161 - fax. 0033-28237039 - e.mail vitale@lma.univ-littoral.fr home: 33 Bd. G. Pompidou - 59123 Bray-Dunes - FRANCE - tel. 0033-28265698 From cat-dist@mta.ca Tue Mar 12 14:47:17 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA17779; Tue, 12 Mar 1996 14:47:16 -0400 Date: Tue, 12 Mar 1996 14:45:55 -0400 (AST) From: categories To: categories Subject: Re: Set membership <-> function composition Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Tue, 12 Mar 1996 10:27:25 -0500 (EST) From: MTHISBEL@ubvms.cc.buffalo.edu On Mike Barr's comments. The bulk of them are right enough, though maybe it is not quite fair to complain that something designed as foundation for every- thing is awkward to work with. Like complaining that the tax code is full of qualifications and exceptions. But, what stirred me to respond is recognition of an old friend in < 0 and <> So would Saunders MacLane, sorry, Mac Lane. He gives the axioms in his 1948 invited address published as 'Duality for groups' in BullAMS 1950. The community has not taken up Saunders' axioms, can't think why. John Isbell From cat-dist@mta.ca Wed Mar 13 10:50:15 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA02616; Wed, 13 Mar 1996 10:50:14 -0400 Date: Wed, 13 Mar 1996 10:48:59 -0400 (AST) From: categories To: categories Subject: Re: Set membership <-> function composition Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Tue, 12 Mar 1996 17:11:35 -0500 From: Robert A. G. Seely Michael Barr's reply to this question was not entirely complete (IMHO), as he forgot to mention that he wrote a short paper some time (3 yrs) ago dealing with matters related to this. Those interested might want to download his paper, which can be obtained by ftp from triples.math.mcgill.ca in the directory pub/barr (look for variable.sets.*.Z, where * = dvi, tex, or ps). = rags = From cat-dist@mta.ca Wed Mar 13 10:51:11 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA02753; Wed, 13 Mar 1996 10:51:10 -0400 Date: Wed, 13 Mar 1996 10:50:22 -0400 (AST) From: categories To: categories Subject: rationals Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Tue, 12 Mar 1996 17:29:31 -0800 From: Vaughan Pratt From: MTHISBEL@ubvms.cc.buffalo.edu < 0 a nd <> So would Saunders MacLane, sorry, Mac Lane. He gives the axioms in hi s 1948 invited address published as 'Duality for groups' in BullAMS 1950. The community has not taken up Saunders' axioms, can't think why. I thought these were Weber's axioms. Lerhbuch der Algebra, 1895. The integers are likewise pairs m-n of natural numbers, with m-n = p-q when m+q = n+p. Natives of Ab are no doubt comfortable defining the integers as the tensor unit. But in Ab, ZZ = Z. Are people from Ab even aware that there are infinitely many integers? Can they even count? People from Set surely know a whole lot more about Ab than people from Ab know about Set. (By Ab I mean the closed category of Abelian groups, with all logic conducted internally, i.e. Hom:Ab\op x Ab -> Ab.) Vaughan From cat-dist@mta.ca Wed Mar 13 13:22:57 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA11537; Wed, 13 Mar 1996 13:22:57 -0400 Date: Wed, 13 Mar 1996 12:49:06 -0400 (AST) From: categories To: categories Subject: Re: Set membership <-> function composition Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Wed, 13 Mar 1996 10:29:57 -0500 From: Peter Freyd One may argue that formal set theory relates to topos theory in the way that untyped lambda calculus relates to the typed theory. If you think it's difficult to get a model of set theory out of a topos try to get a model of untyped lambda calculus out of a model for the typed theory. The semantics of core mathematics -- unlike the semantics of a programming language -- has never presented much of a problem. The perversity of formal set theory as a foundational language for mathematics has not been much in evidence for the simple reason that no mathematician has ever actually used it for his semantics. I am not saying here that the continuum hypothesis is perverse, or even questions about much larger cardinals. (For one thing they can be stated easily in a topos setting.) I am saying that formal set theory allows entirely perverse questions that have nothing to do with the semantics of mathematics. The actual elements used for a mathematical construction are never of interest. Imagine your reaction to an interruption at the beginning of a lecture on number theory, "Which construction of the natural numbers do you have in mind? Russell's or Van Neumann's?" My favorite example of the sort of perverse question one can ask if one were to take formal set theory seriously is "Does any simple group appear as a zero of the Riemann Zeta function?" From cat-dist@mta.ca Wed Mar 13 13:23:40 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA11520; Wed, 13 Mar 1996 13:23:40 -0400 Date: Wed, 13 Mar 1996 12:49:50 -0400 (AST) From: categories To: categories Subject: Re: rationals Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Wed, 13 Mar 1996 07:35:27 -0800 From: Vaughan Pratt We seem to be having mailer problems again, with caret being turned into escape. Peter Freyd's ASCII notation => for internal hom to the rescue: read But in Ab, Z^Z = Z. as But in Ab, Z=>Z = Z. Vaughan From cat-dist@mta.ca Wed Mar 13 16:30:11 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA28002; Wed, 13 Mar 1996 16:30:10 -0400 Date: Wed, 13 Mar 1996 16:28:38 -0400 (AST) From: categories To: categories Subject: Re: Set membership <-> function composition Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Wed, 13 Mar 1996 19:30:06 GMT From: Ralph Loader Hi, >The actual elements used for a mathematical construction are never of >interest. Imagine your reaction to an interruption at the beginning of It's perfectly feasible to imagine that in say, descriptive set theory, properties of certain structures could be shown by showing (1) they have a certain cardinality, (2) sets of such cardinality have epsilon trees with a certain property and (3) using epsilon induction over such epsilon trees to prove something about our original structures. [I don't know of any such instances; I'm not a descriptive set theorist.] Alternatively, what about Godel's constructible universe. This seems to be a mathematical construction, and the actual element relation seems to be not only of interest, but essential to the construction. >a lecture on number theory, "Which construction of the natural numbers >do you have in mind? Russell's or Van Neumann's?" My favorite example >of the sort of perverse question one can ask if one were to take >formal set theory seriously is "Does any simple group appear as a zero >of the Riemann Zeta function?" This is an interesting example. You state a question in mathematical English, and then criticise ZF for being able to express this question, while category theory cannot. One wonders what other questions stated in mathematical English---some of them perhaps perfectly sensible---can be stated in the language of ZF, but not in the language of category theory. I'd much rather that my formalisation of mathematics could state nonsensical things (consistency strength isn't an issue here), than to be living in the fear that my formalisation may be inadequate to express some sensible arguments. Two examples that I think are relevant to this debate. Category theorists are keen on statements to the effect that structures are defined by their universal properties. A typical book on topos theory may define an elementary topos as a category with finite limits and power objects. It then goes on to show that any topos has internal-homs. How? By defining the function space as a certain set of sets of ordered pairs... Let Nat(x) be the statement "x is a triple (omega,S,0) to which the Peano axioms apply". ZF |- "there exists x such that Nat(x)". This is sufficient to do arithmetic; after proving this single existential statement, one need never give a particular construction of the natural numbers again. Indeed, if one is really worried about these things, note that ZF+"Nat(omega)" (where omega is a new constant symbol) is conservative over ZF and then work in the latter theory, without ever fixing on a particular interpretation of ZF+"Nat(omega)" into ZF. Both category theory and set theory are amenable to working with mathematical structures by either explicit constructions or by uniquely characterising properites. In both category theory and set theory, we prove the existence of structures with certain uniquely characterising properties via explicit construction. Ralph. From cat-dist@mta.ca Wed Mar 13 16:55:09 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA25239; Wed, 13 Mar 1996 16:55:08 -0400 Date: Wed, 13 Mar 1996 16:54:29 -0400 (AST) From: categories To: categories Subject: Re: Set membership <-> function composition Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Wed, 13 Mar 1996 15:45:47 -0500 From: Michael Barr - - Date: Wed, 13 Mar 1996 10:29:57 -0500 - From: Peter Freyd - ................................. - - The actual elements used for a mathematical construction are never of - interest. Imagine your reaction to an interruption at the beginning of - a lecture on number theory, "Which construction of the natural numbers - do you have in mind? Russell's or Van Neumann's?" My favorite example - of the sort of perverse question one can ask if one were to take - formal set theory seriously is "Does any simple group appear as a zero - of the Riemann Zeta function?" - - My point exactly. The elements don't matter, so why should elementhood be taken as the fundamental relation of all of mathematics? Equality doesn't matter either, but equivalence relations do. From cat-dist@mta.ca Wed Mar 13 17:13:39 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA32124; Wed, 13 Mar 1996 17:13:39 -0400 Date: Wed, 13 Mar 1996 17:12:59 -0400 (AST) From: categories To: categories Subject: Re: Set membership <-> function composition Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Wed, 13 Mar 1996 15:54:44 -0500 From: Michael Barr - - Date: Wed, 13 Mar 1996 19:30:06 GMT - From: Ralph Loader - ............................ - - Category theorists are keen on statements to the effect that structures are - defined by their universal properties. A typical book on topos theory may - define an elementary topos as a category with finite limits and power - objects. It then goes on to show that any topos has internal-homs. How? - By defining the function space as a certain set of sets of ordered pairs... ................................ - - Ralph. - - Nonsense. How can a set of sets of ordered pairs be an object of a topos. In fact, there is at least one book that defines a topos as a category with finite limits and power objects and constructs the internal homs as a limit of two arrows between two power objects. The construction is hidden inside a cotriple, but that is what it amounts to. From cat-dist@mta.ca Thu Mar 14 10:25:32 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA13370; Thu, 14 Mar 1996 10:25:31 -0400 Date: Thu, 14 Mar 1996 10:24:35 -0400 (AST) From: categories To: categories Subject: Re: Set membership <-> function composition Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Wed, 13 Mar 1996 13:40:25 -0800 From: james dolan -This is an interesting example. You state a question in mathematical -English, and then criticise ZF for being able to express this question, -while category theory cannot. i at least am curious just what is this mathematical question you claim to have in mind which zf can express but which category theory can not. obviously it wasn't "Does any simple group appear as a zero of the Riemann Zeta function?" since that is mere gibberish and not a mathematical question at all. zf was being criticized for being unable to not express this non-question, and category theory was being praised for having the option to express "it" (should someone actually bother to give it a real meaning) or not. whatever was the real point that you were trying to argue might still be interesting to hear but it's hard to even know what that point might have been in light of the apparent misunderstanding you've exhibited here. From cat-dist@mta.ca Thu Mar 14 10:25:33 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA13534; Thu, 14 Mar 1996 10:25:32 -0400 Date: Thu, 14 Mar 1996 10:25:21 -0400 (AST) From: categories To: categories Subject: Re: Set membership <-> function composition Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Wed, 13 Mar 1996 13:45:19 -0800 From: Vaughan Pratt The semantics of core mathematics -- unlike the semantics of a programming language -- has never presented much of a problem. It would be interesting to hear a few mathematicians who *don't* work much in foundations comment on this. === Item A. The perversity of formal set theory as a foundational language for mathematics has not been much in evidence for the simple reason that no mathematician has ever actually used it for his semantics. Isn't this a bit strong? An awful lot of mathematicians are under the impression that their definitions are grounded in set theory. This has the enormous advantage for them that, if pressed as to whether their own mathematics is consistent, they can claim (a) that the definitions could be expanded all the way out to whatever fragment of ZF they're assuming if the auditors insist, and (b) that if their local framework is inconsistent, then the part of ZF they used (and a fortiori the whole of ZF) is itself inconsistent. "If I go down, I'm taking you with me" sort of thing, just like if we ever find a polytime recognizer for an NP-complete set. Being well-calibrated on the structure of ZF and which bits are at greater risk makes it a *lot* easier to organize one's mathematics to minimize the risk of consistency. Pretending there never was any risk of inconsistency in the first place is *very* well contradicted by the historical record, particularly in calculus. Today we have trustworthy infinitesimals, of a very elegant kind, thanks to nonstandard arithmetic. While one might *wish* that these had been discovered by categorical means, the actuality is that their discovery used very heavy doses of formal set theory. Whether we can do it today with less heavy doses is beside the historical point. Formal set theory evolved in response to consistency concerns, and today it engenders for many of us a strong sense of safety, implicit in our trust of our own tools, and explicit in actual products such as infinitesimals we can trust. === Item B. My favorite example of the sort of perverse question one can ask if one were to take formal set theory seriously is "Does any simple group appear as a zero of the Riemann Zeta function?" Item A argues that many of us *do* take formal set theory seriously. In this item I will argue that doing so does not force one into this sort of situation. Now there's nothing inconsistent about going inside a definition and asking implementation-specific questions. People do this all the time, in fact one might argue that mathematicians do it every one or two sentences. In any such visit to the inside of a definition, people seem to treat the occasion as though a tacit NDA (nondisclosure agreement) applied. Perhaps it shouldn't be so tacit. MATH NDA. When you step inside a definition, you agree to bring in only permitted imports. You agree furthermore that when you leave, you will take out only permitted exports. The usual definitions of "simple group" and "zero of the Riemann Zeta function" permit neither importing nor exporting the other concept. Your example enters both definitions at the one time, imports the other concept in each case, and exits each definition with illicit information, racking up a total of four NDA violations in a single exchange. Even if mathematicians don't stick this NDA to their doors, they know instinctively to use it, independently of whether their math is implemented with sets or categories. Violations of the NDA will get you funny looks. === A+B Now here's a *very* important point, it's why I separated the above two issues out as two items. Item B, the NDA protocol, does not conflict with Item A, the reliance on the consistency of ZF that many put their trust in. There is no more conflict here than there is between NDA's in business and the laws of physics. All an NDA does is *restrict* what things can be done, it does not break or even bend any law. If you don't stick to the NDA's, you may get funny looks, but consistency is not put at risk. If you add an unexplored axiom to ZFC you put consistency at serious risk *and* you get funny looks. All very analogous to violating business NDA's and breaking laws of physics. === Back to my original question. CAT is grounded in Set when you take the homfunctor to go to Set, as is standardly done. But the very notion of set is defined by membership; a set is determined by the truth values of membership of candidate elements of it. A choice to be made early on is whether the candidate elements of a given set themselves must form a set, the point of view encouraged by toposes where the very question of membership is a private business discussed only in power objects (a power breakfast comes to mind). The alternative is to allow the candidates to form a proper class, as in ZF, which will blithely tell *every* individual except 1 and 2 that they are not members of {1,2}, without any consideration of their feelings. The first choice does seem saner to me. However a lot of people think globally about membership and equality, and it seems like a lot of religious mumbo-jumbo to them not to be allowed to even *ask* whether two things are not equal when they don't live in the same neighborhood. So when I write about sets, can I safely adopt a "Boolean" style and say that the question "x \in {1,2,3}" (equivalently, "x=1 or x=2 or x=3") has only two answers, yes or no? Or should I do the mumbo-jumbo thing and clarify the ground-rules by explaining how the existence of neighborhoods creates at least one more possible answer? Or should I pretend there's no problem and think mumbo-jumbo even when I know my audience is thinking Boolean? I *hate* that third alternative, it seems so dishonest. But maybe dishonesty is the best policy in this situation... Vaughan Pratt From cat-dist@mta.ca Thu Mar 14 10:26:24 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA13643; Thu, 14 Mar 1996 10:26:23 -0400 Date: Thu, 14 Mar 1996 10:26:15 -0400 (AST) From: categories To: categories Subject: Re: Set membership <-> function composition Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Wed, 13 Mar 1996 16:53:30 -0500 From: Peter Freyd Ralph Loader writes: It's perfectly feasible to imagine that in say, descriptive set theory, properties of certain structures could be shown by showing (1) they have a certain cardinality, (2) sets of such cardinality have epsilon trees with a certain property and (3) using epsilon induction over such epsilon trees to prove something about our original structures. [I don't know of any such instances; I'm not a descriptive set theorist.] There are all sorts of near-by examples but they're not counterexamples to my assertion. The fact that any structure of a certain type is isomorphic to one with further special properties is a standard first-step. The most usual further property is the existence of a well-ordering. But there's no such example, nor will there ever be, in which one must use some property of the elements of every possible structure of the given type in order to prove a property of the structure. That's a tautology if the "property of the structure" in question is an isomorphism-invariant. Alternatively, what about Godel's constructible universe. This seems to be a mathematical construction, and the actual element relation seems to be not only of interest, but essential to the construction. I must agree that when making constructions in mathematical subjects in which the elements are the essence then one will use elements. About my example of the philosopher who asked the number theorist (I actually witnessed this) whether he was proving theorems about Russell's or Van Neumann's numbers led Ralph to reply: You state a question in mathematical English, and then criticize ZF for being able to express this question, while category theory cannot. One wonders what other questions stated in mathematical English---some of them perhaps perfectly sensible---can be stated in the language of ZF, but not in the language of category theory. In fact there are topos-theoretic analogues for Russell and Van Neumann, but not even a philosopher would be tempted to ask the analogue question. Besides the R and VN numbers one could ask the analogue question about the Lawvere and the Church numbers (in category theory, not in set theory). But one wouldn't. Anyway, I do have a counterexample to my own assertion. I think JH Conway gave us some examples of mathematical constructions in which the elements are the essence, to wit, his games and his numbers. Conway games can be described as the result of replacing the single epsilon of ZF with a pair of epsilons (for left and right "moves"). If one restricts attention to "impartial" games (any move legal for one player would have been legal for the other) then the two epsilons can be conflated and the subject conflates to ZF. From cat-dist@mta.ca Thu Mar 14 10:26:58 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA13725; Thu, 14 Mar 1996 10:26:58 -0400 Date: Thu, 14 Mar 1996 10:26:55 -0400 (AST) From: categories To: categories Subject: Re: Set membership <-> function composition Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Thu, 14 Mar 1996 09:38:34 +1100 (EST) From: peterj@maths.su.oz.au Peter Freyd's old question "Does any simple group appear as a zero of the Riemann Zeta funxtion?" reminds me of the pleasing fact that it contains what philosophers would call a "category mistake". Pleasing because it's precisely the sort of mistake you can't make if you're working in a category. Peter Johnstone From cat-dist@mta.ca Thu Mar 14 10:27:39 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA13835; Thu, 14 Mar 1996 10:27:38 -0400 Date: Thu, 14 Mar 1996 10:27:35 -0400 (AST) From: categories To: categories Subject: Re: Set membership <-> function composition Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Thu, 14 Mar 1996 01:25:06 -0800 From: Vaughan Pratt My original problem was what to do about the absolutely ghastly argument I complained about, showing that membership could be figured out in Set. I now have a solution, only a couple of whose 70 lines are needed to describe membership. The rest explicitly, arithmetically, and (except for infinite products) completely describes all the adjunctions of (a lightweight version of) the bicomplete topos Set. For starters, you need to accept Mike Barr's intuition that "the elements don't matter." If it bothers you that {2,4,17} is not "in" my version of Set, you aren't looking at it from Mike's perspective. It's tempting to make Set even lighter weight than I do here by constructing it as Skel(Set). But while this is technically feasible, it makes the definition of limits and colimits on infinite sets obscure, and also loses a property I'll mention below in connection with a nice observation of John Isbell. Instead I retrace what I imagine is a familiar path for set theorists, but from the categorical perspective. I take the objects to be simply the ordinals, each defined as the set of ordinals less than it, and the maps to be all functions (in the usual sense) between ordinals. (So for all cardinals alpha, this Set has only alpha many sets of cardinality less than alpha, which is what I mean by lightweight.) This may well have been already proposed before, since it is so simple and solves my problem so directly. But if so then why didn't someone bring it up as an answer to my question? The ordinals being a transitive class, membership i \in j coincides with (global) strict inclusion i \subset j, which as will be seen below is definable as the left "local" inclusion of i into i+(j-i). This is ten times shorter than the method I complained about (Goldblatt 12.4) for calculating membership in Set! Here are some features of this version of Set. I'll abbreviate \omega to \w, \eta to \i, \epsilon to \e. * The full subcategory consisting of the finite sets is skeletal. * Since every set is well-ordered, by definition, Choice holds. * Since i+j=k is uniquely solvable in j for i<=k (this can be seen informally by deleting the first i elements of k and taking j to be the order type of the residue), it follows that monus (nonnegative minus) can be defined, denoted k-i. (Note that i+j=k is not uniquely solvable in i, witness i+\w=\w which has all finite ordinals as solutions while i+\w=\w+1 has no solutions.) We also have ordinal ("integer") division i/j and remainder i%j, see below. * The *global* inclusion (assumed proper) of i into j is definable, namely as the "local" inclusion of i into i+(j-i) (meaning the first half of the unit of the adjunction defining +, at (i,j-i)), just when this is not the identity on i. (For j <= i, j-i = 0, making the local inclusion the identity.) The global inclusions make Set an irreflexive poset, identical to membership except that we do not normally speak of membership of x in y as a map, only as the truth of the binary relation of membership at the object pair (x,y). If for some crazy reason we want to represent the membership relation by maps in Set, the global inclusion maps are the obvious choice. * The isomorphism 1=>x = x is the identity 1_x, and similarly for the isos \rho: x*1 = x, \lambda: 1*x = x, and \alpha: (x*y)*z = x*(y*z) making Set a strict cartesian closed category. I wrote = rather than tilde to avoid a repeat of yesterday's screwup with caret, but in fact these are equalities in the strongest sense: they make \rho, \lambda, and \alpha all identity natural transformations. Isbell's argument in CTWM VII.1 shows that we can't *always* make \lambda,\rho,\alpha identities, even in a CCC like Skel(Set). In the present context Isbell's argument yields more, namely that any construction we use to further reduce Set from the ordinals to a skeletal category *must* weaken these identities to isos. What saves the day for ordinals is that when x,y,z are countably infinite, x*y and (x*y)*z get to be different infinite ordinals. Isbell's argument gives really nice insight into why set theorists find ordinals work better than cardinals: as cardinals, countable x*y and (x*y)*z have to be the *same* countable cardinal, ordinals create useful elbow room. (Without this category perspective, I don't know how to make a convincing case for ordinal arithmetic over cardinal, anyone know a noncategorical way?) * The inclusion of the rationals into the reals (as Dedekind cuts) is definable, but only as a local inclusion, not a global one, nor a monotone one with respect to the well-ordering of the reals. Set well orders the reals "randomly," and we get to probe around in the resulting well-ordering after the "big coin toss" and sniff out some (all?) aspects of its crazy choices. (Use the global inclusion of 1 into the reals to locate the "least" real "0", which can now be compared with the "real" additive identity of the reals, 0.0.) But because it depends on the coin toss it is not mathematics, just unrepeatable noise. * But this isn't to say that every uncountable ordinal looks random. The least uncountable ordinal \w_1 *is* ordered predictably and repeatably, and that order *is* genuinely mathematical (to believers in \w_1 anyway). There's presumably a lot more to say about Set defined this way, but this is way overlength already, so let me push on to describe the category Set itself. The description talks about 0 and successor early on; these can be understood either externally starting from an already constructed Set (less demanding pedagogically) or internally as a purely categorical definition of Set (in terms of constants 0,1,+ denoting initial and final objects and a coproduct), which will inevitably seem circular just like ZF seems circular. ====================Light Set---V.R. Pratt--3/13/96=========== I'll start from the class of von Neumann ordinals, each the set of all ordinals less than it (sorry, Mike), and define all small sums and products, (co)equalizers, and the classified subobjects. I'll follow the standard ordinal conventions for binary sum and product, which make 1+\w = \w < \w+1 and 2*\w = \w < \w*2. We need some auxiliary operations on ordinals. i/j = the least k satisfying i < j*(k+1) i%j = i - j*(i/j) (i modulo j) Exercises. i <= j*(i/j), i%j < j. Binary sums (for illustration). To form i+j, form j' by adding i to the *elements* of j (recursively), and take i+j to be i union j', with the evident inclusions. (This is not commutative in general, as noted earlier.) This generalizes to all small sums as follows. Given a family n_i of ordinals indexed by is such that i f_i(h) to be and the counit \e_k to be \n.n%k (*not* \n.n%I). Binary products (for illustration). Form i*j as the sum of j copies of i, with the evident projections. (Not commutative in general.) Infinite products are a well-known problem for ordinal arithmetic, starting with \w copies of 2. The problem is to well-order the continuum. Choice says only that a well-ordering exists, we can't determine one by the constructive methods that work on everything else in this note. We just do our best. Given a family n_i of ordinals indexed by in_i (the projections) such that for all x2, the associated subobject is the least j such that there exists a monotone injection g:j->i such that fg = 1!. Theorem: such a g:j->i exists and is unique, and is the pullback of 1:1->2 along f. The equalizer of f:i->j and g:i->j is the subobject of i corresponding to the predicate on i "f(x)=g(x)". Theorem: this exists and is unique. The coequalizer object k of f:i->j and g:i->j is the subobject of j whose characteristic function p:j->2 is the predicate "is the least representative in its block". The coequalizer h:j->k maps each element of j to the least representative of its block. Theorem: h exists and is unique. Vaughan Pratt From cat-dist@mta.ca Thu Mar 14 10:28:24 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA13931; Thu, 14 Mar 1996 10:28:23 -0400 Date: Thu, 14 Mar 1996 10:28:21 -0400 (AST) From: categories To: categories Subject: Re: Set membership <-> function composition Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Thu, 14 Mar 1996 11:43:20 +0000 From: Steve Vickers Ralph Loader writes: >I'd much rather that my formalisation of mathematics could state >nonsensical things (consistency strength isn't an issue here), than to be >living in the fear that my formalisation may be inadequate to express some >sensible arguments. I for one _do_ live in fear (not really ... more a sort of smug schadenfreude) that set theoretic formalisation is inadequate to express some sensible arguments. The nonsensical things in set theory seem to arise from a basic nonsensical postulate: that there is a single fundamental relation "element of" on the mathematical universe that is sufficient to determine the nature of every mathematical object. It's a tour de force of modern mathematics that so much has been accomplished using this postulate, but its essential unreasonableness should not be forgotten and it is therefore complacent to assume that it is adequate to express all sensible arguments. Let me give some examples. 1) The "element of" relation is absolutely _un_fundamental - this is part of the force of Freyd's example about simple groups. What are the elements of a real number? If you consider the real number to be a Dedekind section, then it is a pair of subsets of the rationals, Q, and hence its elements are whatever you think the elements of an ordered pair are. Or, equivalently, it can be represented as a subset of Qx2 (or Q x any doubleton {L,R}). Or, equivalently, a subset of QxQ, with (q,r) in x iff |q-x| < r (i.e. the real is identified with its neighbourhood filter of rational open balls). All these enable a real to be described as a set, but they give it completely different elements. In reality there is no single universal "element of" relation that describes the nature of everything, including the reals; instead, the reals are described by various relations with other specific objects. 2) Topology: Normally one thinks of open sets as being sets of points, but localic topology views points as being sets of opens (e.g. reals as neighbourhood filters above). There is obviously a fundamental relation of points being "in" opens, and localic arguments can be expressed quite reasonably using it. Set theoretic expression using "element of" completely obscures this. In other words, set theory prevents you from adequately expressing reasonable arguments. 3) Generic objects: Suppose we agree on a particular set theoretic representation, e.g. reals as Dedekind sections. What then is a _generic_ real, such as the x in f(x) = x^2? Set theory has to treat this as a mere hole where a specific real could be put, but it is quite reasonable to treat it as a real in its own right (so long as you don't use - e.g. - excluded middle to demand specific properties of it) and that's exactly what people do. What are its elements? One can still make sense of the idea that it is determined by its elements (using "generalized elements" and Kripke-Joyal semantics), but in doing so one must go far beyond classical set theory. 4) What about theories such as that of accessible categories, that, for set theoretic reasons, have to be liberally sprinkled with infinite cardinals? Doesn't this make you think that perhaps set theory is somehow obscuring simple ideas? To my mind, the evidence suggests that despite its undoubted successes, set theory is not right for mathematical foundations, and we should be looking for its replacement. It is easy to be bemused by the fact that all our mathematical upbringing presumes set theoretical foundations, but we should try to recognize its limitations and failures. Steve Vickers. From cat-dist@mta.ca Thu Mar 14 10:29:26 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA14049; Thu, 14 Mar 1996 10:29:26 -0400 Date: Thu, 14 Mar 1996 10:29:21 -0400 (AST) From: categories To: categories Subject: Re: Set membership <-> function composition Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Thu, 14 Mar 1996 12:24:37 GMT From: Ralph Loader cat-dist@mta.ca writes: >My point exactly. The elements don't matter, so why should >elementhood be taken as the fundamental relation of all >of mathematics? Equality doesn't matter either, but >equivalence relations do. Really? Try telling that to people who produce computer verified correctness proofs for communication protocols. I'm sure they'll be pleased to know that their proofs should undergo a very significant increase in size and obscurity to satisfy what appears to be little more than aesthetic prejudice. Equality matters in some contexts, it doesn't matter in others. In some logics equality is definable rather than explicit, in which case this point doesn't appear to make much sense. Trying to be perscriptive about this---or any other---foundational point seems to me about as useful as (and just as perverse as) perscriptive linguistics. Given the known relationships between e.g. topos theory, higher order logics and various set-theories, is arguing about which is the correct / best / most relevant foundations of mathematics really that different from arguing about whether the Russell naturals or the von Neumann naturals are the correct / best / most relevant natural numbers? [Of course, this is fairly independant from questions such as how to present the natural numbers] Ralph (who is quite pleased to be talking to someone who isn't a dogmatic platonist the-universe-is-a-model-of-ZF type). P.S. any sarcasm isn't intended to be personal. From cat-dist@mta.ca Thu Mar 14 10:30:10 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA14160; Thu, 14 Mar 1996 10:30:09 -0400 Date: Thu, 14 Mar 1996 10:30:05 -0400 (AST) From: categories To: categories Subject: Re: Set membership <-> function composition Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Thu, 14 Mar 1996 12:55:58 GMT From: Ralph Loader cat-dist@mta.ca writes: >- Category theorists are keen on statements to the effect that structures are >- defined by their universal properties. A typical book on topos theory may >- define an elementary topos as a category with finite limits and power >- objects. It then goes on to show that any topos has internal-homs. How? >- By defining the function space as a certain set of sets of ordered pairs... >Nonsense. How can a set of sets of ordered pairs be an object of a >topos. In fact, there is at least one book that defines a topos as >a category with finite limits and power objects and constructs the >internal homs as a limit of two arrows between two power objects. >The construction is hidden inside a cotriple, but that is what it >amounts to. My desire for a little irony got the better of my pedantic instincts. I'm well aware that the phrase "representative of a subobject of the power-object of a product" would have be more precise than the morally equivalent set-theoretic terminology. It doesn't effect the point that I was trying to make; that whether one defines certain things by explicit construction or via an axiomatisation is fairly independent of whether one prefers to work in a logical, categorical or set-theoretic foundation. Neither is this effected by the availability of alternative constructions. Of course, for some people, it would be a perfectly sensible point of view that topos theory is interesting precisely because of results to the effect that a couple of elementary constructs are sufficient to justify the fairly general use of set-theoretic notation, such as refering to a `set of sets of ordered pairs'. Ralph. From cat-dist@mta.ca Thu Mar 14 10:53:48 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA15605; Thu, 14 Mar 1996 10:53:47 -0400 Date: Thu, 14 Mar 1996 10:53:13 -0400 (AST) From: categories To: categories Subject: Re: Set membership <-> function composition Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Thu, 14 Mar 1996 09:28:40 -0500 From: Robert A. G. Seely >> Date: Wed, 13 Mar 1996 19:30:06 GMT >> From: Ralph Loader >> >> [ cuts ] >> >> This is an interesting example. You state a question in mathematical >> English, and then criticise ZF for being able to express this question, >> while category theory cannot. One wonders what other questions stated in >> mathematical English---some of them perhaps perfectly sensible---can be >> stated in the language of ZF, but not in the language of category theory. >> I'd much rather that my formalisation of mathematics could state >> nonsensical things (consistency strength isn't an issue here), than to be >> living in the fear that my formalisation may be inadequate to express some >> sensible arguments. >> >> [One] example that I think [is] relevant to this debate. >> >> Category theorists are keen on statements to the effect that structures are >> defined by their universal properties. A typical book on topos theory may >> define an elementary topos as a category with finite limits and power >> objects. It then goes on to show that any topos has internal-homs. How? >> By defining the function space as a certain set of sets of ordered pairs... >> This might be a little disingenuous - Of course, in any topos there will be a monic X=>Y --> P(XxY) , so via the "internal language" X=>Y may be seen as a certain set of sets of ordered pairs. But the point is that via the "internal language" you can (and indeed you may) argue about the structure of a topos in a very "set-like" manner. But of course you are not obliged to do so. So in a very real sense, your (first) example illustrates that your fear is unfounded. (Indeed, one can imagine a topos theorist pondering the matter of simple groups being zeros of the Riemann zeta function in suitable toposes; the point of Peter Freyd's observation was (I think) that a topos theorist without any taste is less likely to stumble upon this question than a set theorist without taste, who might well do so... due to the emphasis upon different fundamental notions in the two approaches.) = rags = From cat-dist@mta.ca Thu Mar 14 17:10:18 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA14222; Thu, 14 Mar 1996 17:10:17 -0400 Date: Thu, 14 Mar 1996 17:09:16 -0400 (AST) From: categories To: categories Subject: Re: Set membership <-> function composition Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Thu, 14 Mar 1996 10:08:42 -0500 (EST) From: Colin Mclarty Several contributors to this thread share Loader's confusion on a couple of points. For one, constructibility in set theory does have an isomorphism invariant meaning, as Mitchell showed in JPAA about 1975. Trivial changes make the definition work in any topos with natural number object. In fact, a good bit of work in set theory today is on finding isomorphism invariant consequences of V=L or related axioms (constructibility relative to some set). Elementhood is not essential. And Peter Freyd's question "Does any simple group appear as a zero of the Riemann Zeta function?" is not absolute nonsense in ZF or in category theory--it is only misleading as it makes a question of (arbitrarily definable) codings look like a question of complex analysis. In ZF the answer is: It depends which coding of groups and numbers you use--it is easy to make up codings where the answer is yes and just as easy to make them up where the answer is no. For what it is worth, the codings in common use all make the answer "no", since they make every group an ordered 3 or 4 tuple while they make a complex number an ordered pair of infinite sets. This is trivia. Now suppose we found some good relation representing groups as complex numbers, which was manageable to work with and for which we could show that some simple groups correspond to points which would falsify the Riemann hypothesis. Then mathematicians might well start asking whether some zero of the zeta function "is" a simple group--just as we now ask whether some given real number "is" rational (a question whose strict answer on most ZF codings is always "no"). And this question would be just as well expressed in category theory as in ZF. best regards, Colin From cat-dist@mta.ca Thu Mar 14 17:10:20 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA14253; Thu, 14 Mar 1996 17:10:20 -0400 Date: Thu, 14 Mar 1996 17:10:14 -0400 (AST) From: categories To: categories Subject: Re: Set membership <-> function composition Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Thu, 14 Mar 1996 10:40:33 -0500 From: Peter Freyd Vaughan writes: An awful lot of mathematicians are under the impression that their definitions are grounded in set theory. Note, please, that I was writing about _core_ mathematics. There's an aperture problem here. What do we take as the universe of "mathematicians"? If we stick to those parts of mathematics as described by the US National Science Foundation as "core mathematics" then I will stand by my statement. A semantics is unneeded. I must agree, of course, that there have been proofs in core mathematics that have used structures for which the semantics became questionable. Because of their technical nature (that is, because they were needed in proofs, not theorems) consistency arguments -- in lieu of clear semantics -- were acceptable. There's a reasonably clear historical argument in favor of ZF for purposes of such arguments. (One example: In what John Thompson described as his best work he proved that certain finite groups -- such as the Monster -- appear as the Galois groups of number fields; in his proof he used the existence of infinitely many automorphisms of the complex numbers. Whether or not your semantics allows more than two automorphisms of the complex numbers, there's no question that the consistency of ZFC implies that the groups in question do appear as the Galois groups of number fields.) From cat-dist@mta.ca Thu Mar 14 17:11:14 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA14435; Thu, 14 Mar 1996 17:11:13 -0400 Date: Thu, 14 Mar 1996 17:11:10 -0400 (AST) From: categories To: categories Subject: Orthogonality and toposes question. Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Thu, 14 Mar 1996 18:35:00 GMT From: Marcelo Fiore Below I consider a notion of orthogonality with respect to cones, generalising that of orthogonality with respect to maps and the sheaf condition for a cover in a Grothendieck topology: 1. We say that an object K is orthogonal to a cone D --> C whenever for every cone D --> K there exists a unique C --> K such that (D --> C --> K) = (D --> K). 2. For a category K and a class J of cones in K we define O(K,J) as the full subcategory of K consisting of all those objects orthogonal to every cone in J. My question is: Let A be a small category and write Psh A for the topos of presheaves on A. Is there a characterisation of the classes J of cones in A for which O(Psh A,J) is a topos? Comments and pointers to relevant literature are welcome. Many thanks, Marcelo. From cat-dist@mta.ca Thu Mar 14 17:12:01 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA14573; Thu, 14 Mar 1996 17:12:00 -0400 Date: Thu, 14 Mar 1996 17:11:56 -0400 (AST) From: categories To: categories Subject: Expressiveness of category theory and set-theory. Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Thu, 14 Mar 1996 20:59:55 GMT From: Ralph Loader cat-dist@mta.ca writes: >Date: Wed, 13 Mar 1996 13:40:25 -0800 >From: james dolan > >-This is an interesting example. You state a question in mathematical >-English, and then criticise ZF for being able to express this question, >-while category theory cannot. > > >i at least am curious just what is this mathematical question you >claim to have in mind which zf can express but which category theory >can not. obviously it wasn't "Does any simple group appear as a zero >of the Riemann Zeta function?" since that is mere gibberish and not a This question clearly is mathematical English, in the sense that it is in the English language, and uses mathematical jargon. It doesn't make sense. I wasn't arguing with that. Ruling out statements from being "mathematical" *merely* on the grounds that they offend your mathematical taste, quickly becomes disasterous. Especially when we're (implicitly) talking about a formalisation in a formal language such as that of first order set theory. Anyway, as a good example, take a set-theoretic proof of Borel determinancy. Can anyone give a reasonable category theoretic proof of Borel determinacy? [This is a result that Friedman showed is a theorem of ZF but not of Z, if my memory serves me correctly.] This could well suffice to answer my concerns w.r.t. the adequacy of category language, by showing how even arguments needing replacement can have category theoretic analogues. Ralph. P.S. My personal opinion on foundations is fairly agnostic, in case anyone mistakes my concerns with rejection of category theoretic foundations. From cat-dist@mta.ca Thu Mar 14 17:12:53 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA14796; Thu, 14 Mar 1996 17:12:53 -0400 Date: Thu, 14 Mar 1996 17:12:48 -0400 (AST) From: categories To: categories Subject: Foundations and formalisability Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Thu, 14 Mar 1996 21:00:06 GMT From: Ralph Loader cat-dist@mta.ca writes: > >This might be a little disingenuous - > >Of course, in any topos there will be a monic X=>Y --> P(XxY) , so via the >"internal language" X=>Y may be seen as a certain set of sets of ordered >pairs. But the point is that via the "internal language" you can (and >indeed you may) argue about the structure of a topos in a very "set-like" >manner. But of course you are not obliged to do so. So in a very real >sense, your (first) example illustrates that your fear is unfounded. We seem to have got completely sidetracked from either of the points I was trying to make (probably my fault for making it unclear that it was a two points, and for using sloppy language). The (good) category theorist proves "there exists internal homs [in any topos]" [by constructing particualar internal homs, or otherwise]. The (good) set theorist proves "there is a structure satisfying the Peano axioms [is a theorem of first order ZF]" [by constucting one explicitly, or otherwise]. Both can then be asked "which is the real internal hom / set of natural numbers". Both can answer that they didn't claim that there is a particular "real" internal hom / set of natural numbers. [See my P.S.] A (bad) topos theorist might never actually prove "there exists internal homs", but rather continually refer to an explicit construction, rather than its universal properties. A (bad) set theorist may construct a set, and never prove that it satisfies the Peano axioms, but rather keep referring to the explicit construction. In both cases, the bad mathematician has a real problem when asked why they're using their particular construction, as opposed to some isomorphic alternative. In both cases the good mathematician does the right thing---showing the existence of structures with appropriate properties, and then using those properties, rather than refering to any particular structure. This was with regards to the question "Which construction of the natural numbers do you have in mind? Russell's or Van Neumann's?". Now we have a slightly different issue: >point of Peter Freyd's observation was (I think) that a topos theorist >without any taste is less likely to stumble upon this question than a set >theorist without taste, who might well do so... due to the emphasis upon >different fundamental notions in the two approaches.) I read Peter Freyd's original criticism to be a criticism of the fact that it was *possible* to ask [Quote: `one can ask'] "Does any simple group appear as a zero of the Riemann Zeta function" in ZF, presumably claiming that this cannot be asked in category theory. If we weaken this to just saying that category theory makes some nonsensical statements more clearly nonsensical than they would be in set theory, then I have no objections to his statement. "Makes ... more clearly" is a matter of aesthetics, which is sometimes an important consideration. However, are aesthetics an overriding considerations for foundations? It's not obvious to me that it's even a _foundationally_ important consideration here---as has been pointed out by others, people don't do real mathematics in either first order topos theory or in first order ZF; it is probably impossible to develop a reasonably clear mathematical vernacular in either. Ralph. P.S. In any case, it is entirely possible to carry out formalisation of mathematics in first order ZF in such a way that statements like "A simple group appears as a zero of the Riemann Zeta function" do not have a formalisation. This is an application of the good practice I advocated above. In brief outline (=incomplete): Let Reals(R,+,*,0,1,<) be "R,+,*,0,1,< is a complete Archimedean linearly ordered field"(2), stated in the language of 1st order ZF in the obvious way. Define formalisations of sentences about the reals so as to be formulae in the form(1) Reals(R,+,*,0,1,<) implies phi(R,+,*,0,1,<) along with a _proof_ of a ``type-checking'' sentence ( there exists (R,+,*,0,1,<) such that Reals(R,+,*,0,1,<) and phi(R,+,*,0,1,<) ) if and only if ( for all (R,+,*,0,1,<), if Reals(R,+,*,0,1,<) then phi(R,+,*,0,1,<) ) Now of course, if a sentence about the reals can be seen to make sense, then there should be a straightforward proof that it is independant of any particular presentation of the reals, so that the type-checking statement will be ZF-provable. Clearly, if phi tries to formalise Freyd's statement, then it's type-checking sentence is false and not provable. Note that if phi is a tautology (or a contradiction) then it will have a provable type-checking sentence. We could probably argue until the cows come home about whether or not this is reasonable. (1) Using a trivial (&conservative) extension of ZF would enable us to drop the "Reals(R,+,*,0,1,<) implies". This is probably necessary if we wish to formalise statements with free variables over the reals [I use sentence in the logical sense of not having free variables]. (2) Apologies if I missed an axiom of the real numbers. P.P.S. This is getting off-topic for a category theory list. If people want to carry this on, perhaps we should take this off the categories list. From cat-dist@mta.ca Thu Mar 14 18:43:54 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA22428; Thu, 14 Mar 1996 18:43:52 -0400 Date: Thu, 14 Mar 1996 18:43:11 -0400 (AST) From: categories To: categories Subject: Re: Set membership <-> function composition Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Thu, 14 Mar 1996 13:30:24 -0800 From: Vaughan Pratt From: Peter Freyd If we stick to those parts of mathematics as described by the US National Science Foundation as "core mathematics" then I will stand by my statement. A semantics is unneeded. Without looking, I'm certain that they include calculus. I'm not sure what is meant by "calculus doesn't need a semantics." My impression was that the evolution of analysis was a beautiful interplay of definition and theorem that went on for centuries, from Newton (if not even earlier) right into the end of this century! Do you see a clear distinction between "definition" and "semantics"? Vaughan Pratt From cat-dist@mta.ca Thu Mar 14 23:09:03 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA03219; Thu, 14 Mar 1996 23:09:02 -0400 Date: Thu, 14 Mar 1996 23:08:32 -0400 (AST) From: categories To: categories Subject: Re: Orthogonality and toposes question. Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Thu, 14 Mar 1996 19:21:43 -0500 (EST) From: Dan Christensen | Below I consider a notion of orthogonality with respect to cones, | generalising that of orthogonality with respect to maps and the sheaf | condition for a cover in a Grothendieck topology: | | 1. We say that an object K is orthogonal to a cone D --> C | whenever for every cone D --> K there exists a unique | C --> K such that (D --> C --> K) = (D --> K). I've come across examples of the above in stable homotopy theory, except that uniqueness of the map C --> K doesn't hold in general. (In general one only gets these weakened versions of colimits in the homotopy category, if one gets anything at all.) It seemed to me to be unnatural, but now I'm happy to find that someone else has come across these partial colimits. Could you pass on any references you know, or any that people send to you? Thanks, Dan From cat-dist@mta.ca Fri Mar 15 09:35:55 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA14166; Fri, 15 Mar 1996 09:35:55 -0400 Date: Fri, 15 Mar 1996 09:35:19 -0400 (AST) From: categories To: categories Subject: Re: Set membership <-> function composition Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Thu, 14 Mar 1996 16:41:51 -0800 From: Vaughan Pratt From: Steve Vickers 1) The "element of" relation is absolutely _un_fundamental - this is part of the force of Freyd's example about simple groups. What are the elements of a real number? Yes, when you need to kick a set theorist, the real number line is a particularly sensitive part. Excellent kick. Ouch. In reality there is no single universal "element of" relation that describes the nature of everything, including the reals; instead, the reals are described by various relations with other specific objects. I'm with you 100% philosophically on this. We move and rest, and need vocabulary for both activities. Sets are great for lolling around in (I wonder how Cantor was at sports in school), but terrible for zipping perfectly smoothly along the real line. Categories give a much smoother ride than sets because they're *built* to. But they also have stationary parts, that show up in two places. (i) The objects. This is where one rests between morphisms. Having your objects form a set is a Good Thing, it fits their punctual style: "Be there on the dot" says the set. (ii) Homsets. Sets are dual to their elements. This seems to be because when dealing with powersets you have a higher probability of meeting the contravariant power set functor herself than one of her covariant brothers. (Not a theorem, just a feeling.) Homsets are no exception. When you pass from moving along one morphism at a time in a category to contemplating the morphisms lying there in profusion in the homsets, you dualize your viewpoint and see a morphism as merely a punctual dot of a homset. This explains the paradox of the very unpunctual morphisms able to make themselves the punctual members of a homset, we just view them dually "from the other direction" (not one parallel to the morphisms though). I agree that it is a type error to try to understand a smooth line as made of points when it is just trying to do its job and get you from point A to point B uninterrupted (poor gap, I interrupted it). Interruptions are incompatible with smooth travel. But travel with no rest at all is pretty grim and hard to sustain when you're trying to get some real work done, whence line *segments* rather than entire lines for category theory. Hell is having to move forever along the real line! But it is equally a type error to try to turn your rest stops into motion. You *need* to rest from time to time. For one thing it gives your maintenance department a turn at doing stuff, maintenance has to shut down when you're on the move, on-the-fly maintenance is *much* harder. And if you're the type of person that has opponents, it's all in the game to give them a turn. But if I'm with you 100% philosophically on this example, I'm only with you about 50% mathematically. It seems to me that set theory supports the go part of stop-and-go traffic *pretty* well. Not perfectly, as we agree. But when you consider how much of the continuum set theory *is* able to comprehend, I'm not terribly sold on the inadequacy of sets for modeling go almost as well as stop. 2) Topology: Normally one thinks of open sets as being sets of points, but localic topology views points as being sets of opens (e.g. reals as neighbourhood filters above). There is obviously a fundamental relation of points being "in" opens, and localic arguments can be expressed quite reasonably using it. Set theoretic expression using "element of" completely obscures this. In other words, set theory prevents you from adequately expressing reasonable arguments. I'm with you <10% on this one. I can't tell what limitation of Set you're talking about here, but unlike your philosophically excellent 1) it doesn't seem to match up to any of the well-known limitations. It sounds like you're saying that set theory doesn't let you talk about the converse of the membership relation. That's certainly not the case. Or maybe you mean that Set\op is not a concrete category. What's wrong with its concrete representation as CABA? If that seems too complicated, how about its coconcrete representation as the category of sets and their *converse* functions (binary relations whose converse is a function)? Maybe you're saying that Hom:Set\op*Set -> Set is outside set theory. That too is implausible. None of these issues hold the sort of terrors for set theorists that the continuum does. At least not a terror that has them terribly bothered mathematically the way the continuum problem does. 3) Generic objects: 0%, needle wrapped around the post. You seem to be saying that set theorists are scratching their heads over what a variable is while the category theorists have it all sorted out. News to set theorists. You can't kick a set theorist in the variables, they're very well protected there. 4) What about theories such as that of accessible categories, that, for set theoretic reasons, have to be liberally sprinkled with infinite cardinals? Doesn't this make you think that perhaps set theory is somehow obscuring simple ideas? I don't know how to define "accessible category" without bringing cardinals into the picture, but maybe I'm the last one to find out how, as usual. What's the trick? To my mind, the evidence suggests that despite its undoubted successes, set theory is not right for mathematical foundations, and we should be looking for its replacement. Whoa, needle went negative there. But I would have the same reaction to a set theorist who claimed that categories were nothing but an alternative language for the mathematics ordinarily and satisfactorily treated by set theory. ("Alternative language for" is the polite code word some people use for "weird way of talking about") Set theory itself will only go away when the natural numbers go away. Let's get real here. The natural numbers are the very oxygen of mathematics, and they are not going away in *any* foreseeable future. Hence neither is the (internally) bicomplete topos of finite sets. This topos is a very nice concrete way of working with natural numbers---it makes numbers *more* categorical, not less, by letting you transform them. But sets *do* have to transform via arbitrary functions, there's no way to wriggle out of *that* one! Transforming sets with binary relations neuters them, neutered sets are only good for the side lines. *Converse* functions on the other hand are fine, if you're not Bill Thurston, who eloquently expressed his inability to relate to Set\op at UACT. I don't care how the infinite sets are organized, just so long as there's a way of doing it that doesn't make the logic that bears on my life inconsistent. I'm not planning on rubbing up against any infinite sets personally without a sturdy layer of math and logic between me and them. You can seriously injure yourself with an infinite set. Mathematics founded on set theory stays close to the air supply. Any religious upstart of a foundations claiming to offer a viable *replacement* for set theory is going to have to argue real hard about the disadvantages of breathing! Whether we should work with sets and categories in exactly equal proportions is an interesting question. I tend to be slightly more settish than cattish in my thinking, if only because I'm lazy and sit around a lot, on the dime if not on the dot. But there's not a big gap. Categories: can't live with sets, can't live without them. Sets: can't live with categories, can't live without them. Vaughan Pratt PS. No reactions yet to my ordinal-based definition of Set. Main thing I want to know is, is it old hat? Second thing, is it good for anything else besides what I made it up for, namely to shorten the passage from function composition in Set to the membership relation on ob(Set)? I don't claim any more *significance* to the membership relation in my version of Set than Mike Barr et al were claiming for other versions of Set. Well, maybe a little more: it is undeniably the membership relation for ordinals, which is all my Set claims to contain *explicitly*. But is pi essentially an ordinal? Of course not. Can pi exist in my Set? No more or less than in anyone else's Set. Is pi made any more real by installing it in a category? Rubbish. From cat-dist@mta.ca Fri Mar 15 09:36:08 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA14205; Fri, 15 Mar 1996 09:36:08 -0400 Date: Fri, 15 Mar 1996 09:36:00 -0400 (AST) From: categories To: categories Subject: Re: Orthogonality and toposes question. Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Fri, 15 Mar 96 9:47:37 MET From: Koslowski With regard to Marcelo Fiore's question about orthogonality with respect to cones: together with Gabriele Castellini and George Strecker I have studied some aspects of this phenomenon for discrete cones in Regular Closure Operators Applied Categorical Structures 2 (1994), 219--244 Kluwer Academic Publishers Section 5 of this article might be of interest. Best regards, -- J"urgen Koslowski From cat-dist@mta.ca Fri Mar 15 14:45:10 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA01830; Fri, 15 Mar 1996 14:45:10 -0400 Date: Fri, 15 Mar 1996 14:43:31 -0400 (AST) From: categories To: categories Subject: Re: Set membership <-> function composition Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Fri, 15 Mar 1996 08:53:57 -0500 From: Peter Freyd There's certainly a clear distinction between "definition" and "semantics". They are -- to echo PeterJ -- in different categories. But Vaughan's point about the calculus is well taken. I must back down a bit. Yes, a semantics for the real numbers and for limits and for continuity and -- hardest these days to believe -- for the very notion of function were indeed needed by 19th C mathematicians. So let me try again. Core mathematics in the 20th C did not provide a problem for semantics and for that reason the inadequacy of formal set theory was not noticed. Inadequate for what? Well, let's start with the Church polymorphic notion of number. From cat-dist@mta.ca Fri Mar 15 15:56:10 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA07398; Fri, 15 Mar 1996 15:56:10 -0400 Date: Fri, 15 Mar 1996 15:55:44 -0400 (AST) From: categories To: categories Subject: sets against categories Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Fri, 15 Mar 1996 12:30:19 -0600 From: saunders@math.uchicago.edu The recent discussion of sets against categories on the internet appears to miss the appropriate sources. It is well known that it is easy to go from sets to categories, harder in the reverse. For this there is a very well-known equicoherence theorem, which is presented in both the standard texts on topos Johnstone, Chapter 9, S 7 Mac Lane / Moerdijk (Sheaves in Geometry and Logic, Chapter 6, S 10.) I fondly imagine that the latter is a bit clearer. Both sources will give your the original literature--for example Mitchell JPAA 2(1972) p. 261 (I suggested this question to Bill Mitchell when he was an instructor at Chicago). As far as I can make out; none of the many messages speaks to this fact. It is a reasonable question for Pratt to raise, though he should have known that the Goldblatt book was hopeless from day one. Of course most mathematicians find sets easier than cats--but they usually can't recite ZFC axioms. The fault may lie with Pat Suppes, who taught sets in the Kindergarten. Otherwise, the exchange convinces me tht e-mail is for the birds. All fluff with no professional substance Saunders Mac Lane Department of Mathematics University of Chicago saunders@math.uchicago.edu From cat-dist@mta.ca Sat Mar 16 10:38:41 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA00157; Sat, 16 Mar 1996 10:38:41 -0400 Date: Sat, 16 Mar 1996 10:37:56 -0400 (AST) From: categories To: categories Subject: Re: Set membership <-> function composition Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Fri, 15 Mar 1996 12:37:36 -0800 From: Vaughan Pratt There's certainly a clear distinction between "definition" and "semantics". They are -- to echo PeterJ -- in different categories. In his evening talk on Post some LICS' ago, Martin Davis told us of his sense of revelation when he learned he'd been a computer scientist all these years. Now I know just how he must have felt. What a relief to find I have *not* been a semanticist all these years. All I ask is a tall ship and a star to steer her by. Definitions tell us our position relative to both our destination and the rocks of inconsistency. Whatever semantics is, if the navigator says he can't do his job without it we're lost. Another round of semantics for the navigator. let's start with the Church polymorphic notion of number. Of course when the navigator's had so much semantics he tells you he's seeing double, you do worry a bit. That semantics is heady stuff. Vaughan Pratt From cat-dist@mta.ca Sat Mar 16 10:38:49 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA00164; Sat, 16 Mar 1996 10:38:49 -0400 Date: Sat, 16 Mar 1996 10:38:45 -0400 (AST) From: categories To: categories Subject: Re: sets against categories Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Fri, 15 Mar 1996 15:11:50 -0800 From: Vaughan Pratt From: saunders@math.uchicago.edu Mac Lane / Moerdijk (Sheaves in Geometry and Logic, Chapter 6, S 10.) Reference *much* appreciated, which I am browsing now. (Peter, will Topos Theory be back in print soon?) It is well known that it is easy to go from sets to categories, harder in the reverse. This is disturbing, since it is the opposite of the answer I came up with myself a couple of days after asking my question. (I am reading "harder" as "necessarily harder" here, my apologies if this was not your intended meaning.) As often in these things, at least some of the problem lies with my question, which was certainly fluffy when I asked it, not knowing then quite what I really wanted to ask. I think I can sharpen it now. Is there a category equivalent to Set for which it is easy to recover the membership relation from the category structure? This is still not a mathematical question as it leaves "easy" open to interpretation. But I think the rest of it is unambiguous. Now I thought I'd answered this sharper question in the affirmative, with an interpretation of "easy" that surely *no* reasonable person could complain about, namely a two line construction of the membership relation. Therefore if my answer was only "fluff", I have made an error somewhere, either in my construction of this version of Set or in my choice of problem. With regard to the latter possibility, I freely admit to knowing less than just about anyone on this list what it feels like to work in a general topos, not enough to write even 6 pages about them let alone 600. My experience of toposes is with one topos only, Set, which makes me about the last person qualified to attempt a contribution to topos theory. However, that my question only concerns the one topos Set gives me hope that, if there is indeed a problem with my construction, it is some technical oversight that I need to repair if possible, and not something to do with other toposes besides Set. In passing, let me again draw people's attention to the fact that I described not just the category Set but its (cartesian) closed structure as well, including complete verification of the coherence conditions. (Not that this was particularly difficult in this case. :) Without giving the full closed structure I do not understand how one can claim to have fully specified which topos one is speaking of. Does the topos literature attend adequately to this detail? (It may well, I just don't know where to find it.) I interpret the reference to Isbell at the end of VII.1 of CTWM as (inter alia) a warning that one cannot take the closed structure for granted merely because it is cartesian closed. If this misinterprets the situation for the cartesian closed case, and coherence is in fact routine there, then my apologies for the misunderstanding. Vaughan Pratt From cat-dist@mta.ca Sat Mar 16 10:49:08 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA00406; Sat, 16 Mar 1996 10:49:08 -0400 Date: Sat, 16 Mar 1996 10:48:55 -0400 (AST) From: categories To: categories Subject: Computational Category Theory Tools Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Sat, 16 Mar 1996 10:43:23 -0400 (AST) From: Bob Rosebrugh CATEGORIES DATABASE/TOOLS A C program for storage of and computation with finitely presented categories is now available as described below. The program is menu-based and stores finitely presented categories, functors between them and finite-set valued functors from them. The storage format is the same as that used by the Carmody-Walters `kan' program (available from the University of Sydney ftp site.) Several tools for computation with finite categories are included. For example, tests for equality of arrows, whether an object is initial and so on. A new implementation of the Todd-Coxeter procedure for computing left Kan extensions is complemented by an implementation of a procedure for computing right Kan extensions. Details are included in the user manual which may be found at ftp://sun1.mta.ca/pub/papers/rosebrugh/catuser.dvi The program was written by Michael Fleming and Ryan Gunther while they were employed at Mount Allison University under NSERC Canada's USRA program. It is free software and without warranty. Indeed, it should be treated as an `alpha' version. Bug reports (to rrosebrugh@mta.ca) are welcome, but may not be acted upon immediately. The source code and compiled (Sun and DOS) versions are avalable for ftp from the directory ftp://sun1.mta.ca/pub/sources/rosebrugh/{unix,DOS} The compiled versions are named category.exe. A set of examples is found in the `examples' subdirectories. Bob Rosebrugh From cat-dist@mta.ca Sat Mar 16 23:08:01 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA19753; Sat, 16 Mar 1996 23:08:01 -0400 Date: Sat, 16 Mar 1996 23:07:22 -0400 (AST) From: categories To: categories Subject: Johnstone quote Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Sat, 16 Mar 1996 16:35:47 -0500 (EST) From: Colin McLarty A friend (David Corfield) says he recalls Johnstone somewhere complaining about logicians who use topos methods in their thinking but keep them out of publications. Can anyone tell me where that is? Colin McLarty From cat-dist@mta.ca Sat Mar 16 23:08:35 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA19367; Sat, 16 Mar 1996 23:08:35 -0400 Date: Sat, 16 Mar 1996 23:08:32 -0400 (AST) From: categories To: categories Subject: 2 bug fixes Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Sat, 16 Mar 1996 18:43:26 -0800 From: Vaughan Pratt The following repairs two problems I found with my ordinal-based axiomatization of Set: missing axiom of infinity (no NNO), and an inconsistent definition of product. 1. Add "There exists x such that 1+x=x." (Set *forbids* FinSet.) (By equality in my axiomatization I always mean identity, not just iso.) [A reminder that i/j = min k[i < j*(k+1)], and i%j = i - j*(i/j) (ordinal division and ordinal remainder, used in the following). Exercises. (i) j*(i/j) <= i. (ii) i%j < j. ] 2. Replace the definition of product by the following. Given an ordinal i, the i-product p = p_i of a family ,j,m p_k, namely \n.n%p_k. (So f_{jj} is the identity.) For successor ordinals i = k+1, the definition of p_i is completed by requiring that it have in addition a *main* projection g_k : p_{k+1} -> n_k, namely \n.n/p_k (a monotone function). For limit ordinals, the definition of p_i is completed, up to Choice, by requiring it to be *a* categorical limit of the diagram whose objects are, for j, m p_j defined at this level. The counit of i-product at family , j p_{j+1} -> n_j. These are the *standard* projections of ordinal product. The unit of I-product at n (the diagonal d_n: n->n^I) is the K combinator, \m.(m,m,m,...), sending m to the constant I-tuple of m's. ----- I-Products act just like counters with I digits; this is lexicographic product adapted to infinite ordinals. Compare the explicit definition \n.n%p_k, a monotone function, at successor products to the underdetermined categorical definition at limit products. The latter defines ordinal product only "up to Choice," bringing in Choice as a "randomizer". That a limit of this (small) diagram exists is immediate by the completeness of Set. Once one such limit has been found in this version of Set, all ordinals of the same cardinality become equally eligible, and the first paragraph of the definition then selects the least ordinal from among these. By definition this is a cardinal, and so our definition makes *all* limit products cardinals, a nice feature. But even though we know exactly which cardinal, the product is only defined up to an automorphism. The well-ordering of that cardinal is thus completely uncorrelated with the projections. Barring further bugs, this definition is an underdetermined alternative to those of Birkhoff 1942 and Hausdorff, who gave fully specified notions of ordinal or lexicographic product. Birkhoff's definition did not always produce ordinals, though it did preserve linearity. Hausdorff's definition did not even send ordinals to linear orders. The above preserves ordinals, inevitably at the cost of nondeterminism at each limit ordinal. Vaughan Pratt PS. I learned after giving the obvious (for Set) ordinal version of the axiom of infinity above, that Peter Freyd had shown it was equivalent to NNO not just for Set but for *any* topos. Now *that's* what I call an interesting property of toposes. A lightweight collection of such nice facts in one place might put hard-to-please types like me in a more receptive frame of mind for the massive body of theory that topos theory seems dependent on. Halmos fits "all" the basic material about naive set theory in his 100-page book. Is it fair to say that the corresponding material treated in topos theory requires considerably more space? And if not, when can we expect the topos counterpart to Halmos? From cat-dist@mta.ca Sun Mar 17 22:22:50 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA17057; Sun, 17 Mar 1996 22:22:49 -0400 Date: Sun, 17 Mar 1996 22:22:43 -0400 (AST) From: categories To: categories Subject: Re: Set membership <-> function composition Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Mon, 18 Mar 1996 10:44:32 +1100 (EST) From: peterj@maths.su.oz.au After seeing the volume of "fluff" that this topic had generated on Friday, I took a vow not to contribute any more to it. But Vaughan Pratt seems to be challenging the rest of us to find something wrong with his ordinal-based definition of Set, and no-one else has taken up the challenge; so I'll have to break my vow and point out its obvious shortcoming. Vaughan's definition is fine as long as you are happy, not just to assume that the axiom of choice holds, but actually to rely on it to construct codings for you. If AC doesn't hold, the Vaughan's category fails to be cartesian closed; and even if it does, you don't have the ability to point to a particular object of it and say "This is the set of real numbers" (still less to point to a particular morphism and say "This is the addition operation on real numbers"); you have to rely on God's (or "the randomizer's", as Vaughan seems to call him) ability to do it for you. I suppose only a minority of mathematicians are unhappy about AC to the extent of actually rejecting any construction that can't be done without it. But I think a very large majority would be unhappy about calling upon God to construct things for them (such as the real numbers) for which they know there is a perfectly good man-made construction. Such people are going to be in a near- permanent state of unhappiness if they are condemned to do mathematics inside Vaughan's category. By the way, the Cole--Mitchell--Osius equivalence between weak Zermelo set theory and well-pointed topos theory, which is described in my book (sorry Vaughan, but Academic Press won't reprint it) and in Mac Lane--Moerdijk, doesn't assume the axiom of choice; it's an "optional extra" which you can add to both sides of the equation if you want to. Peter Johnstone From cat-dist@mailserv.mta.ca Sun Mar 17 22:42:01 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA18736; Sun, 17 Mar 1996 22:42:00 -0400 Received: from mailserv.mta.ca by BIGMAC.MTA.CA with SMTP; Sun, 17 Mar 1996 22:39:12 -0400 (AST) Received: by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA18643; Sun, 17 Mar 1996 22:41:59 -0400 Date: Sun, 17 Mar 1996 22:41:58 -0400 (AST) From: Bob Rosebrugh To: Categories List Subject: Re: Set membership <-> function composition Message-Id: Mime-Version: 1.0 Content-Type: MULTIPART/MIXED; BOUNDARY="Boundary (ID FddD8IJgtE7WWNb1ReXE0Q)" Content-Id: Status: RO X-Status: Date: Sun, 17 Mar 1996 11:28:59 -0500 (EST) From: mthfwl@ubvms.cc.buffalo.edu Younger participants and lurkers in this past week's discussion may be shocked at the large amount of frantic concern to prevent obscurity from becoming extinct. Vaughan Pratt's question: -- should one forget altogether about membership -- `and' -- just work in one's favorite topos? -- still remained unanswered. The possibility of rejecting the rigid epsilon chains as a `foundation' for mathematics occurred to many around 1960. But for me the necessity for doing so became clear at a 1963 debate between Montague and Scott. Each had tried hard to find the right combination of tricks which would permit a correct definition of the fundamental concept of a model of a higher-order theory (such as topological algebra). Each found in turn that his proposal was refuted by the other's counter example (involving of course unforeseen ambiguities between the given theory and global epsilon in the recipient set theory). The whole difficulty Montague and Scott were having seemed in utter contrast with what I had learned about the use of mathematical English and what we try to make clear to students: in a given mathematical discussion there is no structure nor theorem except those which follow from what we explicitly give at the outset. Only in this way can we accurately express our _knowledge of_ real situations. A foundation for mathematics should allow a general definition of model for higher-order theories which would permit that crucial feature of mathematical English to flourish, confusing matters as little as possible with its own contaminants. We are constantly passing from one mathematical discussion to another, introducing or discharging given structures and assumptions, and that too needs to be made flexibly explicit by a foundation. Of course the reasons for this motion are not whim, but the sober needs of further investigating the relations between space and quantity,etc and disseminating the results of such investigation. The idealization of a truly all-purpose computer (on which we might record such discussions) was relevant. The explicit introduction, into a given discussion, of a few inclusion, projection, and evaluation maps on a formal footing with addition, multiplication and a differential equation, etc. clarifies and is a minor effort compared with the complications and collisions attendant on an arbitrary monolithic scheme for keeping them implicit. Vaughan's continuing confusion comes he says from Goldblatt 12.4. More exactly, the few lines introducing 12.4 are `In order to...construct models of set theory from topoi, we have to analyze further the arrow-theoretic account of the membership relation'. However, `the' arrow-theoretic account of membership was actually totally omitted from the book, though it should have been in section 4.1, along with the discussion of related basic matters, such as subobjects and their inclusions. (I return to this below). For the stated narrow purpose of constructing models of epsilon-based set theory, one indeed needs an arrow-theoretic account (not of the mathematically useful relation but) of the von Neumann rigid-epsilon monsters. Goldblatt recites such an account, as do several of the dozen or so texts on topos. The construction had been done around 1971 by each of Cole, Mitchell, and Osius. I had suggested the basic approach they used, but in so doing I was just transmitting (in categorical form) what I had learned from Scott about the 1950's work of Specker. Specker is a mathematician (for example it was he who taught R. Bott algebraic topology!) who realized that transitive ZFvNBG `sets' can actually be seen as ordinary mathematical structures (posets) which happen to satisfy some rather non-ordinary conditions (such as no automorphisms, etc.). Certain special morphisms between these structures can be seen as `epsilons' and certain others as `inclusions'; the functor which adjoins a new top element can be seen, for the special structures, as `singleton', and permits to define those two special classes of morphisms in terms of each other. A further insight concerning how these bizarre structures could be studied, if one wished, in terms of ordinary mathematical concepts such as free infinitary algebras, is elegantly explained in the recent L.M.S. Lecture Notes 220 by Joyal and Moerdijk. They too provide, on the basis of the ordinary mathematical ground (of toposes and similar categories) a foundation for those structures; for anyone who is seriously interested in those structures, that book should be an excellent reference. However, for anyone with potential to advance mathematics, such interest should be discouraged, since the time and energy wasted on these things during this century has vastly overshadowed any byproduct contribution to either mathematics or to the foundation of mathematics. Even most set-theorists work mainly on problems with definite mathematical content (such as Cantor's hypothesis, Souslin's conjecture, `measurable' cardinals, etc. etc.) which have no actual dependence on these rigid epsilon chains for their formulation and treatment. That many mathematicians (including some categorists) continue to pay lip-service to an alleged `foundational' role of these chains can only be attributed to the general cultural backwardness of our times; similarly, certain natural scientists 300 years ago felt compelled to refer to a `hand that started the universe' even though they knew it played no role in their work. It is my impression (though further sifting of the historical record is needed to confirm it) that Hausdorff and other pioneers did not actually give to the rigid epsilon the central role that von Neumann and others later did. Cantor had made several important advances, some of which may have been submerged by the later attempt at a monolithic ideology; my paper on `lauter Einsen' in Philosophia Mathematica (MR'ed by Colin McLarty) describes some potentially useful mathematical constructions which were suggested by Cantor's work but which have nothing to do with an external, rigidly imposed epsilon. (Of course, one of Cantor's other contributions was the theorem that non trivial function spaces are bigger than their domain space, which he knew implied that no single set can parameterize a category of sets. It is amazing in hindsight how Frege and Russell managed to transform this theorem into a propaganda scare concerning the viability of mathematics, thus obscuring more serious problems with the `foundation', such as the space-filling curves.) The omission by Goldblatt of the definition may have contributed to Vaughan's further misconception that `by toposes...membership is discussed only in power objects.' In the next two paragraphs I recall the definition. The elementary membership relation in any category is straightforward, one of the two inverse relations for composition itself, the one which Steenrod called the lifting problem: `y is a member of b' means by definition that there exists x with y = bx. This of course presupposes that y and b have the same codomain, and for uniqueness of the proof x, that b is mono. The mathematical role of these two presuppositions must be understood. It became clear in the early sixties that the definition of SUBOBJECT given by Grothendieck is not a pretense, circumlocution, or paraphrase, but the only correct definition. Here `correct' means in a foundational sense, i.e. the only definition universally and compatibly applicable across all the branches of mathematics: a subobject is NOT an object, but a given inclusion map. The intersection of two objects has no sense, for only maps (with common codomain) can overlap. The category of sets is in no way exceptional in this regard. Singleton is not a functor of objects but a natural transformation (from the identity functor to a covariant power set functor in the categories where the latter exists .) Of course, when I say `only definition' it is not meant to exclude consideration of further mathematical conditions such as regular monos, closed monos etc whose interest may be revealed by the study of the particular category; nor should we long forget that subobjects are typically mere images of fibrations wherein the question of whether there exists a proof of membership is deepened to a study of particular sections. Equality is not obscure, it just keeps changing - but in ways under our control. Here I am speaking of the dual notion to membership, which might be called `dependence' and is just the epic case of Steenrod's extension problem. In commutative algebra for example, what two quantities `are' under a chosen homomorphism may become equal. Neither quotient objects nor subobjects have `preferred' representatives in their isomorphism classes; proposals to introduce such preferred representatives have been justly ignored, since such would only re-introduce spurious complications - of course in any topos further objects do exist which can support maps that PARAMETERIZE precisely these isomorphism classes . **** One topos becomes another. Only a very limited mathematical agenda could have a favorite topos to stay in, because constructions that one is led to make in E will lead to further toposes E' which are both of interest in themselves and also further illuminate what is possible and necessary in E; indeed the most effective way to axiomatize E is to specify a few key E' which are required to exist. A topos that satisfies both an existential condition concerning sections of epis and a disjunctive condition concerning subsets of 1 is an important attempted extreme case of constancy and non-cohesion, that usually in mathematics becomes a more determinate category of variation and cohesion, modelled via structures sketched by diagrams of specified shapes . It may be occasionally of interest however to consider still more extreme affirmations of constancy such as the lack of objects both larger than a given object and smaller than its power object; Goedel's theorem to the effect that such constancy can always be achieved was shown by W. Mitchell to be independent of any extra-categorical structure such as the epsilon chains which most people had assumed are inherent to the very idea of `constructible'. This might be clarified if Mitchell's tour de force could be replaced by something more direct. That startling result of Mitchell and its total lack of follow-up was mentioned by McLarty during this interchange. Mentioned by Loader was another striking result which in its existing form still seems bound up with the epsilon ideology, but which surely could contribute something to the understanding of the category of abstract sets, namely the Martin/Friedman work on Borel determinacy, as I discussed with Friedman twenty years ago. Union and intersection are shadows (in a proof-theory sense) of sums and products, but in this case the tail wags the dog--why? The usual formulation that the replacement schema is required surely depends on a special limitation of the class of theories: how could one statement require a schema? Of course, the proof shows that something is required but what? Replacement can easily be made explicit in a topos, if required; indeed doing so makes it clearer that, in the case of abstract sets, the essence of the schema is just to give more cardinals. *** The title of Goldblatt's book (and not only his!) is in itself misleading. The purpose of topos theory and category theory is not primarily to provide an analysis of logic, but to permit the development of algebraic topology, algebraic geometry, differential topology and geometry, dynamical systems, combinatorics, etc. It emerged in the 1960's that logic and set theory can and should be viewed as a special distillation of this geometry. In that way the actual achievements of logic and set theory are, reciprocally, enjoying much wider mathematical application. Bill Lawvere From cat-dist@mta.ca Sun Mar 17 22:22:52 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA18028; Sun, 17 Mar 1996 22:22:51 -0400 Date: Sun, 17 Mar 1996 22:21:20 -0400 (AST) From: categories To: categories Subject: defining sets from abelian groups Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Sun, 17 Mar 1996 08:54:16 -0800 From: Vaughan Pratt I want to say something along the lines of "You can define abelian groups in the internal logic of Set, but you can't define sets in the internal logic of Ab." Is this intuition supportable? Ideally there would be a precise technical sense in which it is provably the case. Vaughan Pratt From cat-dist@mta.ca Mon Mar 18 10:36:21 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA02518; Mon, 18 Mar 1996 10:36:21 -0400 Date: Mon, 18 Mar 1996 10:35:22 -0400 (AST) From: categories To: categories Subject: Re: defining sets from abelian groups Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Mon, 18 Mar 1996 07:47:40 -0500 From: Peter Freyd Vaughan says -- correctly I think -- that "you can't define sets in the internal logic of Ab." I suspect that the proof will have to use the dualities that reside in Ab. Let Gr be the category of all groups, abelian or not. Then: The category of co-groups in Gr is equivalent to Set. Cf: The category of co-groups in Ab is equivalent to Ab. "Co-group" means, of course, "group in the opposite category". The second of the two assertions above holds for any additive category: it's easy to show that each object in any additive category has a unique co-group (indeed, a unique co-monoid) structure (the co-multiplication is the diagonal map). I know no citation for the first assertion. To prove it, one shows that the only groups with co-group structures are free groups and that the only co-multiplication on Free(X) is such that X -> Free(X) -> Free(X+X) is the point-wise product of the two functions of the form X -> X+X -> Free(X+X). From cat-dist@mta.ca Mon Mar 18 10:51:31 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA02761; Mon, 18 Mar 1996 10:51:30 -0400 Date: Mon, 18 Mar 1996 10:50:43 -0400 (AST) From: categories To: categories Subject: Re: defining sets from abelian groups Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Mon, 18 Mar 1996 09:39:51 -0500 From: Michael Barr - I want to say something along the lines of "You can define abelian - groups in the internal logic of Set, but you can't define sets in the - internal logic of Ab." - - Is this intuition supportable? Ideally there would be a precise - technical sense in which it is provably the case. - - Vaughan Pratt - - I don't know, since I don't understand these issues sufficiently well, but if you can define the free abelian group cotriple, you can then define the coalgebra category for that cotriple and that is the category of sets. In fact, that is a ! operation, in Girard's sense, on the fragment of linear logic that Ab satisfies. (This last was an observation of Jim Otto's.) Michael Barr From cat-dist@mta.ca Mon Mar 18 16:08:41 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA28688; Mon, 18 Mar 1996 16:08:40 -0400 Date: Mon, 18 Mar 1996 16:08:05 -0400 (AST) From: categories To: categories Subject: Re: defining sets from abelian groups Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Mon, 18 Mar 1996 13:28:17 -0500 (EST) From: MTHFWL@ubvms.cc.buffalo.edu In the Spring of 1971 at Chicago, Peter Freyd gave some very interesting lectures in which he showed how to construct a topos from a symmetric monoidal closed category by considering certain structured co-commutative co-algebras. This was done in such a way that for a group G one could recover the topos of G-sets (and hence the group itself) from the category of linear representations. Since the category of abelian groups has a unique closed monoidal structure, this should refute Vaughan Pratt's conjecture. It should have even many more applications than that, which is why I have long urged Peter to write it up. Bill Lawvere From cat-dist@mta.ca Mon Mar 18 16:31:24 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA30862; Mon, 18 Mar 1996 16:31:23 -0400 Date: Mon, 18 Mar 1996 16:30:37 -0400 (AST) From: categories To: categories Subject: Re: defining sets from abelian groups Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Mon, 18 Mar 1996 10:46:38 -0800 From: Vaughan Pratt I don't know, since I don't understand these issues sufficiently well, but if you can define the free abelian group cotriple, you can then define the coalgebra category for that cotriple and that is the category of sets. Peter Freyd succinctly shows you can't with The category of co-groups in Ab is equivalent to Ab. Interesting that Peter used duality to prove it, since my reason for strongly believing it was also duality-based. The general principle I used for my reasoning was that the only categories "definable" in the internal logic of a self-dual category are full subcategories of it. FinAb is self-dual, but FinSet does not fully embed in FinAb. If only I knew what "definable" meant this would be a proof. I came to appreciate this principle while investigating Chu(Set,K). All notions of "definable" I understand (e.g. first order definable) are subsumed by this principle. However that's not sufficient reason to call it a theorem, since someone may have a method of definition I don't know about that violates it. For example I have not yet figured out whether the method of sketches violates it, though I can't imagine how it could. In fact, that is a ! operation, in Girard's sense, on the fragment of linear logic that Ab satisfies. (This last was an observation of Jim Otto's.) Is Jim's statement even well-defined? ! is a functor projecting LL onto a cartesian closed full subcategory of itself. For the above to make sense you would need a full embedding of the coalgebra category, namely Set, back into Ab. But unless I'm dreadfully confused (which I often am) there isn't such. What could a set reasonably be other than the free abelian group on it? But when you're inside Ab, Ab(G,H) = H for H a fag, so that's not it. Similar deal with Rel or CSLat. I was dreadfully confused about this in 1991 when I first got involved with duality via CSLat and their sibling Event spaces. I wish someone had pointed out to me that my ! *didn't* produce a cartesian closed category as I was claiming. Instead I had a long period of waiting for my vision problems to clear up. Adding ! to LL stretches LL out a lot, much wider than Ab with respect to the Stone gamut (the Set<->Set\op axis). Enough in fact to make it look rather like Chu(Set,K) for indefinite K, less such amenities as induction and such obscurities as 1 par 1 |- 1 (noticed by Lafont and Streicher---with its contrapositive _|_ |- _|_ @ _|_, the two objects 1 par 1 and _|_ become sort of the "two halves" of a single coalgebra in Chu(Set,K)). You just have to take the bad with the good when you have a nice model like Chu(Set,K). I've incorporated my proof that Set is a bicomplete equational topos (meaning one with all natural isos identities) into my LL'96 paper, "Linear Logic complements Classical Logic," sent off last night. In the light of Peter Johnstone's remarks it seemed prudent to add an explanatory paragraph as a sort of talisman against the nonmonotonic logic of antiChoice fundamentalism extolled on Sundays. This is now available as ftp://boole.stanford.edu/pub/llcocl.ps.gz, with tex and dvi counterparts in the usual subdirectories, /pub/TEX and /pub/DVI. I'll post the abstract here shortly, or look it up yourself in the file ABSTRACTS in the same directory. This is paper 45 in that directory, getting time to compress its scattered ideas down a bit. Vaughan Pratt From cat-dist@mta.ca Mon Mar 18 16:31:49 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA30436; Mon, 18 Mar 1996 16:31:48 -0400 Date: Mon, 18 Mar 1996 16:31:44 -0400 (AST) From: categories To: categories Subject: Paper available: Linear Logic complements Classical Logic Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Mon, 18 Mar 1996 11:24:50 -0800 From: Vaughan Pratt Subject: Paper available: Linear Logic complements Classical Logic The paper described below is available by FTP or the web as follows. FTP ftp boole.stanford.edu cd pub bin get llcocl.ps.gz WEB URL: http://boole.stanford.edu/pub/llcocl.ps.gz Linear Logic complements Classical Logic V.R. Pratt To appear in preliminary proceedings of Linear Logic '96, Tokyo Classical logic enforces the separation of individuals and predicates, linear logic draws them together via interaction; these are not right-or-wrong alternatives but dual or complementary logics. Linear logic is an incomplete realization of this duality. While its completion is not essential for the development and maintenance of logic, it is crucial for its application. We outline the ``four-square'' program for completing the connection, whose corners are set, function, number, and arithmetic, and define ordinal Set, a bicomplete *equational* topos, meaning its canonical isomorphisms are identities, including associativity of product. This directory also contains 44 other papers on related topics. For a list of abstracts, see the file ABSTRACTS in this directory, URL: http://boole.stanford.edu/pub/ABSTRACTS Vaughan Pratt From cat-dist@mta.ca Tue Mar 19 20:59:40 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA24445; Tue, 19 Mar 1996 20:59:39 -0400 Date: Tue, 19 Mar 1996 20:59:28 -0400 (AST) From: categories To: categories Subject: Category theoretic reflection principles? Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Tue, 19 Mar 1996 12:42:22 GMT From: Ralph Loader Are there any categorical analogues of the reflection principles of set theory? I couldn't find any in the texts I have, or in the MathSci index. These can be used to axiomatise ZF, and it should be possible to translate them into category theory in a reasonably nice way, so as to give a category theoretic account of ZF that is independent of such things as elements. Below is an account of how I think this could be done; my knowledge of the category theory required is sadly lacking in places, suggestions and criticism are very welcome. (1) What are the reflection principles of set-theory. Formal statement: let phi(x) be a first-order formula of set theory. Then the following is a theorem of ZF: for all x, there exists an ordinal alpha such that (a) x in V_alpha and (b) for all y in V_alpha, phi(y) iff 'phi(y) holds in V_alpha'. 'phi(y) holds in V_alpha' means the formula obtained by restricting all quantifiers in phi to the set V_alpha (the V_alpha present the universe of ZF as a union of an increasing sequence of sets). [By coding trickery, it doesn't make any difference if we allow several formula with several free variables to be reflected in the same V_alpha. For our purposes, it's useful to take alpha to be a limit ordinal, so that V_alpha gives a topos.] In other words, the universe of ZF has lots of sub-universes that "look just like" the original universe, where "looks just like" can be measured by any particular formula phi. [A more "dynamic" intuitive way of looking at this is having constructed a universe V of set theory, we can take V to be a set, and build a new universe V' containing it; in this new universe V', the V_alpha required is the original V.] (2) How do we translate these into category theory? More specifically, take our universe to be a topos E. How can we state a reflection principle in E without reference to such things as the "V_alpha" that seem fairly hideous monsters to a category theorist (even better would be to get rid of first order formulae, also). Presumably, we want to replace the V_alpha with an internal category C of some sort, and then replace "x in V_alpha" with "x is an object of the externalisation of C". The statement "for all y, phi(y) iff 'phi(y) holds in V_alpha'" can be replaced by that the externalisation of C is a subcategory of E, and that the embedding preserves various things, including the formula phi. [My scant knowledge of such thing as externalisations comes from Phoa's notes on fibrations, topos theory, the effective topos and modest sets. Apologies if I use terminology specific to those notes.] The V_alpha give subcategories of the universe of ZF in a fairly strong sense, but I think it's enough to have C an internal category, such that the externalisation of C is a full subcategory of E, in an appropriate fibrational sense. [This is probably far more than is needed]. The tricky bit appears to be to get the notion of the inclusion preserving phi(x) right. I think that just taking phi(x) to be an arbitrary formulae of the first order language of categories should be sufficient. There are very likely problems with differences between satisfaction in C and satisfaction in its externalisation, but I'm ignoring this (fingers crossed). Perhaps the formulae phi could be replaced by finite sketches in an appropriate manner (cf. Barr & Well's book), so as to get rid of logic, as well as set theory. I think we end up with something like the following definition: A topos E "has reflection" if: for all finite sets {phi_i(x,y,z,...)} of formula of the first order language of category theory, and objects/arrows (as appropriate) a,b,c,... of E there are: (a) an internal category C in E. (b) a functor F embedding the externalisation of C (a fibration over E) into the usual fibration of E^{arrow} over E. This functor should be at least full and faithful [maybe F needs to be defined in some natural way]. such that the following hold: (c) a,b,c,... are in the image of F. (d) For any I, and x,y,z,... in the fibre of the externalisation of C over I, a formula phi_i(x,y,z,...) [from our finite set] should hold if and only if phi_i(Fx,Fy,Fz,...) holds in the fibre of E^{arrow} over I. Whew! Does this make any sense at all? I hope so, but I wouldn't be surprised if it didn't. (3) Let's do a sanity check to see if our definition looks anything like the reflection principle of ZF. V_alpha certainly generates a subfibration of the fibration of V over itself. There's a slight problem with the fibres over I where I is not in V_alpha, in that the morphisms of that fibration won't generally be in V_alpha. However, I don't think that's a problem: since Set is well pointed, hopefully we can restrict to the fibre over a singleton (?), and which reduces us to the situation of V_alpha being a subcategory of V. That the inclusion of V_alpha in V is full is essentially just the fact that V_alpha is closed under cartesian products (for alpha a limit) and subsets, so if A,B are in V_alpha, then the functions from A to B are also in V_alpha. The statement that phi holds in V_alpha if and only if it holds in V seems to be the same, at least after translating a formula of category theory into a formula of set-theory (morphisms are sets of ordered pairs etc.) So things don't look too bad. That the language of set-theory has much more than category theory (under this translation) tempts us to make C an internal topos, but this isn't needed: Lemma (I hope). Let E be a topos with reflection. Then E has an internal topos. Proof. The statement that something is an elementary topos is well, elementary, and finitely axiomatised (terminal object, pull-backs, cartesian closed, subobject-classifier). Apply reflection to the appropriate sentences of first order logic axiomatising toposes. Since they are true in E, they are also true in the appropriate C, and thus we get an internal topos. Oh, better make this non-trivial (assuming that E is non-trivial), "there is an arrow which isn't an iso". Lemma. This internal topos can be taken to be a full sub-topos of E in some appropriate sense. Proof. As above, but also reflect the formulae "(f',g') is the pull-back of f and g", "x is a terminal object", "tau: x --> omega is a sub-object classifier" etc. O.k., how about this: Lemma (fingers crossed). Let E be a non-trivial topos with reflection. Then E has a natural numbers object. Proof (very sketchy). Let C be a non-trivial internal topos, as above. We know that a (internal) topos has coproducts. Therefore we can generate a minimal subobject (in E) N of C that (i) contains the initial object of C, (ii) is closed under x |--> x+1 (the coproduct with the terminal object, in C). Hopefully it's not too hard to show that x|-->x+1 and 0 give N isomorphic to N+1 (in E), which along with minimality gives us a natural numbers object. [I've entirely glossed over the non-uniqueness of co-products etc., I think this can be made good by a quotient.] (4) Why should anyone be bothered with all this stuff? (i) Hopefully it should give a nice topos-theoretic account of ZF, independent of anything about elements etc. (ii) The main application of reflection principles that I know of, outside of set-theory, is category theory. This makes (i) a little more important. The reason is that reflection principles give us a nice, and very general, way of working around small/large issues, which are normally glossed over in category theory texts. [This is not a criticism---category theory is about category theory, not "limitation of size". But it would be nice to put it on a sound category theoretic basis.] An example. In Mac Lane and Moerdijk, page 12, it is stated that "In general we shall not be very explicit about set-theoretic foundations, and we shall tacitly assume that we are working in some fixed universe U of sets. Members of U are called small sets, whereas a collection of members of U which does not itself belong to U will sometimes be referred to as a large set." For concreteness, I'll assume that U is the universe of ZF; although the following remarks seem in principle to be independent of this. On M&M, page 182, we have Corollary 4. All toposes E have finite colimits. So, having verified that the category Set^C of presheaves over some C^{op} is a topos, we are justified in deducing that Set^C is also has finite colimits? Not quite. The problem is that the proof M&M give of corollary 4 really only applies to small toposes; looking at the proof given, it uses too much in the way of large functors etc. to apply directly to large toposes. Now, we could work around this directly; by replacing the argument for corol. 4 given with an elementary one using diagram chasing. This in principle possible, at least for this result; both M&M and Johnstone give examples (initial object and coequalisers) that should suffice to convince all but the most strong-hearted that in general this would not be desirable. It also not "modular"---in the sense that a mathematician from another field wishes to do this, (s)he has to learn enough about monads etc. to actually carry this out. Another possibility, is to use the completeness theorem from logic---since the result is elementary, and has a proof for small toposes, it has an elementary proof, and thus can be carried out in a large topos. This is unsatisfactory for several reasons (a) it only works for theorems; if corol. 4 was merely a conjecture, or the hypothesis of an argument, then the technique doesn't work [this is a slight over-simplification]. (b) it depends on the logic of the universe U being classical, or at least being formalised in such a way that a completeness result holds. (c) it is not a formalisable method; if you have a recursively axiomatised logic, including arithmetic, in which this method can be formalised, then using Godel's incompleteness theorem, it is possible to show that the logic is inconsistent. O.k., so a quick proof of Corollary 5. Let E be a large topos. E has finite colimits. Proof. Let d be a finite diagram in E. Apply the reflection principle simultaneously to the formulae "E is a topos" and "The finite diagram x has a colimit". We now get a small sub-universe V (containing d) internal to which "E is a topos" holds. It is trivial (bounded formulae) to verify that the two formulae above are absolute, in the sense that they are independent of the universe they are interpreted in. Thus "The diagram d has a colimit in E" holds internally to the universe V, using corollary 4, and thus d has a colimit in E. (5) The other direction? Construct a model of ZF from a topos E with reflection. Should be possible. The main things would be to construct, using reflection, the cumulative hierarchy indexed by an arbitrary well-founded relation in E. Taking an appropriate "directed limit" (this would need to be done outside of E, as if E had the colimit, presumably one could recover the Burali-Forti paradox.) should give us the required universe. Anyway, this is far too long. Once again, comments welcome, even if it's to tell me where I'm talking nonsense. Ralph Loader. From cat-dist@mta.ca Tue Mar 19 20:59:40 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA23443; Tue, 19 Mar 1996 20:59:40 -0400 Date: Tue, 19 Mar 1996 20:58:37 -0400 (AST) From: categories To: categories Subject: [cfp]: algi3 Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Tue, 19 Mar 1996 18:20:46 +0900 From: AKAMA Youji Call for Participation The Third Seminar on Algebra, Logic, and Geometry in Informatics (ALGI 3) April 3-5, 1996 Keio University, Mita, Tokyo The ALGI (Algebra, Logic, and Geometry in Informatics) seminar is a series of informal peripatetic seminars in Japan (hopefully extending to other areas of Eastern Asia / Oceania) on the interaction between informatics and mathematics. Information about ALGI seminars can be found at "http://www.etl.go.jp:8080/People/yoshiki/ALGI-e.html". For the third meeting, watch "http://nicosia.is.s.u-tokyo.ac.jp/~akama/algi3.html". The third ALGI meeting will be held as one of the post-conference workshops of Linear Logic 96 (held at Keio University, organized by Prof. Mitsu OKADA). The scope of ALGI includes Linear Logic, but is not restricted to it. We expect offers of talks about informal, half-baked works, as well as completed ones. Participants should fill in the registration form below and send it to "algi3@is.s.u-tokyo.ac.jp". * Date: 3 April 3:30pm - 5 April. * Place: Keio University, Mita-Campus (downtown Tokyo, 5 minutes walk from JR-Tamachi St or Subway-Mita St). AV Hall, Basement of Library * Program: To be decided. * Schedule 3 April 3:30pm-5:40 pm 4 April: 10:00am-5:40pm 5 April: 10:00am- * For program/registration/hotel information for Linear Logic 96, see "http://abelard.flet.mita.keio.ac.jp/person/linear96/hotel.html". * Registration: Please send the registration form to Yohji AKAMA (algi3@is.s.u-tokyo.jp). * Tentative list of speakers: Yasuo Kawahara (Kyushu University) Categorical Representation Theorem of Fuzzy Relations. Vaughan Pratt (Stanford University) Chu spaces, Satoshi Matsuoka (Nagoya Institute of Technology) A p-time correctness condition for MALL proof nets. Yohji AKAMA and Seiko MIKAMI (The Univesity of Tokyo) Study on Abramsky's Proof Expressions Berndt Farwer (University of Hamburg) Relating object systems to formulae of infinitary linear logic Yoshiki Kinoshita (ETL) A proof of coherence theorem for monoidal categories (talk given in Japanese; draft in English available) Masaru Sirahata (Jaist) A note on proof-theoretic aspects of compact closed categories Masahito Hasegawa (Edinburgh University) Recursion from Cyclic Sharing. Peter O'Hearn (Queen Mary and Westfield College) To be announced. Luke Ong (Oxford University and National University of Singapore) A semantic view of classical proofs: type-theoretic, categorical, denotational characterizations. * General inquiry: Yohji AKAMA, Department of Information Science, The University of Tokyo Hongoh, 7-3-1, Bunkyo-ku,Tokyo, 113, Japan. 03(3812)4177(direct), 03(3812)2111(ext.4097), 03(3818)1073(fax) akama@is.s.u-tokyo.ac.jp ===================================================================== ALGI Registration form Please use the following format: I intend to come to the 3rd meeting of the ALGI seminar. * I intend to give a talk entitled ......... * I will need approximately......minutes Name ....................................... Address .................................... ............................................ Email ..................................... Tel ..................................... Fax ..................................... *Delete if inapplicable Please inform us if you need anything else besides blackboard and OHP Please inform us (in)convenient day of your talk. From cat-dist@mta.ca Tue Mar 19 21:00:35 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA24654; Tue, 19 Mar 1996 21:00:35 -0400 Date: Tue, 19 Mar 1996 21:00:30 -0400 (AST) From: categories To: categories Subject: Re: defining sets from abelian groups Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Tue, 19 Mar 1996 15:12:22 -0500 (EST) From: Andre Joyal Peter Freyd's assertion > Let Gr be the category of all groups, > abelian or not. Then: > > The category of co-groups in Gr is equivalent to Set. > is slightly incorrect. A better formulation should use the category $Set_*$ of pointed sets instead of $Sets$. As such this is essentially an old result of Peter Hilton and Beno Eckmann. They proved that any cogroup in the category of groups is free. I would like to say that the younger generation is not always aware that Eckmann and Hilton have fundamental contributions to category theory. They have provided basic examples of objects equipped with algebraic structures in categories. Consequently opening the road to further abstractions, like the concept of algebraic theory in the sense of Lawvere. Among other things, Eckmann and Hilton where interested in identifying all cogroups in the homotopy category $hTop_*$ of pointed topological spaces. A basic example of such cogroup is the circle $S^1$. It explains why the functor $\pi_1(-)=[S^1,-]:hTop_*\to Sets$ has a natural group structure. If $G$ is a cogroup in $hTop_*$ then so is the smash product $X\smash G$ for any pointed topological space $X$ This is because $X\smash(-)$ preserves coproduct since it has a right adjoint (here we are supposing that Top is a convenient category of topological space). In particular, the spheres $S^{n+1}=S^n\wedge S^1$ have a cogroup structure. Any wedge (topologists call the coproduct the wedge) of cogroups is obviously a cogroup. In particular, any wedge of spheres of dimension $n\geq 1$ has a co-group structure. All the known examples of cogroups in $hTop_*$ are obtained by taking a smash $X\smash S^1$. It was conjecture by Eckmann and Hilton that all cogroups in $hTop^*$ are of the form $X\smash S^1$. They observe that $\pi_1(G)$ is a cogroup in $Groups$ when $G$ is a cogroup in $hTop_*$. This is because the functor $\pi_1: hTop_*\to Groups$ preserves coproducts by Van Kampen theorem. In support to their conjecture they proved that any cogroup in $Groups$ is free. It follows that all cogroups in $Groups$ are of the form $\pi_1(X\smash S^1)$ where $X$ is a pointed set. Andre Joyal From cat-dist@mta.ca Wed Mar 20 11:41:25 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA24530; Wed, 20 Mar 1996 11:41:24 -0400 Date: Wed, 20 Mar 1996 11:40:06 -0400 (AST) From: categories To: categories Subject: Definition of "definable in" Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Tue, 19 Mar 1996 19:57:06 -0800 From: Vaughan Pratt After giving more thought to my question about Set vs. Ab I decided that it was hopeless to try to resolve as a theorem, and that the only way out was to resolve it with a definition. Definition. A category C is *definable in* a closed category D when it embeds fully (as a category) in every self-dual closed category embedding D (as a closed category). This definition settles by fiat the question of whether *finite* sets can be defined from finite groups, since FinAb is self-dual, as I mentioned previously. Extending this to Ab is a matter of checking that Set does not embed in Ab\op x Ab, which would surprise me greatly. If Set actually does embed in Ab, as some have been telling me privately, this does not contradict my definition, it merely answers my original question in the other direction. To convince me that Set embeds in Ab it will suffice for you to give me representatives of 2 and 3 whose homobjects between them are the representatives of 4, 8, 9, and 27. If you have a more productive notion of "definable in", meaning one that lets you define categories not possible with the above, there is a possibility that some trace of Set has leaked into your definition. If, after convincing yourself that all traces of Set have been eliminated, it is *still* more productive, then this would be a notion of "definable in" well worth discussing. Vaughan Pratt From cat-dist@mta.ca Wed Mar 20 14:49:38 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA12449; Wed, 20 Mar 1996 14:49:38 -0400 Date: Wed, 20 Mar 1996 14:48:23 -0400 (AST) From: categories To: categories Subject: Proof of nonexistence of membership Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Wed, 20 Mar 1996 10:25:56 -0800 From: Vaughan Pratt It occurs to me that the arguments that have been advanced against membership can be strengthened to a mathematical proof that the usual notion of membership as a 2-valued binary relation is an inconsistent notion. That is, Theorem. Membership does not exist. Proof. Clearly the universe exists, or we're in serious trouble. But if membership also exists then the Cantor-Russell argument leads to a contradiction. QED My real point here is that the Cantor-Russell argument doesn't *really* prove there is no universal set, or no 2-valued membership relation, or that some sets we can name are not in the universe, or that the universe we exist in must be different from the one in which mathematical objects exist, or that we are arguing with an unreliable logic. What it proves is the sentence "false." Anything powerful enough to prove false is a theorem of the universe dual to ours. Such a theorem is a gedanken wavefunction. To bring it into our universe it has to collapse to a Gedankeneigenfunction of the operator by which we observe it, that is, our logic. When you are young and unobserved you are just some gedanken wavefunction. When you become observed, whether for the purpose of influencing future generations or getting tenure, you collapse to one of the schools of thought constituting the Gedankeneigenfunctions of the observation operator, whether set theorist, or category theorist, or intuitionist, etc. That is, you have to take a stand or risk failure to communicate. I have tried to communicate without taking a stand. I may have underestimated the disadvantages of not collapsing to a Gedankeneigenfunction. There's a lot to be said in favor of collapse. Vaughan Pratt From cat-dist@mta.ca Wed Mar 20 21:03:11 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA01676; Wed, 20 Mar 1996 21:03:10 -0400 Date: Wed, 20 Mar 1996 21:02:02 -0400 (AST) From: categories To: categories Subject: Re: Proof of nonexistence of membership Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Wed, 20 Mar 1996 15:58:58 -0500 (EST) From: MTHISBEL@ubvms.cc.buffalo.edu Dear QED, Your proof of nonexistence of the universe is short and convincing. But why do you call it membership? John Isbell From cat-dist@mta.ca Thu Mar 21 11:10:04 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA28564; Thu, 21 Mar 1996 11:10:04 -0400 Date: Thu, 21 Mar 1996 11:08:33 -0400 (AST) From: categories To: categories Subject: Re: Proof of nonexistence of membership Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Wed, 20 Mar 1996 18:48:59 -0800 From: Vaughan Pratt From: MTHISBEL@ubvms.cc.buffalo.edu Your proof of nonexistence of the universe is short and convincing. But why do you call it membership? Bill Lawvere visited Stanford in 1988 to give a talk and share ideas. I vaguely registered that his (cream-colored?) jacket had a Members Only label, and I found myself wondering why I was noticing such a trivial detail, and why it kept coming back to haunt me in the intervening years. As I stared at your message, John, trying to decide which of its ten meanings you most likely intended, free associating like crazy, suddenly the irony hit me. Thanks! God knows how much longer it would have taken otherwise for my subconscious to deliver this particular message. I should explain what gave rise to my very off-the-wall posting. I'd asked a well-known set theorist where set theorists preferred to set the boundary between the ordinals that existed and those that didn't, or whether they didn't try, and the exchange that followed was about what you'd expect of two explorers from different solar systems meeting and trying to find a common alphabet, lexicon, syntax, and semantics in that order. But we got there, and I thought, ah, *this* must be what a wavefunction feels like when its pushed out of one eigenstate of an operator into another. (Nothing contradictory there when you analyze it in terms of a second operator whose eigenstates are different from the other one, applied for the purpose of temporarily getting out of an eigenstate of the other operator.) The metaphor doesn't have to be quantum mechanics. Instead of two operators you could have two drains and one plug in your bathtub. The water will pick a direction to swirl as one of the two eigenstates of the open drain, and will then get nudged out of that eigenstate when you move the plug over to the other drain. The first open drain represents conferences and journal publication in some discipline, and its eigenstates represent schools of thought in that discipline. The other represents a method of getting out of the rut so that you have a chance when you do go back to the first drain of finding yourself in the other eigenstate. Provided the operators are sufficiently orthogonal you can expect this method to succeed after two tries on average (1/2 + 1/4 + 1/8 + ...). I only know of analog metaphors for this phenomenon, which it seems to me nicely describes the relationship between the competing schools of foundations and the Cantor-Russell-Goedel paradox. (To which some people these days add Heisenberg, I'm on the side that likes this connection, but there's plenty on the other side too.) In the absence of discrete metaphors I'm not sure I can add anything helpful to this. If the above doesn't do it, well, it was just a silly idea then. Vaughan From cat-dist@mta.ca Thu Mar 21 11:10:10 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA23327; Thu, 21 Mar 1996 11:10:09 -0400 Date: Thu, 21 Mar 1996 11:09:41 -0400 (AST) From: categories To: categories Subject: Choice, inclusions, nonstandard analysis Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Thu, 21 Mar 1996 03:33:55 -0800 From: Vaughan Pratt Contents: 1. Defense of Choice 2. Toposes with inclusion 3. Nonstandard analysis without tears. (Sorry this got so long.) From: peterj@maths.su.oz.au Vaughan Pratt seems to be challenging the rest of us to find something wrong with his ordinal-based definition of Set, and no-one else has taken up the challenge; so I'll have to break my vow and point out its obvious shortcoming. Peter's points are sufficiently well taken as to deserve both careful reflection and measured response. I apologize for the one-liner on Monday referring to Peter's Sunday message in the middle of a postscript advertising my LL'96 paper, which violated both of these. Cryptic responses only clog everything up. Peter argues that Choice should be avoided in constructions, on the following ground. I suppose only a minority of mathematicians are unhappy about AC to the extent of actually rejecting any construction that can't be done without it. But I think a very large majority would be unhappy about calling upon God to construct things for them (such as the real numbers) for which they know there is a perfectly good man-made construction. Such people are going to be in a near- permanent state of unhappiness if they are condemned to do mathematics inside Vaughan's category. =================== 1. Defense of Choice Before I address the distinction Peter draws here between natural chaos and mathematical artifact, I'd like to put in a word for Choice, which Peter isn't exactly leaping to defend. Using Choice is like wearing eyeglasses. The wearer barely sees them but sees the world more clearly. The *observer* of the wearer on the other hand sees the glasses directly as the wearer's baggage or ornament, and is only indirectly aware of the wearer's improved vision. Using Choice lets you prove more theorems, but they also shorten existing proofs, sometimes significantly. There is no shortage of examples, but just to point to the case under discussion, if you organize a category-with-epsilon-trees along the lines I was suggesting, the construction of epsilon reduces to the equation \epsilon = <. At a fraction of a line, this is significantly shorter than the published constructions, which seem to require a lot more. Long proofs cloud our mathematical vision. A shorter proof shows us the same result but by a path that makes its truth clearer. The proof as the means is a sine qua non, but that does not make it the end, the truth is the end (wearing my Platonist hat for now). The counterpart to the observer of the wearer of eyeglasses is that movie critic of the foundations world, the axiom system critic who worries about excess baggage, ornamentation, and/or legislation. Why interfere with the natural course of things when with just a little accommodation of nature by longer proofs we can leave her unfettered by legislation? Unfortunately all known ways of building a house seem to entail some disturbance of nature, and this commendable environmental concern is in impractical conflict with the requirement that your house have a picture window with a clear view of mathematical truth. Quantum mechanics and Choice are in much the same boat. Neither makes as direct contact with the truth as F=Ma or x+y=y+x, but both are better understood as sharpening vision, providing respectively the physicist and the mathematician with eyeglasses. In time they may come to feel like absolute truth, but this is a slow process. Arguing against Choice, understood internally, applies nonmonotonic logic to restrict what can be deduced. It is fundamentalist in its rejection of sophisticated reasoning supporting clear thinking. (Sorry if that's too cryptic, happy to explain privately if this worries you.) ============= 2. Toposes with inclusion Such people are going to be in a near- permanent state of unhappiness if they are condemned to do mathematics inside Vaughan's category. At first I had interpreted this to mean that mathematicians would be unhappy working with reals that had bits of the membership relation dangling off them. This seemed no objection at all; of course the user doesn't want construction materials on his nice stuff. The builder has to clean up after construction, or the user isn't obliged to pay the bill in full. But even if the builder doesn't do it, the user can always spend a bit extra to do it himself, and the upshot is the same. But a day or so later, after rereading even if [AC] does [hold], you don't have the ability to point to a particular object of it and say "This is the set of real numbers" (still less to point to a particular morphism and say "This is the addition operation on real numbers"); you have to rely on God's (or "the randomizer's", as Vaughan seems to call him) ability to do it for you. it occurred to me that perhaps Peter was interpreting my construction as meaning quite literally that I was proposing to name reals with ordinals. This certainly would make the users permanently unhappy. My interest in this stuff is ultimately as a user, and I would be unhappiest of all because such a user-unfriendly system would have been my fault, and because it would have been a complete waste of effort. I suppose I could just ask Peter which he meant (or was it something else again?). However both are plausible concerns, and I can think of equally good and more or less independent responses to them, which I'll give now. For the first, I'll define what I'll call for the moment an itopos, for topos-with-inclusion, along with a forgetful functor from itoposes to toposes. (This might be better done for categories in general; here I'm only concerned about clarifying one topos.) For the second I'll point to a particular object of my category and say "This is a monoid embedding the monoid of nonnegative reals as its bounded sequences, the rest being nonstandard reals", and point to a particular morphism and say "This is the addition operation on this monoid, whose restriction to the standard nonnegative reals is standard addition"). This will do double duty as a constructive refutation of Peter's objection and as an interesting (to me), short, and I believe new construction of the reals that bypasses *all* the many intermediate constructions in the standard constructions, *and* produces the nonstandard reals more simply than previous constructions (that I'm aware of) as a potentially useful spinoff. A topos with inclusions is no big deal (though it might be if worked out more carefully than here). Its point is to make explicit the identity of the elements of sets, in part because it is useful in its own right in some situations, in part because it clarifies what is being erased when we claim to erase construction details. The identities of a topos are those of a category, defined by a map i:O->M. An *itopos*, or topos with inclusions, extends the notion of identity to a preorder on the objects as a subcategory of the topos. An *extensional* itopos makes this a partial order. This entails an extension not so much of the signature of a topos itself as just an increase in the arity of identity, as a function from objects to morphisms, from one to ordered two, i.e. not just the diagonal but the "upper triangle" of the homfunctor when a partial order, plus squares on the diagonal when a preorder. The inclusions need to be coordinated with the topos structure, not done here (a good thing too if this is all old hat, which seems rather likely given that it is a rather obvious notion). The strict inclusions for the itopos OSet (for Ordinal Set) that I constructed the other day were already described then as the nonidentity maps from i to j that are the left inclusion of i into i+(j-i). In other words just ignore the excess of j over i and map bijectively and monotonely to what remains of j. Application. In an itopos one can define the usual Boolean operations on sets in the (large) distributive lattice of inclusions (omit the downward remainders), knowing that the intersection of two sets contains the very elements that show up in common in those two sets, not mere stand-ins for them. Cleaning up. There is an evident forgetful functor from OSet to Set, obtained by decrementing the arity of identity to leave only the diagonal identities, those in Set(X,X). The practical impact of forgetting the nondiagonal identities is that functors between toposes need preserve only the retained identities. If you find a need to preserve epsilon structure, it means you should be working in the itopos. This addresses Mike Barr's point, which he mentioned as confirming with Makkai, about most applications ignoring the epsilon structure. Erasing the off-diagonal identities makes it official. =============== 3. Nonstandard analysis without tears Definition. The nonstandard nonnegative reals form the set \omega^\omega of sequences of natural numbers, modulo the following two equational universal Horn clauses whose variables range over sequences, with addition understood as pointwise. 1. 2(a/2) = a 2. a + c = b + c -> a = b The function 2a doubles every element of sequence a: (3,2,..) |-> (6,4,...) The function a/2 shifts the sequence right, setting the leading digit, indexed by 0, to 0. (3,2,...) |-> (0,3,2,...). Think of halving a binary numeral by shifting. End of construction. It can easily be seen that the clauses will not identify an unbounded sequence with a bounded one. The standard nonnegative reals are extracted from this monoid as the (equivalence classes of) bounded sequences. The real denoted by the sequence a_i is sum(a_i / 2^i),i<\omega, in other words ordinary binary notation. Example. The ultimately constant sequences (1,0,0,0,...) and (0,1,1,1,...) denote the respective reals 1.00... and 0.111... in binary notation. These are identified by the following computation: 1.111... = 0.222... by 1 1.000... = 0.111... by 2, with c = 0.111... A little work shows that every bounded real is identified by clauses 1 and 2 with a sequence all of whose elements but the leading "digit" are 0 or 1, and which if ultimately constant ends in 0's. This of course is the standard binary representation for real fractions, but with a single digit in "radix" \omega for the integer part. It should be clear that pointwise addition is ordinary real addition for such reals, with infinite carries propagating in finite time as in the example. This construction makes these standard and nonstandard nonnegative reals a monoid. The same technique that extends the natural numbers to the integers extends these nonnegative reals to the standard and nonstandard reals, of which the standard reals then form a ring (define multiplication as all endomorphisms of the monoid, made a binary operation by associating each endomorphism with where it sends 1) and a field as usual, the standard field of reals. Every real in this monoid being bounded away from zero, the whole monoid without the nonstandard reals cannot form a field, though the above definition of the ring satisfies the ring axioms by construction. But we can easily extend it to a field by the same means by which the integers are made the field of rationals: define an ireal (possibly infinite or infinitesimal real) to be a pair a/b of nonstandard reals, modulo the implication ad = bc -> a/b = c/d. This produces with very little fuss a field suitable for nonstandard analysis without tears. These constructions can all be carried out as operations on objects of the category Set, as a topos obtained by my construction from OSet. All terms used in the construction are made explicitly available in the construction I gave, as part of its signature as a bicomplete topos. No trace of the randomness in the choice of well-ordering of \omega^\omega participates in the construction, which should be understood as merely proving existence and properties of the topos thereby constructed, with the proof erased when done. Here is an indication of how this construction could go, at least for the nonstandard reals. Start with two copies of \omega^\omega, for respectively a and b in clause 2 of the definition. Make \omega^\omega copies of \omega^\omega, one for each c. From the copy for c, delete all sequences pointwise less than c. Send maps a+c, b+c from a,b to c respectively. Now make one more copy of \omega^\omega and send maps x-c from c to it. (Note that monus never "underflows", because we deleted those elements.) The colimit of this diagram implements 2. 1 is an easy coequalizer. That's it. For the promised addition morphism, very roughly speaking, start from +:\omega^2->\omega, form +^\omega, and apply to this morphism the same operations that were applied above to the objects, all of which are functorial. Getting from here to the ireals is a matter of constructing the "integers" then the "rationals" with any standard approach, starting with \omega^\omega instead of \omega. This construction was described as an infinite diagram for conceptual simplicity. It can be made finitary with first order logic or adjunctions, however you prefer to look at it. Hopefully all operations needed for this conversion are already in the signature provided for Set; if not the signature needs more oomph. Vaughan Pratt From cat-dist@mta.ca Thu Mar 21 13:37:34 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA08869; Thu, 21 Mar 1996 13:37:33 -0400 Date: Thu, 21 Mar 1996 13:33:38 -0400 (AST) From: categories To: categories Subject: Re: Definition of "definable in" Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: 21 Mar 96 15:59:04 +0100 From: Reinhard Brger, Prof. Pumpl n Since the set of maps from a non-empty set to the empty set is empty and since Ab x Ab\op has no empty hom-sets, there is no full embedding from Set to Ab x Ab\op. Does that answer your question? Reinhard Boerger From cat-dist@mta.ca Thu Mar 21 13:37:39 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA08918; Thu, 21 Mar 1996 13:37:35 -0400 Date: Thu, 21 Mar 1996 13:34:51 -0400 (AST) From: categories To: categories Subject: Mechanization of category theory Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Thu, 21 Mar 1996 15:00:08 +0100 From: Clemens Ballarin Has anybody experience in mechanizing category theory or knows of such work? I'm about to implement basic parts of category theory in a tactical theorem prover based on higher order logic. I would appreciate to learn from anybodies earlier experiences. Thanks in advance, Clemens From cat-dist@mta.ca Thu Mar 21 13:37:51 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA08922; Thu, 21 Mar 1996 13:37:50 -0400 Date: Thu, 21 Mar 1996 13:36:30 -0400 (AST) From: categories To: categories Subject: Money_Games Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Thu, 21 Mar 1996 11:48:11 -0500 (EST) From: Andre Joyal My paper "Free Lattices, communication and money games" is available on the WWW at: http://www.math.uqam.ca/_rapports/joyal/Money_Games.html It is to appear in the Proceedings of the International Congress of Logic, Methodology and Philosophy of Science held in Firenze, August 1995. Andre Joyal From cat-dist@mta.ca Thu Mar 21 13:38:16 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA06237; Thu, 21 Mar 1996 13:38:15 -0400 Date: Thu, 21 Mar 1996 13:35:34 -0400 (AST) From: categories To: categories Subject: Re: Choice, inclusions, nonstandard analysis Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Thu, 21 Mar 1996 16:53:46 +0000 From: Steve Vickers >Arguing against Choice, understood internally, applies nonmonotonic >logic to restrict what can be deduced. It is fundamentalist in its >rejection of sophisticated reasoning supporting clear thinking. (Sorry >if that's too cryptic, happy to explain privately if this worries you.) There's a sense in which by reasoning non-classically (specifically, with geometric logic) you can eliminate the need for explicit topology: if you define points by a geometric theory, then the topology is implicit if you define a map by geometric constructions, then continuity is automatic >From this point of view, the purpose of explicit topology is to correct the errors introduced by classical reasoning. We thus see sophisticated reasoning (classical principles) necessitating complicated thinking (topology), the reverse of what was intended. You don't need dogma to see this could be a bad idea, though you do need hard work to see whether the classical principles really can be dispensed with. Steve Vickers. From cat-dist@mta.ca Thu Mar 21 23:15:19 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA15465; Thu, 21 Mar 1996 23:15:18 -0400 Date: Thu, 21 Mar 1996 23:14:17 -0400 (AST) From: categories To: categories Subject: Re: Definition of "definable in" Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Thu, 21 Mar 1996 13:08:38 -0800 From: Vaughan Pratt From: Reinhard Brger, Prof. Pumpl n Since the set of maps from a non-empty set to the empty set is empty and since Ab x Ab\op has no empty hom-sets, there is no full embedding from Set to Ab x Ab\op. Does that answer your question? Not if I understand you, for two reasons. First, you said the word "hom-set" which isn't allowed in Ab---you have to say homgroup (or homab). There being no empty group, if Set embeds in Ab then the empty set must embed as a nonempty group. Emptiness in the sense definable via the forgetful functor U:Ab->Set is not a predicate known to be in Ab. Emptiness needs to be defined in terms of the Abelian group representing the empty set. You have to analyze any proposed embedding by treating both the objects and the homobjects between them as Abelian groups. The second problem is my fault. I noticed yesterday that my definition (repeated below, near the end) is too weak. As a simple counterexample, groups are well known to be definable in Set, but Grp certainly does not fully embed as a category in the closed self-dual category Set + Set\op (= Chu(Set,0)), which embeds Set as a closed category (that is, the embedding respects tensor products, not necessarily cartesian products). The objects are just sets and antisets, clearly nowhere to store Grp. I was basing my definition on two theorems of mine. 1. Every category of relational structures, and hence every full subcategory thereof definable by any wacky language you want, far wilder and less computable than first order logic, fully embeds in Chu(Set,2^k) where k is the total arity of the structure. To determine total arity k of a multisorted multirelation structure, form the disjoint union of all the carriers, add one unary predicate per carrier as a marker, and then form the "natural join" of all the relations. The embedding works for total arities up to any ordinal; for a proof look near the end of http://boole.stanford.edu/gamut.ps.gz 2. Every small concrete category embeds in Chu(Set,K) for some set K. Proof: Take K to be the disjoint union of the carriers of the objects, and proceed as in http://boole.stanford.edu/embed.ps.gz On the strength of these two theorems I speculated that any method of defining a category that confined its language to that of V would embed in Chu(V,k) for a suitable object of k. What does "confine language" mean? Terrible things! It might even entail giving up conventional equality in favor of weighted limits when V is not cartesian closed, as with Ab. Some of you might enjoy a world where equality didn't exist, not in the sense you have to settle for in Set where you have to convince skeptical students that equality doesn't exist, but in the more pragmatic sense that no one else in that world uses it either, because it really doesn't exist! What I forget to allow for in my definition was the variability of k. Larger k lets you define more. k functions as a simple but effective and pure notion of signature. Pure in the sense that the 256 colors on your monitor are the clean signature of pixel depth, purified of the grubby representational issues implied by talking instead of the 8 pixel planes as though each plane were a real thing. This representation is clearly meaningless for people whose computers have 6 pixel planes coding 729 colors in ternary. I had foolishly thought that the essence of the Chu construction could be purified to a statement about duality, but had clean forgotten to allow for the possibility that a definitional method might cunningly think to use language to express the definition! Just how little language can be present in a self-dual category embedding Set can be can be seen from the example above of Chu(Set,0), a self-dual category consisting *only* of sets and antisets (aka CABA's if you ignore concreteness issues). The sets are realized as the inconsistent Chu spaces (A,0), the antisets as the empty Chu spaces (0,A), with (0,0) as the one set that is also an antiset. (Obviously this doesn't work for what Dusko Pavlovic calls "little Chu," no repeated rows and columns.) Chu(Set,0) understood skeletally consists of just the "dynamic integers," thinking of (0,A) as minus (A,0). The only subcategories of this sparse category have as their objects some sets and some antisets. This does not even embed Set\op x Set = Chu(Set,1), which also is too small for anything much, e.g. no posets, which enter at Chu(Set,2). I see nothing for it for now but to be upfront about putting Chu in the definition. Old definition. A category C is *definable in* a closed category V when it embeds fully (as a category) in every self-dual closed category embedding V (as a closed category). New definition 1. A category C is *definable in* a closed category V when it embeds fully in the category Chu(V,k) for some k in ob(V). This definition steers between the Scylla of arbitrarily large self-dual categories and the Charibdis of self-dual categories barely bigger than V. It is also a tad shorter. But there is *still* a problem. In Set it is not hard to define Chu(Set,*) as a colimit of Chu(Set,K1) < Chu(Set,K2) < ... For example the category of hypergraphs described in @Article( DW80, Author="D{\"o}rfler, W. and Waller, D.A.", Title="A category-theoretical approach to hypergraphs", Journal="Archives of Mathematics", Volume=34, Number=2, Pages="185-192", Year=1980) does not to my knowledge embed in any Chu(Set,K) for any fixed K. (This is an open question, I imagine mainly because no one has looked hard at it.) But any *small* subcategory of it does, by the general result above that *every* small concrete category embeds in Chu(Set,K) for some K. This too is easily fixed. There is a *nonclosed* category Chu(Set,Set). The definition looks no different from the usual definition of Chu, except that in all small interactions (no proper class of participants), all Chu spaces involved are taken to be over the colimit of all their K's. The only failure of this category to be closed is its lack of tensor unit 1 and its dual _|_ (I've switched to Girard's notation because these days it makes a lot more sense to me). The rest of linear logic is fine; furthermore the absence of 1 and _|_ removes the odd-ball property 1@1 |- 1 that Lafont and Streicher noticed. With that and MIX gone, about all LL should need now is induction, and Chu(Set,Set) should then be a complete model of LL without multiplicative units. If there is any justice, all this should generalize to Chu(V,V) by arranging to embed the k's of any interaction of V-enriched Chu spaces in the appropriate colimit of them in V before letting them interact. This leads to the even shorter: New definition 2. A category C is *definable in* a closed category V when it embeds fully in the category Chu(V,V). In view of Dusko Pavlovic's paper on the couniversality of Chu, about the only improvement likely for this definition (barring further bugs, sigh) is to replace the explicit Chu construction by its abstract properties. The effect will be the same either way, though the definition is presumably not going to get any shorter that way! One residual question is how to do enriched category theory from scratch in V. Max, help! Vaughan Pratt From cat-dist@mta.ca Thu Mar 21 23:15:20 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA15091; Thu, 21 Mar 1996 23:15:19 -0400 Date: Thu, 21 Mar 1996 23:15:15 -0400 (AST) From: categories To: categories Subject: Address:Money_Games Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Thu, 21 Mar 1996 17:38:11 -0500 (EST) From: Andre Joyal The correct WWW address for my paper "Free Lattices, communication and money games" is: http://www.math.uqam.ca/_rapports/RapportsTech.html It is to appear in the Proceedings of the International Congress of Logic, Methodology and Philosophy of Science held in Firenze, August 1995. Andre Joyal From cat-dist@mta.ca Fri Mar 22 11:35:28 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA02837; Fri, 22 Mar 1996 11:35:28 -0400 Date: Fri, 22 Mar 1996 11:30:47 -0400 (AST) From: categories To: categories Subject: Re: Mechanization of category theory Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Fri, 22 Mar 96 13:52:38 GMT From: David Rydeheard > Delivery-Date: Thu, 21 Mar 1996 17:00:00 +0000 > X-Mailer: exmh version 1.6.4+cl+patch 10/10/95 > Mime-Version: 1.0 > Content-Type: text/plain; charset=us-ascii > Date: Thu, 21 Mar 1996 16:11:48 +0100 > From: Clemens Ballarin > Sender: owner-qed@mcs.anl.gov > Precedence: bulk > > Has anybody experience in mechanizing category theory or knows of such work? > I'm about to implement basic parts of category theory in a tactical theorem > prover based on higher order logic. I would appreciate to learn from anybody's > earlier experiences. > > Thanks in advance, > > Clemens ---------------------------------------------- Clemens, there has been a good deal of work on the mechanisation of category theory. I will mention some here and I am sure others will contribute to complete the discussion. The obvious starting point (for me!) is: David Rydeheard and Rod Burstall. Computational Category Theory. Prentice Hall (1988). This describes an encoding of constructions of (finite) limits, colimits and of adjuctions and internal logics, and also constructions of categories, all coded in SML. It makes use of higher orer functions to code the universality of constructions and the parametric polymorphism to capture something of the level of abstraction of category theory. It does not include correctness proofs within the code. The code + examples are available over the WWW from my archive at Imperial College (http://theory.doc.ic.ac.uk:80/tfm/papers/RydeheardD). At about the same time as this was being developed, Roy Dyckhoff [1985] was experimenting with implementing categories in an implementation of a Martin-Lof Type theory, Joe Goguen was implementing categories in OBJ and Tatsuya Hagino was developing his "categorical data types". These are all briefly described in the above book. ----------------------- Now I come to the more invidious part: Trying to summarise what has happened since without missing important contributions. I cannot do this in an email message but will attempt to sketch some directions and others can contribute in their own messages. One major direction has been to continue Roy Dyckhoff's work, using implementations of various type theories as a basis for formalising category theory (examples that spring to mind are: Gotheberg work in Alf, the INRIA work in Coq, and the Edinburgh/Manchester (Aczel) work in LEGO). There has been other implementations of categorical algorithms and systems including that of (1) Robin Cockett and his group, (2) Carmody and Walters, (3) Michael Fleming and Ryan Gunther ftp://sun1.mta.ca/pub/sources/rosebrugh/{unix,DOS}. There have been attempts to provide interactive tools for categorical reasoning ("diagram chasing"). I believe John Gray had a Mac version. Actually an early attempt to automate categorical reasoning is that of Watjen and Struckmann (Inform. Proc. Letters 14, 3 [1982]). The work on "categorical data types" and "categorical programming languages" has continued, eg [Hasegawa, LNCS 953]. There has been work on the normalisation properties of the (essentially algebraic) theories of categories (with structure) (see eg. the PhD thesis of Wolfgang.Gehrke@risc.uni-linz.ac.at). I'm sure that I have omitted important contributions. I'll let others speak for themselves. David [Clemens, it may be worthwhile preparing and posting a comparative survey of these and other systems so that those interested can know what is available.] From cat-dist@mta.ca Fri Mar 22 11:35:30 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA03362; Fri, 22 Mar 1996 11:35:30 -0400 Date: Fri, 22 Mar 1996 11:28:34 -0400 (AST) From: categories To: categories Subject: Re: Choice, inclusions, nonstandard analysis Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Fri, 22 Mar 1996 00:44:30 -0400 From: RJ Wood I would like to comment on Vaughan Pratt's > 1. Defense of Choice ... > Using Choice lets you prove more theorems, but they also shorten > existing proofs, sometimes significantly. There is no shortage of > examples,... Write CD(L) for complete distributivity of a complete lattice L. Write CCD(L) for constructive complete distributivity of L, by which is meant that \/:DL--->L has a left adjoint, where DL is the lattice of down-closed subsets of L, ordered by inclusion. It is easy to show that CD==>CCD but many times in joint work with Fawcett, Rosebrugh and Marmolejo I have been led back to the more interesting AC<==>(CD<==>CCD) * Without choice there is not much that one can prove about CD. In fact, without choice there is a severe shortage of infinite L satisfying CD(L). (Recall that AC is equivalent to `for every set X, CD(PX), where P denotes power set'.) My experience suggests that all theorems about CD follow from constructively proveable theorems about CCD after invoking *. Those that my colleagues and I have discovered have reasonably ``short'' proofs, if one starts with some basic knowledge of adjunctions. Allow me to discharge the facile comment that by *, any theorem that has been proved constructively about CCD (examples exist) proves that ``Using Choice lets you prove more theorems'' because that is not the point of this note. Rather, I think that * and similar results show that some of the definitions and concepts that seem to arise rather ``naturally'' from traditional set-based Mathematics are not particularly natural. Stepping further away from Mathematics, I think that twentieth century Mathematics has frequently sacrificed useful generalization for excessive abstraction. RJ Wood From cat-dist@mta.ca Fri Mar 22 14:38:32 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA18122; Fri, 22 Mar 1996 14:38:32 -0400 Date: Fri, 22 Mar 1996 14:33:29 -0400 (AST) From: categories To: categories Subject: Re: Choice, inclusions, nonstandard analysis Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Fri, 22 Mar 1996 09:18:21 -0800 From: Vaughan Pratt I would like to comment on Vaughan Pratt's Phew, thanks Richard, no fun defending a position alone. Here's another argument for Choice, no more or less a proof than the clarity-of-mathematical-thought argument, it seems to me. "Proof" of AC. It took mathematics about thirty years longer to imagine AC false than it did to imagine it true. This "argument" can be applied in other situations. Applying it to Grothendieck universes (aka inaccessible cardinals) would suggest that they don't exist. We can imagine their nonexistence (their existence is independent of ZFC) but so far we haven't been able to imagine their existence (a proof in ZFC that they don't exist is still on the cards). What arguments exist in *support* of the existence of Grothendieck universes? I see the "cogito ergo sum" argument, what else? Vaughan Pratt From cat-dist@mta.ca Fri Mar 22 17:16:13 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA29090; Fri, 22 Mar 1996 17:16:13 -0400 Date: Fri, 22 Mar 1996 17:10:10 -0400 (AST) From: categories To: categories Subject: Re: Choice, inclusions, nonstandard analysis Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Fri, 22 Mar 1996 16:01:04 -0500 (EST) From: MTHISBEL@ubvms.cc.buffalo.edu Vaughan Pratt says <> I once asked Joe Shoenfield that -- not quite in those terms -- and his answer certainly didn't seem to me "cogito ergo sum". That seems to me, assuming I understand what argument you mean, not radically better than Anselm's proof of the existence of God: we can imagine the best thing in the world, and if it is the best it must exist (otherwise one that existed would be even better), so it exists, QED. Now I don't suppose you mean a White Knight's sort of argument -- the universe imagined me, therefore it exists. You mean I imagine Grothendieck's universe, therefore IT exists. Well, Joe said in effect I can tell you everything that goes to make up the first Grothendieck universe, except I don't have time to finish telling you. It's the null set, and the singleton of the null set, and [and on. Not just countably, of course; we can describe \omega very satisfactorily, and the union of an omega-sequence of ordinals, and on. This differs from Anselm's word game in being a string of constructions. The first Grothendieck universe is rather large, so it is a fairly formidable kit of constructions. Pass to a second Grothendieck universe, and you used at least one miracle, to produce an individual from the first-universe construction. John Isbell From cat-dist@mta.ca Sun Mar 24 20:55:16 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA00481; Sun, 24 Mar 1996 20:55:15 -0400 Date: Sun, 24 Mar 1996 20:53:58 -0400 (AST) From: categories To: categories Subject: Toronto Spring Meeting -- Final Announcement Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Fri, 22 Mar 1996 16:14:30 -0500 (EST) From: York cat TORONTO SPRING MEETING A Weekend Meeting on Category Theory and Its Applications YORK UNIVERSITY, North York (Metropolitan Toronto) Saturday/Sunday, April 13/14, 1996 FINAL ANNOUNCEMENT The meeting will begin on Saturday, April 13, with the first talk at 9 a.m., and end before 2 p.m. on Sunday. If you wish to attend the meeting and if you have not sent your registration form yet, please do so at your earliest convenience - especially if you wish to book a room through yorkcat or if you wish to give a talk, and in any case before April 7. This will give the organizers a chance to finalize hospitality arrangements in good time. Send the form attached below to yorkcat@mathstat.yorku.ca. All talks at the meeting will be held in VARI HALL, Lecture Room D. Vari Hall is located centrally on the York Campus at 4700 Keele Street in North York. It is just east of the Ross Building, a large grey building visible from everywhere; Vari Hall is a yellow brick building in front of Ross, with a rotunda which connects it with Ross. Enter the building at the rotunda and follow the signs to Lecture Room D. The busline 106 connecting the closest subway station (SEE IMPORTANT NOTE BELOW) with York has its terminal stop almost in front of Vari Hall. If you travel by car, turn west from Keele Street into York Boulevard (main gate of the campus) and use the first parking lot on the right (Lot 1A); the fee is $5 on Saturday and $0 on Sunday. Walk west towards Vari Hall. Slightly closer to Vari Hall is Lot DD where the Saturday fee is $7. The registration desk in front of Lecture Room D will be open beginning from 8:45 a.m. on Saturday. The fee of $25 for participants with full employment ($12 for others) will be used to pay for refreshments during the meeting and for lunch on Saturday. Participants and their spouses/friends are invited to a Welcome Party (wine and cheese) at Walter Tholen's home on Friday night (April 12), beginning from 8 p.m. Address and directions (car and public transport) will be sent by email to each participant. This mailing will also contain a short (and necessarily subjective) list of recommended restaurants and Saturday night outings. Complete information on Saturday night entertainment in Toronto as well as on restaurants can be obtained by visting the conference web site at http://www.math.yorku.ca/Who/Faculty/Tholen/tsm/tsm.html Follow the various links to Toronto information sites. Most complete entertainment coverage is at the electronic site of "Eye Weekly Magazine" which will have up-to-date theatre/music/movie listings etc for the weekend of April 13/14 beginning from Thursday, April 11. There are also links to maps (city and campus), weather forecast, and other potentially useful information sites. IMPORTANT NOTE FOR PUBLIC-TRANSPORT USERS The Toronto subway system is currently undergoing a small extension program which affects travel to York University. Beginning from April 1, the closest subway station is no longer "Wilson", but "Downsview". Hence, in the directions given in the Second Announcement, "Wilson subway station" has to be traded for "Downsview subway staion" as the starting point of bus line 106 leading to York University. New bus and subway schedules have not been issued yet, but changes are to be expected marginal since the new Downsview terminal is just one stop further than Wilson. We hope to see you at the Meeting! Xiaomin Dong Sandro Fusco Joan Wick Pelletier Walter Tholen ********************************* CUT HERE ************************************ Registration Form - Toronto Spring Meeting (To be returned to yorkcat@mathstat.yorku.ca at your earliest convenience) Name: I intend to attend the meeting: Yes/No I intend to give a talk: Yes/No/Do not know yet Title: (desired length 20/30 min.) Only if applicable, fill out the following: I would like to reserve - a room in a student dormitory from (arrival date) to (departure date) - a (single/double) room in the Holiday Inn Express from (arrival date) to (departure date) Please note: For bookings on campus or in the Holiday Inn Express prepayment will be reqired. Once we have received your registration, you will be contacted concerning payment. From cat-dist@mta.ca Sun Mar 24 20:55:17 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA02766; Sun, 24 Mar 1996 20:55:17 -0400 Date: Sun, 24 Mar 1996 20:55:07 -0400 (AST) From: categories To: categories Subject: Existence of Grothendieck Universes Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Sat, 23 Mar 1996 15:50:07 -0800 From: Vaughan Pratt I once asked Joe Shoenfield that [...] Well, Joe said in effect I can tell you everything that goes to make up the first Grothendieck universe, except I don't have time to finish telling you. Well, it's no worse than any of my existence "proofs" I suppose. I can't shoot it down with the argument that it would equally well prove the existence of cardinals we already know not to exist, since the extra time Joe would need to tell us everything that goes into making up a nonexistent ordinal might disqualify that proof without disqualifying the other. :) Further reflection on this merely seems to lead back to my original point about there not being enough room in this town for both \in and U. If your U is an inaccessible cardinal, and inaccessible cardinals *do* exist (and some set theorists seem to hope very badly they do, despite knowing it cannot be proven in ZFC), then rejecting membership is one reasonable way out. Becoming an intuitionist is another. Have the reasonable alternatives proposed to date been collected in one place and insightfully classified and compared? The flip side of this is, if inaccessible cardinals are eventually proved *not* to exist, then the Cantor-Russell paradox goes away for those working in a Grothendieck universe. But in that case the one reasonable objection I've been able to grasp so far to membership, namely its incompatibility with existence of one's mathematical home, goes away too. Is there any other argument against membership? Preferably just as short, but I'll settle for long if that's all that's possible. Or is the rejection of membership all just touchy-feely stuff based on a deep-seated feeling for something? "The von Neumann rigid-epsilon monsters" alluded to by Bill Lawvere sounds like it might be made into such an argument. But as I pointed out, when the only sets are the ordinals, one of each, the "monster" is tamed to a gentle line +1'ing steadily along, with the occasional little hiccup at each limit ordinal. That's no monster. A more convincing objection is needed. There must be something else, ideally something we are all very familiar with. The smoothness of space, for example. First off, even if physical space *is* smooth, why should this have any more bearing on our mathematical spaces than their dimension? Obviously no one can get away in these enlightened days with legislating 3, 4, or 26 as an upper bound in mathematics. Second, it is not even clear that the space we inhabit *is* smooth. Start with http://zebu.uoregon.edu/~imamura/209/may8/may8.html and look at what Vilenkin and Linde are proposing as an alternative model of space: foam at fine grain. Their idea that small distances in space are chaotic makes much more sense to me than a model based on extrapolating the smoothness of space-in-the-large down to arbitrarily fine scales as though space were a mathematical manifold. That extrapolation applied to the smoothness in the law of large numbers in statistics for example is well-known to lead to nonsensical results. With the statistical analogy in mind, my only question about the Vilenkin-Linde model is whether the appearance of chaos at fine scales would be nicely explained by populating unit volumes with only finitely many points. It is very easy to construct smooth-in-the-large manifolds from finite sets, and these will naturally look bumpy in the small. We would then have to add another physical constant to the books, the number of points of space per cubic centimeter. -- Vaughan Pratt =================================== PS. I inquired on sci.math.research about my construction of the nonstandard reals. Vladimir Pestov at U. Wellington pointed out an embarrassingly trivial oversight: I'd forgotten that the class of fields subdivides into smaller elementary classes, and had not thought to order my field (the standard part leaves no alternative, it can't be an algebraically closed field). You can't, at least not without further restrictions on the sequences. Luckily the standard part of my field *can* be ordered or I'd have to come up with some other demonstration to Peter Johnstone that one can identify the set of reals and its addition morphism without having to say which ordinals go where. More generally, any sequence can be named by its elements. There is no need to name it by whichever ordinal God picked this time around as the placeholder in the set of sequences of which that sequence is a member. I can't imagine what Peter was thinking. This sort of construction, where you have to take down the scaffolding when you're done, goes on all the time in ordinary mathematics. From cat-dist@mta.ca Mon Mar 25 10:29:28 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA09710; Mon, 25 Mar 1996 10:29:27 -0400 Date: Mon, 25 Mar 1996 10:27:36 -0400 (AST) From: categories To: categories Subject: more on locally closed sublocales and subtoposes Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Mon, 25 Mar 1996 11:26:29 +0100 From: Anders Kock This is to announce the preprint A. Kock and T. Plewe: Locally closed subtoposes, and prolongation by zero. It is available by anonymous ftp from theory.doc.ic.ac.uk/papers/Kock where it appears as the file Kock-Plewe.ps or Kock-Plewe.dvi . It subsumes the paper by Kock, announced here on Feb. 15 1996, and this paper has therefore now been removed from the above ftp-site. Abstract: We prove the equivalence of some conditions on a complemented subtopos of a topos, one of which is that the subtopos is locally closed, and another is that abelian group objects in the smaller topos admit prolongation by zero; the prolongation functor then has a right adjoint. From cat-dist@mta.ca Mon Mar 25 20:40:39 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA25582; Mon, 25 Mar 1996 20:40:39 -0400 Date: Mon, 25 Mar 1996 20:39:56 -0400 (AST) From: categories To: categories Subject: Cohen and the continuum Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Mon, 25 Mar 1996 14:08:43 -0800 From: Vaughan Pratt Not sure if Cohen feels exactly as I do about the continuum, but Stephen D. Edington in his http://ftp2.wpine.com/uu/sermons/envy.html commenting on Cohen sure does. >I guess I could end on that note [definition of envy], but I'll expand >upon it just a bit. To stay with Ms. Cohen's work for just a couple >more minutes, she offers a vice to virtue continuum, in the manner to >which I've already referred, with respect to envy. It runs from >"Destructive" to "Positive" envy. As she sees it, "positive envy" is >not an oxymoron. The stops along the way, on Ms. Cohen's continuum, >are: The Wish to Harm, Self-Hatred, Resentment, Covetousness, >Admiration, and Emulation. A very interesting configuration, let me >run it by you again: The Wish to Harm, Self-Hatred, Resentment, >Covetousness, Admiration, and Emulation. The wish to do harm and >self-hatred, and then admiration and emulation are all a part of the >same "envy continuum", with envy actually giving way to positive >admiration and emulation at some point. > >Where one comes down on that continuum depends much more on who it is >that is doing the viewing, rather than what is actually out there to be >seen. Anais Nin, a novelist, essayist, long-time friend and some-time >lover of Henry Miller, once noted: > >We don't see things as they are, we see them as we are. The last line is my position exactly on where to come down on the continuum. :) Vaughan Pratt From cat-dist@mta.ca Tue Mar 26 14:33:30 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA03173; Tue, 26 Mar 1996 14:33:29 -0400 Date: Tue, 26 Mar 1996 14:27:34 -0400 (AST) From: categories To: categories Subject: Sussex Category Meeting, 7th-12th July 1996 Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Tue, 26 Mar 96 10:18 GMT From: Chris Mulvey Sussex Category Meeting 7th July - 12th July 1996 The University of Sussex invites you to attend the Seventh International Meeting on Category Theory and its Applications to be held at the White House, the Isle of Thorns, Chelwood Gate, East Sussex, England, from Sunday, 7th July to Friday, 12th July, 1996. The Isle of Thorns is the Conference Centre of the University of Sussex, pleasantly situated in the Ashdown Forest, about 25 miles north of Brighton. Those who have attended the previous meetings there will know that it provides a relaxing atmosphere in which to live and work in the quiet of the countryside, and that the food is excellent. The cost of the meeting is expected to be 345 pounds, which includes registration fees, accommodation, and meals. It may be noted that the meeting precedes the European Congress of Mathematicians to be held in Budapest from Monday, 22nd July to Friday, 26th July 1996. It should be noted that accommodation at the White House is limited, and will be assigned in the order of receiving applications. Unfortunately, children are not allowed within the White House, and the number of double rooms available is small. Accommodation at the White House will be available from the afternoon of Sunday, 7th July, to the afternoon of Friday, 12th July, 1996. In order to receive further details of the meeting, together with an application form for accommodation at the meeting, please reply by sending your name and postal address either by email to: c.j.mulvey@sussex.ac.uk or by post to: Dr. Christopher J. Mulvey, School of Mathematical Sciences, University of Sussex, Falmer, BRIGHTON, BN1 9QH, United Kingdom. The completed application form must be returned by the closing date of 15th May, 1996. It would be appreciated if you would forward a copy of this notice to anyone who might be interested in receiving it but might otherwise not receive it. Christopher Mulvey. From cat-dist@mta.ca Wed Mar 27 14:58:11 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA17652; Wed, 27 Mar 1996 14:58:11 -0400 Date: Wed, 27 Mar 1996 14:55:46 -0400 (AST) From: categories To: categories Subject: Re: Existence of Grothendieck Universes Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Tue, 26 Mar 96 13:44:07 -0800 From: oliver@math.ucla.edu Vaughan Pratt writes: If your U is an inaccessible cardinal, and inaccessible cardinals *do* exist (and some set theorists seem to hope very badly they do, despite knowing it cannot be proven in ZFC), ... I think the word "despite" here misses the whole point. It is precisely *because* the existence of inaccessibles cannot be proven in ZFC, that the assumption of their existence is interesting. More exactly, this is how we know that ZFC+inaccessibles is a proper (if modest) extension of ZFC itself. Now of course this is not to say that whenever ZFC fails to prove the existence of some X that we should immediately assume "X exists"; among other problems, that would quickly lead to an inconsistent theory. Inaccessibles, however, have other merits: i) If my model says there are inaccessibles, and yours says there aren't, it may just mean that your model is an initial segment of mine. In that case my model is clearly better, because it has everything in it that yours does, and more besides; moreover, we haven't lost any nice features that your model might happen to have, because they are still true when prefaced by "in your model..." . ii) Inaccessibles are an example of the intuition that says "anything we know how to do too well or too precisely, can't possibly tell the whole story; there must be more." In this case what we know too well how to do is take exponentials of cardinals and limits of sequences of ordinals, where the length of the sequence is a cardinal we already have. Strengthen this intuition to "things we can construct in L" and you start to see why 0# should exist. From cat-dist@mta.ca Thu Mar 28 15:47:17 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA22731; Thu, 28 Mar 1996 15:47:16 -0400 Date: Thu, 28 Mar 1996 15:41:25 -0400 (AST) From: categories To: categories Subject: Re: Existence of Grothendieck Universes Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Wed, 27 Mar 1996 12:59:32 -0800 From: Vaughan Pratt (I promised Bob I'd give it a rest (my idea, not his), but I can't resist one more shot. From: oliver@math.ucla.edu i) If my model says there are inaccessibles,... my model is clearly better, because it has everything in it that yours does, and more besides; moreover, we haven't lost any nice features that your model might happen to have, Consistency is not a nice feature? News to me. My model is more likely to be consistent than yours. Inconsistency of yours would be a beautiful result to most people, like a beautiful building or park. Inconsistency of mine would be a magnitude-9 earthquake! Furthermore mathematics has had no trouble imagining my model since 1939 when Goedel showed us how. It is *very* hard to imagine your model, so hard that not even the smartest people in the world have been able to do it in over half a century of trying. This is *not* a good sign. Strengthen this intuition to "things we can construct in L" and you start to see why 0# should exist. This is an argument for assuming the existence of everything whose nonexistence you can't actually *prove*. But that forces you to retreat every time we disprove the existence of yet another ordinal. Such discoveries happen periodically, and do not astonish working mathematicians. A much more stable approach would be to accept the easily imagined, and reject what is hard to imagine. Following that strategy, you only have to retreat in the face of 50-year or even 200-year earthquakes. Anyway, what are we arguing about here? What exactly *is* the advantage of assuming inaccessibles? (Let's not tempt fate and get too close to inconsistency by assuming measurables!) Sure you can shorten some contrived proofs a lot with inaccessibles, but can you shorten a proof some mathematician might care about? Or do anything else useful with them? Vaughan Pratt From cat-dist@mta.ca Fri Mar 29 16:04:27 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA00283; Fri, 29 Mar 1996 16:04:27 -0400 Date: Fri, 29 Mar 1996 15:59:56 -0400 (AST) From: categories To: categories Subject: Re: Existence of Grothendieck Universes Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Thu, 28 Mar 96 20:57:48 -0800 From: oliver@math.ucla.edu >From: Vaughan Pratt >>From: oliver@math.ucla.edu >>i) If my model says there are inaccessibles,... my model >>is clearly better, because it has everything in it that >>yours does, and more besides; moreover, we haven't lost >>any nice features that your model might happen to have, >Consistency is not a nice feature? News to me. My model is more >likely to be consistent than yours. Careful with language. Models are not consistent or inconsistent; they simply exist or fail to exist. Consistency is a property of *theories*. If my model exists, then it is better than yours. >Furthermore mathematics has had no trouble imagining my model since >1939 when Goedel showed us how. It is *very* hard to imagine your >model, so hard that not even the smartest people in the world have been >able to do it in over half a century of trying. I do not know what you might mean by this. I have no difficulty whatsoever in imagining inaccessible cardinals. If you mean I can't imagine everything that might happen *below* an inaccessible cardinal I plead guilty, and challenge you to imagine all ordinals below Aleph_1. >This is an argument for assuming the existence of everything whose >nonexistence you can't actually *prove*. No, not everything: For example I don't assume the existence of a proof of 0=1 from ZFC, even though I can't prove the nonexistence of such a proof. In my first article I tried to give an idea of why I assume one and not the other. >But that forces you to >retreat every time we disprove the existence of yet another ordinal. -------IF YOU READ NOTHING ELSE IN THE ARTICLE, READ THIS PARAGRAPH--------- Science is a continual process of assuming things that might be proved wrong, taking the chance that you may later be forced to retreat. Read "Conjectures and Refutations" by Karl Popper. >A much more stable approach would be to accept the easily imagined, and >reject what is hard to imagine. Following that strategy, you only have >to retreat in the face of 50-year or even 200-year earthquakes. Truly, I think you are much overestimating the difference between ZFC and ZFC+inaccessibles. To prove a contradiction from ZFC+inaccessibles, or even ZFC+measurables, would be earthquake enough for me; but even a contradiction from ZFC would have little effect on most everyday mathematics as long as it didn't go through in, say, 2nd-order PA. >Anyway, what are we arguing about here? What exactly *is* the >advantage of assuming inaccessibles? Well for example, if inaccessibles exist then we *know* choice is necessary to prove the existence of a nonmeasurable set of reals. If measurables exist then every analytic set of reals (i.e. projection of a Borel set in the plane) is measurable. From cat-dist@mta.ca Fri Mar 29 16:04:28 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA00178; Fri, 29 Mar 1996 16:04:27 -0400 Date: Fri, 29 Mar 1996 16:00:52 -0400 (AST) From: categories To: categories Subject: toposes vs. sets - some simple minded questions and remarks Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Fri, 29 Mar 1996 16:23:38 MEZ From: Thomas Streicher Dear all, I have been following the discussion on toposes vs. set theory on the network. The discussion has reminded me of a more ``pragmatic problem'' that a student of mine (B. Reus) had to face when formalising some variant of Synthetic Domain Theory in a very strong impredicative type theory : Calculus of Constructions with Inductive Types, Extensionality for Functions and Axiom of Unique Choice. This is almost topos logic : what is missing is the principle that equivalent propositions are equal but one has the further assumption of a small internal complete universe. Anyway, the ``pragmatic'' problem he had to face when actually working inside the formal system was HOW TO DEAL WITH SUBTYPES. Notice that the notion of subtype is not the object-oriented one from Computer Science but the good old-fashoned one from Logic. I will now explain more explicitely what I mean. If A is a type and P is a predicate on A then in everyday mathematics one does not hesitate to form the type { x : A | P(x) } . This, of course, is no problem in set theory BUT it definitely is a problem in higher order logic (HOL) because in the latter one does not have the possibility of ``subtype formation'' which allows one to turn a predicate into a type. Now it seems to me that topos logic is more expressive than type theory in the sense that it allows subtype formation. When one extends HOL by subtype formation then any subtype { x : A | P(x) } has to be accompanied by an inclusion map iota_A,P : { x : A | P(x) } >---> A (together with some axioms governing its use; actually, the only place where I could find them spelled out in detail is in some lecture notes by Wesley Phoa). The ``pragmatic'' problem now is that when a \in A and P(a) then one is not allowed to state a \in { x : A | P(x) } BUT ONLY iota_A,P(a) \in { x : A | P(x) } . Now when it comes to formalise arguments in HOL augmented by logical subtypes then notation gets really clumsy as one has to mention the subtype inclusions all the time. (Notice that in dependent type theory one can express { x : A | P(x) } as (\Sigma x : A) P(x) and iota_A,P is projection on the first argument (saliently assuming that propositions are ``proof-irrelevant'', i.e. any proposition considered as a type contains at most one element)). Now -- to my opinion the ``pragmatic'' superiority of (naive) set theory over HOL with subtypes is that one may omit all the ``iotas'' and what one writes down is much more concise. So it is precisely this notational convenience which makes naive set theory a better linguistic tool for communicating mathematical constructions and arguments. But notice that this sloppiness of omitting subtype inclusions renders the ``type-checking'' undecidable -- when one would insist on staying in a typed framework because in order to check whether 7653 \in { x : N | P(x) } one has to PROVE P(7653) which actually is a problem when P is not semidecidable, e.g. when P(x) is a Pi-0-1-formula (which e.g. states the consistency of the formal system in use). !! It is precisely this undecidability of type-checking which forces us to stick to an untyped universe despite the fact that in ordinary mathematical arguments one almost never exploits the strong comprehension principles of ZF(C) !! I am always puzzled by the following two slogans (1) Topos Logic corresponds to Set Theory (2) Topos Logic corresponds to Higher Order Logic which can be found in the topos-theoretic literature. It cannot be the case that both slogans are literally true as one can prove the consistency of Higher Order Logic inside Set Theory and therefore Set Theory must be more expressive than Higher Order Logic (unless one renders G"odel's Second Incompleteness Theorem to be wrong). The slogan I would have in mind would be Topos Logic corresponds to Higher Order Logic with Subtypes . Of course, from the point of view of proof-theoretic strength nothing is gained by adding Subtypes to Higher Order Logic (as this way one surely cannot prove more algorithms to terminate). So I can understand the slogan Topos Logic corresponds to Higher Order Logic in the sense that the logics are equiconsistent. I definitely would like to know from the experts in topos theory which of the correspondences (1) or (2) above is the intended one. Please, note that this question is not meant as a provocation but it simply is curiosity about what the acting person thought when slogans (1) and (2) were promoted (beginning of the 70s I presume). Finally, I would like to ask whether the following impression of mine is absolutely misleading : the correspondence between BZF and topos theory given in the book of Mac Lane and Moerdijk is a mere equiconsistency result saying that there is a nontrivial elementary topos iff there is a consistent model of BZF. If I remember correctly there are given 2 constructions : one turning a model of BZF into an elementary topos (easy) and a second more complicated one constructing a model of BZF from an elementary topos. But that does NOT give an EQUIVALENCE bewteen toposes and models of BZF as far as I can see. When I start with a topos E then I get a model M of BZF which in turn gives rise to a topos E_new but, in general, E and E_new will not be equivalent anymore. Right ?? Sorry for that lengthy and maybe shallow remarks but it is really this ``what I always wanted to know but never dared to ask'' sort of question(s) which I now dare to ask as the arena seems to have been opened already for ``fluffy'' questions. Thomas Streicher From cat-dist@mta.ca Sat Mar 30 09:36:11 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA15714; Sat, 30 Mar 1996 09:36:11 -0400 Date: Sat, 30 Mar 1996 09:33:02 -0400 (AST) From: categories To: categories Subject: Re: Existence of Grothendieck Universes Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Fri, 29 Mar 96 12:16:47 -0800 From: oliver@math.ucla.edu I wrote: If measurables exist then every analytic set of reals (i.e. projection of a Borel set in the plane) is measurable. Careless of me. ZFC is enough on its own to prove that every analytic set is measurable, either countable or contains a perfect subset, and has the property of Baire. Measurables get you the same results one real quantifier higher; i.e. for projections of co-analytic sets. For future reference, if I notice an error after making a submission on lists like this, can I write the moderator and ask to make a correction? From cat-dist@mta.ca Sat Mar 30 18:06:54 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA18607; Sat, 30 Mar 1996 18:06:54 -0400 Date: Sat, 30 Mar 1996 18:04:17 -0400 (AST) From: categories To: categories Subject: AMAST'96: Call for Partecipation Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Sat, 30 Mar 96 15:30:27 +0100 From: Bernhard Reus ======================================================================= [With apologies if you get this announcement more than once. B.Reus] ----------------------------------------------------------------------- A word-wide-web page containing information about the conference is reachable by URL: http://www.pst.informatik.uni-muenchen.de/amast96 . e-mail: amast96-info@informatik.uni-muenchen.de -------------------------------------------------------------------- ********************************************* ******************************************* FIFTH INTERNATIONAL CONFERENCE ON ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY AMAST '96 ******************************************* ********************************************* July 1-5, 1996 Munich, Germany Sponsored by Deutsche Forschungsgemeinschaft M"unchener Universit"atsgesellschaft s d & m Siemens Organized by Ludwig-Maximilians-Universit"at M"unchen FINAL PROGRAMME, REGISTRATION, ACCOMMODATION, and TRAVEL INFORMATION ********************************************************* FINAL PROGRAMME ********************************************************* ---------------------- EDUCATION DAY ---------------------- MONDAY, JULY 1st, 1996 09.00-10.00 Registration 10.00-10.15 Opening 10.15-11.45 Invited Talks Industrial Trials of Formal Specification John Fitzgerald University Newcastle upon Tyne, UK Industrial Applications of ASF+SDF Arie van Deursen CWI Amsterdam, The Netherlands An Experience with MEC in a Real Industrial Project Andre Arnold Univ. Bordeaux, France 11.45-12.15 Discussion 12.15-13.45 Lunch 13.45-15.15 Invited Talks Applying Research Results in the Industrial Environment: The Case of the TRIO Specification Language Dino Mandrioli Politecnico di Milano, Italy Using Heterogeneous Formal Methods in Distributed Software Engineering Education Bernd Kr"amer Fern-Universit"at Hagen, Germany Introducing Formal Methods to Software Engineers Through OMG's CORBA Environment and Interface Definition Language Sriram Sankar Sun Microsystems Laboratories, USA 15.15-15.45 Discussion ------------------------- CONFERENCE SCHEDULE ------------------------- TUESDAY, JULY 2nd, 1996 08.00-8.45 Registration 08.45-9.00 Opening 09:00-10:00 Invited Talk Classification Approach to Design Douglas Smith Kestrel Institute, Palo Alto, USA 10:00-10:15 Discussion 10:15-10:45 Coffee Break 10:45-12:15 Session 1: Theorem Proving Semantic Foundations for Embedding HOL in Nuprl D. J. Howe AT&T Bell Laboratories, Murray Hill Free Variable Tableaux for a Many Sorted Logic with Preorders A. Gavilanes, J. Leach, S. Nieva Univ. Complutense Madrid Automating Induction over Mutually Recursive Functions D. Kapur and M. Subramaniam Univ. at Albany, New York 12:15-13:45 Lunch 13:45-15:15 Session 2: Algebraic Specification Pushouts of Order-Sorted Algebraic Specifications A. E. Haxthausen and F. Nickl Techn. Univ. of Denmark and sd&m, M"unchen A Formal Framework for Modules with State D. Ancona and E. Zucca Univ. di Genova Object-Oriented Implementation of Abstract Data Type Specifications R. Hennicker and C. Schmitz LMU M"unchen and Univ. T"ubingen 15:15-15:30 Coffee Break 15:30-16:30 System Demo Presentations SPECWARE: An Advanced Environment for the Formal Development of Complex Software Systems R. Juellig, Y. Srinivas, J. Liu Kestrel Institute, Palo Alto ASSPEGIQUE: An Integrated Specification Environment Providing Inter-Operability of Tools M. Bidoit*, C. Choppy**, F. Voisin*** LIENS, Paris*, IRIN, Univ. de Nantes**, LRI, Univ. de Paris-Sud*** Towards Integrating Algebraic Specification and Functional Programming: the Opal System K. Didrich, C. Gerke, W. Grieskamp, C. Maeder, P. Pepper Techn. Univ. Berlin InterACT: An Interactive Theorem Prover for Algebraic Specifications R. Geisler, M. Klar, F. Cornelius Techn. Univ. Berlin A new Proof-Manager and Graphic Interface for the Larch Prover F. Voisin LRI, Univ. de Paris-Sud TERSE: A Visual Environment for Supporting Analysis, Verification and Transformation of Term Rewriting Systems N. Kawaguchi, T. Sakabe, Y. Inagaki Nagoya Univ. 16:30-16:45 Coffee Break 16:45-18:15 Session 3: Concurrent and Reactive Systems On the Completeness of the Equations for the Kleene Star in Bisimulation Wan Fokkink Utrecht Univ. An Equational Axiomatization of Observation Congruence for Prefix Iteration L. Aceto and A. Ingolfsdottir Alborg Univ. Finite Axiom Systems for Testing Preorder and De Simone Process Languages I. Ulidowski Kyoto Univ. 19:00 Reception WEDNESDAY, JULY 3rd, 1996 08:30-09:30 Invited Talk Constructive Semantics of Esterel: From Theory to Practice Gerard Berry Centre de Math. Appl., Sophia Antipolis, France 09:30-09:45 Discussion 09:45-10:15 Coffee Break 10.15-12:15 Session 4: Program Verification Using Ghost Variables to Prove Refinement M. Marcus and A. Pnueli Weizmann Institute of Science, Rehovot Tracing the Origins of Verification Conditions R. Fraer INRIA, Sophia Antipolis Preprocessing for Invariant Validation E. P. Gribomont Univ. of Lie`ge Formal Verification of SIGNAL Programs: Application to a Power Transformer Station Controller M. Le Borgne*, H. Marchand*, E. Rutten*, M. Samaan** IRISA/INRIA, Rennes*, EDF/DER, Chatou** 12:15-13:45 Lunch 13:45-14:45 Invited Talk The Discrete Time Toolbus J.A. Bergstra and P. Klint CWI Amsterdam, The Netherlands 14:45-15:00 Discussion 15:00-15:15 Coffee Break 15:15-16:15 System Demo Presentations The TOOLBUS Coordination Architecture P. Klint Univ. Amsterdam A Demonstration of ASD: The Action Semantic Description Tools A. van Deursen and P. D. Mosses CWI Amsterdam and Aarhus Univ. Using Occurrence and Evolving Algebras for the Specification of Language-Based Programming Tools Arnd Poetzsch-Heffter Techn. Univ. M"unchen ECHIDNA: A System for Manipulating Explicit Choice Higher Dimensional Automata R. Buckland and M. Johnson Macquarie Univ. Verification using PEP S. Melzer, S. Romer, J. Esparza Techn. Univ. M"unchen The FC2TOOLS Set A. Bouali, A. Ressouche, V. Roy, R. de Simone INRIA, Sophia-Antipolis & Ecole des Mines de Paris 16:15-16:30 Coffee Break 16:30-18:00 Session 5: Concurrent and Reactive Systems A Study on the Specification and Verification of Performance Properties Xiao Jun Chen*, F. Corradini**, R. Gorrieri*** Univ. "La Sapienza", Roma*, Univ. of Sussex**, Univ. di Bologna*** Symbolic Bisimulation for Timed Processes M. Boreale Istituto per L'Elaborazione dell'Informazione, Pisa Approximative Analysis by Process Algebra with Graded Spatial Actions Y. Isobe, Y. Sato, K. Ohmaki Electrotechnical Laboratory, Tsukuba THURSDAY, JULY 4th, 1996 08:30-09:30 Invited Talk Boolean Formalism and Explanations Eric C. R. Hehner University of Toronto, Canada 09:30-09:45 Discussion 09:45-10:15 Coffee Break 10.15-11:45 Session 6: Logic Programming and Term Rewriting Proving Existential Termination of Normal Logic Programs M. Marchiori Univ. Padova Programming in Lygon: An Overview J. Harland*, D. Pym**, M. Winikoff*** Royal Melbourne Institute of Technology*, Univ. of London**, Univ. of Melbourne*** Some Characteristics of Strong Innermost Normalization M. R. K. Krishna Rao Max-Planck-Institut f"ur Informatik, Saarbr"ucken 11.45-12.15 System Demo Presentations Programming in Lygon: A System Demonstration J. Harland*, D. Pym**, M. Winikoff*** Royal Melbourne Institute of Technology*, Univ. of London**, Univ. of Melbourne*** CtCoq: A System Presentation J. Bertot and Y. Bertot INRIA, Sophia-Antipolis The TYPELAB Specification and Verification Environment F. W. von Henke, M. Luther, M. Strecker, M. Wagner Univ. Ulm 12:15-13:45 Lunch 13:45-14:45 Invited Talk On the Emergence of Properties in Component-Based Systems J. L. Fiadeiro University of Lisbon, Portugal 14:45-15:00 Discussion 15:00-15:15 Coffee Break 15:15-16:15 System Demo Presentations Incremental Formalization B. Steffen, T. Margaria, A. Classen, V. Braun Univ. Passau PROPLANE: A Specification Development Environment J. Souquieres and N. Levy Univ. de Nancy A Logic-Based Technology to Mechanize Software Components Reuse P. Parot INRIA, Le Chesnay TkGofer: A Functional GUI Library W. Schulte, T. Schwinn, T. Vullinghs Univ. Ulm ALPHA - A Class Library for a Metamodel based on Algebraic Graph Theory S. Erdmann and I. Classen Techn. Univ. Berlin 16:15-16:30 Coffee Break 16:30-18:00 Session 7: Algebraic and Logical Foundations Algebraic View Specification B. Paech Techn. Univ. M"unchen Towards Heterogeneous Formal Specifications G. Bernot, S. Coudert, P. Le Gall Univ. d'Evry A Categorical Characterization of Consistency Results C. Baier and M. Majster-Cederbaum Univ. Mannheim 20:00 Conference Dinner FRIDAY, JULY 5th, 1996 08:30-09:30 Invited Talk Algebraic Specification of Reactive Systems Manfred Broy Technische Universit"at M"unchen, Germany 09:30-09:45 Discussion 09:45-10:15 Coffee Break 10.15-11:45 Session 8: Concurrent and Reactive Systems A Model for Mobile Point-To-Point Data-Flow Networks without Channel Sharing R. Grosu and K.Stolen Techn. Univ. M"unchen Coalgebraic Specifications and Models of Deterministic Hybrid Systems B. Jacobs CWI Amsterdam A Bounded Retransmission Protocol for Large Data Packets J.F. Groote and J. van de Pol Utrecht Univ. 11.45-12.15 System Demo Presentations Resolution of Goals with the Functional and Logic Programming Language LPG: Impact of Abstract Interpretation D. Bert, K. Adi, R. Echahed IMAG-LSR, Grenoble Combining Reductions and Computations in ReDuX R. B"undgen and W. Lauterbach Univ. T"ubingen Conditional Directed Narrowing S. Limet and P. Rety LIFO-Univ. d'Orleans 12:15-12.30 Closing ********************************************************* REGISTRATION ********************************************************* REGISTRATION FEES ================== Before May 15: 400 DM ^ After May 15: 450 DM ^ Education Day only: 150 DM * ^ includes a copy of the proceedings, all coffee breaks and lunches, reception and banquet, * includes coffee breaks and lunch on July 1st. Extra Banquet Ticket : 100 DM Extra Reception Ticket : 30 DM. Payment must be in German currency, and can be made by cheque payable to "Prof. Martin Wirsing" or by bank transfer to: Bank: Bayerische Vereinsbank M"unchen Bank code: 70 020 270 Account no: 41 936 290 Account holder: Prof. Martin Wirsing Intended use: AMAST96 Bank transfers must specify registrant's name. Please ask your bank to arrange the transfer free of charges to the beneficiary. (No credit cards can be accepted!) REGISTRATION FORM: ================== Please type or print: ***************** AMAST'96 Registration form ******************** Last Name: First Name: Title: Affiliation: Street Address: City: Country: Phone: Fax: E-mail: Arrival date : Departure date: Payment is made by cheques: yes/no bank transfer: yes/no Total amount: Includes extra tickets for: ***************************************************************** Mail completed form either by e-mail to: hennicke@informatik.uni-muenchen.de or by surface mail to: Prof. Martin Wirsing AMAST'96 Institut f"ur Informatik Ludwig-Maximilians-Universit"at M"unchen Before April 15th: Leopoldstr. 11B, D-80802 M"unchen, After April 15th: Oettingenstr. 67, D-80538 M"unchen ********************************************************* ACCOMMODATION ********************************************************* Below you find a list of appropriate hotels in several price categories. PLEASE BOOK THE REQUIRED ROOMS YOURSELF (AS EARLY AS POSSIBLE!) ********** GUEST HOUSES ***************** All prices inclusive breakfast. Excelsior Kaulbachstr. 85 (1st floor) Tel. +89/34 82 13 Prices: Single: >= 65 DM Double: 114 DM (all rooms without WC and without bath) Location: Munich-Schwabing, 10-15 min walk to the conference building across the English Garden. Steinberg Ohmstr. 9 (1st floor) Tel. +89/33 10 11 Fax +89/33 10 11 Prices: Single: >= 69 DM Double: 100 DM (rooms with WC and bath available) Location: Munich-Schwabing, 10-15 min walk to the conference building across the English Garden. Note: If you are interested in this guest house then please contact first Rolf Hennicker (hennicke@informatik.uni-muenchen.de) since a special price may be possible. **************** HOTELS ********************* All prices inclusive breakfast (if not stated otherwise) and all rooms with WC and shower/bath. Lettl Amalienstr. 53 Tel. +89/286 69 70 Fax +89/28 66 97 97 Prices: Single: >= 110 DM Double: >= 175 DM Location: A small hotel in the University area, between Schwabing and the center. 25 min walk to the conference building, mainly through the English Garden. Cosmopolitan Hohenzollernstr. 5 Tel. +89/38 38 10 Fax +89/38 38 11 11 Prices: Single: 145 DM Double: 185 DM Location: A modern hotel in the middle of Schwabing. 20 min walk to the conference building, mainly through the English Garden. You can also take the bus no. 54 (direction "Ostbahnhof", stop "Tivolistrasse") or bus no. 154 (direction "Bruno-Walter-Ring", stop "Tivolistrasse"). Ariston Uns"oldstr. 10 Tel. +89/22 26 91 Fax 291 35 95 Prices: Single: 145 DM Double: 200 DM SPECIAL PRICE IF BOOKED BEFORE May 28: Single: 90 DM Double: 140 DM (The code word for the special price is AMAST; if there are any problems ask for Mrs. Griessner) Location: A hotel of the sixties, in Munich-Lehel, close to the center. 20 min walk to the conference building. You can also take the tramway no. 17 (direction "Effnerplatz", stop "Tivolistrasse"). M"unchen Park Hilton Am Tucherpark 7 Tel. +89/38 450 Prices: Single: 299 DM Double: 370 DM (both exclusive breakfast) Location: A comfortable hotel at the border of the English Garden. 5-10 min walk to the conference building. ********************************************************* TRAVEL INFORMATION ********************************************************* Munich offers good access by air, rail, and road. The new Munich International Airport has frequent flights to and from most major cities. By rail, the city offers easy access to the major European centers. The area of Munich is well served by the "S-Bahn" and the city by underground. There are single tickets (to be bought for each trip) or stripe cards ("Streifenkarte") which are relatively cheaper when used for several trips. Using a stripe card one has to cancel two stripes for any trip within Munich-City and eight stripes for one trip from Munich airport to the city (or conversely). HOW TO REACH THE CONFERENCE SITE AND THE HOTELS: If you arrive at the airport then take the S-Bahn no. 8 to Munich-City. If you arrive at the central station then take an arbitrary S-Bahn that goes into the direction of "Marienplatz-Ostbahnhof". Then, in any case, proceed as follows: To the conference building: Leave the S-Bahn at "Isartor"; Change to tramway no. 17 (direction "Effnerplatz"); Get out at "Tivolistrasse"; Then the conference building (Oettingenstrasse 67) is on the other side of the street; Conference room = no. 114. Note: The conference building is known to many people in Munich as the previous "Radio Free Europe" building. This may be helpful if you have any trouble. To guest houses Excelsior and Steinberg and to Hotel Cosmopolitan: Leave the S-Bahn at "Marienplatz"; Change to the underground no. U3 or no. U6 (direction "M"unchner Freiheit"); Get out at "Giselastrasse". To Hotel Lettl: Leave the S-Bahn at "Marienplatz"; Change to the underground no. U3 or U6 (direction "M"unchner Freiheit"); Get out at "Universit"at", exit "Schellingstrasse". To Hotel Ariston: Leave the S-Bahn at "Isartor"; Change to tramway no. 17 (direction "Effnerplatz"); Get out at "Nationalmuseum/Haus der Kunst"; (If you are arrived at the central station then it's better to choose directly the underground no. U4 (direction "Arabellapark") or U5 (direction "Neuperlach S"ud"). Leave the underground at "Lehel".) To M"unchen Park Hilton: It's the best to choose a Taxi at some place in Munich-City. Alternatively, you can first to go to the conference building and then walk to the hotel (5-10 min.).