Why worry about the axiom of choice? As I understand it, it has been proven that the axiom of choice is independent of the other axioms of set theory.  Yet I still see people fuss about whether or not theorem X depends on it, and I don't see the point.  Yes, one can prove some pretty disturbing things, but I just don't feel like losing any sleep over it if none of these disturbing things are in conflict with the rest of mathematics.  The discussion seems even more moot in light of the fact that virtually none of the weird phenomena can occur in the presence of even mild regularity assumptions, such as "measurable" or "finitely generated".
So let me turn to two specific questions:

If I am working on a problem which is not directly related to logic or set theory, can important mathematical insight be gained by understanding its dependence on the axiom of choice?
If I am working on a problem and I find a two page proof which uses the fact that every commutative ring has a maximal ideal but I can envision a ten page proof which circumvents the axiom of choice, is there any sense in which my two page proof is "worse" or less useful?

The only answer to these questions that I can think of is that an object whose existence genuinely depends on the axiom of choice do not admit an explicit construction, and this might be worth knowing.  But even this is largely unsatisfying, because often these results take the form "for every topological space there exists X..." and an X associated to a specific topological space is generally no more pathological than the topological space you started with.
Thanks in advance!
 A: As Pete Clark says, 
"In general, I think "Why do people worry about X?" is primarily psychological. I can (and alas, do) worry about the correctness of my proofs for lots of reasons...but fundamentally I am worried about myself and not about some mathematical object or principle."
Let me explain why I worry about the axiom of choice and, generally, about non-constructive methods in mathematics. One of the fascinating aspects of mathematical activity is that it produces results that can transcend our life, like the Pythagorean theorem or Newton's binomial formula. 
Many concepts of (formalized) mathematics evolved as ideal models of concrete things: some functions can model the movement of a particle, Turing machines model something following an algorithm, etc.. Although the relationship between the abstract, formal concept and the "real" thing is sometimes loose, it is a historical fact that the concepts were devised as models of such concrete things. 
Mathematical theorems proved in a constructive way generally have a close connection to algorithmic processes that can possibly be relevant for humans of all times. But for example, the axiom of choice establishes a similarity between finite and infinite sets (which are qualitatively different, for example, no finite set is bijective to a proper subset) that is difficult to justify from an objective point of view. It states that infinite products of nonempty sets are nonempty. As far as I see, there isn't an objective argument to prefer the axiom of choice to it's negation. Future generations of mathematicians could possibly negate it (or more probably, live it undecidable) and a lot of parts of twentieth century mathematics would cease being theorems. 
However, it seems less likely that a future mathematical language would cease providing concepts that mimick, for example, automata. 
Note: The undecidability of the axiom of choice in ZF theory is still a metatheorem, so if a ZF statement can be proved false using AC, then it is (meta) clearly not a theorem. So the axiom of choice could still be useful for studying ZF, as a tool to produce counterexamples that limit our theorem-proving pretensions, but with the same formal status as, say, its negation. 
Also note: I see that this answer is not part of math if math is understood as the study of the consequences of the ZFC axioms, and also it doesn't deal with the specific questions, but I hope that it explains why (some) people worry and fuss about the axiom of choice. It may be relevant, for example, for math professors, that could atract a wider audience by presenting a more secular version of mathematics that excludes the axiom of choice from the set-theoretic formalism. Independently of whether they use it or not in their own work.
A: We have a proof that AC is independent of the other axioms of ZF. But that's not a good enough criterion for deciding whether or not to use an axiom. We choose axioms because because we want to use them to reason reliably. We can use ZF to reason about mundane things like strings of symbols encoded with Godel numbering. But Godel's Incompleteness Theorem shows that we can find axioms independent of ZF, which when added to ZF, give incorrect results when applied to strings of symbols. I think some people worry that AC may allow us to reason incorrectly in some domains, even if it is consistent with ZF. (Of course we don't know ZF itself is consistent, or allows us to reason correctly, either, but the fewer axioms the better.)
A: Daniel Asimov's answer regarding the multiplicative axiom (Russell's terminology) seems important, as it is very difficult to disbelieve that statement (on cardinality principles alone).  But I think the key is that AC is equivalent to the well ordering theorem, which is easy to disbelieve and untrue in some models of ZF. And of course, infinite cardinality requires AC to get a well-defined order, so the intuitiveness of the multiplicative axiom is less intuitive than it seems.
I like a comment James Munkres made in his Topology textbook regarding the construction of the first uncountable ordinal: you can do it without AC, but then you can't use it for anything!  It's that property that you can DO something with your choice that produces both beauty and monsters, and I think this is intrinsically related to some kind of well-ordering.
I really like Horst Herrlich's Springer Lecture Note on AC (#1876), which is both short and comprehensive about what choice does across multiple disciplines.  While it thoroughly discusses the well-known pathologies ("Disasters", as he formally names them!), it also discusses more fundamental issues like how the various equivalent notions of compactness fly apart without AC.
A: The main tradeoff involved in accepting the axiom of choice is basically whether you want an axiom that makes notions of cardinality very well behaved, while in exchange making notions of space very poorly behaved.
In particular, it implies the law of the excluded middle via Diaconescu's theorem, which means it is not satisfied by the topos of sheaves on a topological space. And it also implies that non-measurable subsets of the reals exist, which means that general sets also no longer have a notion of measure.
Alternative choices of axiomatization for sets like the axiom of determinacy (which is consistent with ZF + dependent choice) may completely mess up notions of cardinality for uncountable sets, like making different notions of cardinality non-equivalent and giving the quotient group R/Q (using addition) a larger cardinality than R. In exchange for this, the axiom of determinacy makes every subset of the reals measurable. If you give up even stronger notions of choice, particularly when you give up the excluded middle, you get a notion of set that is compatible with notions of neighbourhoods in a topological space.
So the most fundamental reason to doubt the axiom of choice is not whether or not it is reasonable or consistent (ZFC is equiconsistent with ZF), but whether or not you think that ZFC models something you are interested by. If you care more about cardinalities of sets than about geometric notions, then the axiom of choice is very reasonable. If you would rather not have to think about geometrically weird things like non-measurable sets but do not care whatsoever about set-theoretical weirdness, then you may be interested in other alternative axiomatizations that still behave the same in the special case of countable and/or constructible sets.
Ultimately though, given the historical ubiquity of AC, I consider choice to be part of the definition of sets as a well-pointed topos with natural numbers and choice, with possibly some additional extensions such as universes or replacement. If you assume something that implies the negation of AC, you are studying something different  than "standard" sets and should make that explicit. But that "something else" may be more useful to entire fields of mathematicians than sets are.
A: There are of course reasons to care about the axiom of choice because there are
categories in which epimorphisms do not split. However if one sticks to the
category of sets my position could be (provocatively) described as follows:
The axiom of choice is obviously false but that doesn't stop me from using
it.
Before I go on to explain why I think it is false let me make a general
remark. Set theory is a mathematical model for mathematics it isn't mathematics
itself. We all know that all models usually manage to model some part of what
they model but they almost never correctly model everything. Things are a little
bit more complicated in the case of set theory but it is also supposed to be the
common language of mathematics. However, it really works as such only as a protocol
for conflict resolution; in case we disagree over a proof we are supposed to
work our way down to formal set theory where there couldn't possibly be any
conflicts. However, most mathematicians would rather, I believe, voluntarily
submit to extended flagellation than actually work with formal set theory.
Luckily, in practice all disagreements are resolved long before one reaches that
level. Furthermore, most working mathematicians show a cavalier towards set
theory. It is quite common to speak of the free group on isomorphism classes of
objects in some large category which is not possible in formal set
theory as the the isomorphism classes are themselves proper classes and hence
can not be members of some class. Of course, when pressed a mathematician using
such a phrase would probably modify it by speaking of skeleta but I have once
been criticised when using a slightly different formulation that avoided the
problem without speaking of skeleta as being wrong for set-theoretic
reasons. (This is not meant as a criticism of the person in question, a working
mathematician should have the right to ignore the horny parts of set theory, at
their own peril of course.)
Now, the reason why I believe that the axiom of choice is obviously false is
that gives us an embedding of the field of $p$-adic numbers into $\mathbb C$
which seems fishy as they are constructed in such different ways. In fact if you
try to pin down such an embedding by asking for it to fulfil more conditions
then it doesn't exist. This is true if you ask that it be measurable or take
definable numbers to definable numbers and so on. My own feeling is that its
existence is so counter-intuitive that it couldn't possibly existst. On the
other hand such an embedding is used over and over again in say the theory of
$\ell$-adic cohomology. It is true that in that case at least it can be avoided
(Deligne seems to share some of my disbelief as in his second paper on the Weil
conjecture he starts with a short discussion on how to avoid it but still uses
it as it cuts down on uninteresting arguments).
My feeling about the axiom of choice is pragmatic; it is useful and doesn't seem
to get us in trouble so I have no qualms using it (even though I don't believe
in it fully). I have also a picture of sets which could be used to justify this
contradictory (I am not trying to formalise it so it should not be considered a
competing model of mathematics). To me all elements of a set are not on
equal footing. Taking my cue from algebraic geometry, there are closed points
which are "real" elements but also non-closed points. Hence, the set of
embeddings of the $p$-adic numbers in $\mathbb C$ is under the axiom of choice a
non-empty set but in my opinion it does not contain any closed points. (In fact
all its elements are probably generic, i.e., their closure is the whole set.) As
long as you only deal with "concrete" objects (which should be closed in any set
in which they are contained but maybe should be something more) the conclusions
about them that are obtained by using the axiom of choice should be OK.
A: The way I always justified the usage of the axiom of choice to myself (which I haven't had to do very often) is as an expositional convenience. If somebody told me that I couldn't use the axiom of choice anymore, I would take all the theorems I know about commutative rings and replace "Let R be a commutative ring" with "Let R be a commutative ring with a maximal ideal", and then I would go about my business, since nobody cares about the crappy ring you slapped together which doesn't have a maximal ideal.
A: I would like to point out that a lot of the people who are interested in the Axiom of Choice (AC) are not worried about it in any mathematical way.
In general, I think "Why do people worry about X?" is primarily psychological.  I can (and alas, do) worry about the correctness of my proofs for lots of reasons...but fundamentally I am worried about myself and not about some mathematical object or principle.
In fact, I don't see what there is to worry about concerning AC.  We know it is independent of ZF, we know it has some counter-intuitive consequences, and we know that many of our most basic and fundamental "abstract" theorems either require AC to hold in full generality (in the sense that there are models of ZF in which they are false) or in fact are equivalent to AC: e.g. every vector space has a basis (equivalent), the product of quasi-compact spaces is quasi-compact (equivalent), every field has an algebraic closure (required), every ring has a maximal ideal (equivalent),...I think we have all the information that we need on the role of AC in mathematics.  
On the other hand, if you encounter a theorem, it is often an interesting question to ask whether the proof uses AC and, if it does, whether it can be modified so as not to require AC or only to require some weaker form of AC.  As an example, I asked the following MO question
How much choice is needed to show that formally real fields can be ordered?
and the answer was a reference to a paper where it was shown that the orderability of 
formally real fields is equivalent to the Boolean Prime Ideal Theorem.  This is an interesting paper; I learned more about field theory (not set theory) by reading it.  
Why is it interesting to ask whether a proof requires AC?  For starters, for good reasons (not worries!) people are interested in making proofs constructive as much as possible.  You say that you've proven that for every number field $K$, and positive integer $n$, there exists a genus one curve $C_{/K}$ such that the least degree of a closed point on $C$ is equal to $n$?  (Yes, I have.)  OK, I'll give you $K$ and $n$: can you give me an explicit set of defining equations defining such a curve?  (No, I can't!)  My theorem would be better if it could be made explicit -- it's obvious, isn't it?
It is a generally believed "meta-theorem" that if a result can be shown to require AC, then it is certifiably non-constructive.  Thus, if one is trying to make a certain result constructive, one would certainly like to know whether AC is essentially involved in its proof.  
A: Another useful example is the statement that  $M$ and $M^2$ have the same power for  any infinite set $M$. This is proved with the use of the axiom of choice.
This fact have some applications in supermathematics. If infinite set $M$ is the index set for generators  of a Grassmann-Banach algebra $G$ with an $l_1$-norm then the $l_1$-basis in $G$ has the same power as $M$. (See paper of mine in: 
Siegel W., Duplij S. and  Bagger J., eds. (2004), Concise Encyclopedia of Supersymmetry And Noncommutative Structures in Mathematics and Physics, Berlin, New York: Springer-Verlag; math-ph/0009006.) To circumvent the axiom of choice in this example one needs to consider $M$ to be a well-ordered set. But in general the construction of $G$ does not need a linear ordering in $M$. Of course, when physicists calculate Berezin's integral the power of $M$ and the axiom of choice are under the carpet of the calculations but the foundations (the flooring under the ``carpet'') need the axiom of choice.
A: When I first encountered AC as an undergraduate student, like most math students I thought it was seriously questionable since it led to weird and counter-intuitive things like non-measurable sets and, worst of all, the Banach-Tarski Paradox.
But after I learned that AC is logically equivalent to 
 **The cartesian product of any non-empty collection of non-empty sets is non-empty**

I found it impossible not to believe it.  My only conclusion could be that my mathematical intuition was not well-developed.  
I came to accept the consequences of AC as natural aspects of mathematics, and they no longer seem nearly as weird or counter-intuitive as they did at first.
And I would be fairly unhappy if there existed a vector space without a basis.  Or if there existed two sets A, B without an injection, bijection, or surjection A -> B (i.e., a failure of Trichotomy).

On the other hand, I have begun to be philosophically troubled by the common and probably harmless assumption that mathematicians can choose between the two complex roots of
(*)           z2 + 1  = 0
(and similar situations).  There is no basis for selecting between i and -i . . . or even naming them i and -i !  So although I intend to continue referring to i for convenience, it feels to me that technically one has no right to do so; instead a technically correct discussion should always refer to the set of roots of (*), but never just one of them alone.
A: If you are doing analysis, presumably you want to use Lebesgue measure.  In order for Lebesgue measure to have its usual properties, it is essential that $\mathbb{R}$ is not a countable union of countable sets.
A: I'll give you a reason that applies to people who aren't just philosophically prejudiced:
Anything proven without resorting to the law of excluded middle (which is implied by the axiom of choice) is true in any elementary topos.  There are certainly people who don't like AC for philosophical reasons, but this is a good reason for any mathematician of any persuasion.
A: It is a mistake to think that the axiom of choice has no relevance to, say,
undergraduate mathematics. The axiom of choice makes undergraduate
analysis easier by enabling one to say that $f(x)$ is continuous at $x=a$
if $f(a_n)$ tends to $f(a)$ for each sequence $\langle a_n \rangle$ that
tends to $a$.
The popular undergraduate text Understanding Analysis by Stephen Abbott
owes its success (at least partly) to the use of this definition rather
than the $\varepsilon-\delta$ definition. But the definitions are equivalent
only assuming some form of the axiom of choice. (The book does not mention this,
however.)
A: How I Learned to Stop Worrying and Love the Axiom of Choice
The universe can be very a strange place without choice. One consequence of the Axiom of Choice is that when you partition a set into disjoint nonempty parts, then the number of parts does not exceed the number of elements of the set being partitioned. This can fail without the Axiom of Choice. In fact, if all sets of reals are Lebesgue measurable, then it is possible to partition $2^{\omega}$ into more than $2^{\omega}$ many pairwise disjoint nonempty sets!
A: The best answer I've ever heard --- and I think I heard it here on MathOverflow from Mike Shulman, which suggests that this question is roughly duplicated somewhere else --- is that you should care about constructions "internal" to other categories:


*

*For many, many applications, one wants "topological" objects: topological vector spaces, topological rings, topological groups, etc.  In general, for any algebraic gadget, there's a corresponding topological gadget, by writing the original definition (a la Bourbaki) entirely in terms of sets and functions, and then replacing every set by a topological space and requiring that every function be continuous.

*A closely related example is that you might want "Lie" objects: sets are replaced by smooth manifolds and functions by smooth maps.

*Another closely related example is to work entirely within the "algebraic" category.


In all of these cases, the "axiom of choice" fails.  In fact, from the internal-category perspective, the axiom of choice is the following simple statement: every surjection ("epimorphism") splits, i.e. if $f: X\to Y$ is a surjection, then there exists $g: Y \to X$ so that $f\circ g = {\rm id}_Y$.  But this is simply false in the topological, Lie, and algebraic categories.
This leads to all sorts of extra rich structure if you do algebra internal to these categories.  You have to start thinking about bundles rather than products, there can be "anomalies", etc.
Update:
In the comments, there was a request for a totally explicit example, where Axiom of Choice is commonly used but not necessary.  Here's one that I needed recently.  Let $\mathcal C$ be an abelian tensor category, by which I mean that it is abelian, has a monoidal structure $\otimes$ that is biadditive on hom-sets, and that has a distinguished natural isomorphism $\text{flip}: X\otimes Y \overset\sim\to Y\otimes X$ which is a "symmetry" in the sense that $\text{flip}^2 = \text{id}$.  Then in $\mathcal C$ is makes sense to talk about "Lie algebra objects" and "associative algebra objects", and given an associative algebra $A$ you can define a Lie algebra by "$[x,y] = xy - yx$", where this is short-hand for $[,] = (\cdot) - (\cdot \circ \text{flip})$ — $x,y$ should not be read as elements, but as some sort of generalization.  So we can makes sense of the categories of $\text{LIE}_{\mathcal C} = $"Lie algebras in $\mathcal C$" and $\text{ASSOC}_{\mathcal C} = $"associative algebras in $\mathcal C$", and we have a forgetful functor $\text{Forget}: \text{ASSOC}_{\mathcal C}  \to \text{LIE}_{\mathcal C}$.
Then one can ask whether $\text{Forget}$ has a left adjoint $U: \text{LIE}_{\mathcal C}  \to \text{ASSOC}_{\mathcal C}$.  If $\mathcal C$ admits arbitrary countable direct sums, then the answer is yes: the tensor algebra is thence well-defined, and so just form the quotient as you normally would do, being careful to write everything in terms of objects and morphisms rather than elements.  In particular, if $\mathfrak g \in \text{LIE}_{\mathcal C}$, then $U\mathfrak g \in \text{ASSOC}_{\mathcal C}$ and it is universal with respect to the property that there is a Lie algebra homomorphism $\mathfrak g \to U\mathfrak g$.
Let's say that $\mathfrak g$ is representable if the map  $\mathfrak g \to U\mathfrak g$ is a monomorphism in $\text{LIE}_{\mathcal C}$.  By universality, if there is any associative algebra $A$ and a monomorphism $\mathfrak g \to A$, then $\mathfrak g \to U\mathfrak g$ is mono, so this really is the condition that $\mathfrak g$ has some faithful representation.  The statement that "Every Lie algebra is representable" is normally known as the Poincare-Birkoff-Witt theorem.
The important point is that the usual proof — the one that Birkoff and Witt gave — requires the Axiom of Choice, because it requires picking a vector-space basis, and so it works only when $\mathcal C$ is the category of $\mathbb K$ vector spaces for $\mathbb K$ a field, or more generally when $\mathcal C$ is the category of $R$-modules for $R$ a commutative ring and $\mathfrak g$ is a free $R$-module, or actually the proof can be made to work for arbitrary Dedekind domains $R$.  But in many abelian categories of interest this approach is untenable: not every abelian category is semisimple, and even those that are you often don't have access to bases.  So you need other proofs.  Provided that $\mathcal C$ is "over $\mathbb Q$" (hom sets are $\mathbb Q$-vector spaces, etc.), a proof that works constructively with no other restrictions on $\mathcal C$ is available in 


*

*Deligne, Pierre; Morgan, John W.
Notes on supersymmetry (following Joseph Bernstein). Quantum fields and strings: a course for mathematicians, Vol. 1, 2 (Princeton, NJ, 1996/1997), 41--97, Amer. Math. Soc., Providence, RI, 1999.  MR1701597.


They give a reference to


*

*Corwin, L.; Ne'eman, Y.; Sternberg, S.
Graded Lie algebras in mathematics and physics (Bose-Fermi symmetry).
Rev. Modern Phys. 47 (1975), 573--603. MR0438925.


in which the proof is given when $\mathcal C$ is the category of modules of a (super)commutative ring $R$, with $\otimes = \otimes_R$, and, importantly, $2$ and $3$ are both invertible in $R$. [Edit: I left a comment July 28, 2011, below, but should have included explicitly, that Corwin--Ne'eman--Sternberg require more conditions on $\mathcal C$ than just that $2$ and $3$ are invertible. Certainly as stated "PBW holds when $6$ is invertible" is inconsistent with the examples of Cohn below.]
Finally, with $R$ an arbitrary commutative ring and $\mathcal C$ the category of $R$-modules, if $\mathfrak g$ is torsion-free as a $\mathbb Z$-module then it is representable.  This is proved in:


*

*Cohn, P. M.
A remark on the Birkhoff-Witt theorem.
J. London Math. Soc. 38 1963 197--203. MR0148717
So it seems that almost all Lie algebras are representable.  But notably Cohn gives examples in characteristic $p$ for which PBW fails.  His example is as follows.  Let $\mathbb K$ be some field of characteristic $p\neq 0$; then in the free associative algebra $\mathbb K\langle x,y\rangle$ on two generators we have $(x+y)^p - x^p - y^p = \Lambda_p(x,y)$ is some non-zero Lie series.  Let $R = \mathbb K[\alpha,\beta,\gamma] / (\alpha^p,\beta^p,\gamma^p)$ be a commutative ring, and define $\mathfrak g$ the Lie algebra over $R$ to be generated by $x,y,z$ with the only defining relation being that $\alpha x = \beta y + \gamma z$.  Then $\mathfrak g$ is not representable in the category of $R$-modules: $\Lambda_p(\beta y,\gamma z)\neq 0$ in $\mathfrak g$, but $\Lambda_p(\beta y,\gamma z)= 0$ in $U\mathfrak g$.
A: Many years ago I have been a professor for abstract analysis and had no reservations whatever against using the axiom of choice or "equivalent" statements as e.g. Zorn's lemma since many results in functional analysis depend heavily on it.  I have also been very impressed by nonstandard analysis especially in the version of Nelson. But in the mean time  I have become  more skeptical.  I am still very impressed by the results mathematics has obtained by treating the infinite world  analogous to the finite world, but I have the feeling that there are some sorts of levels in mathematics which should not be confused. 
This is of course a very vague assertion. But consider the general statement that every vector space has a basis. This belongs to the infinite world which is "far away". Here Zorn's lemma seems to be the  appropriate means.
Then consider the statement that each continuous solution of the functional equation f(x+y)=f(x)+f(y) over the reals has the form f(x)=ax.  This belongs to the finite world. 
But the statement that there exist discontinuous solutions mixes  both worlds. It uses the existence of a Hamelbasis for the reals over the rationals.  Here I am not sure what this  really means. It seems that this gives an explanation of what discontinuous solutions look like. But in fact it gives only an illusion of what such solutions look like.
A: Yes, many people continue to fuss about the Axiom of Choice. 
At least part of the explanation for why people continue to fuss as they do over the Axiom of Choice is surely the historical fact that there was a period of several decades during which the axiom was not known to be relatively consistent with the other axioms of set theory.  It was after all not until 1938 that Goedel proved the relatively consistency of ZFC over ZF, using the constructible universe, and several more decades passed until Paul Cohen completed the independence proof by proving that ¬AC is also relatively consistent with ZF, using the method of forcing in 1962. It was during these intermediate times, and especially the time before 1938 when the axiom was not known to be consistent, that the increasingly bizarre consequences of AC were being discovered, and so  the habit naturally developed to pay close attention to when the axiom was used. This habit surely lessened after the independence results, but it was not dropped by everyone. And so today mathematics is populated by large numbers of mathematicians like yourself (and perhaps myself), who freely use AC without worry, and who may even find the possibilities occuring in non-AC situations, such as infinite Dedekind finite sets, to be even weirder than the supposed non-regularities of AC, such as the existence of non-measurable sets. 
Yet, even though I largely agree with the feeling you indicate in your question, there is still some reason to pay attention to AC. First, in mathematical situations where one can prove the existence of a mathematical structure without AC, then  important consequences often follow concerning the complexity of that structure. An explicit construction, even if more complicated that a pure existence proof from AC, often carries with it computational information concerning the nature of the object constructed, such as whethere it is analytic or Borel or $\Delta^1_2$, and so on, and these complexity issues can affect other arguments concerning measurability and whatnot. That is, by nature the non-AC constructions are more explicit and these more explicit argument often carry more information. 
But second, there remain certain parts of set-theoretic investigation that only make sense in non-AC contexts. The Axiom of Determinacy, for example, stands in contradiction with the Axiom of Choice but nevertheless contains some fascinating, profound mathematical work, pointing to a kind of mathematical paradise, in which every set of reals is Lebesgue measurable, every set has the property of Baire and the perfect set property. This axiom leads to an alternative vision of what set theory could be like.  The possibilities of AD place limitations on what we can expect to prove in ZFC, in part because we expect that there are set-theoretic universe close to our own where AD holds. That is, we are interested in AD even if we believe fundamentally in AC, because we can construct the universe L(R), where AD could hold, even if AC holds in the outer universe V. In order to understand L(R), we need to know which theorems we can rely on there, and so we need to know where we used AC.
