[FOM] Re: Constructive analysis

[Bas Spitters]

Dear Steve,


May I suggest to look at:
Bridges & Richman, "Varieties of constructive mathematics"
to start with.


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


So BISH is the common core.


The books suggested by the other participants of this list fall into either 
RUSS (B.A. Kushner)
or TTE (M.Pour-El,J. Richards, Weihrauch)
Where TTE is Weihrauch's system.


In fact, RUSS ~ BISH + CT + MP.
[ CT is Church's thesis, MP is Markov's thesis]


Similarly, TTE ~ BISH + CC + MP +FT.
[ CC is continuous choice, FT is the fan "theorem"]


Both of these similarities should be understood by a realizability 
interpretation. Since TTE is based on classical logic, the interpretation is 
not complete, but it is still a very convenient way to understand large parts 
of the theory.


Bas Spitters


-------------------------------------------------------
Department of Computer Science, University of Nijmegen.
P.O.box 9010, NL-6500 GL Nijmegen, The Netherlands.
e-mail: spitters at cs.kun.nl  Phone: +31-24-3652610.