8
$\begingroup$

The axiom of choice has a reputation as being a nefarious actor in set theory, the source of all sorts of horrible1, nonconstructive things. For example, to quote wikipedia:

The axiom of choice proves the existence ... objects that are proved to exist, but which cannot be explicitly constructed

However, the more I've learned about the subject, the further this popular description seems to be from the truth. For example, the axiom of choice is a consequence of the axiom of constructibility — logically, one must already accept the possible existence of nonconstructible sets before one can even entertain the idea of denying choice!

So, choice is clearly not the origin of nonconstructible things, although it does help such horrors to propagate.

Furthermore, in many constructive approaches to mathematics, the axiom of choice is a theorem — often a trivial one. For example:

  • In the propositions-as-types approach to doing logic in type theory, the assertion $\forall x \in X: \exists y \in x$ is literally a choice function on $X$
  • In the theory of computation, (the analog of) global choice is baked into the foundations (e.g. as the graded lexicographic order on strings). Furthermore, it is heavily used in the very basics of the subject (e.g. "iterate over all strings").

So, this leaves me with a question: how did the axiom of choice get the reputation it has? Were people simply wrong a century ago but the attitudes born from that time still persist? Is there some subtlety that gets lost in the popular account that does warrant criticism? Something else?

1: I do not actually find such things horrible.

$\endgroup$
  • $\begingroup$ Related, perhaps, math.stackexchange.com/questions/132007/…? $\endgroup$ – Asaf Karagila Sep 17 '17 at 17:58
  • $\begingroup$ I'm sure that you can find the answer buried in the analysis of the reactions from Lebesgue his French colleagues in Gregory Moore's wonderful book about the origins of Zermelo's Axiom of Choice. $\endgroup$ – Asaf Karagila Sep 17 '17 at 17:59
  • 1
    $\begingroup$ And another remark: The way the Wikipedia quote singles out the axiom of choice seems rather strange to me. Take for example the axiom of determinacy (AD) which proves (modulo ZF) the negation of choice and hence is a kind of anti-choice principle. (AD) proves the existence of all sorts of objects which cannot be 'explicitly constructed'. So why wouldn't the quote apply to this axiom as well? $\endgroup$ – Stefan Mesken Sep 17 '17 at 19:23
  • 1
    $\begingroup$ @AsafKaragila, I agree totally with you. Is worse than the nonmeasurabilityphobia. But the example is interesting and the comment by Terry Tao is wonderful (as usual). $\endgroup$ – Martín-Blas Pérez Pinilla Sep 18 '17 at 8:21
  • 2
    $\begingroup$ I don't see much evidence of an "anti-AC" position in the mathematical logic community, based on reading papers and hearing talks. This makes me suspect that some current "anti-AC" sentiment is partially a product of the internet, where "anti-AC" arguments spread themselves among readers who find the initial arguments appealing and don't have enough logic background to understand fully what is going on, and aren't around people who could clarify it for them in person. Part of the issue, of course, is that being "pro-AC" or "anti-AC" seems to be a relic of the early 20th century. $\endgroup$ – Carl Mummert Sep 18 '17 at 11:16
1
$\begingroup$

My utterly subjective impression: a sizable part the anti-AC folks hate specially the non Lebesgue measurable sets. This position seem very reasonable until you find that if all sets of reals are Lebesgue measurable, then it is possible to partition $2^\omega$ into more than $2^\omega$ many pairwise disjoint nonempty sets.

Intuitionists/constructivists are the another main source of resistance.

| cite | improve this answer | |
$\endgroup$
  • 2
    $\begingroup$ Intuitionists/constructivists resist TND, not (just) the AC. I wouldn't be surprised if the rejection of the AC is just a historical artifact: people were trying to be constructivists, but until the 1970s-or-so, a truly rigorous logical definition of constructivism wasn't around (Brouwer certainly didn't make himself easily understood), so the AC was chosen as an accessible target. $\endgroup$ – darij grinberg Sep 17 '17 at 20:03
  • $\begingroup$ @darijgrinberg, I suppose that TND = tertium non datur. In fact, in constructive set theory AC $\implies$ TND (en.wikipedia.org/w/…). $\endgroup$ – Martín-Blas Pérez Pinilla Sep 17 '17 at 20:16
  • $\begingroup$ Yes, I mean tertium non datur. Most constructivism these days (or at least most of it that I'm familiar with) works in type theory, though. $\endgroup$ – darij grinberg Sep 17 '17 at 20:34
  • $\begingroup$ @darijgrinberg. What is TND? $\endgroup$ – William Elliot Sep 18 '17 at 5:09
  • $\begingroup$ @WilliamElliot: Law of the excluded middle. The relevant theorem here is Diaconescu's theorem. $\endgroup$ – user14972 Sep 18 '17 at 5:10

Your Answer

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