Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?

share|cite|improve this question
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
up vote 11 down vote accepted

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.

  1. More precisely, this will be impossible in any of the usual formalized systems for constructive mathematics, including intuitionistic type theory.
share|cite|improve this answer
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

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.