[FOM] a very exciting claim

[Andrej Bauer]

On Wednesday 22 March 2006 14:36, Eray Ozkural wrote:
> Excuse my ignorance. Is this also why in many definitions, the
> properties relating to an object of type X, P1, P2, .., PN are given, and
> there is an additional property that says "No other object is X"? I am
> just trying to understand, because (naively) if I give an
> algorithm that enumerates all X, there is no need to make the claim
> of negating the rest. Can you please expand on these claims a little
> further?

I think you are referring to inductive defnitions, for example when we define 
a well-formed formula X to be a string of symbols following some rules 
P1, ..., Pn on how to make new formulas. Books in logic like to add "and no 
other string is a well-formed formula".

This is just a clumsy way of explaining inductive definitions. There are many 
better ways of doing it: to programmers explain them using inductive 
datatypes or grammars, to logicians explain them with 
introduction/elimination rules or induction principles, to mathematicians 
explain them with free algebras.

I am somewhat surprised at what Gabriel is saying:
> Finally, some things are shorter and nicer in a constructive
> mindset yet disturb the classical mind.  E.g., the definition of
> |x|.  Constructively: x if x is at least 0, -x if x is at most 0.
> Period. But a classical mathematical can't stop there.  He feels a need
> to say that |x| is defined for all x.  On the other hand, in a
> constructive mindset, one does not feel such a need.  Nothing is
> missing.

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, 
then you should first prove a pasting lemma which says that you can paste 
together f_1 : (-infinity, 0] --> R and f_2 : [0, infinity) into f : R --> R, 
provided they agree at 0. Classically this is rather easy since

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

But constructively the above equation cannot be proved, so you need to worry 
_more_. 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 personally prefer the definition |x| = max(-x,x), where max comes from a 
proof that (R, <=) is a lattice.

Andrej