Re: [mizar] Once more: empty types

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

Hi Adam,

>Our discussion with Freek in Edinburgh, which actually
>revived this topic, also shows that no one here tries
>to avoid discussion ;-)

Both of you looked quite uneasy about it though :-)  But
I really appreciate it that you reply to my message now.

>To me, the point is that since Mizar types are not just
>syntactic replacement for respective predicates,

Sure.  But why not try to get it as close as possible,
semantically?

>allowing empty types would need more tweaking with the
>code than just requiring 'by' after every 'consider'.

Of course.  I never denied that.  But I think that it's
worth it, to get a much more elegant world.

Mizar still _could_ be "backward compatible", in the sense
that as long as you prove all the clusters and existence
correctness conditions and everything, the system would
behave in the same way as it always behaved.

>And I don't agree that empty types make formalization
>"much more natural"

This is the crux of the issue, I guess.

You _don't_ feel the pain of writing something _wrong_
when you type

  reserve A for set;
  reserve x for Element of A;

?  You don't feel the nagging irritation of that when A
happens to be empty, then x is being allowed to somehow
_incorrectly_ be the empty set?

So I always angrily change the reservation of A to non
empty set in this case.  "I don't want to think about this
issue...  Who cares that what I prove is not as general as
it should be?"

It might be that without that change in the reservation of
A, I still would be able to make things work _by accident._
Because accidentally the empty set would fit what I would
be trying to prove.  But I don't want my theorems to be
true by an accident!  I want them to be true because they
are what they are.

Freek