[FOM] constructive continuity 2

[Frank Waaldijk]

(For the moderator: this message is posted here because the issues below 
seem to me of importance to the foundations of constructive mathematics, and 
I would like to draw attention and reactions to these issues.)

Formal topology is quoted in several places to be a constructive way of 
doing topology, in which the absence of the fan theorem can be compensated 
by the use of inductively defined covering relations on the basic opens of a 
formal space. It is, to freely quote Giovanni Sambin, a quickly developing 
field, in which several different approaches are tried out.

On rereading Erik Palmgren's article `Continuity on the real line and in 
formal spaces' (see http://www.math.uu.se/~palmgren/crealform-rvd2.pdf), I 
find it difficult to reconcile its results with a theorem in my paper `On 
the foundations of constructive mathematics-especially in relation to the 
theory of continuous functions'.

Since the basic definitions regarding formal topology seem to vary, I think 
it not unlikely that this is a definitional matter. Perhaps someone 
well-versed in formal topology could help me understand where the trouble 
lies? This might help in improving my understanding and/or the 
definitions...

The reason for this question is (as in my first message) that the results of 
Palmgren's paper are quoted both in the paper itself and in Peter Schuster's 
paper `What is continuity, constructively?' to be a solution to the problems 
raised in my paper above.

In Erik Palmgren's paper:

Theorem 4.1 states that every Bishop-continuous function from R to R is 
representable by a continuous mapping A_f from {R} to {R} (where I use {R} 
to denote the formal real line)

Theorem 4.6 states in effect the converse: every continuous mapping from {R} 
to {R} represents a Bishop-continuous function from R to R.

Lemma 5.2 is used to show that the reciprocal function x-->1/x is 
representable by a continuous mapping, say Z.

Proposition 3.3 is used in stating that the composition of continuous 
mappings is a continuous mapping.


Now my problem:
Surely Thm 4.1 means that every Bishop-continuous function from [0,1] to R 
is representable by a continuous mapping?

But Corollary 4.4 of my paper above (which I refer to as [Waaldijk2005]) 
states:

In BISH the following statements are equivalent:
1) The fan theorem
2) If f is a Bishop-continuous function from [0,1] to R+, then the 
composition 1/f of  f with the function x-->1/x is again Bishop-continuous

Combining the results we find (?)

If f is a Bishop-continuous function from [0,1] to R+, then A_f is a 
continuous mapping from the formal interval {[0,1]} to {R}+ (Thm 4.1 
Palmgren). Then the composition of A_f with the reciprocal mapping Z 
(representing x-->1/x) is again a continuous mapping (by Lemma 5.2 and Prp. 
3.3 Palmgren), say W from {[0,1]} to {R}+. Then W represents the function 
1/f which (by Thm 4.6 Palmgren) is Bishop-continuous.

Therefore (by Crl. 4.4 Waaldijk) the fan theorem holds.

I cannot pinpoint the reason for this unexpected derivation of the fan 
theorem, but I suspect that it lies somewhere in the definitions involved in 
creating the mapping Z representing the reciprocal function x-->1/x. Or 
perhaps there is some unforeseen difficulty in moving from {R} to the formal 
interval {[0,1]}? In both cases this seems to me to warrant some further 
thinking.

All elucidation and likely correction of some oversight on my part are 
welcome.

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









 


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