FOM: Re: constructive mathematics

[Ayan Mahalanobis]

I don't think I am competent enough to comment on the works of Heyting of
Frege. The comment of Jeffrey has a hint of confusion which is shared by a
lot of working mathematicians and philosophers, so I elaborate a little.

On my comment I explicitly mentioned Bishop's mathematics, not Brouwer's
Intuitionism as constructive mathematics. The two things are different in
their approach and in the theorems they obtain.

Constructive mathematics i.e. Bishop's mathematics is seen as working with
Intuitionistic logic, a confusion may be as this logic is abstracted from
Intuitionism, hence it has all the essence of Intuitionism. Unfortunately or
fortunately this is not the case, for a working constructive mathematician
Intuitionism means adding two more axioms to Bishop's mathematics.

1) Fan theorem which is classically true.
2) Brouwer's continuity theorem.

A consequence of the second theorem is, "every real valued total function
defined on a separable metric space is sequentially continuous".
Probably this continuity theorem was the major concern/interest for most of
the mathematicians and philosophers. Then there was free choice sequence on
which this continuity theorem was used.

But in Bishop's mathematics neither of these axioms are accepted and nor are
the sequences free choice sequences. Any theorem proved in Bishop's
mathematics is a theorem ( the same proof goes along) in Brouwer's
Intuitionism and Classical mathematics. Since Classical mathematics is a
model (informally speaking) of Bishop's mathematics hence my claim is
Bishop's mathematics can't have any subjectivism..

Best,
Ayan.

Ps: For further information please see "Varieties of Constructive
Mathematics"  Bridges-Richman. Cambridge University Press.