FOM: Effective Bounds in Core Mathematics

[Martin Davis]

At 03:55 PM 6/27/00 -0400, 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?

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?





                           Martin Davis
                    Visiting Scholar UC Berkeley
                      Professor Emeritus, NYU
                          martin at eipye.com
                          (Add 1 and get 0)
                        http://www.eipye.com