http://en.wikipedia.org/wiki/Axiom_of_dependent_choice
Is DC sufficient for the understanding of objects that are countable in some suitable sense? For example, is DC sufficient for the full development of the theory of von Neumann algebras on a separable Hilbert space?
Let me adopt an extreme interpretation of your question, in order to prove an affirmative answer.
Yes, in the arena of the countable, DC suffices.
To see why, let me first explain what I mean. If one wants to consider only countable sets, then the natural set-theoretic context is HC, the class of hereditarily countable sets. These are the sets that are countable, and all members are countable, and members-of-members and so on. The class HC is the land of all-countable set theory, the land of the fundamentally countable. I am not proposing that you want to remain within HC. Rather, you want to consider the properties of the objects in HC that are expressable there and what you can prove about them in ZF+DC, versus ZFC.
Since hereditarily countable sets can be coded easily by real numbers, it turns out that the structure HC is mutually interpreted in the usual structure of the reals R and vice versa. That is, the structure HC is essentially equivalent in a highly concrete way to the usual structure of the real numbers. And so questions about the fundamentally countable are equivalent to questions in the usual projective hierarchy of descriptive set theory. Thus, in this interpretation, your question is really asking whether one needs ever needs AC as opposed to DC in order to prove a projective statement.
Question. Are the projective consequences of ZFC the same as those of ZF+DC?
The answer is Yes, by the following theorem.
Theorem. A projective statement is provable in ZFC if and only if it is provable in ZF+DC.
Proof. It suffices to show that for every model W of ZF+DC there is a model of ZFC with the same reals. The reason this suffices is that in this case, any projective statement failing in a model of ZF+DC will also fail in a model of ZFC.
So, suppose that W is a model of ZF+DC. Let L(R) be the inner model of W obtained by constructing relative to reals. This is also a model of ZF+DC. Consider the forcing notion P in L(R) consisting of well-ordered countable sequences of real numbers in L(R), ordered by end-extension. Let G subset P be L(R)-generic for P. Since P is countably closed in L(R), it follows using DC that the forcing extension L(R)[G] has no additional real numbers. (The usual argument that countably closed forcing adds no new $\omega$-sequences makes essential use of DC, and indeed, DC is actually equivalent to that assertion.) And since G adds a well-ordering of these reals in order type $\omega_1$, it follows that L(R)[G] has a well-ordering of the reals. From this, it follows that L(R)[G] is actually a model of ZFC, since it has the form L[A], where A is a subset of $\omega_1$ enumerating these reals in the order that G lists them. Thus, we have provided a model of ZFC, namely L(R)[G], with the same reals as W. It follows that W and L(R)[G] have the same projective truth, since this truth is obtained by quantifying only over this common set of reals. QED
This phenomenon generalizes by the same argument beyond projective statements, to statements of the form "L(R) satisfies $\phi$". The point is that ZFC and ZF+DC prove exactly the same truths for L(R), since any model W of ZF+DC has the same L(R) as the model L(R)[G] in the proof above, and this satisfies ZFC.
The conclusion is that if you wish to study mathematical objects that are essentially countable only in the weak sense that they exist in L(R) — and this includes many highly uncountable objects — then the features about them in L(R) that you can prove in ZFC are exactly the same as the features you can prove in ZF+DC. So this interpretation is not so extreme after all...
