Skip to main content
1 of 2
Joel David Hamkins
  • 236.2k
  • 44
  • 777
  • 1.4k

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 restrrictive 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.

Joel David Hamkins
  • 236.2k
  • 44
  • 777
  • 1.4k