FOM: Effective Bounds in Core Mathematics

[Fred Richman]

Martin Davis wrote:
 
> Fred Richman wrote:
 
> >An analysis of a classical proof of P
> >might reveal a constructive proof of a classically equivalent theorem
> >Q. The constructivist would maintain that Q is what had been proved,
> >not P.  ... the constructivist ...  is simply interested in finer
> >distinctions than the classical mathematician wishes to make.
 
> As stated this is surely not true. The non-constructivist makes the
> very same distinction, but expresses it in different words. Instead of
> saying:
 
>     P has not been proved, the proof only shows Q
 
> the non-constructivist would say
 
>     P has been proved, but non-constructively
 
> Where is there greater fineness of distinction?

The nonconstructivist makes no distinction between P and Q. Actually,
I think that "in his heart, he makes a distinction," but, officially,
P and Q are (often) trivially equivalent in his eyes. For a
constructivist the distinction is reflected in the mathematics itself:
there is no theorem that P is equivalent to Q. The nonconstructivist
can refer to this distinction only indirectly, in the metamathematics
as it were. I think that this internalization of constructivity into
the mathematics, with no loss of classical content, is what makes
constructive mathematics attractive.

> If the constructivist is of the Bishop variety, the tendency will be
> to replace P by P* that can be proved constructively because a
? stronger hypothesis has been built in, e.g., classical continuity
> replaced by uniform effective continuity. With the redefinition, P*
> written in English may even use exactly the same words as P. Is this
> making finer distinctions or a form of obfuscation?

I think that Bishop's decision to use the word "continuity" to mean
uniform continuity (on compact spaces) was misguided. I don't do that.
But one should note that he did it only on compact spaces, where the
two notions are classically equivalent. 

I'd also like to emphasize that Bishop, and other constructivists of
his ilk, talk about uniform continuity, not "uniform effective
continuity". There is a tendency to think that constructive
mathematicians are not playing with a full deck, that their
quantifiers range over restricted classes such as "the constructive
real numbers". This distorts the classical content of the theorems of
constructive mathematics, and makes them much less interesting. I
understand why a classical mathematician would look at constructive
mathematics in this way. However, this view fails to explain why the
theorems of constructive mathematics are true when interpreted
classically. I think that it is more accurate to say that constructive
mathematicians and classical mathematicians are talking about the same
things.

--Fred