Thanks for the answer. From what I understand, ACA_0+Kruskal's theorem actually shows small Veblen ordinal well-founded, so its PTO would have to be strictly higher. I haven't read whole paper, so I might be wrong.

Yes, you are right. I actually had induction up to $\epsilon_0$ in mind. I edited the question.

Before I couldn't find the outline, but now, when I looked it up with "Kritchman-Raz" keyword, I was able to find it. Thanks!

Ahh, right. A subset of size $\omega_1$ doesn't do anything when we add Cohen reals. Thanks.

Now I can see that your idea can be made into an explicit example of the game. Thanks!

Yes, games can be played on any set, and can also have transfinite length.

@JoelDavidHamkins As far as I can understand, your game isn't really explicit, because it either requires the existence of a family without choice function, or existence of specific choice function for some family. In either case, it doesn't fit my definition of "explicit".

@AsafKaragila I know this example cannot be made more constructive, but maybe we can use other means to get such a game.