[FOM] Re: Constructive analysis

[Harvey Friedman]

>As I understand it (again correct me if I am wrong) BISH is more like
>doing classical mathematics constructively and I sometime wonder why would
>a constructivist be interested in that. 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.
>
>--Ayan
>

I got interested in BISH (Bishop style constructive analysis) and
wrote this many years ago:

Set Theoretic Foundations for Constructive Analysis, Annals of
Mathematics, Vol. 105, (1977), pp. 1-28.

As an intuitionist you can think of BISH as lawlike analysis. (I
think the term "lawlike" is due to Brouwer).

As an f.o.m. researcher, you can view BISH as a way of doing analysis
that has a great deal of pragmatic coherence, in that normally one
can easily tell in a mathematical friendly way whether one has
conformed to BISH. Thus BISH is easily coherent enough to merit
foundational investigation. Hence my interest in writing that paper.
What I found particularly interesting is the wealth of
metamathematical information about such formalizations, that
guarantee that certain algorithmic properties must hold if one
conforms to BISH.