I gave this paper a pretty thorough read-through, and decided that the best way to really see what was going on would be to write it all down, expanding the most interesting arguments and collapsing others. This has been my main strategy for learning math for a while now, but I just decided recently that I ought to start a blog for this kind of thing. Although I wrote this post mainly for myself, it might be helpful for anyone else who’s interested in reading the paper.
Towards the end, I note that the result can be made “constructive”, in the sense of avoiding the Axiom of Choice by absoluteness arguments. Basically by Shoenfield’s absoluteness theorem, but I went through the argument by hand because I was not aware of that theorem until I went to Wikipedia to find something to link for absoluteness.
Note that there’s a second sense in which the argument is nonconstructive: Kakutani requires as a hypothesis that the space be compact. In your post you say [0, 1]^{\omega} is compact by Tychonoff’s theorem, but using Tychonoff’s theorem in its general form here is a use of choice. For compact Hausdorff spaces it’s enough to use the ultrafilter lemma, but I believe you can just prove by hand that [0, 1]^{\omega} is compact in ZF.
(1) The absoluteness argument shows that intermediate uses of Choice don’t matter. They happen (definably) in L, and the conclusion reflects back up to V.
(2) As you suspect, you don’t really need Choice for compactness of the Hilbert cube. Given a sequence in it, I can define a convergent subsequence by repeatedly pigeonholing infinitely many points into finitely many holes. I believe sequential compactness is what is needed for the Kakutani theorem.
Variants of open cover compactness are derivable from sequential compactness without Choice in Polish spaces, in case something like that is needed. Or if you somehow really need full open cover compactness… well, return to point (1), I guess.
I gave this paper a pretty thorough read-through, and decided that the best way to really see what was going on would be to write it all down, expanding the most interesting arguments and collapsing others. This has been my main strategy for learning math for a while now, but I just decided recently that I ought to start a blog for this kind of thing. Although I wrote this post mainly for myself, it might be helpful for anyone else who’s interested in reading the paper.
Towards the end, I note that the result can be made “constructive”, in the sense of avoiding the Axiom of Choice by absoluteness arguments. Basically by Shoenfield’s absoluteness theorem, but I went through the argument by hand because I was not aware of that theorem until I went to Wikipedia to find something to link for absoluteness.
Note that there’s a second sense in which the argument is nonconstructive: Kakutani requires as a hypothesis that the space be compact. In your post you say [0, 1]^{\omega} is compact by Tychonoff’s theorem, but using Tychonoff’s theorem in its general form here is a use of choice. For compact Hausdorff spaces it’s enough to use the ultrafilter lemma, but I believe you can just prove by hand that [0, 1]^{\omega} is compact in ZF.
I’m glad you bring this up. I have two comments:
(1) The absoluteness argument shows that intermediate uses of Choice don’t matter. They happen (definably) in L, and the conclusion reflects back up to V.
(2) As you suspect, you don’t really need Choice for compactness of the Hilbert cube. Given a sequence in it, I can define a convergent subsequence by repeatedly pigeonholing infinitely many points into finitely many holes. I believe sequential compactness is what is needed for the Kakutani theorem.
Variants of open cover compactness are derivable from sequential compactness without Choice in Polish spaces, in case something like that is needed. Or if you somehow really need full open cover compactness… well, return to point (1), I guess.