[FOM] Re: Constructive analysis

[Giovanni Sambin]

> Ayan Mahalanobis writes:
> As I understand it (again correct me if I am wrong) BISH is more like 
> doing classical mathematics constructively ...

I am not quite sure I understand here (see also Matt Insall: "...others may do classical mathematics with constructivist methods...").

> The fundamental reason of doing 
> constructive mathematics is meaning as I understood it which is a product 
> of dissatisfaction from classical math. Then to embrace it as a guideline 
> is self-defeating to me.

Should one not use mistakes as a guideline to improve on them? What is the scientific value of the (moral?) judgement of self-defeat?

>Joseph Miller writes:
>Perhaps the constructivists should speak for themselves,

I am happy to openly declare myself as a constructivist, since at least 20 years ago. I have tried to express in a systematic way my views on constructive mathematics in the third part of my paper "Some points in formal topology" (see my page: http://www.math.unipd.it/~sambin ).
One can find there my answers to several of the questions raised here. It is not possible to just give a summary here.

>That said, I agree that Bishop is more interested in justifying old ideas

I would not judge Bishop as bound to old ideas only because he is in favour of compatibility with the classical approach. See his views in his papers "The crisis in contemporary mathematics" (Historia Mathematica 2 (1975), pp. 507-517) and  "Schizophrenia in contemporary mathematics" (Contemporary Mathematics 39 (1985), pp. 1-32)

>Andre Scedrov writes:
>"Notes on Constructive Mathematics" by Per Martin-Lof
>is a favorite of mine. 

I agree, the "Notes" have been one of the main sources of inspiration for formal topology. We plan a seminar on it here in Padua beginning next October.

>Bas Spitters writes:
>The picture that is painted there is the following:
>
>
>CLASS   INT      RUSS
>     \         |           /
>            BISH
>
>
>Where 
>CLASS is classical mathemathics
>INT is intuitionistic mathematics
>RUSS is Russian recursive constructive mathematics
>BISH is Bishop-style mathematics

One should perhaps now add intuitionistic-and-predicative mathematics (as that developed over constructive (Martin-Lof's) type theory)

Giovanni Sambin