Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorThomas Holder
   • CommentTimeNov 12th 2014
   • PermaLink
   Author: Thomas Holder
   Format: MarkdownItexI threw in some references to the early topos approach to set theory in [[ETCS]]. On this occasion I couldn' t resist the temptation to rearrange somewhat the lay-out of the entry: actually I thought it better not to throw HOTT immediately at the reader and gave Palmgren's ideas a proper subsection. I've also deflated a bit the foundational claims of ETCS sticking more to what appears to me to be Lawvere's original intentions.

   I threw in some references to the early topos approach to set theory in ETCS. On this occasion I couldn’ t resist the temptation to rearrange somewhat the lay-out of the entry: actually I thought it better not to throw HOTT immediately at the reader and gave Palmgren’s ideas a proper subsection. I’ve also deflated a bit the foundational claims of ETCS sticking more to what appears to me to be Lawvere’s original intentions.

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeNov 12th 2014
   • (edited Nov 12th 2014)
   • PermaLink
   Author: Urs
   Format: MarkdownItexGood, thanks. But what's a reference supporting the footnote statement "It appears that Lawvere had intended ETCS merely as a practical tool" ? I wouldn't extract that statement for instance from _[[Cohesive Toposes and Cantor's lauter Einsen]]_ (which is a comment on a comment sombody made on ETCS).

   Good, thanks.

   But what’s a reference supporting the footnote statement “It appears that Lawvere had intended ETCS merely as a practical tool” ?

   I wouldn’t extract that statement for instance from Cohesive Toposes and Cantor’s lauter Einsen (which is a comment on a comment sombody made on ETCS).

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeNov 12th 2014
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexMaybe he means the fact Lawvere mentioned somewhere that ETCS was originally invented in order to teach students about sets?

   Maybe he means the fact Lawvere mentioned somewhere that ETCS was originally invented in order to teach students about sets?

4. • CommentRowNumber4.
   • CommentAuthorThomas Holder
   • CommentTimeNov 12th 2014
   • (edited Nov 12th 2014)
   • PermaLink
   Author: Thomas Holder
   Format: TextI was afraid somebody would bring this up because for the moment I don't have a very handy quotation for this. So it is a somewhat personal opinion and therefor relegated to the footnotes and hedged as 'appearance' though it is the result of a close reading of his writings. On the risk of starting a prairie fire to rationally back up my claim provisorily: 1. Lawvere has a very weak concept of foundations as a condensation of the actual practice of mathematics that serves the purpose to advance mathematics by making it more teachable (increase of a knowledgable community) and by producing new facets or objects of study for the already existing expert community. So in a sense foundations for Lawvere are generally merely practical tools they don't serve a purpose of fencing a paradise against doubt or contradiction. 2. Historically, as Mike points out, ETCS served the purpose of undergraduate education and the foundational aspirations were concentrated in the contemporary ETCC from (1963) which has its own peculiar take on sets as discrete categories. As far I as I can tell in Lawvere's writing no foundational claim is brought forward for ETCS and there is always division of labor between ETCC and ETCS which is set theory for undergraduates as exemplified by the 2003 book. So I understand Lawvere as saying that ETCS axiomatizes mathematical objects of a very special form -constant sets which play an important but limited role. This limitation extends also to their structural axiomatization: what one gains by ETCS is a structural-categorical way of thinking and easy graspable notions of set. By itself ETCS could at best be part of a larger program of getting rid of sets like ETCC. 3. I basically see two actual uses of sets in Lawvere: that is firstly, at the gros topos level as yielding a dialectical contradiction providing constancy as a background for variation-cohesion and here Lawvere leaves no doubt, that the constant base S is built from the cohesive E at least morally (the Münchhausen trick of the thesis). Secondly, at the petit level where they play the role of parametrizers. I can't see how somebody holding such a view of sets as derivatives could want to base mathematics on their axiomatization. So it is my impression that one should not, based on the equivalence to some weak version of classical set theory, read ETCS as a stand in for ZFC in foundations with capital f , because it amounts in some sort to admit the adequacy of ZFC for mathematics and acceptance of Foundations. At least I can hardly square this with Lawvere's views on the limited role that sets play in mathematics. The claim in 'lauter Einsen' seems to me to be that Cantor held a dialectical and structural view of sets that is a more modern view than the classical set theory he is supposed to have founded. The remark of Myhill in the ETCS course is an introductory peg. The paper itself subscribes in my view to a loosely 'cohesive variant' of ETCC view i.e. it refers to the Münchhausen internal definition of sets as doubly embedded discretes in the cohesive topos neither the discrete base and certainly not the cohesive could in this context supposed to satisfy choice in general. The cohesive foundations with small f are intended to promote SDG and geometry therefor the Foundational claims are rather deflated. As I don't want to engage in a fight about this being somebody who writes foundations even without an f and therefor attracted by Lawvere foundations I easily step down and omit the footnote but to the best of my knowledge ETCS has at best a minor part in the big Lawverian play of categorical foundations - a part without a capital f.

   I was afraid somebody would bring this up because for the moment I don't have a very handy quotation for this. So it is a somewhat personal opinion and therefor relegated to the footnotes and hedged as 'appearance' though it is the result of a close reading of his writings.
   
   On the risk of starting a prairie fire to rationally back up my claim provisorily:
   
   1. Lawvere has a very weak concept of foundations as a condensation of the actual practice of mathematics that serves the purpose to advance mathematics by making it more teachable (increase of a knowledgable community) and by producing new facets or objects of study for the already existing expert community. So in a sense foundations for Lawvere are generally merely practical tools they don't serve a purpose of fencing a paradise against doubt or contradiction.
   
   2. Historically, as Mike points out, ETCS served the purpose of undergraduate education and the foundational aspirations were concentrated in the contemporary ETCC from (1963) which has its own peculiar take on sets as discrete categories. As far I as I can tell in Lawvere's writing no foundational claim is brought forward for ETCS and there is always division of labor between ETCC and ETCS which is set theory for undergraduates as exemplified by the 2003 book.
   
   So I understand Lawvere as saying that ETCS axiomatizes mathematical objects of a very special form -constant sets which play an important but limited role. This limitation extends also to their structural axiomatization: what one gains by ETCS is a structural-categorical way of thinking and easy graspable notions of set. By itself ETCS could at best be part of a larger program of getting rid of sets like ETCC.
   
   3. I basically see two actual uses of sets in Lawvere: that is firstly, at the gros topos level as yielding a dialectical contradiction providing constancy as a background for variation-cohesion and here Lawvere leaves no doubt, that the constant base S is built from the cohesive E at least morally (the Münchhausen trick of the thesis). Secondly, at the petit level where they play the role of parametrizers. I can't see how somebody holding such a view of sets as derivatives could want to base mathematics on their axiomatization.
   
   So it is my impression that one should not, based on the equivalence to some weak version of classical set theory, read ETCS as a stand in for ZFC in foundations with capital f , because it amounts in some sort to admit the adequacy of ZFC for mathematics and acceptance of Foundations. At least I can hardly square this with Lawvere's views on the limited role that sets play in mathematics.
   
   The claim in 'lauter Einsen' seems to me to be that Cantor held a dialectical and structural view of sets that is a more modern view than the classical set theory he is supposed to have founded. The remark of Myhill in the ETCS course is an introductory peg. The paper itself subscribes in my view to a loosely 'cohesive variant' of ETCC view i.e. it refers to the Münchhausen internal definition of sets as doubly embedded discretes in the cohesive topos neither the discrete base and certainly not the cohesive could in this context supposed to satisfy choice in general. The cohesive foundations with small f are intended to promote SDG and geometry therefor the Foundational claims are rather deflated.
   
   As I don't want to engage in a fight about this being somebody who writes foundations even without an f and therefor attracted by Lawvere foundations I easily step down and omit the footnote but to the best of my knowledge ETCS has at best a minor part in the big Lawverian play of categorical foundations - a part without a capital f.
5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeNov 12th 2014
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks for the informed reply. Don't worry, I am not trying to pick a fight, I am just showing interest in your statement. Some reflection of your reply would serve well on the $n$Lab entry.

   Thanks for the informed reply. Don’t worry, I am not trying to pick a fight, I am just showing interest in your statement. Some reflection of your reply would serve well on the $n$Lab entry.

6. • CommentRowNumber6.
   • CommentAuthorDavid_Corfield
   • CommentTimeNov 13th 2014
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexRe #4 > Lawvere has a very weak concept of foundations We've called it [[practical foundation of mathematics]]. Hmm, looking at this, are we sure about we want to suggest that like a type theory such as HoTT is practical but lacks something that proof-theoretic foundations has, see [[foundation of mathematics]]?

   Re #4

   Lawvere has a very weak concept of foundations

   We’ve called it practical foundation of mathematics.

   Hmm, looking at this, are we sure about we want to suggest that like a type theory such as HoTT is practical but lacks something that proof-theoretic foundations has, see foundation of mathematics?

7. • CommentRowNumber7.
   • CommentAuthorUrs
   • CommentTimeNov 13th 2014
   • (edited Nov 13th 2014)
   • PermaLink
   Author: Urs
   Format: MarkdownItexThomas's Holder's #4 made me think a bit. I may not be aware of past debates and disputes that are being alluded to re capitalization. But the phrase about paradises free of doubt and contradiction made me realize that I have an interest in foundations rather different from such matters. The reason that I got interested in matters of foundations is because looking around I find an increasing lack of scientists to agree on common ground. I come from fundamental high energy mathematical physics which is seeing an increasing fragmentation where the ability is increasingly vanishing to agree across boundaries of little subgroups on what even the subject is. In mathematics the situation is comparatively much better, but even here one sees all around experts of field A flat out dismissing the relevance of fields B and (and that's the disturbing bit) vice versa. I may be wrong, not knowing as much as Thomas does about these matters, but when I see discussion such as _[[Toposes of laws of motion]]_ I sense the desire to establish a common ground that extracts a key essenenc on which one might meet and agree that it defines the subject matter at hand, to proceed more productively from. David Corfield's [talk](http://ncatlab.org/schreiber/show/Sur+la+notion+d%27identification+en+physique+et+en+mathématiques#Corfield) today I think made this kind of point for the field of philosophy of mathematics: here the fragmentation is immense and it would seem rather useful to find a good common ground. That's foundations for me. And it seems to me all three of 1) important, 2) missing, 3) possible and within reach. And my impression is that this is what Lawvere has been pushing towards all along. Of course I may be wrong.

   Thomas’s Holder’s #4 made me think a bit. I may not be aware of past debates and disputes that are being alluded to re capitalization. But the phrase about paradises free of doubt and contradiction made me realize that I have an interest in foundations rather different from such matters.

   The reason that I got interested in matters of foundations is because looking around I find an increasing lack of scientists to agree on common ground. I come from fundamental high energy mathematical physics which is seeing an increasing fragmentation where the ability is increasingly vanishing to agree across boundaries of little subgroups on what even the subject is. In mathematics the situation is comparatively much better, but even here one sees all around experts of field A flat out dismissing the relevance of fields B and (and that’s the disturbing bit) vice versa.

   I may be wrong, not knowing as much as Thomas does about these matters, but when I see discussion such as Toposes of laws of motion I sense the desire to establish a common ground that extracts a key essenenc on which one might meet and agree that it defines the subject matter at hand, to proceed more productively from.

   David Corfield’s talk today I think made this kind of point for the field of philosophy of mathematics: here the fragmentation is immense and it would seem rather useful to find a good common ground.

   That’s foundations for me. And it seems to me all three of 1) important, 2) missing, 3) possible and within reach. And my impression is that this is what Lawvere has been pushing towards all along. Of course I may be wrong.

