[FOM] Re: Constructive analysis
Peter Schuster
Peter.Schuster at mathematik.uni-muenchen.de
Mon Sep 9 08:30:46 EDT 2002
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.
More information about the FOM
mailing list