Axiom of Computable Choice versus Axiom of Choice

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?

-
What exactly do you mean by the "Axiom of Computable Choice"? How would you phrase it as a sentence (or set of sentences) in the first order language of sets? Note also that many would take exception with your statement "[S]tandard mathematics really only operates within the computable realm, with few notable exceptions." I think 90% of research mathematicians have only a vague familiarity with notions of computability and are perfectly happy that way. – Pete L. Clark May 23 '10 at 14:17
What does a computable element of $\aleph_{17}$, say, look like? What would be a computable choice function for the family $\{A_r : r \subseteq \omega\}$ where `$A_r = \{ x \subseteq \omega : r <_T x \}$? – François G. Dorais May 23 '10 at 15:51
Francois is getting at the same thing I was: your question seems to presume a mixture of computability and set theory. How this is supposed to work is not obvious to me. But I am not an expert in set theory and know almost nothing about computability theory. Maybe someone else can make sense of your question... – Pete L. Clark May 23 '10 at 16:52
A typical analysis book is packed full of theorems that cannot be proven constructively. Even very basic theorems like the intermediate value theorem. – Dan Piponi May 23 '10 at 18:39
@sigfpe: You are mistaken. A typical real analysis book is packed with theorems that can be proved constructively. Just have a look at Bishop's "Foundations of Constructive Analysis". You will find the intermediate theorem there, too. – Andrej Bauer May 24 '10 at 12:40

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.

-

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.

-
Andrej, Thank you for the elaboration. Also a great answer to a not so good question. – Halfdan Faber May 23 '10 at 19:44
+1. Thanks, Andrej, I thought you would show up with some constructivist ideas. – Joel David Hamkins May 23 '10 at 20:15
I think you are glossing over the difference between choice in topos theory and choice in theories of higher-order arithmetic such as HA^\omega. In the latter context, the full choice scheme for higher-order arithmetic in all finite types is constructively valid. I don't think that qualifies as "countable and dependent choice". This complete acceptance of choice is inherent in Bishop's quote, "a choice is implied by the very meaning of existence". There is no difference between AC_{0,0} and AC_{15,19} from that perspective. – Carl Mummert May 26 '10 at 15:00
@Carl: Thanks for mentioning higher-order arithmetic. But I was not "glossing over" it, I simply did not mention it. Are you saying that according to Bishop's understanding of mathematics, choice at higher arithmetical types is valid (in an absolute sense)? I would say the consistency of choice with higher-order arithmetic is an accident caused by the fact that only very special sets, namely $\mathbb{N}$, $\mathbb{N}^\mathbb{N}$, $\mathbb{N}^{\mathbb{N}^\mathbb{N}}$, ..., are available in the theory. – Andrej Bauer May 27 '10 at 0:47
I have always read Bishop's statements as saying that, but there may be some other writings I have not seen in which he clarifies his opinion. Since Bishop's book doesn't choose any particular formalism, it's possible to interpret it in many formal systems, and I'm biased because the first interpretation I learned for it was HA^\omega. I will have to use a separate comment to respond about something about AC. – Carl Mummert May 27 '10 at 5:26