Axiom of Computable Choice versus Axiom of Choice

Question

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?

Answer 1

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.

Answer 2

As others have observed before, you cannot simply say "computable" and "ZF" in the same sentence without explaining what you mean. But I can tell you what your options are.

In order to speak about computability you have to provide some sort of an axiomatization or a model of computability. ZF is not such a model, but there are many others. Let us look at some of them and what happens to the axiom of choice. In what follows I mean by "computable model" a model of set theory or type theory in which all (global) maps are computable in some sense. In particular, choice functions happen to be computable in such models, so far as they exist.

Intuitionistic set theory IZF is an intuitionistic variant of set theory. It has many different models, some of which are computable. In IZF we can prove that the axiom of choice implies the law of excluded middle, so this kind of destroys the I in IZF. But restricted forms of choice are ok, notably countable and dependent choice are fine (in the sense that they are consistent with IZF and are validated by various computable models of IZF).

Higher-order intuitionistic logic (internal language of a topos) is essentially the same as IZF with regards to choice.

Martin-Löf type theory is a formulation of constructive mathematics in which choice is valid, in fact it is easy to prove it. The caveat here is that the interpretation of logic is a bit unusual because a proposition is equated with the collection of its proofs (as opposed to with its extension).

Brouwerian intuitionism accepts some choice but not all. More precisely, it accepts countable choice and $AC_{1,0}$, which is choice for families indexed by the set $\mathbb{N}^\mathbb{N}$. There are computable models of Brouwerian intuitionism (certain kinds of realizability models).

Bishop-style constructive mathematics accepts countable and dependent choice but not more. It has many computable and classical models because it is agnostic with respect to the law of excluded middle.

Russian constructivsm is another form of constructivism which accepts countable and dependent choice, but not more. The effective topos is a model.

Realizability toposes provide a rich class of models of computability. In fact, they are so general that the topos of (classical) sets is a special case. I should also point out that realizability toposes are larger than classical sets because they contain the category of sets as a subtopos of sheaves (for the double negation topology). Therefore, they provide the sort of setup that is needed to make sense of your question. In those realizbility toposes that are built from reasonable computational models, i.e., those that are based on the standard notion of Turing computability, choice is never generally valid. This is so because general choice implies the law of excluded middle (as mentioned above), and the law of excluded middle allows us to define the Halting oracle. Nevertheless, countable choice is always valid, which is one reason why various "schools of computability" accept it. In some realizability toposes you get more choice, but never a lot.

Let me make one last remark. There is a very general principle that "computable maps are continuous", where of course we have to look at "correct" topologies for this to make sense. (Ask a MO question if you want to know why.) Applied to choice this says that computable choice functions are continuous. But it is quite easy to come up with examples where the choice function cannot be continuous, for example we cannot choose continuously for each $x \in \mathbb{R}$ an integer $k \in \mathbb{Z}$ such that $x < k$. So you need not get into computability to see why choice has to fail in certain contexts. This might be helpful if you are familiar with topological sheaves.