[FOM] correction to 'constructive cauchy'

[Gabriel Stolzenberg]

   I wish to make a correction to my posting, "constructive cauchy."
Nov 9, 2007.  In it, I made the following remark about the convergence
of a sequence of functions on [0,1].

>   Furthermore, on a meta-level, the claim that "point-wise = uniform"
> is a consequence of the meta-theorem that an integer-valued function
> of a real variable is locally constant.

    In a message to me, Ulrich Kohlenbach gave a natural reading of
this on which it is blatantly wrong.  (As I recall, my thinking about
this point was so sketchy that it may be more accurate to say that I
didn't even have an incorrect argument, much less a correct one.)  Even
better, he offered a correct version, which I quote:

   'The correct "metatheorem" to use to infer "pointwise->uniform" is
    the fan principle (one version of which actually is equivalent to
    the "pointwise->uniform" statement) or the closure of the system
    of reasoning one uses under the fan rule. Here one argues on the
    level of representatives which for say x\in [0,1] can be chosen
    in the compact Cantor space 2^\NN. So it is not the (uniform)
    continuity of a function [0,1]\to\NN but of a function 2^{\NN}\to\NN
    which is used.'


    Gabriel Stolzenberg