Chomp! without the law of the excluded middle Consider the following impartial combinatorial game, a generalization of Chomp! as mentioned in the paper by David Gale: 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}$?
 A: I don't think that there is anything interesting about this constructively, as long as we limit ourselves to finite sets in the strictest sense.  The proof that a winning strategy exists gives us no help in finding the strategy, so in this sense it is nonconstructive, but we never needed help in finding a strategy.  Only finitely many moves are possible, with only finitely many options for each move, so all that we ever had to do to find a winning strategy (if one exists) is to enumerate all of the possibilities.  Practically, this is impossible, so it would be nice if an existence proof for such a strategy would shorten the search, but this is a separate issue from the acceptability of the proof for constructive mathematics.  Put another way, we can already prove constructively, since there are only finitely many possible plays of the game, that one player or the other must have a winning strategy, so any proof that relies on this is still constructive.
A: 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.
A: I think the assertion that Player I has a winning strategy implies (in intuitionistic type theory) the law of the excluded middle.  To see this, let $u$ be an arbitrary truth value and let $S$ be the subset of $\{0,1\}$ that definitely contains 0 and, in addition, contains 1 with truth value $u$.  The ordering is the usual one: $0<1$.  Suppose $\sigma$ is a winning strategy for Player I.  What it tells him to do on his first move must be to choose 0 or to choose 1, because every member of $S$ is 0 or 1.
If it says to choose 1, then, in order for it to be a strategy at all, we must have $1\in S$, which means $u$.
If it says to choose 0, then we must have $\neg(1\in S)$, for if $1\in S$ then Player II could choose 1 and win.  So we must have $\neg u$.
Therefore, $u\lor\neg u$, and, since $u$ was an arbitrary truth value, we have the law of the excluded middle.
