[FOM] Re: Constructive analysis (Correction)

[Bas Spitters]

12-9-2002 11:21:06, Bas Spitters <spitters at cs.kun.nl> wrote:

A correction on my previous post:

>> The second axiom, SE, is the axiom of not-not stable equality, i.e.,
>> for any set A, and all x, y in A,
>>
>>                      (not (not (x = y)) ==> x = y
>
>This follows from Markov's principle (MP) if the apartness is Sigma01, which 
>is usually the case in analysis. So SE does not seem to be needed.

In case the apartness is Sigma01, even MP is not needed here, SE can be proved in BISH.

Sorry,

Bas