10
$\begingroup$

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?

  • 2
    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.2012-07-27

1 Answers 1

12

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.
  • 0
    So it really seems that when we switch to constructive theory, it actually does something even better, it eliminates this pathology altogether, making balls behave more sensibly?2017-03-16