# [FOM] continuing problems with constructive continuity?

Frank Waaldijk frank.waaldijk at hetnet.nl
Fri Feb 8 07:22:20 EST 2008

After pointing out (first in my 1996 thesis, then in a 2001 preprint, 2005
article) that the definition of  continuous function' in bishop-style
constructive mathematics practically implies the fan theorem, I have only
recently found energy to look at some developments in (constructive) formal
topology. Barring what could easily be misunderstanding on my part, I come
to the following conclusions.

In Erik Palmgren's  2003-2004 article Continuity on the real line and in
formal spaces' it is shown, in answer to my thesis/preprint, that

a) a continuous morphism from the formal reals to the formal reals
represents a Bishop-continuous function (uniformly continuous on compact
subspaces).

b) the reciprocal function x -->1/x can be represented by a continuous
morphism on the formal positive/negative reals.

c) the composition of two continuous morphisms is again a continuous
morphism

These three facts are then taken both by Palmgren as well as Peter Schuster
in his 2005 article What is continuity, constructively?' to conclude that
in formal topology the problems raised in my article are resolved. (My
interpretation of course).

This however in my eyes is an optimistic standpoint, which I can best
explain by some corollaries to my article (which hold if my interpretation
above is correct):

COROLLARY to thm. 1.3 of [Waaldijk2005]:
the following two statements are equivalent in BISH:

1) every uniformly continuous real-valued function on [0,1] can be
represented by a continuous morphism on the formal interval [0,1]
2) the fan theorem

COROLLARY to thm. 5.4 of [Waaldijk2005]
the following two statements are equivalent in BISH:
1a) the Euclidean distance function d on R^2 (the real plane, dim2) is
representable by a continuous morphism AND
1b) the (beautiful) uniformly continuous function f_bar is representable by
a continuous morphism
2) the fan theorem

COROLLARY to thm. 6.3 of [Waaldijk2005]
it cannot be shown in BISH that both
1a) the Euclidean distance function on the Hilbert cube is representable by
a continuous morphism
1b) the function k_bin^N from Cantor space to the Hilbert cube is
representable by a continuous morphism

(where for \alpha in {0,1}^N we have: k_bin(\alpha) = SUM_n 2^{-n}\alpha(n)
which is an element of [0,1], and k_bin^N(\alpha) is arrived at by seeing
\alpha as an infinite sequence (\alpha_n) of elements of {0,1}^N by a simple
coding scheme, and then letting k_bin^N(\alpha) be the infinite sequence
(k_bin(alpha_n)).

So, while the development in formal topology tackles what I termed CONT II,
III and IV, it seems to me that CONT I is neglected. The question now
becomes:

Is the class of continuous functions that are representable by a continuous
morphism sufficiently nice?

(I cannot believe that we constructivists will be content to not have a
metric on the Hilbert cube. The same holds for the summing of binary
digits.)

I would like to re-ask another question of my article, that is WHY do we
constructivists wish so much for Brouwer's Thesis (BT) and the weaker fan
theorem (FT) that we are constantly trying to arrive at definitions which
lead to the same results as these axioms, yet we do not simply dare adopt
these axioms? Is it that we are afraid of loss of face to admit that Brouwer
may after all have had a point...are we afraid of the recursive,
non-compact, non-inductive universe...or both...or what? To the layperson,
and to general classical mathematicians trying to understand constructive
mathematics, it hardly becomes clearer if we are in favor of certain axioms
but don't come out and say so and why.

Whatever the cause, in formal topology it seems to me once again the
recursive viewpoint RUSS is excluded from serious consideration. Personally
I don't understand why, if BISH really wishes to maintain that it is a
neutral common ground for CLASS, INT and RUSS.

Please excuse me for raising these questions without the energy to really
delve into formal topology which seems to me a nice idea but treated a
little complicatedly. I also might have difficulty joining discussions for
lack of time/energy, nonetheless I will be happy with replies.

(one can find my article at the link below)

Kind regards,

Frank Waaldijk
http://home.hetnet.nl/~sufra/mathematics.html

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

`