Is (countable) AC necessary for a useful theory of Lebesgue measure? I am working through some notes on the Lebesgue measure, and I noticed that the proof that $\lambda^*$ (the outer measure) is countably sub-additive requires countable choice. (Short version of the proof: There is an interval covering $(I_{mn})_{n\in\Bbb N}$ of $A_m$ for each $x>\lambda^*(A_m)$, so choose $I_{mn}$ such that $\sum_n|I_{mn}|<\lambda^*(A_m)+\frac\epsilon{2^m}$. Then the set $\{I_{mn}|m,n\in\Bbb N\}$ is a countable collection of intervals with total length at most $\sum_m\lambda^*(A_m)+\epsilon$, so $\lambda^*(\bigcup_mA_m)\le\sum_m\lambda^*(A_m)$.) Without this property, $\lambda$ will not be $\sigma$-additive, and suddenly the whole theory becomes much more trivial.
Is this usage of countable choice necessary? I know set theorists like to play with Lebesgue measurability in ${\sf\neg AC}$-land, but maybe that only applies to full ${\sf AC}$, not ${\sf CC}$. Can anyone help clear this up for me?
 A: This is a bit tricky: In a sense, yes. It is consistent with set theory without choice that the set of reals is a countable union of countable sets. This makes it impossible to have a nontrivial measure that vanishes on singletons.  
On the other hand, countable choice suffices for the development of Lebesgue measure and its basic properties. It is more natural and comfortable to work with the stronger axiom of dependent choices, but one can make do with countable choice. 
However, one may still want to develop as much of the theory as possible in a choiceless setting, taking into account the limitations that the first paragraph above highlights. The standard approach then is not to work directly with Borel sets but rather with their codes. A code for a Borel set is a real (or a sequence of integers, or a certain tree) that specifies (via some fixed convention) witnesses to the set being Borel: Enumerate the basic open sets. An open set is union of some of them, so it can be specified by a list of the indices of these basic open sets. A closed set is a complement of one of these, so the code could begin with a number that we understand is our convention for "complement", and then a list of basic open sets. An $F_\sigma$ set is a countable union of closed sets, so it would begin with a number representing "union", and then interleave (in some fixed fashion) codes for the countably many closed sets. Etc. This is more robust than having simply the Borel sets, as the lack of choice may prevent certain possibilities. For instance, one can show that there is no code for $\mathbb R$ witnessing that it is a countable union of countable sets.
We can develop measure theory on the codes, in a sufficiently robust way to recover enough of the properties of Lebesgue measure that the function we end up with would be recognized as such. Countable additivity, for instance, would only be with respect to coded sequences of disjoint sets, etc. And (any code for) $\mathbb R$ is assigned infinite measure, as expected (rather than measure zero, as it would have been the case if we tried to work directly with the sets).
(For a quick idea of what goes on in here, take a look at how Solovay develops and uses codes in his paper on the consistency of "all sets of reals are Lebesgue measurable".)
The only reference that I know of for this is Volume 5 of Fremlin's monograph on Measure theory. Fremlin's notation and style may take some getting used to, but the presentation is very clear and thorough, the relevant subtleties are pointed out, and the differences and limitations of the choiceless setting versus the usual approach are indicated clearly.
A: There is a model of ZF (without choice) where the reals are a countable union of countable sets.  I don't see how Lebesgue measure can be countably additive there.  I recall this from the book "The Axiom of Choice" by ... Jech?   Theorem 10.6.  This theorem is followed by "It follows from Theorem 10.6 that without the Countable Axiom of Choice it is impossible to define satisfactorily Lebesgue measure, or even Borel sets."
