[FOM] Classical/Constructive Arithmetic

[Harvey Friedman]

On 3/23/06 12:15 AM, "Bill Taylor" <W.Taylor at math.canterbury.ac.nz> wrote:

> 
> ->> Examples abound in game theory.  e.g. That Hex has a first-player win.
> ->
> ->I'm afraid I have trouble with this.
> 
> So this is to say:       "For all sized boards, Hex has a 1st-player win"
> has a nice constructive proof?
> 
> That is to say, seemingly, that the usual strategy-stealing argument
> is a *constructive* proof?
> 
> Is that the opinion of the constructivists on this list?
> 

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.

Harvey Friedman