[FOM] Re: Constructive analysis

[Peter Schuster]

In response to the posting by Bas Spitters included below, I would like 
to know whether "TTE ~ BISH + CC + MP + FT" really is the whole story, 
given that, as Bas rightly mentions later on, "TTE is based on classical 
logic", and intuitionistic logic plus MP is not full classical logic. 
Perhaps TTE doesn't use all of classical logic, and that what it makes 
use of can be deduced from BISH + CC + MP + FT, say, but perhaps I am 
also wrong. 

By the way, let me mention that, similarly, INT ~ BISH + CC + FT, at 
least as either component is understood in Bridges-Richman, "Varieties 
of constructive mathematics", CUP, 1987. 

------------

Here are the relevant parts of Bas Spitters' posting: 

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