The Banach-Tarski paradox states that for a solid ball in 3‑dimensional space, there exists a decomposition into a finite number of disjoint subsets, which can then be put back together in a different way to yield two identical copies of the original one.
Obviously it is based on AC. I was wondering if anyone here knew if analysis under the axioms of ZF has been developed to invent a version of Banach-Tarski which is independent of AC. What does the Banach-Tarski paradox look like without AC? Are there any versions of it? (For an example, one of the theorems that has been proven without AC is the Heine-Borel theorem.)