Dear Dear Marta, Martin, Steve and Thomas, I am considering using the word "logos" instead of "elementary topos". https://en.wikipedia.org/wiki/Logos The word "logos" has seldom been used in mathematics. It is a noble word in philosophy where it means: reason, discourse, logic, knowledge, principle of order. The category of sets is a boolean logos with natural number objects. Every (Grothendieck) topos has the structure of a logos, but not every logos is a topos. The initial logos with natural number object and the effective logos are not toposes. A topos E over a base topos S can be regarded as a topos internal to the logos defined by S. More generally, there is a notion of topos relative to a logos. Best regards, André ________________________________ From: Marta Bunge [martabunge@hotmail.com] Sent: Friday, November 04, 2016 8:34 PM To: Martin Escardo; Joyal, André; categories@mta.ca; Steve Vickers Cc: Thomas Streicher Subject: Re: categories: Re: Grothendieck toposes Dear Martin, Andre, and Steve, I will abstain from commenting on the "mystery" of univalence at least until I study the paper by Martin and Thomas (Streicher) which was made kindly made available to me but have not yet found the time to do so. Since Martin in his latest mail goes back to the original question by Steve which prompted some of this correspondence on and off categories, I point out that I had already accepted regarding Grothendieck toposes as S-bounded elementary toposes for a given elementary topos S, as the idea is the same as that of Grothendieck - namely sheaves on a site, without, however, specifying a set theory to be given by Set but by some unspecified elementary (base) topos S. It is not a matter of honesty but of revising the notion of a Grothendieck topos which arose before elementary toposes were introduced. There was, however, another, in my view still not totally settled question in this forum, of whether the notion of an elementary topos ought to be equated with that of a "logical" topos as proposed by Andre, so that the "natural" morphisms bewteen them, according to him, would be the logical morphisms. As I already argued in this forum, the notion of an elementary topos is no more logical than it is geometric, and the way to specify which will it be in any given context is by the choice of morphisms - logical or geometrical, with possibly further conditions in each case. In connection with the latter, I came upon an old paper by Colin McLarty, "The uses and abuses of the history of topos theory", British J. Phil Sc. 41 (1990) 351--375, in which this issue is discussed at length. I reproduce the abstract here: "The view that toposes originated as a generalized set theory is a figment of set theoretically educated common sense. This false history obstructs understanding of category theory and specially of categorical foundations for mathematics. Problems in geometry, topology, and related algebra led to categories and toposes. Elementary toposes arose when Lawvere's interest in the foundations of physics and Tierney's in the foundations of topology led both to study Grothendieck's foundations for algebraic geometry. I end with remarks on a categorical view of the history of set theory, including a false history plausible from that point of view that would make it helpful to introduce toposes as a generalization of set theory." I recommend readin this very interesting article. Very best regards, Marta ************************************************ Marta Bunge Professor Emerita Dept of Mathematics and Statistics McGill University Montreal, QC, Canada H3A 2K6 Home: (514) 935-3618 marta.bunge@mcgill.ca http://www.math.mcgill.ca/people/bunge ************************************************ ________________________________ From: Martin Escardo <m.escardo@cs.bham.ac.uk> Sent: November 4, 2016 7:17:43 PM To: Joyal, André; Marta Bunge; Steven Vickers Subject: Re: categories: Re: Grothendieck toposes And, to continue, I think it is slightly dishonest to say that Grothendiek toposes are defined over Set, as if Set were one uniquely determined thing. It is not, and we know that there are many things (as soon as there is as least one) satisfying the axioms of set theory. Why do we still speak of "the" category of sets, as if we would be able to magically pin one "intended model" (with no precise specification)? Martin On 04/11/16 22:56, Martin Escardo wrote:

But here is a more mundane question.

Mathematical language is precise. Natural language is not. How can we define a precise mathematical language using an imprecise natural language?

When two mathematicians disagree in their chosen foundations, they will nevertheless be able to understand each other's rules and be able to follow them (if they are willing to, or if they are pressed to do so). At some level, the "very basic" foundation seems to be universal (but is it?). So, for example, if I disagreed with type theory as a foundation, I would nevertheless be able to understand its rules of operation (either at a rigorous informal level, or at a formal level if the theory is formalized) and follow its formal proofs.

In particular, how can the precise notion of formal system be defined using imprecise natural language (as we do).

Martin

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]