[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?

[Smaug123]

It's not about the axioms, which are perfectly fine as set theory. It's about the encoding of geometry in set theory, for which there are many options, some with nicer properties than others. Cf the original link in the thread, https://twitter.com/andrejbauer/status/1428471658088738818, which argues that you should model locales rather than points (and I guess if your foundation is set theory then you should use set theory to model those locales, though it sounds rather painful to me, a layman).

[ncallaway]

Me? I have no idea. I was just trying to catch and diffuse what seemed like a miscommunication between two people.

Actually selecting and proposing an axiom set is way outside my knowledge-base. My limited understanding is that the Axiom of Choice, in ZFC leads to Banach-Tarski, and if it’s removed Tarski doesn’t hold, but I don’t have nearly enough information to say if that’s worth exploring removing it.

[thaumasiotes]

The Axiom of Choice is one of the most controversial things in mathematics. There are many people who choose to work without it. I'll give a statement of it here:

The Cartesian product of non-empty sets is itself non-empty.

The Cartesian product of sets S_1, S_2, S_3, ... is of course the set of tuples (s_1, s_2, s_3, ...) such that s_1 ∈ S_1, s_2 ∈ S_2, s_3 ∈ S_3, ... . An element of the Cartesian product is a tuple with one element drawn from each of the sets being, um, Cartesianly multiplied.

Thus, the Cartesian product of the three sets {1, 4}, {a, b}, and {@, 2} is the set {(1,a,@), (1,a,2), (1,b,@), (1,b,2), (4,a,@), (4,a,2), (4,b,@), (4,b,2)}.

The Cartesian product of the three sets {1, 4}, {}, and {@, 2} is {}, the empty set, because no tuples exist such that the second element of the tuple belongs to the set {} (the second Cartesian factor).

So all the Axiom of Choice asserts is that, if all of the Cartesian factors are nonempty, then a tuple exists with one element drawn from each of the Cartesian factors. The only way for it to be impossible for such a tuple to exist is if one of the factors itself has no elements.

It's a theorem for finite Cartesian products, so all the dispute is over infinite products.

It's probably also worth mentioning that the C in ZFC stands for the Axiom of Choice, which is an indicator that people have explored not using it. ZFC without the Axiom of Choice is ZF.

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

[mjw1007]

I was taught that dropping the axiom of choice was enough to make Banach-Tarski go away. That seems considerably short of "there is no such thing as an infinite number".

But the Twitter link at the top of this thread seems to have a rather more interesting way of doing so.

[thaumasiotes]

> I was taught that dropping the axiom of choice was enough to make Banach-Tarski go away. That seems considerably short of "there is no such thing as an infinite number".

The Banach-Tarski theorem is not the only theorem out there that bothers some people. Anything to do with infinities gets a large number of outraged rejections.

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