Intuitionistic Banach-Tarski Paradox
While the Banach-Tarski paradox is a counter-intuitive result which requires the Axiom of Choice, leading some people to argue specifically against Choice, and others to argue for constructive mathematics, as the use of Choice is the only non-constructive step in the proof, and traditional accounts of constructive logic do not contain choice.
However, newer frameworks of constructive logic such as intensional type theory (ITT) do admit Choice as a rather trivial theorem. Does this mean that the Banach Tarski theorem is also a theorem of ITT?
As Kaveh says in a comment, the issue is not going to be choice. Usually, when we examine what goes wrong when we try to formalize a "nonconstructive" classical proof in a constructive system, the problem that we discover is that the proof is already nonconstructive before the axiom of choice is invoked.
In this case, the issue is that the entire concept of partitions and equivalence classes, which underlies the usual proof of the Banach-Tarski paradox, behaves very differently in constructive systems.
Consider the simpler case of a Vitali set in the real line. Two reals are defined to be equivalent if their difference is rational. That is a perfectly good definition in constructive systems, but it is easy to miss the fact that it involves an implicit universal quantifier over the rationals (or the ability to tell whether an arbitrary real is rational). In this particular case, standard methods show that it will not be possible to prove constructively[1] that "for all reals $x$ and $y$, either $x$ is equivalent to $y$ or $x$ is not equivalent to $y$". Thus it is no longer possible to prove that two equivalence classes $[x]$ and $[y]$ are disjoint or identical, that is, impossible to prove that the equivalence classes form a partition of the real line. But that fact is crucial for the usual proof that the Vitali set is nonmeasurable. The same sort of problem is easy to spot in the usual proof of the Banach-Tarski paradox.
- More precisely, this will be impossible in any of the usual formalized systems for constructive mathematics, including intuitionistic type theory.