Also, as someone pointed out in the linked thread, you're completely glossing over the theory of measurable sets.
Let me try to make the analogy more explicit.
The interesting thing about the fifth postulate is that we show we can't prove it from the other axioms because there are models where the first four hold and the fifth doesn't.
The interesting thing about the Banach-Tarski Theorem is that it shows we can't have all four desirable properties of a metric because there are constructions that show they they can't all hold at once.
> ... you're completely glossing over the theory of measurable sets.
I'm not glossing over it, I'm showing why it is necessary and important.
The Banach-Tarski paradox shows that classical set theory makes the wrong assumptions to intrinsically model measure theory and probability.
There are other systems which don't suffer from this paradox and hence don't need all the machinery of sigma algebras and measurable sets.
I wish there was a good accessible book/article/blog post about this, but as is you'd have to Google point-free topology or topos of probability (there are several).
Is there a known set theory of the form ZF+(something) which relatively consistent with ZFC in which additive, isometry invariant measures exist?
I guess what you are saying is that the only known, reasonable way around this is the topos notion you mentioned.
They are as far apart from each other as possible, as similar as polar opposites.
Banach-Tarski is resolved by deciding that "the real numbers" aren't real, and nothing is lost except for dubious overly-simple proofs.
Problem is, there is a lot of mathematics that's widely used and which depends on the reals. Pretty much all of calculus, for example.
Discarding the reals is pretty ambitious.
With (non-)Euclidean geometry, you have a bunch of axioms and it turns out you don't have to accept the parallel postulate even if you accept all the others.
With measure theory, you have a bunch of things you'd like to be true and it turns out you can't accept all of them at once.
Those are quite different.
On the other hand, the analogy between geometry and, say, set theory is closer. There are a bunch of axioms for Euclidean geometry, the parallel postulate seems a bit dicey, and it turns out that you can accept the others and lose that one. There are a bunch of axioms for set theory, the axiom of choice seems a bit dicey, and it turns out that you can accept the others and lose that one.
From this perspective, the role of the Banach-Tarski paradox is to help show why the axiom of choice seems a bit dicey, maybe more so than the other commonly-adopted set-theoretic axioms.
(In set theory, too, there are situations where we can write down a bunch of axioms we would like to be true but that actually can't all be true at once, just like with measure theory. Russell's paradox is the best-known example, and it led set theorists to abandon the otherwise very attractive axiom of "unrestricted comprehension".)
The pun was intended, by the way.