[FOM] on andrej bauer on gs on |x| (II)
gstolzen at math.bu.edu
Sun Apr 2 17:04:32 EDT 2006
> 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
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
> 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
> 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
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,
More information about the FOM