# [FOM] continuing problems with constructive continuity?

Frank Waaldijk frank.waaldijk at hetnet.nl
Tue Feb 12 18:59:38 EST 2008

```>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

```