We shall use the axiom of choice to prove an extremely wimpy version of the Banach Tarski paradox, to wit:
Define an equivalence relation on the interval [0,1] by the following:
x ~ y if and only if x-y is a rational number. This breaks the unit interval
into an uncountable number of equivalence classes, each of which is countable.
Use the axiom of choice to find a subset X of [0,1] which contains exactly
one element of each equivalence class. (Intuitively speaking, we are taking each
equivalence class in turn and picking one element from each, and throwing it into the
set X). This set is what logicians call "non-constructive"; there is no recipe
or formula for this set, because we can't specify exactly how we pick an element from
each equivalence class. All we know is that such a set exists by this abstract axiom.
Since X does not contain two or more elements from any equivalence class, we see
that the translates X + q are all disjoint for all rational numbers q.
In particular, the translates X + q for all q \in Q \cap [0,1] form a disjoint
partition of some subset Y of [0,2]. You can think of Y as all the "small"
rational translations of X.
Now the sets Q \cap [0,1] and Q are both countably infinite, and so there is some
(constructive!) one-to-one correspondence q --> f(q) between them.
Now what we do is that we take our set Y, which is the union of translates X + q
of X, and shift each translate so that X+q shifts to X + f(q). If we do this,
we get the union of all the rational translations of X (not just the small ones).
But this set is all of R, since every element of R is the member of some equivalence
class, and is therefore in some rational translate of X, since X contains one element
from each equivalence class. This proves the theorem.