# If a result is apparently provable with AC, is actually independent of ZF?

Given the number of results that are independent of ZF. It seems that once you've found a proof of a theorem that uses the axiom of choice, the odds are that it will be independent of ZF. So my question is:

-Is there any result that has a solution in ZFC which relies on AC, but has another proof that can be done only in ZF?

I'm especially interested in those results which people thought that were going to be independent of ZF, because only a proof relying on AC was known. And then someone found a proof in ZF.

When I say axiom of choice I'm also including weaker versions like countable choice or DC.

-
I don't understand your question. 98% of theorems in advanced algebra that are usually proven with the AC don't depend on the AC. –  darij grinberg Feb 5 '11 at 14:06
@darij At least the basic results in algebra need AC: the different definitions of noetherian aren't equivalent without DC. ( (mathoverflow.net/questions/53523/maximal-ideal-and-zorns-lemma). –  Gabriel Furstenheim Feb 5 '11 at 14:23
Yes, but few of their applications do. If you read some French, try out this: hlombardi.free.fr/liens/constr.html (particularly "Algèbre Commutative"). There are lots of results of the kind "any sufficiently elementary theorem provable in ZFC is provable in ZF or even constructively", where "sufficiently elementary" means things like "1st order formula", "geometric formula" and the likes. Some of these results, ironically, require ZFC themselves, while others don't. Alas, I am not an expert in this field ("program extraction from classical proofs"). –  darij grinberg Feb 5 '11 at 14:39
The Cantor-Bernstein theorem was first proved using AC but is provable without it as well. –  Asaf Karagila Feb 5 '11 at 15:01
I don't think the question is well-defined as stated. You can trivially insert "by the Axiom of Choice, ..." into the proof of any statement and then remove it. I think you meant to say "if a result apparently depends on AC, does it necessarily?" and then there are a million counterexamples. –  Qiaochu Yuan Feb 5 '11 at 15:34

Construction of the Haar integral for locally compact Hausdorff group $G$ ... as a linear functional on $C_{00}(G)$ ... is often done using the Axiom of Choice. In the Hewitt & Ross textbook ABSTRACT HARMONIC ANALYSIS this is Theorem (15.5), and they do it without AC. They do then have an exercise (15.25) where they outline the much shorter proof using Tihonov's Theorem.

-
I don't understand this answer. They are using the axiom of choice in the form of a well-known equivalent version. –  Andres Caicedo Feb 5 '11 at 19:48
I guess (but don't know) that Gerald means they present a proof without AC and then as an exercise suggest a much easier proof that does use AC (via Tichonoff's theorem). –  Tom Ellis Feb 5 '11 at 22:05
@Tom: Oh, I see! Thanks. –  Andres Caicedo Feb 6 '11 at 0:33
Tom is correct, isn't that what I said? –  Gerald Edgar Feb 6 '11 at 2:53
@Gerald: Yes, that is precisely what you said. (I misread and was confused.) It is a nice example. –  Andres Caicedo Feb 6 '11 at 2:57

The paper "Division by Three" by Doyle and Conway (link to PDF) gives a proof of the following result without appeal to the axiom of choice:

Let $A$ and $B$ be sets, and let $3$ denote a three-element set. If there exists a bijection from $3\times A$ to $3\times B$, then there exists a bijection from $A$ to $B$.

(This result is not due to Doyle and Conway -- it was first obtained by Lindenbaum and Tarski in 1926.)

-
This paper is also notable for giving a great conceptual proof of the Schröder-Bernstein theorem, as a warm-up to the main proof. –  Jim Conant Feb 6 '11 at 19:30
To say that it was first obtained by Lindenbaum and Tarski in 1926 is to skip over the actual history of the situation. Certainly it was not published in 1926, and Tarski many years later said he couldn't remember how Lindenbaum's argument for a key lemma went, but found a proof for it himself. The (Conway-)Doyle paper describes all this better than I can in a small comment box (they, or he [Doyle], surmise that they hit upon the argument Lindenbaum must have used, but I'd treat that as just a guess). –  Todd Trimble Jul 7 at 13:03

Tarski proved that, for any set $A$, the set $W(A)$ of well-orderable subsets of $A$ has strictly larger cardinality than $A$. This is trivial with AC, as then $W(A)$ is the whole power set of $A$ and thus Cantor's theorem applies. But Tarski gave a proof that avoids AC.

I don't have my copy of Howard and Rubin's "Consequences of the Axiom of Choice" handy, but if I did then I could probably find lots of examples by looking at the various forms numbered 0A, 0B, etc. I believe all of these are provable without AC (hence the number 0) but there was once a reason to suspect AC was needed.

-
The online version at consequences.emich.edu/conseq.htm allows you to enter a form number and get a pdf of all equivalent statements. Tarski's result is form 0 AE. –  François G. Dorais Feb 6 '11 at 10:45

There are many such proofs which use $AC$, but which are not even close to being independent of $ZF$. The general reason for this is how $AC$ is used. Normally the non-essential use of $AC$ appears when you have a very targeted application in mind, with additional structure in the background.

For example: Given an arbitrary collection of non-empty sets $\{X_\alpha: \alpha \in Y\}$ asserting that the product $Z =\Pi_{\alpha \in Y} X_{\alpha}$ is non-empty requires $AC$ when you have no structure imposed on the $X_\alpha$ and $Y$. However, when we add the assertion that each $X_\alpha$ is a ring, with additive identity $0_\alpha\in X_\alpha$, we then know that $Z$ is always non-empty without $AC$. The reason for this is because we now can define a function which witnesses that $Z$ is non-empty, in fact the function $\varphi:Y \rightarrow \bigcup X_\alpha$, given by $\varphi(\alpha) = 0_\alpha$ is such a witness, because $\varphi \in Z$.

That having been said, as for a specific example of a theorem for which everyone thought relied on $AC$ but was proven to hold in $ZF$, I cannot think of one off-hand that has not already been mentioned. But I think an example of what you are looking for might be contained in a question by Andres Caicedo, Distinct well-orderings of the same set and in his insightful answer to his own question.

-