Dear Frank Waaldijk,
thank you for your posting on this topic.
> ---------- Forwarded message ----------
> Date: Fri, 8 Feb 2008 02:55:32 +0100
> From: Frank Waaldijk <frank.waaldijk at hetnet.nl>
> Reply-To: Foundations of Mathematics <fom at cs.nyu.edu>
> To: Foundations of Mathematics <fom at cs.nyu.edu>
> Subject: [FOM] constructive continuity 2
>
> (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.)
>
> 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.
The apparent antinomy is explained by the fact that the morphisms F:{[0,1]} ->
{R+} corresponds to the Bishop-continuous functions f:[0,1]
-> R which have positive uniform lower bound, i.e. there is c>0 with f(x)>
c for all x in [0,1], rather than those f being merely positive.
To prove this one notices that the intervall {[0,1}} is covered by
F^{-1}({(a,b) : a>0}) for a morphism F:{[0,1]} -> {R+}. As the interval is
covering compact there is a finite subcovering from which c can be extracted.
Indeed, this looks like the classical proof using the Heine-Borel theorem, but
it refers to formal cover relations, that are inductive generated, and uses the
fact that F^-1 preserves such cover relations.
Though the points of the formal topology {R+} are the positive real
numbers, it is not the same to say that F: {[0,1]} - > {R} has a
positive point function f=Pt(F) and that it factorises through the
inclusion {R+} -> {R}.
More details are found in the paper
E. Palmgren. Resolution of the uniform lower bound problem in constructive
analysis. Mathematical Logic Quarterly 54(2008), 66-69.
I hope this goes some way towards explaining some of the questions raised.
Yours sincerely,
Erik Palmgren