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.
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.