>> For example, we can define a real r as follows: >> >> r = sum from n=0 to infinity of H(n) 2^{-n} >> >> where H(n) = 1 if Turing machine number n halts on input n, >> H(n) = 0 otherwise. >> >> That's definable, but it is not computable. > >Anyhow it is not a definition.
It certainly is. It uniquely characterizes a real number, so it's a definition.
>It would be more useful to define some number by the legs >of a crowd of unicorns touching the ground at a given time.
If you would find that more useful, go ahead. When I talk about mathematical definitions, I'm really talking about definitions that are meaningful to people who understand mathematics. If you prefer to talk about unicorns, then a mathematical definition is probably not appropriate for you.