3 ms·

Not downvoting,in particular there are useful links in your post. But note that by foundations one has atleast two different meanings. One meaning being examin

by enugu 5y ago

Not downvoting,in particular there are useful links in your post. But note that by foundations one has atleast two different meanings. One meaning being examining the consistency of axioms or finding weakest set of axioms for a theorem. The other meaning being - finding a foundation in which a given mathematical theory is naturally and easily described, analogus to designing a programming language in which the programs are easy to describe. Most of the time in mathematics, this is done by defining high level concepts and working from there - no need to change the foundational axioms or rules of inference. But sometimes we need more - for instance, if you read the book "Synthetic Differential Geometry", infinitesimals are naturally embedded in the theory by working in a cartesian closed category of sets. One can either embed this in ZFC using cumbersome models, or change the logic itself(remove the law of excluded middle). The logic in HOTT deals with equality in a more careful way than the usual foundations. This is not restricted to algebraic topology alone - it certainly includes algebraic geometry and tackles a general issue which will plausibly have many more applications once the technology is available. The field of noncommutative geometry, in the style of Connes, is also about this as the problem of taking quotients is another way of the stating the issue with equality. It is a work in progress and might take some time before bearing substantive fruit, but note that the current alternative is that any student learning higher level mathematics at the level of Lurie's books has to go through a huge amount of foundational material while the ideas themselves may not be intrinsically complicated. Instead, this complexity is an artifact of embedding the theory in current foundations like the SDG example mentioned above. With a new foundations, there is the possibility that we can teach the material at this level to students except that there are some tweaks in foundations.

spekcular 5y ago
I don't have much to say here that I didn't already say above about the meta-mathematical issues. However, about object-level mathematical issues, you write: "It is a work in progress and might take some time before bearing substantive fruit, but note that the current alternative is that any student learning higher level mathematics at the level of Lurie's books has to go through a huge amount of foundational material while the ideas themselves may not be intrinsically complicated. Instead, this complexity is an artifact of embedding the theory in current foundations like the SDG example mentioned above." Higher category theory is not the same thing as homotopy type theory. One does not need to learn anything about the foundations of mathematics to read and understand Lurie's work. As far as I know, issues of ZFC vs type theory simply do not arise. You can just pick up Higher Topos Theory and start reading, assuming you have a strong background in algebraic topology. The linked article is only about higher category theory and making sure all of its claims are written down in a clear and rigorous fashion to be maximally useful to workers in the field. It has nothing to do with the foundations of mathematics as a whole.
- enugu 5y ago
  > One does not need to learn anything about the foundations of mathematics to read and understand Lurie's work. By foundations here, I didnt mean foundations of mathematics, rather the amount of material a student needs to read to become familiar with the basic definitions of what a space means. We can teach topology to undergrads, can we teach higher categorical notions of space? Even schemes themselves had a daunting reputation some time back, now we have derived stacks which involve infinite categories. > You can just pick up Higher Topos Theory and start reading Yes, but my point, as illustrated in SDG example, was that definitions can be easy or hard depending on which foundations you use. You havent mentioned whether you disagree with this and if you see Kock's book, I think you will agree. When dealing with higher categories, a foundations which uses '=' symbol in a different way, with an equivalence relation(modelled on homotopy equivalence) playing a much more prominent role could make the theory much more natural. Note, that I am not even emphasizing sets vs type theory here, but excluded middle and a good notion of equivalence(and equivalence between equivalences... like in homotopy theory) in the foundations. Maybe a lot of this debate will get dissolved if we just use two different words for 'examining consistency of axioms' and 'naturality of theory as encoded in a given system' instead of using the same word - foundations - for both of them. At the very least if discussions begin with an awareness of this distinct usage, there would be lot less talking past each other. Urs Schreiber makes the same point about naturality here - https://golem.ph.utexas.edu/category/2016/03/foundations_of_mathematics.html https://golem.ph.utexas.edu/category/2016/03/foundations_of_...
  - spekcular 5y ago
    1) Yeah, Lurie's books are advanced tracts aimed at specialists in algebraic topology. Of course there are going to be substantial prerequisites. This is sort of inevitable if you want to understand the motivating applications. 2) Why would we ever want to teach higher categorical notions of space to undergraduates? We can barely get them out in four years knowing real analysis and abstract algebra. The next stop would be the basic theory of manifolds, not higher topos theory. 3) I looked at Kock's book (the draft of the CUP book on his website). The definitions are more abstract than the ones I would give to undergrads, and consequently harder for them to understand. The appeal is not clear to me. 4) You don't have to change your foundations (meaning ZFC vs. type theory, etc.) to do higher category theory in a reasonable way. Again, go pick up Lurie's books. The exposition would not really be affected by whether you choose type theory or ZFC for a foundation. Let me know if you think there's a counterexample to this claim. (The exposition probably would be affected if you denied the law of excluded middle, for the worse; luckily Lurie doesn't do that.) 5) Foundations are sort of irrelevant here anyway. The point of ZFC is that you can forget about it when actually doing math. If you're thinking about foundations when reading Lurie's books, you're doing something wrong. (Consider: most mathematicians have zero opinion about foundational questions or concepts because they have no bearing on their day to day work.)

