Axiom of choice leaking into everyday mathematics

Question

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?

Answer 1

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.

Answer 2

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.