Consider the following impartial combinatorial game, a generalization of [Chomp!](http://en.wikipedia.org/wiki/Chomp) as mentioned in the paper by [David Gale](http://www.claremontmckenna.edu/math/moneill/Math188/papers/Gale2.pdf): At each step, we have a finite partially ordered set $S$. Player I or II chooses some $s \in S$ and hands $S - S\_{\geq s}$ to Player II or I. A player wins when he gets the empty poset. The statement



> 
> For every initial partially ordered set with greatest element (and at least two elements), Player I has a winning strategy.
> 
> 
> 


has been proven by Gale using the law of the excluded middle. As far as I know, no explicit winning strategy is known. Nevertheless, I would like to ask the following (perhaps too optimistic?):


Is there any proof of the above statement, which does not use the excluded middle? Equivalently(?), is the statement valid in every topos $\mathcal{E}$?



Chomp! without the law of the excluded middle
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.


