Is there any version of the Banach-Tarski paradox in ZF?

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

• Depends on what you mean exactly. There are models of ZF in which every set of real numbers is measurable (en.wikipedia.org/wiki/Solovay_model), which would prevent a lot of the paradoxes you might have in mind. This question is probably too basic for MO, though. Aug 20, 2021 at 14:18
• To add on to what @Sam wrote; many theorems in analysis either don't use choice, or their specific uses in classical analysis don't use choice (e.g. Baire Category Theorem is equivalent to Dependent Choice; but for separable spaces it is provable in ZF). Asking about development of the whole of analysis in ZF or ZF+DC is tantamount to going through Rudin (or some other book on analysis) and checking each theorem to see what you can or cannot do wit or without choice. Some places do that, to some extent (e.g. Schechter's book), but generally it's too broad of a question for a Q&A website. Aug 20, 2021 at 15:23
• "which is independent of AC": I guess you mean "which is a theorem of ZF". The formulation that P is independent of AC might (?) mean that both ZFC+P and ZFC+(not P) are consistent.
– YCor
Aug 20, 2021 at 17:45
• In light of the very nice answer of Paul, I retract my insinuation that this question might be too basic. But I will leave the link to the Solovay model, which is still certainly relevant for some considerations... Aug 20, 2021 at 22:03
• The fact that there is no finitely-additive SO(3)-invariant measure on S2 with the discrete σ-algebra has been proven in ZF + Hahn-Banach by Foreman and Wehrung: hal.archives-ouvertes.fr/hal-00004713 Their argument transports the lack of invariant measure from F2 to S2. It can then be used to transport F2's explicit paradoxical decomposition across: matwbn.icm.edu.pl/ksiazki/fm/fm138/fm13813.pdf Aug 21, 2021 at 2:11

• Reading again, I think Feferman was right and it really is constructive, but a more careful eye is needed than mine. Some versions of constructivism have multiple not-provably-isomorphic versions of $\mathbb{R}$, so the question may be subtle. Aug 20, 2021 at 21:36