Re: [mizar] Once more: empty types

[Jesse Alama <alama@stanford.edu>]

Freek Wiedijk <freek@cs.ru.nl> writes:

> 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.

I would love MIZAR even more if types were allowed to be empty because
it would make some formalizations more natural.

What, though, are the costs?  I suppose that the developers would have
to edit a good deal of code.  But, putting that issue aside, what would
be the logical costs (if any) of allowing non-empty types?  Would there
be some familiar logical steps that wouldn't "go through" if types were
allowed to be empty?

Jesse

-- 
Jesse Alama (alama@stanford.edu)