Choice and Determinacy

15 11 2007

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 \forall (x\in S)\exists y(y\in x) then \exists f\forall (x\in S)(f(x)\in x). 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 \forall (x\in S)\exists y(y\in x), then it can only be because there is a constructive proof of it. But such a proof necessarily gives a function to satisfy \exists f\forall (x\in S)(f(x)\in x). 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 x_i 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:

\exists x_1 \forall x_2 \exists x_3 \forall x_4 \dots (x_1 x_2 x_3 x_4 \dots)\in S

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

\forall x_1 \exists x_2 \forall x_3 \exists x_4 \dots (x_1 x_2 x_3 x_4 \dots)\not\in S

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 \lnot\forall is equivalent to \exists\lnot, 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 x_i aren’t restricted to being integers – however, I’m pretty sure that the version of AD where the x_i 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.