[FOM] Re: Constructive analysis

[Bas Spitters]

On Thursday 05 September 2002 20:37, Ayan Mahalanobis wrote:
> On Thu, 5 Sep 2002, Bas Spitters wrote:
>
> I don't like your interpretation that BISH is the common core of INT RUSS
> ... because whatever one can prove in BISH is simultaneously proved in
> INT.
> You know better than me on this topic, so correct me if I am wrong, the
> spirit of BISH is completely different than that of INT and  they have very
> little common interaction except in meta theory.

As I understand it, Bishop's idea was to do intuitionistic mathematics without 
having to bother about the underlying philosophy, thus focussing on the 
mathematics.
Bishop did aknowledge the value of Brouwer's insights such as the continuity 
theorem and the fan-theorem, but he viewed them as meta-theorems about a 
possible formalization of BISH. In his `numerical language' article he 
explains this, and mentions that these ideas are implicite in Brouwer's 
writing.
See Troelstra and van Dalen or Beeson for technical results on these 
meta-theorems.

Bishop's insight was that one can avoid using the intuitionistic principles by 
considering apparently restricted cases (e.g. only consider uniformly 
continuous functions).

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

Please see Joseph Miller's Calculus example for this one.

Bas