This is something I thought about a couple years ago when I was giving a talk to the math grad students about the Axiom of Choice and the Axiom of Determinacy. I never got around to writing up though, so I figured I’d put it here. My contention is going to be that (contrary to standard assumptions) classical mathematicians should accept Determinacy rather than Choice, and that intuitionists should actually support Choice, even though they have traditionally been some of its primary enemies.

The Axiom of Choice (AC) says that for any collection S of sets, if then . That is, for any collection of non-empty sets, there is a function that assigns an element of each set to that set.

The Axiom of Determinacy (AD) is slightly more complicated to explain. Given a set S of countable sequences of 0 and 1, we can define a game as follows – two players take turns naming either 0 or 1, and if the countable sequence produced is a member of S, then player I wins, and if not, then player II wins. AD says that for any game of this form, one of the two players has a winning strategy (i.e., a function from states that the game could be in on their turn to possible moves on that turn, such that for any sequence of moves the opponent could make, the eventual outcome is a win for this player).

It turns out that AD and AC are incompatible with one another, given the standard axioms of set theory. In particular, there is a standard proof (using AC) that some sets of real numbers are unmeasurable by Lebesgue measure, while AD actually entails that all sets of reals are Lebesgue measurable. (AD has all sorts of other nice consequences for sets of reals as well, which is why set theorists are interested in it. It basically avoids all the pathologies created by AC.) So mathematicians have to choose at most one of the two to accept.

Traditionally, intuitionists or constructivists have rejected AC, because it asserts the existence of a function that is not constructively given in any way. Even ordinary mathematicians realize that whenever AC is needed for a proof, the result is non-constructive. However, I think that intuitionists actually should accept AC. The reason is that an intuitionist shouldn’t accept a universal claim unless there’s a constructive (or uniform) way to prove every instance of that claim. Thus, if they accept the claim that , then it can only be because there is a constructive proof of it. But such a proof necessarily gives a function to satisfy . Thus, although AC looks like it gives non-constructive existence proofs, it only does so because one has accepted universal claims that weren’t uniformly provable – when restricted to uniform constructions, it’s just a triviality, so the intuitionist should accept it. (The intuitionist avoids the pathological choice constructions by just denying that certain collections of sets were really uniformly proven to be non-empty.)

For the classical mathematician however, who rejects the intuitionist assumptions that proofs should be constructive, this argument for AC is unavailable. Additionally, there is a sort of argument that should support AD. Recall that AD says that for any two-player game with countably many turns where the players take turns naming 0 or 1 (or generally integers – it turns out this general version is a consequence of the 0/1 version), one of the players has a winning strategy. If the variables are all understood to be restricted to {0,1}, then we can express what it means for the player I to have a winning strategy as follows:

Similarly, what it means for player II to have a winning strategy is:

If there were only finitely many quantifiers, then these would be real formulas. In fact, these formulas would simply be the negations of one another – classical mathematicians accept that is equivalent to , and vice versa. So determinacy is just a generalization of this claim to infinite sequences of quantifiers instead of finite ones, together with the assumption that for infinitely long sentences, either that sentence or its negation is true. But these are just natural generalizations of classical principles, so the classicist should accept AD rather than AC.

There are some worries of course. (Otherwise AD would be standard rather than AC!) This argument for AD looks like it should work even if the aren’t restricted to being integers – however, I’m pretty sure that the version of AD where the are allowed to be arbitrary ordinals is contradictory. Also, classical mathematicians have arguments for AC that rely on the fact that every possible set of objects exists, independently of any construction. Therefore, if there’s a bunch of elements (say, one from each of a collection of non-empty sets), then there is a set that contains exactly those elements, which is equivalent to AC.

But still, I think there’s something interesting to think about in this reversal.

Russell O'Connor(06:59:18) :Constructivists not only accept the axiom of choice, as you state it above, it is in fact provable in type theory. What is unacceptable is the classical axiom of choice in which the constructive existential is replaced by a classical existential (¬∀¬). Depending on the details of your logic, some form of the axiom of choice will imply excluded middle. One reference seems to be: Samuel Lacas, Benjamin Werner, Which Choices imply the excluded middle? (preprint 1999); however I cannot find it. 😦

Jack Woods(09:59:56) :Kenny,

Dummett makes a similar point about Choice on pp. 52-53 of his

Elements of IntuitionismKenny(11:38:40) :I figured people had made this sort of comment before about intuitionism, because I know I’ve seen some version of choice or other included in some axiomatizations of intuitionist set theory. Does anyone know if anyone has made this point before about determinacy and classical mathematics though?

Grigor Sargsyan(19:03:13) :Hi Kenny,

I think I disagree with you on mathematicians choosing AD over AC. There have been mathematicians who expressed similar views over dinner tables, but I am not sure if anyone ever wrote anything on this. At any rate, AD is not an axiom that talks about sets in general. As you mentioned full AD is not consistent with ZF-AC. Accepting AD over AC will just declare a lot of good mathematics as basically nonsense.

However, ZFC provides a good working environment for anyone, even for the people who believe in AD and only in AD. No matter what a radical AD person proves, AC person can translate that into its own system and completely understand what the AD person is saying. The other direction isn’t know to be the case. In fact, it is an open problem. Do the AD axioms form a consistency hierarchy that is as strong as the large cardinal hierarchy? Here I refer to the standard ways of making AD stronger by either looking at the Solovay sequence, or by making the games longer and etc. Recent intuitions actually hint that it might not be the case that the natural AD hierarchy goes that far. So theoretically someone in topology or analysis (I don’t want to say set theory) could prove a theorem and there will be no way to translate that into ZF+AD+something. We do not yet understand consistency strength hierarchy high up, so at this very moment there are no concrete examples of this phenomenon.