Are any of the counterintuitive functions whose existence is postulated by the axiom of choice computable?

Question

Mathematicians often consider a collection of sets and need to select one element from each one. Usually there is a simple constructive way to do so, and everything works out fairly intuitively. As I understand it, it's only when there isn't such a natural choice function that we need to break out the big gun of the axiom of choice. That's why results that depend on the axiom of choice tend to be so unintuitive - if you need to use the axiom of choice, then you're necessarily considering a "weird" situation where there isn't any natural structure, and so your choice function will almost necessarily be very strange and difficult to describe (for example, wildly discontinuous, in contexts where that notion makes sense).

Are these choice functions that require the axiom of choice ever computable? If not, then that sort of sweeps all the paradoxes under the rug, because if you're (say) a practical-minded computer scientist who only cares about computable functions, then you can just ignore all the weird results that require the axiom of choice because they're just abstract existence results of algorithms that could never be carried out in practice.

To make my question concrete: there are several results about the possibility of partitioning simple shapes in Euclidean space into a small number of subsets with strange properties - for example, the Hausdorff, Banach-Tarski, and Von Neumann paradoxes. Are these partitions computable? For example, for the Banach-Tarski paradox the partition takes the form of a function $B \to \{1, 2, 3, 4, 5\}$, where $B$ is the unit $3$-ball. Composing this function with spherical coordinates, we can convert this partition to a function $[0,1]\times[0,\pi]\times[0,2\pi]\to\{1, 2, 3, 4, 5\}$ (which respects the usual spherical coordinate identifications). Is this function computable? I suspect that the function depends so sensitively on its argument as to be uncomputable. Is this correct? Are the functions even definable?

Answer 1

It is almost always the case, when it makes sense, that "computable implies continuous" - for example, in the linked definition a computable function must be effectively uniformly continuous, hence continuous. So in this specific case, and more generally, we get an immediate answer to your question just by showing that pathological objects can't be continuous.

Note that this means that checking whether two reals are equal isn't computable! When doing computability beyond the naturals, we have to be very very careful ... It isn't at all clear, for example, that there is a "right" definition of computability in a broader context - Church's thesis could be relatively unique to the naturals.

This idea can be further developed via descriptive set theory: we can make precise the intuition that "pathological" objects of the type relevant here are "hard to describe" in various ways. For example, all Borel sets are Lebesgue measurable, and so there can't be a Borel instance of the Banach-Tarski paradox; being Borel corresponds in a precise way to being definable in infinitary first-order logic, so we have a very nice sense in which "the Banach-Tarski paradox can't be done definably."

And meanwhile descriptive set theory can also be used to gauge the complexity of tasks which can be accomplished in a reasonably non-pathological way - see e.g. here. It's also worth noting that there is a deep connection between computability and descriptive set theory, going in both directions (see e.g. the proof of the Harrington-Kechris-Louveau theorem).

Interestingly, these descriptive-set-theoretic bounds can be substantially strengthened in the presence of large cardinals. With strong large cardinal hypotheses, we can rule out pathologies in extremely broad classes of sets, so broad that it boggles the mind (well, mine anyways) to consider anything beyond them "computable" at all.

Answer 2

If you're a "practically-minded computer scientist", then I doubt you're really interested in the concept of computability in the reals. What you would be practically interested in would just be statements about ordinary finite computations, probably quantified.

Does this computation always terminate? Will this and that computation always give the same result? Given arbitrary finite input strings $w$ and $v$ is there always an $x$ such that for every $y$, the computation $P(w,v,x,y)$ will terminate and print "yes"?

In the formalism preferred by mathematical logicians, all of those interesting questions can be formalized as first-order aritmetical statements, where "aritmetical" refers to arithmetic on natural numbers, and quantification over natural numbers.

The undersigned philosophically-minded computer scientists tends to think that those are ultimately the only kind of mathematical statements that we have a good reason to think are inherently either true or false.

And as soon as we have restricted the ultimately interesting statements to arithmetical ones, all uncertainty about the axiom of choice drops away. Namely, it can be proven (using advanced techniques from logic and set theory) that every arithmetical statement that can be proved in ZFC can also be proved in ZF without the axiom of choice.

In this view the axiom of choice is harmless because among statements that actually matter to us, it doesn't make more statements provable -- it just makes already provable statements less unwieldy to prove.

In particular, something like the existence of a Banach-Tarski decomposition is not an arithmetical statements, so we (or, well, I) don't really care whether it is provable or not.