[FOM] Classical/Constructive Arithmetic

[Timothy Y. Chow]

Bill Taylor <W.Taylor at math.canterbury.ac.nz> wrote:
>> Examples where the known proof is nonconstructive, and where one can give
>> a constructive proof, but all known constructive proofs are grotesque
> 
> Examples abound in game theory.  e.g. That Hex has a first-player win.

Aren't we talking about two different senses of the word "constructive" 
here?  It seems to me that the proof that Hex has a first-player win is 
"nonconstructive" only in a computational-complexity sense, not in an 
excluded-middle sense.

Tim