[FOM] continuing problems with constructive continuity?

[Frank Waaldijk]

I hereby really apologise for my posting, especially the last message placed 
which is in hindsight quite silly and very arrogant.

I stated that only careful thinking would make the problems with the 
reciprocal function in BISH go away, it turns out that people in formal 
topology have been doing that careful thinking, whereas I myself was quick 
to conclude there was a serious snag somewhere, even though I could not put 
my finger on it.

Kind replies trying to enlighten me have been given by Erik Palmgren, 
Giovanni Sambin and Bas Spitters. They have helped me remove the beam from 
my own eye, and now I feel very sorry to have doubted their work. I only 
wish I had known about this solution (and understood it!) when I wrote my 
article.

The only issue for me remaining (apart from feeling very foolish) is the 
position of RUSS in formal topology. There seems to be some paradigm shift 
in the position of BISH, INT, CLASS and RUSS. Seeing how little my questions 
have hit any mark, I will refrain from further silliness on my part, and not 
react on this forum.

Apologies and kind regards,

Frank Waaldijk













----- Original Message ----- 
From: "spitters" <b.spitters at cs.ru.nl>
To: "Frank Waaldijk" <frank.waaldijk at hetnet.nl>
Cc: <fom at cs.nyu.edu>
Sent: 13 February, 2008 20:31
Subject: Re: [FOM] continuing problems with constructive continuity?


> On Wednesday 13 February 2008 17:30:11 Frank Waaldijk wrote:
>> First of all, there is the formal interval {[0,1]}. The formal points x 
>> of
>> this interval for which x>0, I would call {(0,1]}, but let's for the 
>> moment
>> call it {x in {[0,1]}| x>0}. However, the assertion that there is an
>> isomorphism from this subset to what I understand to be your definition 
>> of
>> the formal interval {(0,1]}, is equivalent to the fan theorem, if I
>> understand you correctly.
>
> There is only one formal half open interval in the discussion (0,1]. Its 
> set
> of points is indeed {x in [0,1] | x>0}.
>
> The issue revolves around what is required to define a function. It is not
> enough to specify what it does on the points. One needs to work with
> opens/approximations (just is in intuitionism).
>
>> I cannot see myself explaining that to a general mathematician.
>
> Try: Johnstone - Stone spaces. These issues also come up in classical
> mathematics: locale theory.
>
>> Further you wrote:
>> >I understand that you agree that such a nice class of continuous 
>> >functions
>> >is
>> >present if one assumes the fan theorem. I hope to have explained above 
>> >how
>> >one avoids this assumption.
>>
>> My point is that without the fan theorem, you can define a class of
>> morphisms using inductive coverings, obtaining for instance
>> Bishop-continuity (uniform continuity on compact subspaces). But you 
>> cannot
>> show this class of morphisms to have enough nice properties.
>
> I disagree: it does have nice properties. I tried to explain this, but
> apparently failed to make myself clear. I am not sure where to elaborate.
>
> Best regards,
>
> Bas 


-- 
I am using the free version of SPAMfighter for private users.
It has removed 25097 spam emails to date.
Paying users do not have this message in their emails.
Get the free SPAMfighter here: http://www.spamfighter.com/len