[FOM] Non-constructiveness.

[W.Taylor@math.canterbury.ac.nz]

There is a certain aspect to Non-Constructiveness", that seems to be
universally agreed on by working mathematicians, but is not encompassed
by the usual philosophies about this.   So it seems to me to be
an important subject to be adressed by the list.


In current constructivist foundations, it is generally agreed that any
true statement that has, merely in principle, a method for deciding it in a
finite number of steps, can be (in fact *is* thereby) proved constructively.
I have been told there are metatheorems to this effect, indeed.

So that if someone proved by apparently non-constructive means in PA,
that all naturals up to 10^10 were such-and-such, where such-and-such
was simply checkable on any number by a finite procedure, then this
would BE thereby constructively true. 
(This would by no means be proved to a strict ultra-finitist, OC!)


Now; there are a great many contexts where such things ARE proved
non-constructively, and all mathematicians concerned deem them almost
automatically to be non-constructive proofs; yet a logician would have
to mournfully admit that they were constructively true, that in effect
had been constructively proved, merely by virtue of being finite.

I am thinking particularly of some game-theoretic results; such as that
there must be a first-player win in Hex, ("non-constructively" proved
by a strategy-stealing argument); or that the same exists in Chomp,
by a similarly argument cleverly involving the sole corner cell.


Is there room in FoM for determining that these things ARE indeed
only proved non-constructively; by using some alternative formal
criterion of constructiveness?

------------------------------------------------------------------------------
             Bill Taylor            W.Taylor at math.canterbury.ac.nz
------------------------------------------------------------------------------
        The most disturbing game-theoretic paradox isn't
        "The Prisoner's Dilemma"  but "The Double Payment Auction".
------------------------------------------------------------------------------