Dear all,
For what it's worth, a definition of division with 0/0 = 0
won't be possible constructively, because in constructive
mathematics all functions of type real->real are continuous,
and with this definition division is _not_ continuous.
Also, in IEEE 754 floating point of course division is a
total operation. One can easily imagine an "extreal" type
that is in this spirit (with "infinity" and "-infinity"
and "nan" added to the mathematical reals), where division
is total.
Finally, my PhD advisor Jan Bergstra has a theory of
something called "meadows" (related to "fields", I guess),
in which division is total. Google "bergstra meadows"
for some references :-) So that gives some legimity
to formalizing a total division function ("this is just
about meadows"). I never really looked at this work though,
and don't know whether in "meadows" one always has 1/0 = 0.
(I guess one certainly will have 0/0 = 0.)
I'm sure all these observations won't satisfy traditional
mathematicians about the treatment of divisions in systems
that only allow for total functions. Hell, it doesn't
statisfy _me_ :-)
Freek
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
