This is an attempt to answer the question, as revised by Emil to agree with Gale's theorem, assuming that the poset $S$ is finite (which I take to mean K-finite, equivalently a surjective image of $\{0,1,\dots,n-1\}$ for some natural number $n$). I do not require the order-relation or even the equality relation on $S$ to be decidable. To summarize the game (in a form with less mention of sets): The players take turns naming elements of $S$, subject to the constraint that one cannot name an element that is $\geq$ a previously named element. A player wins iff his opponent names the least element of $S$. I claim that the existence of a winning strategy for Player I in this game implies, in intuitionistic type theory (the internal logic of topoi) the principle $(\neg u)\lor(\neg\neg u)$. In particular, since this principle is not intuitionistically valid, the existence of a winning strategy for Player I is not intuitionistically provable.

To verify the claim, consider an arbitrary truth value $u$, and define $S$ to be the poset whose members are 0,1,$a$,and $b$, all of which are distinct except that $a=b$ with truth value $u$. The ordering relation is as follows: 0 is the least element (i.e., it is $\leq$ everything), 1 is the greatest element, and (of course) every element is $\leq$ itself. In particular, $a\leq b$ iff $b\leq a$ iff $u$. Suppose Player I has a winning strategy on this poset, and consider the first move prescribed by this strategy. It can't be 0, as that loses. If it is 1, then we must have $\neg u$, because $u$ implies that $a$ is a winning reply for Player II. If, on the other hand, the strategy's opening move is $a$ (the case of $b$ being symmetrical), then we must have $\neg\neg u$, because $\neg u$ would make $b$ a winning reply for Player II. Since Player I's opening move must be among 0, 1, $a$, and $b$, we have $(\neg u)\lor(\neg\neg u)$ in all cases.