by enugu 5y ago

spekcular 5y ago

I don't have much to say here that I didn't already say above about the meta-mathematical issues. However, about object-level mathematical issues, you write: "It is a work in progress and might take some time before bearing substantive fruit, but note that the current alternative is that any student learning higher level mathematics at the level of Lurie's books has to go through a huge amount of foundational material while the ideas themselves may not be intrinsically complicated. Instead, this complexity is an artifact of embedding the theory in current foundations like the SDG example mentioned above." Higher category theory is not the same thing as homotopy type theory. One does not need to learn anything about the foundations of mathematics to read and understand Lurie's work. As far as I know, issues of ZFC vs type theory simply do not arise. You can just pick up Higher Topos Theory and start reading, assuming you have a strong background in algebraic topology. The linked article is only about higher category theory and making sure all of its claims are written down in a clear and rigorous fashion to be maximally useful to workers in the field. It has nothing to do with the foundations of mathematics as a whole.

enugu 5y ago
> One does not need to learn anything about the foundations of mathematics to read and understand Lurie's work. By foundations here, I didnt mean foundations of mathematics, rather the amount of material a student needs to read to become familiar with the basic definitions of what a space means. We can teach topology to undergrads, can we teach higher categorical notions of space? Even schemes themselves had a daunting reputation some time back, now we have derived stacks which involve infinite categories. > You can just pick up Higher Topos Theory and start reading Yes, but my point, as illustrated in SDG example, was that definitions can be easy or hard depending on which foundations you use. You havent mentioned whether you disagree with this and if you see Kock's book, I think you will agree. When dealing with higher categories, a foundations which uses '=' symbol in a different way, with an equivalence relation(modelled on homotopy equivalence) playing a much more prominent role could make the theory much more natural. Note, that I am not even emphasizing sets vs type theory here, but excluded middle and a good notion of equivalence(and equivalence between equivalences... like in homotopy theory) in the foundations. Maybe a lot of this debate will get dissolved if we just use two different words for 'examining consistency of axioms' and 'naturality of theory as encoded in a given system' instead of using the same word - foundations - for both of them. At the very least if discussions begin with an awareness of this distinct usage, there would be lot less talking past each other. Urs Schreiber makes the same point about naturality here - https://golem.ph.utexas.edu/category/2016/03/foundations_of_mathematics.html https://golem.ph.utexas.edu/category/2016/03/foundations_of_...
- spekcular 5y ago
  1) Yeah, Lurie's books are advanced tracts aimed at specialists in algebraic topology. Of course there are going to be substantial prerequisites. This is sort of inevitable if you want to understand the motivating applications. 2) Why would we ever want to teach higher categorical notions of space to undergraduates? We can barely get them out in four years knowing real analysis and abstract algebra. The next stop would be the basic theory of manifolds, not higher topos theory. 3) I looked at Kock's book (the draft of the CUP book on his website). The definitions are more abstract than the ones I would give to undergrads, and consequently harder for them to understand. The appeal is not clear to me. 4) You don't have to change your foundations (meaning ZFC vs. type theory, etc.) to do higher category theory in a reasonable way. Again, go pick up Lurie's books. The exposition would not really be affected by whether you choose type theory or ZFC for a foundation. Let me know if you think there's a counterexample to this claim. (The exposition probably would be affected if you denied the law of excluded middle, for the worse; luckily Lurie doesn't do that.) 5) Foundations are sort of irrelevant here anyway. The point of ZFC is that you can forget about it when actually doing math. If you're thinking about foundations when reading Lurie's books, you're doing something wrong. (Consider: most mathematicians have zero opinion about foundational questions or concepts because they have no bearing on their day to day work.)