8. • CommentRowNumber8.
   • CommentAuthorThomas Holder
   • CommentTimeNov 14th 2014
   • PermaLink
   Author: Thomas Holder
   Format: TextMy apologies for the pause. But I can't really fix my ideas concerning 'foundations' meaning I don't have anything illuminating to say on it from the hip. When I say that I write it without f I mean that I don't worry enough if the mathematical concepts I am interested in are consistent to invest time that I can use for a better understanding of the concepts. I think this is basically the usual attitude: worry on foundations only when you need to. I think it is basically the attitude of Lawvere. The reason is that precision is often at risk of pedantry. Another reason to be casual in such matters, is that the actual practice of mathematics also seems to rely to a considerable extent on techniques; that is actual proofs not only have a syntactic side of well-formed moves in a formal game and a propostional content but they arrange themselves in proof patterns and my guess is that to large extent mathematics actually consists of manipulation and creation of such proof gestalten. But these are submitted rather to criteria of aesthetics and pragmatics and escape usual criteria of correctness: an idea can be nice without being correct. Newtonian mechanics fails Hamiltonian systems stay. On the other hand I wouldn't dismiss the classical attempts lighthandedly as 'speculative' or ill-conceived: ZFC lets mathematicians go about their business, Frege probably exaggerated the German 'Gründlichkeit' but the motivation for his system namely the disappearance of classical ontology (the defiance of geometric intuition due to new foundations of analysis and geometry) and the unclarity of the concept of number seem to me most honorable motivation for such an undertaking, well Russell he probably wrote PM to prove a point against idealism but then that is how type theory got started (in the end it's the teflon pan that justifies the space project!) and for Hilbert I have a profound admiration: as I said ideas can be nice without being correct and his axiomatic method is really a way of living meaning he actually had an integral understanding of the role of axiomatics as a means to integrate science. Another facet of foundations which I am not quite sure that it in fact complies with Lawvere's own ideas of foundation as concentration is this taking a close look at the really basic stuff- take no idea for granted! This radicality underpining the quest for cohesion is certainly what interests me there. Although Lawvere's approach is influenced or modelled on axiomatisations a la Eilenberg-Stenrod or Lawvere-Tierney the project for my taste is a bit more radical as I see it as an axiomatization of the concept of space willing to throw overboard a lot of topology. Ultimately it seems to me to be an attempt to redo analysis and geometry since 1830 especially influenced by the idea of 'saving the appearances' i.e. the geometric intuition. This seems potentially much more disruptive for the ' ruhigen Gang der Wissenschaft' than the smooth flow of algebra and geometry as codified by Eilenberg-Stenrod or Cartan-Eilenberg. So it might be useful to differentiate a refoundation from a foundation. The funny thing is that even if such a cohesive earthquake would eventually take place the methods of mathematics wouldn't be much shaken.

   My apologies for the pause. But I can't really fix my ideas concerning 'foundations' meaning I don't have anything illuminating to say on it from the hip. When I say that I write it without f I mean that I don't worry enough if the mathematical concepts I am interested in are consistent to invest time that I can use for a better understanding of the concepts. I think this is basically the usual attitude: worry on foundations only when you need to. I think it is basically the attitude of Lawvere. The reason is that precision is often at risk of pedantry.
   
   Another reason to be casual in such matters, is that the actual practice of mathematics also seems to rely to a considerable extent on techniques; that is actual proofs not only have a syntactic side of well-formed moves in a formal game and a propostional content but they arrange themselves in proof patterns and my guess is that to large extent mathematics actually consists of manipulation and creation of such proof gestalten. But these are submitted rather to criteria of aesthetics and pragmatics and escape usual criteria of correctness: an idea can be nice without being correct. Newtonian mechanics fails Hamiltonian systems stay.
   
   On the other hand I wouldn't dismiss the classical attempts lighthandedly as 'speculative' or ill-conceived: ZFC lets mathematicians go about their business, Frege probably exaggerated the German 'Gründlichkeit' but the motivation for his system namely the disappearance of classical ontology (the defiance of geometric intuition due to new foundations of analysis and geometry) and the unclarity of the concept of number seem to me most honorable motivation for such an undertaking, well Russell he probably wrote PM to prove a point against idealism but then that is how type theory got started (in the end it's the teflon pan that justifies the space project!) and for Hilbert I have a profound admiration: as I said ideas can be nice without being correct and his axiomatic method is really a way of living meaning he actually had an integral understanding of the role of axiomatics as a means to integrate science.
   
   Another facet of foundations which I am not quite sure that it in fact complies with Lawvere's own ideas of foundation as concentration is this taking a close look at the really basic stuff- take no idea for granted! This radicality underpining the quest for cohesion is certainly what interests me there. Although Lawvere's approach is influenced or modelled on axiomatisations a la Eilenberg-Stenrod or Lawvere-Tierney the project for my taste is a bit more radical as I see it as an axiomatization of the concept of space willing to throw overboard a lot of topology. Ultimately it seems to me to be an attempt to redo analysis and geometry since 1830 especially influenced by the idea of 'saving the appearances' i.e. the geometric intuition. This seems potentially much more disruptive for the ' ruhigen Gang der Wissenschaft' than the smooth flow of algebra and geometry as codified by Eilenberg-Stenrod or Cartan-Eilenberg. So it might be useful to differentiate a refoundation from a foundation. The funny thing is that even if such a cohesive earthquake would eventually take place the methods of mathematics wouldn't be much shaken.
