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

[Gabriel Stolzenberg]

   To continue.

> Irrespective of whether you're classical or constructive, if you want
> to define absolute value as a function R --> R in the way you suggest
> above,

   Andrej, as I pointed out above, this is not at all the way I would do
it.  (I apologize for writing in a way that makes it seem that it is.)

> then you should first prove a pasting lemma

   I don't agree.  Even if someone paid me to proceed in this way,
I wouldn't seek such a pasting lemma.  I would just make the trivial
estimates needed to establish uniform continuity and extend.  (Your
pasting is just about functions, right?)

>  R = (-infinity, 0] union [0, infinity)

> But constructively the above equation cannot be proved, so you need
> to worry _more_.

   I don't need to worry _at all_ because I wouldn't take such an
unhappy approach.

>  I do not find it self-evident at all (with my constructive hat on)
> that the above definition of |x| defines a function for all real x (I
> know it does).

> Or to put it another way, suppose you define |x| as you said:

>  if x <= 0 then |x| = -x,
>  if x >= 0 then |x| = x.

>  Why is |x| defined for all x, constructively?

   I didn't say it was, certainly not on that definition.  But see
above.

> I personally prefer the definition |x| = max(-x,x), where max comes
> from a proof that (R, <=) is a lattice.

   I used to agree with you but I no longer do.  My reason is that
if you go back to the level of rational intervals, max(I,-I) is, in
general, bigger than |I|.  Here, max(I,-I) is the smallest interval
that contains all max(r,-s) for r and s in I and, as I noted above,
|I| is the smallest one that contains all |r| for r in I.  (These
are not definitions, just properties.  The definitions are in terms
of endpoints.)

   Not only the definitions of |I| and max(I,-I) (and, in terms
of them, of |x| and max(x,-x)), but also the definitions of the
arithmetic operations (first on rational intervals, then on reals)
satisfy a smallest interval condition and, in this sense, can be
thought of as answers to natural questions.

   If you want to see more, check out chapter 1 of my "new course
of analysis" at http://math.bu.edu/people/nk/xyz/.  (It's not a
book.  It's not even course notes.)


   With best regards,

      Gabriel