[FOM] Classical/Constructive Arithmetic

[Timothy Y. Chow]

Harvey Friedman wrote:
> On 3/23/06 12:15 AM, "Bill Taylor" <W.Taylor at math.canterbury.ac.nz> wrote:
> > So this is to say:       "For all sized boards, Hex has a 1st-player win"
> > has a nice constructive proof?
[...]
> You must mean: for all finite sized boards. Yes, using induction. The 
> induction is even with respect to bounded formulas. Note that, also, 
> bounded inductions are sufficient to prove the decidability of bounded 
> formulas.

I still think that confusion is being caused in this discussion by two 
different senses of the word "constructive."

The strategy-stealing argument is "nonconstructive" in the sense that it 
does not yield a polynomial-time algorithm for the first player to win at 
Hex.  This says nothing about whether the proof is "constructive" in the 
sense that Harvey Friedman was originally asking about.

The confusion comes partly from the oft-heard informal remark that the 
strategy-stealing argument "gives you no idea what the winning strategy 
is."  This sure sounds "nonconstructive."  In fact, however, if you are 
not concerned with *computational efficiency*, there is a trivial method 
of finding the winning strategy, namely brute-force search.  Lack of an 
*efficient* algorithm should not be confused with the lack of any 
algorithm at all, as in (for example) the problem of computing the rank of 
an elliptic curve over Q.

Tim