9. • CommentRowNumber9.
   • CommentAuthorTobyBartels
   • CommentTimeNov 17th 2014
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexHowever Lawvere intended it, $ETCS$ does serve as a foundation for ordinary mathematics as well as $ZFC$ does, indeed better. The extra strength granted by Replacement is hardly ever needed, and one can always add it (along with large cardinal axioms or whatever else) if it\'s wanted. And the language fits modern abstract mathematics better, even though there remain people who will deny that. It is inadequate, but only in ways that $ZFC$ is also inadequate (including ways that $HoTT$ rectifies). So I\'m all for calling $ETCS$ a foundation with any and all capital letters. At the same time, we should represent Lawvere\'s motivations accurately.

   However Lawvere intended it, $ETCS$ does serve as a foundation for ordinary mathematics as well as $ZFC$ does, indeed better. The extra strength granted by Replacement is hardly ever needed, and one can always add it (along with large cardinal axioms or whatever else) if it's wanted. And the language fits modern abstract mathematics better, even though there remain people who will deny that. It is inadequate, but only in ways that $ZFC$ is also inadequate (including ways that $HoTT$ rectifies).

   So I'm all for calling $ETCS$ a foundation with any and all capital letters. At the same time, we should represent Lawvere's motivations accurately.

10. • CommentRowNumber10.
    • CommentAuthorThomas Holder
    • CommentTimeNov 17th 2014
    • (edited Nov 17th 2014)
    • PermaLink
    Author: Thomas Holder
    Format: TextThanks for bringing this up again! The pause in between was actually due to my worries that my intervention was mistaken. Especially after I saw the good press for ETCS at [[foundation of mathematics]] and given the fact that the texts where Lawvere actually deals with ETCS like the 1965 squib, the TAC reprint or the Rosebrugh book are the texts I am least familiar with. So I would propose to repair the idea section back to univocal claim that this is foundations and point to the more thorough discussion of ETCS in this context at the above mentioned link. As I pointed out above I am also willing to withdraw the footnote or change it as I don't think it worth to fight over this. I still think for the reasons that I brought up that the view that Lawvere's attitude toward set-theoretic 'foundations' is better represented in the context of his axiomatics for cohesion hence are closer to cohesive HOTT than to a structural version of ZFC.

    Thanks for bringing this up again! The pause in between was actually due to my worries that my intervention was mistaken. Especially after I saw the good press for ETCS at foundation of mathematics and given the fact that the texts where Lawvere actually deals with ETCS like the 1965 squib, the TAC reprint or the Rosebrugh book are the texts I am least familiar with. So I would propose to repair the idea section back to univocal claim that this is foundations and point to the more thorough discussion of ETCS in this context at the above mentioned link.
    
    As I pointed out above I am also willing to withdraw the footnote or change it as I don't think it worth to fight over this. I still think for the reasons that I brought up that the view that Lawvere's attitude toward set-theoretic 'foundations' is better represented in the context of his axiomatics for cohesion hence are closer to cohesive HOTT than to a structural version of ZFC.
