# Axiom of choice - to use or not to use

I was wondering if there are examples of results in mathematics that were first proven using axiom of choice and later someone found a proof of the result without using the axiom of choice.

-
Super far from the answer to your question, but a question from MO that I really like and I think you might like also is mathoverflow.net/questions/3557/… –  BBischof Dec 4 '10 at 6:17
There are probably tons of examples historically considering the axiom of choice wasn't explicitly singled out until relatively recently in history, but I don't think they'll be easy to find since mathematicians were not likely to have pointed out their usage of it before then. –  Qiaochu Yuan Dec 4 '10 at 12:24
The title of your question does not seem related to the question itself... –  Mariano Suárez-Alvarez Dec 4 '10 at 16:09
I think that asking for examples should be under big-list, and even if not then community wiki for sure. –  Asaf Karagila Dec 4 '10 at 19:29
@Mariano: I was just trying to sound Shakespearan. –  Derek Scavo Dec 5 '10 at 6:57

Cantor-Schroder-Bernstein theorem was first proved by Cantor using the axiom of choice. Proofs without using it came later.

-
This is probably the best possible answer to this question. –  Pete L. Clark Dec 4 '10 at 17:54
@Pete: Thanks! I really like the proof this theorem. –  AgCl Dec 4 '10 at 19:36
To say a bit more, the point is that in his proof of this theorem, Cantor introduced the Axiom of Choice for the first time, and people were indeed rather skeptical. –  Pete L. Clark Dec 4 '10 at 21:31

The issue is complicated by the fact that many (most?) "mainstream mathematicians" are not really keeping track of whether they are using some form of AC in their arguments. Moreover, they often do not write their proofs in such a way which makes clear either whether they are using AC or whether this use of AC is really necessary.

Here is an example from my own experience.

Theorem (Luther Claborn): For every abelian group $A$, there exists a Dedekind domain $R$ such that the ideal class group of $R$ is isomorphic to $A$.

I know of three proofs of this theorem.

1) Claborn's original 1966 proof:

http://math.uga.edu/~pete/claborn66.pdf

2) C. Leedham-Green's 1972 proof:

http://math.uga.edu/~pete/leedhamgreen.pdf

3) My 2008 proof:

http://math.uga.edu/~pete/ellipticded.pdf

Of these, the only one I am truly familiar with is my own. My proof uses transfinite induction. To be quite honest, I was pretty tickled by this: it was maybe the fourth time in my life that I had written down a transfinite induction argument and the first time that it was for any serious purpose.

Anyway, I soon heard from the eminent mathematician Bjorn Poonen (then at Berkeley) that he had been thinking about this very result because a student of Eisenbud's had recently given a seminar talk on Leedham-Green's proof (which I would describe as "clever and complicated"). The proof I had given was much more up his own alley, and he immediately found a way to recast / improve it. Among other things, his recasting completely avoided use of the Axiom of Choice. (But I hasten to add that there was more to it than that.)

We speculated briefly on the possibility that this modified argument was the first proof of Claborn's theorem to avoid AC. I asked whether Leedham-Green's proof used AC and he told me that indeed it was also a transfinite induction argument. So then I looked back at Claborn's paper and asked my student about it. We were able to point to some part of Claborn's argument (which, if you look at the paper, you'll see is rather terse: I wish the paper were more than four pages long!) which we thought used AC. But I don't remember what that was, and I am only moderately confident that we were right: if you told me otherwise, I wouldn't be too surprised.

And now I must tell you that I didn't include in my paper any hint that Poonen's modification would give an AC-less proof (and possibly the first such proof!) of Claborn's theorem. I felt that Poonen's argument was so nice that it deserved further exploration in its own right: I wanted to use it -- and still do -- to give a characterization of all abelian groups which can be the group of rational points on some elliptic curve over some field. So in essence I have been keeping to myself the fact that this theorem of Claborn (which lots of people know about) can be proved independently of AC. Sorry!

-

This article is an example of sorts where Doyle and Conway prove without using AC that for any two sets $A,B$ such that there is a bijection between the sets $3\times A$ and $3\times B$, where $3=\{0,1,2\}$, there is a bijection between $A$ and $B$. http://www.math.dartmouth.edu/~doyle/docs/three/three.pdf

This should be relatively easy to prove using well ordering principle which is equivalent to axiom of choice.

-

If $G$ is a locally compact abelian group, then there exists a unique measure $\mu$ on the Borel sets of $G$ such that:

1. $\mu(G)=1$,
2. For every measurable $A$ and $x\in G$: $\mu(A)=\mu(A+x)$,

We can slightly enlarge the Borel sets to include all the subsets of measure zero sets, and thus have a complete measure.

This measure is called Haar measure. In the case of $\mathbb R$ this is exactly the Lebesgue measure.

Haar (the mathematician) proved its existence on separable compact groups in 1933, and von Neumann proved the uniqueness shortly after.

The general case for locally compact Abelian groups was proved by Weil and relied on the axiom of choice. Henri Cartan later proved both existence and uniqueness of the general case without the axiom of choice.

-
(Warning: this comment contains egregious name-dropping.) I had dinner with Richard Borcherds and Stephen DeBacker about ten years ago and listened to the latter tell the former that he had supervised an honors (undergraduate) thesis on the construction of the Haar measure without AC. Borcherds's immediate reaction was that the uniqueness of the Haar measure was a big clue that AC should not be required. I found that to be a nice insight worth remembering. –  Pete L. Clark Apr 15 '12 at 12:15
@Pete: While true and important, remember that the uniqueness of an algebraic closure does require [some of] the axiom of choice. Indeed this is a whole different case here, but not everything unique is essentially "choice free". –  Asaf Karagila Apr 15 '12 at 12:17
@Asaf: One should not expect "unique up to isomorphism" shows AC is not needed. Merely "unique". –  GEdgar Apr 15 '12 at 12:36
A few remarks: $\mu(G) = 1$ can only hold if the group is compact. Haar assumed second countability, but neither compactness nor commutativity and while his proof used a little choice, his argument can without problems be adapted to avoid it in the second countable case. Weil and JvN proved uniqueness independently. Cartan's contribution was to modify Weil's argument to avoid AC in the general case. A nice account of Cartan's argument is here and here for a traditional account. –  t.b. Aug 6 '12 at 22:08

Things come full circle: Constructive proofs of the Hilbert Basis theorem.

-
Constructive/not constructive is not the same dichotomy as not using the Axiom of Choice / using the Axiom of Choice. So far as I know, the standard proof of HBT does not use the Axiom of Choice in any way. (Nor does the word "choice" appear in the article you link to.) –  Pete L. Clark Dec 4 '10 at 17:57
Tbh, why would somebody care about AC if they weren't worried about constructiveness of some or another proof? –  user126 Dec 4 '10 at 18:57
From personal experience: There are many reasons why people interested in set theory may want to keep track of uses of choice that have nothing to do with whether something is constructive or not. –  Andres Caicedo Feb 12 '11 at 21:56
Also, the axiom of choice is not necessarily non-constructive. For example, full choice is valid in constructive type theory. –  François G. Dorais Aug 6 '12 at 22:51