[borisp]

The key idea worth noting is that the AoC asserts the existence of something, namely a choice function, without actually asserting its computability. (An example of something that exists but is not computable is the smallest integer that a human being will never compute, assuming the human race exists for finite time.)

To say that a huge portion of modern analysis "falls apart" without it is somewhat narrow in scope...the existence of bases for arbitrary vector spaces and the existence of maximal ideals in arbitrary commutative rings both depend on the AoC.

What really falls apart is the convenience of stating various theorems that hold for "all" of something. Mathematicians are content to overlook this theoretical speedbump since an abundance of concrete examples exist where we can compute bases, maximal ideals, and so on, explicitly. In other words, if you are ever actually using mathematics to answer a concrete question, the AoC will never come up, since you must actually present whatever data or function you need.

One way to think about it is that whenever you use the AoC to prove a theorem, you have informally added "proof of concept" to your burden of proof. By this, I mean that any theorem or result that uses the AoC must be accompanied by an abundance of examples; otherwise, it is meaningless for "real life" use. Hence, we are content to ignore Banach Tarski and similar paradoxes, since they do not involve things that are explicitly computable.

P.S. Another consequence of the AoC is that we can consistently assign a meaningful limit to all bounded sequences...this is the Hahn-Banach theorem applied to the limit functional on the space of convergent sequences as a subspace of bounded sequences. So I guess (1, -1, 1, -1, ...) has a limit somewhere out there...