5 ms·

I highly recommend https://twitter.com/andrejbauer/status/1428471658088738818 https://twitter.com/andrejbauer/status/1428471658088738818 and follow ups. Yes, t

I highly recommend https://twitter.com/andrejbauer/status/1428471658088738818 https://twitter.com/andrejbauer/status/1428471658088738818 and follow ups. Yes, this stuff is fishy, and yes we can blame ZFC which is a bad formalization in comparison to what we've developed since. But the real scandal is why does our definition of geometry "leak" the underlying set theory it's built atop so much? Surely it's bad to have such a leaky abstraction in pure math! The series goes on to show that by abandoning "points" — which pull all the funny set theory stuff into geometry/topology/whatever is the topic at hand, one can still have a classical foundation — e.g. with the axiom of choice and law of excluded middle — that makes mathematicians feel at ease, but also purge this Banach–Tarski gobbledygook.

boxfire 5y ago
> But who's going to work without AC (other than crazy HoTT people)? Yeah... Those crazy HoTT people, trying to actualize the goal of putting mathematics on an actually firm foundation and removing the rest of the gobblygook handwaved into the religion of math as opposed to the pure logic it represents... Also you can use HoTT WITH AC / law of excluded middle... It's just not there by default and there are some really nice things you get without it, so it's pretty much only the lazy crutch of mathematics since forever. If you see proof via excluded middle, consider it a code smell (and recall by the Curry-Howard correspondence the proof is essentially code)
- Ericson2314 5y ago
  Andreij Bauer is one of those HoTT people, so this is quite tongue-in-cheek.
- creata 5y ago
  You're exaggerating the significance of HoTT. Mathematics is already on a pretty firm foundation. And I somehow doubt Bauer meant any ill intent with that line...[0][1] [0]: https://en.wikipedia.org/wiki/Homotopy_type_theory#Special_Year_on_Univalent_Foundations_of_Mathematics https://en.wikipedia.org/wiki/Homotopy_type_theory#Special_Y... [1]: http://math.andrej.com/2016/10/10/five-stages-of-accepting-constructive-mathematics/ http://math.andrej.com/2016/10/10/five-stages-of-accepting-c...
- mjw1007 5y ago
  For the avoidance of doubt: Andrej Bauer is himself very much one of those crazy HoTT people.
- deleted 5y ago
  [deleted]
