undefined | Better HN

0 pointsthaumasiotes4y ago0 comments

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

0 comments

mjw10074y ago

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.

pfortuny4y ago

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

thaumasiotesOP4y ago

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.

ncallaway4y ago

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

2 more replies

Ericson23144y ago

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.

throwaway815234y ago

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.

Ericson23144y ago

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

j / k navigate · click thread line to collapse

0 pointsthaumasiotes4y ago0 comments

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.

0 comments

mjw10074y ago

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

pfortuny4y ago

thaumasiotesOP4y ago

ncallaway4y ago

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

2 more replies

Ericson23144y ago

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.

throwaway815234y ago

Ericson23144y ago

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

j / k navigate · click thread line to collapse