[FOM] Classical/Constructive Arithmetic

[hendrik@topoi.pooq.com]

On Thu, Mar 23, 2006 at 05:15:04PM +1200, Bill Taylor wrote:
> 
> 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?

The game tree for hex is finite, and there are no draws.  Therefore it 
is a win for someone.  In other words, for this game it is easy to prove 
that it is a win for the first player or a win for the second player (by 
induction packwards from the end of the game, for example.)

Given (p or q) and (not q), it *is* constructive to deduce p.
What's not constructive is to assume that (p or not p) for arbitrary p.

-- hendrik.