[FOM] Re: Constructive analysis

Bas Spitters bass at sci.kun.nl
Tue Sep 10 05:17:03 EDT 2002

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 

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.


More information about the FOM mailing list