[Ericson2314]

I highly recommend 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.

[mjw1007]

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]

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.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]

> 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.

[throwaway81523]

Imho, software people should study foundations (particularly proof theory) much more than they do. That is how you ensure correct code, after all. The people deeply involved in software verification are basically logicians. Also, the test suite for the HOL Light proof assistant (used in software verification) uses a large cardinal axiom, sort of. It uses a version of itself with the large cardinal added, to prove the consistency of the normal version without the large cardinal. Neither version can prove itself consistent, because of Gödel's theorem, but the one with the large cardinal can prove the consistency of the one without it.

One can say that if either is inconsistent then they can prove everything, but that makes it even sharper: the large cardinal is used purely to give engineering assurance of software correctness and not real mathematical rigor. So it's a pure engineering use of one of the most "out there" mathematical objects. It doesn't seem worse than using IEEE floating point arithmetic to design airplanes....

[Ericson2314]

> 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").

That sounds nice, but breaks down when one thinks harder. Music is a little bit physical phenomena, a little more biological phenomena, and even more cultural phenomina. That's many layers at once, and theory has to conform to the evidence.

Math, is not science. This is no evidence external to reasoning. Different foundations / formal systems conclude different things.

At best, we can look at what matches existing working mathematicians mental heuristics and.....that's not ZFC, which admits all sorts of crap because it is untyped.

> On the contrary, ZFC has been a tremendous success in that most mathematicians don't need to worry about it at all.

That is how most mathematicians see it, but us in the type theory crowd see that as bad goalposts necessitated by the fact that ZFC is so clunky to work with --- of course one wants to declare mission accomplished and move on to other things as quickly as possible with a foundation like that.

Check out https://xenaproject.wordpress.com/ for a less heterodox approach, that nevertheless does use a type theoretical "user interface" and "kernel" (trusted foundation) for purely practical reasons. Basically, the idea is making making formalized mathematics not a huge burden necessitates a more ergonomic system than was needed 80 years ago without computers.

[thaumasiotes]

> 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 follow. You can view the Intermediate Value Theorem as something that motivates the definition of "continuous function", so that once you have the definition it had better conform to the theorem, sure.

But the Banach-Tarski theorem isn't like that. It's just a cool result of some other things that work well. It's not motivating anything or being motivated by anything.

[mjw1007]

What I mean is: if you imagine someone drawing up a requirements document for the team assigned to the task of axiomatising geometry, and somebody asked "Do we want our model of geometry to support cutting up a ball into five pieces, moving the pieces rigidly, and reassembling them into two copies?", I think their first idea would be to answer "no".

So it isn't parallel to the intermediate value theorem, but opposite to it.

[pfortuny]

The thingis exactly that in the B-T paradox you are NOT “cutting”, you are “choosing” non-measurable subsets and reorganizing them. Thus, the operation of “cutting” is not taking place (there is no continuous function whose zeros gives you any of the subsets).

[thaumasiotes]

The whole idea of a proof system is that there are some things you can't have without also having other things. The Banach-Tarski theorem is a consequence of things we want. You don't get to pick and choose everything at once.

[ncallaway]

> The Banach-Tarski theorem is a consequence of things we want

Is it? I think the parent comment is saying: “maybe we shouldn’t want things that result in Banach-Tarski”

Maybe it’s a hint that the underlying axioms we’ve selected aren’t exactly what we want.

You’re right that we can’t pick and choose the results of our axioms, but we do explicitly get to pick and choose the axioms we start with. If we choose bad axioms, we get nonsensical results.

In general, it seems like we’ve picked _pretty good_ axioms that mostly give us sensible and useful results. But maybe this result that seems somewhat… odd, is an indication that those axioms have an odd corner somewhere.

[bigbillheck]

> Is it? I think the parent comment is saying: “maybe we shouldn’t want things that result in Banach-Tarski”

OK, which axiom do you want to replace?

[thaumasiotes]

> But maybe this result that seems somewhat… odd, is an indication that those axioms have an odd corner somewhere.

The only way you're going to avoid getting results like this is with axioms like "there is no such thing as an infinite number". At that point, the real line doesn't exist (too many points) and it becomes impossible to duplicate spheres by dividing them at a level of fineness that also doesn't exist.

But that's not a productive approach to anything.

[Ericson2314]

Did you read the original link? We don't want to use topological spaces, we want to use locales! We can get rid of the paradox while sacrificing very little.

[throwaway81523]

The Banach-Tarski theorem motivated the idea of amenable groups in topological group theory. Understanding exactly what that means is on my todo list, but I think the basic idea is that a given space can have additive measures invariant under some transformation groups but not others. Particularly, the Banach-Tarski paradox shows that regular old 3-dimensional Euclidean space doesn't have an additive measure invariant under rotation and translation. On the other hand, 2-dimensional Euclidean space does have it.

[Ericson2314]

Banach-Tarski is quite arguably a red flag that all these non-measursble, non-open sets are barking up the wrong tree.

[boxfire]

> 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)

[creata]

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_Y...

[1]: http://math.andrej.com/2016/10/10/five-stages-of-accepting-c...

[Ericson2314]

Andreij Bauer is one of those HoTT people, so this is quite tongue-in-cheek.

[mjw1007]

For the avoidance of doubt: Andrej Bauer is himself very much one of those crazy HoTT people.