[FOM] continuing problems with constructive continuity?

[Frank Waaldijk]

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