June 2018 - Categories - categories.org.au

104th PSSL -- first announcement
by Benno van den Berg 29 Jun '18

29 Jun '18

Dear colleagues and friends, I am writing to let you know that the next Peripatetic Seminar on Sheaves and Logic (PSSL), the 104th, will be held in Amsterdam during the weekend of October 6 and 7, 2018. We will use the occasion to celebrate the 60th birthdays of Jaap van Oosten and Thomas Streicher. Further details will be available in due course. In the meantime, please do not hesitate to contact me if you have any queries. With best regards, Benno van den Berg [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

CSL 2018 - Call for Participation
by majordomo＠mlist.mta.ca 27 Jun '18

27 Jun '18

Call for Participation ======================================== Computer Science Logic 2018 Birmingham, United Kingdom 4???7 September <http://events.cs.bham.ac.uk/csl18/> ======================================== The European Association for Computer Science Logic and the School of Computer Science of the University of Birmingham kindly invite you to take part in the 2018 edition of CSL. The day after the conference, there will be a free workshop honouring Achim Jung on occasion of his 60th birthday. # The Conference Computer Science Logic (CSL) is the annual conference of the European Association for Computer Science Logic (EACSL). It is an interdisciplinary conference, spanning across both basic and application oriented research in mathematical logic and computer science. CSL 2018 will be the 27th edition in the series. ## Invited Speakers * Bob Coecke ??? University of Oxford * Emmanuel Filiot ??? Universit?? Libre de Bruxelles * Catuscia Palamidessi ??? ??cole Polytechnique * Christine Tasson ??? Universit?? Paris Diderot * Szymon Toru??czyk ??? Uniwersytet Warszawksi ## Programme Thirty-six contributions were selected for presentation at CSL 2018. A full listing is available at <http://events.cs.bham.ac.uk/csl18/acceptedpapers/> # Achim Jung Fest ??? ???An Intersection of Neighborhoods??? (8 Sep) For thirty years, Achim Jung has been at the forefront of research in the fields of Programming Language Semantics, Topological Logic, and, more broadly, the intersection of Computer Science, Logic, and Mathematics. The day following CSL there will be a workshop in commemoration of his career on occasion of his 60th birthday. For more information, please see <http://events.cs.bham.ac.uk/csl18/AJFest/> ## Invited Speakers * Samson Abramsky ??? University of Oxford * Thorsten Altenkirch ??? University of Nottingham * Mai Gehrke ??? Universit?? C??te d'Azur * Michael Huth ??? Imperial College * Ho Weng Kin ??? Nanyang Technological University * Jimmie Lawson ??? Louisiana State University * Michael Mislove ??? Tulane University * Frank Pfenning ??? Carnegie Mellon University * Alex Simpson ??? University of Ljubljana # Registration The fees for the conference and associated events are ------------------------------------------- ------- Early Bird Conference (Standard) ??300 Early Bird Conference (Student) ??240 Regular Conference (after 31 July) ??350 Conference Dinner ??48 Excursion Black Country Living Museum ??32 Achim Jung Fest *free* ------------------------------------------- ------- To register, please follow the link and information provided on the CSL website <http://events.cs.bham.ac.uk/csl18> For any questions please contact Dan R. Ghica <D.R.Ghica(a)cs.bham.ac.uk> [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Ivan Varzinczak, winner of the universal logic prize at UNILOG'2018
by jean-yves beziau 27 Jun '18

27 Jun '18

One of the highlights of UNILOG'2018 in Vichy was the contest Logic Prizes http://www.uni-log.org/logic-prizes-2018 with 9 winners of logic prizes from 9 countries. Each of them had 30mn to present his work facing a jury of 7 logicians. The jury then decided who was the best of them to whom the universal logic prize was attributed. The winner was announced by the president of the jury, Göran Sundholm, during the banquet: It is Ivan Varzinczak, winner of the Louis Couturat Logic Prize (France). As a winner he will be in particular invited speaker at the next UNILOG. The papers of the 9 winners will be published in a special issue of Logica Universalis http://www.logica-universalis.org/ For the next UNILOG, additionally to the 9 prizes recently created, we expect to have at least 6 more countries, reaching 15 prizes. People interested to create a logic prize in a given country can write to: prizes(a)logica-universalis.org Jean-Yves Beziau [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

CT2018 - programme now available
by CT2018 27 Jun '18

27 Jun '18

Dear colleagues, The full programme is now available at http://www.mat.uc.pt/~ct2018/program.html for the: INTERNATIONAL CATEGORY THEORY CONFERENCE - CT2018 8-14 July, 2018 - University of Azores, Ponta Delgada (S. Miguel island), Portugal Invited Speakers ?????? James Borger ?????? James Gray ?????? Anders Kock ?????? Tom Leinster ?????? Ingacio Franco Lopez ?????? Lurdes Sousa Scientific Committee ?????? Maria Manuel Clementino Richard Garner Marino Gran Martin Hyland Emily Riehl Ross Street Walter Tholen Organizing Committee ?????? Maria Manuel Clementino Margarida Raposo ?????? Paula Garr??o Jorge Picado Diana Rodelo Manuela Sobral Lurdes Sousa Looking forward to seeing you there. Best regards, OC -- Category Theory :: ct2018(a)mat.uc.pt [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

FLoC 2018 - Last Joint Call for Workshop Participation
by Andrzej Murawski 22 Jun '18

22 Jun '18

THE SEVENTH FEDERATED LOGIC CONFERENCE (FLoC 2018) 6-19 July 2018 Oxford, England, UK http://www.floc2018.org/workshops REGULAR REGISTRATION CLOSES on 25th June 2018. The seventh Federated Logic Conference (FLoC'18) will be held in Oxford, UK, in July 2018, at the Mathematical Institute and the Blavatnik School of Government at the University of Oxford. In addition to nine major international conferences related to mathematical logic and computer science, FLoC 2018 will feature 79 workshops arranged in three segments: Pre-FLoC: Sat 7 - Sun 8 (workshops related to CSF, FSCD, ITP, LICS and SAT), Mid-FLoC: Wed 11 - Sat 14 (workshops related to CAV, ICLP, IJCAR, ITP and LICS), Post-FLoC: Wed 18 - Thu 19 (workshops related to FM, CAV, ICLP and IJCAR). REGULAR REGISTRATION CLOSES on 25th June 2018. ON SITE REGISTRATION will be possible during the conference. It is imperative that you BOOK ACCOMMODATION ASAP to avoid disappointment. Website: http://www.floc2018.org/ Conference and workshops programme now live: https://easychair.org/sm art-program/FLoC2018/index.html Registration: http://www.floc2018.org/register/ Accommodation: http://www.floc2018.org/accommodation/ Registration for the main conference block gives you access to any other conference in the same period. Conference registration includes reception, lunches and coffee breaks. Stand up banquet can be added to the conference registration. Registration for a workshop day means you can attend any other workshop on the same day. Workshop registration includes lunches and coffee breaks. *** Pre-FLoC workshops (Saturday 7 - Sunday 8 July) 32nd International Workshop on Unification (UNIF 2018), 7 July http://unif2018.cic.unb.br/ 7th International Workshop on Confluence (IWC 2018), 7 July http://cl-informatik.uibk.ac.at/events/iwc-2018/ 7th International Workshop on Classical Logic and Computation (CL&C 2018), 7 July http://www.di.unito.it/~stefano/CL&C/CL&C18.htm Higher-Dimensional Rewriting and Algebra (HDRA 2018), 7 July http://hdra.gforge.inria.fr/ International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2018), 7 July http://lfmtp.org/workshops/2018/ 7th International Workshop on the Cross-Fertilization Between CSP and SAT (CSPSAT 2018), 7 July http://sysrun.haifa.il.ibm.com/hrl/cspsat2018/ <http://lfmtp.org/workshops/2018/> Pragmatics of SAT (PoS 2018), 7 July http://www.pragmaticsofsat.org/2018/ Twenty Years of Deep Inference (TYDI 2018), 7 July https://www.lix.polytechnique.fr/~lutz/orgs/TYDI2018.html 10th International Workshop on Computing with Terms and Graphs (TERMGRAPH 2018), 7 July https://nms.kcl.ac.uk/maribel.fernandez/TERMGRAPH.html Syntax and Semantics of Low-Level Languages (LOLA 2018), 7 July https://cs.appstate.edu/~johannp/lola18/ 9th Workshop on Higher Order Rewriting (HOR 2018), 7 July https://lipn.univ-paris13.fr/HOR18/ 2018 Joint Workshop on Linearity & TLLA (5th International Workshop on Linearity and 2nd Workshop on Trends in Linear Logic and Applications), 7-8 July http://lipn.univ-paris13.fr/TLLALinearity18/ Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF 2018), 7-8 July https://hott-uf.github.io/2018/ Game Semantics 25, 7-8 July http://www.gamesemantics.org/game-semantics-25 Workshop on Proof Complexity (PC 2018), 7-8 July http://easychair.org/smart-program/PC2018/ Programming And Reasoning on Infinite Structures (PARIS 2018), 7-8 July https://www.irif.fr/~saurin/RAPIDO/PARIS-2018/ 6th Workshop on Strategic Reasoning (SR 2018), 7-8 July http://projects.lsv.fr/sr18/ Workshop in honour of Dana Scott's 85th birthday and 50 years of domain theory, 7-8 July https://andrejbauer.github.io/domains-floc-2018/ 5th Workshop on Natural Language and Computer Science (NLCS 2018), 7-8 July http://www.indiana.edu/~iulg/nlcs.html 7th Workshop on Mathematically Structured Functional Programming (MSFP 2018), 8 July https://msfp2018.bentnib.org/ 5th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2018), 8 July http://researchers.lille.inria.fr/niehren/WPTE-2018/main.html The Coq Workshop 2018, 8 July https://coqworkshop2018.inria.fr/ International Workshop on Quantified Boolean Formulas and Beyond (QBF 2018), 8 July http://fmv.jku.at/qbf18/ 5th International Workshop on Graphical Models for Security (GraMSec 2018), 8 July http://gramsec.uni.lu/ Women in Logic 2018, 8 July https://sites.google.com/site/womeninlogic2018/welcome 9th Workshop on Intersection Types and Related Systems (ITRS 2018), 8 July https://www.irif.fr/~michele/itrs2018 Coalgebra Now, 8 July http://homepage.tudelft.nl/c9d1n/floc2018coalgebra/index.html 12th International Workshop on Developments in Computational Models (DCM 2018), 8 July https://sites.google.com/g.uporto.pt/dcm18 IFIP Working Group 1.6: Rewriting, 8 July http://cbr.uibk.ac.at/ifip-wg1.6/ Workshop on Foundations of Computer Security (FCS 2018), 8 July http://www.andrew.cmu.edu/user/liminjia/events/fcs2018/ Mentor Workshop 1, 8 July https://lics.siglog.org/lics18/lmw.php *** Mid-FLoC workshops (Wednesday 11 - Saturday 14 July) Satisfiability Checking and Symbolic Computation: Bridging Two Communities to Solve Real Problems (SC^2 2018), 11 July http://www.sc-square.org/CSA/workshop3.html IFAC Conference on Analysis and Design of Hybrid Systems (ADHS 2018), 11-13 July http://www.cs.ox.ac.uk/conferences/ADHS18/ 16th International Workshop on Satisfiability Modulo Theories (SMT 2018), 12-13 July http://smt-workshop.cs.uiowa.edu/2018/ CAV Tutorials, 13 July http://cavconference.org/2018/invited-speakers-tutorials/ 7th Workshop on Logic and Systems Biology (LSB), 13 July http://perso.ens-lyon.fr/russell.harmer/lsb7.html Isabelle Workshop, 13 July http://sketis.net/isabelle/isabelle-workshop-2018 25th RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion, 13 July https://sites.google.com/a/aixia.it/rcra/rcra-2018 5th Workshop on Formal Reasoning in Distributed Algorithms (FRIDA 2018), 13 July http://forsyte.at/events/frida2018/ 5th Vampire Workshop (Vampire 2018), 13 July http://easychair.org/smart-program/Vampire18/ 19th Workshop on Logic and Computational Complexity (LCC), 13 July http://www.cs.swansea.ac.uk/lcc/index.html 5th Workshop on Horn Clauses for Verification and Synthesis (HCVS 2018), 13 July https://www.sci.unich.it/hcvs18/ Workshop on Learning and Automata (LearnAut 2018), 13 July https://learnaut2018.wordpress.com/ 1st International Workshop on Multi-objective Reasoning in Verification and Synthesis (MoRe 2018), 13 July http://math.umons.ac.be/more2018/ Workshop on Modular Knowledge (Tetrapod), 13 July http://new.kwarc.info/events/Tetrapod-2018/ First Workshop on Automated Deduction for Separation Logics (ADSL 2018), 13 July http://adsl.univ-grenoble-alpes.fr/ DMW18: Deduction Mentoring Workshop, 13 July http://easychair.org/smart-program/DMW18/ Runtime Verification for Rigorous Systems Engineering (RV4RISE), 13 July http://rv4rise.conf.tuwien.ac.at/ 13th International Workshop on User Interfaces for Theorem Provers (UITP 2018), 13 July http://www.informatik.uni-bremen.de/uitp/uitp2018/ Verification Mentoring Workshop 2, 13 July http://cavconference.org/2018/verification-mentoring-workshop/ Summit on Machine Learning Meets Formal Methods, sponsored by the Alan Turing Institute, 13 July http://www.floc2018.org/summit-on-machine-learning/ 4th Workshop on Formal Integrated Development Environment (F-IDE 2018), 14 July https://sites.google.com/view/fideworkshop2018 16th International Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2018), 14 July http://www1.isti.cnr.it/~Massink/EVENTS/QAPL2018/ 16th Overture Workshop: New Capabilities and Applications for Model-based Systems Engineering, 14 July http://overturetool.org/workshops/16th-Overture-Workshop.html FM Doctoral Symposium, 14 July http://www.fm2018.org/doctoral-symposium/ *** Post-FLoC workshops (Wednesday 18 - Thursday 19 July) 18th Refinement Workshop, 18 July http://www.refinenet.org.uk/ 1st International Workshop on Parallel Logical Reasoning (PLR), 18 July https://antonwijs.wixsite.com/plr2018 7th Workshop on Synthesis (SYNT 2018), 18 July http://synt2018.seas.ucla.edu Theorem Prover Components for Educational Software (ThEdu 2018), 18 July http://www.uc.pt/en/congressos/thedu/thedu18 TLA+ Community Event 2018, 18 July http://tla2018.loria.fr/ Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP 2018), 18 July https://sites.google.com/site/aspocp2018/ International Conference on Logical Programming - Doctoral Consortium (ICLP - DC 2018), 18 July http://easychair.org/smart-program/ICLP-DC2018/ 16th International Colloquium on Implementation of Constraint and Logic Programming Systems (CICLOPS 2018), 18 July https://people.cs.kuleuven.be/~tom.schrijvers/CICLOPS2018/ 3rd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2018), 18 July http://iltp.de/ARQNL-2018/ Workshop on Logic and Practice of Programming (LPoP 2018), 18 July http://lpop.cs.stonybrook.edu/ 13th International Workshop on Constraint Based Methods in Bioinformatics (WCB 2018), 18 July http://clp.dimi.uniud.it/wcb/wcb18/ International Workshop on the Verification and Validation of Autonomous Systems (VaVAS), 18-19 July http://cgi.csc.liv.ac.uk/~michael/VaVAS-July2018/ 16th International Workshop on Termination (WST 2018), 18-19 July http://wst2018.webs.upv.es/ MLP18: Machine Learning for Programming, 18-19 July https://prodo.ai/mlp18 The LaSh 2018 Workshop on Logic and Search, 18-19 July http://www.logicandsearch.org/LaSh2018/ 10th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE 2018), 18-19 July http://vstte18.it.uu.se/ 11th International Workshop on Numerical Software Verification (NSV-XI), 18-19 July https://nsv-2018.github.io/nsv2018/ 18th International Workshop on Automated Verification of Critical Systems (AVOCS 2018), 18-19 July http://avocs18.irisa.fr/ Logics for Reasoning about Preferences, Uncertainty, and Vagueness (PRUV 2018), 19 July http://pruv18.inf.unibz.it/ Third Workshop on Fun With Formal Methods (FWFM 2018), 19 July http://persons.iis.nsk.su/en/FWFM2018 International Workshop on External and Internal Calculi for Non-Classical Logics, 19 July http://weic2018.loria.fr/ Robots, Morality, and Trust through the Verification Lens, 19 July http://qav.cs.ox.ac.uk/robots_morality_trust/ 6th Workshop on the Practical Aspects of Automated Reasoning (PAAR 2018), 19 July http://easychair.org/smart-program/PAAR-2018/ Verification of Engineered Molecular Devices and Programs (VEMDP 2018), 19 July http://dna.caltech.edu/vemdp2018/ Workshops Committee General Chair: Moshe Y. Vardi Co-chairs: Daniel Kroening, Marta Kwiatkowska Workshops Chair: Gethin Norman Workshops Deputy Chair: Christoph Haase CAV: Hana Chockler CSF: Cas Cremers FM: Helen Treharne FSCD: Paula Severi ICLP: Stefan Woltran IJCAR: Alberto Griggio ITP: Assia Mahboubi LICS: Patricia Bouyer SAT: Martina Seidl [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Open Positions in Tokyo: Formal Methods, Learning and Cyber-Physical Systems
by Ichiro Hasuo 20 Jun '18

20 Jun '18

[Thanks a lot for disseminating among potentially interested candidates. Apologies for multiple copies] Dear colleagues, For our research project (ERATO MMSD, Metamathematics for Systems Design) we are looking for senior researchers and postdocs (10+ positions in total and some are still open), together with research assistants (PhD students) and internship students. The project runs until March 2022. http://group-mmm.org/eratommsd This broad project aims to extend the realm of formal methods from software to cyber-physical systems (CPS), with particular emphases on logical/categorical metatheories and industrial application esp. in automotive industry. In order to deal with the complexity of real-world cyber-physical systems, we need to rely on empirical, learning-based and data-driven measures for quality assurance (such as search-based testing). At the same time, we are finding logical and automata-theoretic methods--the bedrock of formal verification and synthesis--playing pivotal roles also in those empirical quality assurance measures. This way, our project offers an exciting scientific environment that mixes formal methods, software engineering and machine learning. We also collaborate closely with https://www.autonomoose.net/, an automated driving project at Waterloo, Canada. The following are prerequisites for application. - Your background in one of the following fields: formal methods, programming languages, control theory, control engineering, software science, software engineering, machine learning, numerical optimization, user interface, mathematical logic or category theory - Your willingness to dive into the heterogeneous (and thus exciting!) scientific environment as described in the above For more about the project please visit http://group-mmm.org/eratommsd About the open positions http://group-mmm.org/eratommsd/openpositions.html has more information (esp. how to apply/inquire). Best regards, Ichiro ====== Ichiro Hasuo Associate Professor, National Institute of Informatics i.hasuo(a)acm.org http://group-mmm.org/~ichiro/ [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Announcement about Rudolf Fritsch
by Michael Barr, Prof. 20 Jun '18

20 Jun '18

I regret to announce that last week I received the information that Rudolf Fritsch had died. Here is the email I received from his wife Gerda: Dear Mike, in the early morning hours of Tuesday, June 12th, 2018, my husband passed away. Please find the notice of death in the attachment. Rudo suggested that you might want to distribute the message on the categories list. Sincerely yours, Gerda Fritsch The attachment was too large to post on the categories list. Michael [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

change of base and co/limit preservation
by Christian Williams 17 Jun '18

17 Jun '18

Let F: V -> W be a monoidal functor, and F*: VCat -> WCat be the change of base; suppose T: A->B is a V-functor which preserves a class of weighted co/limits {(j_i: K ->A, w_i: K -> V)}. What is the correct notion of preservation for F*T; i.e. what is the corresponding class of W-co/limits? It seems reasonable to be {(F*(j_i),F*(w_i)}, but I have not found a good reference for this. Under what conditions does F* "preserve co/limit preservation"? There seem to be some interesting questions here. Has this been studied in any depth? Thank you. Sincerely, Christian Williams [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Re: Point-free affine real line?
by Vaughan Pratt 12 Jun '18

12 Jun '18

Peter is right that Q as a field contains order information absent from Q as either a linear or affine space. (−*x*² ≤ 0 ≤ *x*².) > For the order to be definable from the algebraic structure, you need to consider Q as a field It certainly suffices, and indeed is traditional. But is it necessary for the construction of the affine real line? In particular do we have to define multiplication on the rationals only to throw it away at a later stage? Obviously the ordered dyadic rationals would suffice. Equally obviously they don't form a field. But can they be defined as an ordered affine space with the same degree of formality and economy as we routinely define the ordered linear space of rationals? Claim. The ordered algebra (D, xy, x+y, ≤) consisting of the set D of dyadic rationals under the two binary operations xy denoting 2y - x and x+y denoting (x + y)/2 can be defined order-algebraically up to isomorphism as the free ordered algebra on the ordinal 2 satisfying finitely many equations in the two operations along with the inference rules, from x ≤ y infer each of y ≤ xy yx ≤ x x ≤ x+y x+y ≤ y The Dedekind cuts being cuts in the rational line, the following claim depends on a distinct name for the corresponding notion of a cut in the ordered affine line of dyadic rationals, which I suggest calling a dyadic cut. (When cutting at a dyadic rational follow a consistent convention as to which side to associate that rational, as done with the Dedekind cuts, and always have both sides of the cut nonempty.) Claim. The dyadic cuts in the ordered affine space of dyadic rationals are in order-preserving bijection with the Dedekind cugts in the ordered linear space of rationals, with the cuts at dyadic rationals correctly matched to their Dedekind counterparts. Vaughan Pratt On Sun, Jun 10, 2018 at 6:54 AM, Peter Johnstone <ptj(a)dpmms.cam.ac.uk> wrote: > Sorry, what I wrote was a bit sloppy. Vaughan is right that the problem > doesn't arise with the passage from considering Q as a linear space > to considering it as an affine space, since it already has order- > reversing linear automorphisms. For the order to be definable from > the algebraic structure, you need to consider Q as a field, which is > what the usual Dedekind-section construction does. > > Peter Johnstone > > > On Thu, 7 Jun 2018, Vaughan Pratt wrote: > > > Not quite: the affine rational line doesn't have a definable total >> order, >> >>> since it has order-reversing automorphisms, so any definition using >>> Dedekind sections is problematic. >>> >> >> Morphism-wise, since the affine transformations are just the composition >> of >> a linear transformation with a translation, and translation of the >> rational >> line preserves order, affinity can't be the problem here. >> >> Structure-wise, one can equip the rational line with either its linear >> combinations or its linear order, or both. Using both eliminates the >> order-reversing linear transformations. "Affine" only makes sense in the >> context of having the linear combinations, as "affine" limits the linear >> combinations to those whose coefficients sum to one. If it is ok for the >> linear combinations and the linear order to coexist, it must be even more >> ok for the affine combinations and the linear order to coexist. >> >> So whether one considers the morphisms or the structure they preserve, >> affinity (affineness?) must be a red herring here: any problem for the >> rational line as an affine space is surely also a problem for it as a >> vector space. >> >> Vaughan Pratt >> >> >> [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Re: Point-free affine real line?
by Steve Vickers 10 Jun '18

10 Jun '18

Dear Johannes, "Point-free" is as opposed to "point-set" - there is no assumption that the real numbers form a set. Instead, they are taken to be the models of a (geometric) theory of Dedekind sections of the rationals (which do form a set). More generally, a point-free space is one where the points are defined as models of a propositional geometric theory. The topology is then defined intrinsically, opens being the geometric propositions. My motivation for this comes from topos theory. In any elementary topos, each point-free space does in fact have a set (object) of points. Topologically, it amounts to approximating bundles by local homeomorphisms. However, that construction is not geometric - preserved by inverse image functors, and by pullback of bundles -, so the point-set version is not robust under change of base. There are advantages to staying within the geometric fragment of elementary topos logic, and I am exploring how far that can be taken. I also now have other semantics using arithmetic universes, where the point-set versions simply don't exist. If it helps, the point-free real line in an elementary topos E is the localic geometric morphism p: F -> E got from F as topos of sheaves of the internal locale of formal reals in E. If E is an S-topos, then you can do this generically over S to get R as the S-classifier for Dedekind sections, and then p is just the bipullback E x_S R. A point-set R would be some local homeomorphism over E (then equipped separately with a topology), but in general it is not got as a bipullback of a local homeomorphism over S. The question about the affine real line represents a challenge to this geometric approach, and I'd like to form a better idea of whether it is simply a difficult problem, or a fundamental limitation to my approach. To put it another way, am I following in Grothendieck's footsteps in the way I think of toposes, or am I mishandling his ideas in ways that have no bearing on what he was trying to do? All the best, Steve. On 01/06/2018 10:22, huebschm(a)math.univ-lille1.fr wrote: > Dear Steve > > I am not sure whether I understand. > What precisely do you mean by "point-free"? > > > > On Thu, 31 May 2018, Steve Vickers wrote: > >> Algebraic geometry defines the affine line over a field k as an >> affine scheme, > the spectrum of k[X]. It includes a copy of k, each element a being > present as the irreducible polynomial X-a, > with local ring the ring of fractions got by inverting polynomials > f(X) such that f(a) is non-zero. >> >> You can carry this out for the real line R, but it is very much R as >> a set, and the copy of R in the underlying space of the spectrum has >> the discrete topology. > > > > > The standard approach leads to the Zariski topology. > > > >> Does algebraic geometry provide an analogous construction that could >> lead to the point-free R? Can the locally ringed space be >> topologized (point-free) so that the copy of R has its usual topology? >> >> I've run into various problems. >> >> 1. It is not obvious to me that R[X] exists point-free. By that I >> mean that, without presupposing a set R[X], or using non-geometric >> constructions, I can't see how to define a geometric theory whose >> models are the polynomials. The problem comes with trying to pin down >> the requirement that all but finitely many of the coefficients of a >> polynomial must be zero. You cannot continuously define the degree of >> a polynomial, because the function R -> N, a |-> degree(aX + 1), is >> not continuous. >> >> That suggests the construction as Spec(R[X]) might have to be >> adjusted. Is there still some locally ringed space that does the trick? >> >> 2. The "structure sheaf" cannot be a sheaf. We hope its fibres are >> point-free local rings, but, whatever they are, they must be >> R-algebras and so cannot have the discrete topology. The space is >> locally ringed by some bundle other than a sheaf (local homeomorphism). >> >> 3. The usual local rings, got as rings of fractions as described >> above, may be problematic point-free in the same way as R[X] is. >> I don't know what would do instead. The power series ring R[[X]]? > > > > The power series ring recovers a single point ("formal geometry" in > the sense of Grothendieck, Gelfand-Kazhdan, Kontsevich, etc.). > > > Best Johannes > > > > >> (At least as fibre over 0.) >> It does have the property of inverting those polynomials f for which >> f(0) > is non-zero. And it can be defined point-free, as R^N. (However, the > finitely presented approximations R[X|X^n = 0] happily exist point-free.) >> >> Thanks for any references you can provide, >> >> Steve. >> >> [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

4 5