Why do most constructivists accept the axiom of countable choice?

Question

One obvious reason is that it is useful. But is there a philosophical justification for it? This axiom does not seem of constructive flavour to me since there is no clear way to construct a choice function of a countable collection of inhabited sets in general.

Answer 1

The answer to this is going to depend on the sort of underlying model/notion that leads one to care about constructive logic. Not all of them validate countable choice.

One that does (which I am most familiar with) is realizability, which is what you use when your interest in constructive mathematics is due to wanting the logic to have a fundamentally computable character. The reason that the axiom of choice fails in general in realizability is that propositions of the form:

$$∀ x : A. ∃ y : B. P(x, y)$$

are realized by procedures that, for each representation of an $A$ pick a representation of a $B$ and produce a witness that they satisfy $P$. However, in general there can be multiple representations of each $x : A$, and there is no obligation for the realizer to pick representations of the same $y : B$ for every representation of $x : A$. By contrast, a realizer for:

$$∃ f : B^A. ∀ x. P(x, f(x))$$

must give a procedure that does pick representatives of the same $y : B$ for every representative of $x : A$. This is because functions must respect equality, while $∀∃$ needn't. So, for instance, moving from the former to the latter cannot be done when $A$ is the real numbers $ℝ$. We can realize:

$$∀x : ℝ. ∃ n : ℕ. x < n$$

(implicitly embedding $ℕ$ back into $ℝ$) because for each representation of a real number, we can approximate the real enough to figure out some natural number that is bigger, but which natural we pick will depend on the details of the approximation (which is allowed for $∀∃$). But, we cannot realize:

$$∃f : ℕ^ℝ. ∀ x. x < f(x)$$

because there is no way to compute the same natural number for every representation of a given real number (every total, computable function from $ℝ$ to $ℕ$ is actually constant).

Now, the reason that countable choice works is that there is actually only one representation of each natural number. So, the procedure from:

$$∀ n : ℕ. ∃ y : B. P(n,y)$$

already satisfies the criteria for being a function. Or, if you want to complicate things, you could represent natural numbers as finite bit strings,¹ so that there are redundant elements, like $00100$ vs $100$. But, there is a computable function that calculates a canonical representation for any given representation. And that can be used to realize countable choice.

So, at least from a realizability/computability perspective, this is the meaning of axioms of choice. They are statements that we can canonicalize representations of some type. For natural numbers, we can, possibly trivially. For anything else that is countable, we can do it by mapping back and forth between the natural numbers. And for real numbers, finding a canonical representation is an uncomputable problem.

I wouldn't be surprised if other settings often fit into this framework. I.E. when (countable) choice holds, it's because the type is in some sense 'uniquely represented.' And when it doesn't, it isn't, and the operation of finding a 'canonical representation' violates the intrinsic character that the logic is supposed to have (computability, continuity, smoothness, etc.).

1: If you want to get fancy, you could probably represent natural numbers as appropriate terminating expressions in some programming language. Then there are many representations, but we can canonicalize them by doing the terminating reduction to a canonical value.