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

[Eray Ozkural]

On 4/3/06, Andrej Bauer <Andrej.Bauer at andrej.com> wrote:
> 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.

I would actually think that it should be possible to quantify how
easy it is to understand a formula. For instance, we can look
at the number of variables in the description or its length.
In this sense, wouldn't the '|x|=max(x,-x)' be the easiest to
understand?

Another, and perhaps more important, sense of easiness would
be logical depth (as in [1]). Here I mean how many logical
operations the mathematician would have to perform in his
head to understand the definition. Though this seems
impossible to know in general, I would think that this might be
understood as  how many "logical assertions" the mathematician
must make following from (general) axioms (assuming the
mathematician uses some form of a proof system in his head).

Regards,


[1] C. H. Bennett, Logical depth and physical complexity, In R.
Herken, editor, The Universal Turing Machine: A Half-Century Survey,
pp. 227--257. Oxford University Press, 1988.

--
Eray Ozkural, PhD candidate.  Comp. Sci. Dept., Bilkent University, Ankara