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

[Gabriel Stolzenberg]

   This is the first part of my reply to Andrej Bauer's reply (Apr 3)
to my "on adrej bauer on gs on |x| (II)" (Apr 2).

On Mon, 3 Apr 2006, Andrej Bauer wrote:

> 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 :-)

   I agree.  (I should have anticipated such a misunderstanding.)

> 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.

   Sometimes.  But much less often than you might think.  And not
in this case.  If I'd been preoccupied with constructions, I would
have proceeded in a very different way.  For my analysis course,
the over-riding concerns were not constructions but naturality and
incisiveness.  (E.g., don't carry around excess baggage and don't
make things more complicated than they need to be.)  And if I had
thought the classical approach (on which I grew up and then taught),
I would have happily used it.

   In keeping with these concerns, I wanted to have the reals emerge
from the rationals, just as the rationals do from the integers and
the integers from the natural numbers.  Evidently, you don't care much
about this.  (You have other priorities.)

   To be continued.

   With best regards,

     Gabriel