What would be the consequence of requiring that any choice function be computable; i.e. using as the foundational basis ZF + ACC? Does it make a difference if we admit definable functions?
I guess I am sometimes bothered by the thought that any random choice over an uncountable set by definition would seem to almost certainly return a non-computable member. This seems impractical and perhaps even problematic, considering that major branches of mathematics such as for example analysis, with only few notable exceptions, mainly operate within the computable or definable realm.
Presumably an immediate consequence would be that the Banach–Tarski paradox and similar theorems related to unmeasurable sets would fail. But would there be more fundamental consequences?
Best Answer
The Axiom of Choice is a principle that applies to arbitrary families of arbitrary sets, and this is a realm where the concept of recusive functions or Turing Turing computability simply does not apply. For example, mathematicians may use AC to select elements of subsets of a (possibly uncountable dimension) vector space in order to form a basis---you iteratively pick a vector outside the span of what you have so far---and it simply doesn't make sense in this generality for such a function to be recursive or equivalent to a recursive function. This is why people were objecting to your question in the comments.
But let me try to make some sense of the question. Suppose we restrict our choice principle to families of sets that each have at least one computable member. Then, I claim that there is a definable choice function, for we may select from each set in the family the computable member that is computed by the smallest program. Thus, this formulation of what you might mean by ACC is simply provable in ZF. But this function will not in general be itself computable (it merely selects computable members, and this is not the same), and indeed, since the domain of the function is not necessarily $N$, the concept of this function being computable isn't always sensible.
If you intend to have a version of ACC that only applies to countably-indexed families $\langle A_n| n\in N\rangle$, with each $A_n$ a set containing subsets of $N$, at least one of which is computable, then it is provable in ZF that we cannot insist there is always a computable function $f$ such that $f(n)$ is a program computing a member of $A_n$. The reason is that there are only countably many such functions $f$, and we may easily diagonalize against them to produce a bad sequence $\langle A_n | n\in N\rangle$.
If you replace computable with definable, then your principle has a much better chance. One subtle issue, however, is that "being definable" is not first order expressible in set theory, so you cannot state your ACC principle that way. Rather, one can use "ordinal-definable", which is expressible. The principle that every set contains an ordinal-definable element is equivalent (by a previous MO question) to the set-theoretic principle $V=HOD$. And this principle implies AC, in the form that under V=HOD, every family of nonempty sets admits an ordinal definable choice function.
One can also impose more restrictive versisons of definability on the choice functions or on the families. For example, perhaps one wants principles that only apply to sets of reals, and one wants to know when there are, say, projective choice functions. This phenomenon is called uniformization, and is extensively studied in descriptive set theory.
So there are a variety of ways to make sense of your question, and these different interpretations give different answers. So it all depends on what you mean.