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}$?

-
@Toby: I don't know if we really need that $S$ is finite. Gale doesn't mention this assumption, but I thought that it is necessary so that one of the two players has a strategy at all. –  Martin Brandenburg Apr 7 '12 at 18:44
Well, you don’t need the order to be finite, it’s enough if it’s upwards well-founded. –  Emil Jeřábek Apr 7 '12 at 21:47
Actually, is this really a generalization of Gale’s Chomp? As far as I can see, in Chomp the next player would be given $S\smallsetminus S_{\ge s}$ rather than $S_{\ge s}$. Then the condition to make all plays finite (and therefore for one player to have a winning strategy) is that $\le$ is a well partial order. –  Emil Jeřábek Apr 7 '12 at 21:54
In fact, the game with $S_{\ge s}$ is first-player win for the trivial reason that the player can play a maximal element. This also applies to the partial order of ideals in a noetherian ring: The game in the other question is quite different, as it only allows to add one generator to the ideal at a time. –  Emil Jeřábek Apr 7 '12 at 22:11
I agree with Emil that,in order to generalize Chomp, choosing $s$ should give the opponent the set of elements not $\geq s$. And the definition of winning should be that any player who ever chooses the least element loses. But then the game is not (as claimed in the question) always a first-player win (in classical logic). Consider the poset consisting of a least element and two larger elements that are incomparable with each other. Maybe Martin's point is that the trivial strategy in Emil's 3rd comment requires the existence of a maximal element, which isn't constructively available. –  Andreas Blass Apr 8 '12 at 1:56

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.

-

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.

-
In the spirit of the original game, I don't think that this should be accepted as a finite partially ordered set. (The set S is a subset of a finite set but is not itself a finite set. It is, a priori, only subfinite.) –  Toby Bartels Apr 7 '12 at 18:34
@Toby: You're right. If $S$ has to be finite but the partial order $\leq$ can be subfinite, then I can still deduce $(\neg u)\lor\neg\neg u$ from existence of a winning strategy, so the existence can't be proved intuitinonistically. Take $S=\{0,1\}$ and put into $\leq$ (in addition to the pairs for reflexivity) $(0,1)$ if $u$ and $(1,0)$ if $\neg u$. If Player I wins starting with 0, then $\neg u$, for $u$ would give II a good reply, 1. Similarly, if I wins with 1 then $\neg\neg u$. I don't know whether the excluded middle still follows, nor do I see what happens if $\leq$ is also finite. –  Andreas Blass Apr 7 '12 at 19:47
To save future readers the trouble of comparing various time stamps: This answer, Toby's comment, and my reply to Toby all refer to the original version of the question, before Emil edited the definition of the game to agree with the cited paper of Gale. (See the comments under the question.) –  Andreas Blass Apr 8 '12 at 12:17

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.

-
Of course, this still leaves open the case of subfinite sets (for which Andreas has proved that a winning strategy in all cases implies excluded middle) and finitely-indexed sets, as well as outright infinite sets (for which we have no proof of a strategy even classically). –  Toby Bartels Apr 7 '12 at 19:32
This is a little bit hard to digest for a practical-minded reader (who wants to win the game ...). –  Martin Brandenburg Apr 7 '12 at 19:37
If you want to win the game, then simply search through all of the possibilities. If that takes too long and you were hoping that the proof that a strategy exists would help, too bad because it doesn't. But the proof is still constructive (for the strictly finite case), because you can simply search through all of the possibilities. –  Toby Bartels Apr 9 '12 at 23:59
If you want to ensure that all sets used in the game are finite, you not only need the initial poset to be finite, but also the order relation to be decidable, right? So what happens if the initial poset is finite as in the original question, but not necessarily decidable? –  Emil Jeřábek Apr 10 '12 at 11:17
Yes, I did mean to include that but never stated it. So added to the ‘still open’ cases in my first comment under this answer is a finite poset with an arbitrary order relation. –  Toby Bartels Apr 11 '12 at 2:03