November 2017 - Categories - categories.org.au

How analogous are categorial and material set theories?
by Neil Barton 03 Dec '17

03 Dec '17

Dear All, I'm very interested in how categorial and material set theories interact, and in particular the advantages of each. It's well-known that categorial viewpoints are good for isolating schematic structural relationships. We can look at sets through this lens, by considering a categorial set theory like ETCS (possibly augmented, e.g. with replacement). A remark one sometimes finds is that once you have defined membership via arrows from terminal objects, you could use ETCS for all the purposes to which ZFC is normally put. My question is the following: (Q) To what extent can you ``do almost the same work'' with a categorial set theory like ETCS vs. a material set theory like ZFC? Just to give a bit more detail concerning what I'm thinking of: Something material set theory is reasonably good at is building models (say to analyse relative consistency), or comparing cardinality. However, there's no denying that for representing abstract relationships the language is somewhat clunky, since the same abstract schematic type can be multiply instantiated by structures with very different set-theoretic properties. So, to what extent can a categorial set theory like ETCS supply the good bits of the fineness of grain associated with material set theories, whilst modding out the `noise'? For example, the following are easily stated in material set theory: 1. \aleph_17 is an accessible cardinal. In material set theory, it's easy to define the aleph function and then state that the 17th position in this function can be reached by iterating powerset and replacement. But I wouldn't even know how to talk about specific sets of different cardinalities categorially. I suppose you could say something in terms of isomorphism between subobjects, and then exponentials, but it's quite unclear to me how the specifcs would go. Is that an easily claim to state (and prove) in ETCS? 2. How would you state that {{}} and {\beth_\omega} are very different objects? Set-theoretically, these look very different (just consider their transitive closures, for instance). But category-theoretically they should look the same---since they are both singletons they are isomorphic. So is this a case where their different set-theoretic propeties are considered just `noise', or where ETCS just wouldn't see a relationship, or where ETCS can in fact see some of these properties (and I'm just missing something)? 3. How would ETCS deal with model theory and cardinality ascriptions? (This links to a question asked earlier on this mailing list concerning syntactic theories in category theory, and whether from the categorial viewpoint we should be taking notice of them at all.) For instance, it's an interesting theorem (for characterising structure) that a first-order theory categorical in one uncountable power is categorical in every uncountable power (Morley's Theorem). But I have no idea how one might formalise this in something like ETCS---I know of Makkai and Reyes textbook (which I am currently reading) on categorial logic (where theories are represented by categories and models by functors), but I don't see how you could get categoricity-in-power claims out of the set up there. Can this be done? Any help and/or discussion would be greatly appreciated! Best Wishes, Neil -- Dr. Neil Barton Postdoctoral Research Fellow Kurt Gödel Research Center for Mathematical Logic University of Vienna Web: https://neilbarton.net/ [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

3 3

2nd CfP: FM 2018
by Einar Broch Johnsen 29 Nov '17

29 Nov '17

FM 2018: 22nd International Symposium on Formal Methods Oxford, UK, July 15-17, 2018 Conference website http://fm2018.org Submission link https://easychair.org/conferences/?conf=fm2018 Abstract registration deadline January 8, 2018 Submission deadline January 22, 2018 Notification April 9, 2018 Camera Ready May 9, 2018 Call for Papers - Main Conference FM 2018 is the latest in a series of symposia organized by Formal Methods Europe, an independent association that encourages the use of, and research on, formal methods for the engineering of computer-based systems and software. The symposia have been notably successful in bringing together researchers and industrial users around a programme of original papers on research and industrial experience, workshops, tutorials, reports on tools, projects, and ongoing doctoral work. FM 2018 will take place in Oxford, UK, 15-17 July 2018 as part of FLoC 2018, the Federated Logic Conferences. FM 2018 will highlight the development and application of formal methods in a wide range of domains including software and integrated computer-based systems. In the latter field, cyber-physical systems, systems-of-systems, human-computer interaction, manufacturing, sustainability, power, transport, cities, healthcare, and biology are of particular interest. We also welcome papers on experiences of formal methods in industry, and on the design and validation of formal methods tools. Submission Guidelines FM 2018 encourages submissions on formal methods for developing and evaluating systems that interact with physical processes, and systems that use artificial intelligence technology. Examples include autonomous systems, robots, and cyber-physical systems in general. Applying formal methods to these systems of growing interest and importance is challenging because they exhibit much greater non-determinism than traditional systems, making them challenging to assure. All papers must be original and not simultaneously submitted to another journal or conference. The broad topics of interest for FM 2018 include, but are not limited to: * Interdisciplinary formal methods: Techniques, tools and experiences demonstrating formal methods in interdisciplinary frameworks. * Formal methods in practice: Industrial applications of formal methods, experience with formal methods in industry, tool usage reports, experiments with challenge problems. Authors are encouraged to explain how formal methods overcame problems, led to improved designs, or provided new insights. * Tools for formal methods: Advances in automated verification, model-checking, and testing with formal methods, tools integration, environments for formal methods, and experimental validation of tools. Authors are encouraged to demonstrate empirically that the new tool or environment advances the state of the art. * Role of formal methods in software and systems engineering: Development processes with formal methods, usage guidelines for formal methods, and method integration. Authors are encouraged to evaluate process innovations with respect to qualitative or quantitative improvements. Empirical studies and evaluations are also solicited. * Theoretical foundations: All aspects of theory related to specification, verification, refinement, and static and dynamic analysis. Authors are encouraged to explain how their results contribute to the solution of practical problems with methods or tools. Submission Information Papers should be original work, not published or submitted elsewhere, in Springer LNCS format, written in English, submitted through Easychair (https://easychair.org/conferences/?conf=fm2018) Each paper will be evaluated by at least three members of the Programme Committee. Authors of papers reporting experimental work are strongly encouraged to make their experimental results available for use by reviewers. Similarly, case study papers should describe significant case studies, and the complete development should be made available at the time of review. The usual criteria for novelty, reproducibility, correctness and the ability for others to build upon the described work apply. Tool papers should explain enhancements made compared to previously published work. A tool paper need not present the theory behind the tool but should focus on the tool's features, how it is used, its evaluation, and examples and screen shots illustrating the tool's use. Authors of tool papers should make their tool available for use by reviewers. We solicit two categories of papers: * Regular Papers should not exceed 15 pages, not counting references and appendices. * Short papers, including tool papers, should not exceed 6 pages, not counting references and appendices. Besides tool papers, short papers are encouraged for any subject that can be described within the page limit, and in particular for novel ideas without an extensive experimental evaluation. Short papers will be accompanied by short presentations. For regular and tool papers, an appendix can provide additional material such as details on proofs or experiments. The appendix is not part of the page count and not guaranteed to be read or taken into account by the reviewers. It should not contain information necessary to the understanding and the evaluation of the presented work. Papers will be accepted or rejected in the category in which they were submitted ??? there will be no "demotions" from a regular to a short paper. Keynote Speakers Annabelle McIver, Macquarie University, Sydney, Australia Leonardo de Moura, Microsoft Research, Redmond, USA Kim Guldstrand Larsen, Aalborg University & UP4ALL, Denmark Best Paper Award During the conference, the Programme Committee Chairs will present an award to the authors of the submission selected as the FM 2018 Best Paper. Publication Accepted papers will be published in the Symposium Proceedings to appear in Springer's Lecture Notes in Computer Science. Extended versions of selected papers will be invited for publication in a special issue of one or more journals. Location FM2018, the 22nd International Symposium on Formal Methods, will take place in Oxford, UK, 15-17 July 2018 as part of FLoC 2018, the Federated Logic Conferences. General Chair Erik P. de Vink, Eindhoven University of Technology, NL Programme Chairs Bill W. Roscoe, University of Oxford, GB Jan Peleska, University of Bremen, DE Committees Program Committee Bernhard K. Airchernig, TU Graz, AT Joerg Brauer, Verified Systems International GmbH, DE Ana Cavalcanti, University of York, GB Frank De Boer, CWI, NL John S. Fitzgerald, Newcastle University, GB Martin Fraenzle, Universitaet Oldenburg, DE Vijay Ganesh, University of Waterloo, CA Diego Garbervetsky, Universidad de Buenos Aires, AR Dimitria Giannakopoulou, NASA Ames, US Thomas Gibson-Robinson, University of Oxford, GB Stefania Gnesi, ISTI-CNR, IT Anne E. Haxthausen, Technical University of Denmark, DK Ian J. Hayes, University of Queensland, AU Constance Heitmeyer, Naval Research Laboratory, US Jozef Hooman, TNO-ESI and Radboud University Nijmegen, NL Laura Humphrey, Air Force Research Laboratory, US Fuyuki Ishikawa, National Institute of Informatics, JP Einar Broch Johnsen, University of Oslo, NO Cliff Jones, Newcastle University, GB Joost-Pieter Katoen, RWTH Aachen University, DE Gerwin Klein, NICTA and University of New South Wales, AU Laura Kovacs, Chalmers University of Technology, SE Peter Gorm Larsen, Aarhus University, DK Yves Ledru, Universit?? Grenoble Alpes, FR Rustan Leino, Microsoft Research, US Elizabeth Leonard, Naval Research Laboratory, US Martin Leucker, University of L??beck, DE Michael Leuschel, University of D??sseldorf, DE Zhiming Liu, Southwest University, CN Tiziana Margaria, University of Limerick and Lero, IE Mieke Massink, CNR-ISTI, IT Annabelle McIver, Macquarie University, AU Dominique Mery, LORIA and Universit?? de Lorraine, FR Mohammad Reza Mousavi, Halmstad University, SE Peter M??ller, ETH Z??rich, CH Colin O'Halloran, D-RisQ Software Systems, GB Jose Oliveira, Universidade do Minho, PT Olaf Owe, Universitity of Oslo, NO Sam Owre, SRI International, US Alexandre Petrenko, CRIM, CA Anna Philippou, University of Cyprus, CY Elvinia Riccobene, University of Milan, IT Grigore Rosu, University of Illinois at Urbana-Champaign, US Augusto Sampaio, Federal University of Pernambuco, BR Gerardo Schneider, Chalmers University of Gothenburg, SE Natasha Sharygina, University of Lugano, CH Ana Sokolova, University of Salzburg, AT Jun Sun, Singapore University of Technology and Design, SG Stefano Tonetta, FBK-irst, IT Farn Wang, National Tainwan University, TW Heike Wehrheim, University of Paderborn, DE Michael Whalen, University of Minnesota, US Jim Woodcock, University of York, GB H??sn?? Yenig??n, Sabanci University, TR Fatiha Zaidi, Universit?? Paris-Sud, FR Gianluigi Zavattaro, Universita di Bologna, IT Contact All questions about submissions should be emailed to the programme chairs. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

call for feedback: a categorical approach to game semantics
by Tom Hirschowitz 28 Nov '17

28 Nov '17

Dear categorists, Clovis Eberhart and I just uploaded a new preprint, on which we'd be eager to read your constructive comments. https://hal.archives-ouvertes.fr/hal-01634162/document What's in a game? A theory of game models Abstract: Game semantics is a rich and successful class of denotational models for programming languages. Most game models feature a rather intuitive setup, yet surprisingly difficult proofs of such basic results as associativity of composition of strategies. We set out to unify these models into a basic abstract framework for game semantics, game settings. Our main contribution is the generic construction, for any game setting, of a category of games and strategies. Furthermore, we extend the framework to deal with innocence, and prove that innocent strategies form a subcategory. We finally show that our constructions cover many concrete cases, mainly among the early models and the very recent sheaf-based ones. Best wishes, Tom [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Jobs at the University of Michigan-Dearborn
by Thomas Fiore 28 Nov '17

28 Nov '17

Dear Category Theorists, We have an assistant professorship of mathematics open at the University of Michigan-Dearborn. https://www.mathjobs.org/jobs/jobs/11099 The position is open to all areas of mathematics, including higher category theory, algebraic topology, and mathematical music theory. The deadline is December 8th, 2017. Research is part of this job, as are teaching and service. Dearborn is 30 miles east of Ann Arbor, well within commuting distance. The wider region around Dearborn is home to much topology activity, for instance: Ann Arbor and Wayne State are nearby, and Michigan State University is a little further away. We also have a statistics position open, with the earlier deadline of November 30, 2017. People with expertise to teach upper level statistics courses can also apply. https://www.mathjobs.org/jobs/jobs/10721 I would be happy to answer any questions potential applicants may have. very best regards, Tom Fiore http://www-personal.umd.umich.edu/~tmfiore/ [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

"Categorical Logic, Toposes and Dualities" January 8-12, 2018, Nice (France).
by Clemens.BERGER＠unice.fr 28 Nov '17

28 Nov '17

Dear all, this is an announcement of a workshop to be held in Nice (France) from January 8 to January 12, 2018, on the theme "Categorical Logic, Toposes and Dualities". Those interested in attending, please contact Mai Gehrke (mgehrke(a)unice.fr) The website of the workshop is located at http://www-math.unice.fr/~patras/CatLogTop/index.html All the best, Clemens. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

A New Preprint
by Amir Tabatabai 27 Nov '17

27 Nov '17

Dear All, I have recently posted my new preprint "Geometric Modality and Weak Exponentials" on arxiv whose link is attached in the following. Corrections, comments and suggestions are all welcome. https://arxiv.org/abs/1711.01736 Abstract: The intuitionistic implication and hence the notion of function space in constructive disciplines is both non-geometric and impredicative. In this paper we try to solve both of these problems by first introducing weak exponential objects as a formalization for predicative function spaces and then by proposing modal spaces as a way to introduce a natural family of geometric predicative implications based on the interplay between the concepts of time and space. This combination then leads to a brand new family of modal propositional logics with predicative implications and then to topological semantics for these logics and some weak modal and sub-intuitionistic logics, as well. Finally, we will lift these notions and the corresponding relations to a higher and more structured level of modal topoi and modal type theory. Best wishes, Amir. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Re: How analogous are categorial and material set theories?
by Michael Shulman 27 Nov '17

27 Nov '17

Sorry, forgot to include original citations: the comparison of ZFC to ETCS goes back to Osius, Cole, and Mitchell in the 1970s, while various replacement axioms for ETCS have been formulated by Lawvere, Cole, Osius, and McLarty. On Mon, Nov 27, 2017 at 4:06 AM, Michael Shulman <shulman(a)sandiego.edu> wrote: > In general, I don't think ETCS has any more trouble building models or > comparing cardinality than ZFC does. A model in the abstract sense of > model theory doesn't use any of the "internal" membership-structure of > a ZFC-set; it is a purely structural entity: a set equipped with > certain functions and relations. So I don't see why any > model-theoretic theorem would be any harder to formalize in ETCS than > in ZFC. > > To translate statements from ZFC to ETCS that *do* involve internal > membership-structure, like distinguishing between {{}} and > {\beth_\omega}, one has to make that structure explicit by talking > about sets equipped with certain well-founded relations. There are > various ways to recover a model of a ZFC-like set theory inside ETCS: > rigid trees, accessible well-pointed graphs, etc. If one only wants > to talk about ordinal numbers, which is much more common, then one > doesn't need all that machinery; one can just talk about well-ordered > sets (up to isomorphism, like any other kind of structured set). > > ETCS is weaker than ZFC in that it doesn't include an analogue of the > axiom of replacement, which is needed for things like defining the > aleph function in generality. However, there are various ways to add > a replacement axiom to it, generally stated as a sort of "stack" > condition. This in particular allows defining families of sets by > recursion over well-founded relations, so that you can recurse over > any ordinal to get an aleph function on that ordinal, and then play > games with the analogue of proper classes to get "one aleph function" > if you like. > > Some of these issues are discussed in my preprint > https://arxiv.org/abs/1004.3802 . > > On Fri, Nov 24, 2017 at 2:36 PM, Neil Barton <bartonna(a)gmail.com> wrote: >> Dear All, >> >> I'm very interested in how categorial and material set theories >> interact, and in particular the advantages of each. >> >> It's well-known that categorial viewpoints are good for isolating >> schematic structural relationships. We can look at sets through this >> lens, by considering a categorial set theory like ETCS (possibly >> augmented, e.g. with replacement). A remark one sometimes finds is >> that once you have defined membership via arrows from terminal >> objects, you could use ETCS for all the purposes to which ZFC is >> normally put. >> >> My question is the following: >> >> (Q) To what extent can you ``do almost the same work'' with a >> categorial set theory like ETCS vs. a material set theory like ZFC? >> >> Just to give a bit more detail concerning what I'm thinking of: >> Something material set theory is reasonably good at is building models >> (say to analyse relative consistency), or comparing cardinality. >> However, there's no denying that for representing abstract >> relationships the language is somewhat clunky, since the same abstract >> schematic type can be multiply instantiated by structures with very >> different set-theoretic properties. So, to what extent can a >> categorial set theory like ETCS supply the good bits of the fineness >> of grain associated with material set theories, whilst modding out the >> `noise'? >> >> For example, the following are easily stated in material set theory: >> >> 1. \aleph_17 is an accessible cardinal. >> >> In material set theory, it's easy to define the aleph function and >> then state that the 17th position in this function can be reached by >> iterating powerset and replacement. But I wouldn't even know how to >> talk about specific sets of different cardinalities categorially. I >> suppose you could say something in terms of isomorphism between >> subobjects, and then exponentials, but it's quite unclear to me how >> the specifcs would go. Is that an easily claim to state (and prove) in >> ETCS? >> >> 2. How would you state that {{}} and {\beth_\omega} are very different >> objects? Set-theoretically, these look very different (just consider >> their transitive closures, for instance). But category-theoretically >> they should look the same---since they are both singletons they are >> isomorphic. So is this a case where their different set-theoretic >> propeties are considered just `noise', or where ETCS just wouldn't see >> a relationship, or where ETCS can in fact see some of these properties >> (and I'm just missing something)? >> >> 3. How would ETCS deal with model theory and cardinality ascriptions? >> (This links to a question asked earlier on this mailing list >> concerning syntactic theories in category theory, and whether from the >> categorial viewpoint we should be taking notice of them at all.) For >> instance, it's an interesting theorem (for characterising structure) >> that a first-order theory categorical in one uncountable power is >> categorical in every uncountable power (Morley's Theorem). But I have >> no idea how one might formalise this in something like ETCS---I know >> of Makkai and Reyes textbook (which I am currently reading) on >> categorial logic (where theories are represented by categories and >> models by functors), but I don't see how you could get >> categoricity-in-power claims out of the set up there. Can this be >> done? >> >> Any help and/or discussion would be greatly appreciated! >> >> Best Wishes, >> >> Neil >> >> -- >> Dr. Neil Barton >> Postdoctoral Research Fellow >> Kurt Gödel Research Center for Mathematical Logic >> University of Vienna >> Web: https://neilbarton.net/ >> >> >> [For admin and other information see: http://www.mta.ca/~cat-dist/ ] [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Last announcement PSSL 102
by Xabier Garcia Martinez 26 Nov '17

26 Nov '17

Dear friends and colleagues, This is a reminder that the 30th of November we will reach the deadline for registration to participate in the 102nd edition of the PSSL (Peripatetic Seminar on Sheaves and Logic) to be held at the University of Santiago de Compostela, Spain, the weekend of 13th - 14th of January 2018. More information can be found at the webpage: http://www.usc.es/regaca/pssl102/ We hope to see you soon, Xabier Garcia-Martinez Tim Van der Linden [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

postdoctoral positions at the University of Western Ontario
by Dan Christensen 26 Nov '17

26 Nov '17

[Please forward as appropriate.] The Math Department at Western will be hiring one or more postdocs to start in summer 2018. The application deadline is January 4, 2018. The full ad is available at https://www.mathjobs.org/jobs/UWO/PDF and I have included the text of it below. The Math Department has several faculty working in topology, category theory, homotopy type theory and related areas, including Jardine, Kapulkin and me. Applicants in these and other areas represented in the department are particularly encouraged to apply. Our department has an active postdoctoral program and a busy seminar schedule with many visitors. More information about the department and the School of Mathematical and Statistical Sciences are available at http://uwo.ca/math/ and http://uwo.ca/smss/ The positions have a reduced teaching load of just two half-courses. A "half-course" is a 13-week course meeting for 3 or 4 hours each week. Note also that the cost of living in London is quite low. Feel free to contact me with questions, or to use the e-mail address below. Dan ------------- The University of Western Ontario, Department of Mathematics Postdoctoral Positions The Department of Mathematics at the University of Western Ontario has one or more postdoctoral positions available, in any area of Mathematics that is represented within the Department. Information about the Department can be found at http://uwo.ca/math. Each position has a two-year term with a flexible start date of July 1, 2018. The salary will be $44,000 CDN per year (currently under negotiation), plus a tax-free research fund of $1,500 per year. The positions will involve teaching two half-courses per year, in addition to research. Candidates should have completed a Ph.D. in July 2015 or later. The filling of these positions is subject to budgetary considerations. All applications should include a cover letter, a curriculum vitae (including pubication list), a research statement, and at least three letters of reference. At least one letter of reference should comment on the teaching abilities of the applicant. E-mail inquiries may be sent to math-pos(a)uwo.ca. Screening of applications will begin on January 4, 2018, and will continue until all positions are filled. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Thanks for the post card
by Dana Scott 24 Nov '17

24 Nov '17

[Note from moderator: apologies to Bill that his message was garbled in some mail readers, and thanks to Dana for clean-up] Re CT 2017 Vancouver Dear colleagues and friends, Yesterday I received from Canada Post a large post card (40 cm x 55 cm) which has travelled from Vancouver as a 'small packet'. It is filled with good wishes, many signatures and thoughts on mathematics, that express so much friendship. Enclosed was a copy of the group photo of the participants with some smiling faces. This beautiful surprise has made me very happy. Thank you all. Hope to see you next year in the Azores. The many young people whom I don't yet know, I hope to meet there. I thank my friend Lauchie MacDonald for organizing this successful conference. Best wishes, Bill Lawvere Reply-To: "Lawvere, F." <wlawvere(a)buffalo.edu> [For admin and other information see: http://www.mta.ca/~cat-dist/ ] [DSS: I cleaned up Bill's message for readability.] [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0