[FOM] continuing problems with constructive continuity?

[Frank Waaldijk]

>Bas Spitters wrote:

> The crucial observation is that in order to prove that a continuous 
> morphism
> representing a uniformly continuous function f from [0,1] to (0,1] in fact
> maps into the formal open subspace (0,1] of [0,1]. This requires (some 
> form
> of) the fan theorem. Knowing that f(x)>0 for all x in [0,1] is not enough.
> Similarly, the fan theorem is needed to prove that inf f >0.
>
> I hope that this is enough to reconstruct the answers to the rest of your
> questions.

Thank you Bas for your quick response and clarification. But to me this 
seems not enough to answer my more fundamental questions.

First: if I understand you correctly, what we have in formal topology now is 
the situation that if a morphism f from {[0,1]} to {[0,1]} has the property 
that f(x) >0 for all x, then the assertion that f is a morphism to {(0,1]} 
requires the fan theorem? [In fact this assertion is equivalent to the fan 
theorem, if taken for an arbitrary f. This follows from your explanation and 
the theorems I mentioned earlier.]

This does not strike me as a very elegant situation. It suggests immediately 
that there are two different formal subspaces of {[0,1]}, both defining 
(0,1], but not isomorphic? Or is {(0,1]} not a subspace of {[0,1]}? Not a 
definition set-up that I would care to put my money on. I really mean this.

The fundamental problem which I see is: how can there be a nice class of 
continuous morphisms if one insists on inductive covering relations? For 
this please look again at my paper [Waaldijk2005]. Because even if you 
accept this very unelegant double identity of (0,1] (and how many other 
multiple identities of other formal spaces need we define in order for 
things to `work out smoothly'...?), you have not answered my question about 
the metric on the Hilbert cube and the function k_bin^N. Are you seriously 
proposing that these functions be excluded from the class of continuous 
morphisms?

So (perhaps for the umpteenth time, I know, but I never seem to get an 
answer) why do we not simply drop the requirement of inductive coverings? We 
seem so bent on having Heine-Borel, but if so then at the same time, why 
don't we accept that the real compactness issue is an axiom which should not 
be clouded in definitions? Definitions which -in my opinion, attested to by 
the theorems in my paper- can only lead to awkwardness.

Then finally another question is why many beautiful recursive continuous 
functions are excluded from `morphism'-status in formal topology. RUSS is in 
this respect being sidelined, but not explicitly.

I do not know how to construct an answer to these questions from your 
explanation. But I was a little surprised, on reading the papers that I 
mentioned in my starting message, that these papers say they have solved the 
problems/questions I raised. If I understand you correctly, it is now 
recognized that these issues have not yet been resolved?

>From my rather distant viewpoint, I therefore do not see a significant 
improvement in formal topology over Bishop-style mathematics. The 
definitions and the language are very `formal', `logical', especially when 
contrasted to Bishop's natural style. But even what I would call the 
fundamental problem of BISH (implication of the fan theorem in the 
definition of continuous function) has as it seems to me not at all been 
resolved in formal topology.

While I'm at it, let me state that I find it difficult to believe in any 
development which hasn't invested at least as much in `general mathematics' 
as in its formal language. Where I see the core of constructive general 
mathematics actually to lie with the separable metric spaces. Maybe this 
core has some desirable add-ons in the sense of function spaces which are 
not necessarily separable, but I come across all sorts of category theory in 
formal topology, only to conclude (from my lay perspective) that even the 
situation between the real intervals [0,1] and (0,1] is unclear.

I'm sorry to sound critical here. But on the other hand, foundations of 
mathematics to me seem seldom easy to build, so one I think should take 
one's time and not disregard too quickly what Brouwer or Bishop or others 
have put forward. I personally do not see how the problems raised in my 
paper will go away, unless some careful thinking is done. I'm curious about 
what you envisage in your planned paper!

kind regards

Frank Waaldijk



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