This is a short post to ask a simple question that arises out of the discussion in a previous post about countability. As is well-known, the familiar statement that a countable union of countable sets is countable requires the axiom of countable choice. Indeed, it comes in in the very first step of the proof, where one says something along the lines of, “For each set let be an enumeration of its elements.” This uses the axiom of choice because if we don’t know anything about the sets then we can’t actually define these enumerations: we just have to assert that a sequence of enumerations exists.
However, if we do have explicit enumerations of the sets then the proof yields for us an explicit enumeration of their union. So one might take the following attitude to this particular application of the axiom of choice: the real theorem is “An explicitly enumerated union of explicitly enumerated sets is explicitly enumerated,” but because we often care only that enumerations should exist and don’t want to keep having to define artificial ones, it is convenient to appeal to the axiom of choice so that we can extend the theorem to the murky world of countable but not explicitly enumerated sets.
The question is this. Suppose we decided that we wanted a theory of explicit countability rather than pure-existence countability. Many of the basic results would still be valid: the rationals are explicitly countable, an explicit countable union of explicitly countable sets is explicitly countable, and so on. So where would things start to get difficult? Obviously, the statements one made would be less general, but where would that really matter to a mathematician not working in set theory?
As davidspeyer pointed out in an interesting comment on the previous countability post, there do exist explicitly definable sets that we can show are countable even though we cannot give a complete description of their elements: his example was the set of zeros of the Riemann zeta function, which are countable because they are isolated. However, even sets like this are explicitly countable in the required sense, since one can easily choose an ordering of in such a way that the elements of any subset of that has no accumulation point must be well-ordered. (For instance, write them as with and put them in order of first and then .)
To make the question slightly clearer, let us distinguish between two sorts of countability proof. One would be as follows: you’re given an explicitly defined set and you prove that it is countable. The other is where you deduce that your set is countable from some other property that it has. (For instance, you might have a collection of disjoint non-empty open sets in a separable metric space and you might deduce that it was countable by choosing distinct elements in each set that belonged to a countable dense set.) In the first case, are there instances where one can prove that the set is countable but not that it is explicitly countable? In the second case, are there ever circumstances where one cannot convert the general statement into an obviously corresponding, and equally useful, one about explicit countability? (For instance, if you have an explicitly enumerated dense set in your metric space then you can explicitly enumerate the open sets by taking the smallest element from the dense set, taking its index, and using that to order the open sets. Therefore, a collection of disjoint open sets in an explicitly separable metric space is explicitly countable.)
I’m writing this in the expectation that there are places where the axiom of countable choice is more than just a convenience in the sense just explained. But I haven’t thought of any myself. (The one thought I have is that countable ordinals become harder and harder to describe as they get bigger and bigger. Perhaps there is a countable ordinal that one can only just describe, but that is so big that describing an enumeration of it is not possible. Or perhaps that’s nonsense and there are sound theoretical reasons that any ordinal you can describe can also be explicitly counted.)