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

[Andrej Bauer]

Dear Gabriel,

I did indeed misunderstand what you wrote as a claim that your definition

  1) if x <= 0 then |x| = -x
  2) if x >= 0 then |x| = x

is a valid definition of |x| for _all_ real x. I think it was not only my 
fault :-)

You have further commented that you used to prefer the definition |x| = 
max(-x,x), but now you prefer to define the absolute value via rational 
intervals. I would like to comment on that.

It is in the constructive mindset (pun intended, I always intend all the puns) 
to preoccupy oneself with constructions. Thus, for example, you have a 
particular construction of the reals set in your mind: a real is a certain 
set of rational intervals. To this I would say that it is methodologically 
better to keep things as _algebraic_ and _abstract_ as possible, without 
going overboard on the "abstract" part. Too many sets and sequences of things 
can be hard on one's mind.

Thus, for example, instead of working with a particular construction of reals, 
I would say it is better to work axiomatically from the axioms of an ordered 
field with suitable additional properties (Archimedean axiom + completeness). 
>From this point of view, it is more reasonable to define |x| via a pasting 
lemma which uses only the axiomatized structure of the ordered field. This 
often leads to slick proofs.

Let me give an example. In defining |x| I would prefer to avoid any talk of 
the absolute value of an interval (unless my interest was in computation with 
intervals for the sake of intervals), and I would do it as follows. First, 
given two functions

  f : (-infinity, 0] --> R
  g :  [0, infinity) --> R

we may paste them together into h : R --> R by the formula

 h(x) = f(min(x,0)) + g(max(0,x)) - (f(0) + g(0))/2

If g and f are continuous then so is h, obviously since h is just a 
composition of continuous functions (even uniformly continuous if f and g are 
such). Furthermore, if f(0)= g(0) then h is a continuous extension of both f 
and g.

The idea behind the definition of h is of course that (-infinity,0] and 
[0,infinity) are both retracts of R.

Now define |x| as the pasting of the functions f(x) = -x and g(x) = x. The 
formula for h in this case simplifies to |x| = min(x,0) + max(0,x).

I find the above construction cleaner and easier to understand (once you draw 
a picture of what f(min(x,0)) looks like) than any definition that goes back 
to a particular construction of R. It also teaches us about the importance of 
retracts.

If you like "reals as interval", for thought provking reading I recommend Paul 
Taylor's http://www.cs.man.ac.uk/~pt/ASD/analysis.html#ASD/intawi

Best regards,

Andrej