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

[ncallaway]

This is a great overview and explanation of the Axiom of Choice! I was familiar with the basics of it, but this really did a good job clarifying it for me, so thanks for that.

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