What is the reverse mathematical strength of the Banach-Tarski paradox?
The usual proof of Banach-Tarski should carry out in $\mathrm{ZF}+\mathrm{AC}_\kappa$, where $\kappa$ is the supremum of the sizes of partitions of $\mathbb R$, and $\mathrm{AC}_\kappa$ is choice for families of sets of size $\kappa$. However I am mainly focusing on replacing $\textrm{ZF}$ here with a weaker theory.
All machinery appearing in the proof seems to have low rank in the von Neumann hierarchy, so the axiom of powerset does not seem to have to be iterated many times. (In contrast it is a result of Friedman that Borel determinacy requires $\omega_1$-fold iteration of powerset applies to $\mathbb N$ in order to prove, although its statement only refers to sets of low rank. Yet all machinery used in proving Banach-Tarski seems to have low rank.) For example, if $\mathcal P(\mathbb N)$ is identified with the reals, the unit ball will be a subset of $\mathcal P(\mathcal P(N))$, a finite set of pieces of the unit ball will be codable as a member of $\mathcal P(\mathcal P(\mathcal N))$ using a coding function $[\mathcal P(\mathcal P(\mathcal N))]^{<\aleph_0}\to \mathcal P(\mathcal P(\mathcal N))$ (where $[\mathcal P(\mathcal P(\mathcal N))]^{<\aleph_0}$ is the set of finite subsets of $\mathcal P(\mathcal P(\mathcal N))$), and a quotient of the unit ball will be identified with $\mathcal P(\mathcal P(\mathcal P(\mathbb N)))$.
Some results are known about theories being sufficient or not sufficient to prove Banach-Tarski, although most are about choice rather than replacing the $\mathrm{ZF}$ part of the theory:
- It is known that the Hahn-Banach theorem implies the Banach-Tarski paradox. (Pawlikowski, "The Hahn-Banach theorem implies the Banach-Tarski Paradox", 1989), proven with base theory $\mathrm{ZF}$.
- It is known that Banach-Tarski is implied by the statement "every partial preorder extends to a linear preorder that preserves strict order" (MO question #150945), but this is proven with base theory $\mathrm{ZF}$.
- Banach-Tarski is number HR 309 in Howard and Rubin's book Consequences of the Axiom of Choice. There is an MO question "Equivalence of the Banach–Tarski paradox" relevant to this result.
- Banach-Tarski is known to not be provable in $\mathrm{ZF}+\mathrm{DC}$ if it is consistent, where $\mathrm{DC}$ is the axiom of dependent choice. (Corollary 13.3 of Wagon, The Banach-Tarski Paradox, 1993)