4
$\begingroup$

Sometimes it is difficult to know whether or not we are formally invoking the axiom of choice. I wonder if some basic math proofs, which are not ordinarily associated with the axiom of choice, are in fact “secretly” using the axiom of choice?

Consider for example the following standard fact of linear algebra:


Suppose $V$ and $W$ are vector spaces, each with an uncountably infinite number of vectors. Let $T:V\rightarrow W$ be a surjective linear map.

Claim: If $\{v_1, …, v_n\}$ spans $V$, then $\{T(v_1), …, T(v_n)\}$ spans $W$.

Proof: Fix $w \in W$. Since $T$ is surjective, there exists a $v_w \in V$ such that $T(v_w)=w$, [and so on with the standard proof]. $\Box$


The idea here is that the proof must hold for all $w \in W$. So we must choose a $v_w \in V$ for each of the uncountably many $w \in W$. Is this an implicit use of the choice axiom?

$\endgroup$
  • 2
    $\begingroup$ There are a couple of choices happening in this proof, neither of which requires AC, if I'm not mistaken. First you choose a preimage for $w$, then you have to choose a linear combination of $v_1,\ldots,v_n$ that equals that preimage. Since those vectors are a spanning set, but not necessarily a basis, there may be more than one linear combination that works. $\endgroup$ – G Tony Jacobs Oct 11 '17 at 16:55
8
$\begingroup$

No, that argument does not depend on AC. You can argue that it "morally" needs infinitely many choices, but it does that while proving a claim, not while constructing an object. Or, in other words, nothing that depends on the choices it makes needs to be remembered beyond "yes, this is true for $w$ too".

I've written a longer answer previously that tries to explain some of the technical details that lead to this.


By the way, I think it is somewhat misleading to speak about AC "leaking into" everyday mathematics. The overwhelming consensus among mathematicians these days is that arguments that depend on AC are perfectly fine in "everyday mathematics". Caring about whether a particular argument depends on AC is essentially only done in the specialized area of set theory.

$\endgroup$
  • $\begingroup$ Disclaimer: I myself once published a computer science paper where the proof of our main claim required AC -- I don't remember what for anymore -- and we did mention that explicitly. But that was not so much to warn the reader of anything fishy about the argument, as it was pointing out a curiosity, because it is quite rare for computer-science proofs to need to go there. $\endgroup$ – Henning Makholm Oct 11 '17 at 16:59
  • $\begingroup$ I suppose the set-based setting here involves the uncountably infinite collection of sets $\{V_w\}_{w \in W}$, where $V_w = \{v \in V : T(v)=w\}$. Then fixing a $w \in W$ and choosing a particular element $v_w \in V_w$ is fine without the axiom of choice, but remembering, as you say, amounts to constructing the set $\{(w,v_w) : w \in W \}$ and that would use axiom of choice. $\endgroup$ – Michael Oct 11 '17 at 17:50
  • $\begingroup$ @Michael Correct. $\endgroup$ – Henning Makholm Oct 11 '17 at 17:57
  • $\begingroup$ Concerning your CS paper disclaimer, how can it be? Any arithmetical sentence that ZFC proves can be proven by ZF (without AC). So either your "main claim" isn't encodable as an arithmetical sentence, or it is just easier to prove using AC, but it makes me extremely curious as to what claim it was! $\endgroup$ – user21820 Oct 12 '17 at 9:27
  • $\begingroup$ @user21820: As I said, I don't remember the details (and cannot even find which paper it was now). We were doing static analysis for process calculi at the time, so it may have involved quantifying over all infinitely long histories of interaction between a system and its environment. I seem to remember that we had a later paper where we proved a more general result using more finitary techniques, so it wasn't a strict case of "this may be false in the absence of AC", but more "the proof we could come up with uses AC". $\endgroup$ – Henning Makholm Oct 12 '17 at 10:07
4
$\begingroup$

The proof that you suggest does not require the axiom of choice, as several people have pointed out.

However, other proofs do use the axiom of choice in a very subtle and implicit way. For example, every infinite set has a countably infinite subset is a statement which requires the use of the axiom of choice (or a different definition for "infinite").

Another important example would be that if we define a sequence recursively by simply showing that at each step "there is a way to continue to sequence", then there is a sequence which satisfies the construction.

A common place where this sort of argument is used is in analysis or topology, when arguing that in a metric space (e.g. $\Bbb R$), if $x$ is in the closure of $A$, then there is a sequence from $A$ converging to $x$. Simply at each step take a point closer than the last one you've taken. Another would be in arguing that in a finitely-splitting tree with infinitely many levels there is an infinite branch: at each step there is a node extending the branch you have so far, such that this node has infinite many points above it.


Henning said, and correctly so, that modern mathematician are not excited by using the axiom of choice. It is a good and useful axiom when it comes to managing the infinite.

The axiom of choice is not "leaking" into everyday mathematics, it was always there to some extent. When the French school of Lebesgue and Borel objected the use of the axiom of choice, they were implicitly using it themselves. As the methods for proving independence of logical statements in a set theoretic context were developed into the 1960s we saw that in fact a great deal of statements that are seemingly naive require the axiom of choice.

How naive? Well, naive enough that without them developing the notion of Borel sets become meaningless, let alone the Lebesgue measure. In an ironic twist of poetic justice, those who argued so thoroughly against using the axiom of choice were using it themselves all along.

(One could make the case that something like Dependent Choice is "good" and "uncountable choice" is evil, but there are things to say about that just as well.)

In any case, mathematicians saw that assuming the axiom of choice does not lead to [logical] contradictions, and they started to embrace it even deeper. The result, now, 80 years after Gödel's constructible universe, is that a few generations of mathematicians were educated upon results using the axiom of choice, and this sort of mathematics is ingrained in our "everyday mathematics".

And as it is always the case, after a few generations, some things simply become "fact". The standard of what we call "proof", the incompleteness phenomenon of mathematics, and just as those, the axiom of choice itself, are part of the subliminal mathematics that we take almost for granted when we think about mathematics. Even if sometimes we stop to think about those things are get confused and baffled.

$\endgroup$
  • $\begingroup$ On the "every infinite set has a countably infinite subset" example: That seems to only make a countable number of choices (so perhaps it only uses an "axiom of countable choice"?). My understanding is that the axiom of choice only becomes controversial and surprising when used for uncountably many choices (leading to crazy things like the Banach-Tarski paradox, the prisoner hat theorem, and so on). $\endgroup$ – Michael Oct 12 '17 at 17:13
  • $\begingroup$ Yes, you are correct. Nonetheless, there is a real possibility of these sets popping up in the vicinity of the real numbers. Even worse, if the Banach–Tarski paradox fails, you end up with failure of things like the Hahn–Banach theorem, and a bunch of other "very reasonable" theorems, and much worse: it means that there is a way to partition the real numbers into more sets than elements. How's that for weirdness? $\endgroup$ – Asaf Karagila Oct 12 '17 at 17:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.