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. (more…)