[FOM] Non-constructiveness.

[Vladimir Sazonov]

W.Taylor at math.canterbury.ac.nz wrote:
> 
> 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!)


According to a not so old posting of Bill Taylor, he, as anybody 
else interested in such kind of questions, should be called 
ultra-finitist. 


> 
> 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?

I already mentioned that Troelstra and van Dalen in their two volumes 
book on constructivism are discussing some possibility for a 
strong (ultra?) constructivism where a constructive proof of 
existence of a finite object would lead to the REAL construction 
of this object. 

Let me also mention again my result that RELATIVE to an 
intuitionistic version of a (version of a ) Bounded Arithmetic 
(BA) the well-known Markov's Principle (roughly formulated as) 

(M)            not not exists => exists

is constructive iff P=NP. 

Here existential quantification is taken over finite binary strings. 
To realize plausibility of this result, note that quite feasible 
finite string 111...11 consisting of one thousand of `1' cannot be 
feasibly reached if to start from the empty string and enumerate 
all binary string in the lexicographical order. Here exponential 
complexity is the reason why the ordinary justification of M 
does not work in the framework of BA. 

Relative to HA (Heyting Arithmetic), M is constructive because 
complexity issues are ignored in HA. 

In general, to deal with the problem of "real" or feasible 
constructiveness we need corresponding theory of feasible 
objects (numbers, binary strings, hereditarily-finite sets, 
etc. BA is a good, but still too rough instrument. 

Here, like for Church Thesis, we need a formal definition 
of what is feasible constructivism to say that something is 
non-feasibly-constructive. 

Robert Black wrote in reply to the above notes of Bill Taylor: 

> I can't see anything wrong with this. (The constructive part of) PA
> obviously decides any such statement correctly. Furthermore we have a
> constructive proof that PA is consistent (Goedel/Genzen 1933) and
> thus the whole of PA only decides it one way. Thus we have a
> constructive proof that there is a constructive proof of the result,
> which of course is a constructive proof of the result. This is really
> just the basic idea of the Hilbert programme, only substituting
> 'constructive' for 'finitary'.

This is just the ordinary view on constructiveness which neglects 
the REAL feeling of mathematicians on constructivism which is, 
in fact, related with the feasibility issues. 

------------------------------------------------------------------------------
>              Bill Taylor            W.Taylor at math.canterbury.ac.nz
> --------------------------------------------------------------------------

Vladimir Sazonov

P.S. I am sorry that I did not reply to other postings 
(say, to Aatu Koskensilta). I will hardly be able to 
participate actively the nearest time.