[FOM] Re: Constructive analysis
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
More information about the FOM