Re: [mizar] weak types

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Freek Wiedijk wrote:

> I see.  I still don't like it.  Talking about 1/0, it's
> nonsense.  1/0 is not 0, it is not some unknown real number,
> it is _illegal._
>

To be a bit more precise, x/y is defined as x*y", so breaking the permissiveness
we rather put 0" = 0 (it is not original, I owe the information, that this works
pretty well in HOL, to John Harrison; and John has shown me a book of a British
algebraist, sorry I do no remember the name, that observed that nobody knows why
mathematician do not allow division by zero).
I do not know what you mean by _illegal_ (I am not kidding, there are few
different meanings of it). The problem is of course what to do with
      x/y
if we either do not know if y (maybe a complicated term) is zero, or if it is
hard to prove, or ....

Let us think about an experiment. Let we introduce
   fd(x,y)       fd - funny division
with the meaning as it is in MML, and x/y in your meaning (Michael Kohlhase has
nothing against our x/y, but claims that we should use a different notation).

Then we will see which functor the authors would prefer. It is difficult to
forecast the result, but I believe that (most of)
the authors would prefer the functor that is easier to use, i.e. fd(x,y)

>
> By the way, by now you all know my dislike of only non-empty
> types because of "Element of".  But _if_ empty types are
> forbidden, I think that "Element of X" should have had a
> guard "X is non empty set".

Originally it had. When we broke the permissiveness, putting Element of {} equal
to {} some theorems then got simplified. Again, if you like you may go back to
the original definition:

   let X be set;
   assume
Z: X is non empty;
   mode element of X means it in X;
   existence by Z;

I think that using 'element of ...' defined above instead of 'Element of ...' is
a sort of masochism. But maybe it is more honest way to cope with the problem.

Andrzej