[FOM] on andrej bauer on gs on |x| (I)

[Gabriel Stolzenberg]

Dear Andrej,

> I am somewhat surprised at what Gabriel is saying:

   I understand.  It's misleading.  I suppose it would have been
clearer if I had used instead something like '1 for x > 0, 0 for
x = 0 and -1 for x < 0.'  Let me try to sort things out.  Some
of the issues are kind of interesting.

   As I recall, I was imagining a classical mathematician defining a
function the way I said (by cases) and a constructive mathematician
observing him.  Forget for the moment that it's |x|.  It is what it
is.  Is it everywhere defined?  At this stage, the constructivist
doesn't care.  He sees a function defined for both nonnegative and
nonpositive numbers.  Period.

   But, as we know, the classical mathematician does care.  To him,
it is obvious from the form of the definition that the function is
everywhere defined and it would be perverse not to say so.  (It's
not that, at this moment, he can point to any place where he will
need this.  He's not thinking in pragmatic terms.)  However, the
constructivist doesn't see that this appeal to LEM adds anything
helpful.

   Now, if the constructivist is not merely heckling his classical
colleague, he has his own elegant way of dealing with |x| (and not
only with it).  Reals can be defined as families of closed rational
intervals, every pair of which intersect and among which are ones of
arbitrarily small length.  |x| can be defined as the set of all |I|,
for I in x.  So, in order to make this work, we must first define
|I| for a rational interval, I = [r,s].  For reasons I won't go into
here, we would like it to be the smallest interval that contains all
|t| for t in I.  I'll leave its definition as an exercise.

   (Another nice way to proceed is to extend the uniformly continuous
function, |r|, from Q to R.  If we don't do this, then we must later
prove that |x| is uniformly continuous.)

   To be continued.

   With best regards,

      Gabriel