[FOM] Re: Constructive analysis (Correction)
bass at sci.kun.nl
Thu Sep 12 14:04:44 EDT 2002
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.
More information about the FOM