[FOM] Re: Constructive analysis

[Bas Spitters]

On Monday 09 September 2002 12:30, Peter Schuster wrote:
> 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.

As I see it the situation is as follows. Typically, in TTE one takes a 
classical theorem and tries to understand its computational meaning.

Suppose that the theorem is: 
  If x is A and x is B, then x is C         (*).
One could try to prove: 
  If x is effectively A and x is effectively B, then x is effectively C.

I conjecture that when (*) is provable in BISH + CC + MP + FT such statements 
can usually be proved using a (variant of) Kleene's realizability 
interpretation. Some results have been obtained by Andrej Bauer and Peter 
Lietz.

One could also try to prove:
If x is A and  x is effectively B, then x is effectively C.
In this case, the realizability interpretation will not be directly 
applicable, but sometimes the ideas behind this interpretation can still be 
of use.

Bas