Is trying to prove a theorem without Axiom of Choice useless?

Suppose there is a well-known theorem whose usual proof uses Axiom of Choice. Is trying to prove it without Axiom of Choice useless? What merits can such a proof have?

It is often not useless at all. First let me give out a few reasons why it is useful:

1. It gives us a better understanding of how well-behaved some objects are. For example, vector spaces are not well-behaved in general, but in particular cases they are well-behaved (e.g. finitely generated ones).

   On the other hand, compact metric spaces are quite well-behaved and many of their properties remain valid even without the axiom of choice.

2. It can be the case that a proof without the axiom of choice is a much more constructive one, and allows us to examine the features of an object which was proved only to exist if the axiom of choice were used.

   One example coming to mind is the compactness of closed and bounded subsets of $\mathbb R$, another is the uniform continuity of a continuous function from a compact metric space into a metric space.

3. If a proof fails it allows us a better understanding of how much choice is needed for a certain assertion. Dependent Choice for Baire's Category theorem; Countable Choice for the equivalence between different topological properties; etc.

On the other hand, it is somewhat useless to try and prove a theorem without the axiom of choice if other parts of the theory already assume it. If you already assume that every vector space has a basis, showing that a certain proposition relying on this property holds without the axiom of choice is moot.

One example for this is the ultrafilter theorem which, together with the Krein-Milman theorem, imply the axiom of choice [4], so if you end up using both these propositions there is no use in avoiding choice anymore. It's there.

Regardless of the above, one should remember that not all things in modern mathematics are true in the absence of choice (that is, aside from the axiom of choice itself) and often reformulation and distinction between equivalent definitions is required. In those cases one can, and should, ask themselves how much choice is needed for a particular result.

For example, the assertion "$\mathbb R$ is not a countable union of countable sets" requires the axiom of choice, but it is provable from a vastly weaker statement, "countable unions of countable sets are countable".

Further reading:

1. Why worry about the axiom of choice? (MathOverflow)
2. Axiom of choice - to use or not to use
3. Advantage of accepting the axiom of choice
4. Is Banach-Alaoglu equivalent to AC?
5. Motivating implications of the axiom of choice?