This question arose after reading the answers (and the comments to the answers) to Why worry about the axiom of choice?.
First things first. In my intuitive conception of the hierarchy of sets, the axiom of choice is obviously true. I mean, how can the product of a family of non-empty sets fail to be non-empty? I simply cannot fathom it. Now, I understand that there are people who disagree with me; a mathematician of a (more) constructive persuasion would reply that mathematical existence is constructive existence. Well, we can agree to disagree. And besides, the distinction between constructive and non-constructive proofs is very much worth having in mind. First, because constructive proofs usually give more information and second, there are many contexts where AC is not available (e.g. topoi).
A second (personal) reason for championing AC is a pragmatic one: it allows us to prove many things. And "many things" include things that physicists use without a blink. Analysis can hardly get off the ground without some form of choice. Countable choice (ACC) or dependent countable choice (ACDC) is enough for most elementary analysis and many constructivists have no problem with ACC or ACDC. For example, ACC and the stronger ACDC are enough to prove that the countable union of countable sets is countable or Baire's theorem but it is not enough to prove Hahn-Banach, Tychonoff or Krein-Milman (please, correct me if I am wrong). And this is where my question comes in. In one of the comments to the post cited above someone wrote (quoting from memory) that the majority of practicing mathematicians views countable choice as "true". I have seen this repeated many times, and the way I read this is that while the majority of practicing mathematicians views ACC as "obviously true", a part of this population harbours, in various degrees, some doubts about full AC. Assuming that I have not misread these statements, why in the minds of some people ACC is "unproblematic" but AC's validity is not? What is the intuitive explanation (or philosophical reason, if you will) why making countably infinite choices is "unproblematic" but making arbitrarily infinite choices is somehow "more suspicious" and "fraught with dangers"? I for one, cannot see any difference, but then again I freely confess my ignorance about these matters. Let me stress once again that I do not think for a moment that denying AC is "wrong" in some absolute sense of the word; I just would like to understand better what is the obstruction (to use a geometric metaphor) from passing from countably infinite choices to arbitrarily infinite ones.
Note: some rewriting and expansion of the original post to address some of the comments.
Best Answer
Here is one explanation of why countable choice is not problematic in constructive mathematics.
For this discussion it is useful to formulate the axiom of choice as follows:
This says that a total relation $R \subseteq X \times Y$ contains a function. The usual formulation of the axiom of choice is equivalent to the above one. Indeed, if $(S_i)_{i \in I}$ is a family of non-empty sets we take $X = I$, $Y = \bigcup_i S_i$ and $R(i,x) \iff x \in S_i$ to obtain a choice function $f : I \to \bigcup_i S_i$. Conversely, given a total relation $R \subseteq X \times Y$, consider the the family $(S_x)_{x \in X}$ where $S_x = \lbrace y \in Y \mid R(x,y)\rbrace$ and apply the usual axiom of choice.
One way of viewing sets in constructive mathematics is to imagine that they are collections together with given equality, i.e., some sort of "presets" equipped with equivalence relations. This actually makes sense if you think about how we implement abstract sets in computers: each element of the abstract set is represented by a finite sequence of bits, where each element may have many valid representations (and this is unavoidable in general). Let me give two specific examples:
a natural number $n \in \mathbb{N}$ is represented in the usual binary system, and let us allow leadings zeroes, so that $42$ is represented by $101010$ as well as $0101010$, $00101010$, etc.
a (computable) real $x \in \mathbb{R}$ is represented by machine code (a binary string) that computes arbitrarily good approximations of $x$. Specifically, a piece of code $p$ represents $x$ when $p(n)$ outputs a rational number that differs from $x$ by at most $2^{-n}$. Of course we only represent computable reals this way, and every computable real has many different representations.
Let me write $\mathbb{R}$ for the set of computable reals, because those are the only reals relevant to this discussion.
An essential difference between the first and the second example is that there is a computable canonical choice of representatives for elements of $\mathbb{N}$ (chop off the leading zeroes), whereas there is no such canonical choice for $\mathbb{R}$, for if we had it we could decide equality of computable reals and consequently solve the Halting problem.
According to the constructive interpretation of logic, a statement of the form
holds if there is a program $p$ which takes as input a representative for $x \in X$ and produces a representative for $y \in Y$, together with a witness for $R(x,y)$. Crucially, $p$ need not respect equality of $X$. For example,
is accepted because we can write a program which takes as input a representative of $x$, namely a program $p$ as described above, and outputs a natural number larger than $x$, for example $round(p(0)) + 1000$. However, the number $n$ will necessarily depend on $p$, and there is no way too make it depend only on $x$ (computably).
Let us have a look at the axiom of choice again:
We accept this if there is a program which takes as input a $p$ witnessing totality of $R$ and outputs a representative of a choice function $f$, as well as a witness that $\forall x \in X. R(x, f(x))$ holds. This is probematic because $p$ need not respect equality of $X$, whereas a representative for $f$ must respect equality. It is not clear where we could get it from, and in specific examples we can show that there isn't one. Already the following fails:
Indeed, every computable map $f : \mathbb{R} \to \mathbb{N}$ is constant (because a non-constant one would allow us to write a Halting oracle).
However, if we specialize to countable choice
then we can produce the desired program. Given $p$ that witnesses totality of $R$, define the following program $q$ that represents a choice function: $q$ takes as input a binary representation of a natural number $n$, possibly with leading zeroes, chops of the leading zeroes, and applies $p$. Now, even if $p$ did not respect equality of natural numbers, $q$ does because it applies $p$ to canonically chosen representatives.
In general, we will accept choice for those sets $X$ that have computable canonical representatives for their elements. Ok, this was a bit quick, but I hope I got the idea accross.
Let me finish with a general comment. Most working mathematicians cannot imagine alternative mathematical universes because they were thoroughly trained to think about only one mathemtical universe, namely classical set theory. As a result their mathematical intuition has fallen a victim to classical set theory. The first step towards understanding why someone might call into question a mathematical principle which seems obviously true to them, is to broaden their horizon by studying other mathematical universes. On a smaller scale this is quite obvious: one cannot make sense of non-Euclidean geometry by interpreting points and lines as those of the Euclidean plane. Similarly, you cannot understand in what way the axiom of choice could fail by interpreting it in classical set theory. You must switch to a different universe, even though you think there isn't one... Of course, this takes some effort, but it's a real eye-opener.