# [FOM] correction to 'constructive cauchy'

Gabriel Stolzenberg gstolzen at math.bu.edu
Wed Jan 30 12:56:10 EST 2008

   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