[mizar] Once more: empty types

[Freek Wiedijk <freek@cs.ru.nl>]

Hi,

We've had this topic many times before, but I would like
to bring it up once more: empty types in Mizar.

The reason is that I met Adam Naumowicz and Artur Kornilowicz
at the MathWiki workshop in Edinburgh, and that it then
became clear to me that both of them didn't see the point
of allowing empty types.  Particularly Artur though that
having "permissive" mode definitions should be good enough
for me and that I should not be so difficult.

Before, I thought that it was just Andrzej that I couldn't
convince that Mizar is much worse for not having empty types.
But now I found out that it's _me_ that seems to be the
exception.

So is there _anyone_ on this list that understands that it's
_much_ more natural (and therefore leads to much better
formalizations) if you are allowed to have types that can
be empty?

One of my main arguments (I've said it before, but let's
say it once more) is that one should be able to have:

  for a,X being set holds a in X iff a is Element of X

For _any_ set X, not just for non-empty sets.  (In fact
I think the reason that there so many "non empty set"
reservations in MML is exactly because of the fact that this
equivalence is not possible.  If you in the current system
write "Element of X", you don't get the correct meaning when
X is empty.  So then one has to reserve X to be non empty,
to be able to prove the results.  While if "Element of X"
had the _right_ meaning, then X could have ben any set.)

Anyway, I know it's probably useless posting this, but I
wanted to give it one more try.

So to know whether there's _anyone_ like me here: please
reply to this if you agree with me that it is crazy that
Mizar forbids empty types and that it would be a much better
system if it did not.

Freek