3 ms·

Isn't Vladimir Voevodsky's [1] Univalent Foundations [2] / Homotopy Type Theory [3] a new candidate challenging to subsume set theory as the foundations of math

by espeed 9y ago

Isn't Vladimir Voevodsky's [1] Univalent Foundations [2] / Homotopy Type Theory [3] a new candidate challenging to subsume set theory as the foundations of mathematics [4]? [1] https://en.wikipedia.org/wiki/Vladimir_Voevodsky https://en.wikipedia.org/wiki/Vladimir_Voevodsky [2] https://en.wikipedia.org/wiki/Univalent_foundations https://en.wikipedia.org/wiki/Univalent_foundations [3] https://homotopytypetheory.org/ https://homotopytypetheory.org/ [4] https://www.youtube.com/results?search_query=Vladimir+Voevodsky+univalence+foundation+of+mathematics https://www.youtube.com/results?search_query=Vladimir+Voevod...

kryptiskt 9y ago
I wish people called these things "a foundation of mathematics" rather than "the foundation of mathematics". We have been able to pick and choose ever since foundations became a thing, and as long as they yield worthwhile results they're worthy objects of study. We don't have to pick one and stick with it, and it would be silly to classify stuff done with other axioms as non-mathematics.
- ellius 9y ago
  I don’t disagree with you, but I think the human mind is essentially programmed to seek first causes. Part of what has made us so successful as a species is that we want to chase patterns down to their foundations, and I think it’s natural to feel that there is some “root” truth that explains the entirety of existence. I think that’s why a lot of people turn to simplistic unifying philosophies; it reduces a lot of intellectual anxiety if you have one big idea that subsumes all others, and upon which you can fall back when faced with uncomfortable questions. All of which is a long way of saying that while you’re correct, I think as a species we’ll always trend towards trying to find “THE foundation” even when the more rational thing is to “pick and choose” like you’re suggesting.
  - bohadi 9y ago
    An interesting thought brought to mind by your comments, our search for foundations (whether set theory, type theory, category theory, or higher order) reveals as much about our own minds as it does any idea of some external nature.
  - broadwaylamb 9y ago
    I think the issue here is that if mathematics is talking about anything at all, then the search for the first cause tells us what that thing is. This is a philosophical issue separate from the sociological activity of doing mathematics. The latter doesn't need an all-encompassing foundation to continue to do useful and interesting mathematics, so pragmatics shrug the issue off. On the other hand, even if mathematics is purely about "structure", then we should still be able to organize our knowledge in a way that provides a single foundation (even if that means showing that the different formulations are logically equivalent).
    - jessaustin 9y ago
      One suspects that if the search for "foundations" were made rigorous enough to analyze in any meaningful way, someone like Gödel would come along with some sort of impossibility theorem. In other words, if we were to really examine the idea that any particular foundation could be the best/most natural/simplest/whatever, we'd see that it is folly.
slack3r 9y ago
I wouldn't say it "challenges" set theory. For this to be the case there have to demonstrable advantages over working with set theory. The main attraction of HoTT is that it allows people to do homotopy theory on computers using theorem provers. It is still a very open question whether this is an improvement over pen and paper math. It's still not clear if HoTT is just some neat technical gimmick that allows one to model homotopy theory using type theory. This is still certainly worth investigating, but saying that HoTT "subsumes" set theory is a bit strong. I would refer the interested reader to the discussion at https://mathematicswithoutapologies.wordpress.com/2015/05/13/univalent-foundations-no-comment/ https://mathematicswithoutapologies.wordpress.com/2015/05/13... (between Jacob Lurie, Shulman and Voevodsky).
adamnemecek 9y ago
It is but it’s still too new.

by espeed 9y ago

kryptiskt 9y ago

I wish people called these things "a foundation of mathematics" rather than "the foundation of mathematics". We have been able to pick and choose ever since foundations became a thing, and as long as they yield worthwhile results they're worthy objects of study. We don't have to pick one and stick with it, and it would be silly to classify stuff done with other axioms as non-mathematics.

ellius 9y ago
I don’t disagree with you, but I think the human mind is essentially programmed to seek first causes. Part of what has made us so successful as a species is that we want to chase patterns down to their foundations, and I think it’s natural to feel that there is some “root” truth that explains the entirety of existence. I think that’s why a lot of people turn to simplistic unifying philosophies; it reduces a lot of intellectual anxiety if you have one big idea that subsumes all others, and upon which you can fall back when faced with uncomfortable questions. All of which is a long way of saying that while you’re correct, I think as a species we’ll always trend towards trying to find “THE foundation” even when the more rational thing is to “pick and choose” like you’re suggesting.
- bohadi 9y ago
  An interesting thought brought to mind by your comments, our search for foundations (whether set theory, type theory, category theory, or higher order) reveals as much about our own minds as it does any idea of some external nature.
- broadwaylamb 9y ago
  I think the issue here is that if mathematics is talking about anything at all, then the search for the first cause tells us what that thing is. This is a philosophical issue separate from the sociological activity of doing mathematics. The latter doesn't need an all-encompassing foundation to continue to do useful and interesting mathematics, so pragmatics shrug the issue off. On the other hand, even if mathematics is purely about "structure", then we should still be able to organize our knowledge in a way that provides a single foundation (even if that means showing that the different formulations are logically equivalent).
  - jessaustin 9y ago
    One suspects that if the search for "foundations" were made rigorous enough to analyze in any meaningful way, someone like Gödel would come along with some sort of impossibility theorem. In other words, if we were to really examine the idea that any particular foundation could be the best/most natural/simplest/whatever, we'd see that it is folly.

slack3r 9y ago

I wouldn't say it "challenges" set theory. For this to be the case there have to demonstrable advantages over working with set theory. The main attraction of HoTT is that it allows people to do homotopy theory on computers using theorem provers. It is still a very open question whether this is an improvement over pen and paper math. It's still not clear if HoTT is just some neat technical gimmick that allows one to model homotopy theory using type theory. This is still certainly worth investigating, but saying that HoTT "subsumes" set theory is a bit strong. I would refer the interested reader to the discussion at https://mathematicswithoutapologies.wordpress.com/2015/05/13/univalent-foundations-no-comment/ https://mathematicswithoutapologies.wordpress.com/2015/05/13... (between Jacob Lurie, Shulman and Voevodsky).

adamnemecek 9y ago

It is but it’s still too new.