[FOM] Classical/Constructive Arithmetic
hendrik at topoi.pooq.com
Fri Mar 24 09:18:05 EST 2006
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.
More information about the FOM