[BreakfastB0b]

Banach–Tarski relies upon the Axiom of Choice / Law of the Excluded Middle. Zermelo–Fraenkel set theory is independent of the Axiom of Choice and there's an entire field of Mathematics called Constructivist Mathematics which avoids including the Axiom of Choice / Law of the Excluded Middle.

I had a hard time grasping why the Axiom of Choice / Law of the Excluded Middle was so problematic until I heard it translated into a Computer Science context.

The Law of The Excluded Middle sounds very reasonable at first. For all propositions P, P ∨ ¬P. i.e. Every proposition is either true or false. Sounds fine right? But when viewed in the context of computer science via the Curry-Howard Isomorphism. A proposition is actually a program, and deciding the truth value of a proposition involves "running" that program. So The Law of the Excluded Middle is actually the Halting Problem! It's really saying that all possible programs terminate and yield true or false, but we know that some programs don't terminate, some propositions aren't true or false, but undecidable.

So circling back around to the Banach-Tarski paradox. I would be very skeptical of any paradoxes resulting from assuming the halting problem doesn't exist!