The funny things is that the same result for an orbit on a sphere doesn't need the Axiom Of Choice at all. It just uses the concept of actual infinity.
I had to read this several times before I understood what you were saying. But you are right. The point is that you can get what wikipedia calls a paradoxical decomposition of a groups of rotations, and that doesn't require choice. Converting that into a proof of B-T requires taking a member of each equivalence class, and that does require choice.
The point about the orbit on a sphere not needing AC is really step 1 of the proof there, except using rotations on a sphere as the "location" of the free group.
As a side issue, B-T is proof that there isn't a finitely additive, isometry-invariant measure on R^3 that's defined for all subsets. Interestingly, there is such a measure on R^2, although it's now 26 years since I proved it.
I had to read this several times before I understood what you were saying. But you are right. The point is that you can get what wikipedia calls a paradoxical decomposition of a groups of rotations, and that doesn't require choice. Converting that into a proof of B-T requires taking a member of each equivalence class, and that does require choice.
The proof on WikiPedia is pretty good, actually:
http://en.wikipedia.org/wiki/Banach-Tarski_paradox#A_sketch_...
The point about the orbit on a sphere not needing AC is really step 1 of the proof there, except using rotations on a sphere as the "location" of the free group.
As a side issue, B-T is proof that there isn't a finitely additive, isometry-invariant measure on R^3 that's defined for all subsets. Interestingly, there is such a measure on R^2, although it's now 26 years since I proved it.