# [FOM] constructive continuity 2

Erik Palmgren palmgren at math.uu.se
Wed Feb 13 18:19:30 EST 2008

```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
```