11. • CommentRowNumber11.
    • CommentAuthorThomas Holder
    • CommentTimeNov 17th 2014
    • PermaLink
    Author: Thomas Holder
    Format: MarkdownItexThe passage in [[ETCS]] now reads: The **Elementary Theory of the Category of Sets** , or _ETCS_ for short, is an axiomatic formulation of [[set theory]] in a [[category theory|category-theoretic]] spirit. As such, it is the prototypical [[structural set theory]]. Proposed shortly after [[ETCC]] in ([Lawvere 65](#Lawvere65)) it is also the paradigm for a [[foundations|categorical foundation]] of mathematics.[^Law] [^Law]: For a careful comparative discussion of its virtues as foundation see [[foundations of mathematics]] or the [texts by Todd Trimble](#ExpositionByTrimble) referred to below.

    The passage in ETCS now reads:

    The Elementary Theory of the Category of Sets , or ETCS for short, is an axiomatic formulation of set theory in a category-theoretic spirit. As such, it is the prototypical structural set theory. Proposed shortly after ETCC in (Lawvere 65) it is also the paradigm for a categorical foundation of mathematics.¹

    ---

    1. For a careful comparative discussion of its virtues as foundation see foundations of mathematics or the texts by Todd Trimble referred to below. ↩

12. • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeNov 25th 2014
    • PermaLink
    Author: Urs
    Format: MarkdownItexThanks! (Now I have finally come back to this thread :-)

    Thanks!

    (Now I have finally come back to this thread :-)