mjw1007 5y ago
I remember sitting in maths lectures and wishing that when they did thing like prove the intermediate value theorem they'd make it clearer that what was going on wasn't so much "We're rigorously proving that this thing that seems obvious is true" as "We're checking that the formalisation we introduced earlier is fit for purpose". I think things like the Banach-Tarski theorem are the other side of that coin: they're showing some of the places where the formalisation we're starting with isn't a great fit for some things we might hope to use it for. I don't think I'd go as far as to say that makes the formalisation outright bad, but looking at alternate systems which don't admit Banach-Tarski-like results is surely a worthwhile way of spending time.
- Ericson2314 5y ago
  Ultimately this crowd wants to change the practice of mathematics in the real world, so they are very accomiadating. See https://golem.ph.utexas.edu/category/2021/06/large_sets_1.html https://golem.ph.utexas.edu/category/2021/06/large_sets_1.ht... for tackling the "large cardinal pissing contest" that is much of modern set theory. Your very statement is a good retreat from platonism with blinders, acknowledging the inherit "moral relativism" that there are many possible foundations, and it is up to usflawed humans to decide what we like to work with best. The earlier intuitionists like Brouwer were polemicists, perhaps because they felt very alone. Now there is a good network of CS-mathematician hybrids to keep everyone feeling more sane. Here we see the dual track that you can question your foundational choices and your higher level abstractions (point-set topology vs locales which are distilled to being purely order-theoretic) concurrently. It's nice to take the same skepticism and interest in finding definitions the work with not alienste the working mathematician at multiple levels. Because, for all the trepidation about abandoning ZFC, the mainstream formalizations have clearly failed in that mathematicians that aren't logicians or set theorists would rather engage with them as little as possible.
  - bigbillheck 5y ago
    > Ultimately this crowd wants to change the practice of mathematics in the real world, so they are very accomiadating PhD mathematician in industry here. The way I see it, foundations is to the rest of mathematics the way music theory is to music: it needs to be a describer, not a prescriber. (If I were less charitable I'd have said "ornithology is to birds"). > the mainstream formalizations have clearly failed in that mathematicians that aren't logicians or set theorists would rather engage with them as little as possible On the contrary, ZFC has been a tremendous success in that most mathematicians don't need to worry about it at all.

boxfire 5y ago

> But who's going to work without AC (other than crazy HoTT people)? Yeah... Those crazy HoTT people, trying to actualize the goal of putting mathematics on an actually firm foundation and removing the rest of the gobblygook handwaved into the religion of math as opposed to the pure logic it represents... Also you can use HoTT WITH AC / law of excluded middle... It's just not there by default and there are some really nice things you get without it, so it's pretty much only the lazy crutch of mathematics since forever. If you see proof via excluded middle, consider it a code smell (and recall by the Curry-Howard correspondence the proof is essentially code)

Ericson2314 5y ago
Andreij Bauer is one of those HoTT people, so this is quite tongue-in-cheek.
creata 5y ago
You're exaggerating the significance of HoTT. Mathematics is already on a pretty firm foundation. And I somehow doubt Bauer meant any ill intent with that line...[0][1] [0]: https://en.wikipedia.org/wiki/Homotopy_type_theory#Special_Year_on_Univalent_Foundations_of_Mathematics https://en.wikipedia.org/wiki/Homotopy_type_theory#Special_Y... [1]: http://math.andrej.com/2016/10/10/five-stages-of-accepting-constructive-mathematics/ http://math.andrej.com/2016/10/10/five-stages-of-accepting-c...
mjw1007 5y ago
For the avoidance of doubt: Andrej Bauer is himself very much one of those crazy HoTT people.
deleted 5y ago
[deleted]

mjw1007 5y ago

I remember sitting in maths lectures and wishing that when they did thing like prove the intermediate value theorem they'd make it clearer that what was going on wasn't so much "We're rigorously proving that this thing that seems obvious is true" as "We're checking that the formalisation we introduced earlier is fit for purpose". I think things like the Banach-Tarski theorem are the other side of that coin: they're showing some of the places where the formalisation we're starting with isn't a great fit for some things we might hope to use it for. I don't think I'd go as far as to say that makes the formalisation outright bad, but looking at alternate systems which don't admit Banach-Tarski-like results is surely a worthwhile way of spending time.

Ericson2314 5y ago
Ultimately this crowd wants to change the practice of mathematics in the real world, so they are very accomiadating. See https://golem.ph.utexas.edu/category/2021/06/large_sets_1.html https://golem.ph.utexas.edu/category/2021/06/large_sets_1.ht... for tackling the "large cardinal pissing contest" that is much of modern set theory. Your very statement is a good retreat from platonism with blinders, acknowledging the inherit "moral relativism" that there are many possible foundations, and it is up to usflawed humans to decide what we like to work with best. The earlier intuitionists like Brouwer were polemicists, perhaps because they felt very alone. Now there is a good network of CS-mathematician hybrids to keep everyone feeling more sane. Here we see the dual track that you can question your foundational choices and your higher level abstractions (point-set topology vs locales which are distilled to being purely order-theoretic) concurrently. It's nice to take the same skepticism and interest in finding definitions the work with not alienste the working mathematician at multiple levels. Because, for all the trepidation about abandoning ZFC, the mainstream formalizations have clearly failed in that mathematicians that aren't logicians or set theorists would rather engage with them as little as possible.
- bigbillheck 5y ago
  > Ultimately this crowd wants to change the practice of mathematics in the real world, so they are very accomiadating PhD mathematician in industry here. The way I see it, foundations is to the rest of mathematics the way music theory is to music: it needs to be a describer, not a prescriber. (If I were less charitable I'd have said "ornithology is to birds"). > the mainstream formalizations have clearly failed in that mathematicians that aren't logicians or set theorists would rather engage with them as little as possible On the contrary, ZFC has been a tremendous success in that most mathematicians don't need to worry about it at all.