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?

-
I comment just to clarify that it is known to be true with the use of AC, but without AC then it is not necessarily false -- just impossible to know. – Chris Gerig Jul 27 '12 at 0:25
do you have a reference for " traditional accounts of constructive logic do not contain choice"? ps: in constructive mathematics objects are typically well-behaved, classical non-well-behaving objects like non-continuous functions simply do not exist. For example, if I was to guess the answer, I would say that the paradox does not arise probably because those classical non-measurable sets do not exist in constructive mathematics, and a choice axiom (may depend on what one exactly means by it) probably doesn't have an effect on it. – Kaveh Jul 27 '12 at 0:56

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.
Actually, the Vitali case is not simpler, this is exactly how Banach-Tarski use the Axiom of Choice. Instead of the group $\mathbb{Q}$ acting on $\mathbb{R}$ by translation, we have a free group $F$ generated by two rotations which acts on the unit sphere $S_2$ and we must pick one representative from each orbit (i.e. equivalence class). As in the Vitali case, each orbit is dense in $S_2$ so (a very significant fragment of) the Law of Excluded Middle is required to separate the points of $S_2$ into mutually disjoint orbits. – François G. Dorais Jul 27 '12 at 4:08