[FOM] constructive continuity 2
Frank Waaldijk
frank.waaldijk at hetnet.nl
Thu Feb 7 20:55:32 EST 2008
(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
More information about the FOM
mailing list